lustrec / src / tools / zustre_verifier.ml @ ff2d7a82
History  View  Annotate  Download (24.1 KB)
1 
open LustreSpec 

2 
open Machine_code 
3 
open Format 
4 
(* open Horn_backend_common 
5 
* open Horn_backend *) 
6  
7 
module HBC = Horn_backend_common 
8 
let machine_step_name = HBC.machine_step_name 
9 
let node_name = HBC.node_name 
10 
let concat = HBC.concat 
11 
let rename_machine = HBC.rename_machine 
12 
let rename_machine_list = HBC.rename_machine_list 
13 
let rename_next = HBC.rename_next 
14 
let rename_current = HBC.rename_current 
15 
let rename_current_list = HBC.rename_current_list 
16 
let rename_mid_list = HBC.rename_mid_list 
17 
let rename_next_list = HBC.rename_next_list 
18 
let full_memory_vars = HBC.full_memory_vars 
19 

20 
let active = ref false 
21 
let ctx = ref (Z3.mk_context []) 
22 
let machine_reset_name = HBC.machine_reset_name 
23 
let machine_stateless_name = HBC.machine_stateless_name 
24  
25 
(** Sorts 
26  
27 
A sort is introduced for each basic type and each enumerated type. 
28  
29 
A hashtbl records these and allow easy access to sort values, when 
30 
provided with a enumerated type name. 
31  
32 
*) 
33 

34 
let bool_sort = Z3.Boolean.mk_sort !ctx 
35 
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx 
36 
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx 
37  
38 
let const_sorts = Hashtbl.create 13 
39 
let const_tags = Hashtbl.create 13 
40 
let sort_elems = Hashtbl.create 13 
41  
42 
let get_const_sort = Hashtbl.find const_sorts 
43 
let get_sort_elems = Hashtbl.find sort_elems 
44 
let get_tag_sort = Hashtbl.find const_tags 
45 

46  
47 

48 
let decl_sorts () = 
49 
Hashtbl.iter (fun typ decl > 
50 
match typ with 
51 
 Tydec_const var > 
52 
(match decl.top_decl_desc with 
53 
 TypeDef tdef > ( 
54 
match tdef.tydef_desc with 
55 
 Tydec_enum tl > 
56 
let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in 
57 
Hashtbl.add const_sorts var new_sort; 
58 
Hashtbl.add sort_elems new_sort tl; 
59 
List.iter (fun t > Hashtbl.add const_tags t new_sort) tl 
60 

61 
 _ > assert false 
62 
) 
63 
 _ > assert false 
64 
) 
65 
 _ > ()) Corelang.type_table 
66  
67 

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

94 
let decl_var id = 
95 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in 
96 
register_fdecl id.var_id fdecl; 
97 
fdecl 
98  
99 
let decl_rel name args = 
100 
(*verifier ce qui est construit. On veut un declarerel *) 
101 
let args_sorts = List.map (fun v > type_to_sort v.var_type) args in 
102 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in 
103 
register_fdecl name fdecl; 
104 
fdecl 
105 

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

142 
(* Prints a constant value *) 
143 
let rec horn_const_to_expr c = 
144 
match c with 
145 
 Const_int i > Z3.Arithmetic.Integer.mk_numeral_i !ctx i 
146 
 Const_real (_,_,s) > Z3.Arithmetic.Real.mk_numeral_i !ctx 0 
147 
 Const_tag t > horn_tag_to_expr t 
148 
 _ > assert false 
149  
150  
151  
152 
(* Default value for each type, used when building arrays. Eg integer array 
153 
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value 
154 
for the type integer (arrays). 
155 
*) 
156 
let rec horn_default_val t = 
157 
let t = Types.dynamic_type t in 
158 
if Types.is_bool_type t then Z3.Boolean.mk_true !ctx else 
159 
if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
160 
if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
161 
(* match (Types.dynamic_type t).Types.tdesc with 
162 
*  Types.Tarray(dim, l) > (\* TODO PL: this strange code has to be (heavily) checked *\) 
163 
* let valt = Types.array_element_type t in 
164 
* fprintf fmt "((as const (Array Int %a)) %a)" 
165 
* pp_type valt 
166 
* pp_default_val valt 
167 
*  Types.Tstruct(l) > assert false 
168 
*  Types.Ttuple(l) > assert false 
169 
* _ > *) assert false 
170  
171  
172 
let horn_basic_app i val_to_expr vl = 
173 
match i, vl with 
174 
 "ite", [v1; v2; v3] > 
175 
Z3.Boolean.mk_ite 
176 
!ctx 
177 
(val_to_expr v1) 
178 
(val_to_expr v2) 
179 
(val_to_expr v3) 
180  
181 
 "uminus", [v] > 
182 
Z3.Arithmetic.mk_unary_minus 
183 
!ctx 
184 
(val_to_expr v) 
185 
 "not", [v] > 
186 
Z3.Boolean.mk_not 
187 
!ctx 
188 
(val_to_expr v) 
189 
 "=", [v1; v2] > 
190 
Z3.Boolean.mk_eq 
191 
!ctx 
192 
(val_to_expr v1) 
193 
(val_to_expr v2) 
194 
 "&&", [v1; v2] > 
195 
Z3.Boolean.mk_and 
196 
!ctx 
197 
[val_to_expr v1; 
198 
val_to_expr v2] 
199 
 "", [v1; v2] > 
200 
Z3.Boolean.mk_or 
201 
!ctx 
202 
[val_to_expr v1; 
203 
val_to_expr v2] 
204  
205 
 "impl", [v1; v2] > 
206 
Z3.Boolean.mk_implies 
207 
!ctx 
208 
(val_to_expr v1) 
209 
(val_to_expr v2) 
210 
 "mod", [v1; v2] > 
211 
Z3.Arithmetic.Integer.mk_mod 
212 
!ctx 
213 
(val_to_expr v1) 
214 
(val_to_expr v2) 
215 
 "equi", [v1; v2] > 
216 
Z3.Boolean.mk_eq 
217 
!ctx 
218 
(val_to_expr v1) 
219 
(val_to_expr v2) 
220 
 "xor", [v1; v2] > 
221 
Z3.Boolean.mk_xor 
222 
!ctx 
223 
(val_to_expr v1) 
224 
(val_to_expr v2) 
225 
 "!=", [v1; v2] > 
226 
Z3.Boolean.mk_not 
227 
!ctx 
228 
( 
229 
Z3.Boolean.mk_eq 
230 
!ctx 
231 
(val_to_expr v1) 
232 
(val_to_expr v2) 
233 
) 
234 
 "/", [v1; v2] > 
235 
Z3.Arithmetic.mk_div 
236 
!ctx 
237 
(val_to_expr v1) 
238 
(val_to_expr v2) 
239  
240 
(*  _, [v1; v2] > Z3.Boolean.mk_and 
241 
* !ctx 
242 
* (val_to_expr v1) 
243 
* (val_to_expr v2) 
244 
* 
245 
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) 
246 
 _ > ( 
247 
Format.eprintf 
248 
"internal error: zustre unkown function %s@." i; 
249 
assert false) 
250  
251 

252 
(* Convert a value expression [v], with internal function calls only. 
253 
[pp_var] is a printer for variables (typically [pp_c_var_read]), 
254 
but an offset suffix may be added for array variables 
255 
*) 
256 
let rec horn_val_to_expr ?(is_lhs=false) self v = 
257 
match v.value_desc with 
258 
 Cst c > horn_const_to_expr c 
259  
260 
(* Code specific for arrays *) 
261 
 Array il > 
262 
(* An array definition: 
263 
(store ( 
264 
... 
265 
(store ( 
266 
store ( 
267 
default_val 
268 
) 
269 
idx_n val_n 
270 
) 
271 
idx_n1 val_n1) 
272 
... 
273 
idx_1 val_1 
274 
) *) 
275 
let rec build_array (tab, x) = 
276 
match tab with 
277 
 [] > horn_default_val v.value_type(* (get_type v) *) 
278 
 h::t > 
279 
Z3.Z3Array.mk_store 
280 
!ctx 
281 
(build_array (t, (x+1))) 
282 
(Z3.Arithmetic.Integer.mk_numeral_i !ctx x) 
283 
(horn_val_to_expr ~is_lhs:is_lhs self h) 
284 
in 
285 
build_array (il, 0) 
286 

287 
 Access(tab,index) > 
288 
Z3.Z3Array.mk_select !ctx 
289 
(horn_val_to_expr ~is_lhs:is_lhs self tab) 
290 
(horn_val_to_expr ~is_lhs:is_lhs self index) 
291  
292 
(* Code specific for arrays *) 
293 

294 
 Power (v, n) > assert false 
295 
 LocalVar v > 
296 
horn_var_to_expr 
297 
(rename_machine 
298 
self 
299 
v) 
300 
 StateVar v > 
301 
if Types.is_array_type v.var_type 
302 
then assert false 
303 
else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) 
304 
 Fun (n, vl) > horn_basic_app n (horn_val_to_expr self) vl 
305  
306 
let no_reset_to_exprs machines m i = 
307 
let (n,_) = List.assoc i m.minstances in 
308 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 
309  
310 
let m_list = 
311 
rename_machine_list 
312 
(concat m.mname.node_id i) 
313 
(rename_mid_list (full_memory_vars machines target_machine)) 
314 
in 
315 
let c_list = 
316 
rename_machine_list 
317 
(concat m.mname.node_id i) 
318 
(rename_current_list (full_memory_vars machines target_machine)) 
319 
in 
320 
match c_list, m_list with 
321 
 [chd], [mhd] > 
322 
let expr = 
323 
Z3.Boolean.mk_eq !ctx 
324 
(horn_var_to_expr mhd) 
325 
(horn_var_to_expr chd) 
326 
in 
327 
[expr] 
328 
 _ > ( 
329 
let exprs = 
330 
List.map2 (fun mhd chd > 
331 
Z3.Boolean.mk_eq !ctx 
332 
(horn_var_to_expr mhd) 
333 
(horn_var_to_expr chd) 
334 
) 
335 
m_list 
336 
c_list 
337 
in 
338 
exprs 
339 
) 
340  
341 
let instance_reset_to_exprs machines m i = 
342 
let (n,_) = List.assoc i m.minstances in 
343 
let target_machine = List.find (fun m > m.mname.node_id = (Corelang.node_name n)) machines in 
344 
let vars = 
345 
( 
346 
(rename_machine_list 
347 
(concat m.mname.node_id i) 
348 
(rename_current_list (full_memory_vars machines target_machine)) 
349 
) 
350 
@ 
351 
(rename_machine_list 
352 
(concat m.mname.node_id i) 
353 
(rename_mid_list (full_memory_vars machines target_machine)) 
354 
) 
355 
) 
356 
in 
357 
let expr = 
358 
Z3.Expr.mk_app 
359 
!ctx 
360 
(get_fdecl (machine_reset_name (Corelang.node_name n))) 
361 
(List.map (horn_var_to_expr) vars) 
362 
in 
363 
[expr] 
364  
365 
let instance_call_to_exprs machines reset_instances m i inputs outputs = 
366 
let self = m.mname.node_id in 
367 
try (* stateful node instance *) 
368 
begin 
369 
let (n,_) = List.assoc i m.minstances in 
370 
let target_machine = List.find (fun m > m.mname.node_id = Corelang.node_name n) machines in 
371  
372 
(* Checking whether this specific instances has been reset yet *) 
373 
let reset_exprs = 
374 
if not (List.mem i reset_instances) then 
375 
(* If not, declare mem_m = mem_c *) 
376 
no_reset_to_exprs machines m i 
377 
else 
378 
[] (* Nothing to add yet *) 
379 
in 
380 

381 
let mems = full_memory_vars machines target_machine in 
382 
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in 
383 
let mid_mems = rename_mems rename_mid_list in 
384 
let next_mems = rename_mems rename_next_list in 
385  
386 
let call_expr = 
387 
match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with 
388 
 "_arrow", [i1; i2], [o], [mem_m], [mem_x] > begin 
389 
let stmt1 = (* out = ite mem_m then i1 else i2 *) 
390 
Z3.Boolean.mk_eq !ctx 
391 
( (* output var *) 
392 
horn_val_to_expr 
393 
~is_lhs:true 
394 
self 
395 
(mk_val (LocalVar o) o.var_type) 
396 
) 
397 
( 
398 
Z3.Boolean.mk_ite !ctx 
399 
(horn_var_to_expr mem_m) 
400 
(horn_val_to_expr self i1) 
401 
(horn_val_to_expr self i2) 
402 
) 
403 
in 
404 
let stmt2 = (* mem_X = false *) 
405 
Z3.Boolean.mk_eq !ctx 
406 
(horn_var_to_expr mem_x) 
407 
(Z3.Boolean.mk_false !ctx) 
408 
in 
409 
[stmt1; stmt2] 
410 
end 
411  
412 
 node_name_n > 
413 
let expr = 
414 
Z3.Expr.mk_app 
415 
!ctx 
416 
(get_fdecl (machine_step_name (node_name n))) 
417 
( (* Arguments are input, output, mid_mems, next_mems *) 
418 
( 
419 
List.map (horn_val_to_expr self) ( 
420 
inputs @ 
421 
(List.map (fun v > mk_val (LocalVar v) v.var_type) outputs) 
422 
) 
423 
) @ ( 
424 
List.map (horn_var_to_expr) (mid_mems@next_mems) 
425 
) 
426 
) 
427 
in 
428 
[expr] 
429 
in 
430  
431 
reset_exprs@call_expr 
432 
end 
433 
with Not_found > ( (* stateless node instance *) 
434 
let (n,_) = List.assoc i m.mcalls in 
435 
let expr = 
436 
Z3.Expr.mk_app 
437 
!ctx 
438 
(get_fdecl (machine_stateless_name (node_name n))) 
439 
((* Arguments are inputs, outputs *) 
440 
List.map (horn_val_to_expr self) 
441 
( 
442 
inputs @ (List.map (fun v > mk_val (LocalVar v) v.var_type) outputs) 
443 
) 
444 
) 
445 
in 
446 
[expr] 
447 
) 
448 

449  
450 
(* Convert instruction to Z3.Expr and update the set of reset instances *) 
451 
let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list = 
452 
match Corelang.get_instr_desc instr with 
453 
 MComment _ > [], reset_instances 
454 
 MNoReset i > (* we assign middle_mem with mem_m. And declare i as reset *) 
455 
no_reset_to_exprs machines m i, 
456 
i::reset_instances 
457 
 MReset i > (* we assign middle_mem with reset: reset(mem_m) *) 
458 
instance_reset_to_exprs machines m i, 
459 
i::reset_instances 
460 
 MLocalAssign (i,v) > 
461 
assign_to_exprs 
462 
m (horn_var_to_expr) 
463 
(mk_val (LocalVar i) i.var_type) v, 
464 
reset_instances 
465 
 MStateAssign (i,v) > 
466 
assign_to_exprs 
467 
m (horn_var_to_expr) 
468 
(mk_val (StateVar i) i.var_type) v, 
469 
reset_instances 
470 
 MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl) > 
471 
assert false (* This should not happen anymore *) 
472 
 MStep (il, i, vl) > 
473 
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = 
474 
mem_c and print the call to mem_m *) 
475 
instance_call_to_exprs machines reset_instances m i vl il, 
476 
reset_instances (* Since this instance call will only happen once, we 
477 
don't have to update reset_instances *) 
478  
479 
 MBranch (g,hl) > (* (g = tag1 => expr1) and (g = tag2 => expr2) ... 
480 
should not be produced yet. Later, we will have to 
481 
compare the reset_instances of each branch and 
482 
introduced the mem_m = mem_c for branches to do not 
483 
address it while other did. Am I clear ? *) 
484 
(* For each branch we obtain the logical encoding, and the information 
485 
whether a sub node has been reset or not. If a node has been reset in one 
486 
of the branch, then all others have to have the mem_m = mem_c 
487 
statement. *) 
488 
let self = m.mname.node_id in 
489 
let branch_to_expr (tag, instrs) = 
490 
Z3.Boolean.mk_implies 
491 
(Z3.Boolean.mk_eq !ctx 
492 
(horn_val_to_expr self g) 
493 
(horn_tag_to_expr tag)) 
494 
(machine_instrs_to_exprs machines reset_instances m instrs) 
495 
in 
496 
List.map branch_to_expr hl, 
497 
reset_instances 
498  
499 
and instrs_to_expr machines reset_instances m instrs = 
500 
let instr_to_expr rs i = instr_to_expr machines rs m i in 
501 
match instrs with 
502 
 [x] > instr_to_expres reset_instances x 
503 
 _::_ > (* 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 *) 
504  
505 
List.fold_left (fun (exprs, rs) i > 
506 
let exprs_i, rs = ppi rs i in 
507 
expr@exprs_i, rs 
508 
) 
509 
([], reset_instances) instrs 
510 

511 

512 
 [] > [], reset_instances 
513  
514  
515 
let basic_library_to_horn_expr i vl = 
516 
match i, vl with 
517 
 "ite", [v1; v2; v3] > Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3 
518  
519 
 "uminus", [v] > Format.fprintf fmt "( %a)" pp_val v 
520 
 "not", [v] > Format.fprintf fmt "(not %a)" pp_val v 
521 
 "=", [v1; v2] > Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 
522 
 "&&", [v1; v2] > Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 
523 
 "", [v1; v2] > Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 
524 
 "impl", [v1; v2] > Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 
525 
 "mod", [v1; v2] > Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2 
526 
 "equi", [v1; v2] > Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2 
527 
 "xor", [v1; v2] > Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2 
528 
 "!=", [v1; v2] > Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 
529 
 "/", [v1; v2] > Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 
530 
 _, [v1; v2] > Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 
531 
 _ > (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false) 
532 
(*  "mod", [v1; v2] > Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
533  
534 
*) 
535  
536 

537 
(* Prints a [value] indexed by the suffix list [loop_vars] *) 
538 
let rec value_suffix_to_expr self value = 
539 
match value.value_desc with 
540 
 Fun (n, vl) > 
541 
basic_library_to_horn_expr n (value_suffix_to_expr self vl) 
542 
 _ > 
543 
horn_val_to_expr self value 
544  
545 

546 
(* type_directed assignment: array vs. statically sized type 
547 
 [var_type]: type of variable to be assigned 
548 
 [var_name]: name of variable to be assigned 
549 
 [value]: assigned value 
550 
 [pp_var]: printer for variables 
551 
*) 
552 
let assign_to_exprs m var_name value = 
553 
let self = m.mname.node_id in 
554 
let e = 
555 
Z3.Boolean.mk_eq 
556 
!ctx 
557 
(horn_val_to_expr ~is_lhs:true self var_name) 
558 
(value_suffix_to_expr self value) 
559 
in 
560 
[e] 
561  
562 
(* TODO: empty list means true statement *) 
563 
let decl_machine machines m = 
564 
if m.Machine_code.mname.node_id = Machine_code.arrow_id then 
565 
(* We don't print arrow function *) 
566 
() 
567 
else 
568 
begin 
569 
let vars = 
570 
List.map decl_var 
571 
( 
572 
(inout_vars machines m)@ 
573 
(rename_current_list (full_memory_vars machines m)) @ 
574 
(rename_mid_list (full_memory_vars machines m)) @ 
575 
(rename_next_list (full_memory_vars machines m)) @ 
576 
(rename_machine_list m.mname.node_id m.mstep.step_locals) 
577 
) 
578 
in 
579 

580 
if is_stateless m then 
581 
begin 
582 
(* Declaring single predicate *) 
583 
let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in 
584 
match m.mstep.step_asserts with 
585 
 [] > 
586 
begin 
587  
588 
(* Rule for single predicate *) 
589 
fprintf fmt "; Stateless step rule @."; 
590 
fprintf fmt "@[<v 2>(rule (=> @ "; 
591 
ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs); 
592 
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." 
593 
pp_machine_stateless_name m.mname.node_id 
594 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m); 
595 
end 
596 
 assertsl > 
597 
begin 
598 
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in 
599 

600 
fprintf fmt "; Stateless step rule with Assertions @."; 
601 
(*Rule for step*) 
602 
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; 
603 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 
604 
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl 
605 
pp_machine_stateless_name m.mname.node_id 
606 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m); 
607 

608 
end 
609 

610 
end 
611 
else 
612 
begin 
613 
(* Declaring predicate *) 
614 
let _ = decl_rel (machine_reset_name m.mname.node_id) (reset_vars machines m) in 
615 
let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in 
616  
617 
(* Rule for reset *) 
618 
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." 
619 
(pp_machine_reset machines) m 
620 
pp_machine_reset_name m.mname.node_id 
621 
(Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m); 
622  
623 
match m.mstep.step_asserts with 
624 
 [] > 
625 
begin 
626 
fprintf fmt "; Step rule @."; 
627 
(* Rule for step*) 
628 
fprintf fmt "@[<v 2>(rule (=> @ "; 
629 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 
630 
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." 
631 
pp_machine_step_name m.mname.node_id 
632 
(Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m); 
633 
end 
634 
 assertsl > 
635 
begin 
636 
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in 
637 
(* print_string pp_val; *) 
638 
fprintf fmt "; Step rule with Assertions @."; 
639 

640 
(*Rule for step*) 
641 
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; 
642 
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); 
643 
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl 
644 
pp_machine_step_name m.mname.node_id 
645 
(Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m); 
646 
end 
647 

648 

649 
end 
650 
end 
651  
652 
let param_stat = ref false 
653 
let param_eldarica = ref false 
654 
let param_utvpi = ref false 
655 
let param_tosmt = ref false 
656 
let param_pp = ref false 
657 

658 
module Verifier = 
659 
(struct 
660 
include VerifierType.Default 
661 
let name = "zustre" 
662 
let options = [ 
663 
"stat", Arg.Set param_stat, "print statistics"; 
664 
"eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules"; 
665 
"no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy"; 
666 
"tosmt", Arg.Set param_tosmt, "Print lowlevel (possibly unreadable) SMT2 statements"; 
667 
"nopp", Arg.Set param_pp, "No preprocessing (inlining and slicing)"; 
668 
] 
669 

670 
let activate () = ( 
671 
active := true; 
672 
Options.output := "horn"; 
673 
) 
674 
let is_active () = !active 
675  
676 
let get_normalization_params () = 
677 
(* make sure the output is "Horn" *) 
678 
assert(!Options.output = "horn"); 
679 
Backends.get_normalization_params () 
680  
681 
let setup_solver () = 
682 
let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in 
683 
(* let help = Z3.Fixedpoint.get_help fp in 
684 
* Format.eprintf "Fp help : %s@." help; 
685 
* 
686 
* let solver =Z3.Solver.mk_solver !ctx None in 
687 
* let help = Z3.Solver.get_help solver in 
688 
* Format.eprintf "Z3 help : %s@." help; *) 
689 

690 
let module P = Z3.Params in 
691 
let module S = Z3.Symbol in 
692 
let mks = S.mk_string !ctx in 
693 
let params = P.mk_params !ctx in 
694  
695 
(* self.fp.set (engine='spacer') *) 
696 
P.add_symbol params (mks "engine") (mks "spacer"); 
697 

698 
(* #z3.set_option(rational_to_decimal=True) *) 
699 
(* #self.fp.set('precision',30) *) 
700 
if !param_stat then 
701 
(* self.fp.set('print_statistics',True) *) 
702 
P.add_bool params (mks "print_statistics") true; 
703  
704 
(* Dont know where to find this parameter *) 
705 
(* if !param_spacer_verbose then 
706 
* if self.args.spacer_verbose: 
707 
* z3.set_option (verbose=1) *) 
708  
709 
(* The option is not recogined*) 
710 
(* self.fp.set('use_heavy_mev',True) *) 
711 
(* P.add_bool params (mks "use_heavy_mev") true; *) 
712 

713 
(* self.fp.set('pdr.flexible_trace',True) *) 
714 
P.add_bool params (mks "pdr.flexible_trace") true; 
715  
716 
(* self.fp.set('reset_obligation_queue',False) *) 
717 
P.add_bool params (mks "spacer.reset_obligation_queue") false; 
718  
719 
(* self.fp.set('spacer.elim_aux',False) *) 
720 
P.add_bool params (mks "spacer.elim_aux") false; 
721  
722 
(* if self.args.eldarica: 
723 
* self.fp.set('print_fixedpoint_extensions', False) *) 
724 
if !param_eldarica then 
725 
P.add_bool params (mks "print_fixedpoint_extensions") false; 
726 

727 
(* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *) 
728 
if !param_utvpi then 
729 
P.add_bool params (mks "pdr.utvpi") false; 
730  
731 
(* if self.args.tosmt: 
732 
* self.log.info("Setting low level printing") 
733 
* self.fp.set ('print.low_level_smt2',True) *) 
734 
if !param_tosmt then 
735 
P.add_bool params (mks "print.low_level_smt2") true; 
736  
737 
(* if not self.args.pp: 
738 
* self.log.info("No preprocessing") 
739 
* self.fp.set ('xform.slice', False) 
740 
* self.fp.set ('xform.inline_linear',False) 
741 
* self.fp.set ('xform.inline_eager',False) *\) *) 
742 
if !param_pp then ( 
743 
P.add_bool params (mks "xform.slice") false; 
744 
P.add_bool params (mks "xform.inline_linear") false; 
745 
P.add_bool params (mks "xform.inline_eager") false 
746 
); 
747 
Z3.Fixedpoint.set_parameters fp params 
748 

749 

750 
let run basename prog machines = 
751 
let machines = Machine_code.arrow_machine::machines in 
752 
let machines = preprocess machines in 
753 
setup_solver (); 
754 
decl_sorts (); 
755 
List.iter (decl_machine machines) (List.rev machines); 
756  
757 

758 
() 
759  
760 
end: VerifierType.S) 
761 
