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