lustrec / src / horn_backend.ml @ 587cdc0d
History | View | Annotate | Download (14.6 KB)
1 |
open Format |
---|---|
2 |
open LustreSpec |
3 |
open Corelang |
4 |
open Machine_code |
5 |
|
6 |
|
7 |
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id |
8 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
9 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id |
10 |
|
11 |
let pp_type fmt t = |
12 |
match (Types.repr t).Types.tdesc with |
13 |
| Types.Tbool -> Format.fprintf fmt "Bool" |
14 |
| Types.Tint -> Format.fprintf fmt "Int" |
15 |
| Types.Treal -> Format.fprintf fmt "Real" |
16 |
| Types.Tclock _ |
17 |
| Types.Tarray _ |
18 |
| Types.Tstatic _ |
19 |
| Types.Tconst _ |
20 |
| Types.Tarrow _ |
21 |
| _ -> Format.eprintf "internal error: pp_type %a@." |
22 |
Types.print_ty t; assert false |
23 |
|
24 |
|
25 |
let pp_decl_var fmt id = |
26 |
Format.fprintf fmt "(declare-var %s %a)" |
27 |
id.var_id |
28 |
pp_type id.var_type |
29 |
|
30 |
let pp_var fmt id = Format.pp_print_string fmt id.var_id |
31 |
|
32 |
|
33 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
34 |
let rename f = (fun v -> {v with var_id = f v.var_id } ) |
35 |
let rename_machine p = rename (fun n -> concat p n) |
36 |
let rename_machine_list p = List.map (rename_machine p) |
37 |
|
38 |
let rename_current = rename (fun n -> n ^ "_c") |
39 |
let rename_current_list = List.map rename_current |
40 |
let rename_next = rename (fun n -> n ^ "_x") |
41 |
let rename_next_list = List.map rename_next |
42 |
|
43 |
|
44 |
let get_machine machines node_name = |
45 |
List.find (fun m -> m.mname.node_id = node_name) machines |
46 |
|
47 |
let full_memory_vars machines machine = |
48 |
let rec aux fst prefix m = |
49 |
(rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @ |
50 |
List.fold_left (fun accu (id, (n, _)) -> |
51 |
let name = node_name n in |
52 |
if name = "_arrow" then accu else |
53 |
let machine_n = get_machine machines name in |
54 |
( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu |
55 |
) [] (m.minstances) |
56 |
in |
57 |
aux true machine.mname.node_id machine |
58 |
|
59 |
let stateless_vars machines m = |
60 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
61 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs) |
62 |
|
63 |
let step_vars machines m = |
64 |
(stateless_vars machines m)@ |
65 |
(rename_current_list (full_memory_vars machines m)) @ |
66 |
(rename_next_list (full_memory_vars machines m)) |
67 |
|
68 |
let init_vars machines m = |
69 |
(stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m)) |
70 |
|
71 |
(********************************************************************************************) |
72 |
(* Instruction Printing functions *) |
73 |
(********************************************************************************************) |
74 |
|
75 |
let pp_horn_var m fmt id = |
76 |
if Types.is_array_type id.var_type |
77 |
then |
78 |
assert false (* no arrays in Horn output *) |
79 |
else |
80 |
Format.fprintf fmt "%s" id.var_id |
81 |
|
82 |
|
83 |
(* Used to print boolean constants *) |
84 |
let pp_horn_tag fmt t = |
85 |
pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t) |
86 |
|
87 |
(* Prints a constant value *) |
88 |
let rec pp_horn_const fmt c = |
89 |
match c with |
90 |
| Const_int i -> pp_print_int fmt i |
91 |
| Const_real r -> pp_print_string fmt r |
92 |
| Const_float r -> pp_print_float fmt r |
93 |
| Const_tag t -> pp_horn_tag fmt t |
94 |
| _ -> assert false |
95 |
|
96 |
(* Prints a value expression [v], with internal function calls only. |
97 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
98 |
but an offset suffix may be added for array variables |
99 |
*) |
100 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
101 |
match v with |
102 |
| Cst c -> pp_horn_const fmt c |
103 |
| Array _ |
104 |
| Access _ -> assert false (* no arrays *) |
105 |
| Power (v, n) -> assert false |
106 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
107 |
| StateVar v -> |
108 |
if Types.is_array_type v.var_type |
109 |
then assert false |
110 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
111 |
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
112 |
|
113 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
114 |
let rec pp_value_suffix self pp_value fmt value = |
115 |
match value with |
116 |
| Fun (n, vl) -> |
117 |
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl |
118 |
| _ -> |
119 |
pp_horn_val self pp_value fmt value |
120 |
|
121 |
(* type_directed assignment: array vs. statically sized type |
122 |
- [var_type]: type of variable to be assigned |
123 |
- [var_name]: name of variable to be assigned |
124 |
- [value]: assigned value |
125 |
- [pp_var]: printer for variables |
126 |
*) |
127 |
let pp_assign m self pp_var fmt var_type var_name value = |
128 |
fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value |
129 |
|
130 |
let pp_instance_call |
131 |
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) = |
132 |
try (* stateful node instance *) |
133 |
begin |
134 |
let (n,_) = List.assoc i m.minstances in |
135 |
match node_name n, inputs, outputs with |
136 |
| "_arrow", [i1; i2], [o] -> begin |
137 |
if init then |
138 |
pp_assign |
139 |
m |
140 |
self |
141 |
(pp_horn_var m) |
142 |
(* (pp_horn_val self (pp_horn_var m) fmt o) *) |
143 |
fmt |
144 |
o.var_type (LocalVar o) i1 |
145 |
else |
146 |
pp_assign |
147 |
m self (pp_horn_var m) fmt |
148 |
o.var_type (LocalVar o) i2 |
149 |
|
150 |
end |
151 |
| name, _, _ -> |
152 |
begin |
153 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in |
154 |
if init then |
155 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
156 |
pp_machine_init_name (node_name n) |
157 |
(* inputs *) |
158 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
159 |
(Utils.pp_final_char_if_non_empty " " inputs) |
160 |
(* outputs *) |
161 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
162 |
(Utils.pp_final_char_if_non_empty " " outputs) |
163 |
(* memories (next) *) |
164 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
165 |
rename_machine_list |
166 |
(concat m.mname.node_id i) |
167 |
(rename_next_list (* concat m.mname.node_id i *) |
168 |
(full_memory_vars machines target_machine) |
169 |
) |
170 |
) |
171 |
else |
172 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
173 |
pp_machine_step_name (node_name n) |
174 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
175 |
(Utils.pp_final_char_if_non_empty " " inputs) |
176 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
177 |
(Utils.pp_final_char_if_non_empty " " outputs) |
178 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
179 |
(rename_machine_list |
180 |
(concat m.mname.node_id i) |
181 |
(rename_current_list (* concat m.mname.node_id i *) |
182 |
(full_memory_vars machines target_machine)) |
183 |
) @ |
184 |
(rename_machine_list |
185 |
(concat m.mname.node_id i) |
186 |
(rename_next_list (* concat m.mname.node_id i *) |
187 |
(full_memory_vars machines target_machine)) |
188 |
) |
189 |
) |
190 |
|
191 |
end |
192 |
end |
193 |
with Not_found -> ( (* stateless node instance *) |
194 |
let (n,_) = List.assoc i m.mcalls in |
195 |
Format.fprintf fmt "(%s %a%t%a)" |
196 |
(node_name n) |
197 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs |
198 |
(Utils.pp_final_char_if_non_empty " " inputs) |
199 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
200 |
(* (Utils.fprintf_list ~sep:" " (pp_horn_var m)) outputs *) |
201 |
) |
202 |
|
203 |
let pp_machine_init (m: machine_t) self fmt inst = |
204 |
let (node, static) = List.assoc inst m.minstances in |
205 |
fprintf fmt "(%a %a%t%s->%s)" |
206 |
pp_machine_init_name (node_name node) |
207 |
(Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static |
208 |
(Utils.pp_final_char_if_non_empty " " static) |
209 |
self inst |
210 |
|
211 |
(* TODO *) |
212 |
let rec pp_conditional machines ?(init=false) (m: machine_t) self fmt c tl el = |
213 |
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}" |
214 |
(pp_horn_val self (pp_horn_var m)) c |
215 |
(Utils.pp_newline_if_non_empty tl) |
216 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) tl |
217 |
(Utils.pp_newline_if_non_empty el) |
218 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el |
219 |
|
220 |
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr = |
221 |
match instr with |
222 |
| MReset i -> |
223 |
pp_machine_init m self fmt i |
224 |
| MLocalAssign (i,v) -> |
225 |
pp_assign |
226 |
m self (pp_horn_var m) fmt |
227 |
i.var_type (LocalVar i) v |
228 |
| MStateAssign (i,v) -> |
229 |
pp_assign |
230 |
m self (pp_horn_var m) fmt |
231 |
i.var_type (StateVar i) v |
232 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> assert false (* This should not happen anymore *) |
233 |
(* pp_machine_instr machines ~init:init m self fmt (MLocalAssign (i0, Fun (i, vl))) *) |
234 |
| MStep (il, i, vl) -> |
235 |
pp_instance_call machines ~init:init m self fmt i vl il |
236 |
| MBranch (g,hl) -> |
237 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false |
238 |
then (* boolean case, needs special treatment in C because truth value is not unique *) |
239 |
(* may disappear if we optimize code by replacing last branch test with default *) |
240 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
241 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
242 |
pp_conditional machines ~init:init m self fmt g tl el |
243 |
else assert false (* enum type case *) |
244 |
|
245 |
|
246 |
(**************************************************************) |
247 |
|
248 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
249 |
|
250 |
(* Print the machine m: |
251 |
two functions: m_init and m_step |
252 |
- m_init is a predicate over m memories |
253 |
- m_step is a predicate over old_memories, inputs, new_memories, outputs |
254 |
We first declare all variables then the two /rules/. |
255 |
*) |
256 |
let print_machine machines fmt m = |
257 |
let pp_instr init = pp_machine_instr machines ~init:init m in |
258 |
if m.mname.node_id = arrow_id then |
259 |
(* We don't print arrow function *) |
260 |
() |
261 |
else |
262 |
begin |
263 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
264 |
|
265 |
(* Printing variables *) |
266 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
267 |
((step_vars machines m)@ |
268 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
269 |
Format.pp_print_newline fmt (); |
270 |
|
271 |
|
272 |
|
273 |
if is_stateless m then |
274 |
begin |
275 |
(* Declaring single predicate *) |
276 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
277 |
pp_machine_stateless_name m.mname.node_id |
278 |
(Utils.fprintf_list ~sep:" " pp_type) |
279 |
(List.map (fun v -> v.var_type) (stateless_vars machines m)); |
280 |
|
281 |
(* Rule for single predicate *) |
282 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@." |
283 |
(Utils.fprintf_list ~sep:"@ " |
284 |
(pp_instr |
285 |
true (* In this case, the boolean init can be set to true or false. |
286 |
The node is stateless. *) |
287 |
m.mname.node_id) |
288 |
) |
289 |
m.mstep.step_instrs |
290 |
pp_machine_stateless_name m.mname.node_id |
291 |
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m); |
292 |
end |
293 |
else |
294 |
begin |
295 |
(* Declaring predicate *) |
296 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
297 |
pp_machine_init_name m.mname.node_id |
298 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (init_vars machines m)); |
299 |
|
300 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
301 |
pp_machine_step_name m.mname.node_id |
302 |
(Utils.fprintf_list ~sep:" " pp_type) (List.map (fun v -> v.var_type) (step_vars machines m)); |
303 |
Format.pp_print_newline fmt (); |
304 |
|
305 |
(* Rule for init *) |
306 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@." |
307 |
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs |
308 |
pp_machine_init_name m.mname.node_id |
309 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); |
310 |
|
311 |
(* Rule for step *) |
312 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>%a@]@ )@ (%a %a)@]@.))@.@." |
313 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
314 |
pp_machine_step_name m.mname.node_id |
315 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
316 |
|
317 |
match m.mspec with |
318 |
None -> () (* No node spec; we do nothing *) |
319 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> |
320 |
( |
321 |
(* For the moment, we only deal with simple case: single ensures, no other parameters *) |
322 |
() |
323 |
|
324 |
) |
325 |
| _ -> () (* Other cases give nothing *) |
326 |
end |
327 |
end |
328 |
|
329 |
|
330 |
|
331 |
let main_print machines fmt = |
332 |
if !Options.main_node <> "" then |
333 |
begin |
334 |
let node = !Options.main_node in |
335 |
let machine = get_machine machines node in |
336 |
|
337 |
Format.fprintf fmt "; Collecting semantics for node %s@.@." node; |
338 |
(* We print the types of the main node "memory tree" TODO: add the output *) |
339 |
let main_output = |
340 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
341 |
in |
342 |
let main_output_dummy = |
343 |
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs |
344 |
in |
345 |
let main_memory_next = |
346 |
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
347 |
main_output |
348 |
in |
349 |
let main_memory_current = |
350 |
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
351 |
main_output_dummy |
352 |
in |
353 |
|
354 |
(* Special case when the main node is stateless *) |
355 |
let init_name, step_name = |
356 |
if is_stateless machine then |
357 |
pp_machine_stateless_name, pp_machine_stateless_name |
358 |
else |
359 |
pp_machine_init_name, pp_machine_step_name |
360 |
in |
361 |
|
362 |
Format.fprintf fmt "(declare-rel MAIN (%a))@." |
363 |
(Utils.fprintf_list ~sep:" " pp_type) |
364 |
(List.map (fun v -> v.var_type) main_memory_next); |
365 |
|
366 |
Format.fprintf fmt "; Initial set@."; |
367 |
Format.fprintf fmt "(declare-rel INIT_STATE ())@."; |
368 |
Format.fprintf fmt "(rule INIT_STATE)@."; |
369 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
370 |
init_name node |
371 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
372 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ; |
373 |
|
374 |
Format.fprintf fmt "; Inductive def@."; |
375 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
376 |
Format.fprintf fmt |
377 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
378 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
379 |
step_name node |
380 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
381 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ; |
382 |
|
383 |
Format.fprintf fmt "; Property def@."; |
384 |
Format.fprintf fmt "(declare-rel ERR ())@."; |
385 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (and %a))@ (MAIN %a)@])@ ERR))@." |
386 |
(Utils.fprintf_list ~sep:" " pp_var) main_output |
387 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next |
388 |
; |
389 |
Format.fprintf fmt "(query ERR)@."; |
390 |
|
391 |
() |
392 |
end |
393 |
|
394 |
|
395 |
let translate fmt basename prog machines = |
396 |
List.iter (print_machine machines fmt) (List.rev machines); |
397 |
|
398 |
main_print machines fmt |
399 |
|
400 |
|
401 |
(* Local Variables: *) |
402 |
(* compile-command:"make -C .." *) |
403 |
(* End: *) |