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 -> failwith "fresh: no binding for meta")
 102                    seed in
 103             string2val(String.concat "" strings)))
 104       all_fresh in
 105   let (_,res) =
 106     List.split
 107       (List.fold_left
 108          (function freshs_node_env_preds ->
 109            function (fresh,fn) ->
 110              List.map
 111                (function (freshs,((node,env,pred) as cur)) ->
 112                  try
 113                    let _ = List.assoc fresh freshs in
 114                    (freshs,(node,(fresh,fn env)::env,pred))
 115                  with Not_found -> (freshs,cur))
 116                freshs_node_env_preds)
 117          (List.combine local_freshs new_triples)
 118          fresh_env) in
 119   (List.rev res, fresh_env)
 120
 121 (* ----------------------------------------------------------------------- *)
 122 (* Create the environment to be used afterwards *)
 123 (* anything that a used after fresh variable refers to has to have a unique
 124 value, by virtue of the placement of the quantifier.  thus we augment
 125 inherited env with the first element of l, if any *)
 126
 127 let collect_used_after used_after envs l inherited_env =
 128   List.map2
 129     (function env -> function l ->
 130       let inherited_env =
 131         match l with
 132           [] -> inherited_env
 133         | (_,fse,_)::_ ->
 134             (* l represents the result from a single tree. fse is a complete
 135                environment in that tree.  for a fresh seed, the environments
 136                for all leaves contain the same information *)
 137             fse@inherited_env  in
 138       List.map
 139         (function (v,vl) -> (v,vl inherited_env))
 140         (List.filter (function (v,vl) -> List.mem v used_after) env))
 141     envs l
 142
 143 (* ----------------------------------------------------------------------- *)
 144 (* distinguish between distinct witness trees, each gets an index n *)
 145
 146 let numberify trees =
 147   let trees =
 148     Common.fold_left_with_index
 149       (function acc -> function xs -> function n ->
 150         (List.map (function x -> (n,x)) xs) @ acc)
 151       [] trees in
 152   List.fold_left
 153     (function res ->
 154       function (n,x) ->
 155         let (same,diff) = List.partition (function (ns,xs) -> x = xs) res in
 156         match same with
 157           [(ns,xs)] -> (n::ns,xs)::diff
 158         | _ -> ([n],x)::res)
 159     [] trees
 160
 161 (* ----------------------------------------------------------------------- *)
 162 (* entry point *)
 163
 164 let process used_after inherited_env l =
 165   let (trees, fresh_envs) =
 166     List.split (List.map (process_tree inherited_env) l) in
 167   let trees = numberify trees in
 168   (trees, collect_used_after used_after fresh_envs l inherited_env)