1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
(* The compilation presented here was first defined in Garoche, Gurfinkel,
|
13
|
Kahsai, HCSV'14.
|
14
|
|
15
|
This is a modified version that handle reset *)
|
16
|
|
17
|
open Format
|
18
|
open Lustre_types
|
19
|
open Machine_code_types
|
20
|
open Corelang
|
21
|
open Machine_code_common
|
22
|
open Horn_backend_common
|
23
|
|
24
|
(********************************************************************************************)
|
25
|
(* Instruction Printing functions *)
|
26
|
(********************************************************************************************)
|
27
|
|
28
|
let pp_horn_var _ fmt id =
|
29
|
(*if Types.is_array_type id.var_type then assert false (* no arrays in Horn
|
30
|
output *) else*)
|
31
|
fprintf fmt "%s" id.var_id
|
32
|
|
33
|
(* Used to print boolean constants *)
|
34
|
let pp_horn_tag fmt t =
|
35
|
pp_print_string fmt
|
36
|
(if t = tag_true then "true" else if t = tag_false then "false" else t)
|
37
|
|
38
|
(* Prints a constant value *)
|
39
|
let pp_horn_const fmt c =
|
40
|
match c with
|
41
|
| Const_int i ->
|
42
|
pp_print_int fmt i
|
43
|
| Const_real r ->
|
44
|
Real.pp fmt r
|
45
|
| Const_tag t ->
|
46
|
pp_horn_tag fmt t
|
47
|
| _ ->
|
48
|
assert false
|
49
|
|
50
|
(* Default value for each type, used when building arrays. Eg integer array
|
51
|
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
|
52
|
for the type integer (arrays). *)
|
53
|
let rec pp_default_val fmt t =
|
54
|
let t = Types.dynamic_type t in
|
55
|
if Types.is_bool_type t then fprintf fmt "true"
|
56
|
else if Types.is_int_type t then fprintf fmt "0"
|
57
|
else if Types.is_real_type t then fprintf fmt "0"
|
58
|
else
|
59
|
match (Types.dynamic_type t).Types.tdesc with
|
60
|
| Types.Tarray _ ->
|
61
|
(* TODO PL: this strange code has to be (heavily) checked *)
|
62
|
let valt = Types.array_element_type t in
|
63
|
fprintf fmt "((as const (Array Int %a)) %a)" pp_type valt pp_default_val
|
64
|
valt
|
65
|
| Types.Tstruct _ ->
|
66
|
assert false
|
67
|
| Types.Ttuple _ ->
|
68
|
assert false
|
69
|
| _ ->
|
70
|
assert false
|
71
|
|
72
|
let pp_mod pp_val v1 v2 fmt =
|
73
|
if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then
|
74
|
(* C semantics: converting it from Euclidean operators (a mod_M b) - ((a
|
75
|
mod_M b > 0 && a < 0) ? abs(b) : 0) *)
|
76
|
Format.fprintf fmt
|
77
|
"(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))" pp_val
|
78
|
v1 pp_val v2 pp_val v1 pp_val v2 pp_val v1 pp_val v2
|
79
|
else Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
|
80
|
|
81
|
let pp_div pp_val v1 v2 fmt =
|
82
|
if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then
|
83
|
(* C semantics: converting it from Euclidean operators (a - (a mod_C b))
|
84
|
div_M b *)
|
85
|
Format.fprintf fmt "(div (- %a %t) %a)" pp_val v1 (pp_mod pp_val v1 v2)
|
86
|
pp_val v2
|
87
|
else Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
|
88
|
|
89
|
let pp_basic_lib_fun i pp_val fmt vl =
|
90
|
match i, vl with
|
91
|
| "ite", [ v1; v2; v3 ] ->
|
92
|
Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val
|
93
|
v3
|
94
|
| "uminus", [ v ] ->
|
95
|
Format.fprintf fmt "(- %a)" pp_val v
|
96
|
| "not", [ v ] ->
|
97
|
Format.fprintf fmt "(not %a)" pp_val v
|
98
|
| "=", [ v1; v2 ] ->
|
99
|
Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
|
100
|
| "&&", [ v1; v2 ] ->
|
101
|
Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
|
102
|
| "||", [ v1; v2 ] ->
|
103
|
Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
|
104
|
| "impl", [ v1; v2 ] ->
|
105
|
Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
|
106
|
| "equi", [ v1; v2 ] ->
|
107
|
Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
|
108
|
| "xor", [ v1; v2 ] ->
|
109
|
Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
|
110
|
| "!=", [ v1; v2 ] ->
|
111
|
Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
|
112
|
| "mod", [ v1; v2 ] ->
|
113
|
pp_mod pp_val v1 v2 fmt
|
114
|
| "/", [ v1; v2 ] ->
|
115
|
pp_div pp_val v1 v2 fmt
|
116
|
| _, [ v1; v2 ] ->
|
117
|
Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
|
118
|
| _ ->
|
119
|
Format.eprintf "internal error: Basic_library.pp_horn %s@." i;
|
120
|
assert false
|
121
|
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *)
|
122
|
|
123
|
(* Prints a value expression [v], with internal function calls only. [pp_var] is
|
124
|
a printer for variables (typically [pp_c_var_read]), but an offset suffix may
|
125
|
be added for array variables *)
|
126
|
let rec pp_horn_val ?(is_lhs = false) m self pp_var fmt v =
|
127
|
match v.value_desc with
|
128
|
| Cst c ->
|
129
|
pp_horn_const fmt c
|
130
|
(* Code specific for arrays *)
|
131
|
| Array il ->
|
132
|
(* An array definition: (store ( ... (store ( store ( default_val ) idx_n
|
133
|
val_n ) idx_n-1 val_n-1) ... idx_1 val_1 ) *)
|
134
|
let rec print fmt (tab, x) =
|
135
|
match tab with
|
136
|
| [] ->
|
137
|
pp_default_val fmt v.value_type (* (get_type v) *)
|
138
|
| h :: t ->
|
139
|
fprintf fmt "(store %a %i %a)" print
|
140
|
(t, x + 1)
|
141
|
x
|
142
|
(pp_horn_val ~is_lhs m self pp_var)
|
143
|
h
|
144
|
in
|
145
|
print fmt (il, 0)
|
146
|
| Access (tab, index) ->
|
147
|
fprintf fmt "(select %a %a)"
|
148
|
(pp_horn_val ~is_lhs m self pp_var)
|
149
|
tab
|
150
|
(pp_horn_val ~is_lhs m self pp_var)
|
151
|
index
|
152
|
(* Code specific for arrays *)
|
153
|
| Power _ ->
|
154
|
assert false
|
155
|
| Var v ->
|
156
|
if is_memory m v then
|
157
|
if Types.is_array_type v.var_type then assert false
|
158
|
else
|
159
|
pp_var fmt
|
160
|
(rename_machine self
|
161
|
((if is_lhs then rename_next else rename_current (* self *)) v))
|
162
|
else pp_var fmt (rename_machine self v)
|
163
|
| Fun (n, vl) ->
|
164
|
fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
|
165
|
| ResetFlag ->
|
166
|
(* TODO: handle reset flag *)
|
167
|
assert false
|
168
|
|
169
|
(* Prints a [value] indexed by the suffix list [loop_vars] *)
|
170
|
let rec pp_value_suffix m self pp_value fmt value =
|
171
|
match value.value_desc with
|
172
|
| Fun (n, vl) ->
|
173
|
pp_basic_lib_fun n (pp_value_suffix m self pp_value) fmt vl
|
174
|
| _ ->
|
175
|
pp_horn_val m self pp_value fmt value
|
176
|
|
177
|
(* type_directed assignment: array vs. statically sized type - [var_type]: type
|
178
|
of variable to be assigned - [var_name]: name of variable to be assigned -
|
179
|
[value]: assigned value - [pp_var]: printer for variables *)
|
180
|
let pp_assign m pp_var fmt var_name value =
|
181
|
let self = m.mname.node_id in
|
182
|
fprintf fmt "(= %a %a)"
|
183
|
(pp_horn_val ~is_lhs:true m self pp_var)
|
184
|
var_name
|
185
|
(pp_value_suffix m self pp_var)
|
186
|
value
|
187
|
|
188
|
(* In case of no reset call, we define mid_mem = current_mem *)
|
189
|
let pp_no_reset machines m fmt i =
|
190
|
let n, _ = List.assoc i m.minstances in
|
191
|
let target_machine =
|
192
|
List.find (fun m -> m.mname.node_id = node_name n) machines
|
193
|
in
|
194
|
|
195
|
let m_list =
|
196
|
rename_machine_list (concat m.mname.node_id i)
|
197
|
(rename_mid_list (full_memory_vars machines target_machine))
|
198
|
in
|
199
|
let c_list =
|
200
|
rename_machine_list (concat m.mname.node_id i)
|
201
|
(rename_current_list (full_memory_vars machines target_machine))
|
202
|
in
|
203
|
match c_list, m_list with
|
204
|
| [ chd ], [ mhd ] ->
|
205
|
fprintf fmt "(= %a %a)" (pp_horn_var m) mhd (pp_horn_var m) chd
|
206
|
| _ ->
|
207
|
fprintf fmt "@[<v 0>(and @[<v 0>";
|
208
|
List.iter2
|
209
|
(fun mhd chd ->
|
210
|
fprintf fmt "(= %a %a)@ " (pp_horn_var m) mhd (pp_horn_var m) chd)
|
211
|
m_list c_list;
|
212
|
fprintf fmt ")@]@ @]"
|
213
|
|
214
|
let pp_instance_reset machines m fmt i =
|
215
|
let n, _ = List.assoc i m.minstances in
|
216
|
let target_machine =
|
217
|
List.find (fun m -> m.mname.node_id = node_name n) machines
|
218
|
in
|
219
|
|
220
|
fprintf fmt "(%a @[<v 0>%a)@]" pp_machine_reset_name (node_name n)
|
221
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
222
|
(rename_machine_list (concat m.mname.node_id i)
|
223
|
(rename_current_list (full_memory_vars machines target_machine))
|
224
|
@ rename_machine_list (concat m.mname.node_id i)
|
225
|
(rename_mid_list (full_memory_vars machines target_machine)))
|
226
|
|
227
|
let pp_instance_call machines reset_instances m fmt i inputs outputs =
|
228
|
let self = m.mname.node_id in
|
229
|
try
|
230
|
(* stateful node instance *)
|
231
|
let n, _ = List.assoc i m.minstances in
|
232
|
let target_machine =
|
233
|
List.find (fun m -> m.mname.node_id = node_name n) machines
|
234
|
in
|
235
|
(* Checking whether this specific instances has been reset yet *)
|
236
|
if not (List.mem i reset_instances) then
|
237
|
(* If not, declare mem_m = mem_c *)
|
238
|
pp_no_reset machines m fmt i;
|
239
|
|
240
|
let mems = full_memory_vars machines target_machine in
|
241
|
let rename_mems f =
|
242
|
rename_machine_list (concat m.mname.node_id i) (f mems)
|
243
|
in
|
244
|
let mid_mems = rename_mems rename_mid_list in
|
245
|
let next_mems = rename_mems rename_next_list in
|
246
|
|
247
|
match node_name n, inputs, outputs, mid_mems, next_mems with
|
248
|
| "_arrow", [ i1; i2 ], [ o ], [ mem_m ], [ mem_x ] ->
|
249
|
fprintf fmt "@[<v 5>(and ";
|
250
|
fprintf fmt "(= %a (ite %a %a %a))"
|
251
|
(pp_horn_val ~is_lhs:true m self (pp_horn_var m))
|
252
|
(mk_val (Var o) o.var_type)
|
253
|
(* output var *)
|
254
|
(pp_horn_var m)
|
255
|
mem_m
|
256
|
(pp_horn_val m self (pp_horn_var m))
|
257
|
i1
|
258
|
(pp_horn_val m self (pp_horn_var m))
|
259
|
i2;
|
260
|
fprintf fmt "@ ";
|
261
|
fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
|
262
|
fprintf fmt ")@]"
|
263
|
| _ ->
|
264
|
fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" pp_machine_step_name (node_name n)
|
265
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
|
266
|
inputs
|
267
|
(Utils.pp_final_char_if_non_empty "@ " inputs)
|
268
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
|
269
|
(List.map (fun v -> mk_val (Var v) v.var_type) outputs)
|
270
|
(Utils.pp_final_char_if_non_empty "@ " outputs)
|
271
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
272
|
(mid_mems @ next_mems)
|
273
|
with Not_found ->
|
274
|
(* stateless node instance *)
|
275
|
let n, _ = List.assoc i m.mcalls in
|
276
|
fprintf fmt "(%a @[<v 0>%a%t%a)@]" pp_machine_stateless_name (node_name n)
|
277
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
|
278
|
inputs
|
279
|
(Utils.pp_final_char_if_non_empty "@ " inputs)
|
280
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
|
281
|
(List.map (fun v -> mk_val (Var v) v.var_type) outputs)
|
282
|
|
283
|
(* Print the instruction and update the set of reset instances *)
|
284
|
let rec pp_machine_instr machines reset_instances (m : machine_t) fmt instr :
|
285
|
ident list =
|
286
|
match get_instr_desc instr with
|
287
|
| MSpec _ | MComment _ ->
|
288
|
reset_instances
|
289
|
(* TODO: handle reset flag *)
|
290
|
| MResetAssign _ ->
|
291
|
reset_instances
|
292
|
(* TODO: handle clear_reset *)
|
293
|
| MClearReset ->
|
294
|
reset_instances
|
295
|
| MNoReset i ->
|
296
|
(* we assign middle_mem with mem_m. And declare i as reset *)
|
297
|
pp_no_reset machines m fmt i;
|
298
|
i :: reset_instances
|
299
|
| MSetReset i ->
|
300
|
(* we assign middle_mem with reset: reset(mem_m) *)
|
301
|
pp_instance_reset machines m fmt i;
|
302
|
i :: reset_instances
|
303
|
| MLocalAssign (i, v) ->
|
304
|
pp_assign m (pp_horn_var m) fmt (mk_val (Var i) i.var_type) v;
|
305
|
reset_instances
|
306
|
| MStateAssign (i, v) ->
|
307
|
pp_assign m (pp_horn_var m) fmt (mk_val (Var i) i.var_type) v;
|
308
|
reset_instances
|
309
|
| MStep ([ _ ], i, vl)
|
310
|
when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl)
|
311
|
->
|
312
|
assert false (* This should not happen anymore *)
|
313
|
| MStep (il, i, vl) ->
|
314
|
(* if reset instance, just print the call over mem_m , otherwise declare
|
315
|
mem_m = mem_c and print the call to mem_m *)
|
316
|
pp_instance_call machines reset_instances m fmt i vl il;
|
317
|
reset_instances
|
318
|
(* Since this instance call will only happen once, we don't have to update
|
319
|
reset_instances *)
|
320
|
| MBranch (g, hl) ->
|
321
|
(* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced
|
322
|
yet. Later, we will have to compare the reset_instances of each branch
|
323
|
and introduced the mem_m = mem_c for branches to do not address it while
|
324
|
other did. Am I clear ? *)
|
325
|
(* For each branch we obtain the logical encoding, and the information
|
326
|
whether a sub node has been reset or not. If a node has been reset in one
|
327
|
of the branch, then all others have to have the mem_m = mem_c statement. *)
|
328
|
let self = m.mname.node_id in
|
329
|
let pp_branch fmt (tag, instrs) =
|
330
|
fprintf fmt "@[<v 3>(or (not (= %a %a))@ "
|
331
|
(*"@[<v 3>(=> (= %a %s)@ "*)
|
332
|
(* Issues with some versions of Z3. It seems that => within Horn
|
333
|
predicate may cause trouble. I have hard time producing a MWE, so
|
334
|
I'll just keep the fix here as (not a) or b *)
|
335
|
(pp_horn_val m self (pp_horn_var m))
|
336
|
g pp_horn_tag tag;
|
337
|
let _ (* rs *) =
|
338
|
pp_machine_instrs machines reset_instances m fmt instrs
|
339
|
in
|
340
|
fprintf fmt "@])";
|
341
|
()
|
342
|
(* rs *)
|
343
|
in
|
344
|
pp_conj pp_branch fmt hl;
|
345
|
reset_instances
|
346
|
|
347
|
and pp_machine_instrs machines reset_instances m fmt instrs =
|
348
|
let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
|
349
|
match instrs with
|
350
|
| [ x ] ->
|
351
|
ppi reset_instances fmt x
|
352
|
| _ :: _ ->
|
353
|
fprintf fmt "(and @[<v 0>";
|
354
|
let rs =
|
355
|
List.fold_left
|
356
|
(fun rs i ->
|
357
|
let rs = ppi rs fmt i in
|
358
|
fprintf fmt "@ ";
|
359
|
rs)
|
360
|
reset_instances instrs
|
361
|
in
|
362
|
fprintf fmt "@])";
|
363
|
rs
|
364
|
| [] ->
|
365
|
fprintf fmt "true";
|
366
|
reset_instances
|
367
|
|
368
|
let pp_machine_reset machines fmt m =
|
369
|
let locals = local_memory_vars m in
|
370
|
fprintf fmt "@[<v 5>(and @ ";
|
371
|
|
372
|
(* print "x_m = x_c" for each local memory *)
|
373
|
(Utils.fprintf_list ~sep:"@ " (fun fmt v ->
|
374
|
fprintf fmt "(= %a %a)" (pp_horn_var m) (rename_mid v) (pp_horn_var m)
|
375
|
(rename_current v)))
|
376
|
fmt locals;
|
377
|
fprintf fmt "@ ";
|
378
|
|
379
|
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special
|
380
|
treatment for _arrow: _first = true *)
|
381
|
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
|
382
|
let name = node_name n in
|
383
|
if name = "_arrow" then
|
384
|
fprintf fmt "(= %s._arrow._first_m true)" (concat m.mname.node_id id)
|
385
|
else
|
386
|
let machine_n = get_machine machines name in
|
387
|
fprintf fmt "(%s_reset @[<hov 0>%a@])" name
|
388
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
389
|
(rename_machine_list
|
390
|
(concat m.mname.node_id id)
|
391
|
(reset_vars machines machine_n))))
|
392
|
fmt m.minstances;
|
393
|
|
394
|
fprintf fmt "@]@ )"
|
395
|
|
396
|
(**************************************************************)
|
397
|
|
398
|
(* Print the machine m: two functions: m_init and m_step - m_init is a predicate
|
399
|
over m memories - m_step is a predicate over old_memories, inputs,
|
400
|
new_memories, outputs We first declare all variables then the two /rules/. *)
|
401
|
let print_machine machines fmt m =
|
402
|
if m.mname.node_id = Arrow.arrow_id then (* We don't print arrow function *)
|
403
|
()
|
404
|
else (
|
405
|
fprintf fmt "; %s@." m.mname.node_id;
|
406
|
|
407
|
(* Printing variables *)
|
408
|
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
409
|
(inout_vars m
|
410
|
@ rename_current_list (full_memory_vars machines m)
|
411
|
@ rename_mid_list (full_memory_vars machines m)
|
412
|
@ rename_next_list (full_memory_vars machines m)
|
413
|
@ rename_machine_list m.mname.node_id m.mstep.step_locals);
|
414
|
pp_print_newline fmt ();
|
415
|
|
416
|
if is_stateless m then (
|
417
|
(* Declaring single predicate *)
|
418
|
fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
|
419
|
m.mname.node_id
|
420
|
(Utils.fprintf_list ~sep:" " pp_type)
|
421
|
(List.map (fun v -> v.var_type) (inout_vars m));
|
422
|
|
423
|
match m.mstep.step_asserts with
|
424
|
| [] ->
|
425
|
(* Rule for single predicate *)
|
426
|
fprintf fmt "; Stateless step rule @.";
|
427
|
fprintf fmt "@[<v 2>(rule (=> @ ";
|
428
|
ignore
|
429
|
(pp_machine_instrs machines []
|
430
|
(* No reset info for stateless nodes *) m fmt m.mstep.step_instrs);
|
431
|
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_stateless_name
|
432
|
m.mname.node_id
|
433
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
434
|
(inout_vars m)
|
435
|
| assertsl ->
|
436
|
let pp_val =
|
437
|
pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m)
|
438
|
in
|
439
|
|
440
|
fprintf fmt "; Stateless step rule with Assertions @.";
|
441
|
(*Rule for step*)
|
442
|
fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
|
443
|
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
|
444
|
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
|
445
|
assertsl pp_machine_stateless_name m.mname.node_id
|
446
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
447
|
(step_vars machines m))
|
448
|
else (
|
449
|
(* Declaring predicate *)
|
450
|
fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
|
451
|
m.mname.node_id
|
452
|
(Utils.fprintf_list ~sep:" " pp_type)
|
453
|
(List.map (fun v -> v.var_type) (reset_vars machines m));
|
454
|
|
455
|
fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name m.mname.node_id
|
456
|
(Utils.fprintf_list ~sep:" " pp_type)
|
457
|
(List.map (fun v -> v.var_type) (step_vars machines m));
|
458
|
|
459
|
pp_print_newline fmt ();
|
460
|
|
461
|
(* Rule for reset *)
|
462
|
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
|
463
|
(pp_machine_reset machines)
|
464
|
m pp_machine_reset_name m.mname.node_id
|
465
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
466
|
(reset_vars machines m);
|
467
|
|
468
|
match m.mstep.step_asserts with
|
469
|
| [] ->
|
470
|
fprintf fmt "; Step rule @.";
|
471
|
(* Rule for step*)
|
472
|
fprintf fmt "@[<v 2>(rule (=> @ ";
|
473
|
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
|
474
|
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name
|
475
|
m.mname.node_id
|
476
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
477
|
(step_vars machines m)
|
478
|
| assertsl ->
|
479
|
let pp_val =
|
480
|
pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m)
|
481
|
in
|
482
|
(* print_string pp_val; *)
|
483
|
fprintf fmt "; Step rule with Assertions @.";
|
484
|
|
485
|
(*Rule for step*)
|
486
|
fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
|
487
|
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
|
488
|
fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
|
489
|
assertsl pp_machine_step_name m.mname.node_id
|
490
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
491
|
(step_vars machines m)))
|
492
|
|
493
|
let mk_flags arity =
|
494
|
let b_range =
|
495
|
let rec range i j = if i > arity then [] else i :: range (i + 1) j in
|
496
|
range 2 arity
|
497
|
in
|
498
|
List.fold_left (fun acc _ -> acc ^ " false") "true" b_range
|
499
|
|
500
|
(*Get sfunction infos from command line*)
|
501
|
let get_sf_info () =
|
502
|
let splitted = Str.split (Str.regexp "@") !Options.sfunction in
|
503
|
Log.report ~level:1 (fun fmt ->
|
504
|
fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
|
505
|
let sf_name, flags, arity =
|
506
|
match splitted with
|
507
|
| [ h; flg; par ] ->
|
508
|
h, flg, par
|
509
|
| _ ->
|
510
|
failwith "Wrong Sfunction info"
|
511
|
in
|
512
|
|
513
|
Log.report ~level:1 (fun fmt ->
|
514
|
fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags
|
515
|
arity);
|
516
|
sf_name, flags, arity
|
517
|
|
518
|
(*a function to print the rules in case we have an s-function*)
|
519
|
let print_sfunction machines fmt m =
|
520
|
if m.mname.node_id = Arrow.arrow_id then (* We don't print arrow function *)
|
521
|
()
|
522
|
else (
|
523
|
Format.fprintf fmt "; SFUNCTION@.";
|
524
|
Format.fprintf fmt "; %s@." m.mname.node_id;
|
525
|
Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
|
526
|
|
527
|
(* Check if there is annotation for s-function *)
|
528
|
if m.mannot != [] then
|
529
|
Format.fprintf fmt "; @[%a@]@]@\n"
|
530
|
(Utils.fprintf_list ~sep:"@ " Printers.pp_s_function)
|
531
|
m.mannot;
|
532
|
|
533
|
(* Printing variables *)
|
534
|
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
535
|
(step_vars machines m
|
536
|
@ rename_machine_list m.mname.node_id m.mstep.step_locals);
|
537
|
Format.pp_print_newline fmt ();
|
538
|
let sf_name, flags, _ = get_sf_info () in
|
539
|
|
540
|
if is_stateless m then (
|
541
|
(* Declaring single predicate *)
|
542
|
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
|
543
|
m.mname.node_id
|
544
|
(Utils.fprintf_list ~sep:" " pp_type)
|
545
|
(List.map (fun v -> v.var_type) (reset_vars machines m));
|
546
|
Format.pp_print_newline fmt ();
|
547
|
(* Rule for single predicate *)
|
548
|
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
|
549
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
|
550
|
str_flags
|
551
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
552
|
(reset_vars machines m) pp_machine_stateless_name m.mname.node_id
|
553
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
554
|
(reset_vars machines m))
|
555
|
else (
|
556
|
(* Declaring predicate *)
|
557
|
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
|
558
|
m.mname.node_id
|
559
|
(Utils.fprintf_list ~sep:" " pp_type)
|
560
|
(List.map (fun v -> v.var_type) (inout_vars m));
|
561
|
|
562
|
Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name
|
563
|
m.mname.node_id
|
564
|
(Utils.fprintf_list ~sep:" " pp_type)
|
565
|
(List.map (fun v -> v.var_type) (step_vars machines m));
|
566
|
|
567
|
Format.pp_print_newline fmt ();
|
568
|
(* Adding assertions *)
|
569
|
match m.mstep.step_asserts with
|
570
|
| [] ->
|
571
|
(* Rule for step*)
|
572
|
fprintf fmt "@[<v 2>(rule (=> @ ";
|
573
|
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
|
574
|
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name
|
575
|
m.mname.node_id
|
576
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
577
|
(step_vars machines m)
|
578
|
| assertsl ->
|
579
|
let pp_val =
|
580
|
pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m)
|
581
|
in
|
582
|
(* print_string pp_val; *)
|
583
|
fprintf fmt "; with Assertions @.";
|
584
|
|
585
|
(*Rule for step*)
|
586
|
fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
|
587
|
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
|
588
|
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
|
589
|
pp_machine_step_name m.mname.node_id
|
590
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m))
|
591
|
(step_vars machines m)))
|
592
|
|
593
|
(**************** XML printing functions *************)
|
594
|
|
595
|
let rec pp_xml_expr fmt expr =
|
596
|
(match expr.expr_annot with
|
597
|
| None ->
|
598
|
fprintf fmt "%t"
|
599
|
| Some ann ->
|
600
|
fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann) (fun fmt ->
|
601
|
match expr.expr_desc with
|
602
|
| Expr_const c ->
|
603
|
Printers.pp_const fmt c
|
604
|
| Expr_ident id ->
|
605
|
fprintf fmt "%s" id
|
606
|
| Expr_array a ->
|
607
|
fprintf fmt "[%a]" pp_xml_tuple a
|
608
|
| Expr_access (a, d) ->
|
609
|
fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
|
610
|
| Expr_power (a, d) ->
|
611
|
fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
|
612
|
| Expr_tuple el ->
|
613
|
fprintf fmt "(%a)" pp_xml_tuple el
|
614
|
| Expr_ite (c, t, e) ->
|
615
|
fprintf fmt
|
616
|
"@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])"
|
617
|
pp_xml_expr c pp_xml_expr t pp_xml_expr e
|
618
|
| Expr_arrow (e1, e2) ->
|
619
|
fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2
|
620
|
| Expr_fby (e1, e2) ->
|
621
|
fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2
|
622
|
| Expr_pre e ->
|
623
|
fprintf fmt "pre %a" pp_xml_expr e
|
624
|
| Expr_when (e, id, l) ->
|
625
|
fprintf fmt "%a when %s(%s)" pp_xml_expr e l id
|
626
|
| Expr_merge (id, hl) ->
|
627
|
fprintf fmt "merge %s %a" id pp_xml_handlers hl
|
628
|
| Expr_appl (id, e, r) ->
|
629
|
pp_xml_app fmt id e r)
|
630
|
|
631
|
and pp_xml_tuple fmt el = Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
|
632
|
|
633
|
and pp_xml_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_xml_expr h
|
634
|
|
635
|
and pp_xml_handlers fmt hl = Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
|
636
|
|
637
|
and pp_xml_app fmt id e r =
|
638
|
match r with
|
639
|
| None ->
|
640
|
pp_xml_call fmt id e
|
641
|
| Some c ->
|
642
|
fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c
|
643
|
|
644
|
and pp_xml_call fmt id e =
|
645
|
match id, e.expr_desc with
|
646
|
| "+", Expr_tuple [ e1; e2 ] ->
|
647
|
fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2
|
648
|
| "uminus", _ ->
|
649
|
fprintf fmt "(- %a)" pp_xml_expr e
|
650
|
| "-", Expr_tuple [ e1; e2 ] ->
|
651
|
fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2
|
652
|
| "*", Expr_tuple [ e1; e2 ] ->
|
653
|
fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2
|
654
|
| "/", Expr_tuple [ e1; e2 ] ->
|
655
|
fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2
|
656
|
| "mod", Expr_tuple [ e1; e2 ] ->
|
657
|
fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2
|
658
|
| "&&", Expr_tuple [ e1; e2 ] ->
|
659
|
fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2
|
660
|
| "||", Expr_tuple [ e1; e2 ] ->
|
661
|
fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2
|
662
|
| "xor", Expr_tuple [ e1; e2 ] ->
|
663
|
fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2
|
664
|
| "impl", Expr_tuple [ e1; e2 ] ->
|
665
|
fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2
|
666
|
| "<", Expr_tuple [ e1; e2 ] ->
|
667
|
fprintf fmt "(%a < %a)" pp_xml_expr e1 pp_xml_expr e2
|
668
|
| "<=", Expr_tuple [ e1; e2 ] ->
|
669
|
fprintf fmt "(%a <= %a)" pp_xml_expr e1 pp_xml_expr e2
|
670
|
| ">", Expr_tuple [ e1; e2 ] ->
|
671
|
fprintf fmt "(%a > %a)" pp_xml_expr e1 pp_xml_expr e2
|
672
|
| ">=", Expr_tuple [ e1; e2 ] ->
|
673
|
fprintf fmt "(%a >= %a)" pp_xml_expr e1 pp_xml_expr e2
|
674
|
| "!=", Expr_tuple [ e1; e2 ] ->
|
675
|
fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2
|
676
|
| "=", Expr_tuple [ e1; e2 ] ->
|
677
|
fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2
|
678
|
| "not", _ ->
|
679
|
fprintf fmt "(not %a)" pp_xml_expr e
|
680
|
| _, Expr_tuple _ ->
|
681
|
fprintf fmt "%s %a" id pp_xml_expr e
|
682
|
| _ ->
|
683
|
fprintf fmt "%s (%a)" id pp_xml_expr e
|
684
|
|
685
|
and pp_xml_eexpr fmt e =
|
686
|
fprintf fmt "%a%t %a"
|
687
|
(Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers)
|
688
|
e.eexpr_quantifiers
|
689
|
(fun fmt ->
|
690
|
match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
|
691
|
pp_xml_expr e.eexpr_qfexpr
|
692
|
|
693
|
and pp_xml_sf_value fmt e =
|
694
|
fprintf fmt "%a"
|
695
|
(* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
|
696
|
(* (fun fmt -> match e.eexpr_quantifiers *)
|
697
|
(* with [] -> () *)
|
698
|
(* | _ -> fprintf fmt ";") *)
|
699
|
pp_xml_expr e.eexpr_qfexpr
|
700
|
|
701
|
and pp_xml_s_function fmt expr_ann =
|
702
|
let pp_xml_annot fmt (kwds, ee) =
|
703
|
Format.fprintf fmt " %t : %a"
|
704
|
(fun fmt ->
|
705
|
match kwds with
|
706
|
| [] ->
|
707
|
assert false
|
708
|
| [ x ] ->
|
709
|
Format.pp_print_string fmt x
|
710
|
| _ ->
|
711
|
Format.fprintf fmt "%a"
|
712
|
(Utils.fprintf_list ~sep:"/" Format.pp_print_string)
|
713
|
kwds)
|
714
|
pp_xml_sf_value ee
|
715
|
in
|
716
|
Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
|
717
|
|
718
|
and pp_xml_expr_annot fmt expr_ann =
|
719
|
let pp_xml_annot fmt (kwds, ee) =
|
720
|
Format.fprintf fmt "(*! %t: %a; *)"
|
721
|
(fun fmt ->
|
722
|
match kwds with
|
723
|
| [] ->
|
724
|
assert false
|
725
|
| [ x ] ->
|
726
|
Format.pp_print_string fmt x
|
727
|
| _ ->
|
728
|
Format.fprintf fmt "/%a/"
|
729
|
(Utils.fprintf_list ~sep:"/" Format.pp_print_string)
|
730
|
kwds)
|
731
|
pp_xml_eexpr ee
|
732
|
in
|
733
|
Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
|
734
|
|
735
|
(* Local Variables: *)
|
736
|
(* compile-command:"make -C ../../.." *)
|
737
|
(* End: *)
|