1
|
open Lustre_types
|
2
|
open Machine_code_types
|
3
|
open Machine_code_common
|
4
|
|
5
|
(* open Horn_backend_common
|
6
|
* open Horn_backend *)
|
7
|
open Zustre_data
|
8
|
|
9
|
let report = Log.report ~plugin:"z3 interface"
|
10
|
|
11
|
module HBC = Horn_backend_common
|
12
|
|
13
|
let node_name = HBC.node_name
|
14
|
|
15
|
let concat = HBC.concat
|
16
|
|
17
|
let rename_machine = HBC.rename_machine
|
18
|
|
19
|
let rename_machine_list = HBC.rename_machine_list
|
20
|
|
21
|
let rename_next = HBC.rename_next
|
22
|
|
23
|
let rename_mid = HBC.rename_mid
|
24
|
|
25
|
let rename_current = HBC.rename_current
|
26
|
|
27
|
let rename_current_list = HBC.rename_current_list
|
28
|
|
29
|
let rename_mid_list = HBC.rename_mid_list
|
30
|
|
31
|
let rename_next_list = HBC.rename_next_list
|
32
|
|
33
|
let full_memory_vars = HBC.full_memory_vars
|
34
|
|
35
|
let inout_vars = HBC.inout_vars
|
36
|
|
37
|
let reset_vars = HBC.reset_vars
|
38
|
|
39
|
let step_vars = HBC.step_vars
|
40
|
|
41
|
let local_memory_vars = HBC.local_memory_vars
|
42
|
|
43
|
let step_vars_m_x = HBC.step_vars_m_x
|
44
|
|
45
|
let step_vars_c_m_x = HBC.step_vars_c_m_x
|
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
|
52
|
|
53
|
let preprocess = Horn_backend.preprocess
|
54
|
|
55
|
exception UnknownFunction of (string * (Format.formatter -> unit))
|
56
|
(** Sorts
|
57
|
|
58
|
A sort is introduced for each basic type and each enumerated type.
|
59
|
|
60
|
A hashtbl records these and allow easy access to sort values, when provided
|
61
|
with a enumerated type name. *)
|
62
|
|
63
|
let bool_sort = Z3.Boolean.mk_sort !ctx
|
64
|
|
65
|
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
|
66
|
|
67
|
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
|
68
|
|
69
|
let get_const_sort = Hashtbl.find const_sorts
|
70
|
|
71
|
let get_sort_elems = Hashtbl.find sort_elems
|
72
|
|
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
|
|
79
|
let decl_sorts () =
|
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
|
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
|
119
|
|
120
|
(* let idx_var = *)
|
121
|
(* Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort *)
|
122
|
|
123
|
(* let uid_var = *)
|
124
|
(* Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort *)
|
125
|
|
126
|
(** Func decls
|
127
|
|
128
|
Similarly fun_decls are registerd, by their name, into a hashtbl. The
|
129
|
proposed encoding introduces a 0-ary fun_decl to model variables and
|
130
|
fun_decl with arguments to declare reset and step predicates. *)
|
131
|
let register_fdecl id fd = Hashtbl.add decls id fd
|
132
|
|
133
|
let get_fdecl id =
|
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
|
139
|
|
140
|
let pp_fdecls fmt =
|
141
|
Format.fprintf fmt "Registered fdecls: @[%a@]@ "
|
142
|
(Utils.fprintf_list ~sep:"@ " Format.pp_print_string)
|
143
|
(Hashtbl.fold (fun id _ accu -> id :: accu) decls [])
|
144
|
|
145
|
let decl_var id =
|
146
|
(* Format.eprintf "Declaring var %s@." id.var_id; *)
|
147
|
let fdecl =
|
148
|
Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type)
|
149
|
in
|
150
|
register_fdecl id.var_id fdecl;
|
151
|
fdecl
|
152
|
|
153
|
(* Declaring the function used in expr *)
|
154
|
let decl_fun op args typ =
|
155
|
let args = List.map type_to_sort args in
|
156
|
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in
|
157
|
register_fdecl op fdecl;
|
158
|
fdecl
|
159
|
|
160
|
let idx_sort = int_sort
|
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 =
|
166
|
let fd = Z3.Z3List.get_cons_decl uid_sort in
|
167
|
fun head tail -> Z3.FuncDecl.apply fd [ head; tail ]
|
168
|
|
169
|
let get_instance_uid =
|
170
|
let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in
|
171
|
let cpt = ref 0 in
|
172
|
fun i ->
|
173
|
let id =
|
174
|
if Hashtbl.mem hash i then Hashtbl.find hash i
|
175
|
else (
|
176
|
incr cpt;
|
177
|
Hashtbl.add hash i !cpt;
|
178
|
!cpt)
|
179
|
in
|
180
|
Z3.Arithmetic.Integer.mk_numeral_i !ctx id
|
181
|
|
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 *)
|
184
|
let args_sorts =
|
185
|
if no_additional_vars then args_sorts
|
186
|
else idx_sort :: uid_sort :: args_sorts
|
187
|
in
|
188
|
|
189
|
(* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
|
190
|
if !debug then
|
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;
|
195
|
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
|
196
|
Z3.Fixedpoint.register_relation !fp fdecl;
|
197
|
register_fdecl name fdecl;
|
198
|
fdecl
|
199
|
|
200
|
(* Shared variables to describe counter and uid *)
|
201
|
|
202
|
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int
|
203
|
|
204
|
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx)
|
205
|
|
206
|
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
|
207
|
|
208
|
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort
|
209
|
|
210
|
let _ = register_fdecl "__uid__" uid_fd
|
211
|
|
212
|
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd
|
213
|
|
214
|
(** Conversion functions
|
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. *)
|
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)
|
221
|
|
222
|
(* Used to print boolean constants *)
|
223
|
let horn_tag_to_expr t =
|
224
|
if t = tag_true then Z3.Boolean.mk_true !ctx
|
225
|
else if t = tag_false then Z3.Boolean.mk_false !ctx
|
226
|
else
|
227
|
(* Finding the associated sort *)
|
228
|
let sort = get_tag_sort t in
|
229
|
let elems = get_sort_elems sort in
|
230
|
let res : Z3.Expr.expr option =
|
231
|
List.fold_left2
|
232
|
(fun res cst expr ->
|
233
|
match res with
|
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)
|
240
|
in
|
241
|
match res with None -> assert false | Some s -> s
|
242
|
|
243
|
(* Prints a constant value *)
|
244
|
let horn_const_to_expr c =
|
245
|
match c with
|
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
|
254
|
|
255
|
(* Default value for each type, used when building arrays. Eg integer array
|
256
|
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
|
257
|
for the type integer (arrays). *)
|
258
|
let horn_default_val t =
|
259
|
let t = Types.dynamic_type t in
|
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
|
274
|
|
275
|
(* Conversion of basic library functions *)
|
276
|
|
277
|
let horn_basic_app i vl (vltyp, typ) =
|
278
|
match i, vl with
|
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
|
319
|
| _ ->
|
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 *)
|
340
|
|
341
|
(* | _ -> (
|
342
|
* let msg fmt = Format.fprintf fmt
|
343
|
* "internal error: zustre unkown function %s (nb args = %i)@."
|
344
|
* i (List.length vl)
|
345
|
* in
|
346
|
* raise (UnknownFunction(i, msg))
|
347
|
* ) *)
|
348
|
|
349
|
(* Convert a value expression [v], with internal function calls only. [pp_var]
|
350
|
is a printer for variables (typically [pp_c_var_read]), but an offset suffix
|
351
|
may be added for array variables *)
|
352
|
let rec horn_val_to_expr ?(is_lhs = false) m self v =
|
353
|
(* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *)
|
354
|
match v.value_desc with
|
355
|
| Cst c ->
|
356
|
horn_const_to_expr c
|
357
|
(* Code specific for arrays *)
|
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)
|
376
|
(* Code specific for arrays *)
|
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)
|
391
|
|
392
|
let no_reset_to_exprs machines m i =
|
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
|
397
|
|
398
|
let m_list =
|
399
|
rename_machine_list (concat m.mname.node_id i)
|
400
|
(rename_mid_list (full_memory_vars machines target_machine))
|
401
|
in
|
402
|
let c_list =
|
403
|
rename_machine_list (concat m.mname.node_id i)
|
404
|
(rename_current_list (full_memory_vars machines target_machine))
|
405
|
in
|
406
|
match c_list, m_list with
|
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
|
| _ ->
|
413
|
let exprs =
|
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
|
418
|
in
|
419
|
exprs
|
420
|
|
421
|
let instance_reset_to_exprs machines m i =
|
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
|
426
|
let vars =
|
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)
|
430
|
in
|
431
|
|
432
|
let expr =
|
433
|
Z3.Expr.mk_app !ctx
|
434
|
(get_fdecl (machine_reset_name (Corelang.node_name n)))
|
435
|
(List.map horn_var_to_expr (idx :: uid :: vars))
|
436
|
in
|
437
|
[ expr ]
|
438
|
|
439
|
let instance_call_to_exprs machines reset_instances m i inputs outputs =
|
440
|
let self = m.mname.node_id in
|
441
|
|
442
|
(* Building call args *)
|
443
|
let idx_uid_inout =
|
444
|
(* Additional input to register step counters, and uid *)
|
445
|
let idx = horn_var_to_expr idx in
|
446
|
let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
|
447
|
let inout =
|
448
|
List.map (horn_val_to_expr m self)
|
449
|
(inputs @ List.map (fun v -> mk_val (Var v) v.var_type) outputs)
|
450
|
in
|
451
|
idx :: uid :: inout
|
452
|
in
|
453
|
|
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
|
459
|
in
|
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 ]
|
518
|
|
519
|
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
|
520
|
(* let rec value_suffix_to_expr self value = *)
|
521
|
(* match value.value_desc with *)
|
522
|
(* | Fun (n, vl) -> *)
|
523
|
(* horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
|
524
|
|
525
|
(* | _ -> *)
|
526
|
(* horn_val_to_expr self value *)
|
527
|
|
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 *)
|
531
|
let assign_to_exprs m var_name value =
|
532
|
let self = m.mname.node_id in
|
533
|
let e =
|
534
|
Z3.Boolean.mk_eq !ctx
|
535
|
(horn_val_to_expr ~is_lhs:true m self var_name)
|
536
|
(horn_val_to_expr m self value)
|
537
|
(* was: TODO deal with array accesses (value_suffix_to_expr self value) *)
|
538
|
in
|
539
|
[ e ]
|
540
|
|
541
|
(* Convert instruction to Z3.Expr and update the set of reset instances *)
|
542
|
let rec instr_to_exprs machines reset_instances (m : machine_t) instr :
|
543
|
Z3.Expr.expr list * ident list =
|
544
|
match Corelang.get_instr_desc instr with
|
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
|
->
|
560
|
assert false (* This should not happen anymore *)
|
561
|
| MStep (il, i, vl) ->
|
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 ? *)
|
572
|
(* For each branch we obtain the logical encoding, and the information
|
573
|
whether a sub node has been reset or not. If a node has been reset in one
|
574
|
of the branch, then all others have to have the mem_m = mem_c statement. *)
|
575
|
let self = m.mname.node_id in
|
576
|
let branch_to_expr (tag, instrs) =
|
577
|
let branch_def, branch_resets =
|
578
|
instrs_to_expr machines reset_instances m instrs
|
579
|
in
|
580
|
let e =
|
581
|
Z3.Boolean.mk_implies !ctx
|
582
|
(Z3.Boolean.mk_eq !ctx
|
583
|
(horn_val_to_expr m self g)
|
584
|
(horn_tag_to_expr tag))
|
585
|
branch_def
|
586
|
in
|
587
|
|
588
|
[ e ], branch_resets
|
589
|
in
|
590
|
|
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 =
|
600
|
let instr_to_exprs rs i = instr_to_exprs machines rs m i in
|
601
|
let e_list, rs =
|
602
|
match instrs with
|
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
|
616
|
in
|
617
|
let e =
|
618
|
match e_list with
|
619
|
| [ e ] ->
|
620
|
e
|
621
|
| [] ->
|
622
|
Z3.Boolean.mk_true !ctx
|
623
|
| _ ->
|
624
|
Z3.Boolean.mk_and !ctx e_list
|
625
|
in
|
626
|
e, rs
|
627
|
|
628
|
(*********************************************************)
|
629
|
|
630
|
(* Quantifiying universally all occuring variables *)
|
631
|
let add_rule ?(dont_touch = []) vars expr =
|
632
|
(* let fds = Z3.Expr.get_args expr in *)
|
633
|
(* Format.eprintf "Expr %s: args: [%a]@." *)
|
634
|
(* (Z3.Expr.to_string expr) *)
|
635
|
(* (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt
|
636
|
(Z3.Expr.to_string e))) fds; *)
|
637
|
|
638
|
(* (\* Old code relying on provided vars *\) *)
|
639
|
(* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *)
|
640
|
(* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl
|
641
|
id.var_id)) vars) in *)
|
642
|
|
643
|
(* New code: we extract vars from expr *)
|
644
|
let module FDSet = Set.Make (struct
|
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
|
674
|
Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
|
675
|
(Z3.Expr.to_string expr)
|
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
|
(* ? *)
|
689
|
in
|
690
|
|
691
|
(* Format.eprintf "OK@.@?"; *)
|
692
|
|
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
|
695
|
|
696
|
(********************************************************)
|
697
|
|
698
|
let machine_reset machines m =
|
699
|
let locals = local_memory_vars m in
|
700
|
|
701
|
(* print "x_m = x_c" for each local memory *)
|
702
|
let mid_mem_def =
|
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
|
709
|
in
|
710
|
|
711
|
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special
|
712
|
treatment for _arrow: _first = true *)
|
713
|
let reset_instances =
|
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
|
739
|
in
|
740
|
|
741
|
Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
|
742
|
|
743
|
(* TODO: empty list means true statement *)
|
744
|
let decl_machine machines m =
|
745
|
if m.mname.node_id = Arrow.arrow_id then (* We don't do arrow function *)
|
746
|
()
|
747
|
else
|
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))
|
811
|
in
|
812
|
|
813
|
let _ =
|
814
|
add_rule (idx :: uid :: vars)
|
815
|
(Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
|
816
|
in
|
817
|
|
818
|
(* Rule for step*)
|
819
|
let vars = step_vars machines m in
|
820
|
let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
|
821
|
let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
|
822
|
let horn_step_body, _ (* don't care for reset here *) =
|
823
|
instrs_to_expr machines [] m m.mstep.step_instrs
|
824
|
in
|
825
|
let horn_step_head =
|
826
|
Z3.Expr.mk_app !ctx
|
827
|
(get_fdecl (machine_step_name m.mname.node_id))
|
828
|
(List.map horn_var_to_expr
|
829
|
(idx :: uid :: (* Additional vars: counters, uid *)
|
830
|
vars))
|
831
|
in
|
832
|
match m.mstep.step_asserts with
|
833
|
| [] ->
|
834
|
(* Rule for single predicate *)
|
835
|
let vars =
|
836
|
step_vars_c_m_x machines m
|
837
|
@ rename_machine_list m.mname.node_id m.mstep.step_locals
|
838
|
in
|
839
|
add_rule (idx :: uid :: vars)
|
840
|
(Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
|
841
|
| assertsl ->
|
842
|
(* Rule for step Assertions @.; *)
|
843
|
let body_with_asserts =
|
844
|
Z3.Boolean.mk_and !ctx
|
845
|
(horn_step_body
|
846
|
:: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
|
847
|
in
|
848
|
let vars =
|
849
|
step_vars_c_m_x machines m
|
850
|
@ rename_machine_list m.mname.node_id m.mstep.step_locals
|
851
|
in
|
852
|
add_rule (idx :: uid :: vars)
|
853
|
(Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
|
854
|
|
855
|
(* Debug functions *)
|
856
|
(* let rec extract_expr_fds e = (* Format.eprintf "@[<v 2>Extracting fundecls
|
857
|
from expr %s@ " *) (* (Z3.Expr.to_string e); *)
|
858
|
|
859
|
(* Removing quantifier is there are some *) let e = (* I didn't found a nicer
|
860
|
way to do it than with an exception. My bad *) try let eq =
|
861
|
Z3.Quantifier.quantifier_of_expr e in let e2 = Z3.Quantifier.get_body eq in
|
862
|
(* Format.eprintf "Extracted quantifier body@ "; *) e2
|
863
|
|
864
|
with _ -> Format.eprintf "No quantifier info@ "; e in let _ = try ( let fd =
|
865
|
Z3.Expr.get_func_decl e in let fd_symbol = Z3.FuncDecl.get_name fd in let
|
866
|
fd_name = Z3.Symbol.to_string fd_symbol in if not (Hashtbl.mem decls fd_name)
|
867
|
then register_fdecl fd_name fd; (* Format.eprintf "fdecls (%s): %s@ " *) (*
|
868
|
fd_name *) (* (Z3.FuncDecl.to_string fd); *) try ( let args =
|
869
|
Z3.Expr.get_args e in (* Format.eprintf "@[<v>@ "; *) (* List.iter
|
870
|
extract_expr_fds args; *) (* Format.eprintf "@]@ "; *) () ) with _ ->
|
871
|
Format.eprintf "Impossible to extract fundecl args for expression %s@ "
|
872
|
(Z3.Expr.to_string e) ) with _ -> Format.eprintf "Impossible to extract
|
873
|
anything from expression %s@ " (Z3.Expr.to_string e) in (* Format.eprintf
|
874
|
"@]@ " *) () *)
|
875
|
(* Local Variables: *)
|
876
|
(* compile-command:"make -C ../.." *)
|
877
|
(* End: *)
|