popl09/popltoctl.ml

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