popl09/popltoctl.ml

   1 module Past = Ast_popl
   2 module Ast = Ast_cocci
   3 module V = Visitor_ast
   4 module CTL  = Ast_ctl
   5
   6 (* --------------------------------------------------------------------- *)
   7 (* result type *)
   8
   9 type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif
  10 type formula =
  11     (cocci_predicate,Ast_cocci.meta_name, Wrapper_ctl.info) Ast_ctl.generic_ctl
  12
  13 (* --------------------------------------------------------------------- *)
  14
  15 let contains_modif =
  16   let bind x y = x or y in
  17   let option_default = false in
  18   let mcode r (_,_,kind,_) =
  19     match kind with
  20       Ast.MINUS(_,_,_,_) -> true
  21     | Ast.PLUS _ -> failwith "not possible"
  22     | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
  23   let do_nothing r k e = k e in
  24   let rule_elem r k re =
  25     let res = k re in
  26     match Ast.unwrap re with
  27       Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
  28       bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
  29     | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
  30     | _ -> res in
  31   let recursor =
  32     V.combiner bind option_default
  33       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
  34       do_nothing do_nothing do_nothing do_nothing
  35       do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
  36       do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
  37   recursor.V.combiner_rule_elem
  38
  39 let ctl_exists keep_wit v x =
  40   CTL.Exists(!Flag_popl.keep_all_wits or keep_wit,v,x)
  41
  42 let predmaker keep_wit term =
  43   if (!Flag_popl.keep_all_wits or keep_wit) &&
  44      (!Flag_popl.mark_all or contains_modif term)
  45   then
  46     let v = ("","_v") in
  47     ctl_exists true v
  48       (CTL.Pred (Lib_engine.Match(term),CTL.Modif v))
  49   else CTL.Pred (Lib_engine.Match(term),CTL.Control)
  50
  51 (* --------------------------------------------------------------------- *)
  52
  53 let is_true = function CTL.True -> true | _ -> false
  54
  55 let is_false = function CTL.False -> true | _ -> false
  56
  57 let ctl_true       = CTL.True
  58
  59 let ctl_false      = CTL.False
  60
  61 let ctl_and x y    =
  62   if is_true x then y
  63   else if is_true y then x else CTL.And(CTL.STRICT,x,y)
  64
  65 let ctl_or x y     =
  66   if is_false x then y
  67   else if is_false y then x else CTL.Or(x,y)
  68
  69 let ctl_seqor x y  = CTL.SeqOr(x,y)
  70
  71 let ctl_not x      = CTL.Not(x)
  72
  73 let ctl_ax x       =
  74   if is_true x then CTL.True
  75   else CTL.AX(CTL.FORWARD,CTL.STRICT,x)
  76
  77 let ctl_ex x       =
  78   if is_true x then CTL.True
  79   else CTL.EX(CTL.FORWARD,x)
  80
  81 let ctl_back_ex x  =
  82   if is_true x then CTL.True
  83   else CTL.EX(CTL.BACKWARD,x)
  84
  85 let after          = CTL.Pred(Lib_engine.After, CTL.Control)
  86 let fall           = CTL.Pred(Lib_engine.FallThrough, CTL.Control)
  87 let exit           = CTL.Pred(Lib_engine.Exit, CTL.Control)
  88 let truepred       = CTL.Pred(Lib_engine.TrueBranch, CTL.Control)
  89 let falsepred      = CTL.Pred(Lib_engine.FalseBranch, CTL.Control)
  90 let retpred        = CTL.Pred(Lib_engine.Return, CTL.Control)
  91
  92 let string2var x = ("",x)
  93
  94 let labelctr = ref 0
  95 let get_label_ctr _ =
  96   let cur = !labelctr in
  97   labelctr := cur + 1;
  98   string2var (Printf.sprintf "l%d" cur)
  99
 100 let ctl_au x y = CTL.AU(CTL.FORWARD,CTL.STRICT,x,y)
 101
 102 let ctl_uncheck x  = CTL.Uncheck(x)
 103
 104 let make_meta_rule_elem d =
 105   let nm = "_S" in
 106   Ast.make_meta_rule_elem nm d ([],[],[])
 107
 108 (* --------------------------------------------------------------------- *)
 109
 110 let rec ctl_seq keep_wit a = function
 111     Past.Seq(elem,seq) ->
 112       ctl_element keep_wit (ctl_seq keep_wit a seq) elem
 113   | Past.Empty -> a
 114   | Past.SExists(var,seq) -> ctl_exists keep_wit var (ctl_seq keep_wit a seq)
 115
 116 and ctl_term keep_wit a = function
 117     Past.Atomic(term) -> ctl_and (predmaker keep_wit term) (ctl_ax a)
 118   | Past.IfThen(test,thn,(_,_,_,aft)) -> ifthen keep_wit (Some a) test thn aft
 119   | Past.TExists(var,term) ->
 120       ctl_exists keep_wit var (ctl_term keep_wit a term)
 121
 122 and ctl_element keep_wit a = function
 123     Past.Term(term,ba) ->
 124       do_between_dots keep_wit ba (ctl_term keep_wit a term) a
 125   | Past.Or(seq1,seq2) ->
 126       ctl_seqor (ctl_seq keep_wit a seq1) (ctl_seq keep_wit a seq2)
 127   | Past.DInfo(dots) -> ctl_au (guard_ctl_dots keep_wit a dots) a
 128   | Past.EExists(var,elem) ->
 129       ctl_exists keep_wit var (ctl_element keep_wit a elem)
 130
 131 (* --------------------------------------------------------------------- *)
 132
 133 and guard_ctl_seq keep_wit a = function
 134     Past.Seq(elem,Past.Empty) -> guard_ctl_element keep_wit a elem
 135   | Past.Seq(elem,seq) ->
 136       ctl_element keep_wit (guard_ctl_seq keep_wit a seq) elem
 137   | Past.Empty -> ctl_true
 138   | Past.SExists(var,seq) ->
 139       ctl_exists keep_wit var (guard_ctl_seq keep_wit a seq)
 140
 141 and guard_ctl_term keep_wit = function
 142     Past.Atomic(term) -> predmaker keep_wit term
 143   | Past.IfThen(test,thn,(_,_,_,aft)) -> ifthen keep_wit None test thn aft
 144   | Past.TExists(var,term) ->
 145       ctl_exists keep_wit var (guard_ctl_term keep_wit term)
 146
 147 and guard_ctl_element keep_wit a = function
 148     Past.Term(term,_) -> guard_ctl_term keep_wit term
 149   | Past.Or(seq1,seq2) ->
 150       ctl_seqor
 151         (guard_ctl_seq keep_wit a seq1) (guard_ctl_seq keep_wit a seq2)
 152   | Past.DInfo(dots) -> ctl_au (guard_ctl_dots keep_wit a dots) a
 153   | Past.EExists(var,elem) ->
 154       ctl_exists keep_wit var (guard_ctl_element keep_wit a elem)
 155
 156 and guard_ctl_dots keep_wit a = function
 157     Past.Dots -> ctl_true
 158 (* | Past.Nest(_) when not keep_wit -> ctl_true
 159    a possible optimization, but irrelevant to popl example *)
 160   | Past.Nest(seq) ->
 161       ctl_or
 162         (guard_ctl_seq true a seq)
 163         (ctl_not (guard_ctl_seq false a seq))
 164   | Past.When(dots,seq) ->
 165       ctl_and
 166         (guard_ctl_dots keep_wit a dots)
 167         (ctl_not (guard_ctl_seq false a seq))
 168
 169 (* --------------------------------------------------------------------- *)
 170
 171 and ifthen keep_wit a test thn aft =
 172 (* "if (test) thn; after" becomes:
 173     if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after))
 174              & EX After
 175     (* doesn't work for C code if (x) return 1; else return 2; *)
 176 *)
 177   let end_code =
 178     match (aft,a) with
 179       (Ast.CONTEXT(_,Ast.NOTHING),None) -> ctl_true
 180     | (Ast.CONTEXT(_,Ast.NOTHING),Some a) -> ctl_ax (ctl_ax a)
 181     | (_,None) -> failwith "not possible"
 182     | (_,Some a) ->
 183         ctl_ax
 184           (ctl_and
 185              (predmaker keep_wit (make_meta_rule_elem aft))
 186              (ctl_ax a)) in
 187   let body =
 188     ctl_or
 189       (ctl_and truepred
 190          (ctl_ax
 191             (guard_ctl_term keep_wit thn)))
 192       (ctl_or fall
 193          (ctl_and after end_code)) in
 194   ctl_and (ctl_term keep_wit body test)
 195     (match a with Some CTL.True | None -> ctl_true | Some _ -> ctl_ex after)
 196
 197 and do_between_dots keep_wit ba term after =
 198     match ba with
 199       Past.AddingBetweenDots (brace_term,n)
 200     | Past.DroppingBetweenDots (brace_term,n) ->
 201         (* not sure at all what to do here for after... *)
 202         let match_brace = ctl_term keep_wit after brace_term in
 203         let v = Printf.sprintf "_r_%d" n in
 204         let case1 = ctl_and (CTL.Ref v) match_brace in
 205         let case2 = ctl_and (ctl_not (CTL.Ref v)) term in
 206         CTL.Let
 207           (v,ctl_or
 208              (ctl_back_ex truepred)
 209              (ctl_back_ex (ctl_back_ex falsepred)),
 210            ctl_or case1 case2)
 211     | Past.NoDots -> term
 212
 213 (* --------------------------------------------------------------------- *)
 214
 215 let toctl sl = ctl_seq true ctl_true sl