lustrec / src / backends / Horn / horn_backend_printers.ml @ 45f0f48d
History | View | Annotate | Download (13.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 LustreSpec |
20 |
open Corelang |
21 |
open Machine_code |
22 |
|
23 |
open Horn_backend_common |
24 |
|
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 |
(* Prints a value expression [v], with internal function calls only. |
50 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
51 |
but an offset suffix may be added for array variables |
52 |
*) |
53 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
54 |
match v.value_desc with |
55 |
| Cst c -> pp_horn_const fmt c |
56 |
| Array _ |
57 |
| Access _ -> assert false (* no arrays *) |
58 |
| Power (v, n) -> assert false |
59 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
60 |
| StateVar v -> |
61 |
if Types.is_array_type v.var_type |
62 |
then assert false |
63 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
64 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
65 |
|
66 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
67 |
let rec pp_value_suffix self pp_value fmt value = |
68 |
match value.value_desc with |
69 |
| Fun (n, vl) -> |
70 |
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl |
71 |
| _ -> |
72 |
pp_horn_val self pp_value fmt value |
73 |
|
74 |
(* type_directed assignment: array vs. statically sized type |
75 |
- [var_type]: type of variable to be assigned |
76 |
- [var_name]: name of variable to be assigned |
77 |
- [value]: assigned value |
78 |
- [pp_var]: printer for variables |
79 |
*) |
80 |
let pp_assign m pp_var fmt var_name value = |
81 |
let self = m.mname.node_id in |
82 |
fprintf fmt "(= %a %a)" |
83 |
(pp_horn_val ~is_lhs:true self pp_var) var_name |
84 |
(pp_value_suffix self pp_var) value |
85 |
|
86 |
|
87 |
(* In case of no reset call, we define mid_mem = current_mem *) |
88 |
let pp_no_reset machines m fmt i = |
89 |
let (n,_) = List.assoc i m.minstances in |
90 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
91 |
|
92 |
let m_list = |
93 |
rename_machine_list |
94 |
(concat m.mname.node_id i) |
95 |
(rename_mid_list (full_memory_vars machines target_machine)) |
96 |
in |
97 |
let c_list = |
98 |
rename_machine_list |
99 |
(concat m.mname.node_id i) |
100 |
(rename_current_list (full_memory_vars machines target_machine)) |
101 |
in |
102 |
match c_list, m_list with |
103 |
| [chd], [mhd] -> |
104 |
fprintf fmt "(= %a %a)" |
105 |
(pp_horn_var m) mhd |
106 |
(pp_horn_var m) chd |
107 |
|
108 |
| _ -> ( |
109 |
fprintf fmt "@[<v 0>(and @[<v 0>"; |
110 |
List.iter2 (fun mhd chd -> |
111 |
fprintf fmt "(= %a %a)@ " |
112 |
(pp_horn_var m) mhd |
113 |
(pp_horn_var m) chd |
114 |
) |
115 |
m_list |
116 |
c_list ; |
117 |
fprintf fmt ")@]@ @]" |
118 |
) |
119 |
|
120 |
let pp_instance_reset machines m fmt i = |
121 |
let (n,_) = List.assoc i m.minstances in |
122 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
123 |
|
124 |
fprintf fmt "(%a @[<v 0>%a)@]" |
125 |
pp_machine_reset_name (node_name n) |
126 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
127 |
( |
128 |
(rename_machine_list |
129 |
(concat m.mname.node_id i) |
130 |
(rename_current_list (full_memory_vars machines target_machine)) |
131 |
) |
132 |
@ |
133 |
(rename_machine_list |
134 |
(concat m.mname.node_id i) |
135 |
(rename_mid_list (full_memory_vars machines target_machine)) |
136 |
) |
137 |
) |
138 |
|
139 |
let pp_instance_call machines reset_instances m fmt i inputs outputs = |
140 |
let self = m.mname.node_id in |
141 |
try (* stateful node instance *) |
142 |
begin |
143 |
let (n,_) = List.assoc i m.minstances in |
144 |
let target_machine = List.find (fun m -> m.mname.node_id = node_name n) machines in |
145 |
(* Checking whether this specific instances has been reset yet *) |
146 |
if not (List.mem i reset_instances) then |
147 |
(* If not, declare mem_m = mem_c *) |
148 |
pp_no_reset machines m fmt i; |
149 |
|
150 |
let mems = full_memory_vars machines target_machine in |
151 |
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in |
152 |
let mid_mems = rename_mems rename_mid_list in |
153 |
let next_mems = rename_mems rename_next_list in |
154 |
|
155 |
match node_name n, inputs, outputs, mid_mems, next_mems with |
156 |
| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin |
157 |
fprintf fmt "@[<v 5>(and "; |
158 |
fprintf fmt "(= %a (ite %a %a %a))" |
159 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *) |
160 |
(pp_horn_var m) mem_m |
161 |
(pp_horn_val self (pp_horn_var m)) i1 |
162 |
(pp_horn_val self (pp_horn_var m)) i2 |
163 |
; |
164 |
fprintf fmt "@ "; |
165 |
fprintf fmt "(= %a false)" (pp_horn_var m) mem_x; |
166 |
fprintf fmt ")@]" |
167 |
end |
168 |
|
169 |
| node_name_n -> begin |
170 |
fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" |
171 |
pp_machine_step_name (node_name n) |
172 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs |
173 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
174 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
175 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
176 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
177 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems) |
178 |
|
179 |
end |
180 |
end |
181 |
with Not_found -> ( (* stateless node instance *) |
182 |
let (n,_) = List.assoc i m.mcalls in |
183 |
fprintf fmt "(%s @[<v 0>%a%t%a)@]" |
184 |
(node_name n) |
185 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
186 |
inputs |
187 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
188 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
189 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
190 |
) |
191 |
|
192 |
|
193 |
(* Print the instruction and update the set of reset instances *) |
194 |
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list = |
195 |
match instr with |
196 |
| MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *) |
197 |
pp_no_reset machines m fmt i; |
198 |
i::reset_instances |
199 |
| MReset i -> (* we assign middle_mem with reset: reset(mem_m) *) |
200 |
pp_instance_reset machines m fmt i; |
201 |
i::reset_instances |
202 |
| MLocalAssign (i,v) -> |
203 |
pp_assign |
204 |
m (pp_horn_var m) fmt |
205 |
(mk_val (LocalVar i) i.var_type) v; |
206 |
reset_instances |
207 |
| MStateAssign (i,v) -> |
208 |
pp_assign |
209 |
m (pp_horn_var m) fmt |
210 |
(mk_val (StateVar i) i.var_type) v; |
211 |
reset_instances |
212 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) -> |
213 |
assert false (* This should not happen anymore *) |
214 |
| MStep (il, i, vl) -> |
215 |
(* if reset instance, just print the call over mem_m , otherwise declare mem_m = |
216 |
mem_c and print the call to mem_m *) |
217 |
pp_instance_call machines reset_instances m fmt i vl il; |
218 |
reset_instances (* Since this instance call will only happen once, we |
219 |
don't have to update reset_instances *) |
220 |
|
221 |
| MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ... |
222 |
should not be produced yet. Later, we will have to |
223 |
compare the reset_instances of each branch and |
224 |
introduced the mem_m = mem_c for branches to do not |
225 |
address it while other did. Am I clear ? *) |
226 |
(* For each branch we obtain the logical encoding, and the information |
227 |
whether a sub node has been reset or not. If a node has been reset in one |
228 |
of the branch, then all others have to have the mem_m = mem_c |
229 |
statement. *) |
230 |
let self = m.mname.node_id in |
231 |
let pp_branch fmt (tag, instrs) = |
232 |
fprintf fmt |
233 |
"@[<v 3>(or (not (= %a %s))@ " |
234 |
(*"@[<v 3>(=> (= %a %s)@ "*) (* Issues with some versions of Z3. It |
235 |
seems that => within Horn predicate |
236 |
may cause trouble. I have hard time |
237 |
producing a MWE, so I'll just keep the |
238 |
fix here as (not a) or b *) |
239 |
(pp_horn_val self (pp_horn_var m)) g |
240 |
tag; |
241 |
let rs = pp_machine_instrs machines reset_instances m fmt instrs in |
242 |
fprintf fmt "@])"; |
243 |
() (* rs *) |
244 |
in |
245 |
pp_conj pp_branch fmt hl; |
246 |
reset_instances |
247 |
|
248 |
and pp_machine_instrs machines reset_instances m fmt instrs = |
249 |
let ppi rs fmt i = pp_machine_instr machines rs m fmt i in |
250 |
match instrs with |
251 |
| [x] -> ppi reset_instances fmt x |
252 |
| _::_ -> |
253 |
fprintf fmt "(and @[<v 0>"; |
254 |
let rs = List.fold_left (fun rs i -> |
255 |
let rs = ppi rs fmt i in |
256 |
fprintf fmt "@ "; |
257 |
rs |
258 |
) |
259 |
reset_instances instrs |
260 |
in |
261 |
fprintf fmt "@])"; |
262 |
rs |
263 |
|
264 |
| [] -> fprintf fmt "true"; reset_instances |
265 |
|
266 |
let pp_machine_reset machines fmt m = |
267 |
let locals = local_memory_vars machines m in |
268 |
fprintf fmt "@[<v 5>(and @ "; |
269 |
|
270 |
(* print "x_m = x_c" for each local memory *) |
271 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v -> |
272 |
fprintf fmt "(= %a %a)" |
273 |
(pp_horn_var m) (rename_mid v) |
274 |
(pp_horn_var m) (rename_current v) |
275 |
)) fmt locals; |
276 |
fprintf fmt "@ "; |
277 |
|
278 |
(* print "child_reset ( associated vars _ {c,m} )" for each subnode. |
279 |
Special treatment for _arrow: _first = true |
280 |
*) |
281 |
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) -> |
282 |
let name = node_name n in |
283 |
if name = "_arrow" then ( |
284 |
fprintf fmt "(= %s._arrow._first_m true)" |
285 |
(concat m.mname.node_id id) |
286 |
) else ( |
287 |
let machine_n = get_machine machines name in |
288 |
fprintf fmt "(%s_reset @[<hov 0>%a@])" |
289 |
name |
290 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
291 |
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) |
292 |
) |
293 |
)) fmt m.minstances; |
294 |
|
295 |
fprintf fmt "@]@ )" |
296 |
|
297 |
|
298 |
|
299 |
(**************************************************************) |
300 |
|
301 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
302 |
|
303 |
(* Print the machine m: |
304 |
two functions: m_init and m_step |
305 |
- m_init is a predicate over m memories |
306 |
- m_step is a predicate over old_memories, inputs, new_memories, outputs |
307 |
We first declare all variables then the two /rules/. |
308 |
*) |
309 |
let print_machine machines fmt m = |
310 |
if m.mname.node_id = arrow_id then |
311 |
(* We don't print arrow function *) |
312 |
() |
313 |
else |
314 |
begin |
315 |
fprintf fmt "; %s@." m.mname.node_id; |
316 |
|
317 |
(* Printing variables *) |
318 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
319 |
( |
320 |
(inout_vars machines m)@ |
321 |
(rename_current_list (full_memory_vars machines m)) @ |
322 |
(rename_mid_list (full_memory_vars machines m)) @ |
323 |
(rename_next_list (full_memory_vars machines m)) @ |
324 |
(rename_machine_list m.mname.node_id m.mstep.step_locals) |
325 |
); |
326 |
pp_print_newline fmt (); |
327 |
|
328 |
if is_stateless m then |
329 |
begin |
330 |
(* Declaring single predicate *) |
331 |
fprintf fmt "(declare-rel %a (%a))@." |
332 |
pp_machine_stateless_name m.mname.node_id |
333 |
(Utils.fprintf_list ~sep:" " pp_type) |
334 |
(List.map (fun v -> v.var_type) (inout_vars machines m)); |
335 |
|
336 |
(* Rule for single predicate *) |
337 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
338 |
ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs); |
339 |
fprintf fmt "@ (%a %a)@]@.))@.@." |
340 |
pp_machine_stateless_name m.mname.node_id |
341 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m); |
342 |
end |
343 |
else |
344 |
begin |
345 |
(* Declaring predicate *) |
346 |
fprintf fmt "(declare-rel %a (%a))@." |
347 |
pp_machine_reset_name m.mname.node_id |
348 |
(Utils.fprintf_list ~sep:" " pp_type) |
349 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
350 |
|
351 |
fprintf fmt "(declare-rel %a (%a))@." |
352 |
pp_machine_step_name m.mname.node_id |
353 |
(Utils.fprintf_list ~sep:" " pp_type) |
354 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
355 |
|
356 |
pp_print_newline fmt (); |
357 |
|
358 |
(* Rule for reset *) |
359 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
360 |
(pp_machine_reset machines) m |
361 |
pp_machine_reset_name m.mname.node_id |
362 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m); |
363 |
|
364 |
match m.mstep.step_asserts with |
365 |
| [] -> |
366 |
begin |
367 |
|
368 |
(* Rule for step*) |
369 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
370 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
371 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
372 |
pp_machine_step_name m.mname.node_id |
373 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
374 |
end |
375 |
| assertsl -> |
376 |
begin |
377 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
378 |
(* print_string pp_val; *) |
379 |
fprintf fmt "; with Assertions @."; |
380 |
|
381 |
(*Rule for step*) |
382 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
383 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
384 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
385 |
pp_machine_step_name m.mname.node_id |
386 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
387 |
end |
388 |
|
389 |
|
390 |
end |
391 |
end |
392 |
|
393 |
|
394 |
(* Local Variables: *) |
395 |
(* compile-command:"make -C ../../.." *) |
396 |
(* End: *) |