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