2 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
24 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
25 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
26 * This file is part of Coccinelle.
28 * Coccinelle is free software: you can redistribute it and/or modify
29 * it under the terms of the GNU General Public License as published by
30 * the Free Software Foundation, according to version 2 of the License.
32 * Coccinelle is distributed in the hope that it will be useful,
33 * but WITHOUT ANY WARRANTY; without even the implied warranty of
34 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
35 * GNU General Public License for more details.
37 * You should have received a copy of the GNU General Public License
38 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
40 * The authors reserve the right to distribute this or future versions of
41 * Coccinelle under other licenses.
45 (* **********************************************************************
47 * Wrapping for FUNCTORS and MODULES
50 * $Id: wrapper_ctl.ml,v 1.68 2010/01/28 14:23:46 npalix Exp $
52 * **********************************************************************)
56 type ('pred
, 'mvar
) wrapped_ctl
=
57 ('pred
* 'mvar
Ast_ctl.modif
, 'mvar
, info
) Ast_ctl.generic_ctl
59 type ('
value, 'pred
) wrapped_binding
=
60 | ClassicVal
of '
value
61 | PredVal
of 'pred
Ast_ctl.modif
63 type ('pred
,'state
,'mvar
,'
value) labelfunc
=
65 ('state
* ('pred
* ('mvar
, '
value) Ast_ctl.generic_substitution
)) list
67 (* pad: what is 'wit ? *)
68 type ('pred
,'state
,'mvar
,'
value,'wit
) wrapped_labelfunc
=
69 ('pred
* 'mvar
Ast_ctl.modif
) ->
71 ('mvar
,('
value,'pred
) wrapped_binding
) Ast_ctl.generic_substitution
*
75 (* ********************************************************************** *)
76 (* Module type: CTL_ENGINE_BIS (wrapper for CTL_ENGINE) *)
77 (* ********************************************************************** *)
79 (* This module must convert the labelling function passed as parameter, by
80 using convert_label. Then create a SUBST2 module handling the
81 wrapped_binding. Then it can instantiates the generic CTL_ENGINE
82 module. Call sat. And then process the witness tree to remove all that
83 is not revelevant for the transformation phase.
86 module CTL_ENGINE_BIS
=
87 functor (SUB
: Ctl_engine.SUBST
) ->
88 functor (G
: Ctl_engine.GRAPH
) ->
89 functor(P
: Ctl_engine.PREDICATE
) ->
92 exception TODO_CTL
of string (* implementation still not quite done so... *)
93 exception NEVER_CTL
of string (* Some things should never happen *)
101 type value = (SUB.value,predicate
) wrapped_binding
102 let eq_mvar = SUB.eq_mvar
105 | (ClassicVal
(v1
),ClassicVal
(v2
)) -> SUB.eq_val v1 v2
106 | (PredVal
(v1
),PredVal
(v2
)) -> v1
= v2
(* FIX ME: ok? *)
108 let merge_val wv1 wv2
=
110 | (ClassicVal
(v1
),ClassicVal
(v2
)) -> ClassicVal
(SUB.merge_val v1 v2
)
111 | _
-> wv1
(* FIX ME: ok? *)
114 let print_mvar x
= SUB.print_mvar x
117 ClassicVal v
-> SUB.print_value v
118 | PredVal
(A.Modif v
) -> P.print_predicate v
119 | PredVal
(A.UnModif v
) -> P.print_predicate v
120 | PredVal
(A.Control
) -> Format.print_string
"no value"
123 module WRAPPER_PRED
=
125 type t
= P.t
* SUB.mvar
Ast_ctl.modif
126 let print_predicate (pred
, modif
) =
128 P.print_predicate pred
;
130 Ast_ctl.Modif x
| Ast_ctl.UnModif x
->
131 Format.print_string
" with <modifTODO>"
132 | Ast_ctl.Control
-> ())
136 (* Instantiate a wrapped version of CTL_ENGINE *)
137 module WRAPPER_ENGINE
=
138 Ctl_engine.CTL_ENGINE
(WRAPPER_ENV
) (G
) (WRAPPER_PRED
)
140 (* Wrap a label function *)
141 let (wrap_label
: ('pred
,'state
,'mvar
,'
value) labelfunc
->
142 ('pred
,'state
,'mvar
,'
value,'wit
) wrapped_labelfunc
) =
148 | A.Modif
(x
) -> [A.Subst
(x
,PredVal
(A.Modif
(p'
)))]
149 | A.UnModif
(x
) -> [A.Subst
(x
,PredVal
(A.UnModif
(p'
)))]
154 | A.Subst
(x
,v
) -> A.Subst
(x
,ClassicVal
(v
))
155 | A.NegSubst
(x
,v
) -> A.NegSubst
(x
,ClassicVal
(v
)) in
157 let conv_trip (s
,(p'
,env
)) =
158 (s
,penv p'
@ (List.map
conv_sub env
),[](*pad: ?*))
160 List.map
conv_trip (oldlabelfunc p
)
162 (* ---------------------------------------------------------------- *)
164 (* FIX ME: what about negative witnesses and negative substitutions *)
165 let unwrap_wits modifonly wits
=
168 (function A.Subst
(x
,ClassicVal
(v
)) -> Some
(x
,v
) | _
-> None
)
170 let rec loop neg acc
= function
171 A.Wit
(st
,[A.Subst
(x
,PredVal
(A.Modif
(v
)))],anno
,wit
) ->
174 | _
-> raise
(NEVER_CTL
"predvar tree should have no children"))
175 | A.Wit
(st
,[A.Subst
(x
,PredVal
(A.UnModif
(v
)))],anno
,wit
)
176 when not modifonly
or !Flag.track_iso_usage
->
179 | _
-> raise
(NEVER_CTL
"predvar tree should have no children"))
180 | A.Wit
(st
,th
,anno
,wit
) ->
181 List.concat
(List.map
(loop neg
((mkth th
) @ acc
)) wit
)
182 | A.NegWit
(_
) -> [] (* why not failure? *) in
183 List.concat
(List.map
(function wit
-> loop false [] wit
) wits
)
187 (* a match can return many trees, but within each tree, there has to be
188 at most one value for each variable that is in the used_after list *)
189 let collect_used_after used_after envs
=
190 let print_var var
= SUB.print_mvar var
; Format.print_flush
() in
193 (function used_after_var
->
199 let vl = List.assoc used_after_var env
in
202 | Some old_vl
when SUB.eq_val vl old_vl
-> rest
203 | Some old_vl
-> print_var used_after_var
;
204 Format.print_newline
();
205 SUB.print_value old_vl
;
206 Format.print_newline
();
208 Format.print_newline
();
209 failwith
"incompatible values"
210 with Not_found
-> rest
)
214 | Some
vl -> [(used_after_var
, vl)])
218 (* a match can return many trees, but within each tree, there has to be
219 at most one value for each variable that is in the used_after list *)
220 (* actually, this should always be the case, because these variables
221 should be quantified at the top level. so the more complicated
222 definition above should not be needed. *)
223 let collect_used_after used_after envs
=
226 (function used_after_var
->
232 let vl = List.assoc used_after_var env
in
233 if List.exists
(function x
-> SUB.eq_val x
vl) rest
236 with Not_found
-> rest
)
238 List.map
(function x
-> (used_after_var
, x
)) vl)
241 (* ----------------------------------------------------- *)
243 (* The wrapper for sat from the CTL_ENGINE *)
244 let satbis_noclean (grp
,lab
,states
) (phi
,reqopt
) :
245 ('pred
,'anno
) WRAPPER_ENGINE.triples
=
246 WRAPPER_ENGINE.sat
(grp
,wrap_label lab
,states
) phi reqopt
248 (* Returns the "cleaned up" result from satbis_noclean *)
251 (predicate
,G.node
,SUB.mvar
,SUB.value) labelfunc
*
253 ((predicate
,SUB.mvar
) wrapped_ctl
*
254 (WRAPPER_PRED.t list list
)) ->
255 (WRAPPER_ENV.mvar list
* (SUB.mvar
* SUB.value) list
) ->
256 ((WRAPPER_PRED.t
, 'a
) WRAPPER_ENGINE.triples
*
257 ((G.node
* (SUB.mvar
* SUB.value) list
* predicate
)
260 (WRAPPER_ENV.mvar
* SUB.value) list list
))) =
261 fun m phi
(used_after
, binding
) ->
262 let noclean = satbis_noclean m phi
in
263 let witness_trees = List.map
(fun (_
,_
,w
) -> w
) noclean in
264 let res = List.map
(unwrap_wits true) witness_trees in
267 (function bindings_per_witness_tree
->
268 (List.map
(function (_
,env
,_
) -> env
) bindings_per_witness_tree
))
269 (List.map
(unwrap_wits false) witness_trees) in
271 (res,not
(noclean = []),
272 (* throw in the old binding. By construction it doesn't conflict
273 with any of the new things, and it is useful if there are no new
275 (List.map
(collect_used_after used_after
) new_bindings)))
277 let print_bench _
= WRAPPER_ENGINE.print_bench()
279 (* END OF MODULE: CTL_ENGINE_BIS *)