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