engine/postprocess_transinfo.ml

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