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