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
|
match (Types.dynamic_type t).Types.tdesc with
|
100
|
| Types.Tint -> fprintf fmt "0"
|
101
|
| Types.Treal -> fprintf fmt "0"
|
102
|
| Types.Tbool -> fprintf fmt "true"
|
103
|
| Types.Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
|
104
|
let valt = Types.array_element_type t in
|
105
|
fprintf fmt "((as const (Array Int %a)) %a)"
|
106
|
pp_type valt
|
107
|
pp_default_val valt
|
108
|
| Types.Tstruct(l) -> assert false
|
109
|
| Types.Ttuple(l) -> assert false
|
110
|
|_ -> assert false
|
111
|
|
112
|
|
113
|
(* Prints a value expression [v], with internal function calls only.
|
114
|
[pp_var] is a printer for variables (typically [pp_c_var_read]),
|
115
|
but an offset suffix may be added for array variables
|
116
|
*)
|
117
|
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
|
118
|
match v.value_desc with
|
119
|
| Cst c -> pp_horn_const fmt c
|
120
|
|
121
|
(* Code specific for arrays *)
|
122
|
| Array il ->
|
123
|
(* An array definition:
|
124
|
(store (
|
125
|
...
|
126
|
(store (
|
127
|
store (
|
128
|
default_val
|
129
|
)
|
130
|
idx_n val_n
|
131
|
)
|
132
|
idx_n-1 val_n-1)
|
133
|
...
|
134
|
idx_1 val_1
|
135
|
) *)
|
136
|
let rec print fmt (tab, x) =
|
137
|
match tab with
|
138
|
| [] -> pp_default_val fmt v.value_type(* (get_type v) *)
|
139
|
| h::t ->
|
140
|
fprintf fmt "(store %a %i %a)"
|
141
|
print (t, (x+1))
|
142
|
x
|
143
|
(pp_horn_val ~is_lhs:is_lhs self pp_var) h
|
144
|
in
|
145
|
print fmt (il, 0)
|
146
|
|
147
|
| Access(tab,index) ->
|
148
|
fprintf fmt "(select %a %a)"
|
149
|
(pp_horn_val ~is_lhs:is_lhs self pp_var) tab
|
150
|
(pp_horn_val ~is_lhs:is_lhs self pp_var) index
|
151
|
|
152
|
(* Code specific for arrays *)
|
153
|
|
154
|
| Power (v, n) -> assert false
|
155
|
| LocalVar v -> pp_var fmt (rename_machine self v)
|
156
|
| StateVar v ->
|
157
|
if Types.is_array_type v.var_type
|
158
|
then assert false
|
159
|
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
|
160
|
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
|
161
|
|
162
|
(* Prints a [value] indexed by the suffix list [loop_vars] *)
|
163
|
let rec pp_value_suffix self pp_value fmt value =
|
164
|
match value.value_desc with
|
165
|
| Fun (n, vl) ->
|
166
|
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
|
167
|
| _ ->
|
168
|
pp_horn_val self pp_value fmt value
|
169
|
|
170
|
(* type_directed assignment: array vs. statically sized type
|
171
|
- [var_type]: type of variable to be assigned
|
172
|
- [var_name]: name of variable to be assigned
|
173
|
- [value]: assigned value
|
174
|
- [pp_var]: printer for variables
|
175
|
*)
|
176
|
let pp_assign m pp_var fmt var_name value =
|
177
|
let self = m.mname.node_id in
|
178
|
fprintf fmt "(= %a %a)"
|
179
|
(pp_horn_val ~is_lhs:true self pp_var) var_name
|
180
|
(pp_value_suffix self pp_var) value
|
181
|
|
182
|
|
183
|
(* In case of no reset call, we define mid_mem = current_mem *)
|
184
|
let pp_no_reset machines m fmt i =
|
185
|
let (n,_) = List.assoc i m.minstances in
|
186
|
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in
|
187
|
|
188
|
let m_list =
|
189
|
rename_machine_list
|
190
|
(concat m.mname.node_id i)
|
191
|
(rename_mid_list (full_memory_vars machines target_machine))
|
192
|
in
|
193
|
let c_list =
|
194
|
rename_machine_list
|
195
|
(concat m.mname.node_id i)
|
196
|
(rename_current_list (full_memory_vars machines target_machine))
|
197
|
in
|
198
|
match c_list, m_list with
|
199
|
| [chd], [mhd] ->
|
200
|
fprintf fmt "(= %a %a)"
|
201
|
(pp_horn_var m) mhd
|
202
|
(pp_horn_var m) chd
|
203
|
|
204
|
| _ -> (
|
205
|
fprintf fmt "@[<v 0>(and @[<v 0>";
|
206
|
List.iter2 (fun mhd chd ->
|
207
|
fprintf fmt "(= %a %a)@ "
|
208
|
(pp_horn_var m) mhd
|
209
|
(pp_horn_var m) chd
|
210
|
)
|
211
|
m_list
|
212
|
c_list ;
|
213
|
fprintf fmt ")@]@ @]"
|
214
|
)
|
215
|
|
216
|
let pp_instance_reset machines m fmt i =
|
217
|
let (n,_) = List.assoc i m.minstances in
|
218
|
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in
|
219
|
|
220
|
fprintf fmt "(%a @[<v 0>%a)@]"
|
221
|
pp_machine_reset_name (node_name n)
|
222
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
223
|
(
|
224
|
(rename_machine_list
|
225
|
(concat m.mname.node_id i)
|
226
|
(rename_current_list (full_memory_vars machines target_machine))
|
227
|
)
|
228
|
@
|
229
|
(rename_machine_list
|
230
|
(concat m.mname.node_id i)
|
231
|
(rename_mid_list (full_memory_vars machines target_machine))
|
232
|
)
|
233
|
)
|
234
|
|
235
|
let pp_instance_call machines reset_instances m fmt i inputs outputs =
|
236
|
let self = m.mname.node_id in
|
237
|
try (* stateful node instance *)
|
238
|
begin
|
239
|
let (n,_) = List.assoc i m.minstances in
|
240
|
let target_machine = List.find (fun m -> m.mname.node_id = node_name n) machines in
|
241
|
(* Checking whether this specific instances has been reset yet *)
|
242
|
if not (List.mem i reset_instances) then
|
243
|
(* If not, declare mem_m = mem_c *)
|
244
|
pp_no_reset machines m fmt i;
|
245
|
|
246
|
let mems = full_memory_vars machines target_machine in
|
247
|
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
|
248
|
let mid_mems = rename_mems rename_mid_list in
|
249
|
let next_mems = rename_mems rename_next_list in
|
250
|
|
251
|
match node_name n, inputs, outputs, mid_mems, next_mems with
|
252
|
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
|
253
|
fprintf fmt "@[<v 5>(and ";
|
254
|
fprintf fmt "(= %a (ite %a %a %a))"
|
255
|
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
|
256
|
(pp_horn_var m) mem_m
|
257
|
(pp_horn_val self (pp_horn_var m)) i1
|
258
|
(pp_horn_val self (pp_horn_var m)) i2
|
259
|
;
|
260
|
fprintf fmt "@ ";
|
261
|
fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
|
262
|
fprintf fmt ")@]"
|
263
|
end
|
264
|
|
265
|
| node_name_n -> begin
|
266
|
fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
|
267
|
pp_machine_step_name (node_name n)
|
268
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
|
269
|
(Utils.pp_final_char_if_non_empty "@ " inputs)
|
270
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
|
271
|
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
|
272
|
(Utils.pp_final_char_if_non_empty "@ " outputs)
|
273
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
|
274
|
|
275
|
end
|
276
|
end
|
277
|
with Not_found -> ( (* stateless node instance *)
|
278
|
let (n,_) = List.assoc i m.mcalls in
|
279
|
fprintf fmt "(%s @[<v 0>%a%t%a)@]"
|
280
|
(node_name n)
|
281
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
|
282
|
inputs
|
283
|
(Utils.pp_final_char_if_non_empty "@ " inputs)
|
284
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
|
285
|
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
|
286
|
)
|
287
|
|
288
|
|
289
|
(* Print the instruction and update the set of reset instances *)
|
290
|
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
|
291
|
match instr with
|
292
|
| MComment _ -> reset_instances
|
293
|
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
|
294
|
pp_no_reset machines m fmt i;
|
295
|
i::reset_instances
|
296
|
| MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
|
297
|
pp_instance_reset machines m fmt i;
|
298
|
i::reset_instances
|
299
|
| MLocalAssign (i,v) ->
|
300
|
pp_assign
|
301
|
m (pp_horn_var m) fmt
|
302
|
(mk_val (LocalVar i) i.var_type) v;
|
303
|
reset_instances
|
304
|
| MStateAssign (i,v) ->
|
305
|
pp_assign
|
306
|
m (pp_horn_var m) fmt
|
307
|
(mk_val (StateVar i) i.var_type) v;
|
308
|
reset_instances
|
309
|
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
|
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 mem_m =
|
313
|
mem_c and print the call to mem_m *)
|
314
|
pp_instance_call machines reset_instances m fmt i vl il;
|
315
|
reset_instances (* Since this instance call will only happen once, we
|
316
|
don't have to update reset_instances *)
|
317
|
|
318
|
| MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
|
319
|
should not be produced yet. Later, we will have to
|
320
|
compare the reset_instances of each branch and
|
321
|
introduced the mem_m = mem_c for branches to do not
|
322
|
address it while 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
|
326
|
statement. *)
|
327
|
let self = m.mname.node_id in
|
328
|
let pp_branch fmt (tag, instrs) =
|
329
|
fprintf fmt
|
330
|
"@[<v 3>(or (not (= %a %s))@ "
|
331
|
(*"@[<v 3>(=> (= %a %s)@ "*) (* Issues with some versions of Z3. It
|
332
|
seems that => within Horn predicate
|
333
|
may cause trouble. I have hard time
|
334
|
producing a MWE, so I'll just keep the
|
335
|
fix here as (not a) or b *)
|
336
|
(pp_horn_val self (pp_horn_var m)) g
|
337
|
tag;
|
338
|
let _ (* rs *) = pp_machine_instrs machines reset_instances m fmt instrs in
|
339
|
fprintf fmt "@])";
|
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] -> ppi reset_instances fmt x
|
349
|
| _::_ ->
|
350
|
fprintf fmt "(and @[<v 0>";
|
351
|
let rs = List.fold_left (fun rs i ->
|
352
|
let rs = ppi rs fmt i in
|
353
|
fprintf fmt "@ ";
|
354
|
rs
|
355
|
)
|
356
|
reset_instances instrs
|
357
|
in
|
358
|
fprintf fmt "@])";
|
359
|
rs
|
360
|
|
361
|
| [] -> fprintf fmt "true"; reset_instances
|
362
|
|
363
|
let pp_machine_reset machines fmt m =
|
364
|
let locals = local_memory_vars machines m in
|
365
|
fprintf fmt "@[<v 5>(and @ ";
|
366
|
|
367
|
(* print "x_m = x_c" for each local memory *)
|
368
|
(Utils.fprintf_list ~sep:"@ " (fun fmt v ->
|
369
|
fprintf fmt "(= %a %a)"
|
370
|
(pp_horn_var m) (rename_mid v)
|
371
|
(pp_horn_var m) (rename_current v)
|
372
|
)) fmt locals;
|
373
|
fprintf fmt "@ ";
|
374
|
|
375
|
(* print "child_reset ( associated vars _ {c,m} )" for each subnode.
|
376
|
Special treatment for _arrow: _first = true
|
377
|
*)
|
378
|
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
|
379
|
let name = node_name n in
|
380
|
if name = "_arrow" then (
|
381
|
fprintf fmt "(= %s._arrow._first_m true)"
|
382
|
(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@])"
|
386
|
name
|
387
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
388
|
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
|
389
|
)
|
390
|
)) fmt m.minstances;
|
391
|
|
392
|
fprintf fmt "@]@ )"
|
393
|
|
394
|
|
395
|
|
396
|
(**************************************************************)
|
397
|
|
398
|
let is_stateless m = m.minstances = [] && m.mmemory = []
|
399
|
|
400
|
(* Print the machine m:
|
401
|
two functions: m_init and m_step
|
402
|
- m_init is a predicate over m memories
|
403
|
- m_step is a predicate over old_memories, inputs, new_memories, outputs
|
404
|
We first declare all variables then the two /rules/.
|
405
|
*)
|
406
|
let print_machine machines fmt m =
|
407
|
if m.mname.node_id = arrow_id then
|
408
|
(* We don't print arrow function *)
|
409
|
()
|
410
|
else
|
411
|
begin
|
412
|
fprintf fmt "; %s@." m.mname.node_id;
|
413
|
|
414
|
(* Printing variables *)
|
415
|
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
416
|
(
|
417
|
(inout_vars machines m)@
|
418
|
(rename_current_list (full_memory_vars machines m)) @
|
419
|
(rename_mid_list (full_memory_vars machines m)) @
|
420
|
(rename_next_list (full_memory_vars machines m)) @
|
421
|
(rename_machine_list m.mname.node_id m.mstep.step_locals)
|
422
|
);
|
423
|
pp_print_newline fmt ();
|
424
|
|
425
|
if is_stateless m then
|
426
|
begin
|
427
|
(* Declaring single predicate *)
|
428
|
fprintf fmt "(declare-rel %a (%a))@."
|
429
|
pp_machine_stateless_name m.mname.node_id
|
430
|
(Utils.fprintf_list ~sep:" " pp_type)
|
431
|
(List.map (fun v -> v.var_type) (inout_vars machines m));
|
432
|
|
433
|
(* Rule for single predicate *)
|
434
|
fprintf fmt "@[<v 2>(rule (=> @ ";
|
435
|
ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs);
|
436
|
fprintf fmt "@ (%a %a)@]@.))@.@."
|
437
|
pp_machine_stateless_name m.mname.node_id
|
438
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
|
439
|
end
|
440
|
else
|
441
|
begin
|
442
|
(* Declaring predicate *)
|
443
|
fprintf fmt "(declare-rel %a (%a))@."
|
444
|
pp_machine_reset_name m.mname.node_id
|
445
|
(Utils.fprintf_list ~sep:" " pp_type)
|
446
|
(List.map (fun v -> v.var_type) (reset_vars machines m));
|
447
|
|
448
|
fprintf fmt "(declare-rel %a (%a))@."
|
449
|
pp_machine_step_name m.mname.node_id
|
450
|
(Utils.fprintf_list ~sep:" " pp_type)
|
451
|
(List.map (fun v -> v.var_type) (step_vars machines m));
|
452
|
|
453
|
pp_print_newline fmt ();
|
454
|
|
455
|
(* Rule for reset *)
|
456
|
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
|
457
|
(pp_machine_reset machines) m
|
458
|
pp_machine_reset_name m.mname.node_id
|
459
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
|
460
|
|
461
|
match m.mstep.step_asserts with
|
462
|
| [] ->
|
463
|
begin
|
464
|
|
465
|
(* Rule for step*)
|
466
|
fprintf fmt "@[<v 2>(rule (=> @ ";
|
467
|
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
|
468
|
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
|
469
|
pp_machine_step_name m.mname.node_id
|
470
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
|
471
|
end
|
472
|
| assertsl ->
|
473
|
begin
|
474
|
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
|
475
|
(* print_string pp_val; *)
|
476
|
fprintf fmt "; with Assertions @.";
|
477
|
|
478
|
(*Rule for step*)
|
479
|
fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
|
480
|
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
|
481
|
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
|
482
|
pp_machine_step_name m.mname.node_id
|
483
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
|
484
|
end
|
485
|
|
486
|
|
487
|
end
|
488
|
end
|
489
|
|
490
|
|
491
|
let mk_flags arity =
|
492
|
let b_range =
|
493
|
let rec range i j =
|
494
|
if i > arity then [] else i :: (range (i+1) j) in
|
495
|
range 2 arity;
|
496
|
in
|
497
|
List.fold_left (fun acc x -> acc ^ " false") "true" b_range
|
498
|
|
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 -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
|
504
|
let sf_name, flags, arity = match splitted with
|
505
|
[h;flg;par] -> h, flg, par
|
506
|
| _ -> failwith "Wrong Sfunction info"
|
507
|
|
508
|
in
|
509
|
Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
|
510
|
sf_name, flags, arity
|
511
|
|
512
|
|
513
|
(*a function to print the rules in case we have an s-function*)
|
514
|
let print_sfunction machines fmt m =
|
515
|
if m.mname.node_id = arrow_id then
|
516
|
(* We don't print arrow function *)
|
517
|
()
|
518
|
else
|
519
|
begin
|
520
|
Format.fprintf fmt "; SFUNCTION@.";
|
521
|
Format.fprintf fmt "; %s@." m.mname.node_id;
|
522
|
Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
|
523
|
|
524
|
(* Check if there is annotation for s-function *)
|
525
|
if m.mannot != [] then(
|
526
|
Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
|
527
|
);
|
528
|
|
529
|
(* Printing variables *)
|
530
|
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
|
531
|
((step_vars machines m)@
|
532
|
(rename_machine_list m.mname.node_id m.mstep.step_locals));
|
533
|
Format.pp_print_newline fmt ();
|
534
|
let sf_name, flags, arity = get_sf_info() in
|
535
|
|
536
|
if is_stateless m then
|
537
|
begin
|
538
|
(* Declaring single predicate *)
|
539
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
540
|
pp_machine_stateless_name m.mname.node_id
|
541
|
(Utils.fprintf_list ~sep:" " pp_type)
|
542
|
(List.map (fun v -> v.var_type) (reset_vars machines m));
|
543
|
Format.pp_print_newline fmt ();
|
544
|
(* Rule for single predicate *)
|
545
|
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
|
546
|
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
|
547
|
str_flags
|
548
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m)
|
549
|
pp_machine_stateless_name m.mname.node_id
|
550
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m);
|
551
|
end
|
552
|
else
|
553
|
begin
|
554
|
(* Declaring predicate *)
|
555
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
556
|
pp_machine_reset_name m.mname.node_id
|
557
|
(Utils.fprintf_list ~sep:" " pp_type)
|
558
|
(List.map (fun v -> v.var_type) (inout_vars machines m));
|
559
|
|
560
|
Format.fprintf fmt "(declare-rel %a (%a))@."
|
561
|
pp_machine_step_name m.mname.node_id
|
562
|
(Utils.fprintf_list ~sep:" " 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
|
begin
|
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)@]@]@.))@.@."
|
575
|
pp_machine_step_name m.mname.node_id
|
576
|
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
|
577
|
end
|
578
|
| assertsl ->
|
579
|
begin
|
580
|
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
|
581
|
(* print_string pp_val; *)
|
582
|
fprintf fmt "; with Assertions @.";
|
583
|
|
584
|
(*Rule for step*)
|
585
|
fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
|
586
|
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
|
587
|
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
|
588
|
pp_machine_step_name m.mname.node_id
|
589
|
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
|
590
|
end
|
591
|
|
592
|
end
|
593
|
|
594
|
end
|
595
|
(* Local Variables: *)
|
596
|
(* compile-command:"make -C ../../.." *)
|
597
|
(* End: *)
|