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.
25 (* **********************************************************************
27 * Wrapping for FUNCTORS and MODULES
30 * $Id: wrapper_ctl.ml,v 1.68 2010/01/28 14:23:46 npalix Exp $
32 * **********************************************************************)
36 type ('pred, 'mvar) wrapped_ctl =
37 ('pred * 'mvar Ast_ctl.modif, 'mvar, info) Ast_ctl.generic_ctl
39 type ('value, 'pred) wrapped_binding =
40 | ClassicVal of 'value
41 | PredVal of 'pred Ast_ctl.modif
43 type ('pred,'state,'mvar,'value) labelfunc =
45 ('state * ('pred * ('mvar, 'value) Ast_ctl.generic_substitution)) list
47 (* pad: what is 'wit ? *)
48 type ('pred,'state,'mvar,'value,'wit) wrapped_labelfunc =
49 ('pred * 'mvar Ast_ctl.modif) ->
51 ('mvar,('value,'pred) wrapped_binding) Ast_ctl.generic_substitution *
55 (* ********************************************************************** *)
56 (* Module type: CTL_ENGINE_BIS (wrapper for CTL_ENGINE) *)
57 (* ********************************************************************** *)
59 (* This module must convert the labelling function passed as parameter, by
60 using convert_label. Then create a SUBST2 module handling the
61 wrapped_binding. Then it can instantiates the generic CTL_ENGINE
62 module. Call sat. And then process the witness tree to remove all that
63 is not revelevant for the transformation phase.
66 module CTL_ENGINE_BIS =
67 functor (SUB : Ctl_engine.SUBST) ->
68 functor (G : Ctl_engine.GRAPH) ->
69 functor(P : Ctl_engine.PREDICATE) ->
72 exception TODO_CTL of string (* implementation still not quite done so... *)
73 exception NEVER_CTL of string (* Some things should never happen *)
81 type value = (SUB.value,predicate) wrapped_binding
82 let eq_mvar = SUB.eq_mvar
85 | (ClassicVal(v1),ClassicVal(v2)) -> SUB.eq_val v1 v2
86 | (PredVal(v1),PredVal(v2)) -> v1 = v2 (* FIX ME: ok? *)
88 let merge_val wv1 wv2 =
90 | (ClassicVal(v1),ClassicVal(v2)) -> ClassicVal(SUB.merge_val v1 v2)
91 | _ -> wv1 (* FIX ME: ok? *)
94 let print_mvar x = SUB.print_mvar x
97 ClassicVal v -> SUB.print_value v
98 | PredVal(A.Modif v) -> P.print_predicate v
99 | PredVal(A.UnModif v) -> P.print_predicate v
100 | PredVal(A.Control) -> Format.print_string "no value"
103 module WRAPPER_PRED =
105 type t = P.t * SUB.mvar Ast_ctl.modif
106 let print_predicate (pred, modif) =
108 P.print_predicate pred;
110 Ast_ctl.Modif x | Ast_ctl.UnModif x ->
111 Format.print_string " with <modifTODO>"
112 | Ast_ctl.Control -> ())
116 (* Instantiate a wrapped version of CTL_ENGINE *)
117 module WRAPPER_ENGINE =
118 Ctl_engine.CTL_ENGINE (WRAPPER_ENV) (G) (WRAPPER_PRED)
120 (* Wrap a label function *)
121 let (wrap_label: ('pred,'state,'mvar,'value) labelfunc ->
122 ('pred,'state,'mvar,'value,'wit) wrapped_labelfunc) =
128 | A.Modif(x) -> [A.Subst(x,PredVal(A.Modif(p')))]
129 | A.UnModif(x) -> [A.Subst(x,PredVal(A.UnModif(p')))]
134 | A.Subst(x,v) -> A.Subst(x,ClassicVal(v))
135 | A.NegSubst(x,v) -> A.NegSubst(x,ClassicVal(v)) in
137 let conv_trip (s,(p',env)) =
138 (s,penv p' @ (List.map conv_sub env),[](*pad: ?*))
140 List.map conv_trip (oldlabelfunc p)
142 (* ---------------------------------------------------------------- *)
144 (* FIX ME: what about negative witnesses and negative substitutions *)
145 let unwrap_wits modifonly wits =
148 (function A.Subst(x,ClassicVal(v)) -> Some (x,v) | _ -> None)
150 let rec loop neg acc = function
151 A.Wit(st,[A.Subst(x,PredVal(A.Modif(v)))],anno,wit) ->
154 | _ -> raise (NEVER_CTL "predvar tree should have no children"))
155 | A.Wit(st,[A.Subst(x,PredVal(A.UnModif(v)))],anno,wit)
156 when not modifonly or !Flag.track_iso_usage ->
159 | _ -> raise (NEVER_CTL "predvar tree should have no children"))
160 | A.Wit(st,th,anno,wit) ->
161 List.concat (List.map (loop neg ((mkth th) @ acc)) wit)
162 | A.NegWit(_) -> [] (* why not failure? *) in
163 List.concat (List.map (function wit -> loop false [] wit) wits)
167 (* a match can return many trees, but within each tree, there has to be
168 at most one value for each variable that is in the used_after list *)
169 let collect_used_after used_after envs =
170 let print_var var = SUB.print_mvar var; Format.print_flush() in
173 (function used_after_var ->
179 let vl = List.assoc used_after_var env in
182 | Some old_vl when SUB.eq_val vl old_vl -> rest
183 | Some old_vl -> print_var used_after_var;
184 Format.print_newline();
185 SUB.print_value old_vl;
186 Format.print_newline();
188 Format.print_newline();
189 failwith "incompatible values"
190 with Not_found -> rest)
194 | Some vl -> [(used_after_var, vl)])
198 (* a match can return many trees, but within each tree, there has to be
199 at most one value for each variable that is in the used_after list *)
200 (* actually, this should always be the case, because these variables
201 should be quantified at the top level. so the more complicated
202 definition above should not be needed. *)
203 let collect_used_after used_after envs =
206 (function used_after_var ->
212 let vl = List.assoc used_after_var env in
213 if List.exists (function x -> SUB.eq_val x vl) rest
216 with Not_found -> rest)
218 List.map (function x -> (used_after_var, x)) vl)
221 (* ----------------------------------------------------- *)
223 (* The wrapper for sat from the CTL_ENGINE *)
224 let satbis_noclean (grp,lab,states) (phi,reqopt) :
225 ('pred,'anno) WRAPPER_ENGINE.triples =
226 WRAPPER_ENGINE.sat (grp,wrap_label lab,states) phi reqopt
228 (* Returns the "cleaned up" result from satbis_noclean *)
231 (predicate,G.node,SUB.mvar,SUB.value) labelfunc *
233 ((predicate,SUB.mvar) wrapped_ctl *
234 (WRAPPER_PRED.t list list)) ->
235 (WRAPPER_ENV.mvar list * (SUB.mvar * SUB.value) list) ->
236 ((WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples *
237 ((G.node * (SUB.mvar * SUB.value) list * predicate)
240 (WRAPPER_ENV.mvar * SUB.value) list list))) =
241 fun m phi (used_after, binding) ->
242 let noclean = satbis_noclean m phi in
243 let witness_trees = List.map (fun (_,_,w) -> w) noclean in
244 let res = List.map (unwrap_wits true) witness_trees in
247 (function bindings_per_witness_tree ->
248 (List.map (function (_,env,_) -> env) bindings_per_witness_tree))
249 (List.map (unwrap_wits false) witness_trees) in
251 (res,not(noclean = []),
252 (* throw in the old binding. By construction it doesn't conflict
253 with any of the new things, and it is useful if there are no new
255 (List.map (collect_used_after used_after) new_bindings)))
257 let print_bench _ = WRAPPER_ENGINE.print_bench()
259 (* END OF MODULE: CTL_ENGINE_BIS *)