Revision 97d3f81a
Added by Teme Kahsai almost 10 years ago
src/backends/Horn/horn_backend.ml | ||
---|---|---|
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 is defined in Garoche, Gurfinkel, Kahsai, |
|
13 |
HCSV'14 *) |
|
14 |
|
|
15 |
open Format |
|
16 |
open LustreSpec |
|
17 |
open Corelang |
|
18 |
open Machine_code |
|
19 |
|
|
20 |
|
|
21 |
let pp_machine_init_name fmt id = fprintf fmt "%s_init" id |
|
22 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
|
23 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id |
|
24 |
|
|
25 |
let pp_type fmt t = |
|
26 |
match (Types.repr t).Types.tdesc with |
|
27 |
| Types.Tbool -> Format.fprintf fmt "Bool" |
|
28 |
| Types.Tint -> Format.fprintf fmt "Int" |
|
29 |
| Types.Treal -> Format.fprintf fmt "Real" |
|
30 |
| Types.Tclock _ |
|
31 |
| Types.Tarray _ |
|
32 |
| Types.Tstatic _ |
|
33 |
| Types.Tconst _ |
|
34 |
| Types.Tarrow _ |
|
35 |
| _ -> Format.eprintf "internal error: pp_type %a@." |
|
36 |
Types.print_ty t; assert false |
|
37 |
|
|
38 |
let pp_decl_var fmt id = |
|
39 |
Format.fprintf fmt "(declare-var %s %a)" |
|
40 |
id.var_id |
|
41 |
pp_type id.var_type |
|
42 |
|
|
43 |
let pp_var fmt id = Format.pp_print_string fmt id.var_id |
|
44 |
|
|
45 |
|
|
46 |
let pp_conj pp fmt l = |
|
47 |
match l with |
|
48 |
[] -> assert false |
|
49 |
| [x] -> pp fmt x |
|
50 |
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l |
|
51 |
|
|
52 |
|
|
53 |
|
|
54 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
|
55 |
let rename f = (fun v -> {v with var_id = f v.var_id } ) |
|
56 |
let rename_machine p = rename (fun n -> concat p n) |
|
57 |
let rename_machine_list p = List.map (rename_machine p) |
|
58 |
|
|
59 |
let rename_current = rename (fun n -> n ^ "_c") |
|
60 |
let rename_current_list = List.map rename_current |
|
61 |
let rename_next = rename (fun n -> n ^ "_x") |
|
62 |
let rename_next_list = List.map rename_next |
|
63 |
|
|
64 |
|
|
65 |
let get_machine machines node_name = |
|
66 |
List.find (fun m -> m.mname.node_id = node_name) machines |
|
67 |
|
|
68 |
|
|
69 |
let full_memory_vars machines machine = |
|
70 |
let rec aux fst prefix m = |
|
71 |
(rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @ |
|
72 |
List.fold_left (fun accu (id, (n, _)) -> |
|
73 |
let name = node_name n in |
|
74 |
if name = "_arrow" then accu else |
|
75 |
let machine_n = get_machine machines name in |
|
76 |
( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu |
|
77 |
) [] (m.minstances) |
|
78 |
in |
|
79 |
aux true machine.mname.node_id machine |
|
80 |
|
|
81 |
|
|
82 |
let stateless_vars machines m = |
|
83 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
|
84 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs) |
|
85 |
|
|
86 |
let step_vars machines m = |
|
87 |
(stateless_vars machines m)@ |
|
88 |
(rename_current_list (full_memory_vars machines m)) @ |
|
89 |
(rename_next_list (full_memory_vars machines m)) |
|
90 |
|
|
91 |
let init_vars machines m = |
|
92 |
(stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m)) |
|
93 |
|
|
94 |
(********************************************************************************************) |
|
95 |
(* Instruction Printing functions *) |
|
96 |
(********************************************************************************************) |
|
97 |
|
|
98 |
let pp_horn_var m fmt id = |
|
99 |
if Types.is_array_type id.var_type |
|
100 |
then |
|
101 |
assert false (* no arrays in Horn output *) |
|
102 |
else |
|
103 |
Format.fprintf fmt "%s" id.var_id |
|
104 |
|
|
105 |
|
|
106 |
(* Used to print boolean constants *) |
|
107 |
let pp_horn_tag fmt t = |
|
108 |
pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t) |
|
109 |
|
|
110 |
(* Prints a constant value *) |
|
111 |
let rec pp_horn_const fmt c = |
|
112 |
match c with |
|
113 |
| Const_int i -> pp_print_int fmt i |
|
114 |
| Const_real r -> pp_print_string fmt r |
|
115 |
| Const_float r -> pp_print_float fmt r |
|
116 |
| Const_tag t -> pp_horn_tag fmt t |
|
117 |
| _ -> assert false |
|
118 |
|
|
119 |
(* Prints a value expression [v], with internal function calls only. |
|
120 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
|
121 |
but an offset suffix may be added for array variables |
|
122 |
*) |
|
123 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
|
124 |
match v with |
|
125 |
| Cst c -> pp_horn_const fmt c |
|
126 |
| Array _ |
|
127 |
| Access _ -> assert false (* no arrays *) |
|
128 |
| Power (v, n) -> assert false |
|
129 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
130 |
| StateVar v -> |
|
131 |
if Types.is_array_type v.var_type |
|
132 |
then assert false |
|
133 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
134 |
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
135 |
|
|
136 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
|
137 |
let rec pp_value_suffix self pp_value fmt value = |
|
138 |
match value with |
|
139 |
| Fun (n, vl) -> |
|
140 |
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl |
|
141 |
| _ -> |
|
142 |
pp_horn_val self pp_value fmt value |
|
143 |
|
|
144 |
(* type_directed assignment: array vs. statically sized type |
|
145 |
- [var_type]: type of variable to be assigned |
|
146 |
- [var_name]: name of variable to be assigned |
|
147 |
- [value]: assigned value |
|
148 |
- [pp_var]: printer for variables |
|
149 |
*) |
|
150 |
let pp_assign m self pp_var fmt var_type var_name value = |
|
151 |
fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value |
|
152 |
|
|
153 |
let pp_instance_call |
|
154 |
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) = |
|
155 |
try (* stateful node instance *) |
|
156 |
begin |
|
157 |
let (n,_) = List.assoc i m.minstances in |
|
158 |
match node_name n, inputs, outputs with |
|
159 |
| "_arrow", [i1; i2], [o] -> begin |
|
160 |
if init then |
|
161 |
pp_assign |
|
162 |
m |
|
163 |
self |
|
164 |
(pp_horn_var m) |
|
165 |
fmt |
|
166 |
o.var_type (LocalVar o) i1 |
|
167 |
else |
|
168 |
pp_assign |
|
169 |
m self (pp_horn_var m) fmt |
|
170 |
o.var_type (LocalVar o) i2 |
|
171 |
|
|
172 |
end |
|
173 |
| name, _, _ -> |
|
174 |
begin |
|
175 |
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in |
|
176 |
if init then |
|
177 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
178 |
pp_machine_init_name (node_name n) |
|
179 |
(* inputs *) |
|
180 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
181 |
inputs |
|
182 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
183 |
(* outputs *) |
|
184 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
185 |
(List.map (fun v -> LocalVar v) outputs) |
|
186 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
187 |
(* memories (next) *) |
|
188 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
|
189 |
rename_machine_list |
|
190 |
(concat m.mname.node_id i) |
|
191 |
(rename_next_list (full_memory_vars machines target_machine) |
|
192 |
) |
|
193 |
) |
|
194 |
else |
|
195 |
Format.fprintf fmt "(%a %a%t%a%t%a)" |
|
196 |
pp_machine_step_name (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))) |
|
200 |
(List.map (fun v -> LocalVar v) outputs) |
|
201 |
(Utils.pp_final_char_if_non_empty " " outputs) |
|
202 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
|
203 |
(rename_machine_list |
|
204 |
(concat m.mname.node_id i) |
|
205 |
(rename_current_list (full_memory_vars machines target_machine)) |
|
206 |
) @ |
|
207 |
(rename_machine_list |
|
208 |
(concat m.mname.node_id i) |
|
209 |
(rename_next_list (full_memory_vars machines target_machine)) |
|
210 |
) |
|
211 |
) |
|
212 |
|
|
213 |
end |
|
214 |
end |
|
215 |
with Not_found -> ( (* stateless node instance *) |
|
216 |
let (n,_) = List.assoc i m.mcalls in |
|
217 |
Format.fprintf fmt "(%s %a%t%a)" |
|
218 |
(node_name n) |
|
219 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
220 |
inputs |
|
221 |
(Utils.pp_final_char_if_non_empty " " inputs) |
|
222 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) |
|
223 |
(List.map (fun v -> LocalVar v) outputs) |
|
224 |
) |
|
225 |
|
|
226 |
let pp_machine_init (m: machine_t) self fmt inst = |
|
227 |
let (node, static) = List.assoc inst m.minstances in |
|
228 |
fprintf fmt "(%a %a%t%s->%s)" |
|
229 |
pp_machine_init_name (node_name node) |
|
230 |
(Utils.fprintf_list ~sep:" " Dimension.pp_dimension) static |
|
231 |
(Utils.pp_final_char_if_non_empty " " static) |
|
232 |
self inst |
|
233 |
|
|
234 |
(* TODO *) |
|
235 |
let rec pp_conditional machines ?(init=false) (m: machine_t) self fmt c tl el = |
|
236 |
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}" |
|
237 |
(pp_horn_val self (pp_horn_var m)) c |
|
238 |
(Utils.pp_newline_if_non_empty tl) |
|
239 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) tl |
|
240 |
(Utils.pp_newline_if_non_empty el) |
|
241 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el |
|
242 |
|
|
243 |
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr = |
|
244 |
match instr with |
|
245 |
| MReset i -> |
|
246 |
pp_machine_init m self fmt i |
|
247 |
| MLocalAssign (i,v) -> |
|
248 |
pp_assign |
|
249 |
m self (pp_horn_var m) fmt |
|
250 |
i.var_type (LocalVar i) v |
|
251 |
| MStateAssign (i,v) -> |
|
252 |
pp_assign |
|
253 |
m self (pp_horn_var m) fmt |
|
254 |
i.var_type (StateVar i) v |
|
255 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
|
256 |
assert false (* This should not happen anymore *) |
|
257 |
| MStep (il, i, vl) -> |
|
258 |
pp_instance_call machines ~init:init m self fmt i vl il |
|
259 |
| MBranch (g,hl) -> |
|
260 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false |
|
261 |
then (* boolean case, needs special treatment in C because truth value is not unique *) |
|
262 |
(* may disappear if we optimize code by replacing last branch test with default *) |
|
263 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
|
264 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
|
265 |
pp_conditional machines ~init:init m self fmt g tl el |
|
266 |
else assert false (* enum type case *) |
|
267 |
|
|
268 |
|
|
269 |
(**************************************************************) |
|
270 |
|
|
271 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
|
272 |
|
|
273 |
(* Print the machine m: |
|
274 |
two functions: m_init and m_step |
|
275 |
- m_init is a predicate over m memories |
|
276 |
- m_step is a predicate over old_memories, inputs, new_memories, outputs |
|
277 |
We first declare all variables then the two /rules/. |
|
278 |
*) |
|
279 |
let print_machine machines fmt m = |
|
280 |
let pp_instr init = pp_machine_instr machines ~init:init m in |
|
281 |
if m.mname.node_id = arrow_id then |
|
282 |
(* We don't print arrow function *) |
|
283 |
() |
|
284 |
else |
|
285 |
begin |
|
286 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
287 |
|
|
288 |
(* Printing variables *) |
|
289 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
290 |
((step_vars machines m)@ |
|
291 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
292 |
Format.pp_print_newline fmt (); |
|
293 |
|
|
294 |
|
|
295 |
|
|
296 |
if is_stateless m then |
|
297 |
begin |
|
298 |
(* Declaring single predicate *) |
|
299 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
300 |
pp_machine_stateless_name m.mname.node_id |
|
301 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
302 |
(List.map (fun v -> v.var_type) (stateless_vars machines m)); |
|
303 |
|
|
304 |
(* Rule for single predicate *) |
|
305 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." |
|
306 |
(pp_conj (pp_instr |
|
307 |
true (* In this case, the boolean init can be set to true or false. |
|
308 |
The node is stateless. *) |
|
309 |
m.mname.node_id) |
|
310 |
) |
|
311 | 1 |
m.mstep.step_instrs |
312 | 2 |
pp_machine_stateless_name m.mname.node_id |
313 | 3 |
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m); |
... | ... | |
328 | 18 |
Format.pp_print_newline fmt (); |
329 | 19 |
|
330 | 20 |
(* Rule for init *) |
331 |
(* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *)
|
|
332 |
(* (pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs *)
|
|
333 |
(* pp_machine_init_name m.mname.node_id *)
|
|
334 |
(* (Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m); *)
|
|
21 |
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
|
|
22 |
(pp_conj (pp_instr true m.mname.node_id)) m.mstep.step_instrs
|
|
23 |
pp_machine_init_name m.mname.node_id
|
|
24 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m);
|
|
335 | 25 |
|
336 | 26 |
(* (\* Rule for step *\) *) |
337 | 27 |
(* Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@." *) |
Also available in: Unified diff
sync horn backend