popl/popltoctl.ml

   1 (*
   2  * Copyright 2010, INRIA, University of Copenhagen
   3  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
   4  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
   5  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   6  * This file is part of Coccinelle.
   7  *
   8  * Coccinelle is free software: you can redistribute it and/or modify
   9  * it under the terms of the GNU General Public License as published by
  10  * the Free Software Foundation, according to version 2 of the License.
  11  *
  12  * Coccinelle is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  19  *
  20  * The authors reserve the right to distribute this or future versions of
  21  * Coccinelle under other licenses.
  22  *)
  23
  24
  25 (*
  26  * Copyright 2010, INRIA, University of Copenhagen
  27  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
  28  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
  29  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
  30  * This file is part of Coccinelle.
  31  *
  32  * Coccinelle is free software: you can redistribute it and/or modify
  33  * it under the terms of the GNU General Public License as published by
  34  * the Free Software Foundation, according to version 2 of the License.
  35  *
  36  * Coccinelle is distributed in the hope that it will be useful,
  37  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  38  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  39  * GNU General Public License for more details.
  40  *
  41  * You should have received a copy of the GNU General Public License
  42  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  43  *
  44  * The authors reserve the right to distribute this or future versions of
  45  * Coccinelle under other licenses.
  46  *)
  47
  48
  49 module Past = Ast_popl
  50 module Ast = Ast_cocci
  51 module V = Visitor_ast
  52 module CTL  = Ast_ctl
  53
  54 (* --------------------------------------------------------------------- *)
  55 (* result type *)
  56
  57 type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif
  58 type formula =
  59     (cocci_predicate,Ast_cocci.meta_name, Wrapper_ctl.info) Ast_ctl.generic_ctl
  60
  61 (* --------------------------------------------------------------------- *)
  62
  63 let contains_modif =
  64   let bind x y = x or y in
  65   let option_default = false in
  66   let mcode r (_,_,kind,_) =
  67     match kind with
  68       Ast.MINUS(_,_) -> true
  69     | Ast.PLUS -> failwith "not possible"
  70     | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
  71   let do_nothing r k e = k e in
  72   let rule_elem r k re =
  73     let res = k re in
  74     match Ast.unwrap re with
  75       Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
  76       bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
  77     | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res
  78     | _ -> res in
  79   let recursor =
  80     V.combiner bind option_default
  81       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
  82       mcode
  83       do_nothing do_nothing do_nothing do_nothing
  84       do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
  85       do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
  86   recursor.V.combiner_rule_elem
  87
  88 let ctl_exists v x keep_wit = CTL.Exists(v,x,keep_wit)
  89
  90 let predmaker guard term =
  91   let pos = ("","_p") in
  92   ctl_exists true pos
  93     (if guard && contains_modif term
  94     then
  95       let v = ("","_v") in
  96       ctl_exists true v
  97         (CTL.Pred (Lib_engine.Match(term),CTL.Modif v))
  98     else CTL.Pred (Lib_engine.Match(term),CTL.Control))
  99
 100 (* --------------------------------------------------------------------- *)
 101
 102 let is_true = function CTL.True -> true | _ -> false
 103
 104 let is_false = function CTL.False -> true | _ -> false
 105
 106 let ctl_true       = CTL.True
 107
 108 let ctl_false      = CTL.False
 109
 110 let ctl_and x y    =
 111   if is_true x then y
 112   else if is_true y then x else CTL.And(CTL.STRICT,x,y)
 113
 114 let ctl_or x y     =
 115   if is_false x then y
 116   else if is_false y then x else CTL.Or(x,y)
 117
 118 let ctl_seqor x y  = CTL.SeqOr(x,y)
 119
 120 let ctl_not x      = CTL.Not(x)
 121
 122 let ctl_ax x       =
 123   if is_true x then CTL.True
 124   else CTL.AX(CTL.FORWARD,CTL.STRICT,x)
 125
 126 let after          = CTL.Pred(Lib_engine.After, CTL.Control)
 127 let exit           = CTL.Pred(Lib_engine.Exit, CTL.Control)
 128 let truepred       = CTL.Pred(Lib_engine.TrueBranch, CTL.Control)
 129 let retpred        = CTL.Pred(Lib_engine.Return, CTL.Control)
 130
 131 let string2var x = ("",x)
 132
 133 let labelctr = ref 0
 134 let get_label_ctr _ =
 135   let cur = !labelctr in
 136   labelctr := cur + 1;
 137   string2var (Printf.sprintf "l%d" cur)
 138
 139 let ctl_au x seq_after y =
 140   let lv = get_label_ctr() in
 141   let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
 142   let preflabelpred = CTL.Pred(Lib_engine.PrefixLabel lv,CTL.Control) in
 143   let matchgoto = CTL.Pred(Lib_engine.Goto,CTL.Control) in
 144   let matchbreak =
 145     predmaker false
 146       (Ast.make_term
 147          (Ast.Break(Ast.make_mcode "break",Ast.make_mcode ";"))) in
 148   let matchcontinue =
 149     predmaker false
 150       (Ast.make_term
 151          (Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in
 152   let stop_early =
 153     ctl_or after
 154       (ctl_and (ctl_and truepred labelpred)
 155          (CTL.AU
 156             (CTL.FORWARD,CTL.STRICT,preflabelpred,
 157              ctl_and preflabelpred
 158                (ctl_or retpred
 159                   (ctl_and (ctl_or (ctl_or matchgoto matchbreak) matchcontinue)
 160                         (CTL.AG
 161                            (CTL.FORWARD,CTL.STRICT,
 162                             ctl_not seq_after))))))) in
 163   CTL.AU(CTL.FORWARD,CTL.STRICT,x,ctl_or y stop_early)
 164
 165 let ctl_uncheck x  = CTL.Uncheck(x)
 166
 167 (* --------------------------------------------------------------------- *)
 168
 169 let rec ctl_seq keep_wit a = function
 170     Past.Seq(elem,seq) ->
 171       ctl_element keep_wit (ctl_seq keep_wit a seq) elem
 172   | Past.Empty -> a
 173   | Past.SExists(var,seq) -> ctl_exists keep_wit var (ctl_seq keep_wit a seq)
 174
 175 and ctl_element keep_wit a = function
 176     Past.Term(term) -> ctl_and (predmaker keep_wit term) (ctl_ax a)
 177   | Past.Or(seq1,seq2) ->
 178       ctl_seqor (ctl_seq keep_wit a seq1) (ctl_seq keep_wit a seq2)
 179   | Past.DInfo(dots,seq_bef,seq_aft) ->
 180       let shortest l =
 181         List.fold_left ctl_or ctl_false
 182           (List.map (ctl_element false ctl_true) l) in
 183       let s = shortest (Common.union_set seq_bef seq_aft) in
 184       ctl_au (ctl_and (guard_ctl_dots keep_wit dots) (ctl_not s))
 185         (shortest seq_aft) a
 186   | Past.EExists(var,elem) ->
 187       ctl_exists keep_wit var (ctl_element keep_wit a elem)
 188
 189 (* --------------------------------------------------------------------- *)
 190
 191 and guard_ctl_seq keep_wit = function
 192     Past.Seq(elem,Past.Empty) -> guard_ctl_element keep_wit elem
 193   | Past.Seq(elem,seq) ->
 194       ctl_element keep_wit (guard_ctl_seq keep_wit seq) elem
 195   | Past.Empty -> ctl_true
 196   | Past.SExists(var,seq) ->
 197       ctl_exists keep_wit var (guard_ctl_seq keep_wit seq)
 198
 199 and guard_ctl_element keep_wit = function
 200     Past.Term(term) -> predmaker keep_wit term
 201   | Past.Or(seq1,seq2) ->
 202       ctl_seqor (guard_ctl_seq keep_wit seq1) (guard_ctl_seq keep_wit seq2)
 203   | Past.DInfo(dots,seq_bef,seq_aft) ->
 204       let shortest l =
 205         List.fold_left ctl_or ctl_false
 206           (List.map (ctl_element false ctl_true) l) in
 207       let s = shortest (Common.union_set seq_bef seq_aft) in
 208       let aft = ctl_or s exit in
 209       ctl_au (ctl_and (guard_ctl_dots keep_wit dots) (ctl_not s))
 210         (shortest seq_aft) aft
 211   | Past.EExists(var,elem) ->
 212       ctl_exists keep_wit var (guard_ctl_element keep_wit elem)
 213
 214 and guard_ctl_dots keep_wit = function
 215     Past.Dots -> ctl_true
 216   | Past.Nest(_) when not keep_wit -> ctl_true
 217   | Past.Nest(seq) ->
 218       ctl_or (guard_ctl_seq true seq) (ctl_not (guard_ctl_seq false seq))
 219   | Past.When(dots,seq) ->
 220       ctl_and
 221         (guard_ctl_dots keep_wit dots)
 222         (ctl_not (ctl_seq false ctl_true seq))
 223   | Past.DExists(var,dots) ->
 224       ctl_exists keep_wit var (guard_ctl_dots keep_wit dots)
 225
 226 (* --------------------------------------------------------------------- *)
 227
 228 let toctl sl = ctl_seq true ctl_true sl