File: wrapper_ctl.ml

package info (click to toggle)
coccinelle 1.0.8.deb-5
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 26,148 kB
  • sloc: ml: 136,392; ansic: 23,594; sh: 2,189; makefile: 2,157; perl: 1,576; lisp: 840; python: 823; awk: 70; csh: 12
file content (258 lines) | stat: -rw-r--r-- 8,551 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
(*
 * This file is part of Coccinelle, licensed under the terms of the GPL v2.
 * See copyright.txt in the Coccinelle source code for more information.
 * The Coccinelle source code can be obtained at http://coccinelle.lip6.fr
 *)

(* **********************************************************************
 *
 * Wrapping for FUNCTORS and MODULES
 *
 *
 * $Id$
 *
 * **********************************************************************)

type info = int

type ('pred, 'mvar) wrapped_ctl =
    ('pred * 'mvar Ast_ctl.modif,  'mvar, info) Ast_ctl.generic_ctl

type ('value, 'pred) wrapped_binding =
  | ClassicVal of 'value
  | PredVal of 'pred Ast_ctl.modif

type ('pred,'state,'mvar,'value) labelfunc =
    'pred ->
      ('state * ('pred * ('mvar, 'value) Ast_ctl.generic_substitution)) list

(* pad: what is 'wit ? *)
type ('pred,'state,'mvar,'value,'wit) wrapped_labelfunc =
  ('pred * 'mvar Ast_ctl.modif) ->
      ('state *
       ('mvar,('value,'pred) wrapped_binding) Ast_ctl.generic_substitution *
       'wit
      ) list

type 'pred preprocfunc =
    'pred -> bool

(* pad: what is 'wit ? *)
type ('pred,'mvar) wrapped_preprocfunc =
  ('pred * 'mvar Ast_ctl.modif) -> bool

(* ********************************************************************** *)
(* Module type: CTL_ENGINE_BIS (wrapper for CTL_ENGINE)                   *)
(* ********************************************************************** *)

(* This module must convert the labelling function passed as parameter, by
   using convert_label. Then create a SUBST2 module handling the
   wrapped_binding.  Then it can instantiates the generic CTL_ENGINE
   module. Call sat.  And then process the witness tree to remove all that
   is not revelevant for the transformation phase.
*)

module CTL_ENGINE_BIS =
  functor (SUB : Ctl_engine.SUBST) ->
    functor (G : Ctl_engine.GRAPH) ->
      functor(P : Ctl_engine.PREDICATE) ->
struct

  exception TODO_CTL of string  (* implementation still not quite done so... *)
  exception NEVER_CTL of string		  (* Some things should never happen *)

  module A = Ast_ctl

  type predicate = P.t
  module WRAPPER_ENV =
  struct
    type mvar = SUB.mvar
    type value = (SUB.value,predicate) wrapped_binding
    let eq_mvar = SUB.eq_mvar
    let eq_val wv1 wv2 =
      match (wv1,wv2) with
	| (ClassicVal(v1),ClassicVal(v2)) -> SUB.eq_val v1 v2
	| (PredVal(v1),PredVal(v2))       -> v1 = v2   (* FIX ME: ok? *)
	| _                               -> false
    let merge_val wv1 wv2 =
      match (wv1,wv2) with
	| (ClassicVal(v1),ClassicVal(v2)) -> ClassicVal(SUB.merge_val v1 v2)
	| _                               -> wv1       (* FIX ME: ok? *)


    let print_mvar x = SUB.print_mvar x
    let print_value x =
      match x with
	ClassicVal v -> SUB.print_value v
      | PredVal(A.Modif v) -> P.print_predicate v
      | PredVal(A.UnModif v) -> P.print_predicate v
      |	PredVal(A.Control) -> Format.print_string "no value"
  end

  module WRAPPER_PRED =
    struct
      type t = P.t * SUB.mvar Ast_ctl.modif
      let print_predicate (pred, modif) =
        begin
          P.print_predicate pred;
	  (match modif with
	    Ast_ctl.Modif x | Ast_ctl.UnModif x ->
	      Format.print_string " with <modifTODO>"
	  | Ast_ctl.Control -> ())
        end
    end

  (* Instantiate a wrapped version of CTL_ENGINE *)
  module WRAPPER_ENGINE =
    Ctl_engine.CTL_ENGINE (WRAPPER_ENV) (G) (WRAPPER_PRED)

  (* Wrap a label function *)
  let (wrap_label: ('pred,'state,'mvar,'value) labelfunc ->
	('pred,'state,'mvar,'value,'wit) wrapped_labelfunc) =
    fun oldlabelfunc ->
      fun (p, predvar) ->

	let penv p'  =
	  match predvar with
	  | A.Modif(x)   -> [A.Subst(x,PredVal(A.Modif(p')))]
	  | A.UnModif(x) -> [A.Subst(x,PredVal(A.UnModif(p')))]
	  | A.Control    -> [] in

	let conv_sub sub =
	  match sub with
	  | A.Subst(x,v)    -> A.Subst(x,ClassicVal(v))
	  | A.NegSubst(x,v) -> A.NegSubst(x,ClassicVal(v)) in

	let conv_trip (s,(p',env)) =
          (s,penv p' @ (List.map conv_sub env),[](*pad: ?*))
        in
        List.map conv_trip (oldlabelfunc p)

  (* Wrap a preproc function - selects interesting predicates *)
  let (wrap_preproc: 'pred preprocfunc ->
	('pred,'mvar) wrapped_preprocfunc) =
    fun oldpreprocfunc ->
      fun (p, predvar) ->
	oldpreprocfunc p

  (* ---------------------------------------------------------------- *)

  (* FIX ME: what about negative witnesses and negative substitutions *)
  let unwrap_wits modifonly wits =
    let mkth th =
      Common.map_filter
	(function A.Subst(x,ClassicVal(v)) -> Some (x,v) | _ -> None)
	th in
    let rec loop neg acc = function
	A.Wit(st,[A.Subst(x,PredVal(A.Modif(v)))],anno,wit) ->
	  (match wit with
	    [] -> [(st,acc,v)]
	  | _ -> raise (NEVER_CTL "predvar tree should have no children"))
      | A.Wit(st,[A.Subst(x,PredVal(A.UnModif(v)))],anno,wit)
	when not modifonly || !Flag.track_iso_usage ->
	  (match wit with
	    [] -> [(st,acc,v)]
	  | _ -> raise (NEVER_CTL "predvar tree should have no children"))
      | A.Wit(st,th,anno,wit) ->
	  List.concat (List.map (loop neg ((mkth th) @ acc)) wit)
      | A.NegWit(_) -> [] (* why not failure? *) in
    List.concat (List.map (function wit -> loop false [] wit) wits)
  ;;

(*
  (* a match can return many trees, but within each tree, there has to be
     at most one value for each variable that is in the used_after list *)
  let collect_used_after used_after envs =
    let print_var var = SUB.print_mvar var; Format.print_flush() in
    List.concat
      (List.map
	 (function used_after_var ->
	   let vl =
	     List.fold_left
	       (function rest ->
		 function env ->
		   try
		     let vl = List.assoc used_after_var env in
		     match rest with
		       None -> Some vl
		     | Some old_vl when SUB.eq_val vl old_vl -> rest
		     | Some old_vl -> print_var used_after_var;
			 Format.print_newline();
			 SUB.print_value old_vl;
			 Format.print_newline();
			 SUB.print_value vl;
			 Format.print_newline();
			 failwith "incompatible values"
		   with Not_found -> rest)
	       None envs in
	   match vl with
	     None -> []
	   | Some vl -> [(used_after_var, vl)])
	 used_after)
*)

  (* a match can return many trees, but within each tree, there has to be
     at most one value for each variable that is in the used_after list *)
  (* actually, this should always be the case, because these variables
  should be quantified at the top level.  so the more complicated
  definition above should not be needed. *)
  let collect_used_after used_after envs =
    List.concat
      (List.map
	 (function used_after_var ->
	   let vl =
	     List.fold_left
	       (function rest ->
		 function env ->
		   try
		     let vl = List.assoc used_after_var env in
		     if List.exists (function x -> SUB.eq_val x vl) rest
		     then rest
		     else vl::rest
		   with Not_found -> rest)
	       [] envs in
	   List.map (function x -> (used_after_var, x)) vl)
	 used_after)

  (* ----------------------------------------------------- *)

  (* The wrapper for sat from the CTL_ENGINE *)
  let satbis_noclean (grp,lab,preproc,states) (phi,reqopt) :
      ('pred,'anno) WRAPPER_ENGINE.triples =
    WRAPPER_ENGINE.sat (grp,wrap_label lab,wrap_preproc preproc,states)
      phi reqopt

  (* Returns the "cleaned up" result from satbis_noclean *)
  let (satbis :
         G.cfg *
	 (predicate,G.node,SUB.mvar,SUB.value) labelfunc *
	 predicate preprocfunc *
         G.node list ->
	   ((predicate,SUB.mvar) wrapped_ctl *
	      (WRAPPER_PRED.t list list)) ->
	     (WRAPPER_ENV.mvar list * (SUB.mvar * SUB.value) list) ->
	       ((WRAPPER_PRED.t, 'a) WRAPPER_ENGINE.triples *
		  ((G.node * (SUB.mvar * SUB.value) list * predicate)
		     list list *
		     bool *
		     (WRAPPER_ENV.mvar * SUB.value) list list))) =
    fun m phi (used_after, binding) ->
      let noclean = satbis_noclean m phi in
      let witness_trees = List.map (fun (_,_,w) -> w) noclean in
      let res = List.map (unwrap_wits true) witness_trees in
      let new_bindings =
	List.map
	  (function bindings_per_witness_tree ->
	    (List.map (function (_,env,_) -> env) bindings_per_witness_tree))
	  (List.map (unwrap_wits false) witness_trees) in
      (noclean,
       (res,not(noclean = []),
	   (* throw in the old binding.  By construction it doesn't conflict
           with any of the new things, and it is useful if there are no new
	   things. *)
	(List.map (collect_used_after used_after) new_bindings)))

let print_bench _ = WRAPPER_ENGINE.print_bench()

(* END OF MODULE: CTL_ENGINE_BIS *)
end