Revision 51106b7e
Added by PierreLoïc Garoche over 5 years ago
src/tools/zustre/zustre_common.ml  

366  366 
is a printer for variables (typically [pp_c_var_read]), but an offset suffix 
367  367 
may be added for array variables 
368  368 
*) 
369 
let rec horn_val_to_expr ?(is_lhs=false) self v = 

369 
let rec horn_val_to_expr ?(is_lhs=false) m self v =


370  370 
match v.value_desc with 
371  371 
 Cst c > horn_const_to_expr c 
372  372  
...  ...  
393  393 
!ctx 
394  394 
(build_array (t, (x+1))) 
395  395 
(Z3.Arithmetic.Integer.mk_numeral_i !ctx x) 
396 
(horn_val_to_expr ~is_lhs:is_lhs self h) 

396 
(horn_val_to_expr ~is_lhs:is_lhs m self h)


397  397 
in 
398  398 
build_array (il, 0) 
399 


399 


400  400 
 Access(tab,index) > 
401  401 
Z3.Z3Array.mk_select !ctx 
402 
(horn_val_to_expr ~is_lhs:is_lhs self tab) 

403 
(horn_val_to_expr ~is_lhs:is_lhs self index) 

402 
(horn_val_to_expr ~is_lhs:is_lhs m self tab)


403 
(horn_val_to_expr ~is_lhs:is_lhs m self index)


404  404  
405  405 
(* Code specific for arrays *) 
406  406 

407  407 
 Power (v, n) > assert false 
408 
 LocalVar v > 

409 
horn_var_to_expr 

410 
(rename_machine 

411 
self 

412 
v) 

413 
 StateVar v > 

414 
if Types.is_array_type v.var_type 

415 
then assert false 

416 
else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) 

417 
 Fun (n, vl) > horn_basic_app n (horn_val_to_expr self) vl 

408 
 Var v > 

409 
if is_memory m v then 

410 
if Types.is_array_type v.var_type 

411 
then assert false 

412 
else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) 

413 


414 
else 

415 
horn_var_to_expr 

416 
(rename_machine 

417 
self 

418 
v) 

419 
 Fun (n, vl) > horn_basic_app n (horn_val_to_expr m self) vl 

418  420  
419  421 
let no_reset_to_exprs machines m i = 
420  422 
let (n,_) = List.assoc i m.minstances in 
...  ...  
478  480 
let idx = horn_var_to_expr idx in 
479  481 
let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in 
480  482 
let inout = 
481 
List.map (horn_val_to_expr self) 

482 
(inputs @ (List.map (fun v > mk_val (LocalVar v) v.var_type) outputs))


483 
List.map (horn_val_to_expr m self)


484 
(inputs @ (List.map (fun v > mk_val (Var v) v.var_type) outputs)) 

483  485 
in 
484  486 
idx::uid::inout 
485  487 
in 
...  ...  
509  511 
let stmt1 = (* out = ite mem_m then i1 else i2 *) 
510  512 
Z3.Boolean.mk_eq !ctx 
511  513 
( (* output var *) 
512 
horn_val_to_expr 

514 
horn_val_to_expr


513  515 
~is_lhs:true 
514 
self 

515 
(mk_val (LocalVar o) o.var_type)


516 
m self


517 
(mk_val (Var o) o.var_type) 

516  518 
) 
517  519 
( 
518  520 
Z3.Boolean.mk_ite !ctx 
519  521 
(horn_var_to_expr mem_m) 
520 
(horn_val_to_expr self i1) 

521 
(horn_val_to_expr self i2) 

522 
(horn_val_to_expr m self i1)


523 
(horn_val_to_expr m self i2)


522  524 
) 
523  525 
in 
524  526 
let stmt2 = (* mem_X = false *) 
...  ...  
578  580 
let e = 
579  581 
Z3.Boolean.mk_eq 
580  582 
!ctx 
581 
(horn_val_to_expr ~is_lhs:true self var_name) 

582 
(horn_val_to_expr self value) 

583 
(horn_val_to_expr ~is_lhs:true m self var_name)


584 
(horn_val_to_expr m self value)


583  585 
(* was: TODO deal with array accesses (value_suffix_to_expr self value) *) 
584  586 
in 
585  587 
[e] 
...  ...  
598  600 
 MLocalAssign (i,v) > 
599  601 
assign_to_exprs 
600  602 
m 
601 
(mk_val (LocalVar i) i.var_type) v,


603 
(mk_val (Var i) i.var_type) v, 

602  604 
reset_instances 
603  605 
 MStateAssign (i,v) > 
604  606 
assign_to_exprs 
605  607 
m 
606 
(mk_val (StateVar i) i.var_type) v,


608 
(mk_val (Var i) i.var_type) v, 

607  609 
reset_instances 
608  610 
 MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v > v.value_type) vl) > 
609  611 
assert false (* This should not happen anymore *) 
...  ...  
629  631 
let e = 
630  632 
Z3.Boolean.mk_implies !ctx 
631  633 
(Z3.Boolean.mk_eq !ctx 
632 
(horn_val_to_expr self g) 

634 
(horn_val_to_expr m self g)


633  635 
(horn_tag_to_expr tag)) 
634  636 
branch_def in 
635  637  
...  ...  
857  859 
begin 
858  860 
(*Rule for step "; Stateless step rule with Assertions @.";*) 
859  861 
let body_with_asserts = 
860 
Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl) 

862 
Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)


861  863 
in 
862  864 
let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in 
863  865 
add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head) 
...  ...  
915  917 
(* Rule for step Assertions @.; *) 
916  918 
let body_with_asserts = 
917  919 
Z3.Boolean.mk_and !ctx 
918 
(horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl) 

920 
(horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)


919  921 
in 
920  922 
let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in 
921  923 
add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head) 
Also available in: Unified diff
Fixing issues with changes in machine code