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