engine/postprocess_transinfo.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 (* two goals: first drop from the environments things that are not used,
  46    and second prompt for the names of fresh variables that are used *)
  47
  48 (* have to add in the whole inherited env because inherited variables are
  49 not returned by get_fvs.  It would be better if that were the case, but
  50 since at the moment I think we can only inherit one value per variable,
  51 perhaps it doesn't matter - these bindings will always be the same no matter
  52 how we reached a particular match *)
  53
  54 module Ast = Ast_cocci
  55
  56 let extra_counter = ref 0
  57 let get_extra _ =
  58   let ctr = !extra_counter in
  59   extra_counter := !extra_counter + 1;
  60   "__extra_counter__"^(string_of_int ctr)
  61
  62 let get_seeded seed =
  63   let ctr = !extra_counter in
  64   extra_counter := !extra_counter + 1;
  65   seed^(string_of_int ctr)
  66
  67 let read_fresh_id _ =
  68   try
  69     let s = read_line () in
  70     match Parse_c.tokens_of_string s with
  71       [Parser_c.TIdent _; Parser_c.EOF _] -> s
  72     | [Parser_c.EOF _] -> get_extra()
  73     | _ -> failwith ("wrong fresh id: " ^ s)
  74   with End_of_file -> get_extra()
  75
  76 let get_vars = function
  77     Lib_engine.Match(re) -> (Ast.get_fvs re, Ast.get_fresh re)
  78   | _ -> ([],[])
  79
  80 let string2val str = Lib_engine.NormalMetaVal(Ast_c.MetaIdVal(str,[]))
  81
  82 (* ----------------------------------------------------------------------- *)
  83 (* Get values for fresh variables *)
  84
  85 let process_tree inherited_env l =
  86   let (all_fresh,local_freshs,new_triples) =
  87     List.fold_left
  88       (function (all_fresh,local_freshs,new_triples) ->
  89         function (node,env,pred) ->
  90           let (other,fresh) = get_vars pred in
  91           let env = List.filter (function (x,_) -> List.mem x other) env in
  92           (Common.union_set fresh all_fresh,
  93            fresh::local_freshs,
  94            (node,env@inherited_env,pred)::new_triples))
  95       ([],[],[]) l in
  96   let local_freshs = List.rev local_freshs in
  97   let new_triples = List.rev new_triples in
  98   let fresh_env =
  99     List.map
 100       (function
 101           ((r,n) as fresh,Ast.NoVal) ->
 102             Printf.printf "%s: name for %s: " r n; (* not debugging code!!! *)
 103             flush stdout;
 104             (fresh,let v = string2val(read_fresh_id()) in function _ -> v)
 105         | ((r,n) as fresh,Ast.StringSeed seed) ->
 106             (fresh,let v = string2val(get_seeded seed) in function _ -> v)
 107         | ((r,n) as fresh,Ast.ListSeed seed) ->
 108             (fresh,
 109              function env ->
 110                let strings =
 111                  List.map
 112                    (function
 113                        Ast.SeedString s -> s
 114                      | Ast.SeedId id ->
 115                          try
 116                            (match List.assoc id env with
 117                              Lib_engine.NormalMetaVal(Ast_c.MetaIdVal(str,_)) ->
 118                                str
 119                            | _ -> failwith "bad id value")
 120                          with
 121                            Not_found -> failwith "fresh: no binding for meta")
 122                    seed in
 123             string2val(String.concat "" strings)))
 124       all_fresh in
 125   let (_,res) =
 126     List.split
 127       (List.fold_left
 128          (function freshs_node_env_preds ->
 129            function (fresh,fn) ->
 130              List.map
 131                (function (freshs,((node,env,pred) as cur)) ->
 132                  try
 133                    let _ = List.assoc fresh freshs in
 134                    (freshs,(node,(fresh,fn env)::env,pred))
 135                  with Not_found -> (freshs,cur))
 136                freshs_node_env_preds)
 137          (List.combine local_freshs new_triples)
 138          fresh_env) in
 139   (List.rev res, fresh_env)
 140
 141 (* ----------------------------------------------------------------------- *)
 142 (* Create the environment to be used afterwards *)
 143 (* anything that a used after fresh variable refers to has to have a unique
 144 value, by virtue of the placement of the quantifier.  thus we augment
 145 inherited env with the first element of l, if any *)
 146
 147 let collect_used_after used_after envs l inherited_env =
 148   List.map2
 149     (function env -> function l ->
 150       let inherited_env =
 151         match l with
 152           [] -> inherited_env
 153         | (_,fse,_)::_ ->
 154             (* l represents the result from a single tree. fse is a complete
 155                environment in that tree.  for a fresh seed, the environments
 156                for all leaves contain the same information *)
 157             fse@inherited_env  in
 158       List.map
 159         (function (v,vl) -> (v,vl inherited_env))
 160         (List.filter (function (v,vl) -> List.mem v used_after) env))
 161     envs l
 162
 163 (* ----------------------------------------------------------------------- *)
 164 (* distinguish between distinct witness trees, each gets an index n *)
 165
 166 let numberify trees =
 167   let trees =
 168     Common.fold_left_with_index
 169       (function acc -> function xs -> function n ->
 170         (List.map (function x -> (n,x)) xs) @ acc)
 171       [] trees in
 172   List.fold_left
 173     (function res ->
 174       function (n,x) ->
 175         let (same,diff) = List.partition (function (ns,xs) -> x = xs) res in
 176         match same with
 177           [(ns,xs)] -> (n::ns,xs)::diff
 178         | _ -> ([n],x)::res)
 179     [] trees
 180
 181 (* ----------------------------------------------------------------------- *)
 182 (* entry point *)
 183
 184 let process used_after inherited_env l =
 185   let (trees, fresh_envs) =
 186     List.split (List.map (process_tree inherited_env) l) in
 187   let trees = numberify trees in
 188   (trees, collect_used_after used_after fresh_envs l inherited_env)