Commit | Line | Data |
---|---|---|
9bc82bae C |
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 | ||
c491d8ee C |
25 | (* |
26 | * Copyright 2010, INRIA, University of Copenhagen | |
27 | * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix | |
28 | * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen | |
29 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
30 | * This file is part of Coccinelle. | |
31 | * | |
32 | * Coccinelle is free software: you can redistribute it and/or modify | |
33 | * it under the terms of the GNU General Public License as published by | |
34 | * the Free Software Foundation, according to version 2 of the License. | |
35 | * | |
36 | * Coccinelle is distributed in the hope that it will be useful, | |
37 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
38 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
39 | * GNU General Public License for more details. | |
40 | * | |
41 | * You should have received a copy of the GNU General Public License | |
42 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
43 | * | |
44 | * The authors reserve the right to distribute this or future versions of | |
45 | * Coccinelle under other licenses. | |
46 | *) | |
47 | ||
48 | ||
34e49164 C |
49 | (* two goals: first drop from the environments things that are not used, |
50 | and second prompt for the names of fresh variables that are used *) | |
51 | ||
52 | (* have to add in the whole inherited env because inherited variables are | |
53 | not returned by get_fvs. It would be better if that were the case, but | |
54 | since at the moment I think we can only inherit one value per variable, | |
55 | perhaps it doesn't matter - these bindings will always be the same no matter | |
56 | how we reached a particular match *) | |
57 | ||
58 | module Ast = Ast_cocci | |
59 | ||
60 | let extra_counter = ref 0 | |
61 | let get_extra _ = | |
62 | let ctr = !extra_counter in | |
63 | extra_counter := !extra_counter + 1; | |
64 | "__extra_counter__"^(string_of_int ctr) | |
65 | ||
b1b2de81 C |
66 | let get_seeded seed = |
67 | let ctr = !extra_counter in | |
68 | extra_counter := !extra_counter + 1; | |
69 | seed^(string_of_int ctr) | |
70 | ||
71 | let read_fresh_id _ = | |
ae4735db | 72 | try |
34e49164 | 73 | let s = read_line () in |
485bce71 | 74 | match Parse_c.tokens_of_string s with |
34e49164 | 75 | [Parser_c.TIdent _; Parser_c.EOF _] -> s |
b1b2de81 | 76 | | [Parser_c.EOF _] -> get_extra() |
34e49164 C |
77 | | _ -> failwith ("wrong fresh id: " ^ s) |
78 | with End_of_file -> get_extra() | |
79 | ||
80 | let get_vars = function | |
81 | Lib_engine.Match(re) -> (Ast.get_fvs re, Ast.get_fresh re) | |
82 | | _ -> ([],[]) | |
83 | ||
5636bb2c | 84 | let string2val str = Lib_engine.NormalMetaVal(Ast_c.MetaIdVal(str,[])) |
34e49164 C |
85 | |
86 | (* ----------------------------------------------------------------------- *) | |
87 | (* Get values for fresh variables *) | |
88 | ||
89 | let process_tree inherited_env l = | |
90 | let (all_fresh,local_freshs,new_triples) = | |
91 | List.fold_left | |
92 | (function (all_fresh,local_freshs,new_triples) -> | |
93 | function (node,env,pred) -> | |
94 | let (other,fresh) = get_vars pred in | |
95 | let env = List.filter (function (x,_) -> List.mem x other) env in | |
96 | (Common.union_set fresh all_fresh, | |
97 | fresh::local_freshs, | |
98 | (node,env@inherited_env,pred)::new_triples)) | |
99 | ([],[],[]) l in | |
100 | let local_freshs = List.rev local_freshs in | |
101 | let new_triples = List.rev new_triples in | |
102 | let fresh_env = | |
103 | List.map | |
b1b2de81 | 104 | (function |
978fd7e5 | 105 | ((r,n) as fresh,Ast.NoVal) -> |
b1b2de81 C |
106 | Printf.printf "%s: name for %s: " r n; (* not debugging code!!! *) |
107 | flush stdout; | |
978fd7e5 C |
108 | (fresh,let v = string2val(read_fresh_id()) in function _ -> v) |
109 | | ((r,n) as fresh,Ast.StringSeed seed) -> | |
110 | (fresh,let v = string2val(get_seeded seed) in function _ -> v) | |
111 | | ((r,n) as fresh,Ast.ListSeed seed) -> | |
112 | (fresh, | |
113 | function env -> | |
114 | let strings = | |
115 | List.map | |
116 | (function | |
117 | Ast.SeedString s -> s | |
118 | | Ast.SeedId id -> | |
119 | try | |
120 | (match List.assoc id env with | |
5636bb2c | 121 | Lib_engine.NormalMetaVal(Ast_c.MetaIdVal(str,_)) -> |
978fd7e5 C |
122 | str |
123 | | _ -> failwith "bad id value") | |
124 | with | |
125 | Not_found -> failwith "fresh: no binding for meta") | |
126 | seed in | |
127 | string2val(String.concat "" strings))) | |
34e49164 C |
128 | all_fresh in |
129 | let (_,res) = | |
130 | List.split | |
131 | (List.fold_left | |
132 | (function freshs_node_env_preds -> | |
978fd7e5 | 133 | function (fresh,fn) -> |
34e49164 C |
134 | List.map |
135 | (function (freshs,((node,env,pred) as cur)) -> | |
b1b2de81 C |
136 | try |
137 | let _ = List.assoc fresh freshs in | |
978fd7e5 | 138 | (freshs,(node,(fresh,fn env)::env,pred)) |
b1b2de81 | 139 | with Not_found -> (freshs,cur)) |
34e49164 C |
140 | freshs_node_env_preds) |
141 | (List.combine local_freshs new_triples) | |
142 | fresh_env) in | |
143 | (List.rev res, fresh_env) | |
144 | ||
145 | (* ----------------------------------------------------------------------- *) | |
146 | (* Create the environment to be used afterwards *) | |
978fd7e5 C |
147 | (* anything that a used after fresh variable refers to has to have a unique |
148 | value, by virtue of the placement of the quantifier. thus we augment | |
149 | inherited env with the first element of l, if any *) | |
150 | ||
151 | let collect_used_after used_after envs l inherited_env = | |
152 | List.map2 | |
153 | (function env -> function l -> | |
154 | let inherited_env = | |
155 | match l with | |
156 | [] -> inherited_env | |
157 | | (_,fse,_)::_ -> | |
158 | (* l represents the result from a single tree. fse is a complete | |
159 | environment in that tree. for a fresh seed, the environments | |
160 | for all leaves contain the same information *) | |
161 | fse@inherited_env in | |
162 | List.map | |
163 | (function (v,vl) -> (v,vl inherited_env)) | |
164 | (List.filter (function (v,vl) -> List.mem v used_after) env)) | |
165 | envs l | |
34e49164 | 166 | |
708f4980 C |
167 | (* ----------------------------------------------------------------------- *) |
168 | (* distinguish between distinct witness trees, each gets an index n *) | |
169 | ||
170 | let numberify trees = | |
171 | let trees = | |
172 | Common.fold_left_with_index | |
173 | (function acc -> function xs -> function n -> | |
174 | (List.map (function x -> (n,x)) xs) @ acc) | |
175 | [] trees in | |
176 | List.fold_left | |
177 | (function res -> | |
178 | function (n,x) -> | |
179 | let (same,diff) = List.partition (function (ns,xs) -> x = xs) res in | |
180 | match same with | |
181 | [(ns,xs)] -> (n::ns,xs)::diff | |
182 | | _ -> ([n],x)::res) | |
183 | [] trees | |
184 | ||
34e49164 C |
185 | (* ----------------------------------------------------------------------- *) |
186 | (* entry point *) | |
187 | ||
188 | let process used_after inherited_env l = | |
34e49164 C |
189 | let (trees, fresh_envs) = |
190 | List.split (List.map (process_tree inherited_env) l) in | |
708f4980 | 191 | let trees = numberify trees in |
978fd7e5 | 192 | (trees, collect_used_after used_after fresh_envs l inherited_env) |