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