lustrec / src / tools / zustre / zustre_common.ml @ a0c92fa8
History | View | Annotate | Download (29.6 KB)
1 |
open Lustre_types |
---|---|
2 |
open Machine_code_types |
3 |
open Machine_code_common |
4 |
open Format |
5 |
(* open Horn_backend_common |
6 |
* open Horn_backend *) |
7 |
open Zustre_data |
8 |
|
9 |
let report = Log.report ~plugin:"z3 interface" |
10 |
|
11 |
module HBC = Horn_backend_common |
12 |
let node_name = HBC.node_name |
13 |
|
14 |
let concat = HBC.concat |
15 |
|
16 |
let rename_machine = HBC.rename_machine |
17 |
let rename_machine_list = HBC.rename_machine_list |
18 |
|
19 |
let rename_next = HBC.rename_next |
20 |
let rename_mid = HBC.rename_mid |
21 |
let rename_current = HBC.rename_current |
22 |
|
23 |
let rename_current_list = HBC.rename_current_list |
24 |
let rename_mid_list = HBC.rename_mid_list |
25 |
let rename_next_list = HBC.rename_next_list |
26 |
|
27 |
let full_memory_vars = HBC.full_memory_vars |
28 |
let inout_vars = HBC.inout_vars |
29 |
let reset_vars = HBC.reset_vars |
30 |
let step_vars = HBC.step_vars |
31 |
let local_memory_vars = HBC.local_memory_vars |
32 |
let step_vars_m_x = HBC.step_vars_m_x |
33 |
let step_vars_c_m_x = HBC.step_vars_c_m_x |
34 |
|
35 |
let machine_reset_name = HBC.machine_reset_name |
36 |
let machine_step_name = HBC.machine_step_name |
37 |
let machine_stateless_name = HBC.machine_stateless_name |
38 |
|
39 |
let preprocess = Horn_backend.preprocess |
40 |
|
41 |
|
42 |
exception UnknownFunction of (string * (Format.formatter -> unit)) |
43 |
(** Sorts |
44 |
|
45 |
A sort is introduced for each basic type and each enumerated type. |
46 |
|
47 |
A hashtbl records these and allow easy access to sort values, when |
48 |
provided with a enumerated type name. |
49 |
|
50 |
*) |
51 |
|
52 |
let bool_sort = Z3.Boolean.mk_sort !ctx |
53 |
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx |
54 |
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx |
55 |
|
56 |
|
57 |
let get_const_sort = Hashtbl.find const_sorts |
58 |
let get_sort_elems = Hashtbl.find sort_elems |
59 |
let get_tag_sort id = try Hashtbl.find const_tags id with _ -> Format.eprintf "Unable to find sort for tag=%s@." id; assert false |
60 |
|
61 |
|
62 |
|
63 |
let decl_sorts () = |
64 |
Hashtbl.iter (fun typ decl -> |
65 |
match typ with |
66 |
| Tydec_const var -> |
67 |
(match decl.top_decl_desc with |
68 |
| TypeDef tdef -> ( |
69 |
match tdef.tydef_desc with |
70 |
| Tydec_enum tl -> |
71 |
let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in |
72 |
Hashtbl.add const_sorts var new_sort; |
73 |
Hashtbl.add sort_elems new_sort tl; |
74 |
List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl |
75 |
|
76 |
| _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false |
77 |
) |
78 |
| _ -> assert false |
79 |
) |
80 |
| _ -> ()) Corelang.type_table |
81 |
|
82 |
|
83 |
let rec type_to_sort t = |
84 |
if Types.is_bool_type t then bool_sort else |
85 |
if Types.is_int_type t then int_sort else |
86 |
if Types.is_real_type t then real_sort else |
87 |
match (Types.repr t).Types.tdesc with |
88 |
| Types.Tconst ty -> get_const_sort ty |
89 |
| Types.Tclock t -> type_to_sort t |
90 |
| Types.Tarray(dim,ty) -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty) |
91 |
| Types.Tstatic(d, ty)-> type_to_sort ty |
92 |
| Types.Tarrow _ |
93 |
| _ -> Format.eprintf "internal error: pp_type %a@." |
94 |
Types.print_ty t; assert false |
95 |
|
96 |
|
97 |
(* let idx_var = *) |
98 |
(* Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort *) |
99 |
|
100 |
(* let uid_var = *) |
101 |
(* Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort *) |
102 |
|
103 |
(** Func decls |
104 |
|
105 |
Similarly fun_decls are registerd, by their name, into a hashtbl. The |
106 |
proposed encoding introduces a 0-ary fun_decl to model variables and |
107 |
fun_decl with arguments to declare reset and step predicates. |
108 |
|
109 |
|
110 |
|
111 |
*) |
112 |
let register_fdecl id fd = Hashtbl.add decls id fd |
113 |
let get_fdecl id = |
114 |
try |
115 |
Hashtbl.find decls id |
116 |
with Not_found -> (report ~level:3 (fun fmt -> Format.fprintf fmt "Unable to find func_decl %s@.@?" id); raise Not_found) |
117 |
|
118 |
let pp_fdecls fmt = |
119 |
Format.fprintf fmt "Registered fdecls: @[%a@]@ " |
120 |
(Utils.fprintf_list ~sep:"@ " Format.pp_print_string) (Hashtbl.fold (fun id _ accu -> id::accu) decls []) |
121 |
|
122 |
|
123 |
let decl_var id = |
124 |
(* Format.eprintf "Declaring var %s@." id.var_id; *) |
125 |
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in |
126 |
register_fdecl id.var_id fdecl; |
127 |
fdecl |
128 |
|
129 |
(* Declaring the function used in expr *) |
130 |
let decl_fun op args typ = |
131 |
let args = List.map type_to_sort args in |
132 |
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in |
133 |
register_fdecl op fdecl; |
134 |
fdecl |
135 |
|
136 |
let idx_sort = int_sort |
137 |
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort |
138 |
let uid_conc = |
139 |
let fd = Z3.Z3List.get_cons_decl uid_sort in |
140 |
fun head tail -> Z3.FuncDecl.apply fd [head;tail] |
141 |
|
142 |
let get_instance_uid = |
143 |
let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in |
144 |
let cpt = ref 0 in |
145 |
fun i -> |
146 |
let id = |
147 |
if Hashtbl.mem hash i then |
148 |
Hashtbl.find hash i |
149 |
else ( |
150 |
incr cpt; |
151 |
Hashtbl.add hash i !cpt; |
152 |
!cpt |
153 |
) |
154 |
in |
155 |
Z3.Arithmetic.Integer.mk_numeral_i !ctx id |
156 |
|
157 |
|
158 |
|
159 |
let decl_rel ?(no_additional_vars=false) name args_sorts = |
160 |
(* Enriching arg_sorts with two new variables: a counting index and an |
161 |
uid *) |
162 |
let args_sorts = |
163 |
if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in |
164 |
|
165 |
(* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *) |
166 |
if !debug then |
167 |
Format.eprintf "Registering fdecl %s (%a)@." |
168 |
name |
169 |
(Utils.fprintf_list ~sep:"@ " |
170 |
(fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort))) |
171 |
args_sorts |
172 |
; |
173 |
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in |
174 |
Z3.Fixedpoint.register_relation !fp fdecl; |
175 |
register_fdecl name fdecl; |
176 |
fdecl |
177 |
|
178 |
|
179 |
|
180 |
(* Shared variables to describe counter and uid *) |
181 |
|
182 |
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int |
183 |
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) |
184 |
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int |
185 |
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort |
186 |
let _ = register_fdecl "__uid__" uid_fd |
187 |
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd |
188 |
|
189 |
(** Conversion functions |
190 |
|
191 |
The following is similar to the Horn backend. Each printing function is |
192 |
rephrased from pp_xx to xx_to_expr and produces a Z3 value. |
193 |
|
194 |
*) |
195 |
|
196 |
|
197 |
(* Returns the f_decl associated to the variable v *) |
198 |
let horn_var_to_expr v = |
199 |
Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id) |
200 |
|
201 |
|
202 |
|
203 |
|
204 |
(* Used to print boolean constants *) |
205 |
let horn_tag_to_expr t = |
206 |
if t = tag_true then |
207 |
Z3.Boolean.mk_true !ctx |
208 |
else if t = tag_false then |
209 |
Z3.Boolean.mk_false !ctx |
210 |
else |
211 |
(* Finding the associated sort *) |
212 |
let sort = get_tag_sort t in |
213 |
let elems = get_sort_elems sort in |
214 |
let res : Z3.Expr.expr option = |
215 |
List.fold_left2 (fun res cst expr -> |
216 |
match res with |
217 |
| Some _ -> res |
218 |
| None -> if t = cst then Some (expr:Z3.Expr.expr) else None |
219 |
) None elems (Z3.Enumeration.get_consts sort) |
220 |
in |
221 |
match res with None -> assert false | Some s -> s |
222 |
|
223 |
(* Prints a constant value *) |
224 |
let rec horn_const_to_expr c = |
225 |
match c with |
226 |
| Const_int i -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i |
227 |
| Const_real r -> Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r) |
228 |
| Const_tag t -> horn_tag_to_expr t |
229 |
| _ -> assert false |
230 |
|
231 |
|
232 |
|
233 |
(* Default value for each type, used when building arrays. Eg integer array |
234 |
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value |
235 |
for the type integer (arrays). |
236 |
*) |
237 |
let rec horn_default_val t = |
238 |
let t = Types.dynamic_type t in |
239 |
if Types.is_bool_type t then Z3.Boolean.mk_true !ctx else |
240 |
if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else |
241 |
if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else |
242 |
(* match (Types.dynamic_type t).Types.tdesc with |
243 |
* | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\) |
244 |
* let valt = Types.array_element_type t in |
245 |
* fprintf fmt "((as const (Array Int %a)) %a)" |
246 |
* pp_type valt |
247 |
* pp_default_val valt |
248 |
* | Types.Tstruct(l) -> assert false |
249 |
* | Types.Ttuple(l) -> assert false |
250 |
* |_ -> *) assert false |
251 |
|
252 |
(* Conversion of basic library functions *) |
253 |
|
254 |
let horn_basic_app i vl (vltyp, typ) = |
255 |
match i, vl with |
256 |
| "ite", [v1; v2; v3] -> Z3.Boolean.mk_ite !ctx v1 v2 v3 |
257 |
| "uminus", [v] -> Z3.Arithmetic.mk_unary_minus |
258 |
!ctx v |
259 |
| "not", [v] -> |
260 |
Z3.Boolean.mk_not |
261 |
!ctx v |
262 |
| "=", [v1; v2] -> |
263 |
Z3.Boolean.mk_eq |
264 |
!ctx v1 v2 |
265 |
| "&&", [v1; v2] -> |
266 |
Z3.Boolean.mk_and |
267 |
!ctx |
268 |
[v1; v2] |
269 |
| "||", [v1; v2] -> |
270 |
Z3.Boolean.mk_or |
271 |
!ctx |
272 |
[v1; |
273 |
v2] |
274 |
|
275 |
| "impl", [v1; v2] -> |
276 |
Z3.Boolean.mk_implies |
277 |
!ctx v1 v2 |
278 |
| "mod", [v1; v2] -> |
279 |
Z3.Arithmetic.Integer.mk_mod |
280 |
!ctx v1 v2 |
281 |
| "equi", [v1; v2] -> |
282 |
Z3.Boolean.mk_eq |
283 |
!ctx |
284 |
v1 v2 |
285 |
| "xor", [v1; v2] -> |
286 |
Z3.Boolean.mk_xor |
287 |
!ctx v1 v2 |
288 |
| "!=", [v1; v2] -> |
289 |
Z3.Boolean.mk_not |
290 |
!ctx |
291 |
( |
292 |
Z3.Boolean.mk_eq |
293 |
!ctx v1 v2 |
294 |
) |
295 |
| "/", [v1; v2] -> |
296 |
Z3.Arithmetic.mk_div |
297 |
!ctx v1 v2 |
298 |
|
299 |
| "+", [v1; v2] -> |
300 |
Z3.Arithmetic.mk_add |
301 |
!ctx |
302 |
[v1; v2] |
303 |
| "-", [v1; v2] -> |
304 |
Z3.Arithmetic.mk_sub |
305 |
!ctx |
306 |
[v1 ; v2] |
307 |
|
308 |
| "*", [v1; v2] -> |
309 |
Z3.Arithmetic.mk_mul |
310 |
!ctx |
311 |
[ v1; v2] |
312 |
|
313 |
|
314 |
| "<", [v1; v2] -> |
315 |
Z3.Arithmetic.mk_lt |
316 |
!ctx v1 v2 |
317 |
| "<=", [v1; v2] -> |
318 |
Z3.Arithmetic.mk_le |
319 |
!ctx v1 v2 |
320 |
| ">", [v1; v2] -> |
321 |
Z3.Arithmetic.mk_gt |
322 |
!ctx v1 v2 |
323 |
| ">=", [v1; v2] -> |
324 |
Z3.Arithmetic.mk_ge |
325 |
!ctx v1 v2 |
326 |
| "int_to_real", [v1] -> |
327 |
Z3.Arithmetic.Integer.mk_int2real |
328 |
!ctx v1 |
329 |
| _ -> |
330 |
let fd = |
331 |
try |
332 |
get_fdecl i |
333 |
with Not_found -> begin |
334 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) -> %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); |
335 |
decl_fun i vltyp typ |
336 |
end |
337 |
in |
338 |
Z3.FuncDecl.apply fd vl |
339 |
|
340 |
|
341 |
(* | _, [v1; v2] -> Z3.Boolean.mk_and |
342 |
* !ctx |
343 |
* (val_to_expr v1) |
344 |
* (val_to_expr v2) |
345 |
* |
346 |
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) |
347 |
|
348 |
(* | _ -> ( |
349 |
* let msg fmt = Format.fprintf fmt |
350 |
* "internal error: zustre unkown function %s (nb args = %i)@." |
351 |
* i (List.length vl) |
352 |
* in |
353 |
* raise (UnknownFunction(i, msg)) |
354 |
* ) *) |
355 |
|
356 |
|
357 |
(* Convert a value expression [v], with internal function calls only. [pp_var] |
358 |
is a printer for variables (typically [pp_c_var_read]), but an offset suffix |
359 |
may be added for array variables |
360 |
*) |
361 |
let rec horn_val_to_expr ?(is_lhs=false) m self v = |
362 |
(* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *) |
363 |
match v.value_desc with |
364 |
| Cst c -> horn_const_to_expr c |
365 |
|
366 |
(* Code specific for arrays *) |
367 |
| Array il -> |
368 |
(* An array definition: |
369 |
(store ( |
370 |
... |
371 |
(store ( |
372 |
store ( |
373 |
default_val |
374 |
) |
375 |
idx_n val_n |
376 |
) |
377 |
idx_n-1 val_n-1) |
378 |
... |
379 |
idx_1 val_1 |
380 |
) *) |
381 |
let rec build_array (tab, x) = |
382 |
match tab with |
383 |
| [] -> horn_default_val v.value_type(* (get_type v) *) |
384 |
| h::t -> |
385 |
Z3.Z3Array.mk_store |
386 |
!ctx |
387 |
(build_array (t, (x+1))) |
388 |
(Z3.Arithmetic.Integer.mk_numeral_i !ctx x) |
389 |
(horn_val_to_expr ~is_lhs:is_lhs m self h) |
390 |
in |
391 |
build_array (il, 0) |
392 |
|
393 |
| Access(tab,index) -> |
394 |
Z3.Z3Array.mk_select !ctx |
395 |
(horn_val_to_expr ~is_lhs:is_lhs m self tab) |
396 |
(horn_val_to_expr ~is_lhs:is_lhs m self index) |
397 |
|
398 |
(* Code specific for arrays *) |
399 |
|
400 |
| Power (v, n) -> assert false |
401 |
| Var v -> |
402 |
if is_memory m v then |
403 |
if Types.is_array_type v.var_type |
404 |
then assert false |
405 |
else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
406 |
|
407 |
else |
408 |
horn_var_to_expr |
409 |
(rename_machine |
410 |
self |
411 |
v) |
412 |
| Fun (n, vl) -> horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v -> v.value_type) vl, v.value_type) |
413 |
|
414 |
let no_reset_to_exprs machines m i = |
415 |
let (n,_) = List.assoc i m.minstances in |
416 |
let target_machine = List.find (fun m -> m.mname.node_id = (Corelang.node_name n)) machines in |
417 |
|
418 |
let m_list = |
419 |
rename_machine_list |
420 |
(concat m.mname.node_id i) |
421 |
(rename_mid_list (full_memory_vars machines target_machine)) |
422 |
in |
423 |
let c_list = |
424 |
rename_machine_list |
425 |
(concat m.mname.node_id i) |
426 |
(rename_current_list (full_memory_vars machines target_machine)) |
427 |
in |
428 |
match c_list, m_list with |
429 |
| [chd], [mhd] -> |
430 |
let expr = |
431 |
Z3.Boolean.mk_eq !ctx |
432 |
(horn_var_to_expr mhd) |
433 |
(horn_var_to_expr chd) |
434 |
in |
435 |
[expr] |
436 |
| _ -> ( |
437 |
let exprs = |
438 |
List.map2 (fun mhd chd -> |
439 |
Z3.Boolean.mk_eq !ctx |
440 |
(horn_var_to_expr mhd) |
441 |
(horn_var_to_expr chd) |
442 |
) |
443 |
m_list |
444 |
c_list |
445 |
in |
446 |
exprs |
447 |
) |
448 |
|
449 |
let instance_reset_to_exprs machines m i = |
450 |
let (n,_) = List.assoc i m.minstances in |
451 |
let target_machine = List.find (fun m -> m.mname.node_id = (Corelang.node_name n)) machines in |
452 |
let vars = |
453 |
(rename_machine_list |
454 |
(concat m.mname.node_id i) |
455 |
(rename_current_list (full_memory_vars machines target_machine))@ (rename_mid_list (full_memory_vars machines target_machine)) |
456 |
) |
457 |
|
458 |
in |
459 |
let expr = |
460 |
Z3.Expr.mk_app |
461 |
!ctx |
462 |
(get_fdecl (machine_reset_name (Corelang.node_name n))) |
463 |
(List.map (horn_var_to_expr) (idx::uid::vars)) |
464 |
in |
465 |
[expr] |
466 |
|
467 |
let instance_call_to_exprs machines reset_instances m i inputs outputs = |
468 |
let self = m.mname.node_id in |
469 |
|
470 |
(* Building call args *) |
471 |
let idx_uid_inout = |
472 |
(* Additional input to register step counters, and uid *) |
473 |
let idx = horn_var_to_expr idx in |
474 |
let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in |
475 |
let inout = |
476 |
List.map (horn_val_to_expr m self) |
477 |
(inputs @ (List.map (fun v -> mk_val (Var v) v.var_type) outputs)) |
478 |
in |
479 |
idx::uid::inout |
480 |
in |
481 |
|
482 |
try (* stateful node instance *) |
483 |
begin |
484 |
let (n,_) = List.assoc i m.minstances in |
485 |
let target_machine = List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines in |
486 |
|
487 |
(* Checking whether this specific instances has been reset yet *) |
488 |
let reset_exprs = |
489 |
if not (List.mem i reset_instances) then |
490 |
(* If not, declare mem_m = mem_c *) |
491 |
no_reset_to_exprs machines m i |
492 |
else |
493 |
[] (* Nothing to add yet *) |
494 |
in |
495 |
|
496 |
let mems = full_memory_vars machines target_machine in |
497 |
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in |
498 |
let mid_mems = rename_mems rename_mid_list in |
499 |
let next_mems = rename_mems rename_next_list in |
500 |
|
501 |
let call_expr = |
502 |
match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with |
503 |
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin |
504 |
let stmt1 = (* out = ite mem_m then i1 else i2 *) |
505 |
Z3.Boolean.mk_eq !ctx |
506 |
( (* output var *) |
507 |
horn_val_to_expr |
508 |
~is_lhs:true |
509 |
m self |
510 |
(mk_val (Var o) o.var_type) |
511 |
) |
512 |
( |
513 |
Z3.Boolean.mk_ite !ctx |
514 |
(horn_var_to_expr mem_m) |
515 |
(horn_val_to_expr m self i1) |
516 |
(horn_val_to_expr m self i2) |
517 |
) |
518 |
in |
519 |
let stmt2 = (* mem_X = false *) |
520 |
Z3.Boolean.mk_eq !ctx |
521 |
(horn_var_to_expr mem_x) |
522 |
(Z3.Boolean.mk_false !ctx) |
523 |
in |
524 |
[stmt1; stmt2] |
525 |
end |
526 |
|
527 |
| node_name_n -> |
528 |
let expr = |
529 |
Z3.Expr.mk_app |
530 |
!ctx |
531 |
(get_fdecl (machine_step_name (node_name n))) |
532 |
( (* Arguments are input, output, mid_mems, next_mems *) |
533 |
idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems) |
534 |
|
535 |
) |
536 |
in |
537 |
[expr] |
538 |
in |
539 |
|
540 |
reset_exprs@call_expr |
541 |
end |
542 |
with Not_found -> ( (* stateless node instance *) |
543 |
let (n,_) = List.assoc i m.mcalls in |
544 |
let expr = |
545 |
Z3.Expr.mk_app |
546 |
!ctx |
547 |
(get_fdecl (machine_stateless_name (node_name n))) |
548 |
idx_uid_inout (* Arguments are inputs, outputs *) |
549 |
in |
550 |
[expr] |
551 |
) |
552 |
|
553 |
|
554 |
|
555 |
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *) |
556 |
(* let rec value_suffix_to_expr self value = *) |
557 |
(* match value.value_desc with *) |
558 |
(* | Fun (n, vl) -> *) |
559 |
(* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *) |
560 |
|
561 |
(* | _ -> *) |
562 |
(* horn_val_to_expr self value *) |
563 |
|
564 |
|
565 |
(* type_directed assignment: array vs. statically sized type |
566 |
- [var_type]: type of variable to be assigned |
567 |
- [var_name]: name of variable to be assigned |
568 |
- [value]: assigned value |
569 |
- [pp_var]: printer for variables |
570 |
*) |
571 |
let assign_to_exprs m var_name value = |
572 |
let self = m.mname.node_id in |
573 |
let e = |
574 |
Z3.Boolean.mk_eq |
575 |
!ctx |
576 |
(horn_val_to_expr ~is_lhs:true m self var_name) |
577 |
(horn_val_to_expr m self value) |
578 |
(* was: TODO deal with array accesses (value_suffix_to_expr self value) *) |
579 |
in |
580 |
[e] |
581 |
|
582 |
|
583 |
(* Convert instruction to Z3.Expr and update the set of reset instances *) |
584 |
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list = |
585 |
match Corelang.get_instr_desc instr with |
586 |
| MComment _ -> [], reset_instances |
587 |
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *) |
588 |
no_reset_to_exprs machines m i, |
589 |
i::reset_instances |
590 |
| MReset i -> (* we assign middle_mem with reset: reset(mem_m) *) |
591 |
instance_reset_to_exprs machines m i, |
592 |
i::reset_instances |
593 |
| MLocalAssign (i,v) -> |
594 |
assign_to_exprs |
595 |
m |
596 |
(mk_val (Var i) i.var_type) v, |
597 |
reset_instances |
598 |
| MStateAssign (i,v) -> |
599 |
assign_to_exprs |
600 |
m |
601 |
(mk_val (Var i) i.var_type) v, |
602 |
reset_instances |
603 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) -> |
604 |
assert false (* This should not happen anymore *) |
605 |
| MStep (il, i, vl) -> |
606 |
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = |
607 |
mem_c and print the call to mem_m *) |
608 |
instance_call_to_exprs machines reset_instances m i vl il, |
609 |
reset_instances (* Since this instance call will only happen once, we |
610 |
don't have to update reset_instances *) |
611 |
|
612 |
| MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ... |
613 |
should not be produced yet. Later, we will have to |
614 |
compare the reset_instances of each branch and |
615 |
introduced the mem_m = mem_c for branches to do not |
616 |
address it while other did. Am I clear ? *) |
617 |
(* For each branch we obtain the logical encoding, and the information |
618 |
whether a sub node has been reset or not. If a node has been reset in one |
619 |
of the branch, then all others have to have the mem_m = mem_c |
620 |
statement. *) |
621 |
let self = m.mname.node_id in |
622 |
let branch_to_expr (tag, instrs) = |
623 |
let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in |
624 |
let e = |
625 |
Z3.Boolean.mk_implies !ctx |
626 |
(Z3.Boolean.mk_eq !ctx |
627 |
(horn_val_to_expr m self g) |
628 |
(horn_tag_to_expr tag)) |
629 |
branch_def in |
630 |
|
631 |
[e], branch_resets |
632 |
|
633 |
in |
634 |
List.fold_left (fun (instrs, resets) b -> |
635 |
let b_instrs, b_resets = branch_to_expr b in |
636 |
instrs@b_instrs, resets@b_resets |
637 |
) ([], reset_instances) hl |
638 |
| MSpec _ -> assert false |
639 |
|
640 |
and instrs_to_expr machines reset_instances m instrs = |
641 |
let instr_to_exprs rs i = instr_to_exprs machines rs m i in |
642 |
let e_list, rs = |
643 |
match instrs with |
644 |
| [x] -> instr_to_exprs reset_instances x |
645 |
| _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *) |
646 |
|
647 |
List.fold_left (fun (exprs, rs) i -> |
648 |
let exprs_i, rs_i = instr_to_exprs rs i in |
649 |
exprs@exprs_i, rs@rs_i |
650 |
) |
651 |
([], reset_instances) instrs |
652 |
|
653 |
|
654 |
| [] -> [], reset_instances |
655 |
in |
656 |
let e = |
657 |
match e_list with |
658 |
| [e] -> e |
659 |
| [] -> Z3.Boolean.mk_true !ctx |
660 |
| _ -> Z3.Boolean.mk_and !ctx e_list |
661 |
in |
662 |
e, rs |
663 |
|
664 |
|
665 |
(*********************************************************) |
666 |
|
667 |
(* Quantifiying universally all occuring variables *) |
668 |
let add_rule ?(dont_touch=[]) vars expr = |
669 |
(* let fds = Z3.Expr.get_args expr in *) |
670 |
(* Format.eprintf "Expr %s: args: [%a]@." *) |
671 |
(* (Z3.Expr.to_string expr) *) |
672 |
(* (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *) |
673 |
|
674 |
(* (\* Old code relying on provided vars *\) *) |
675 |
(* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *) |
676 |
(* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *) |
677 |
|
678 |
(* New code: we extract vars from expr *) |
679 |
let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl |
680 |
let compare = compare |
681 |
let hash = Hashtbl.hash |
682 |
end) |
683 |
in |
684 |
(* Fonction seems unused |
685 |
|
686 |
let rec get_expr_vars e = |
687 |
let open Utils in |
688 |
let nb_args = Z3.Expr.get_num_args e in |
689 |
if nb_args <= 0 then ( |
690 |
let fdecl = Z3.Expr.get_func_decl e in |
691 |
(* let params = Z3.FuncDecl.get_parameters fdecl in *) |
692 |
(* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *) |
693 |
let dkind = Z3.FuncDecl.get_decl_kind fdecl in |
694 |
match dkind with Z3enums.OP_UNINTERPRETED -> ( |
695 |
(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *) |
696 |
(* let open Z3.FuncDecl.Parameter in *) |
697 |
(* List.iter (fun p -> *) |
698 |
(* match p with *) |
699 |
(* P_Int i -> Format.eprintf "int %i" i *) |
700 |
(* | P_Dbl f -> Format.eprintf "dbl %f" f *) |
701 |
(* | P_Sym s -> Format.eprintf "symb" *) |
702 |
(* | P_Srt s -> Format.eprintf "sort" *) |
703 |
(* | P_Ast _ ->Format.eprintf "ast" *) |
704 |
(* | P_Fdl f -> Format.eprintf "fundecl" *) |
705 |
(* | P_Rat s -> Format.eprintf "rat %s" s *) |
706 |
|
707 |
(* ) params; *) |
708 |
(* Format.eprintf "]@."; *) |
709 |
FDSet.singleton fdecl |
710 |
) |
711 |
| _ -> FDSet.empty |
712 |
) |
713 |
else (*if nb_args > 0 then*) |
714 |
List.fold_left |
715 |
(fun accu e -> FDSet.union accu (get_expr_vars e)) |
716 |
FDSet.empty (Z3.Expr.get_args e) |
717 |
in |
718 |
*) |
719 |
(* Unsed variable. Coul;d be reintroduced |
720 |
let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in |
721 |
let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in |
722 |
let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in |
723 |
*) |
724 |
if !debug then ( |
725 |
Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @." |
726 |
(Z3.Expr.to_string expr) |
727 |
(Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) |
728 |
) |
729 |
; |
730 |
let expr = Z3.Quantifier.mk_forall_const |
731 |
!ctx (* context *) |
732 |
(List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *) |
733 |
(* sorts (\* sort list*\) *) |
734 |
(* symbols (\* symbol list *\) *) |
735 |
expr (* expression *) |
736 |
None (* quantifier weight, None means 1 *) |
737 |
[] (* pattern list ? *) |
738 |
[] (* ? *) |
739 |
None (* ? *) |
740 |
None (* ? *) |
741 |
in |
742 |
(* Format.eprintf "OK@.@?"; *) |
743 |
|
744 |
(* |
745 |
TODO: bizarre la declaration de INIT tout seul semble poser pb. |
746 |
*) |
747 |
Z3.Fixedpoint.add_rule !fp |
748 |
(Z3.Quantifier.expr_of_quantifier expr) |
749 |
None |
750 |
|
751 |
|
752 |
(********************************************************) |
753 |
|
754 |
let machine_reset machines m = |
755 |
let locals = local_memory_vars machines m in |
756 |
|
757 |
(* print "x_m = x_c" for each local memory *) |
758 |
let mid_mem_def = |
759 |
List.map (fun v -> |
760 |
Z3.Boolean.mk_eq !ctx |
761 |
(horn_var_to_expr (rename_mid v)) |
762 |
(horn_var_to_expr (rename_current v)) |
763 |
) locals |
764 |
in |
765 |
|
766 |
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. |
767 |
Special treatment for _arrow: _first = true |
768 |
*) |
769 |
|
770 |
let reset_instances = |
771 |
|
772 |
List.map (fun (id, (n, _)) -> |
773 |
let name = node_name n in |
774 |
if name = "_arrow" then ( |
775 |
Z3.Boolean.mk_eq !ctx |
776 |
( |
777 |
let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in |
778 |
Z3.Expr.mk_const_f !ctx vdecl |
779 |
) |
780 |
(Z3.Boolean.mk_true !ctx) |
781 |
|
782 |
) else ( |
783 |
let machine_n = get_machine machines name in |
784 |
|
785 |
Z3.Expr.mk_app |
786 |
!ctx |
787 |
(get_fdecl (name ^ "_reset")) |
788 |
(List.map (horn_var_to_expr) |
789 |
(idx::uid:: (* Additional vars: counters, uid *) |
790 |
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) |
791 |
)) |
792 |
|
793 |
) |
794 |
) m.minstances |
795 |
|
796 |
|
797 |
in |
798 |
|
799 |
Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances) |
800 |
|
801 |
|
802 |
|
803 |
(* TODO: empty list means true statement *) |
804 |
let decl_machine machines m = |
805 |
if m.mname.node_id = Arrow.arrow_id then |
806 |
(* We don't do arrow function *) |
807 |
() |
808 |
else |
809 |
begin |
810 |
let _ = |
811 |
List.map decl_var |
812 |
( |
813 |
(inout_vars machines m)@ |
814 |
(rename_current_list (full_memory_vars machines m)) @ |
815 |
(rename_mid_list (full_memory_vars machines m)) @ |
816 |
(rename_next_list (full_memory_vars machines m)) @ |
817 |
(rename_machine_list m.mname.node_id m.mstep.step_locals) |
818 |
) |
819 |
in |
820 |
if is_stateless m then |
821 |
begin |
822 |
if !debug then |
823 |
Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id; |
824 |
|
825 |
(* Declaring single predicate *) |
826 |
let vars = inout_vars machines m in |
827 |
let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in |
828 |
let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in |
829 |
|
830 |
let horn_body, _ (* don't care for reset here *) = |
831 |
instrs_to_expr |
832 |
machines |
833 |
([] (* No reset info for stateless nodes *) ) |
834 |
m |
835 |
m.mstep.step_instrs |
836 |
in |
837 |
let horn_head = |
838 |
Z3.Expr.mk_app |
839 |
!ctx |
840 |
(get_fdecl (machine_stateless_name m.mname.node_id)) |
841 |
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) |
842 |
in |
843 |
(* this line seems useless *) |
844 |
let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in |
845 |
(* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *) |
846 |
match m.mstep.step_asserts with |
847 |
| [] -> |
848 |
begin |
849 |
(* Rule for single predicate : "; Stateless step rule @." *) |
850 |
(*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*) |
851 |
(* TODO clean code *) |
852 |
(* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *) |
853 |
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) |
854 |
|
855 |
end |
856 |
| assertsl -> |
857 |
begin |
858 |
(*Rule for step "; Stateless step rule with Assertions @.";*) |
859 |
let body_with_asserts = |
860 |
Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) |
861 |
in |
862 |
let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in |
863 |
add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head) |
864 |
end |
865 |
end |
866 |
else |
867 |
begin |
868 |
|
869 |
(* Rule for reset *) |
870 |
|
871 |
let vars = reset_vars machines m in |
872 |
let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in |
873 |
let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in |
874 |
let horn_reset_body = machine_reset machines m in |
875 |
let horn_reset_head = |
876 |
Z3.Expr.mk_app |
877 |
!ctx |
878 |
(get_fdecl (machine_reset_name m.mname.node_id)) |
879 |
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) |
880 |
in |
881 |
|
882 |
|
883 |
let _ = |
884 |
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head) |
885 |
|
886 |
in |
887 |
|
888 |
(* Rule for step*) |
889 |
let vars = step_vars machines m in |
890 |
let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in |
891 |
let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in |
892 |
let horn_step_body, _ (* don't care for reset here *) = |
893 |
instrs_to_expr |
894 |
machines |
895 |
[] |
896 |
m |
897 |
m.mstep.step_instrs |
898 |
in |
899 |
let horn_step_head = |
900 |
Z3.Expr.mk_app |
901 |
!ctx |
902 |
(get_fdecl (machine_step_name m.mname.node_id)) |
903 |
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) |
904 |
in |
905 |
match m.mstep.step_asserts with |
906 |
| [] -> |
907 |
begin |
908 |
(* Rule for single predicate *) |
909 |
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in |
910 |
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head) |
911 |
|
912 |
end |
913 |
| assertsl -> |
914 |
begin |
915 |
(* Rule for step Assertions @.; *) |
916 |
let body_with_asserts = |
917 |
Z3.Boolean.mk_and !ctx |
918 |
(horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) |
919 |
in |
920 |
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in |
921 |
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head) |
922 |
|
923 |
end |
924 |
|
925 |
end |
926 |
end |
927 |
|
928 |
|
929 |
|
930 |
(* Debug functions *) |
931 |
(* |
932 |
let rec extract_expr_fds e = |
933 |
(* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *) |
934 |
(* (Z3.Expr.to_string e); *) |
935 |
|
936 |
(* Removing quantifier is there are some *) |
937 |
let e = (* I didn't found a nicer way to do it than with an exception. My |
938 |
bad *) |
939 |
try |
940 |
let eq = Z3.Quantifier.quantifier_of_expr e in |
941 |
let e2 = Z3.Quantifier.get_body eq in |
942 |
(* Format.eprintf "Extracted quantifier body@ "; *) |
943 |
e2 |
944 |
|
945 |
with _ -> Format.eprintf "No quantifier info@ "; e |
946 |
in |
947 |
let _ = |
948 |
try |
949 |
( |
950 |
let fd = Z3.Expr.get_func_decl e in |
951 |
let fd_symbol = Z3.FuncDecl.get_name fd in |
952 |
let fd_name = Z3.Symbol.to_string fd_symbol in |
953 |
if not (Hashtbl.mem decls fd_name) then |
954 |
register_fdecl fd_name fd; |
955 |
(* Format.eprintf "fdecls (%s): %s@ " *) |
956 |
(* fd_name *) |
957 |
(* (Z3.FuncDecl.to_string fd); *) |
958 |
try |
959 |
( |
960 |
let args = Z3.Expr.get_args e in |
961 |
(* Format.eprintf "@[<v>@ "; *) |
962 |
(* List.iter extract_expr_fds args; *) |
963 |
(* Format.eprintf "@]@ "; *) |
964 |
() |
965 |
) |
966 |
with _ -> |
967 |
Format.eprintf "Impossible to extract fundecl args for expression %s@ " |
968 |
(Z3.Expr.to_string e) |
969 |
) |
970 |
with _ -> |
971 |
Format.eprintf "Impossible to extract anything from expression %s@ " |
972 |
(Z3.Expr.to_string e) |
973 |
in |
974 |
(* Format.eprintf "@]@ " *) |
975 |
() |
976 |
*) |
977 |
(* Local Variables: *) |
978 |
(* compile-command:"make -C ../.." *) |
979 |
(* End: *) |