engine/asttoctl.ml

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