engine/asttoctl.ml

   1 (*
   2  * Copyright 2010, INRIA, University of Copenhagen
   3  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
   4  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
   5  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   6  * This file is part of Coccinelle.
   7  *
   8  * Coccinelle is free software: you can redistribute it and/or modify
   9  * it under the terms of the GNU General Public License as published by
  10  * the Free Software Foundation, according to version 2 of the License.
  11  *
  12  * Coccinelle is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  19  *
  20  * The authors reserve the right to distribute this or future versions of
  21  * Coccinelle under other licenses.
  22  *)
  23
  24
  25 (*
  26  * Copyright 2010, INRIA, University of Copenhagen
  27  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
  28  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
  29  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
  30  * This file is part of Coccinelle.
  31  *
  32  * Coccinelle is free software: you can redistribute it and/or modify
  33  * it under the terms of the GNU General Public License as published by
  34  * the Free Software Foundation, according to version 2 of the License.
  35  *
  36  * Coccinelle is distributed in the hope that it will be useful,
  37  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  38  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  39  * GNU General Public License for more details.
  40  *
  41  * You should have received a copy of the GNU General Public License
  42  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  43  *
  44  * The authors reserve the right to distribute this or future versions of
  45  * Coccinelle under other licenses.
  46  *)
  47
  48
  49 (* true = don't see all matched nodes, only modified ones *)
  50 let onlyModif = ref true(*false*)
  51 (* set to true for line numbers in the output of ctl_engine *)
  52 let line_numbers = ref false
  53 (* if true, only eg if header is included in not for ...s *)
  54 let simple_get_end = ref false(*true*)
  55
  56 (* Question: where do we put the existential quantifier for or.  At the
  57 moment, let it float inwards. *)
  58
  59 (* nest shouldn't overlap with what comes after.  not checked for. *)
  60
  61 module Ast = Ast_cocci
  62 module V = Visitor_ast
  63 module CTL = Ast_ctl
  64 module FV = Free_vars
  65
  66 let warning s = Printf.fprintf stderr "warning: %s\n" s
  67
  68 type cocci_predicate = Lib_engine.predicate * string Ast_ctl.modif
  69 type formula =
  70     (cocci_predicate,string, Wrapper_ctl.info) Ast_ctl.generic_ctl
  71
  72
  73 let aftpred = (Lib_engine.After,CTL.Control)
  74 let retpred = (Lib_engine.Return,CTL.Control)
  75 let exitpred = (Lib_engine.ErrorExit,CTL.Control)
  76
  77 let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1
  78 let subset l1 l2 = List.for_all (function x -> List.mem x l2) l1
  79
  80 (* --------------------------------------------------------------------- *)
  81
  82 let rec drop_vs f =
  83   CTL.rewrap f
  84     (match CTL.unwrap f with
  85       CTL.False as x ->  x
  86     | CTL.True as x -> x
  87     | CTL.Pred(p) as x -> x
  88     | CTL.Not(phi) -> CTL.Not(drop_vs phi)
  89     | CTL.Exists(v,phi) ->
  90         (match CTL.unwrap phi with
  91           CTL.Pred((x,CTL.Modif v1)) when v = v1 -> CTL.Pred((x,CTL.Control))
  92         | _ -> CTL.Exists(v,drop_vs phi))
  93     | CTL.And(phi1,phi2) -> CTL.And(drop_vs phi1,drop_vs phi2)
  94     | CTL.Or(phi1,phi2) -> CTL.Or(drop_vs phi1,drop_vs phi2)
  95     | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(drop_vs phi1,drop_vs phi2)
  96     | CTL.Implies(phi1,phi2) -> CTL.Implies(drop_vs phi1,drop_vs phi2)
  97     | CTL.AF(dir,phi1,phi2) -> CTL.AF(dir,drop_vs phi1,drop_vs phi2)
  98     | CTL.AX(dir,phi) -> CTL.AX(dir,drop_vs phi)
  99     | CTL.AG(dir,phi) -> CTL.AG(dir,drop_vs phi)
 100     | CTL.AU(dir,phi1,phi2,phi3,phi4) ->
 101         CTL.AU(dir,drop_vs phi1,drop_vs phi2,drop_vs phi3,drop_vs phi4)
 102     | CTL.EF(dir,phi) -> CTL.EF(dir,drop_vs phi)
 103     | CTL.EX(dir,phi) -> CTL.EX(dir,drop_vs phi)
 104     | CTL.EG(dir,phi) -> CTL.EG(dir,drop_vs phi)
 105     | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,drop_vs phi1,drop_vs phi2)
 106     | CTL.Ref(v) as x -> x
 107     | CTL.Let(v,term1,body) -> CTL.Let(v,drop_vs term1,drop_vs body))
 108
 109 (* --------------------------------------------------------------------- *)
 110
 111 let wrap n ctl = (ctl,n)
 112
 113 let aftret =
 114   wrap 0 (CTL.Or(wrap 0 (CTL.Pred aftpred),wrap 0 (CTL.Pred exitpred)))
 115
 116 let wrapImplies n (x,y) = wrap n (CTL.Implies(x,y))
 117 let wrapExists n (x,y) = wrap n (CTL.Exists(x,y))
 118 let wrapAnd n (x,y) = wrap n (CTL.And(x,y))
 119 let wrapOr n (x,y) = wrap n (CTL.Or(x,y))
 120 let wrapSeqOr n (x,y) = wrap n (CTL.SeqOr(x,y))
 121 let wrapAU n (x,y) = wrap n (CTL.AU(CTL.FORWARD,x,y,drop_vs x,drop_vs y))
 122 let wrapEU n (x,y) = wrap n (CTL.EU(CTL.FORWARD,x,y))
 123 let wrapAX n (x) = wrap n (CTL.AX(CTL.FORWARD,x))
 124 let wrapBackAX n (x) = wrap n (CTL.AX(CTL.BACKWARD,x))
 125 let wrapEX n (x) = wrap n (CTL.EX(CTL.FORWARD,x))
 126 let wrapBackEX n (x) = wrap n (CTL.EX(CTL.BACKWARD,x))
 127 let wrapAG n (x) = wrap n (CTL.AG(CTL.FORWARD,x))
 128 let wrapEG n (x) = wrap n (CTL.EG(CTL.FORWARD,x))
 129 let wrapAF n (x) = wrap n (CTL.AF(CTL.FORWARD,x,drop_vs x))
 130 let wrapEF n (x) = wrap n (CTL.EF(CTL.FORWARD,x))
 131 let wrapNot n (x) = wrap n (CTL.Not(x))
 132 let wrapPred n (x) = wrap n (CTL.Pred(x))
 133 let wrapLet n (x,y,z) = wrap n (CTL.Let(x,y,z))
 134 let wrapRef n (x) = wrap n (CTL.Ref(x))
 135
 136 (* --------------------------------------------------------------------- *)
 137
 138 let get_option fn = function
 139     None -> None
 140   | Some x -> Some (fn x)
 141
 142 let get_list_option fn = function
 143     None -> []
 144   | Some x -> fn x
 145
 146 (* --------------------------------------------------------------------- *)
 147 (* --------------------------------------------------------------------- *)
 148 (* Eliminate OptStm *)
 149
 150 (* for optional thing with nothing after, should check that the optional thing
 151 never occurs.  otherwise the matching stops before it occurs *)
 152 let elim_opt =
 153   let mcode x = x in
 154   let donothing r k e = k e in
 155
 156   let fvlist l =
 157     List.fold_left Common.union_set [] (List.map Ast.get_fvs l) in
 158
 159   let rec dots_list unwrapped wrapped =
 160     match (unwrapped,wrapped) with
 161       ([],_) -> []
 162
 163     | (Ast.Dots(_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_) as u)::urest,
 164        d0::_::d1::rest)
 165     | (Ast.Nest(_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_) as u)::urest,
 166        d0::_::d1::rest) ->
 167          let l = Ast.get_line stm in
 168          let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in
 169          let new_rest2 = dots_list urest rest in
 170          let fv_rest1 = fvlist new_rest1 in
 171          let fv_rest2 = fvlist new_rest2 in
 172          [d0;(Ast.Disj[(Ast.DOTS(new_rest1),l,fv_rest1,Ast.NoDots);
 173                         (Ast.DOTS(new_rest2),l,fv_rest2,Ast.NoDots)],
 174               l,fv_rest1,Ast.NoDots)]
 175
 176     | (Ast.OptStm(stm)::urest,_::rest) ->
 177          let l = Ast.get_line stm in
 178          let new_rest1 = dots_list urest rest in
 179          let new_rest2 = stm::new_rest1 in
 180          let fv_rest1 = fvlist new_rest1 in
 181          let fv_rest2 = fvlist new_rest2 in
 182          [(Ast.Disj[(Ast.DOTS(new_rest2),l,fv_rest2,Ast.NoDots);
 183                      (Ast.DOTS(new_rest1),l,fv_rest1,Ast.NoDots)],
 184            l,fv_rest2,Ast.NoDots)]
 185
 186     | ([Ast.Dots(_,_,_);Ast.OptStm(stm)],[d1;_]) ->
 187         let l = Ast.get_line stm in
 188         let fv_stm = Ast.get_fvs stm in
 189         let fv_d1 = Ast.get_fvs d1 in
 190         let fv_both = Common.union_set fv_stm fv_d1 in
 191         [d1;(Ast.Disj[(Ast.DOTS([stm]),l,fv_stm,Ast.NoDots);
 192                        (Ast.DOTS([d1]),l,fv_d1,Ast.NoDots)],
 193              l,fv_both,Ast.NoDots)]
 194
 195     | ([Ast.Nest(_,_,_);Ast.OptStm(stm)],[d1;_]) ->
 196         let l = Ast.get_line stm in
 197         let rw = Ast.rewrap stm in
 198         let rwd = Ast.rewrap stm in
 199         let dots =
 200           Ast.Dots(("...",{ Ast.line = 0; Ast.column = 0 },
 201                     Ast.CONTEXT(Ast.NOTHING)),
 202                    Ast.NoWhen,[]) in
 203         [d1;rw(Ast.Disj[rwd(Ast.DOTS([stm]));
 204                          (Ast.DOTS([rw dots]),l,[],Ast.NoDots)])]
 205
 206     | (_::urest,stm::rest) -> stm :: (dots_list urest rest)
 207     | _ -> failwith "not possible" in
 208
 209   let stmtdotsfn r k d =
 210     let d = k d in
 211     Ast.rewrap d
 212       (match Ast.unwrap d with
 213         Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l)
 214       | Ast.CIRCLES(l) -> failwith "elimopt: not supported"
 215       | Ast.STARS(l) -> failwith "elimopt: not supported") in
 216
 217   V.rebuilder
 218     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
 219     donothing donothing stmtdotsfn
 220     donothing donothing donothing donothing donothing donothing donothing
 221     donothing donothing donothing
 222
 223 (* --------------------------------------------------------------------- *)
 224 (* Count depth of braces.  The translation of a closed brace appears deeply
 225 nested within the translation of the sequence term, so the name of the
 226 paren var has to take into account the names of the nested braces.  On the
 227 other hand the close brace does not escape, so we don't have to take into
 228 account other paren variable names. *)
 229
 230 (* called repetitively, which is inefficient, but less trouble than adding a
 231 new field to Seq and FunDecl *)
 232 let count_nested_braces s =
 233   let bind x y = max x y in
 234   let option_default = 0 in
 235   let stmt_count r k s =
 236     match Ast.unwrap s with
 237       Ast.Seq(_,_,_,_,_) | Ast.FunDecl(_,_,_,_,_,_) -> (k s) + 1
 238     | _ -> k s in
 239   let donothing r k e = k e in
 240   let mcode r x = 0 in
 241   let recursor = V.combiner bind option_default
 242       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
 243       donothing donothing donothing
 244       donothing donothing donothing donothing donothing donothing
 245       donothing stmt_count donothing donothing in
 246   "p"^(string_of_int (recursor.V.combiner_statement s))
 247
 248 (* --------------------------------------------------------------------- *)
 249 (* Top-level code *)
 250
 251 let ctr = ref 0
 252 let fresh_var _ =
 253   let c = !ctr in
 254   (*ctr := !ctr + 1;*)
 255   Printf.sprintf "v%d" c
 256
 257 let labctr = ref 0
 258 let fresh_label_var s =
 259   let c = !labctr in
 260   labctr := !labctr + 1;
 261   Printf.sprintf "%s%d" s c
 262
 263 let lctr = ref 0
 264 let fresh_let_var _ =
 265   let c = !lctr in
 266   lctr := !lctr + 1;
 267   Printf.sprintf "l%d" c
 268
 269 let sctr = ref 0
 270 let fresh_metavar _ =
 271   let c = !sctr in
 272 (*sctr := !sctr + 1;*)
 273   Printf.sprintf "_S%d" c
 274
 275 let get_unquantified quantified vars =
 276   List.filter (function x -> not (List.mem x quantified)) vars
 277
 278 type after = After of formula | Guard of formula | Tail
 279
 280 let make_seq n l =
 281   let rec loop = function
 282       [] -> failwith "not possible"
 283     | [x] -> x
 284     | x::xs -> wrapAnd n (x,wrapAX n (loop xs)) in
 285   loop l
 286
 287 let make_seq_after2 n first = function
 288     After rest -> wrapAnd n (first,wrapAX n (wrapAX n rest))
 289   | _ -> first
 290
 291 let make_seq_after n first = function
 292     After rest -> make_seq n [first;rest]
 293   | _ -> first
 294
 295 let a2n = function After f -> Guard f | x -> x
 296
 297 let and_opt n first = function
 298     After rest -> wrapAnd n (first,rest)
 299   | _ -> first
 300
 301 let contains_modif =
 302   let bind x y = x or y in
 303   let option_default = false in
 304   let mcode r (_,_,kind) =
 305     match kind with
 306       Ast.MINUS(_) -> true
 307     | Ast.PLUS -> failwith "not possible"
 308     | Ast.CONTEXT(info) -> not (info = Ast.NOTHING) in
 309   let do_nothing r k e = k e in
 310   let recursor =
 311     V.combiner bind option_default
 312       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
 313       do_nothing do_nothing do_nothing
 314       do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
 315       do_nothing do_nothing do_nothing do_nothing in
 316   recursor.V.combiner_rule_elem
 317
 318 let make_match n guard used_after code =
 319   if guard
 320   then wrapPred n (Lib_engine.Match(code),CTL.Control)
 321   else
 322     let v = fresh_var() in
 323     if contains_modif code
 324     then wrapExists n (v,wrapPred n (Lib_engine.Match(code),CTL.Modif v))
 325     else
 326       let any_used_after =
 327         List.exists (function x -> List.mem x used_after) (Ast.get_fvs code) in
 328       if !onlyModif && not any_used_after
 329       then wrapPred n (Lib_engine.Match(code),CTL.Control)
 330       else wrapExists n (v,wrapPred n (Lib_engine.Match(code),CTL.UnModif v))
 331
 332 let make_raw_match n code = wrapPred n (Lib_engine.Match(code),CTL.Control)
 333
 334 let rec seq_fvs quantified = function
 335     [] -> []
 336   | fv1::fvs ->
 337       let t1fvs = get_unquantified quantified fv1 in
 338       let termfvs =
 339         List.fold_left Common.union_set []
 340           (List.map (get_unquantified quantified) fvs) in
 341       let bothfvs = Common.inter_set t1fvs termfvs in
 342       let t1onlyfvs = Common.minus_set t1fvs bothfvs in
 343       let new_quantified = Common.union_set bothfvs quantified in
 344       (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs)
 345
 346 let seq_fvs2 quantified fv1 fv2 =
 347   match seq_fvs quantified [fv1;fv2] with
 348     [(t1fvs,bfvs);(t2fvs,[])] -> (t1fvs,bfvs,t2fvs)
 349   | _ -> failwith "impossible"
 350
 351 let seq_fvs3 quantified fv1 fv2 fv3 =
 352   match seq_fvs quantified [fv1;fv2;fv3] with
 353     [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,[])] ->
 354       (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs)
 355   | _ -> failwith "impossible"
 356
 357 let seq_fvs4 quantified fv1 fv2 fv3 fv4 =
 358   match seq_fvs quantified [fv1;fv2;fv3;fv4] with
 359     [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,b34fvs);(t4fvs,[])] ->
 360       (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs,b34fvs,t4fvs)
 361   | _ -> failwith "impossible"
 362
 363 let seq_fvs5 quantified fv1 fv2 fv3 fv4 fv5 =
 364   match seq_fvs quantified [fv1;fv2;fv3;fv4;fv5] with
 365     [(t1fvs,b12fvs);(t2fvs,b23fvs);(t3fvs,b34fvs);(t4fvs,b45fvs);(t5fvs,[])] ->
 366       (t1fvs,b12fvs,t2fvs,b23fvs,t3fvs,b34fvs,t4fvs,b45fvs,t5fvs)
 367   | _ -> failwith "impossible"
 368
 369 let quantify n =
 370   List.fold_right (function cur -> function code -> wrapExists n (cur,code))
 371
 372 let intersectll lst nested_list =
 373   List.filter (function x -> List.exists (List.mem x) nested_list) lst
 374
 375 (* --------------------------------------------------------------------- *)
 376 (* annotate dots with before and after neighbors *)
 377
 378 let rec get_before sl a =
 379   match Ast.unwrap sl with
 380     Ast.DOTS(x) ->
 381       let rec loop sl a =
 382         match sl with
 383           [] -> ([],a)
 384         | e::sl ->
 385             let (e,ea) = get_before_e e a in
 386             let (sl,sla) = loop sl ea in
 387             (e::sl,sla) in
 388       let (l,a) = loop x a in
 389       (Ast.rewrap sl (Ast.DOTS(l)),a)
 390   | Ast.CIRCLES(x) -> failwith "not supported"
 391   | Ast.STARS(x) -> failwith "not supported"
 392
 393 and get_before_e s a =
 394   match Ast.unwrap s with
 395     Ast.Dots(d,Ast.NoWhen,t) ->
 396       (Ast.rewrap s (Ast.Dots(d,Ast.NoWhen,a@t)),a)
 397   | Ast.Dots(d,Ast.WhenNot w,t) ->
 398       let (w,_) = get_before w [] in
 399       (Ast.rewrap s (Ast.Dots(d,Ast.WhenNot w,a@t)),a)
 400   | Ast.Dots(d,Ast.WhenAlways w,t) ->
 401       let (w,_) = get_before_e w [] in
 402       (Ast.rewrap s (Ast.Dots(d,Ast.WhenAlways w,a@t)),a)
 403   | Ast.Nest(stmt_dots,w,t) ->
 404       let (w,_) = List.split (List.map (function s -> get_before s []) w) in
 405       let (sd,_) = get_before stmt_dots a in
 406       let a =
 407         List.filter
 408           (function
 409               Ast.Other a ->
 410                 let unifies =
 411                   Unify_ast.unify_statement_dots
 412                     (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
 413                 (match unifies with
 414                   Unify_ast.MAYBE -> false
 415                 | _ -> true)
 416             | Ast.Other_dots a ->
 417                 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
 418                 (match unifies with
 419                   Unify_ast.MAYBE -> false
 420                 | _ -> true)
 421             | _ -> true)
 422           a in
 423       (Ast.rewrap s (Ast.Nest(sd,w,a@t)),[Ast.Other_dots stmt_dots])
 424   | Ast.Disj(stmt_dots_list) ->
 425       let (dsl,dsla) =
 426         List.split (List.map (function e -> get_before e a) stmt_dots_list) in
 427       (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
 428   | Ast.Atomic(ast) ->
 429       (match Ast.unwrap ast with
 430         Ast.MetaStmt(_,_,_) -> (s,[])
 431       | _ -> (s,[Ast.Other s]))
 432   | Ast.Seq(lbrace,decls,dots,body,rbrace) ->
 433       let index = count_nested_braces s in
 434       let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
 435       let (bd,_) = get_before body dea in
 436       (Ast.rewrap s (Ast.Seq(lbrace,de,dots,bd,rbrace)),
 437        [Ast.WParen(rbrace,index)])
 438   | Ast.IfThen(ifheader,branch,aft) ->
 439       let (br,_) = get_before_e branch [] in
 440       (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s])
 441   | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
 442       let (br1,_) = get_before_e branch1 [] in
 443       let (br2,_) = get_before_e branch2 [] in
 444       (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
 445   | Ast.While(header,body,aft) ->
 446       let (bd,_) = get_before_e body [] in
 447       (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
 448   | Ast.For(header,body,aft) ->
 449       let (bd,_) = get_before_e body [] in
 450       (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
 451   | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) ->
 452       let index = count_nested_braces s in
 453       let (de,dea) = get_before decls [Ast.WParen(lbrace,index)] in
 454       let (bd,_) = get_before body dea in
 455       (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,dots,bd,rbrace)),[])
 456   | _ -> failwith "not supported"
 457
 458 let rec get_after sl a =
 459   match Ast.unwrap sl with
 460     Ast.DOTS(x) ->
 461       let rec loop sl =
 462         match sl with
 463           [] -> ([],a)
 464         | e::sl ->
 465             let (sl,sla) = loop sl in
 466             let (e,ea) = get_after_e e sla in
 467             (e::sl,ea) in
 468       let (l,a) = loop x in
 469       (Ast.rewrap sl (Ast.DOTS(l)),a)
 470   | Ast.CIRCLES(x) -> failwith "not supported"
 471   | Ast.STARS(x) -> failwith "not supported"
 472
 473 and get_after_e s a =
 474   match Ast.unwrap s with
 475     Ast.Dots(d,Ast.NoWhen,t) ->
 476       (Ast.rewrap s (Ast.Dots(d,Ast.NoWhen,a@t)),a)
 477   | Ast.Dots(d,Ast.WhenNot w,t) ->
 478       let (w,_) = get_after w [] in
 479       (Ast.rewrap s (Ast.Dots(d,Ast.WhenNot w,a@t)),a)
 480   | Ast.Dots(d,Ast.WhenAlways w,t) ->
 481       let (w,_) = get_after_e w [] in
 482       (Ast.rewrap s (Ast.Dots(d,Ast.WhenAlways w,a@t)),a)
 483   | Ast.Nest(stmt_dots,w,t) ->
 484       let (w,_) = List.split (List.map (function s -> get_after s []) w) in
 485       let (sd,_) = get_after stmt_dots a in
 486       let a =
 487         List.filter
 488           (function
 489               Ast.Other a ->
 490                 let unifies =
 491                   Unify_ast.unify_statement_dots
 492                     (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in
 493                 (match unifies with
 494                   Unify_ast.MAYBE -> false
 495                 | _ -> true)
 496             | Ast.Other_dots a ->
 497                 let unifies = Unify_ast.unify_statement_dots a stmt_dots in
 498                 (match unifies with
 499                   Unify_ast.MAYBE -> false
 500                 | _ -> true)
 501             | _ -> true)
 502           a in
 503       (Ast.rewrap s (Ast.Nest(sd,w,a@t)),[Ast.Other_dots stmt_dots])
 504   | Ast.Disj(stmt_dots_list) ->
 505       let (dsl,dsla) =
 506         List.split (List.map (function e -> get_after e a) stmt_dots_list) in
 507       (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla)
 508   | Ast.Atomic(ast) ->
 509       (match Ast.unwrap ast with
 510         Ast.MetaStmt(nm,Ast.SequencibleAfterDots _,i) ->
 511           (* check after information for metavar optimization *)
 512           (* if the error is not desired, could just return [], then
 513              the optimization (check for EF) won't take place *)
 514           List.iter
 515             (function
 516                 Ast.Other x ->
 517                   (match Ast.unwrap x with
 518                     Ast.Dots(_,_,_) | Ast.Nest(_,_,_) ->
 519                       failwith
 520                         "dots/nest not allowed before and after stmt metavar"
 521                   | _ -> ())
 522               | Ast.Other_dots x ->
 523                   (match Ast.undots x with
 524                     x::_ ->
 525                       (match Ast.unwrap x with
 526                         Ast.Dots(_,_,_) | Ast.Nest(_,_,_) ->
 527                           failwith
 528                             ("dots/nest not allowed before and after stmt "^
 529                              "metavar")
 530                       | _ -> ())
 531                   | _ -> ())
 532               | _ -> ())
 533             a;
 534           (Ast.rewrap s
 535              (Ast.Atomic
 536                 (Ast.rewrap s
 537                    (Ast.MetaStmt(nm,Ast.SequencibleAfterDots a,i)))),[])
 538       | Ast.MetaStmt(_,_,_) -> (s,[])
 539       | _ -> (s,[Ast.Other s]))
 540   | Ast.Seq(lbrace,decls,dots,body,rbrace) ->
 541       let index = count_nested_braces s in
 542       let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
 543       let (de,_) = get_after decls bda in
 544       (Ast.rewrap s (Ast.Seq(lbrace,de,dots,bd,rbrace)),
 545        [Ast.WParen(lbrace,index)])
 546   | Ast.IfThen(ifheader,branch,aft) ->
 547       let (br,_) = get_after_e branch a in
 548       (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s])
 549   | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
 550       let (br1,_) = get_after_e branch1 a in
 551       let (br2,_) = get_after_e branch2 a in
 552       (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])
 553   | Ast.While(header,body,aft) ->
 554       let (bd,_) = get_after_e body a in
 555       (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])
 556   | Ast.For(header,body,aft) ->
 557       let (bd,_) = get_after_e body a in
 558       (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])
 559   | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) ->
 560       let index = count_nested_braces s in
 561       let (bd,bda) = get_after body [Ast.WParen(rbrace,index)] in
 562       let (de,_) = get_after decls bda in
 563       (Ast.rewrap s (Ast.FunDecl(header,lbrace,de,dots,bd,rbrace)),[])
 564   | _ -> failwith "not supported"
 565
 566
 567 let preprocess_dots sl =
 568   let (sl,_) = get_before sl [] in
 569   let (sl,_) = get_after sl [] in
 570   sl
 571
 572 let preprocess_dots_e sl =
 573   let (sl,_) = get_before_e sl [] in
 574   let (sl,_) = get_after_e sl [] in
 575   sl
 576
 577 (* --------------------------------------------------------------------- *)
 578 (* the main translation loop *)
 579
 580 let decl_to_not_decl n dots stmt make_match f =
 581   if dots
 582   then f
 583   else
 584     let de =
 585       let md = Ast.make_meta_decl "_d" (Ast.CONTEXT(Ast.NOTHING)) in
 586       Ast.rewrap md (Ast.Decl md) in
 587     wrapAU n (make_match de,
 588               wrap n (CTL.And(wrap n (CTL.Not (make_match de)), f)))
 589
 590 let rec statement_list stmt_list used_after after quantified guard =
 591   let n = if !line_numbers then Ast.get_line stmt_list else 0 in
 592   match Ast.unwrap stmt_list with
 593     Ast.DOTS(x) ->
 594       let rec loop quantified = function
 595           ([],_) -> (match after with After f -> f | _ -> wrap n CTL.True)
 596         | ([e],_) -> statement e used_after after quantified guard
 597         | (e::sl,fv::fvs) ->
 598             let shared = intersectll fv fvs in
 599             let unqshared = get_unquantified quantified shared in
 600             let new_quantified = Common.union_set unqshared quantified in
 601             quantify n unqshared
 602               (statement e used_after (After(loop new_quantified (sl,fvs)))
 603                  new_quantified guard)
 604         | _ -> failwith "not possible" in
 605       loop quantified (x,List.map Ast.get_fvs x)
 606   | Ast.CIRCLES(x) -> failwith "not supported"
 607   | Ast.STARS(x) -> failwith "not supported"
 608
 609 and statement stmt used_after after quantified guard =
 610
 611   let n = if !line_numbers then Ast.get_line stmt else 0 in
 612   let wrapExists = wrapExists n in
 613   let wrapAnd = wrapAnd n in
 614   let wrapOr = wrapOr n in
 615   let wrapSeqOr = wrapSeqOr n in
 616   let wrapAU = wrapAU n in
 617   let wrapAX = wrapAX n in
 618   let wrapBackAX = wrapBackAX n in
 619   let wrapEX = wrapEX n in
 620   let wrapBackEX = wrapBackEX n in
 621   let wrapAG = wrapAG n in
 622   let wrapAF = wrapAF n in
 623   let wrapEF = wrapEF n in
 624   let wrapNot = wrapNot n in
 625   let wrapPred = wrapPred n in
 626   let make_seq = make_seq n in
 627   let make_seq_after2 = make_seq_after2 n in
 628   let make_seq_after = make_seq_after n in
 629   let and_opt = and_opt n in
 630   let quantify = quantify n in
 631   let make_match = make_match n guard used_after in
 632   let make_raw_match = make_raw_match n in
 633
 634   let make_meta_rule_elem d =
 635     let nm = fresh_metavar() in
 636     Ast.make_meta_rule_elem nm d in
 637
 638   match Ast.unwrap stmt with
 639     Ast.Atomic(ast) ->
 640       (match Ast.unwrap ast with
 641         Ast.MetaStmt((s,i,(Ast.CONTEXT(Ast.BEFOREAFTER(_,_)) as d)),seqible,_)
 642       | Ast.MetaStmt((s,i,(Ast.CONTEXT(Ast.AFTER(_)) as d)),seqible,_) ->
 643           let label_var = (*fresh_label_var*) "_lab" in
 644           let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in
 645           let prelabel_pred =
 646             wrapPred(Lib_engine.PrefixLabel(label_var),CTL.Control) in
 647           let matcher d = make_match (make_meta_rule_elem d) in
 648           let full_metamatch = matcher d in
 649           let first_metamatch =
 650             matcher
 651               (match d with
 652                 Ast.CONTEXT(Ast.BEFOREAFTER(bef,_)) ->
 653                   Ast.CONTEXT(Ast.BEFORE(bef))
 654               | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING)
 655               | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in
 656           let middle_metamatch =
 657             matcher
 658               (match d with
 659                 Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING)
 660               | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in
 661           let last_metamatch =
 662             matcher
 663               (match d with
 664                 Ast.CONTEXT(Ast.BEFOREAFTER(_,aft)) ->
 665                   Ast.CONTEXT(Ast.AFTER(aft))
 666               | Ast.CONTEXT(_) -> d
 667               | Ast.MINUS(_) | Ast.PLUS -> failwith "not possible") in
 668
 669           let left_or =
 670             make_seq
 671               [full_metamatch; and_opt (wrapNot(prelabel_pred)) after] in
 672           let right_or =
 673             make_seq
 674               [first_metamatch;
 675                 wrapAU(middle_metamatch,
 676                        make_seq
 677                          [wrapAnd(last_metamatch,label_pred);
 678                            and_opt (wrapNot(prelabel_pred)) after])] in
 679           let body f =
 680             wrapAnd(label_pred,
 681                     f (wrapAnd(make_raw_match ast,
 682                                wrapOr(left_or,right_or)))) in
 683           let id x = x in
 684           (match seqible with
 685             Ast.Sequencible | Ast.SequencibleAfterDots [] ->
 686               quantify (label_var::get_unquantified quantified [s])
 687                 (body
 688                    (function x ->
 689                      (wrapAnd(wrapNot(wrapBackAX(label_pred)),x))))
 690           | Ast.SequencibleAfterDots l ->
 691               let afts =
 692                 List.map (process_bef_aft Tail quantified used_after n) l in
 693               let ors =
 694                 List.fold_left (function x -> function y -> wrapOr(x,y))
 695                   (List.hd afts) (List.tl afts) in
 696               quantify (label_var::get_unquantified quantified [s])
 697                 (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))),
 698                          body
 699                            (function x ->
 700                              wrapAnd(wrapNot(wrapBackAX(label_pred)),x))))
 701           | Ast.NotSequencible ->
 702               quantify (label_var::get_unquantified quantified [s]) (body id))
 703
 704       | Ast.MetaStmt((s,i,d),seqible,_) ->
 705           let label_var = (*fresh_label_var*) "_lab" in
 706           let label_pred = wrapPred(Lib_engine.Label(label_var),CTL.Control) in
 707           let prelabel_pred =
 708             wrapPred(Lib_engine.PrefixLabel(label_var),CTL.Control) in
 709           let matcher d = make_match (make_meta_rule_elem d) in
 710           let first_metamatch = matcher d in
 711           let rest_metamatch =
 712             matcher
 713               (match d with
 714                 Ast.MINUS(_) -> Ast.MINUS([])
 715               | Ast.CONTEXT(_) -> Ast.CONTEXT(Ast.NOTHING)
 716               | Ast.PLUS -> failwith "not possible") in
 717           (* first_nodea and first_nodeb are separated here and above to
 718              improve let sharing - only first_nodea is unique to this site *)
 719           let first_nodeb = first_metamatch in
 720           let rest_nodes = wrapAnd(rest_metamatch,prelabel_pred) in
 721           let last_node = and_opt (wrapNot(prelabel_pred)) after in
 722           let body f =
 723             wrapAnd
 724               (label_pred,
 725                f (wrapAnd
 726                     (make_raw_match ast,
 727                      (make_seq
 728                         [first_nodeb; wrapAU(rest_nodes,last_node)])))) in
 729           (match seqible with
 730             Ast.Sequencible | Ast.SequencibleAfterDots [] ->
 731               quantify (label_var::get_unquantified quantified [s])
 732                 (body
 733                    (function x -> wrapAnd(wrapNot(wrapBackAX(label_pred)),x)))
 734           | Ast.SequencibleAfterDots l ->
 735               let afts =
 736                 List.map (process_bef_aft Tail quantified used_after n) l in
 737               let ors =
 738                 List.fold_left (function x -> function y -> wrapOr(x,y))
 739                   (List.hd afts) (List.tl afts) in
 740               quantify (label_var::get_unquantified quantified [s])
 741                 (wrapAnd(wrapEF(wrapAnd(ors,wrapBackAX(label_pred))),
 742                          body
 743                            (function x ->
 744                              wrapAnd(wrapNot(wrapBackAX(label_pred)),x))))
 745           | Ast.NotSequencible ->
 746               quantify (label_var::get_unquantified quantified [s])
 747                 (body (function x -> x)))
 748       | _ ->
 749           let stmt_fvs = Ast.get_fvs stmt in
 750           let fvs = get_unquantified quantified stmt_fvs in
 751           let between_dots = Ast.get_dots_bef_aft stmt in
 752           let term = make_match ast in
 753           let term =
 754             match between_dots with
 755               Ast.BetweenDots brace_term ->
 756                 (match Ast.unwrap brace_term with
 757                   Ast.Atomic(brace_ast) ->
 758                     let case1 =
 759                       wrapAnd
 760                         (wrapOr
 761                            (wrapBackEX
 762                               (wrapPred(Lib_engine.TrueBranch,CTL.Control)),
 763                             wrapBackEX
 764                               (wrapBackEX(wrapPred(Lib_engine.FalseBranch,
 765                                                    CTL.Control)))),
 766                          make_match brace_ast) in
 767                     let case2 =
 768                       wrapAnd
 769                         (wrapNot
 770                            (wrapOr
 771                               (wrapBackEX
 772                                  (wrapPred(Lib_engine.TrueBranch,CTL.Control)),
 773                                wrapBackEX
 774                                  (wrapBackEX(wrapPred(Lib_engine.FalseBranch,
 775                                                       CTL.Control))))),
 776                          term) in
 777                     wrapOr(case1,case2)
 778                 | _ -> failwith "not possible")
 779             | Ast.NoDots -> term in
 780           make_seq_after (quantify fvs term) after)
 781   | Ast.Seq(lbrace,decls,dots,body,rbrace) ->
 782       let (lbfvs,b1fvs,_,b2fvs,_,b3fvs,rbfvs) =
 783         seq_fvs4 quantified
 784           (Ast.get_fvs lbrace) (Ast.get_fvs decls)
 785           (Ast.get_fvs body) (Ast.get_fvs rbrace) in
 786       let v = count_nested_braces stmt in
 787       let paren_pred = wrapPred(Lib_engine.Paren v,CTL.Control) in
 788       let start_brace =
 789         wrapAnd(quantify lbfvs (make_match lbrace),paren_pred) in
 790       let end_brace =
 791         wrapAnd(quantify rbfvs (make_match rbrace),paren_pred) in
 792       let new_quantified2 =
 793         Common.union_set b1fvs (Common.union_set b2fvs quantified) in
 794       let new_quantified3 = Common.union_set b3fvs new_quantified2 in
 795       wrapExists
 796         (v,quantify b1fvs
 797            (make_seq
 798               [start_brace;
 799                 quantify b2fvs
 800                   (statement_list decls used_after
 801                      (After
 802                         (decl_to_not_decl n dots stmt make_match
 803                            (quantify b3fvs
 804                               (statement_list body used_after
 805                                  (After (make_seq_after end_brace after))
 806                                  new_quantified3 guard))))
 807                      new_quantified2 guard)]))
 808   | Ast.IfThen(ifheader,branch,aft) ->
 809
 810 (* "if (test) thn" becomes:
 811     if(test) & AX((TrueBranch & AX thn) v FallThrough v After)
 812
 813     "if (test) thn; after" becomes:
 814     if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
 815              & EX After
 816 *)
 817
 818        (* free variables *)
 819        let (efvs,bfvs,_) =
 820          seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch) in
 821        let new_quantified = Common.union_set bfvs quantified in
 822        (* if header *)
 823        let if_header = quantify efvs (make_match ifheader) in
 824        (* then branch and after *)
 825        let true_branch =
 826          make_seq
 827            [wrapPred(Lib_engine.TrueBranch,CTL.Control);
 828              statement branch used_after (a2n after) new_quantified guard] in
 829        let fall_branch =  wrapPred(Lib_engine.FallThrough,CTL.Control) in
 830        let after_pred = wrapPred(Lib_engine.After,CTL.Control) in
 831        let (aft_needed,after_branch) =
 832          match aft with
 833            Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after)
 834          | _ ->
 835              (true,
 836               make_seq_after after_pred
 837                 (After
 838                    (make_seq_after (make_match (make_meta_rule_elem aft))
 839                       after))) in
 840        let or_cases = wrapOr(true_branch,wrapOr(fall_branch,after_branch)) in
 841        (* the code *)
 842        (match (after,aft_needed) with
 843          (After _,_) (* pattern doesn't end here *)
 844        | (_,true) (* + code added after *) ->
 845            quantify bfvs
 846              (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
 847        | _ -> quantify bfvs (wrapAnd(if_header, wrapAX or_cases)))
 848
 849   | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) ->
 850
 851 (*  "if (test) thn else els" becomes:
 852     if(test) & AX((TrueBranch & AX thn) v
 853                   (FalseBranch & AX (else & AX els)) v After)
 854              & EX FalseBranch
 855
 856     "if (test) thn else els; after" becomes:
 857     if(test) & AX((TrueBranch & AX thn) v
 858                   (FalseBranch & AX (else & AX els)) v
 859                   (After & AXAX after))
 860              & EX FalseBranch
 861              & EX After
 862
 863
 864  Note that we rely on the well-formedness of C programs.  For example, we
 865  do not use EX to check that there is at least one then branch, because
 866  there is always one.  And we do not check that there is only one then or
 867  else branch, because these again are always the case in a well-formed C
 868  program. *)
 869        (* free variables *)
 870        let (e1fvs,b1fvs,s1fvs) =
 871          seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch1) in
 872        let (e2fvs,b2fvs,s2fvs) =
 873          seq_fvs2 quantified (Ast.get_fvs ifheader) (Ast.get_fvs branch2) in
 874        let bothfvs =
 875          Common.union_set
 876            (Common.union_set b1fvs b2fvs)
 877            (Common.inter_set s1fvs s2fvs) in
 878        let exponlyfvs = Common.inter_set e1fvs e2fvs in
 879        let new_quantified = Common.union_set bothfvs quantified in
 880        (* if header *)
 881        let if_header = quantify exponlyfvs (make_match ifheader) in
 882        (* then and else branches *)
 883        let true_branch =
 884          make_seq
 885            [wrapPred(Lib_engine.TrueBranch,CTL.Control);
 886              statement branch1 used_after (a2n after) new_quantified guard] in
 887        let false_pred = wrapPred(Lib_engine.FalseBranch,CTL.Control) in
 888        let false_branch =
 889            make_seq
 890            [false_pred; make_match els;
 891              statement branch2 used_after (a2n after) new_quantified guard] in
 892        let after_pred = wrapPred(Lib_engine.After,CTL.Control) in
 893        let (aft_needed,after_branch) =
 894          match aft with
 895            Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after)
 896          | _ ->
 897              (true,
 898               make_seq_after after_pred
 899                 (After
 900                    (make_seq_after (make_match (make_meta_rule_elem aft))
 901                       after))) in
 902        let or_cases = wrapOr(true_branch,wrapOr(false_branch,after_branch)) in
 903        (* the code *)
 904        (match (after,aft_needed) with
 905          (After _,_) (* pattern doesn't end here *)
 906        | (_,true) (* + code added after *) ->
 907           quantify bothfvs
 908             (wrapAnd
 909                (if_header,
 910                  wrapAnd(wrapAX or_cases,
 911                          wrapAnd(wrapEX false_pred,wrapEX after_pred))))
 912       | _ ->
 913           quantify bothfvs
 914             (wrapAnd (if_header, wrapAnd(wrapAX or_cases, wrapEX false_pred))))
 915
 916   | Ast.While(header,body,aft) | Ast.For(header,body,aft) ->
 917    (* the translation in this case is similar to that of an if with no else *)
 918        (* free variables *)
 919       let (efvs,bfvs,_) =
 920         seq_fvs2 quantified (Ast.get_fvs header) (Ast.get_fvs body) in
 921       let new_quantified = Common.union_set bfvs quantified in
 922       (* if header *)
 923       let header = quantify efvs (make_match header) in
 924       let body =
 925         make_seq
 926           [wrapPred(Lib_engine.TrueBranch,CTL.Control);
 927             statement body used_after (a2n after) new_quantified guard] in
 928       let after_pred = wrapPred(Lib_engine.FallThrough,CTL.Control) in
 929       let (aft_needed,after_branch) =
 930         match aft with
 931           Ast.CONTEXT(Ast.NOTHING) -> (false,make_seq_after2 after_pred after)
 932         | _ ->
 933             (true,
 934              make_seq_after after_pred
 935                (After
 936                   (make_seq_after (make_match (make_meta_rule_elem aft))
 937                      after))) in
 938       let or_cases = wrapOr(body,after_branch) in
 939       (* the code *)
 940       (match (after,aft_needed) with
 941         (After _,_) (* pattern doesn't end here *)
 942       | (_,true) (* + code added after *) ->
 943           quantify bfvs
 944             (wrapAnd (header, wrapAnd(wrapAX or_cases, wrapEX after_pred)))
 945       | _ -> quantify bfvs (wrapAnd(header, wrapAX or_cases)))
 946
 947   | Ast.Disj(stmt_dots_list) ->
 948       let processed =
 949         List.map
 950           (function x -> statement_list x used_after after quantified guard)
 951           stmt_dots_list in
 952       let rec loop = function
 953           [] -> wrap n CTL.True
 954         | [x] -> x
 955         | x::xs -> wrapSeqOr(x,loop xs) in
 956       loop processed
 957 (*
 958       let do_one e =
 959         statement_list e used_after (a2n after) quantified true in
 960       let add_nots l e =
 961         List.fold_left
 962           (function rest -> function cur -> wrapAnd(wrapNot(do_one cur),rest))
 963           e l in
 964       let process_one nots cur =
 965         match Ast.unwrap cur with
 966           Ast.DOTS(x::xs) ->
 967             let on = List.map (function x -> Ast.OrOther_dots x) nots in
 968             (match Ast.unwrap x with
 969               Ast.Dots(d,w,t) ->
 970                 List.iter
 971                   (function x ->
 972                     Printf.printf "a not\n";
 973                     Pretty_print_cocci.statement_dots x)
 974                   nots;
 975                 let cur =
 976                   Ast.rewrap cur
 977                     (Ast.DOTS((Ast.rewrap x (Ast.Dots(d,w,on@t)))::xs)) in
 978                 statement_list cur used_after after quantified guard
 979             | Ast.Nest(sd,w,t) ->
 980                 let cur =
 981                   Ast.rewrap cur
 982                     (Ast.DOTS((Ast.rewrap x (Ast.Nest(sd,w,on@t)))::xs)) in
 983                 statement_list cur used_after after quantified guard
 984             | _ ->
 985                 add_nots nots
 986                   (statement_list cur used_after after quantified guard))
 987         | Ast.DOTS([]) ->
 988             add_nots nots
 989               (statement_list cur used_after after quantified guard)
 990         | _ -> failwith "CIRCLES, STARS not supported" in
 991       let rec loop after = function
 992           [] -> failwith "disj shouldn't be empty" (*wrap n CTL.False*)
 993         | [(nots,cur)] -> process_one nots cur
 994         | (nots,cur)::rest -> wrapOr(process_one nots cur, loop after rest) in
 995       loop after (preprocess_disj stmt_dots_list)
 996 *)
 997   | Ast.Nest(stmt_dots,whencode,befaft) ->
 998       let dots_pattern =
 999         statement_list stmt_dots used_after (a2n after) quantified guard in
1000       let udots_pattern =
1001         let whencodes =
1002           List.map
1003             (function sl ->
1004               statement_list sl used_after (a2n after) quantified true)
1005             whencode in
1006         List.fold_left (function rest -> function cur -> wrapOr(cur,rest))
1007           (statement_list stmt_dots used_after (a2n after) quantified true)
1008           whencodes in
1009       (match (after,guard&&(whencode=[])) with
1010         (After a,true) ->
1011           let nots =
1012             List.map (process_bef_aft after quantified used_after n) befaft in
1013           (match nots with
1014             [] -> wrapAF(wrapOr(a,aftret))
1015           | x::xs ->
1016               let left =
1017                 wrapNot
1018                   (List.fold_left
1019                      (function rest -> function cur -> wrapOr(cur,rest))
1020                      x xs) in
1021               wrapAU(left,wrapOr(a,aftret)))
1022       | (After a,false) ->
1023           let left = wrapOr(dots_pattern,wrapNot udots_pattern) in
1024           let nots =
1025             List.map (process_bef_aft after quantified used_after n) befaft in
1026           let left =
1027             match nots with
1028               [] -> left
1029             | x::xs ->
1030                 wrapAnd
1031                   (wrapNot
1032                      (List.fold_left
1033                         (function rest -> function cur -> wrapOr(cur,rest))
1034                         x xs),
1035                    left) in
1036           wrapAU(left,wrapOr(a,aftret))
1037       | (_,true) -> wrap n CTL.True
1038       | (_,false) -> wrapAG(wrapOr(dots_pattern,wrapNot udots_pattern)))
1039   | Ast.Dots((_,i,d),whencodes,t) ->
1040       let dot_code =
1041         match d with
1042           Ast.MINUS(_) ->
1043             (* no need for the fresh metavar, but ... is a bit weird as a
1044                variable name *)
1045             Some(make_match (make_meta_rule_elem d))
1046         | _ -> None in
1047       let whencodes =
1048         (match whencodes with
1049           Ast.NoWhen -> []
1050         | Ast.WhenNot whencodes ->
1051             [wrapNot
1052                 (statement_list whencodes used_after (a2n after) quantified
1053                    true)]
1054         | Ast.WhenAlways s ->
1055             [statement s used_after (a2n after) quantified true]) @
1056         (List.map wrapNot
1057            (List.map (process_bef_aft after quantified used_after n) t)) in
1058       let phi2 =
1059         match whencodes with
1060           [] -> None
1061         | x::xs ->
1062             Some
1063               (List.fold_left
1064                  (function rest -> function cur -> wrapAnd(cur,rest))
1065                  x xs) in
1066       let phi3 =
1067         match (dot_code,phi2) with (* add - on dots, if any *)
1068           (None,None) -> None
1069         | (Some dotcode,None) -> Some dotcode
1070         | (None,Some whencode) -> Some whencode
1071         | (Some dotcode,Some whencode) -> Some(wrapAnd (dotcode,whencode)) in
1072       let exit = wrap n (CTL.Pred (Lib_engine.Exit,CTL.Control)) in
1073       (* add in the after code to make the result *)
1074       (match (after,phi3) with
1075         (Tail,Some whencode) -> wrapAU(whencode,wrapOr(exit,aftret))
1076       | (Tail,None) -> wrapAF(wrapOr(exit,aftret))
1077       | (After f,Some whencode) | (Guard f,Some whencode) ->
1078           wrapAU(whencode,wrapOr(f,aftret))
1079       | (After f,None) | (Guard f,None) -> wrapAF(wrapOr(f,aftret)))
1080   | Ast.FunDecl(header,lbrace,decls,dots,body,rbrace) ->
1081       let (hfvs,b1fvs,lbfvs,b2fvs,_,b3fvs,_,b4fvs,rbfvs) =
1082         seq_fvs5 quantified (Ast.get_fvs header) (Ast.get_fvs lbrace)
1083           (Ast.get_fvs decls) (Ast.get_fvs body) (Ast.get_fvs rbrace) in
1084       let function_header = quantify hfvs (make_match header) in
1085       let v = count_nested_braces stmt in
1086       let paren_pred = wrapPred(Lib_engine.Paren v,CTL.Control) in
1087       let start_brace =
1088         wrapAnd(quantify lbfvs (make_match lbrace),paren_pred) in
1089       let end_brace =
1090         let stripped_rbrace =
1091           match Ast.unwrap rbrace with
1092             Ast.SeqEnd((data,info,_)) ->
1093               Ast.rewrap rbrace
1094                 (Ast.SeqEnd ((data,info,Ast.CONTEXT(Ast.NOTHING))))
1095           | _ -> failwith "unexpected close brace" in
1096         let exit = wrap n (CTL.Pred (Lib_engine.Exit,CTL.Control)) in
1097         let errorexit = wrap n (CTL.Pred (Lib_engine.ErrorExit,CTL.Control)) in
1098         wrapAnd(quantify rbfvs (make_match rbrace),
1099                 wrapAU(make_match stripped_rbrace,
1100                        wrapOr(exit,errorexit))) in
1101       let new_quantified3 =
1102         Common.union_set b1fvs
1103           (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in
1104       let new_quantified4 = Common.union_set b4fvs new_quantified3 in
1105       quantify b1fvs
1106         (make_seq
1107            [function_header;
1108              wrapExists
1109                (v,
1110                 (quantify b2fvs
1111                    (make_seq
1112                       [start_brace;
1113                         quantify b3fvs
1114                           (statement_list decls used_after
1115                              (After
1116                                 (decl_to_not_decl n dots stmt
1117                                    make_match
1118                                    (quantify b4fvs
1119                                       (statement_list body used_after
1120                                          (After
1121                                             (make_seq_after end_brace after))
1122                                          new_quantified4 guard))))
1123                              new_quantified3 guard)])))])
1124   | Ast.OptStm(stm) ->
1125       failwith "OptStm should have been compiled away\n";
1126   | Ast.UniqueStm(stm) ->
1127       failwith "arities not yet supported"
1128   | Ast.MultiStm(stm) ->
1129       failwith "arities not yet supported"
1130   | _ -> failwith "not supported"
1131
1132 and process_bef_aft after quantified used_after ln = function
1133     Ast.WParen (re,n) ->
1134       let paren_pred = wrapPred ln (Lib_engine.Paren n,CTL.Control) in
1135       wrapAnd ln (make_raw_match ln re,paren_pred)
1136   | Ast.Other s -> statement s used_after (a2n after) quantified true
1137   | Ast.Other_dots d -> statement_list d used_after (a2n after) quantified true
1138   | Ast.OrOther_dots d -> statement_list d used_after Tail quantified true
1139
1140 (* Returns a triple for each disj element.  The first element of the triple is
1141 Some v if the triple element needs a name, and None otherwise.  The second
1142 element is a list of names whose negations should be conjuncted with the
1143 term.  The third element is the original term *)
1144 and (preprocess_disj :
1145        Ast.statement Ast.dots list ->
1146          (Ast.statement Ast.dots list * Ast.statement Ast.dots) list) =
1147   function
1148     [] -> []
1149   | [s] -> [([],s)]
1150   | cur::rest ->
1151       let template =
1152         List.map (function r -> Unify_ast.unify_statement_dots cur r) rest in
1153       let processed = preprocess_disj rest in
1154       if List.exists (function Unify_ast.MAYBE -> true | _ -> false) template
1155       then
1156         ([], cur) ::
1157         (List.map2
1158            (function ((nots,r) as x) ->
1159              function Unify_ast.MAYBE -> (cur::nots,r) | Unify_ast.NO -> x)
1160            processed template)
1161       else ([], cur) :: processed
1162
1163 (* --------------------------------------------------------------------- *)
1164 (* Letify:
1165 Phase 1: Use a hash table to identify formulas that appear more than once.
1166 Phase 2: Replace terms by variables.
1167 Phase 3: Drop lets to the point as close as possible to the uses of their
1168 variables *)
1169
1170 let formula_table =
1171   (Hashtbl.create(50) :
1172      ((cocci_predicate,string,Wrapper_ctl.info) CTL.generic_ctl,
1173       int ref (* count *) * string ref (* name *) * bool ref (* processed *))
1174      Hashtbl.t)
1175
1176 let add_hash phi =
1177   let (cell,_,_) =
1178     try Hashtbl.find formula_table phi
1179     with Not_found ->
1180       let c = (ref 0,ref "",ref false) in
1181       Hashtbl.add formula_table phi c;
1182       c in
1183   cell := !cell + 1
1184
1185 let rec collect_duplicates f =
1186   add_hash f;
1187   match CTL.unwrap f with
1188     CTL.False -> ()
1189   | CTL.True -> ()
1190   | CTL.Pred(p) -> ()
1191   | CTL.Not(phi) -> collect_duplicates phi
1192   | CTL.Exists(v,phi) -> collect_duplicates phi
1193   | CTL.And(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1194   | CTL.Or(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1195   | CTL.SeqOr(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1196   | CTL.Implies(phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1197   | CTL.AF(_,phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1198   | CTL.AX(_,phi) -> collect_duplicates phi
1199   | CTL.AG(_,phi) -> collect_duplicates phi
1200   | CTL.AU(_,phi1,phi2,phi3,phi4) ->
1201       collect_duplicates phi1; collect_duplicates phi2;
1202       collect_duplicates phi3; collect_duplicates phi4
1203   | CTL.EF(_,phi) -> collect_duplicates phi
1204   | CTL.EX(_,phi) -> collect_duplicates phi
1205   | CTL.EG(_,phi) -> collect_duplicates phi
1206   | CTL.EU(_,phi1,phi2) -> collect_duplicates phi1; collect_duplicates phi2
1207   | CTL.Uncheck(phi) -> collect_duplicates phi
1208   | _ -> failwith "not possible"
1209
1210 let assign_variables _ =
1211   Hashtbl.iter
1212     (function formula ->
1213       function (cell,str,_) -> if !cell > 1 then str := fresh_let_var())
1214     formula_table
1215
1216 let rec replace_formulas dec f =
1217   let (ct,name,treated) = Hashtbl.find formula_table f in
1218   let real_ct = !ct - dec in
1219   if real_ct > 1
1220   then
1221     if not !treated
1222     then
1223       begin
1224         treated := true;
1225         let (acc,new_f) = replace_subformulas (dec + (real_ct - 1)) f in
1226         ((!name,new_f) :: acc, CTL.rewrap f (CTL.Ref !name))
1227       end
1228     else ([],CTL.rewrap f (CTL.Ref !name))
1229   else replace_subformulas dec f
1230
1231 and replace_subformulas dec f =
1232   match CTL.unwrap f with
1233     CTL.False -> ([],f)
1234   | CTL.True -> ([],f)
1235   | CTL.Pred(p) -> ([],f)
1236   | CTL.Not(phi) ->
1237       let (acc,new_phi) = replace_formulas dec phi in
1238       (acc,CTL.rewrap f (CTL.Not(new_phi)))
1239   | CTL.Exists(v,phi) ->
1240       let (acc,new_phi) = replace_formulas dec phi in
1241       (acc,CTL.rewrap f (CTL.Exists(v,new_phi)))
1242   | CTL.And(phi1,phi2) ->
1243       let (acc1,new_phi1) = replace_formulas dec phi1 in
1244       let (acc2,new_phi2) = replace_formulas dec phi2 in
1245       (acc1@acc2,CTL.rewrap f (CTL.And(new_phi1,new_phi2)))
1246   | CTL.Or(phi1,phi2) ->
1247       let (acc1,new_phi1) = replace_formulas dec phi1 in
1248       let (acc2,new_phi2) = replace_formulas dec phi2 in
1249       (acc1@acc2,CTL.rewrap f (CTL.Or(new_phi1,new_phi2)))
1250   | CTL.SeqOr(phi1,phi2) ->
1251       let (acc1,new_phi1) = replace_formulas dec phi1 in
1252       let (acc2,new_phi2) = replace_formulas dec phi2 in
1253       (acc1@acc2,CTL.rewrap f (CTL.SeqOr(new_phi1,new_phi2)))
1254   | CTL.Implies(phi1,phi2) ->
1255       let (acc1,new_phi1) = replace_formulas dec phi1 in
1256       let (acc2,new_phi2) = replace_formulas dec phi2 in
1257       (acc1@acc2,CTL.rewrap f (CTL.Implies(new_phi1,new_phi2)))
1258   | CTL.AF(dir,phi1,phi2) ->
1259       let (acc,new_phi1) = replace_formulas dec phi1 in
1260       let (acc,new_phi2) = replace_formulas dec phi2 in
1261       (acc,CTL.rewrap f (CTL.AF(dir,new_phi1,new_phi2)))
1262   | CTL.AX(dir,phi) ->
1263       let (acc,new_phi) = replace_formulas dec phi in
1264       (acc,CTL.rewrap f (CTL.AX(dir,new_phi)))
1265   | CTL.AG(dir,phi) ->
1266       let (acc,new_phi) = replace_formulas dec phi in
1267       (acc,CTL.rewrap f (CTL.AG(dir,new_phi)))
1268   | CTL.AU(dir,phi1,phi2,phi3,phi4) ->
1269       let (acc1,new_phi1) = replace_formulas dec phi1 in
1270       let (acc2,new_phi2) = replace_formulas dec phi2 in
1271       let (acc3,new_phi3) = replace_formulas dec phi3 in
1272       let (acc4,new_phi4) = replace_formulas dec phi4 in
1273       (acc1@acc2@acc3@acc4,
1274        CTL.rewrap f (CTL.AU(dir,new_phi1,new_phi2,new_phi3,new_phi4)))
1275   | CTL.EF(dir,phi) ->
1276       let (acc,new_phi) = replace_formulas dec phi in
1277       (acc,CTL.rewrap f (CTL.EF(dir,new_phi)))
1278   | CTL.EX(dir,phi) ->
1279       let (acc,new_phi) = replace_formulas dec phi in
1280       (acc,CTL.rewrap f (CTL.EX(dir,new_phi)))
1281   | CTL.EG(dir,phi) ->
1282       let (acc,new_phi) = replace_formulas dec phi in
1283       (acc,CTL.rewrap f (CTL.EG(dir,new_phi)))
1284   | CTL.EU(dir,phi1,phi2) ->
1285       let (acc1,new_phi1) = replace_formulas dec phi1 in
1286       let (acc2,new_phi2) = replace_formulas dec phi2 in
1287       (acc1@acc2,CTL.rewrap f (CTL.EU(dir,new_phi1,new_phi2)))
1288   | _ -> failwith "not possible"
1289
1290 let ctlfv_table =
1291   (Hashtbl.create(50) :
1292      ((cocci_predicate,string,Wrapper_ctl.info) CTL.generic_ctl,
1293       string list (* fvs *) *
1294         string list (* intersection of fvs of subterms *))
1295      Hashtbl.t)
1296
1297 let rec ctl_fvs f =
1298   try let (fvs,_) = Hashtbl.find ctlfv_table f in fvs
1299   with Not_found ->
1300     let ((fvs,_) as res) =
1301       match CTL.unwrap f with
1302         CTL.False | CTL.True | CTL.Pred(_) -> ([],[])
1303       | CTL.Not(phi) | CTL.Exists(_,phi)
1304       | CTL.AX(_,phi) | CTL.AG(_,phi)
1305       | CTL.EF(_,phi) | CTL.EX(_,phi) | CTL.EG(_,phi) -> (ctl_fvs phi,[])
1306       | CTL.AU(_,phi1,phi2,phi3,phi4) ->
1307           let phi1fvs = ctl_fvs phi1 in
1308           let phi2fvs = ctl_fvs phi2 in
1309           (* phi3 has the same fvs as phi1 and phi4 as phi2 *)
1310           (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs)
1311       | CTL.And(phi1,phi2) | CTL.Or(phi1,phi2) | CTL.SeqOr(phi1,phi2)
1312       | CTL.Implies(phi1,phi2) | CTL.AF(_,phi1,phi2) | CTL.EU(_,phi1,phi2) ->
1313           let phi1fvs = ctl_fvs phi1 in
1314           let phi2fvs = ctl_fvs phi2 in
1315           (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs)
1316       | CTL.Ref(v) -> ([v],[v])
1317       | CTL.Let(v,term,body) ->
1318           let phi1fvs = ctl_fvs term in
1319           let phi2fvs = Common.minus_set (ctl_fvs body) [v] in
1320           (Common.union_set phi1fvs phi2fvs,intersect phi1fvs phi2fvs) in
1321     Hashtbl.add ctlfv_table f res;
1322     fvs
1323
1324 let rev_order_bindings b =
1325   let b =
1326     List.map
1327       (function (nm,term) ->
1328         let (fvs,_) = Hashtbl.find ctlfv_table term in (nm,fvs,term))
1329       b in
1330   let rec loop bound = function
1331       [] -> []
1332     | unbound ->
1333         let (now_bound,still_unbound) =
1334           List.partition (function (_,fvs,_) -> subset fvs bound)
1335             unbound in
1336         let get_names = List.map (function (x,_,_) -> x) in
1337         now_bound @ (loop ((get_names now_bound) @ bound) still_unbound) in
1338   List.rev(loop [] b)
1339
1340 let drop_bindings b f = (* innermost bindings first in b *)
1341   let process_binary f ffvs inter nm term fail =
1342     if List.mem nm inter
1343     then CTL.rewrap f (CTL.Let(nm,term,f))
1344     else CTL.rewrap f (fail()) in
1345   let find_fvs f =
1346     let _ = ctl_fvs f in Hashtbl.find ctlfv_table f in
1347   let rec drop_one nm term f =
1348     match CTL.unwrap f with
1349       CTL.False ->  f
1350     | CTL.True -> f
1351     | CTL.Pred(p) -> f
1352     | CTL.Not(phi) -> CTL.rewrap f (CTL.Not(drop_one nm term phi))
1353     | CTL.Exists(v,phi) -> CTL.rewrap f (CTL.Exists(v,drop_one nm term phi))
1354     | CTL.And(phi1,phi2) ->
1355         let (ffvs,inter) = find_fvs f in
1356         process_binary f ffvs inter nm term
1357           (function _ -> CTL.And(drop_one nm term phi1,drop_one nm term phi2))
1358     | CTL.Or(phi1,phi2) ->
1359         let (ffvs,inter) = find_fvs f in
1360         process_binary f ffvs inter nm term
1361           (function _ -> CTL.Or(drop_one nm term phi1,drop_one nm term phi2))
1362     | CTL.SeqOr(phi1,phi2) ->
1363         let (ffvs,inter) = find_fvs f in
1364         process_binary f ffvs inter nm term
1365           (function _ ->
1366             CTL.SeqOr(drop_one nm term phi1,drop_one nm term phi2))
1367     | CTL.Implies(phi1,phi2) ->
1368         let (ffvs,inter) = find_fvs f in
1369         process_binary f ffvs inter nm term
1370           (function _ ->
1371             CTL.Implies(drop_one nm term phi1,drop_one nm term phi2))
1372     | CTL.AF(dir,phi1,phi2) ->
1373         let (ffvs,inter) = find_fvs f in
1374         process_binary f ffvs inter nm term
1375           (function _ ->
1376             CTL.AF(dir,drop_one nm term phi1,drop_one nm term phi2))
1377     | CTL.AX(dir,phi) ->
1378         CTL.rewrap f (CTL.AX(dir,drop_one nm term phi))
1379     | CTL.AG(dir,phi) -> CTL.rewrap f (CTL.AG(dir,drop_one nm term phi))
1380     | CTL.AU(dir,phi1,phi2,phi3,phi4) ->
1381         let (ffvs,inter) = find_fvs f in
1382         process_binary f ffvs inter nm term
1383           (function _ ->
1384             CTL.AU(dir,drop_one nm term phi1,drop_one nm term phi2,
1385                    drop_one nm term phi3,drop_one nm term phi4))
1386     | CTL.EF(dir,phi) -> CTL.rewrap f (CTL.EF(dir,drop_one nm term phi))
1387     | CTL.EX(dir,phi) ->
1388         CTL.rewrap f (CTL.EX(dir,drop_one nm term phi))
1389     | CTL.EG(dir,phi) -> CTL.rewrap f (CTL.EG(dir,drop_one nm term phi))
1390     | CTL.EU(dir,phi1,phi2) ->
1391         let (ffvs,inter) = find_fvs f in
1392         process_binary f ffvs inter nm term
1393           (function _ ->
1394             CTL.EU(dir,drop_one nm term phi1,drop_one nm term phi2))
1395     | (CTL.Ref(v) as x) -> process_binary f [v] [v] nm term (function _ -> x)
1396     | CTL.Let(v,term1,body) ->
1397         let (ffvs,inter) = find_fvs f in
1398         process_binary f ffvs inter nm term
1399           (function _ ->
1400             CTL.Let(v,drop_one nm term term1,drop_one nm term body)) in
1401   List.fold_left
1402     (function processed -> function (nm,_,term) -> drop_one nm term processed)
1403     f b
1404
1405 let letify f =
1406   failwith "this code should not be used!!!"(*;
1407   Hashtbl.clear formula_table;
1408   Hashtbl.clear ctlfv_table;
1409   (* create a count of the number of occurrences of each subformula *)
1410   collect_duplicates f;
1411   (* give names to things that appear more than once *)
1412   assign_variables();
1413   (* replace duplicated formulas by their variables *)
1414   let (bindings,new_f) = replace_formulas 0 f in
1415   (* collect fvs of terms in bindings and new_f *)
1416   List.iter (function f -> let _ = ctl_fvs f in ())
1417     (new_f::(List.map (function (_,term) -> term) bindings));
1418   (* sort bindings with uses before defs *)
1419   let bindings = rev_order_bindings bindings in
1420   (* insert bindings as lets into the formula *)
1421   let res = drop_bindings bindings new_f in
1422   res*)
1423
1424 (* --------------------------------------------------------------------- *)
1425 (* Function declaration *)
1426
1427 let top_level used_after t =
1428   match Ast.unwrap t with
1429     Ast.DECL(decl) -> failwith "not supported decl"
1430   | Ast.INCLUDE(inc,s) ->
1431       (* no indication of whether inc or s is modified *)
1432       wrap 0 (CTL.Pred((Lib_engine.Include(inc,s),CTL.Control)))
1433   | Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
1434   | Ast.FUNCTION(stmt) ->
1435       (*Printf.printf "orig\n";
1436       Pretty_print_cocci.statement "" stmt;
1437       Format.print_newline();*)
1438       let unopt = elim_opt.V.rebuilder_statement stmt in
1439       (*Printf.printf "unopt\n";
1440       Pretty_print_cocci.statement "" unopt;
1441       Format.print_newline();*)
1442       let unopt = preprocess_dots_e unopt in
1443       (*letify*)
1444         (statement unopt used_after Tail [] false)
1445   | Ast.CODE(stmt_dots) ->
1446       let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in
1447       let unopt = preprocess_dots unopt in
1448       (*letify*)
1449         (statement_list unopt used_after Tail [] false)
1450   | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords"
1451
1452 (* --------------------------------------------------------------------- *)
1453 (* Contains dots *)
1454
1455 let contains_dots =
1456   let bind x y = x or y in
1457   let option_default = false in
1458   let mcode r x = false in
1459   let statement r k s =
1460     match Ast.unwrap s with Ast.Dots(_,_,_) -> true | _ -> k s in
1461   let continue r k e = k e in
1462   let stop r k e = false in
1463   let res =
1464     V.combiner bind option_default
1465       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
1466       continue continue continue
1467       stop stop stop stop stop stop stop statement continue continue in
1468   res.V.combiner_top_level
1469
1470 (* --------------------------------------------------------------------- *)
1471 (* Entry points *)
1472
1473 let asttoctl l used_after =
1474   ctr := 0;
1475   lctr := 0;
1476   sctr := 0;
1477   let l =
1478     List.filter
1479       (function t ->
1480         match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
1481       l in
1482   List.map2 top_level used_after l
1483
1484 let pp_cocci_predicate (pred,modif) =
1485   Pretty_print_engine.pp_predicate pred
1486
1487 let cocci_predicate_to_string (pred,modif) =
1488   Pretty_print_engine.predicate_to_string pred