lustrec / src / tools / zustre / zustre_common.ml @ 04a188ec
History  View  Annotate  Download (29.5 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 
module HBC = Horn_backend_common 
10 
let node_name = HBC.node_name 
11  
12 
let concat = HBC.concat 
13  
14 
let rename_machine = HBC.rename_machine 
15 
let rename_machine_list = HBC.rename_machine_list 
16  
17 
let rename_next = HBC.rename_next 
18 
let rename_mid = HBC.rename_mid 
19 
let rename_current = HBC.rename_current 
20  
21 
let rename_current_list = HBC.rename_current_list 
22 
let rename_mid_list = HBC.rename_mid_list 
23 
let rename_next_list = HBC.rename_next_list 
24  
25 
let full_memory_vars = HBC.full_memory_vars 
26 
let inout_vars = HBC.inout_vars 
27 
let reset_vars = HBC.reset_vars 
28 
let step_vars = HBC.step_vars 
29 
let local_memory_vars = HBC.local_memory_vars 
30 
let step_vars_m_x = HBC.step_vars_m_x 
31 
let step_vars_c_m_x = HBC.step_vars_c_m_x 
32 

33 
let machine_reset_name = HBC.machine_reset_name 
34 
let machine_step_name = HBC.machine_step_name 
35 
let machine_stateless_name = HBC.machine_stateless_name 
36  
37 
let preprocess = Horn_backend.preprocess 
38 

39  
40 
exception UnknownFunction of (string * (Format.formatter > unit)) 
41 
(** Sorts 
42  
43 
A sort is introduced for each basic type and each enumerated type. 
44  
45 
A hashtbl records these and allow easy access to sort values, when 
46 
provided with a enumerated type name. 
47  
48 
*) 
49 

50 
let bool_sort = Z3.Boolean.mk_sort !ctx 
51 
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx 
52 
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx 
53  
54  
55 
let get_const_sort = Hashtbl.find const_sorts 
56 
let get_sort_elems = Hashtbl.find sort_elems 
57 
let get_tag_sort id = try Hashtbl.find const_tags id with _ > Format.eprintf "Unable to find sort for tag=%s@." id; assert false 
58 

59  
60 

61 
let decl_sorts () = 
62 
Hashtbl.iter (fun typ decl > 
63 
match typ with 
64 
 Tydec_const var > 
65 
(match decl.top_decl_desc with 
66 
 TypeDef tdef > ( 
67 
match tdef.tydef_desc with 
68 
 Tydec_enum tl > 
69 
let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in 
70 
Hashtbl.add const_sorts var new_sort; 
71 
Hashtbl.add sort_elems new_sort tl; 
72 
List.iter (fun t > Hashtbl.add const_tags t new_sort) tl 
73 

74 
 _ > Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false 
75 
) 
76 
 _ > assert false 
77 
) 
78 
 _ > ()) Corelang.type_table 
79  
80 

81 
let rec type_to_sort t = 
82 
if Types.is_bool_type t then bool_sort else 
83 
if Types.is_int_type t then int_sort else 
84 
if Types.is_real_type t then real_sort else 
85 
match (Types.repr t).Types.tdesc with 
86 
 Types.Tconst ty > get_const_sort ty 
87 
 Types.Tclock t > type_to_sort t 
88 
 Types.Tarray(dim,ty) > Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty) 
89 
 Types.Tstatic(d, ty)> type_to_sort ty 
90 
 Types.Tarrow _ 
91 
 _ > Format.eprintf "internal error: pp_type %a@." 
92 
Types.print_ty t; assert false 
93  
94  
95 
(* let idx_var = *) 
96 
(* Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort *) 
97 

98 
(* let uid_var = *) 
99 
(* Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort *) 
100  
101 
(** Func decls 
102  
103 
Similarly fun_decls are registerd, by their name, into a hashtbl. The 
104 
proposed encoding introduces a 0ary fun_decl to model variables and 
105 
fun_decl with arguments to declare reset and step predicates. 
106  
107  
108  
109 
*) 
110 
let register_fdecl id fd = Hashtbl.add decls id fd 
111 
let get_fdecl id = 
112 
try 
113 
Hashtbl.find decls id 
114 
with Not_found > (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found) 
115  
116 
let pp_fdecls fmt = 
117 
Format.fprintf fmt "Registered fdecls: @[%a@]@ " 
118 
(Utils.fprintf_list ~sep:"@ " Format.pp_print_string) (Hashtbl.fold (fun id _ accu > id::accu) decls []) 
119  
120 

121 
let decl_var id = 
122 
(* Format.eprintf "Declaring var %s@." id.var_id; *) 
123 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in 
124 
register_fdecl id.var_id fdecl; 
125 
fdecl 
126  
127 
let idx_sort = int_sort 
128 
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort 
129 
let uid_conc = 
130 
let fd = Z3.Z3List.get_cons_decl uid_sort in 
131 
fun head tail > Z3.FuncDecl.apply fd [head;tail] 
132  
133 
let get_instance_uid = 
134 
let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in 
135 
let cpt = ref 0 in 
136 
fun i > 
137 
let id = 
138 
if Hashtbl.mem hash i then 
139 
Hashtbl.find hash i 
140 
else ( 
141 
incr cpt; 
142 
Hashtbl.add hash i !cpt; 
143 
!cpt 
144 
) 
145 
in 
146 
Z3.Arithmetic.Integer.mk_numeral_i !ctx id 
147 

148  
149 

150 
let decl_rel ?(no_additional_vars=false) name args_sorts = 
151 
(* Enriching arg_sorts with two new variables: a counting index and an 
152 
uid *) 
153 
let args_sorts = 
154 
if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in 
155 

156 
(* let args_sorts = List.map (fun v > type_to_sort v.var_type) args in *) 
157 
if !debug then 
158 
Format.eprintf "Registering fdecl %s (%a)@." 
159 
name 
160 
(Utils.fprintf_list ~sep:"@ " 
161 
(fun fmt sort > Format.fprintf fmt "%s" (Z3.Sort.to_string sort))) 
162 
args_sorts 
163 
; 
164 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in 
165 
Z3.Fixedpoint.register_relation !fp fdecl; 
166 
register_fdecl name fdecl; 
167 
fdecl 
168 

169  
170  
171 
(* Shared variables to describe counter and uid *) 
172  
173 
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int 
174 
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) 
175 
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int 
176 
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort 
177 
let _ = register_fdecl "__uid__" uid_fd 
178 
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 
179  
180 
(** Conversion functions 
181  
182 
The following is similar to the Horn backend. Each printing function is 
183 
rephrased from pp_xx to xx_to_expr and produces a Z3 value. 
184  
185 
*) 
186  
187  
188 
(* Returns the f_decl associated to the variable v *) 
189 
let horn_var_to_expr v = 
190 
Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id) 
191  
192  
193  
194  
195 
(* Used to print boolean constants *) 
196 
let horn_tag_to_expr t = 
197 
if t = tag_true then 
198 
Z3.Boolean.mk_true !ctx 
199 
else if t = tag_false then 
200 
Z3.Boolean.mk_false !ctx 
201 
else 
202 
(* Finding the associated sort *) 
203 
let sort = get_tag_sort t in 
204 
let elems = get_sort_elems sort in 
205 
let res : Z3.Expr.expr option = 
206 
List.fold_left2 (fun res cst expr > 
207 
match res with 
208 
 Some _ > res 
209 
 None > if t = cst then Some (expr:Z3.Expr.expr) else None 
210 
) None elems (Z3.Enumeration.get_consts sort) 
211 
in 
212 
match res with None > assert false  Some s > s 
213 

214 
(* Prints a constant value *) 
215 
let rec horn_const_to_expr c = 
216 
match c with 
217 
 Const_int i > Z3.Arithmetic.Integer.mk_numeral_i !ctx i 
218 
 Const_real r > Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r) 
219 
 Const_tag t > horn_tag_to_expr t 
220 
 _ > assert false 
221  
222  
223  
224 
(* Default value for each type, used when building arrays. Eg integer array 
225 
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value 
226 
for the type integer (arrays). 
227 
*) 
228 
let rec horn_default_val t = 
229 
let t = Types.dynamic_type t in 
230 
if Types.is_bool_type t then Z3.Boolean.mk_true !ctx else 
231 
if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
232 
if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
233 
(* match (Types.dynamic_type t).Types.tdesc with 
234 
*  Types.Tarray(dim, l) > (\* TODO PL: this strange code has to be (heavily) checked *\) 
235 
* let valt = Types.array_element_type t in 
236 
* fprintf fmt "((as const (Array Int %a)) %a)" 
237 
* pp_type valt 
238 
* pp_default_val valt 
239 
*  Types.Tstruct(l) > assert false 
240 
*  Types.Ttuple(l) > assert false 
241 
* _ > *) assert false 
242  
243 
(* Conversion of basic library functions *) 
244 

245 
let horn_basic_app i val_to_expr vl = 
246 
match i, vl with 
247 
 "ite", [v1; v2; v3] > 
248 
Z3.Boolean.mk_ite 
249 
!ctx 
250 
(val_to_expr v1) 
251 
(val_to_expr v2) 
252 
(val_to_expr v3) 
253  
254 
 "uminus", [v] > 
255 
Z3.Arithmetic.mk_unary_minus 
256 
!ctx 
257 
(val_to_expr v) 
258 
 "not", [v] > 
259 
Z3.Boolean.mk_not 
260 
!ctx 
261 
(val_to_expr v) 
262 
 "=", [v1; v2] > 
263 
Z3.Boolean.mk_eq 
264 
!ctx 
265 
(val_to_expr v1) 
266 
(val_to_expr v2) 
267 
 "&&", [v1; v2] > 
268 
Z3.Boolean.mk_and 
269 
!ctx 
270 
[val_to_expr v1; 
271 
val_to_expr v2] 
272 
 "", [v1; v2] > 
273 
Z3.Boolean.mk_or 
274 
!ctx 
275 
[val_to_expr v1; 
276 
val_to_expr v2] 
277  
278 
 "impl", [v1; v2] > 
279 
Z3.Boolean.mk_implies 
280 
!ctx 
281 
(val_to_expr v1) 
282 
(val_to_expr v2) 
283 
 "mod", [v1; v2] > 
284 
Z3.Arithmetic.Integer.mk_mod 
285 
!ctx 
286 
(val_to_expr v1) 
287 
(val_to_expr v2) 
288 
 "equi", [v1; v2] > 
289 
Z3.Boolean.mk_eq 
290 
!ctx 
291 
(val_to_expr v1) 
292 
(val_to_expr v2) 
293 
 "xor", [v1; v2] > 
294 
Z3.Boolean.mk_xor 
295 
!ctx 
296 
(val_to_expr v1) 
297 
(val_to_expr v2) 
298 
 "!=", [v1; v2] > 
299 
Z3.Boolean.mk_not 
300 
!ctx 
301 
( 
302 
Z3.Boolean.mk_eq 
303 
!ctx 
304 
(val_to_expr v1) 
305 
(val_to_expr v2) 
306 
) 
307 
 "/", [v1; v2] > 
308 
Z3.Arithmetic.mk_div 
309 
!ctx 
310 
(val_to_expr v1) 
311 
(val_to_expr v2) 
312  
313 
 "+", [v1; v2] > 
314 
Z3.Arithmetic.mk_add 
315 
!ctx 
316 
[val_to_expr v1; val_to_expr v2] 
317  
318 
 "", [v1; v2] > 
319 
Z3.Arithmetic.mk_sub 
320 
!ctx 
321 
[val_to_expr v1 ; val_to_expr v2] 
322 

323 
 "*", [v1; v2] > 
324 
Z3.Arithmetic.mk_mul 
325 
!ctx 
326 
[val_to_expr v1; val_to_expr v2] 
327  
328  
329 
 "<", [v1; v2] > 
330 
Z3.Arithmetic.mk_lt 
331 
!ctx 
332 
(val_to_expr v1) 
333 
(val_to_expr v2) 
334  
335 
 "<=", [v1; v2] > 
336 
Z3.Arithmetic.mk_le 
337 
!ctx 
338 
(val_to_expr v1) 
339 
(val_to_expr v2) 
340  
341 
 ">", [v1; v2] > 
342 
Z3.Arithmetic.mk_gt 
343 
!ctx 
344 
(val_to_expr v1) 
345 
(val_to_expr v2) 
346  
347 
 ">=", [v1; v2] > 
348 
Z3.Arithmetic.mk_ge 
349 
!ctx 
350 
(val_to_expr v1) 
351 
(val_to_expr v2) 
352  
353 
 "int_to_real", [v1] > 
354 
Z3.Arithmetic.Integer.mk_int2real 
355 
!ctx 
356 
(val_to_expr v1) 
357  
358 

359 
(*  _, [v1; v2] > Z3.Boolean.mk_and 
360 
* !ctx 
361 
* (val_to_expr v1) 
362 
* (val_to_expr v2) 
363 
* 
364 
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) 
365 
 _ > ( 
366 
let msg fmt = Format.fprintf fmt 
367 
"internal error: zustre unkown function %s (nb args = %i)@." 
368 
i (List.length vl) 
369 
in 
370 
raise (UnknownFunction(i, msg)) 
371 
) 
372  
373 

374 
(* Convert a value expression [v], with internal function calls only. [pp_var] 
375 
is a printer for variables (typically [pp_c_var_read]), but an offset suffix 
376 
may be added for array variables 
377 
*) 
378 
let rec horn_val_to_expr ?(is_lhs=false) m self v = 
379 
match v.value_desc with 
380 
 Cst c > horn_const_to_expr c 
381  
382 
(* Code specific for arrays *) 
383 
 Array il > 
384 
(* An array definition: 
385 
(store ( 
386 
... 
387 
(store ( 
388 
store ( 
389 
default_val 
390 
) 
391 
idx_n val_n 
392 
) 
393 
idx_n1 val_n1) 
394 
... 
395 
idx_1 val_1 
396 
) *) 
397 
let rec build_array (tab, x) = 
398 
match tab with 
399 
 [] > horn_default_val v.value_type(* (get_type v) *) 
400 
 h::t > 
401 
Z3.Z3Array.mk_store 
402 
!ctx 
403 
(build_array (t, (x+1))) 
404 
(Z3.Arithmetic.Integer.mk_numeral_i !ctx x) 
405 
(horn_val_to_expr ~is_lhs:is_lhs m self h) 
406 
in 
407 
build_array (il, 0) 
408 

409 
 Access(tab,index) > 
410 
Z3.Z3Array.mk_select !ctx 
411 
(horn_val_to_expr ~is_lhs:is_lhs m self tab) 
412 
(horn_val_to_expr ~is_lhs:is_lhs m self index) 
413  
414 
(* Code specific for arrays *) 
415 

416 
 Power (v, n) > assert false 
417 
 Var v > 
418 
if is_memory m v then 
419 
if Types.is_array_type v.var_type 
420 
then assert false 
421 
else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) 
422 

423 
else 
424 
horn_var_to_expr 
425 
(rename_machine 
426 
self 
427 
v) 
428 
 Fun (n, vl) > horn_basic_app n (horn_val_to_expr m self) vl 
429  
430 
let no_reset_to_exprs machines m i = 
431 
let (n,_) = List.assoc i m.minstances in 
432 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 
433  
434 
let m_list = 
435 
rename_machine_list 
436 
(concat m.mname.node_id i) 
437 
(rename_mid_list (full_memory_vars machines target_machine)) 
438 
in 
439 
let c_list = 
440 
rename_machine_list 
441 
(concat m.mname.node_id i) 
442 
(rename_current_list (full_memory_vars machines target_machine)) 
443 
in 
444 
match c_list, m_list with 
445 
 [chd], [mhd] > 
446 
let expr = 
447 
Z3.Boolean.mk_eq !ctx 
448 
(horn_var_to_expr mhd) 
449 
(horn_var_to_expr chd) 
450 
in 
451 
[expr] 
452 
 _ > ( 
453 
let exprs = 
454 
List.map2 (fun mhd chd > 
455 
Z3.Boolean.mk_eq !ctx 
456 
(horn_var_to_expr mhd) 
457 
(horn_var_to_expr chd) 
458 
) 
459 
m_list 
460 
c_list 
461 
in 
462 
exprs 
463 
) 
464  
465 
let instance_reset_to_exprs machines m i = 
466 
let (n,_) = List.assoc i m.minstances in 
467 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 
468 
let vars = 
469 
(rename_machine_list 
470 
(concat m.mname.node_id i) 
471 
(rename_current_list (full_memory_vars machines target_machine))@ (rename_mid_list (full_memory_vars machines target_machine)) 
472 
) 
473 

474 
in 
475 
let expr = 
476 
Z3.Expr.mk_app 
477 
!ctx 
478 
(get_fdecl (machine_reset_name (Corelang.node_name n))) 
479 
(List.map (horn_var_to_expr) (idx::uid::vars)) 
480 
in 
481 
[expr] 
482  
483 
let instance_call_to_exprs machines reset_instances m i inputs outputs = 
484 
let self = m.mname.node_id in 
485  
486 
(* Building call args *) 
487 
let idx_uid_inout = 
488 
(* Additional input to register step counters, and uid *) 
489 
let idx = horn_var_to_expr idx in 
490 
let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in 
491 
let inout = 
492 
List.map (horn_val_to_expr m self) 
493 
(inputs @ (List.map (fun v > mk_val (Var v) v.var_type) outputs)) 
494 
in 
495 
idx::uid::inout 
496 
in 
497 

498 
try (* stateful node instance *) 
499 
begin 
500 
let (n,_) = List.assoc i m.minstances in 
501 
let target_machine = List.find (fun m > m.mname.node_id = Corelang.node_name n) machines in 
502  
503 
(* Checking whether this specific instances has been reset yet *) 
504 
let reset_exprs = 
505 
if not (List.mem i reset_instances) then 
506 
(* If not, declare mem_m = mem_c *) 
507 
no_reset_to_exprs machines m i 
508 
else 
509 
[] (* Nothing to add yet *) 
510 
in 
511 

512 
let mems = full_memory_vars machines target_machine in 
513 
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in 
514 
let mid_mems = rename_mems rename_mid_list in 
515 
let next_mems = rename_mems rename_next_list in 
516  
517 
let call_expr = 
518 
match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with 
519 
 "_arrow", [i1; i2], [o], [mem_m], [mem_x] > begin 
520 
let stmt1 = (* out = ite mem_m then i1 else i2 *) 
521 
Z3.Boolean.mk_eq !ctx 
522 
( (* output var *) 
523 
horn_val_to_expr 
524 
~is_lhs:true 
525 
m self 
526 
(mk_val (Var o) o.var_type) 
527 
) 
528 
( 
529 
Z3.Boolean.mk_ite !ctx 
530 
(horn_var_to_expr mem_m) 
531 
(horn_val_to_expr m self i1) 
532 
(horn_val_to_expr m self i2) 
533 
) 
534 
in 
535 
let stmt2 = (* mem_X = false *) 
536 
Z3.Boolean.mk_eq !ctx 
537 
(horn_var_to_expr mem_x) 
538 
(Z3.Boolean.mk_false !ctx) 
539 
in 
540 
[stmt1; stmt2] 
541 
end 
542  
543 
 node_name_n > 
544 
let expr = 
545 
Z3.Expr.mk_app 
546 
!ctx 
547 
(get_fdecl (machine_step_name (node_name n))) 
548 
( (* Arguments are input, output, mid_mems, next_mems *) 
549 
idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems) 
550 

551 
) 
552 
in 
553 
[expr] 
554 
in 
555  
556 
reset_exprs@call_expr 
557 
end 
558 
with Not_found > ( (* stateless node instance *) 
559 
let (n,_) = List.assoc i m.mcalls in 
560 
let expr = 
561 
Z3.Expr.mk_app 
562 
!ctx 
563 
(get_fdecl (machine_stateless_name (node_name n))) 
564 
idx_uid_inout (* Arguments are inputs, outputs *) 
565 
in 
566 
[expr] 
567 
) 
568  
569  
570 

571 
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *) 
572 
(* let rec value_suffix_to_expr self value = *) 
573 
(* match value.value_desc with *) 
574 
(*  Fun (n, vl) > *) 
575 
(* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *) 
576 

577 
(*  _ > *) 
578 
(* horn_val_to_expr self value *) 
579  
580  
581 
(* type_directed assignment: array vs. statically sized type 
582 
 [var_type]: type of variable to be assigned 
583 
 [var_name]: name of variable to be assigned 
584 
 [value]: assigned value 
585 
 [pp_var]: printer for variables 
586 
*) 
587 
let assign_to_exprs m var_name value = 
588 
let self = m.mname.node_id in 
589 
let e = 
590 
Z3.Boolean.mk_eq 
591 
!ctx 
592 
(horn_val_to_expr ~is_lhs:true m self var_name) 
593 
(horn_val_to_expr m self value) 
594 
(* was: TODO deal with array accesses (value_suffix_to_expr self value) *) 
595 
in 
596 
[e] 
597  
598 

599 
(* Convert instruction to Z3.Expr and update the set of reset instances *) 
600 
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list = 
601 
match Corelang.get_instr_desc instr with 
602 
 MComment _ > [], reset_instances 
603 
 MNoReset i > (* we assign middle_mem with mem_m. And declare i as reset *) 
604 
no_reset_to_exprs machines m i, 
605 
i::reset_instances 
606 
 MReset i > (* we assign middle_mem with reset: reset(mem_m) *) 
607 
instance_reset_to_exprs machines m i, 
608 
i::reset_instances 
609 
 MLocalAssign (i,v) > 
610 
assign_to_exprs 
611 
m 
612 
(mk_val (Var i) i.var_type) v, 
613 
reset_instances 
614 
 MStateAssign (i,v) > 
615 
assign_to_exprs 
616 
m 
617 
(mk_val (Var i) i.var_type) v, 
618 
reset_instances 
619 
 MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl) > 
620 
assert false (* This should not happen anymore *) 
621 
 MStep (il, i, vl) > 
622 
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = 
623 
mem_c and print the call to mem_m *) 
624 
instance_call_to_exprs machines reset_instances m i vl il, 
625 
reset_instances (* Since this instance call will only happen once, we 
626 
don't have to update reset_instances *) 
627  
628 
 MBranch (g,hl) > (* (g = tag1 => expr1) and (g = tag2 => expr2) ... 
629 
should not be produced yet. Later, we will have to 
630 
compare the reset_instances of each branch and 
631 
introduced the mem_m = mem_c for branches to do not 
632 
address it while other did. Am I clear ? *) 
633 
(* For each branch we obtain the logical encoding, and the information 
634 
whether a sub node has been reset or not. If a node has been reset in one 
635 
of the branch, then all others have to have the mem_m = mem_c 
636 
statement. *) 
637 
let self = m.mname.node_id in 
638 
let branch_to_expr (tag, instrs) = 
639 
let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in 
640 
let e = 
641 
Z3.Boolean.mk_implies !ctx 
642 
(Z3.Boolean.mk_eq !ctx 
643 
(horn_val_to_expr m self g) 
644 
(horn_tag_to_expr tag)) 
645 
branch_def in 
646  
647 
[e], branch_resets 
648 

649 
in 
650 
List.fold_left (fun (instrs, resets) b > 
651 
let b_instrs, b_resets = branch_to_expr b in 
652 
instrs@b_instrs, resets@b_resets 
653 
) ([], reset_instances) hl 
654 
 MSpec _ > assert false 
655  
656 
and instrs_to_expr machines reset_instances m instrs = 
657 
let instr_to_exprs rs i = instr_to_exprs machines rs m i in 
658 
let e_list, rs = 
659 
match instrs with 
660 
 [x] > instr_to_exprs reset_instances x 
661 
 _::_ > (* 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 *) 
662 

663 
List.fold_left (fun (exprs, rs) i > 
664 
let exprs_i, rs_i = instr_to_exprs rs i in 
665 
exprs@exprs_i, rs@rs_i 
666 
) 
667 
([], reset_instances) instrs 
668 

669 

670 
 [] > [], reset_instances 
671 
in 
672 
let e = 
673 
match e_list with 
674 
 [e] > e 
675 
 [] > Z3.Boolean.mk_true !ctx 
676 
 _ > Z3.Boolean.mk_and !ctx e_list 
677 
in 
678 
e, rs 
679  
680  
681 
(*********************************************************) 
682  
683 
(* Quantifiying universally all occuring variables *) 
684 
let add_rule ?(dont_touch=[]) vars expr = 
685 
(* let fds = Z3.Expr.get_args expr in *) 
686 
(* Format.eprintf "Expr %s: args: [%a]@." *) 
687 
(* (Z3.Expr.to_string expr) *) 
688 
(* (Utils.fprintf_list ~sep:", " (fun fmt e > Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *) 
689  
690 
(* (\* Old code relying on provided vars *\) *) 
691 
(* let sorts = (List.map (fun id > type_to_sort id.var_type) vars) in *) 
692 
(* let symbols = (List.map (fun id > Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *) 
693 

694 
(* New code: we extract vars from expr *) 
695 
let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl 
696 
let compare = compare 
697 
let hash = Hashtbl.hash 
698 
end) 
699 
in 
700 
(* Fonction seems unused 
701  
702 
let rec get_expr_vars e = 
703 
let open Utils in 
704 
let nb_args = Z3.Expr.get_num_args e in 
705 
if nb_args <= 0 then ( 
706 
let fdecl = Z3.Expr.get_func_decl e in 
707 
(* let params = Z3.FuncDecl.get_parameters fdecl in *) 
708 
(* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *) 
709 
let dkind = Z3.FuncDecl.get_decl_kind fdecl in 
710 
match dkind with Z3enums.OP_UNINTERPRETED > ( 
711 
(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE > "true"  Z3enums.OP_UNINTERPRETED > "uninter"); *) 
712 
(* let open Z3.FuncDecl.Parameter in *) 
713 
(* List.iter (fun p > *) 
714 
(* match p with *) 
715 
(* P_Int i > Format.eprintf "int %i" i *) 
716 
(*  P_Dbl f > Format.eprintf "dbl %f" f *) 
717 
(*  P_Sym s > Format.eprintf "symb" *) 
718 
(*  P_Srt s > Format.eprintf "sort" *) 
719 
(*  P_Ast _ >Format.eprintf "ast" *) 
720 
(*  P_Fdl f > Format.eprintf "fundecl" *) 
721 
(*  P_Rat s > Format.eprintf "rat %s" s *) 
722 

723 
(* ) params; *) 
724 
(* Format.eprintf "]@."; *) 
725 
FDSet.singleton fdecl 
726 
) 
727 
 _ > FDSet.empty 
728 
) 
729 
else (*if nb_args > 0 then*) 
730 
List.fold_left 
731 
(fun accu e > FDSet.union accu (get_expr_vars e)) 
732 
FDSet.empty (Z3.Expr.get_args e) 
733 
in 
734 
*) 
735 
(* Unsed variable. Coul;d be reintroduced 
736 
let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in 
737 
let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in 
738 
let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in 
739 
*) 
740 
if !debug then ( 
741 
Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @." 
742 
(Z3.Expr.to_string expr) 
743 
(Utils.fprintf_list ~sep:",@ " (fun fmt e > Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) 
744 
) 
745 
; 
746 
let expr = Z3.Quantifier.mk_forall_const 
747 
!ctx (* context *) 
748 
(List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *) 
749 
(* sorts (\* sort list*\) *) 
750 
(* symbols (\* symbol list *\) *) 
751 
expr (* expression *) 
752 
None (* quantifier weight, None means 1 *) 
753 
[] (* pattern list ? *) 
754 
[] (* ? *) 
755 
None (* ? *) 
756 
None (* ? *) 
757 
in 
758 
(* Format.eprintf "OK@.@?"; *) 
759  
760 
(* 
761 
TODO: bizarre la declaration de INIT tout seul semble poser pb. 
762 
*) 
763 
Z3.Fixedpoint.add_rule !fp 
764 
(Z3.Quantifier.expr_of_quantifier expr) 
765 
None 
766  
767 

768 
(********************************************************) 
769 

770 
let machine_reset machines m = 
771 
let locals = local_memory_vars machines m in 
772 

773 
(* print "x_m = x_c" for each local memory *) 
774 
let mid_mem_def = 
775 
List.map (fun v > 
776 
Z3.Boolean.mk_eq !ctx 
777 
(horn_var_to_expr (rename_mid v)) 
778 
(horn_var_to_expr (rename_current v)) 
779 
) locals 
780 
in 
781  
782 
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. 
783 
Special treatment for _arrow: _first = true 
784 
*) 
785  
786 
let reset_instances = 
787 

788 
List.map (fun (id, (n, _)) > 
789 
let name = node_name n in 
790 
if name = "_arrow" then ( 
791 
Z3.Boolean.mk_eq !ctx 
792 
( 
793 
let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in 
794 
Z3.Expr.mk_const_f !ctx vdecl 
795 
) 
796 
(Z3.Boolean.mk_true !ctx) 
797 

798 
) else ( 
799 
let machine_n = get_machine machines name in 
800 

801 
Z3.Expr.mk_app 
802 
!ctx 
803 
(get_fdecl (name ^ "_reset")) 
804 
(List.map (horn_var_to_expr) 
805 
(idx::uid:: (* Additional vars: counters, uid *) 
806 
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) 
807 
)) 
808 

809 
) 
810 
) m.minstances 
811 

812 

813 
in 
814 

815 
Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances) 
816 

817 

818  
819 
(* TODO: empty list means true statement *) 
820 
let decl_machine machines m = 
821 
if m.mname.node_id = Arrow.arrow_id then 
822 
(* We don't do arrow function *) 
823 
() 
824 
else 
825 
begin 
826 
let _ = 
827 
List.map decl_var 
828 
( 
829 
(inout_vars machines m)@ 
830 
(rename_current_list (full_memory_vars machines m)) @ 
831 
(rename_mid_list (full_memory_vars machines m)) @ 
832 
(rename_next_list (full_memory_vars machines m)) @ 
833 
(rename_machine_list m.mname.node_id m.mstep.step_locals) 
834 
) 
835 
in 
836 
if is_stateless m then 
837 
begin 
838 
if !debug then 
839 
Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id; 
840  
841 
(* Declaring single predicate *) 
842 
let vars = inout_vars machines m in 
843 
let vars_types = List.map (fun v > type_to_sort v.var_type) vars in 
844 
let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in 
845 

846 
let horn_body, _ (* don't care for reset here *) = 
847 
instrs_to_expr 
848 
machines 
849 
([] (* No reset info for stateless nodes *) ) 
850 
m 
851 
m.mstep.step_instrs 
852 
in 
853 
let horn_head = 
854 
Z3.Expr.mk_app 
855 
!ctx 
856 
(get_fdecl (machine_stateless_name m.mname.node_id)) 
857 
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) 
858 
in 
859 
(* this line seems useless *) 
860 
let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in 
861 
(* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *) 
862 
match m.mstep.step_asserts with 
863 
 [] > 
864 
begin 
865 
(* Rule for single predicate : "; Stateless step rule @." *) 
866 
(*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*) 
867 
(* TODO clean code *) 
868 
(* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *) 
869 
add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head) 
870 

871 
end 
872 
 assertsl > 
873 
begin 
874 
(*Rule for step "; Stateless step rule with Assertions @.";*) 
875 
let body_with_asserts = 
876 
Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) 
877 
in 
878 
let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in 
879 
add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head) 
880 
end 
881 
end 
882 
else 
883 
begin 
884  
885 
(* Rule for reset *) 
886  
887 
let vars = reset_vars machines m in 
888 
let vars_types = List.map (fun v > type_to_sort v.var_type) vars in 
889 
let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in 
890 
let horn_reset_body = machine_reset machines m in 
891 
let horn_reset_head = 
892 
Z3.Expr.mk_app 
893 
!ctx 
894 
(get_fdecl (machine_reset_name m.mname.node_id)) 
895 
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) 
896 
in 
897  
898 

899 
let _ = 
900 
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head) 
901 

902 
in 
903  
904 
(* Rule for step*) 
905 
let vars = step_vars machines m in 
906 
let vars_types = List.map (fun v > type_to_sort v.var_type) vars in 
907 
let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in 
908 
let horn_step_body, _ (* don't care for reset here *) = 
909 
instrs_to_expr 
910 
machines 
911 
[] 
912 
m 
913 
m.mstep.step_instrs 
914 
in 
915 
let horn_step_head = 
916 
Z3.Expr.mk_app 
917 
!ctx 
918 
(get_fdecl (machine_step_name m.mname.node_id)) 
919 
( List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars)) 
920 
in 
921 
match m.mstep.step_asserts with 
922 
 [] > 
923 
begin 
924 
(* Rule for single predicate *) 
925 
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in 
926 
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head) 
927 

928 
end 
929 
 assertsl > 
930 
begin 
931 
(* Rule for step Assertions @.; *) 
932 
let body_with_asserts = 
933 
Z3.Boolean.mk_and !ctx 
934 
(horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl) 
935 
in 
936 
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in 
937 
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head) 
938 

939 
end 
940 

941 
end 
942 
end 
943  
944  
945  
946 
(* Debug functions *) 
947 
(* 
948 
let rec extract_expr_fds e = 
949 
(* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *) 
950 
(* (Z3.Expr.to_string e); *) 
951 

952 
(* Removing quantifier is there are some *) 
953 
let e = (* I didn't found a nicer way to do it than with an exception. My 
954 
bad *) 
955 
try 
956 
let eq = Z3.Quantifier.quantifier_of_expr e in 
957 
let e2 = Z3.Quantifier.get_body eq in 
958 
(* Format.eprintf "Extracted quantifier body@ "; *) 
959 
e2 
960 

961 
with _ > Format.eprintf "No quantifier info@ "; e 
962 
in 
963 
let _ = 
964 
try 
965 
( 
966 
let fd = Z3.Expr.get_func_decl e in 
967 
let fd_symbol = Z3.FuncDecl.get_name fd in 
968 
let fd_name = Z3.Symbol.to_string fd_symbol in 
969 
if not (Hashtbl.mem decls fd_name) then 
970 
register_fdecl fd_name fd; 
971 
(* Format.eprintf "fdecls (%s): %s@ " *) 
972 
(* fd_name *) 
973 
(* (Z3.FuncDecl.to_string fd); *) 
974 
try 
975 
( 
976 
let args = Z3.Expr.get_args e in 
977 
(* Format.eprintf "@[<v>@ "; *) 
978 
(* List.iter extract_expr_fds args; *) 
979 
(* Format.eprintf "@]@ "; *) 
980 
() 
981 
) 
982 
with _ > 
983 
Format.eprintf "Impossible to extract fundecl args for expression %s@ " 
984 
(Z3.Expr.to_string e) 
985 
) 
986 
with _ > 
987 
Format.eprintf "Impossible to extract anything from expression %s@ " 
988 
(Z3.Expr.to_string e) 
989 
in 
990 
(* Format.eprintf "@]@ " *) 
991 
() 
992 
*) 
993 
(* Local Variables: *) 
994 
(* compilecommand:"make C ../.." *) 
995 
(* End: *) 