engine/asttoctl.ml

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