engine/asttoctl.ml

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