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 | (* ********************************************************************** |
50 | * | |
51 | * Wrapping for FUNCTORS and MODULES | |
34e49164 | 52 | * |
ae4735db C |
53 | * |
54 | * $Id: wrapper_ctl.ml,v 1.68 2010/01/28 14:23:46 npalix Exp $ | |
34e49164 C |
55 | * |
56 | * **********************************************************************) | |
57 | ||
58 | type info = int | |
59 | ||
ae4735db | 60 | type ('pred, 'mvar) wrapped_ctl = |
34e49164 C |
61 | ('pred * 'mvar Ast_ctl.modif, 'mvar, info) Ast_ctl.generic_ctl |
62 | ||
ae4735db | 63 | type ('value, 'pred) wrapped_binding = |
34e49164 C |
64 | | ClassicVal of 'value |
65 | | PredVal of 'pred Ast_ctl.modif | |
66 | ||
67 | type ('pred,'state,'mvar,'value) labelfunc = | |
ae4735db | 68 | 'pred -> |
34e49164 C |
69 | ('state * ('pred * ('mvar, 'value) Ast_ctl.generic_substitution)) list |
70 | ||
71 | (* pad: what is 'wit ? *) | |
72 | type ('pred,'state,'mvar,'value,'wit) wrapped_labelfunc = | |
ae4735db C |
73 | ('pred * 'mvar Ast_ctl.modif) -> |
74 | ('state * | |
34e49164 C |
75 | ('mvar,('value,'pred) wrapped_binding) Ast_ctl.generic_substitution * |
76 | 'wit | |
77 | ) list | |
78 | ||
79 | (* ********************************************************************** *) | |
80 | (* Module type: CTL_ENGINE_BIS (wrapper for CTL_ENGINE) *) | |
81 | (* ********************************************************************** *) | |
82 | ||
83 | (* This module must convert the labelling function passed as parameter, by | |
84 | using convert_label. Then create a SUBST2 module handling the | |
85 | wrapped_binding. Then it can instantiates the generic CTL_ENGINE | |
86 | module. Call sat. And then process the witness tree to remove all that | |
87 | is not revelevant for the transformation phase. | |
88 | *) | |
89 | ||
90 | module CTL_ENGINE_BIS = | |
91 | functor (SUB : Ctl_engine.SUBST) -> | |
92 | functor (G : Ctl_engine.GRAPH) -> | |
93 | functor(P : Ctl_engine.PREDICATE) -> | |
94 | struct | |
95 | ||
96 | exception TODO_CTL of string (* implementation still not quite done so... *) | |
97 | exception NEVER_CTL of string (* Some things should never happen *) | |
98 | ||
99 | module A = Ast_ctl | |
100 | ||
101 | type predicate = P.t | |
102 | module WRAPPER_ENV = | |
103 | struct | |
104 | type mvar = SUB.mvar | |
105 | type value = (SUB.value,predicate) wrapped_binding | |
106 | let eq_mvar = SUB.eq_mvar | |
ae4735db | 107 | let eq_val wv1 wv2 = |
34e49164 C |
108 | match (wv1,wv2) with |
109 | | (ClassicVal(v1),ClassicVal(v2)) -> SUB.eq_val v1 v2 | |
110 | | (PredVal(v1),PredVal(v2)) -> v1 = v2 (* FIX ME: ok? *) | |
111 | | _ -> false | |
ae4735db | 112 | let merge_val wv1 wv2 = |
34e49164 C |
113 | match (wv1,wv2) with |
114 | | (ClassicVal(v1),ClassicVal(v2)) -> ClassicVal(SUB.merge_val v1 v2) | |
115 | | _ -> wv1 (* FIX ME: ok? *) | |
116 | ||
117 | ||
118 | let print_mvar x = SUB.print_mvar x | |
ae4735db | 119 | let print_value x = |
34e49164 C |
120 | match x with |
121 | ClassicVal v -> SUB.print_value v | |
122 | | PredVal(A.Modif v) -> P.print_predicate v | |
123 | | PredVal(A.UnModif v) -> P.print_predicate v | |
124 | | PredVal(A.Control) -> Format.print_string "no value" | |
125 | end | |
126 | ||
ae4735db C |
127 | module WRAPPER_PRED = |
128 | struct | |
34e49164 | 129 | type t = P.t * SUB.mvar Ast_ctl.modif |
ae4735db | 130 | let print_predicate (pred, modif) = |
34e49164 C |
131 | begin |
132 | P.print_predicate pred; | |
133 | (match modif with | |
134 | Ast_ctl.Modif x | Ast_ctl.UnModif x -> | |
135 | Format.print_string " with <modifTODO>" | |
136 | | Ast_ctl.Control -> ()) | |
137 | end | |
138 | end | |
139 | ||
140 | (* Instantiate a wrapped version of CTL_ENGINE *) | |
141 | module WRAPPER_ENGINE = | |
142 | Ctl_engine.CTL_ENGINE (WRAPPER_ENV) (G) (WRAPPER_PRED) | |
143 | ||
144 | (* Wrap a label function *) | |
ae4735db C |
145 | let (wrap_label: ('pred,'state,'mvar,'value) labelfunc -> |
146 | ('pred,'state,'mvar,'value,'wit) wrapped_labelfunc) = | |
34e49164 C |
147 | fun oldlabelfunc -> |
148 | fun (p, predvar) -> | |
149 | ||
ae4735db | 150 | let penv p' = |
34e49164 C |
151 | match predvar with |
152 | | A.Modif(x) -> [A.Subst(x,PredVal(A.Modif(p')))] | |
153 | | A.UnModif(x) -> [A.Subst(x,PredVal(A.UnModif(p')))] | |
154 | | A.Control -> [] in | |
155 | ||
156 | let conv_sub sub = | |
157 | match sub with | |
158 | | A.Subst(x,v) -> A.Subst(x,ClassicVal(v)) | |
159 | | A.NegSubst(x,v) -> A.NegSubst(x,ClassicVal(v)) in | |
160 | ||
ae4735db C |
161 | let conv_trip (s,(p',env)) = |
162 | (s,penv p' @ (List.map conv_sub env),[](*pad: ?*)) | |
34e49164 C |
163 | in |
164 | List.map conv_trip (oldlabelfunc p) | |
165 | ||
166 | (* ---------------------------------------------------------------- *) | |
167 | ||
168 | (* FIX ME: what about negative witnesses and negative substitutions *) | |
169 | let unwrap_wits modifonly wits = | |
170 | let mkth th = | |
171 | Common.map_filter | |
172 | (function A.Subst(x,ClassicVal(v)) -> Some (x,v) | _ -> None) | |
173 | th in | |
174 | let rec loop neg acc = function | |
175 | A.Wit(st,[A.Subst(x,PredVal(A.Modif(v)))],anno,wit) -> | |
176 | (match wit with | |
177 | [] -> [(st,acc,v)] | |
178 | | _ -> raise (NEVER_CTL "predvar tree should have no children")) | |
179 | | A.Wit(st,[A.Subst(x,PredVal(A.UnModif(v)))],anno,wit) | |
180 | when not modifonly or !Flag.track_iso_usage -> | |
181 | (match wit with | |
182 | [] -> [(st,acc,v)] | |
183 | | _ -> raise (NEVER_CTL "predvar tree should have no children")) | |
184 | | A.Wit(st,th,anno,wit) -> | |
185 | List.concat (List.map (loop neg ((mkth th) @ acc)) wit) | |
186 | | A.NegWit(_) -> [] (* why not failure? *) in | |
187 | List.concat (List.map (function wit -> loop false [] wit) wits) | |
188 | ;; | |
189 | ||
190 | (* | |
191 | (* a match can return many trees, but within each tree, there has to be | |
192 | at most one value for each variable that is in the used_after list *) | |
193 | let collect_used_after used_after envs = | |
194 | let print_var var = SUB.print_mvar var; Format.print_flush() in | |
195 | List.concat | |
196 | (List.map | |
197 | (function used_after_var -> | |
198 | let vl = | |
199 | List.fold_left | |
200 | (function rest -> | |
201 | function env -> | |
202 | try | |
203 | let vl = List.assoc used_after_var env in | |
204 | match rest with | |
205 | None -> Some vl | |
206 | | Some old_vl when SUB.eq_val vl old_vl -> rest | |
207 | | Some old_vl -> print_var used_after_var; | |
208 | Format.print_newline(); | |
209 | SUB.print_value old_vl; | |
210 | Format.print_newline(); | |
211 | SUB.print_value vl; | |
212 | Format.print_newline(); | |
213 | failwith "incompatible values" | |
214 | with Not_found -> rest) | |
215 | None envs in | |
216 | match vl with | |
217 | None -> [] | |
218 | | Some vl -> [(used_after_var, vl)]) | |
219 | used_after) | |
220 | *) | |
221 | ||
222 | (* a match can return many trees, but within each tree, there has to be | |
223 | at most one value for each variable that is in the used_after list *) | |
224 | (* actually, this should always be the case, because these variables | |
225 | should be quantified at the top level. so the more complicated | |
226 | definition above should not be needed. *) | |
227 | let collect_used_after used_after envs = | |
228 | List.concat | |
229 | (List.map | |
230 | (function used_after_var -> | |
231 | let vl = | |
232 | List.fold_left | |
233 | (function rest -> | |
234 | function env -> | |
235 | try | |
236 | let vl = List.assoc used_after_var env in | |
237 | if List.exists (function x -> SUB.eq_val x vl) rest | |
238 | then rest | |
239 | else vl::rest | |
240 | with Not_found -> rest) | |
241 | [] envs in | |
242 | List.map (function x -> (used_after_var, x)) vl) | |
243 | used_after) | |
244 | ||
245 | (* ----------------------------------------------------- *) | |
246 | ||
247 | (* The wrapper for sat from the CTL_ENGINE *) | |
248 | let satbis_noclean (grp,lab,states) (phi,reqopt) : | |
249 | ('pred,'anno) WRAPPER_ENGINE.triples = | |
250 | WRAPPER_ENGINE.sat (grp,wrap_label lab,states) phi reqopt | |
ae4735db | 251 | |
34e49164 C |
252 | (* Returns the "cleaned up" result from satbis_noclean *) |
253 | let (satbis : | |
254 | G.cfg * | |
255 | (predicate,G.node,SUB.mvar,SUB.value) labelfunc * | |
ae4735db | 256 | G.node list -> |
34e49164 C |
257 | ((predicate,SUB.mvar) wrapped_ctl * |
258 | (WRAPPER_PRED.t list list)) -> | |
259 | (WRAPPER_ENV.mvar list * (SUB.mvar * SUB.value) list) -> | |
260 | ((WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples * | |
261 | ((G.node * (SUB.mvar * SUB.value) list * predicate) | |
262 | list list * | |
263 | bool * | |
264 | (WRAPPER_ENV.mvar * SUB.value) list list))) = | |
265 | fun m phi (used_after, binding) -> | |
266 | let noclean = satbis_noclean m phi in | |
267 | let witness_trees = List.map (fun (_,_,w) -> w) noclean in | |
268 | let res = List.map (unwrap_wits true) witness_trees in | |
269 | let new_bindings = | |
270 | List.map | |
271 | (function bindings_per_witness_tree -> | |
272 | (List.map (function (_,env,_) -> env) bindings_per_witness_tree)) | |
273 | (List.map (unwrap_wits false) witness_trees) in | |
274 | (noclean, | |
275 | (res,not(noclean = []), | |
276 | (* throw in the old binding. By construction it doesn't conflict | |
277 | with any of the new things, and it is useful if there are no new | |
278 | things. *) | |
279 | (List.map (collect_used_after used_after) new_bindings))) | |
280 | ||
281 | let print_bench _ = WRAPPER_ENGINE.print_bench() | |
282 | ||
283 | (* END OF MODULE: CTL_ENGINE_BIS *) | |
284 | end |