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.
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.
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.
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/>.
20 * The authors reserve the right to distribute this or future versions of
21 * Coccinelle under other licenses.
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.
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.
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.
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/>.
44 * The authors reserve the right to distribute this or future versions of
45 * Coccinelle under other licenses.
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 *)
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 *)
58 module Ast
= Ast_cocci
60 let extra_counter = ref 0
62 let ctr = !extra_counter in
63 extra_counter := !extra_counter + 1;
64 "__extra_counter__"^
(string_of_int
ctr)
67 let ctr = !extra_counter in
68 extra_counter := !extra_counter + 1;
69 seed^
(string_of_int
ctr)
73 let s = read_line
() in
74 match Parse_c.tokens_of_string
s with
75 [Parser_c.TIdent _
; Parser_c.EOF _
] -> s
76 | [Parser_c.EOF _
] -> get_extra()
77 | _
-> failwith
("wrong fresh id: " ^
s)
78 with End_of_file
-> get_extra()
80 let get_vars = function
81 Lib_engine.Match
(re
) -> (Ast.get_fvs re
, Ast.get_fresh re
)
84 let string2val str
= Lib_engine.NormalMetaVal
(Ast_c.MetaIdVal
(str
,[]))
86 (* ----------------------------------------------------------------------- *)
87 (* Get values for fresh variables *)
89 let process_tree inherited_env l
=
90 let (all_fresh
,local_freshs
,new_triples
) =
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
,
98 (node
,env@inherited_env
,pred
)::new_triples
))
100 let local_freshs = List.rev
local_freshs in
101 let new_triples = List.rev
new_triples in
105 ((r
,n
) as fresh
,Ast.NoVal
) ->
106 Printf.printf
"%s: name for %s: " r n
; (* not debugging code!!! *)
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
) ->
117 Ast.SeedString
s -> s
120 (match List.assoc id
env with
121 Lib_engine.NormalMetaVal
(Ast_c.MetaIdVal
(str
,_
)) ->
123 | _
-> failwith
"bad id value")
125 Not_found
-> failwith
"fresh: no binding for meta")
127 string2val(String.concat
"" strings)))
132 (function freshs_node_env_preds
->
133 function (fresh
,fn
) ->
135 (function (freshs
,((node
,env,pred
) as cur
)) ->
137 let _ = List.assoc fresh freshs
in
138 (freshs
,(node
,(fresh
,fn
env)::env,pred
))
139 with Not_found
-> (freshs
,cur
))
140 freshs_node_env_preds
)
141 (List.combine
local_freshs new_triples)
143 (List.rev res
, fresh_env)
145 (* ----------------------------------------------------------------------- *)
146 (* Create the environment to be used afterwards *)
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 *)
151 let collect_used_after used_after envs l inherited_env
=
153 (function env -> function l
->
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 *)
163 (function (v,vl
) -> (v,vl
inherited_env))
164 (List.filter
(function (v,vl
) -> List.mem
v used_after
) env))
167 (* ----------------------------------------------------------------------- *)
168 (* distinguish between distinct witness trees, each gets an index n *)
170 let numberify trees
=
172 Common.fold_left_with_index
173 (function acc
-> function xs
-> function n
->
174 (List.map
(function x
-> (n
,x
)) xs
) @ acc
)
179 let (same
,diff
) = List.partition
(function (ns
,xs
) -> x
= xs
) res
in
181 [(ns
,xs
)] -> (n
::ns
,xs
)::diff
185 (* ----------------------------------------------------------------------- *)
188 let process used_after
inherited_env l
=
189 let (trees, fresh_envs
) =
190 List.split
(List.map
(process_tree inherited_env) l
) in
191 let trees = numberify trees in
192 (trees, collect_used_after used_after fresh_envs l
inherited_env)