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