parsing_cocci/unitary_ast0.ml

   1 (*
   2  * Copyright 2012, INRIA
   3  * Julia Lawall, Gilles Muller
   4  * Copyright 2010-2011, INRIA, University of Copenhagen
   5  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
   6  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
   7  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
   8  * This file is part of Coccinelle.
   9  *
  10  * Coccinelle is free software: you can redistribute it and/or modify
  11  * it under the terms of the GNU General Public License as published by
  12  * the Free Software Foundation, according to version 2 of the License.
  13  *
  14  * Coccinelle is distributed in the hope that it will be useful,
  15  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  16  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  17  * GNU General Public License for more details.
  18  *
  19  * You should have received a copy of the GNU General Public License
  20  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  21  *
  22  * The authors reserve the right to distribute this or future versions of
  23  * Coccinelle under other licenses.
  24  *)
  25
  26
  27 # 0 "./unitary_ast0.ml"
  28 (*
  29  * Copyright 2012, INRIA
  30  * Julia Lawall, Gilles Muller
  31  * Copyright 2010-2011, INRIA, University of Copenhagen
  32  * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
  33  * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
  34  * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
  35  * This file is part of Coccinelle.
  36  *
  37  * Coccinelle is free software: you can redistribute it and/or modify
  38  * it under the terms of the GNU General Public License as published by
  39  * the Free Software Foundation, according to version 2 of the License.
  40  *
  41  * Coccinelle is distributed in the hope that it will be useful,
  42  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  43  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  44  * GNU General Public License for more details.
  45  *
  46  * You should have received a copy of the GNU General Public License
  47  * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
  48  *
  49  * The authors reserve the right to distribute this or future versions of
  50  * Coccinelle under other licenses.
  51  *)
  52
  53
  54 # 0 "./unitary_ast0.ml"
  55 (* find unitary metavariables *)
  56 module Ast0 = Ast0_cocci
  57 module Ast = Ast_cocci
  58 module V0 = Visitor_ast0
  59 module VT0 = Visitor_ast0_types
  60
  61 let set_minus s minus = List.filter (function n -> not (List.mem n minus)) s
  62
  63 let rec nub = function
  64     [] -> []
  65   | (x::xs) when (List.mem x xs) -> nub xs
  66   | (x::xs) -> x::(nub xs)
  67
  68 (* ----------------------------------------------------------------------- *)
  69 (* Find the variables that occur free and occur free in a unitary way *)
  70
  71 (* take everything *)
  72 let minus_checker name = let id = Ast0.unwrap_mcode name in [id]
  73
  74 (* take only what is in the plus code *)
  75 let plus_checker (nm,_,_,mc,_,_) =
  76   match mc with Ast0.PLUS _ -> [nm] | _ -> []
  77
  78 let get_free checker t =
  79   let bind x y = x @ y in
  80   let option_default = [] in
  81
  82   (* considers a single list *)
  83   let collect_unitary_nonunitary free_usage =
  84     let free_usage = List.sort compare free_usage in
  85     let rec loop1 todrop = function
  86         [] -> []
  87       | (x::xs) as all -> if x = todrop then loop1 todrop xs else all in
  88     let rec loop2 = function
  89         [] -> ([],[])
  90       | [x] -> ([x],[])
  91       | x::y::xs ->
  92           if x = y
  93           then
  94             let (unitary,non_unitary) = loop2(loop1 x xs) in
  95             (unitary,x::non_unitary)
  96           else
  97             let (unitary,non_unitary) = loop2 (y::xs) in
  98             (x::unitary,non_unitary) in
  99     loop2 free_usage in
 100
 101   (* considers a list of lists *)
 102   let detect_unitary_frees l =
 103     let (unitary,nonunitary) =
 104       List.split (List.map collect_unitary_nonunitary l) in
 105     let unitary = nub (List.concat unitary) in
 106     let nonunitary = nub (List.concat nonunitary) in
 107     let unitary =
 108       List.filter (function x -> not (List.mem x nonunitary)) unitary in
 109     unitary@nonunitary@nonunitary in
 110
 111   let whencode afn bfn expression = function
 112       Ast0.WhenNot(a) -> afn a
 113     | Ast0.WhenAlways(b) -> bfn b
 114     | Ast0.WhenModifier(_) -> option_default
 115     | Ast0.WhenNotTrue(a) -> expression a
 116     | Ast0.WhenNotFalse(a) -> expression a in
 117
 118   let ident r k i =
 119     match Ast0.unwrap i with
 120       Ast0.MetaId(name,_,_,_) | Ast0.MetaFunc(name,_,_)
 121     | Ast0.MetaLocalFunc(name,_,_) -> checker name
 122     | Ast0.DisjId(starter,id_list,mids,ender) ->
 123         detect_unitary_frees(List.map r.VT0.combiner_rec_ident id_list)
 124     | _ -> k i in
 125
 126   let expression r k e =
 127     match Ast0.unwrap e with
 128       Ast0.MetaErr(name,_,_) | Ast0.MetaExpr(name,_,_,_,_)
 129     | Ast0.MetaExprList(name,_,_) -> checker name
 130     | Ast0.DisjExpr(starter,expr_list,mids,ender) ->
 131         detect_unitary_frees(List.map r.VT0.combiner_rec_expression expr_list)
 132     | _ -> k e in
 133
 134   let typeC r k t =
 135     match Ast0.unwrap t with
 136       Ast0.MetaType(name,_) -> checker name
 137     | Ast0.DisjType(starter,types,mids,ender) ->
 138         detect_unitary_frees(List.map r.VT0.combiner_rec_typeC types)
 139     | _ -> k t in
 140
 141   let parameter r k p =
 142     match Ast0.unwrap p with
 143       Ast0.MetaParam(name,_) | Ast0.MetaParamList(name,_,_) -> checker name
 144     | _ -> k p in
 145
 146   let declaration r k d =
 147     match Ast0.unwrap d with
 148       Ast0.MetaDecl(name,_) | Ast0.MetaField(name,_)
 149     | Ast0.MetaFieldList(name,_,_) -> checker name
 150     | Ast0.DisjDecl(starter,decls,mids,ender) ->
 151         detect_unitary_frees(List.map r.VT0.combiner_rec_declaration decls)
 152     | _ -> k d in
 153
 154   let case_line r k c =
 155     match Ast0.unwrap c with
 156       Ast0.DisjCase(starter,case_lines,mids,ender) ->
 157         detect_unitary_frees(List.map r.VT0.combiner_rec_case_line case_lines)
 158     | _ -> k c in
 159
 160   let statement r k s =
 161     match Ast0.unwrap s with
 162       Ast0.MetaStmt(name,_) | Ast0.MetaStmtList(name,_) -> checker name
 163     | Ast0.Disj(starter,stmt_list,mids,ender) ->
 164         detect_unitary_frees
 165           (List.map r.VT0.combiner_rec_statement_dots stmt_list)
 166     | Ast0.Nest(starter,stmt_dots,ender,whn,multi) ->
 167         bind (r.VT0.combiner_rec_statement_dots stmt_dots)
 168           (detect_unitary_frees
 169              (List.map
 170                 (whencode
 171                    r.VT0.combiner_rec_statement_dots
 172                    r.VT0.combiner_rec_statement
 173                     r.VT0.combiner_rec_expression)
 174                 whn))
 175     | Ast0.Dots(d,whn) | Ast0.Circles(d,whn) | Ast0.Stars(d,whn) ->
 176         detect_unitary_frees
 177           (List.map
 178              (whencode
 179                 r.VT0.combiner_rec_statement_dots r.VT0.combiner_rec_statement
 180                 r.VT0.combiner_rec_expression)
 181              whn)
 182     | _ -> k s in
 183
 184   let res = V0.combiner bind option_default
 185       {V0.combiner_functions with
 186         VT0.combiner_identfn = ident;
 187         VT0.combiner_exprfn = expression;
 188         VT0.combiner_tyfn = typeC;
 189         VT0.combiner_paramfn = parameter;
 190         VT0.combiner_declfn = declaration;
 191         VT0.combiner_stmtfn = statement;
 192         VT0.combiner_casefn = case_line} in
 193
 194   collect_unitary_nonunitary
 195     (List.concat (List.map res.VT0.combiner_rec_top_level t))
 196
 197 (* ----------------------------------------------------------------------- *)
 198 (* update the variables that are unitary *)
 199
 200 let update_unitary unitary =
 201   let is_unitary name =
 202     match (List.mem (Ast0.unwrap_mcode name) unitary,
 203            !Flag.sgrep_mode2, Ast0.get_mcode_mcodekind name) with
 204       (true,true,_) | (true,_,Ast0.CONTEXT(_)) -> Ast0.PureContext
 205     | (true,_,_) -> Ast0.Pure
 206     | (false,true,_) | (false,_,Ast0.CONTEXT(_)) -> Ast0.Context
 207     | (false,_,_) -> Ast0.Impure in
 208
 209   let ident r k i =
 210     match Ast0.unwrap i with
 211       Ast0.MetaId(name,constraints,seed,_) ->
 212         Ast0.rewrap i (Ast0.MetaId(name,constraints,seed,is_unitary name))
 213     | Ast0.MetaFunc(name,constraints,_) ->
 214         Ast0.rewrap i (Ast0.MetaFunc(name,constraints,is_unitary name))
 215     | Ast0.MetaLocalFunc(name,constraints,_) ->
 216         Ast0.rewrap i (Ast0.MetaLocalFunc(name,constraints,is_unitary name))
 217     | _ -> k i in
 218
 219   let expression r k e =
 220     match Ast0.unwrap e with
 221       Ast0.MetaErr(name,constraints,_) ->
 222         Ast0.rewrap e (Ast0.MetaErr(name,constraints,is_unitary name))
 223     | Ast0.MetaExpr(name,constraints,ty,form,_) ->
 224         Ast0.rewrap e (Ast0.MetaExpr(name,constraints,ty,form,is_unitary name))
 225     | Ast0.MetaExprList(name,lenname,_) ->
 226         Ast0.rewrap e (Ast0.MetaExprList(name,lenname,is_unitary name))
 227     | _ -> k e in
 228
 229   let typeC r k t =
 230     match Ast0.unwrap t with
 231       Ast0.MetaType(name,_) ->
 232         Ast0.rewrap t (Ast0.MetaType(name,is_unitary name))
 233     | _ -> k t in
 234
 235   let parameter r k p =
 236     match Ast0.unwrap p with
 237       Ast0.MetaParam(name,_) ->
 238         Ast0.rewrap p (Ast0.MetaParam(name,is_unitary name))
 239     | Ast0.MetaParamList(name,lenname,_) ->
 240         Ast0.rewrap p (Ast0.MetaParamList(name,lenname,is_unitary name))
 241     | _ -> k p in
 242
 243   let statement r k s =
 244     match Ast0.unwrap s with
 245       Ast0.MetaStmt(name,_) ->
 246         Ast0.rewrap s (Ast0.MetaStmt(name,is_unitary name))
 247     | Ast0.MetaStmtList(name,_) ->
 248         Ast0.rewrap s (Ast0.MetaStmtList(name,is_unitary name))
 249     | _ -> k s in
 250
 251   let res = V0.rebuilder
 252       {V0.rebuilder_functions with
 253         VT0.rebuilder_identfn = ident;
 254         VT0.rebuilder_exprfn = expression;
 255         VT0.rebuilder_tyfn = typeC;
 256         VT0.rebuilder_paramfn = parameter;
 257         VT0.rebuilder_stmtfn = statement} in
 258
 259   List.map res.VT0.rebuilder_rec_top_level
 260
 261 (* ----------------------------------------------------------------------- *)
 262
 263 let rec split3 = function
 264     [] -> ([],[],[])
 265   | (a,b,c)::xs -> let (l1,l2,l3) = split3 xs in (a::l1,b::l2,c::l3)
 266
 267 let rec combine3 = function
 268     ([],[],[]) -> []
 269   | (a::l1,b::l2,c::l3) -> (a,b,c) :: combine3 (l1,l2,l3)
 270   | _ -> failwith "not possible"
 271
 272 (* ----------------------------------------------------------------------- *)
 273 (* process all rules *)
 274
 275 let do_unitary rules =
 276   let rec loop = function
 277       [] -> ([],[])
 278     | (r::rules) ->
 279       match r with
 280         Ast0.ScriptRule (_,_,_,_,_,_)
 281       | Ast0.InitialScriptRule (_,_,_,_) | Ast0.FinalScriptRule (_,_,_,_) ->
 282           let (x,rules) = loop rules in
 283           (x, r::rules)
 284       | Ast0.CocciRule ((minus,metavars,chosen_isos),((plus,_) as plusz),rt) ->
 285           let mm1 = List.map Ast.get_meta_name metavars in
 286           let (used_after, rest) = loop rules in
 287           let (m_unitary, m_nonunitary) = get_free minus_checker minus in
 288           let (p_unitary, p_nonunitary) = get_free plus_checker plus in
 289           let p_free =
 290             if !Flag.sgrep_mode2 then []
 291             else p_unitary @ p_nonunitary in
 292           let (in_p, m_unitary) =
 293             List.partition (function x -> List.mem x p_free) m_unitary in
 294           let m_nonunitary = in_p @ m_nonunitary in
 295           let (m_unitary, not_local) =
 296             List.partition (function x -> List.mem x mm1) m_unitary in
 297           let m_unitary =
 298             List.filter (function x -> not (List.mem x used_after))
 299               m_unitary in
 300           let rebuilt = update_unitary m_unitary minus in
 301           (set_minus (m_nonunitary @ used_after) mm1,
 302              (Ast0.CocciRule
 303                 ((rebuilt, metavars, chosen_isos),plusz,rt))::rest) in
 304   let (_,rules) = loop rules in
 305   rules
 306
 307 (*
 308 let do_unitary minus plus =
 309   let (minus,metavars,chosen_isos) = split3 minus in
 310   let (plus,_) = List.split plus in
 311   let rec loop = function
 312       ([],[],[]) -> ([],[])
 313     | (mm1::metavars,m1::minus,p1::plus) ->
 314         let mm1 = List.map Ast.get_meta_name mm1 in
 315         let (used_after,rest) = loop (metavars,minus,plus) in
 316         let (m_unitary,m_nonunitary) = get_free minus_checker m1 in
 317         let (p_unitary,p_nonunitary) = get_free plus_checker p1 in
 318         let p_free =
 319           if !Flag.sgrep_mode2
 320           then []
 321           else p_unitary @ p_nonunitary in
 322         let (in_p,m_unitary) =
 323           List.partition (function x -> List.mem x p_free) m_unitary in
 324         let m_nonunitary = in_p@m_nonunitary in
 325         let (m_unitary,not_local) =
 326           List.partition (function x -> List.mem x mm1) m_unitary in
 327         let m_unitary =
 328           List.filter (function x -> not(List.mem x used_after)) m_unitary in
 329         let rebuilt = update_unitary m_unitary m1 in
 330         (set_minus (m_nonunitary @ used_after) mm1,
 331          rebuilt::rest)
 332     | _ -> failwith "not possible" in
 333   let (_,rules) = loop (metavars,minus,plus) in
 334   combine3 (rules,metavars,chosen_isos)
 335 *)