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