lustrec / src / machine_code.ml @ 2196a0a6
History | View | Annotate | Download (25.1 KB)
1 |
|
---|---|
2 |
(* ---------------------------------------------------------------------------- |
3 |
* SchedMCore - A MultiCore Scheduling Framework |
4 |
* Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE |
5 |
* Copyright (C) 2012-2013, INPT, Toulouse, FRANCE |
6 |
* |
7 |
* This file is part of Prelude |
8 |
* |
9 |
* Prelude is free software; you can redistribute it and/or |
10 |
* modify it under the terms of the GNU Lesser General Public License |
11 |
* as published by the Free Software Foundation ; either version 2 of |
12 |
* the License, or (at your option) any later version. |
13 |
* |
14 |
* Prelude is distributed in the hope that it will be useful, but |
15 |
* WITHOUT ANY WARRANTY ; without even the implied warranty of |
16 |
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU |
17 |
* Lesser General Public License for more details. |
18 |
* |
19 |
* You should have received a copy of the GNU Lesser General Public |
20 |
* License along with this program ; if not, write to the Free Software |
21 |
* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 |
22 |
* USA |
23 |
*---------------------------------------------------------------------------- *) |
24 |
|
25 |
(* This module is used for the lustre to C compiler *) |
26 |
|
27 |
open Corelang |
28 |
open Clocks |
29 |
open Causality |
30 |
|
31 |
exception NormalizationError |
32 |
|
33 |
module OrdVarDecl:Map.OrderedType with type t=var_decl = |
34 |
struct type t = var_decl;; let compare = compare end |
35 |
|
36 |
module ISet = Set.Make(OrdVarDecl) |
37 |
|
38 |
type value_t = |
39 |
| Cst of constant |
40 |
| LocalVar of var_decl |
41 |
| StateVar of var_decl |
42 |
| Fun of ident * value_t list |
43 |
| Array of value_t list |
44 |
| Access of value_t * value_t |
45 |
| Power of value_t * value_t |
46 |
|
47 |
type instr_t = |
48 |
| MLocalAssign of var_decl * value_t |
49 |
| MStateAssign of var_decl * value_t |
50 |
| MReset of ident |
51 |
| MStep of var_decl list * ident * value_t list |
52 |
| MBranch of value_t * (label * instr_t list) list |
53 |
|
54 |
let rec pp_val fmt v = |
55 |
match v with |
56 |
| Cst c -> Printers.pp_const fmt c |
57 |
| LocalVar v -> Format.pp_print_string fmt v.var_id |
58 |
| StateVar v -> Format.pp_print_string fmt v.var_id |
59 |
| Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl |
60 |
| Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i |
61 |
| Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n |
62 |
| Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl |
63 |
|
64 |
let rec pp_instr fmt i = |
65 |
match i with |
66 |
| MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v |
67 |
| MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v |
68 |
| MReset i -> Format.fprintf fmt "reset %s" i |
69 |
| MStep (il, i, vl) -> |
70 |
Format.fprintf fmt "%a = %s (%a)" |
71 |
(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il |
72 |
i |
73 |
(Utils.fprintf_list ~sep:", " pp_val) vl |
74 |
| MBranch (g,hl) -> |
75 |
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" |
76 |
pp_val g |
77 |
(Utils.fprintf_list ~sep:"@," pp_branch) hl |
78 |
|
79 |
and pp_branch fmt (t, h) = |
80 |
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h |
81 |
|
82 |
type step_t = { |
83 |
step_checks: (Location.t * value_t) list; |
84 |
step_inputs: var_decl list; |
85 |
step_outputs: var_decl list; |
86 |
step_locals: var_decl list; |
87 |
step_instrs: instr_t list; |
88 |
} |
89 |
|
90 |
type static_call = top_decl * (Dimension.dim_expr list) |
91 |
|
92 |
|
93 |
type eexpr_minimachine_t = { |
94 |
muid: tag; |
95 |
mquantifiers: (quantifier_type * var_decl list) list; |
96 |
mmmemory: var_decl list; |
97 |
mmcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, |
98 |
no internals *) |
99 |
mminstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *) |
100 |
mminit: instr_t list; |
101 |
mmstep_logic: step_t; |
102 |
mmstep_effects: step_t; |
103 |
(* mmlogic: step_t; *) |
104 |
} |
105 |
|
106 |
type spec_machine_t = { |
107 |
m_requires: eexpr_minimachine_t list; |
108 |
m_ensures: eexpr_minimachine_t list; |
109 |
m_behaviors: (string * eexpr_minimachine_t list * eexpr_minimachine_t list) list; |
110 |
} |
111 |
|
112 |
type machine_t = { |
113 |
mname: node_desc; |
114 |
mmemory: var_decl list; |
115 |
mcalls: (ident * static_call) list; (* map from stateful/stateless instance to node, no internals *) |
116 |
minstances: (ident * static_call) list; (* sub-map of mcalls, from stateful instance to node *) |
117 |
minit: instr_t list; |
118 |
mstatic: var_decl list; (* static inputs only *) |
119 |
mstep: step_t; |
120 |
mspec: spec_machine_t option; |
121 |
mannot: (string list * eexpr_minimachine_t) list; |
122 |
} |
123 |
|
124 |
let get_val_type v = |
125 |
match v with |
126 |
| Cst c -> (Typing.type_const Location.dummy_loc c).Types.tdesc |
127 |
| LocalVar v |
128 |
| StateVar v-> (Types.repr v.var_type).Types.tdesc |
129 |
| Fun _ |
130 |
| Array _ |
131 |
| Access _ |
132 |
| Power _ -> raise (Not_found) (* Not a variable *) |
133 |
|
134 |
let pp_step fmt s = |
135 |
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@]@ " |
136 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs |
137 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs |
138 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals |
139 |
(Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val fmt c)) s.step_checks |
140 |
(Utils.fprintf_list ~sep:"@ " pp_instr) s.step_instrs |
141 |
|
142 |
let pp_static_call fmt (node, args) = |
143 |
Format.fprintf fmt "%s<%a>" |
144 |
(node_name node) |
145 |
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args |
146 |
|
147 |
let pp_eexpr fmt ee = |
148 |
Format.fprintf fmt |
149 |
"%a%t @[<v 2>mem : %a@;instances: %a@;init : %a@;logic step :@; @[<v 2>%a@]@;effects step :@; @[<v 2>%a@]@;@]@;" |
150 |
(Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) ee.mquantifiers |
151 |
(fun fmt -> match ee.mquantifiers with [] -> () | _ -> Format.fprintf fmt ";") |
152 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) ee.mmmemory |
153 |
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) ee.mminstances |
154 |
(Utils.fprintf_list ~sep:"@ " pp_instr) ee.mminit |
155 |
pp_step ee.mmstep_logic |
156 |
pp_step ee.mmstep_effects |
157 |
|
158 |
|
159 |
let pp_spec fmt spec = |
160 |
Format.fprintf fmt "@[<hov 2>(*@@ "; |
161 |
Utils.fprintf_list ~sep:"@;@@ " (fun fmt r -> Format.fprintf fmt "requires %a;" pp_eexpr r) fmt spec.m_requires; |
162 |
Utils.fprintf_list ~sep:"@;@@ " (fun fmt r -> Format.fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.m_ensures; |
163 |
Utils.fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures) -> |
164 |
Format.fprintf fmt "behavior %s:@[@ %a@ %a@]" |
165 |
name |
166 |
(Utils.fprintf_list ~sep:"@ " (fun fmt r -> Format.fprintf fmt "assumes %a;" pp_eexpr r)) assumes |
167 |
(Utils.fprintf_list ~sep:"@ " (fun fmt r -> Format.fprintf fmt "ensures %a;" pp_eexpr r)) ensures |
168 |
) fmt spec.m_behaviors; |
169 |
Format.fprintf fmt "@]*)"; |
170 |
() |
171 |
|
172 |
|
173 |
|
174 |
|
175 |
let pp_machine fmt m = |
176 |
Format.fprintf fmt |
177 |
"@[<v 2>machine %s@;mem : %a@;instances: %a@;init : %a@;step :@; @[<v 2>%a@]@;spec: %a@;@]@ " |
178 |
m.mname.node_id |
179 |
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory |
180 |
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances |
181 |
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit |
182 |
pp_step m.mstep |
183 |
(fun fmt s -> match s with None -> () | Some s -> pp_spec fmt s) m.mspec |
184 |
|
185 |
let is_output m id = |
186 |
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs |
187 |
|
188 |
let conditional c t e = |
189 |
MBranch(c, [ (tag_true, t); (tag_false, e) ]) |
190 |
|
191 |
let dummy_var_decl name typ = |
192 |
{ |
193 |
var_id = name; |
194 |
var_dec_type = dummy_type_dec; |
195 |
var_dec_clock = dummy_clock_dec; |
196 |
var_dec_const = false; |
197 |
var_type = typ; |
198 |
var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true; |
199 |
var_loc = Location.dummy_loc |
200 |
} |
201 |
|
202 |
let arrow_id = "_arrow" |
203 |
|
204 |
let arrow_typ = Types.new_ty Types.Tunivar |
205 |
|
206 |
let arrow_desc = |
207 |
{ |
208 |
node_id = arrow_id; |
209 |
node_type = Type_predef.type_bin_poly_op; |
210 |
node_clock = Clock_predef.ck_bin_univ; |
211 |
node_inputs= [dummy_var_decl "_in1" arrow_typ; dummy_var_decl "_in2" arrow_typ]; |
212 |
node_outputs= [dummy_var_decl "_out" arrow_typ]; |
213 |
node_locals= []; |
214 |
node_gencalls = []; |
215 |
node_checks = []; |
216 |
node_asserts = []; |
217 |
node_eqs= []; |
218 |
node_spec = None; |
219 |
node_annot = []; } |
220 |
|
221 |
let arrow_top_decl = |
222 |
{ |
223 |
top_decl_desc = Node arrow_desc; |
224 |
top_decl_loc = Location.dummy_loc |
225 |
} |
226 |
|
227 |
let arrow_machine = |
228 |
let state = "_first" in |
229 |
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in |
230 |
let var_input1 = List.nth arrow_desc.node_inputs 0 in |
231 |
let var_input2 = List.nth arrow_desc.node_inputs 1 in |
232 |
let var_output = List.nth arrow_desc.node_outputs 0 in |
233 |
{ |
234 |
mname = arrow_desc; |
235 |
mmemory = [var_state]; |
236 |
mcalls = []; |
237 |
minstances = []; |
238 |
minit = [MStateAssign(var_state, Cst (const_of_bool true))]; |
239 |
mstatic = []; |
240 |
mstep = { |
241 |
step_inputs = arrow_desc.node_inputs; |
242 |
step_outputs = arrow_desc.node_outputs; |
243 |
step_locals = []; |
244 |
step_checks = []; |
245 |
step_instrs = [conditional (StateVar var_state) |
246 |
[MStateAssign(var_state, Cst (const_of_bool false)); |
247 |
MLocalAssign(var_output, LocalVar var_input1)] |
248 |
[MLocalAssign(var_output, LocalVar var_input2)] ] |
249 |
}; |
250 |
mspec = None; |
251 |
mannot = []; |
252 |
} |
253 |
|
254 |
let is_stateless_node node = |
255 |
(node_name node <> arrow_id) && |
256 |
match node.top_decl_desc with |
257 |
| Node id -> false (* TODO: add a check after the machines are produced. Start from the main node and do a DFS to compute the stateless/statefull property of nodes. Stateless nodes should not be reset *) |
258 |
| ImportedNode id -> id.nodei_stateless |
259 |
| ImportedFun _ -> true |
260 |
| _ -> assert false |
261 |
|
262 |
let new_instance = |
263 |
let cpt = ref (-1) in |
264 |
fun caller callee tag -> |
265 |
begin |
266 |
let o = |
267 |
if is_stateless_node callee then |
268 |
node_name callee |
269 |
else |
270 |
Printf.sprintf "ni_%d" (incr cpt; !cpt) in |
271 |
let o = |
272 |
if !Options.ansi && is_generic_node callee |
273 |
then Printf.sprintf "%s_inst_%d" o (Utils.position (fun e -> e.expr_tag = tag) caller.node_gencalls) |
274 |
else o in |
275 |
o |
276 |
end |
277 |
|
278 |
let const_of_carrier cr = |
279 |
match (carrier_repr cr).carrier_desc with |
280 |
| Carry_const id -> id |
281 |
| Carry_name -> assert false |
282 |
| Carry_var -> assert false |
283 |
| Carry_link _ -> assert false (* TODO check this Xavier *) |
284 |
|
285 |
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *) |
286 |
(* the context contains m : state aka memory variables *) |
287 |
(* si : initialization instructions *) |
288 |
(* j : node aka machine instances *) |
289 |
(* d : local variables *) |
290 |
(* s : step instructions *) |
291 |
let translate_ident vars (m, si, j, d, s) id = |
292 |
try (* id is a node var *) |
293 |
(* Format.eprintf "translate ident: %s@.@?" id; *) |
294 |
let var_id = try List.find (fun v -> v.var_id= id) vars with Not_found -> assert false in |
295 |
if ISet.exists (fun v -> v.var_id = id) m |
296 |
then StateVar var_id |
297 |
else LocalVar var_id |
298 |
with Not_found -> (* id is a constant *) |
299 |
LocalVar (Corelang.var_decl_of_const (Hashtbl.find Corelang.consts_table id)) |
300 |
|
301 |
let rec control_on_clock vars ((m, si, j, d, s) as args) ck inst = |
302 |
match ck.cdesc with |
303 |
| Con (ck1, cr, l) -> |
304 |
let id = const_of_carrier cr in |
305 |
control_on_clock vars args ck1 (MBranch (translate_ident vars args id, |
306 |
[l, [inst]] )) |
307 |
| _ -> inst |
308 |
|
309 |
let rec join_branches hl1 hl2 = |
310 |
match hl1, hl2 with |
311 |
| [] , _ -> hl2 |
312 |
| _ , [] -> hl1 |
313 |
| (t1, h1)::q1, (t2, h2)::q2 -> |
314 |
if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else |
315 |
if t1 > t2 then (t2, h2) :: join_branches hl1 q2 |
316 |
else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2 |
317 |
|
318 |
and join_guards inst1 insts2 = |
319 |
match inst1, insts2 with |
320 |
| _ , [] -> |
321 |
[inst1] |
322 |
| MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 -> |
323 |
MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)) |
324 |
:: q |
325 |
| _ -> inst1 :: insts2 |
326 |
|
327 |
let join_guards_list insts = |
328 |
List.fold_right join_guards insts [] |
329 |
|
330 |
let find_eq x eqs = |
331 |
let rec aux accu eqs = |
332 |
match eqs with |
333 |
| [] -> |
334 |
begin |
335 |
Format.eprintf "Looking for variable %a in the following equations@.%a@.@?" |
336 |
Format.pp_print_string x |
337 |
Printers.pp_node_eqs eqs; |
338 |
assert false |
339 |
end |
340 |
| hd::tl -> |
341 |
if List.mem x hd.eq_lhs then hd, accu@tl else aux (hd::accu) tl |
342 |
in |
343 |
aux [] eqs |
344 |
|
345 |
let rec translate_expr vars ((m, si, j, d, s) as args) expr = |
346 |
match expr.expr_desc with |
347 |
| Expr_const v -> Cst v |
348 |
| Expr_ident x -> translate_ident vars args x |
349 |
| Expr_array el -> Array (List.map (translate_expr vars args) el) |
350 |
| Expr_access (t, i) -> Access (translate_expr vars args t, translate_expr vars args (expr_of_dimension i)) |
351 |
| Expr_power (e, n) -> Power (translate_expr vars args e, translate_expr vars args (expr_of_dimension n)) |
352 |
| Expr_tuple _ |
353 |
| Expr_arrow _ |
354 |
| Expr_fby _ |
355 |
| Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) |
356 |
| Expr_when (e1, _, _) -> translate_expr vars args e1 |
357 |
| Expr_merge (x, _) -> raise NormalizationError |
358 |
| Expr_appl (id, e, _) when Basic_library.is_internal_fun id -> |
359 |
let nd = node_from_name id in |
360 |
(match e.expr_desc with |
361 |
| Expr_tuple el -> Fun (node_name nd, List.map (translate_expr vars args) el) |
362 |
| _ -> Fun (node_name nd, [translate_expr vars args e])) |
363 |
| Expr_ite (g,t,e) -> ( |
364 |
(* special treatment depending on the active backend. For horn backend or |
365 |
acsl spec, ite are preserved in expression. While they are removed for C |
366 |
or Java backends. *) |
367 |
Fun ("ite", [translate_expr vars args g; translate_expr vars args t; translate_expr vars args e]) |
368 |
) |
369 |
| _ -> raise NormalizationError |
370 |
|
371 |
let translate_guard node args expr = |
372 |
match expr.expr_desc with |
373 |
| Expr_ident x -> translate_ident node args x |
374 |
| _ -> assert false |
375 |
|
376 |
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = |
377 |
match expr.expr_desc with |
378 |
| Expr_ite (c, t, e) -> let g = translate_guard node args c in |
379 |
conditional g [translate_act node args (y, t)] |
380 |
[translate_act node args (y, e)] |
381 |
| Expr_merge (x, hl) -> MBranch (translate_ident node args x, List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl) |
382 |
| _ -> MLocalAssign (y, translate_expr node args expr) |
383 |
|
384 |
let reset_instance vars args i r c = |
385 |
match r with |
386 |
| None -> [] |
387 |
| Some (x, l) -> [control_on_clock vars args c (MBranch (translate_ident vars args x, [l, [MReset i]]))] |
388 |
|
389 |
let translate_eq node keep_ite (local_vars: var_decl list) ((m, si, j, d, s) as args) eq = |
390 |
(*Format.eprintf "translate_eq %a@." Printers.pp_node_eq eq;*) |
391 |
let vars = local_vars@(node_vars node) in |
392 |
let get_var x = |
393 |
let test v = v.var_id = x in |
394 |
if List.exists test vars then List.find test vars else assert false in |
395 |
match eq.eq_lhs, eq.eq_rhs.expr_desc with |
396 |
| [x], Expr_arrow (e1, e2) -> |
397 |
let var_x = get_var x in |
398 |
let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in |
399 |
let c1 = translate_expr vars args e1 in |
400 |
let c2 = translate_expr vars args e2 in |
401 |
(m, |
402 |
MReset o :: si, |
403 |
Utils.IMap.add o (arrow_top_decl, []) j, |
404 |
d, |
405 |
(control_on_clock vars args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s) |
406 |
| [x], Expr_pre e1 when ISet.mem (get_var x) d -> |
407 |
let var_x = get_var x in |
408 |
(ISet.add var_x m, |
409 |
si, |
410 |
j, |
411 |
d, |
412 |
control_on_clock vars args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr vars args e1)) :: s) |
413 |
| [x], Expr_fby (e1, e2) when ISet.mem (get_var x) d -> |
414 |
let var_x = get_var x in |
415 |
(ISet.add var_x m, |
416 |
MStateAssign (var_x, translate_expr vars args e1) :: si, |
417 |
j, |
418 |
d, |
419 |
control_on_clock vars args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr vars args e2)) :: s) |
420 |
| p, Expr_appl (f, arg, r) -> |
421 |
let var_p = List.map (fun v -> get_var v) p in |
422 |
let el = |
423 |
match arg.expr_desc with |
424 |
| Expr_tuple el -> el |
425 |
| _ -> [arg] in |
426 |
let vl = List.map (translate_expr vars args) el in |
427 |
let node_f = node_from_name f in |
428 |
let call_f = |
429 |
node_f, |
430 |
NodeDep.filter_static_inputs (node_inputs node_f) el in |
431 |
let o = new_instance node node_f eq.eq_rhs.expr_tag in |
432 |
(m, |
433 |
(if is_stateless_node node_f then si else MReset o :: si), |
434 |
(if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j), |
435 |
d, |
436 |
reset_instance vars args o r eq.eq_rhs.expr_clock @ |
437 |
(control_on_clock vars args eq.eq_rhs.expr_clock (MStep (var_p, o, vl))) :: s) |
438 |
|
439 |
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) |
440 |
are preserved. While they are replaced as if g then x = t else x = e in C or Java |
441 |
backends. *) |
442 |
| [x], Expr_ite (c, t, e) when keep_ite -> |
443 |
let var_x = get_var x in |
444 |
(m, |
445 |
si, |
446 |
j, |
447 |
d, |
448 |
(control_on_clock vars args eq.eq_rhs.expr_clock |
449 |
(MLocalAssign (var_x, translate_expr vars args eq.eq_rhs))::s) |
450 |
) |
451 |
|
452 |
| [x], _ -> ( |
453 |
let var_x = get_var x in |
454 |
(m, si, j, d, |
455 |
control_on_clock vars args eq.eq_rhs.expr_clock (translate_act vars args (var_x, eq.eq_rhs)) :: s) |
456 |
) |
457 |
| _ -> |
458 |
begin |
459 |
Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq; |
460 |
assert false |
461 |
end |
462 |
|
463 |
let translate_eqs node keep_ite local_vars args eqs = |
464 |
List.fold_right (fun eq args -> translate_eq node keep_ite local_vars args eq) eqs args;; |
465 |
|
466 |
|
467 |
(* The eexpr shoud have been normalized, ie. its eexpr_normalized field updated |
468 |
We add a new boolean output var and bound it to the main expression |
469 |
characterizing the eexpr. |
470 |
|
471 |
*) |
472 |
let translate_eexpr nd eexpr = |
473 |
(* Format.eprintf "Translating eexpr: %a" Printers.pp_eexpr eexpr; *) |
474 |
let output_var, eqs, locals = match eexpr.eexpr_normalized with None -> assert false | Some x -> x in |
475 |
(* both inputs and outputs are considered here as inputs for the specification *) |
476 |
let inputs = nd.node_inputs @ nd.node_outputs in |
477 |
let inputs_quantifiers = inputs @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in |
478 |
|
479 |
let eexpr_local_vars = output_var :: locals @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in |
480 |
let visible_vars = eexpr_local_vars @ inputs in |
481 |
|
482 |
let sort_eqs inputs eqs = |
483 |
let eqs_logic, new_locals_logic, sch_logic = Scheduling.schedule_eqs inputs visible_vars eqs in |
484 |
(* Format.eprintf "sch: [%a]@;new locals: [%a]@;locals:[%a]@.eexpr local vars: [%a]@.@?" *) |
485 |
(* (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch_logic *) |
486 |
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) new_locals_logic *) |
487 |
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) locals *) |
488 |
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) eexpr_local_vars; *) |
489 |
let locals = eexpr_local_vars @ new_locals_logic @ (List.flatten (List.map snd eexpr.eexpr_quantifiers)) in |
490 |
let sorted_eqs_rev_logic, remainder_logic = |
491 |
List.fold_left |
492 |
(fun (accu, eqs_remainder) v -> |
493 |
if List.exists (fun eq -> List.mem v eq.eq_lhs) accu |
494 |
then (* The variable was already handled by a previous selected eq. |
495 |
Typically it is part of a tuple *) |
496 |
((* Format.eprintf "Case 1 for variable %s@." v; *) |
497 |
(accu, eqs_remainder) |
498 |
) |
499 |
else if List.exists (fun vdecl -> vdecl.var_id = v) locals || output_var.var_id = v |
500 |
then ((* Select the eq associated to v. *) |
501 |
(* Format.eprintf "Case 2 for variable %s@." v; *) |
502 |
let eq_v, remainder = find_eq v eqs_remainder in |
503 |
eq_v::accu, remainder |
504 |
) |
505 |
else ((* else it is a constant value, checked during typing phase *) |
506 |
(* Format.eprintf "Case 3 for variable %s@." v; *) |
507 |
accu, eqs_remainder |
508 |
) |
509 |
) |
510 |
([], eqs_logic) |
511 |
sch_logic |
512 |
in |
513 |
if List.length remainder_logic > 0 then ( |
514 |
Format.eprintf "Spec equations not used are@.%a@.Full equation set is:@.%a@.@?" |
515 |
Printers.pp_node_eqs remainder_logic |
516 |
Printers.pp_node_eqs eqs_logic; |
517 |
assert false ); |
518 |
List.rev sorted_eqs_rev_logic, locals |
519 |
in |
520 |
|
521 |
|
522 |
|
523 |
(* Generating logic definition instructions *) |
524 |
let sorted_eqs, locals = sort_eqs inputs_quantifiers eqs in |
525 |
|
526 |
let init_args = |
527 |
ISet.empty, |
528 |
[], |
529 |
Utils.IMap.empty, |
530 |
List.fold_right (fun l -> ISet.add l) locals ISet.empty, |
531 |
[] |
532 |
in |
533 |
|
534 |
let m, init, j, locals, s_logic = |
535 |
translate_eqs nd true (* keep_ite *) eexpr_local_vars init_args (sorted_eqs) |
536 |
in |
537 |
let s_logic = List.filter (fun i -> match i with MStateAssign _ -> false | _ -> true) s_logic in |
538 |
|
539 |
let _,_,_,_, s_side_effects = |
540 |
translate_eqs nd false (* explose ite *) eexpr_local_vars init_args (sorted_eqs) |
541 |
in |
542 |
let s_side_effects = |
543 |
List.filter (fun i -> |
544 |
match i with |
545 |
| MStep([v], _, _) |
546 |
| MLocalAssign(v,_) -> v.var_id <> output_var.var_id |
547 |
| _ -> true) s_side_effects in |
548 |
|
549 |
{ |
550 |
muid = eexpr.eexpr_tag; |
551 |
mquantifiers = eexpr.eexpr_quantifiers; |
552 |
mmmemory = ISet.elements m; |
553 |
mmcalls = []; (* no calls *) |
554 |
mminstances = []; (* no calls *) |
555 |
mminit = init; |
556 |
mmstep_logic = { |
557 |
step_inputs = inputs; |
558 |
step_outputs = [output_var]; |
559 |
step_locals = ISet.elements (ISet.remove output_var (ISet.diff locals m)); |
560 |
step_checks = [] (* Not handled yet *); |
561 |
step_instrs = ( |
562 |
(* special treatment depending on the active backend. For horn backend, |
563 |
common branches are not merged while they are in C or Java |
564 |
backends. *) |
565 |
match !Options.output with |
566 |
| "horn" -> s_logic |
567 |
| "C" | "java" | _ -> join_guards_list s_logic |
568 |
) |
569 |
}; |
570 |
mmstep_effects = { |
571 |
step_inputs = inputs; |
572 |
step_outputs = []; |
573 |
step_locals = ISet.elements (ISet.remove output_var (ISet.diff locals m)); |
574 |
step_checks = [] (* Not handled yet *); |
575 |
step_instrs = ( |
576 |
(* special treatment depending on the active backend. For horn backend, |
577 |
common branches are not merged while they are in C or Java |
578 |
backends. *) |
579 |
match !Options.output with |
580 |
| "horn" -> s_side_effects |
581 |
| "C" | "java" | _ -> join_guards_list s_side_effects |
582 |
) |
583 |
} |
584 |
} |
585 |
|
586 |
|
587 |
let translate_spec nd spec = |
588 |
(* Each eexpr of the spec is expressed as a minimachine: |
589 |
instrs (to update memory and set local vars) |
590 |
+ expr (to compute the output |
591 |
+ memory defs |
592 |
+ instances (for callee nodes) |
593 |
*) |
594 |
let transl = List.map (translate_eexpr nd) in |
595 |
{ |
596 |
m_requires = transl spec.requires; |
597 |
m_ensures = transl spec.ensures; |
598 |
m_behaviors = |
599 |
List.map |
600 |
(fun (beh_id, req, ens, _) -> beh_id, transl req, transl ens) |
601 |
spec.behaviors |
602 |
} |
603 |
|
604 |
let translate_decl top = |
605 |
let nd = match top.top_decl_desc with Node nd -> nd | _ -> assert false in |
606 |
(*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*) |
607 |
let nd, sch = Scheduling.schedule_node nd in |
608 |
(* Format.eprintf "node sch: [%a]@.@?" *) |
609 |
(* (Utils.fprintf_list ~sep:", " Format.pp_print_string) sch; *) |
610 |
|
611 |
(* let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in *) |
612 |
let sorted_eqs_rev, remainder = |
613 |
List.fold_left |
614 |
(fun (accu, node_eqs_remainder) v -> |
615 |
if List.exists (fun eq -> List.mem v eq.eq_lhs) accu |
616 |
then (* The variable was already handled by a previous selected eq. |
617 |
Typically it is part of a tuple *) |
618 |
(accu, node_eqs_remainder) |
619 |
else |
620 |
if List.exists (fun vdecl -> vdecl.var_id = v) nd.node_locals |
621 |
|| List.exists (fun vdecl -> vdecl.var_id = v) nd.node_outputs |
622 |
then (* Select the eq associated to v. *) |
623 |
let eq_v, remainder = find_eq v node_eqs_remainder in |
624 |
eq_v::accu, remainder |
625 |
else (* else it is a constant value, checked during typing phase *) |
626 |
accu, node_eqs_remainder |
627 |
) |
628 |
([], nd.node_eqs) |
629 |
sch |
630 |
in |
631 |
if List.length remainder > 0 then ( |
632 |
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?" |
633 |
Printers.pp_node_eqs remainder |
634 |
Printers.pp_node_eqs nd.node_eqs; |
635 |
assert false ) |
636 |
; |
637 |
|
638 |
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in |
639 |
let keep_ite = (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false) in |
640 |
let m, init, j, locals, s = translate_eqs nd keep_ite [] init_args (List.rev sorted_eqs_rev) in |
641 |
let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in |
642 |
{ |
643 |
mname = nd; |
644 |
mmemory = ISet.elements m; |
645 |
mcalls = mmap; |
646 |
minstances = List.filter (fun (_, (n,_)) -> not (is_stateless_node n)) mmap; |
647 |
minit = init; |
648 |
mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs; |
649 |
mstep = { |
650 |
step_inputs = nd.node_inputs; |
651 |
step_outputs = nd.node_outputs; |
652 |
step_locals = ISet.elements (ISet.diff locals m); |
653 |
step_checks = List.map (fun d -> d.Dimension.dim_loc, translate_expr (node_vars nd) init_args (expr_of_dimension d)) nd.node_checks; |
654 |
step_instrs = ( |
655 |
(* special treatment depending on the active backend. For horn backend, |
656 |
common branches are not merged while they are in C or Java |
657 |
backends. *) |
658 |
match !Options.output with |
659 |
| "horn" -> s |
660 |
| "C" | "java" | _ -> join_guards_list s |
661 |
); |
662 |
}; |
663 |
mspec = Utils.option_map (translate_spec nd) nd.node_spec; |
664 |
mannot = List.flatten ( |
665 |
List.map (fun ann -> List.map (fun (kwd, eexpr) -> kwd, (translate_eexpr nd eexpr)) ann.annots) nd.node_annot); |
666 |
} |
667 |
|
668 |
|
669 |
let translate_prog decls = |
670 |
let nodes = get_nodes decls in |
671 |
arrow_machine :: List.map translate_decl nodes |
672 |
|
673 |
let get_machine_opt name machines = |
674 |
List.fold_left |
675 |
(fun res m -> |
676 |
match res with |
677 |
| Some _ -> res |
678 |
| None -> if m.mname.node_id = name then Some m else None) |
679 |
None machines |
680 |
|
681 |
|
682 |
(* Local Variables: *) |
683 |
(* compile-command:"make -C .." *) |
684 |
(* End: *) |