lustrec / src / tools / zustre_verifier.ml @ 46cb4020
History  View  Annotate  Download (25.8 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  
8 
module HBC = Horn_backend_common 
9 
let machine_step_name = HBC.machine_step_name 
10 
let node_name = HBC.node_name 
11 
let concat = HBC.concat 
12 
let rename_machine = HBC.rename_machine 
13 
let rename_machine_list = HBC.rename_machine_list 
14 
let rename_next = HBC.rename_next 
15 
let rename_current = HBC.rename_current 
16 
let rename_current_list = HBC.rename_current_list 
17 
let rename_mid_list = HBC.rename_mid_list 
18 
let rename_next_list = HBC.rename_next_list 
19 
let full_memory_vars = HBC.full_memory_vars 
20 
let inout_vars = HBC.inout_vars 
21 
let reset_vars = HBC.reset_vars 
22 
let step_vars = HBC.step_vars 
23 
let local_memory_vars = HBC.local_memory_vars 
24 

25 
let machine_reset_name = HBC.machine_reset_name 
26 
let machine_stateless_name = HBC.machine_stateless_name 
27  
28 
let rename_mid = HBC.rename_mid 
29  
30 
let preprocess = Horn_backend.preprocess 
31 

32 
let active = ref false 
33 
let ctx = ref (Z3.mk_context []) 
34 
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx) 
35  
36 
(** Sorts 
37  
38 
A sort is introduced for each basic type and each enumerated type. 
39  
40 
A hashtbl records these and allow easy access to sort values, when 
41 
provided with a enumerated type name. 
42  
43 
*) 
44 

45 
let bool_sort = Z3.Boolean.mk_sort !ctx 
46 
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx 
47 
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx 
48  
49 
let const_sorts = Hashtbl.create 13 
50 
let const_tags = Hashtbl.create 13 
51 
let sort_elems = Hashtbl.create 13 
52  
53 
let get_const_sort = Hashtbl.find const_sorts 
54 
let get_sort_elems = Hashtbl.find sort_elems 
55 
let get_tag_sort = Hashtbl.find const_tags 
56 

57  
58 

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

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

79 
let rec type_to_sort t = 
80 
if Types.is_bool_type t then bool_sort else 
81 
if Types.is_int_type t then int_sort else 
82 
if Types.is_real_type t then real_sort else 
83 
match (Types.repr t).Types.tdesc with 
84 
 Types.Tconst ty > get_const_sort ty 
85 
 Types.Tclock t > type_to_sort t 
86 
 Types.Tarray(dim,ty) > Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty) 
87 
 Types.Tstatic(d, ty)> type_to_sort ty 
88 
 Types.Tarrow _ 
89 
 _ > Format.eprintf "internal error: pp_type %a@." 
90 
Types.print_ty t; assert false 
91  
92 
(** Func decls 
93  
94 
Similarly fun_decls are registerd, by their name, into a hashtbl. The 
95 
proposed encoding introduces a 0ary fun_decl to model variables 
96 
and fun_decl with arguments to declare reset and step predicates. 
97  
98  
99  
100 
*) 
101 
let decls = Hashtbl.create 13 
102 
let register_fdecl id fd = Hashtbl.add decls id fd 
103 
let get_fdecl id = Hashtbl.find decls id 
104 

105 
let decl_var id = 
106 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in 
107 
register_fdecl id.var_id fdecl; 
108 
fdecl 
109  
110 
let decl_rel name args = 
111 
(*verifier ce qui est construit. On veut un declarerel *) 
112 
let args_sorts = List.map (fun v > type_to_sort v.var_type) args in 
113 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in 
114 
register_fdecl name fdecl; 
115 
fdecl 
116 

117  
118  
119 
(** Conversion functions 
120  
121 
The following is similar to the Horn backend. Each printing function 
122 
is rephrased from pp_xx to xx_to_expr and produces a Z3 value. 
123  
124 
*) 
125  
126  
127 
(* Returns the f_decl associated to the variable v *) 
128 
let horn_var_to_expr v = 
129 
Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id) 
130  
131  
132  
133  
134 
(* Used to print boolean constants *) 
135 
let horn_tag_to_expr t = 
136 
if t = Corelang.tag_true then 
137 
Z3.Boolean.mk_true !ctx 
138 
else if t = Corelang.tag_false then 
139 
Z3.Boolean.mk_false !ctx 
140 
else 
141 
(* Finding the associated sort *) 
142 
let sort = get_tag_sort t in 
143 
let elems = get_sort_elems sort in 
144 
let res : Z3.Expr.expr option = 
145 
List.fold_left2 (fun res cst expr > 
146 
match res with 
147 
 Some _ > res 
148 
 None > if t = cst then Some (expr:Z3.Expr.expr) else None 
149 
) None elems (Z3.Enumeration.get_consts sort) 
150 
in 
151 
match res with None > assert false  Some s > s 
152 

153 
(* Prints a constant value *) 
154 
let rec horn_const_to_expr c = 
155 
match c with 
156 
 Const_int i > Z3.Arithmetic.Integer.mk_numeral_i !ctx i 
157 
 Const_real (_,_,s) > Z3.Arithmetic.Real.mk_numeral_i !ctx 0 
158 
 Const_tag t > horn_tag_to_expr t 
159 
 _ > assert false 
160  
161  
162  
163 
(* Default value for each type, used when building arrays. Eg integer array 
164 
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value 
165 
for the type integer (arrays). 
166 
*) 
167 
let rec horn_default_val t = 
168 
let t = Types.dynamic_type t in 
169 
if Types.is_bool_type t then Z3.Boolean.mk_true !ctx else 
170 
if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
171 
if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
172 
(* match (Types.dynamic_type t).Types.tdesc with 
173 
*  Types.Tarray(dim, l) > (\* TODO PL: this strange code has to be (heavily) checked *\) 
174 
* let valt = Types.array_element_type t in 
175 
* fprintf fmt "((as const (Array Int %a)) %a)" 
176 
* pp_type valt 
177 
* pp_default_val valt 
178 
*  Types.Tstruct(l) > assert false 
179 
*  Types.Ttuple(l) > assert false 
180 
* _ > *) assert false 
181  
182 
(* Conversion of basic library functions *) 
183 

184 
let horn_basic_app i val_to_expr vl = 
185 
match i, vl with 
186 
 "ite", [v1; v2; v3] > 
187 
Z3.Boolean.mk_ite 
188 
!ctx 
189 
(val_to_expr v1) 
190 
(val_to_expr v2) 
191 
(val_to_expr v3) 
192  
193 
 "uminus", [v] > 
194 
Z3.Arithmetic.mk_unary_minus 
195 
!ctx 
196 
(val_to_expr v) 
197 
 "not", [v] > 
198 
Z3.Boolean.mk_not 
199 
!ctx 
200 
(val_to_expr v) 
201 
 "=", [v1; v2] > 
202 
Z3.Boolean.mk_eq 
203 
!ctx 
204 
(val_to_expr v1) 
205 
(val_to_expr v2) 
206 
 "&&", [v1; v2] > 
207 
Z3.Boolean.mk_and 
208 
!ctx 
209 
[val_to_expr v1; 
210 
val_to_expr v2] 
211 
 "", [v1; v2] > 
212 
Z3.Boolean.mk_or 
213 
!ctx 
214 
[val_to_expr v1; 
215 
val_to_expr v2] 
216  
217 
 "impl", [v1; v2] > 
218 
Z3.Boolean.mk_implies 
219 
!ctx 
220 
(val_to_expr v1) 
221 
(val_to_expr v2) 
222 
 "mod", [v1; v2] > 
223 
Z3.Arithmetic.Integer.mk_mod 
224 
!ctx 
225 
(val_to_expr v1) 
226 
(val_to_expr v2) 
227 
 "equi", [v1; v2] > 
228 
Z3.Boolean.mk_eq 
229 
!ctx 
230 
(val_to_expr v1) 
231 
(val_to_expr v2) 
232 
 "xor", [v1; v2] > 
233 
Z3.Boolean.mk_xor 
234 
!ctx 
235 
(val_to_expr v1) 
236 
(val_to_expr v2) 
237 
 "!=", [v1; v2] > 
238 
Z3.Boolean.mk_not 
239 
!ctx 
240 
( 
241 
Z3.Boolean.mk_eq 
242 
!ctx 
243 
(val_to_expr v1) 
244 
(val_to_expr v2) 
245 
) 
246 
 "/", [v1; v2] > 
247 
Z3.Arithmetic.mk_div 
248 
!ctx 
249 
(val_to_expr v1) 
250 
(val_to_expr v2) 
251  
252 
 "+", [v1; v2] > 
253 
Z3.Arithmetic.mk_add 
254 
!ctx 
255 
[val_to_expr v1; val_to_expr v2] 
256  
257 
 "", [v1; v2] > 
258 
Z3.Arithmetic.mk_sub 
259 
!ctx 
260 
[val_to_expr v1 ; val_to_expr v2] 
261 

262 
 "*", [v1; v2] > 
263 
Z3.Arithmetic.mk_mul 
264 
!ctx 
265 
[val_to_expr v1; val_to_expr v2] 
266  
267  
268 
 "<", [v1; v2] > 
269 
Z3.Arithmetic.mk_lt 
270 
!ctx 
271 
(val_to_expr v1) 
272 
(val_to_expr v2) 
273  
274 
 "<=", [v1; v2] > 
275 
Z3.Arithmetic.mk_le 
276 
!ctx 
277 
(val_to_expr v1) 
278 
(val_to_expr v2) 
279  
280 
 ">", [v1; v2] > 
281 
Z3.Arithmetic.mk_gt 
282 
!ctx 
283 
(val_to_expr v1) 
284 
(val_to_expr v2) 
285  
286 
 ">=", [v1; v2] > 
287 
Z3.Arithmetic.mk_ge 
288 
!ctx 
289 
(val_to_expr v1) 
290 
(val_to_expr v2) 
291  
292 

293 
(*  _, [v1; v2] > Z3.Boolean.mk_and 
294 
* !ctx 
295 
* (val_to_expr v1) 
296 
* (val_to_expr v2) 
297 
* 
298 
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) 
299 
 _ > ( 
300 
Format.eprintf 
301 
"internal error: zustre unkown function %s@." i; 
302 
assert false) 
303  
304 

305 
(* Convert a value expression [v], with internal function calls only. 
306 
[pp_var] is a printer for variables (typically [pp_c_var_read]), 
307 
but an offset suffix may be added for array variables 
308 
*) 
309 
let rec horn_val_to_expr ?(is_lhs=false) self v = 
310 
match v.value_desc with 
311 
 Cst c > horn_const_to_expr c 
312  
313 
(* Code specific for arrays *) 
314 
 Array il > 
315 
(* An array definition: 
316 
(store ( 
317 
... 
318 
(store ( 
319 
store ( 
320 
default_val 
321 
) 
322 
idx_n val_n 
323 
) 
324 
idx_n1 val_n1) 
325 
... 
326 
idx_1 val_1 
327 
) *) 
328 
let rec build_array (tab, x) = 
329 
match tab with 
330 
 [] > horn_default_val v.value_type(* (get_type v) *) 
331 
 h::t > 
332 
Z3.Z3Array.mk_store 
333 
!ctx 
334 
(build_array (t, (x+1))) 
335 
(Z3.Arithmetic.Integer.mk_numeral_i !ctx x) 
336 
(horn_val_to_expr ~is_lhs:is_lhs self h) 
337 
in 
338 
build_array (il, 0) 
339 

340 
 Access(tab,index) > 
341 
Z3.Z3Array.mk_select !ctx 
342 
(horn_val_to_expr ~is_lhs:is_lhs self tab) 
343 
(horn_val_to_expr ~is_lhs:is_lhs self index) 
344  
345 
(* Code specific for arrays *) 
346 

347 
 Power (v, n) > assert false 
348 
 LocalVar v > 
349 
horn_var_to_expr 
350 
(rename_machine 
351 
self 
352 
v) 
353 
 StateVar v > 
354 
if Types.is_array_type v.var_type 
355 
then assert false 
356 
else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) 
357 
 Fun (n, vl) > horn_basic_app n (horn_val_to_expr self) vl 
358  
359 
let no_reset_to_exprs machines m i = 
360 
let (n,_) = List.assoc i m.minstances in 
361 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 
362  
363 
let m_list = 
364 
rename_machine_list 
365 
(concat m.mname.node_id i) 
366 
(rename_mid_list (full_memory_vars machines target_machine)) 
367 
in 
368 
let c_list = 
369 
rename_machine_list 
370 
(concat m.mname.node_id i) 
371 
(rename_current_list (full_memory_vars machines target_machine)) 
372 
in 
373 
match c_list, m_list with 
374 
 [chd], [mhd] > 
375 
let expr = 
376 
Z3.Boolean.mk_eq !ctx 
377 
(horn_var_to_expr mhd) 
378 
(horn_var_to_expr chd) 
379 
in 
380 
[expr] 
381 
 _ > ( 
382 
let exprs = 
383 
List.map2 (fun mhd chd > 
384 
Z3.Boolean.mk_eq !ctx 
385 
(horn_var_to_expr mhd) 
386 
(horn_var_to_expr chd) 
387 
) 
388 
m_list 
389 
c_list 
390 
in 
391 
exprs 
392 
) 
393  
394 
let instance_reset_to_exprs machines m i = 
395 
let (n,_) = List.assoc i m.minstances in 
396 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 
397 
let vars = 
398 
( 
399 
(rename_machine_list 
400 
(concat m.mname.node_id i) 
401 
(rename_current_list (full_memory_vars machines target_machine)) 
402 
) 
403 
@ 
404 
(rename_machine_list 
405 
(concat m.mname.node_id i) 
406 
(rename_mid_list (full_memory_vars machines target_machine)) 
407 
) 
408 
) 
409 
in 
410 
let expr = 
411 
Z3.Expr.mk_app 
412 
!ctx 
413 
(get_fdecl (machine_reset_name (Corelang.node_name n))) 
414 
(List.map (horn_var_to_expr) vars) 
415 
in 
416 
[expr] 
417  
418 
let instance_call_to_exprs machines reset_instances m i inputs outputs = 
419 
let self = m.mname.node_id in 
420 
try (* stateful node instance *) 
421 
begin 
422 
let (n,_) = List.assoc i m.minstances in 
423 
let target_machine = List.find (fun m > m.mname.node_id = Corelang.node_name n) machines in 
424  
425 
(* Checking whether this specific instances has been reset yet *) 
426 
let reset_exprs = 
427 
if not (List.mem i reset_instances) then 
428 
(* If not, declare mem_m = mem_c *) 
429 
no_reset_to_exprs machines m i 
430 
else 
431 
[] (* Nothing to add yet *) 
432 
in 
433 

434 
let mems = full_memory_vars machines target_machine in 
435 
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in 
436 
let mid_mems = rename_mems rename_mid_list in 
437 
let next_mems = rename_mems rename_next_list in 
438  
439 
let call_expr = 
440 
match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with 
441 
 "_arrow", [i1; i2], [o], [mem_m], [mem_x] > begin 
442 
let stmt1 = (* out = ite mem_m then i1 else i2 *) 
443 
Z3.Boolean.mk_eq !ctx 
444 
( (* output var *) 
445 
horn_val_to_expr 
446 
~is_lhs:true 
447 
self 
448 
(mk_val (LocalVar o) o.var_type) 
449 
) 
450 
( 
451 
Z3.Boolean.mk_ite !ctx 
452 
(horn_var_to_expr mem_m) 
453 
(horn_val_to_expr self i1) 
454 
(horn_val_to_expr self i2) 
455 
) 
456 
in 
457 
let stmt2 = (* mem_X = false *) 
458 
Z3.Boolean.mk_eq !ctx 
459 
(horn_var_to_expr mem_x) 
460 
(Z3.Boolean.mk_false !ctx) 
461 
in 
462 
[stmt1; stmt2] 
463 
end 
464  
465 
 node_name_n > 
466 
let expr = 
467 
Z3.Expr.mk_app 
468 
!ctx 
469 
(get_fdecl (machine_step_name (node_name n))) 
470 
( (* Arguments are input, output, mid_mems, next_mems *) 
471 
( 
472 
List.map (horn_val_to_expr self) ( 
473 
inputs @ 
474 
(List.map (fun v > mk_val (LocalVar v) v.var_type) outputs) 
475 
) 
476 
) @ ( 
477 
List.map (horn_var_to_expr) (mid_mems@next_mems) 
478 
) 
479 
) 
480 
in 
481 
[expr] 
482 
in 
483  
484 
reset_exprs@call_expr 
485 
end 
486 
with Not_found > ( (* stateless node instance *) 
487 
let (n,_) = List.assoc i m.mcalls in 
488 
let expr = 
489 
Z3.Expr.mk_app 
490 
!ctx 
491 
(get_fdecl (machine_stateless_name (node_name n))) 
492 
((* Arguments are inputs, outputs *) 
493 
List.map (horn_val_to_expr self) 
494 
( 
495 
inputs @ (List.map (fun v > mk_val (LocalVar v) v.var_type) outputs) 
496 
) 
497 
) 
498 
in 
499 
[expr] 
500 
) 
501  
502  
503 

504 
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *) 
505 
(* let rec value_suffix_to_expr self value = *) 
506 
(* match value.value_desc with *) 
507 
(*  Fun (n, vl) > *) 
508 
(* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *) 
509 

510 
(*  _ > *) 
511 
(* horn_val_to_expr self value *) 
512  
513  
514 
(* type_directed assignment: array vs. statically sized type 
515 
 [var_type]: type of variable to be assigned 
516 
 [var_name]: name of variable to be assigned 
517 
 [value]: assigned value 
518 
 [pp_var]: printer for variables 
519 
*) 
520 
let assign_to_exprs m var_name value = 
521 
let self = m.mname.node_id in 
522 
let e = 
523 
Z3.Boolean.mk_eq 
524 
!ctx 
525 
(horn_val_to_expr ~is_lhs:true self var_name) 
526 
(horn_val_to_expr self value) 
527 
(* was: TODO deal with array accesses (value_suffix_to_expr self value) *) 
528 
in 
529 
[e] 
530  
531 

532 
(* Convert instruction to Z3.Expr and update the set of reset instances *) 
533 
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list = 
534 
match Corelang.get_instr_desc instr with 
535 
 MComment _ > [], reset_instances 
536 
 MNoReset i > (* we assign middle_mem with mem_m. And declare i as reset *) 
537 
no_reset_to_exprs machines m i, 
538 
i::reset_instances 
539 
 MReset i > (* we assign middle_mem with reset: reset(mem_m) *) 
540 
instance_reset_to_exprs machines m i, 
541 
i::reset_instances 
542 
 MLocalAssign (i,v) > 
543 
assign_to_exprs 
544 
m 
545 
(mk_val (LocalVar i) i.var_type) v, 
546 
reset_instances 
547 
 MStateAssign (i,v) > 
548 
assign_to_exprs 
549 
m 
550 
(mk_val (StateVar i) i.var_type) v, 
551 
reset_instances 
552 
 MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl) > 
553 
assert false (* This should not happen anymore *) 
554 
 MStep (il, i, vl) > 
555 
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = 
556 
mem_c and print the call to mem_m *) 
557 
instance_call_to_exprs machines reset_instances m i vl il, 
558 
reset_instances (* Since this instance call will only happen once, we 
559 
don't have to update reset_instances *) 
560  
561 
 MBranch (g,hl) > (* (g = tag1 => expr1) and (g = tag2 => expr2) ... 
562 
should not be produced yet. Later, we will have to 
563 
compare the reset_instances of each branch and 
564 
introduced the mem_m = mem_c for branches to do not 
565 
address it while other did. Am I clear ? *) 
566 
(* For each branch we obtain the logical encoding, and the information 
567 
whether a sub node has been reset or not. If a node has been reset in one 
568 
of the branch, then all others have to have the mem_m = mem_c 
569 
statement. *) 
570 
let self = m.mname.node_id in 
571 
let branch_to_expr (tag, instrs) = 
572 
let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in 
573 
let e = 
574 
Z3.Boolean.mk_implies !ctx 
575 
(Z3.Boolean.mk_eq !ctx 
576 
(horn_val_to_expr self g) 
577 
(horn_tag_to_expr tag)) 
578 
branch_def in 
579  
580 
[e], branch_resets 
581 

582 
in 
583 
List.fold_left (fun (instrs, resets) b > 
584 
let b_instrs, b_resets = branch_to_expr b in 
585 
instrs@b_instrs, resets@b_resets 
586 
) ([], reset_instances) hl 
587  
588 
and instrs_to_expr machines reset_instances m instrs = 
589 
let instr_to_exprs rs i = instr_to_exprs machines rs m i in 
590 
let e_list, rs = 
591 
match instrs with 
592 
 [x] > instr_to_exprs reset_instances x 
593 
 _::_ > (* 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 *) 
594 

595 
List.fold_left (fun (exprs, rs) i > 
596 
let exprs_i, rs_i = instr_to_exprs rs i in 
597 
exprs@exprs_i, rs@rs_i 
598 
) 
599 
([], reset_instances) instrs 
600 

601 

602 
 [] > [], reset_instances 
603 
in 
604 
let e = 
605 
match e_list with 
606 
 [e] > e 
607 
 [] > Z3.Boolean.mk_true !ctx 
608 
 _ > Z3.Boolean.mk_and !ctx e_list 
609 
in 
610 
e, rs 
611  
612 

613 
let machine_reset machines m = 
614 
let locals = local_memory_vars machines m in 
615 

616 
(* print "x_m = x_c" for each local memory *) 
617 
let mid_mem_def = 
618 
List.map (fun v > 
619 
Z3.Boolean.mk_eq !ctx 
620 
(horn_var_to_expr (rename_mid v)) 
621 
(horn_var_to_expr (rename_current v)) 
622 
) locals 
623 
in 
624  
625 
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. 
626 
Special treatment for _arrow: _first = true 
627 
*) 
628  
629 
let reset_instances = 
630 

631 
List.map (fun (id, (n, _)) > 
632 
let name = node_name n in 
633 
if name = "_arrow" then ( 
634 
Z3.Boolean.mk_eq !ctx 
635 
( 
636 
let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in 
637 
Z3.Expr.mk_const_f !ctx vdecl 
638 
) 
639 
(Z3.Boolean.mk_true !ctx) 
640 

641 
) else ( 
642 
let machine_n = get_machine machines name in 
643 

644 
Z3.Expr.mk_app 
645 
!ctx 
646 
(get_fdecl (name ^ "_reset")) 
647 
(List.map (horn_var_to_expr) 
648 
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) 
649 
) 
650 

651 
) 
652 
) m.minstances 
653 

654 

655 
in 
656 

657 
Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances) 
658 

659 

660  
661 
(* TODO: empty list means true statement *) 
662 
let decl_machine machines m = 
663 
if m.mname.node_id = Arrow.arrow_id then 
664 
(* We don't do arrow function *) 
665 
() 
666 
else 
667 
begin 
668 
let vars = 
669 
List.map decl_var 
670 
( 
671 
(inout_vars machines m)@ 
672 
(rename_current_list (full_memory_vars machines m)) @ 
673 
(rename_mid_list (full_memory_vars machines m)) @ 
674 
(rename_next_list (full_memory_vars machines m)) @ 
675 
(rename_machine_list m.mname.node_id m.mstep.step_locals) 
676 
) 
677 
in 
678 

679 
if is_stateless m then 
680 
begin 
681 
(* Declaring single predicate *) 
682 
let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in 
683 
let horn_body, _ (* don't care for reset here *) = 
684 
instrs_to_expr 
685 
machines 
686 
([] (* No reset info for stateless nodes *) ) 
687 
m 
688 
m.mstep.step_instrs 
689 
in 
690 
let horn_head = 
691 
Z3.Expr.mk_app 
692 
!ctx 
693 
(get_fdecl (machine_stateless_name m.mname.node_id)) 
694 
(List.map (horn_var_to_expr) (inout_vars machines m)) 
695 
in 
696 
match m.mstep.step_asserts with 
697 
 [] > 
698 
begin 
699 
(* Rule for single predicate : "; Stateless step rule @." *) 
700 
Z3.Fixedpoint.add_rule !fp 
701 
(Z3.Boolean.mk_implies !ctx horn_body horn_head) 
702 
None 
703 
end 
704 
 assertsl > 
705 
begin 
706 
(*Rule for step "; Stateless step rule with Assertions @.";*) 
707 
let body_with_asserts = 
708 
Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl) 
709 
in 
710 
Z3.Fixedpoint.add_rule !fp 
711 
(Z3.Boolean.mk_implies !ctx body_with_asserts horn_head) 
712 
None 
713 
end 
714 
end 
715 
else 
716 
begin 
717 
(* Declaring predicate *) 
718 
let _ = decl_rel (machine_reset_name m.mname.node_id) (reset_vars machines m) in 
719 
let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in 
720  
721 
(* Rule for reset *) 
722  
723 
let horn_reset_body = machine_reset machines m in 
724 
let horn_reset_head = 
725 
Z3.Expr.mk_app 
726 
!ctx 
727 
(get_fdecl (machine_reset_name m.mname.node_id)) 
728 
(List.map (horn_var_to_expr) (reset_vars machines m)) 
729 
in 
730 

731 
let _ = 
732 
Z3.Fixedpoint.add_rule !fp 
733 
(Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head) 
734 
None 
735 
in 
736  
737 
(* Rule for step*) 
738 
let horn_step_body, _ (* don't care for reset here *) = 
739 
instrs_to_expr 
740 
machines 
741 
[] 
742 
m 
743 
m.mstep.step_instrs 
744 
in 
745 
let horn_step_head = 
746 
Z3.Expr.mk_app 
747 
!ctx 
748 
(get_fdecl (machine_step_name m.mname.node_id)) 
749 
(List.map (horn_var_to_expr) (step_vars machines m)) 
750 
in 
751 
match m.mstep.step_asserts with 
752 
 [] > 
753 
begin 
754 
(* Rule for single predicate *) 
755 
Z3.Fixedpoint.add_rule !fp 
756 
(Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head) 
757 
None 
758 
end 
759 
 assertsl > 
760 
begin 
761 
(* Rule for step Assertions @.; *) 
762 
let body_with_asserts = 
763 
Z3.Boolean.mk_and !ctx 
764 
(horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl) 
765 
in 
766 
Z3.Fixedpoint.add_rule !fp 
767 
(Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head) 
768 
None 
769 
end 
770 

771 
end 
772 
end 
773  
774 
let param_stat = ref false 
775 
let param_eldarica = ref false 
776 
let param_utvpi = ref false 
777 
let param_tosmt = ref false 
778 
let param_pp = ref false 
779 

780 
module Verifier = 
781 
(struct 
782 
include VerifierType.Default 
783 
let name = "zustre" 
784 
let options = [ 
785 
"stat", Arg.Set param_stat, "print statistics"; 
786 
"eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules"; 
787 
"no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy"; 
788 
"tosmt", Arg.Set param_tosmt, "Print lowlevel (possibly unreadable) SMT2 statements"; 
789 
"nopp", Arg.Set param_pp, "No preprocessing (inlining and slicing)"; 
790 
] 
791 

792 
let activate () = ( 
793 
active := true; 
794 
Options.output := "horn"; 
795 
) 
796 
let is_active () = !active 
797  
798 
let get_normalization_params () = 
799 
(* make sure the output is "Horn" *) 
800 
assert(!Options.output = "horn"); 
801 
Backends.get_normalization_params () 
802  
803 
let setup_solver () = 
804 
fp := Z3.Fixedpoint.mk_fixedpoint !ctx; 
805 
(* let help = Z3.Fixedpoint.get_help fp in 
806 
* Format.eprintf "Fp help : %s@." help; 
807 
* 
808 
* let solver =Z3.Solver.mk_solver !ctx None in 
809 
* let help = Z3.Solver.get_help solver in 
810 
* Format.eprintf "Z3 help : %s@." help; *) 
811 

812 
let module P = Z3.Params in 
813 
let module S = Z3.Symbol in 
814 
let mks = S.mk_string !ctx in 
815 
let params = P.mk_params !ctx in 
816  
817 
(* self.fp.set (engine='spacer') *) 
818 
P.add_symbol params (mks "engine") (mks "spacer"); 
819 

820 
(* #z3.set_option(rational_to_decimal=True) *) 
821 
(* #self.fp.set('precision',30) *) 
822 
if !param_stat then 
823 
(* self.fp.set('print_statistics',True) *) 
824 
P.add_bool params (mks "print_statistics") true; 
825  
826 
(* Dont know where to find this parameter *) 
827 
(* if !param_spacer_verbose then 
828 
* if self.args.spacer_verbose: 
829 
* z3.set_option (verbose=1) *) 
830  
831 
(* The option is not recogined*) 
832 
(* self.fp.set('use_heavy_mev',True) *) 
833 
(* P.add_bool params (mks "use_heavy_mev") true; *) 
834 

835 
(* self.fp.set('pdr.flexible_trace',True) *) 
836 
P.add_bool params (mks "pdr.flexible_trace") true; 
837  
838 
(* self.fp.set('reset_obligation_queue',False) *) 
839 
P.add_bool params (mks "spacer.reset_obligation_queue") false; 
840  
841 
(* self.fp.set('spacer.elim_aux',False) *) 
842 
P.add_bool params (mks "spacer.elim_aux") false; 
843  
844 
(* if self.args.eldarica: 
845 
* self.fp.set('print_fixedpoint_extensions', False) *) 
846 
if !param_eldarica then 
847 
P.add_bool params (mks "print_fixedpoint_extensions") false; 
848 

849 
(* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *) 
850 
if !param_utvpi then 
851 
P.add_bool params (mks "pdr.utvpi") false; 
852  
853 
(* if self.args.tosmt: 
854 
* self.log.info("Setting low level printing") 
855 
* self.fp.set ('print.low_level_smt2',True) *) 
856 
if !param_tosmt then 
857 
P.add_bool params (mks "print.low_level_smt2") true; 
858  
859 
(* if not self.args.pp: 
860 
* self.log.info("No preprocessing") 
861 
* self.fp.set ('xform.slice', False) 
862 
* self.fp.set ('xform.inline_linear',False) 
863 
* self.fp.set ('xform.inline_eager',False) *\) *) 
864 
if !param_pp then ( 
865 
P.add_bool params (mks "xform.slice") false; 
866 
P.add_bool params (mks "xform.inline_linear") false; 
867 
P.add_bool params (mks "xform.inline_eager") false 
868 
); 
869 
Z3.Fixedpoint.set_parameters !fp params 
870 

871 

872 
let run basename prog machines = 
873 
let machines = Machine_code_common.arrow_machine::machines in 
874 
let machines = preprocess machines in 
875 
setup_solver (); 
876 
decl_sorts (); 
877 
List.iter (decl_machine machines) (List.rev machines); 
878  
879  
880 
(* Debug instructions *) 
881 
let rules_expr = Z3.Fixedpoint.get_rules !fp in 
882 
Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." 
883 
(Utils.fprintf_list ~sep:"@ " 
884 
(fun fmt e > Format.pp_print_string fmt (Z3.Expr.to_string e)) ) 
885 
rules_expr; 
886 

887 
() 
888 

889 

890  
891 
end: VerifierType.S) 
892 
