lustrec / src / backends / Riny / riny_backend.ml @ 3d04f75e
History | View | Annotate | Download (6.45 KB)
1 |
open LustreSpec |
---|---|
2 |
open Corelang |
3 |
open Machine_code |
4 |
|
5 |
|
6 |
let pp_var fmt id = Format.pp_print_string fmt id.var_id |
7 |
|
8 |
let rec pp_c_val self pp_var fmt v = |
9 |
match v with |
10 |
| Cst c -> C_backend_common.pp_c_const fmt c |
11 |
| Array _ |
12 |
| Access _ |
13 |
| Power _ -> assert false |
14 |
| LocalVar v -> pp_var fmt v |
15 |
| StateVar v -> |
16 |
(* array memory vars are represented by an indirection to a local var with the right type, |
17 |
in order to avoid casting everywhere. *) |
18 |
if Types.is_array_type v.var_type |
19 |
then assert false |
20 |
else Format.fprintf fmt "%s_%a" self pp_var v |
21 |
| Fun (n, vl) -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl |
22 |
|
23 |
module CSrc = C_backend_src.Main (C_backend_src.EmptyMod) |
24 |
(* let pp_assign = CSrc.pp_assign *) |
25 |
|
26 |
let pp_assign m self pp_var fmt var_type var_name value = |
27 |
Format.fprintf fmt "%a = %a;" |
28 |
(pp_c_val self pp_var) var_name |
29 |
(pp_c_val self pp_var) value |
30 |
|
31 |
|
32 |
let check_type_restrictions m = |
33 |
(* Checking that all memories are of type real. Since everything should be |
34 |
inlined, only arrows instances would be allowed *) |
35 |
let is_real_var v = Types.is_real_type v.var_type in |
36 |
if not (List.for_all is_real_var m.mmemory) then ( |
37 |
Format.eprintf "Main node contains variable with non real type: %s@.@?" |
38 |
(List.find (fun v -> not (is_real_var v)) m.mmemory).var_id ; |
39 |
assert false |
40 |
) else |
41 |
Format.printf " - All variables are real: OK@."; |
42 |
|
43 |
|
44 |
let call_name (_, (td, _)) = node_name td in |
45 |
let is_arrow_call c = call_name c = "_arrow" in |
46 |
if not (List.for_all is_arrow_call m.minstances) then ( |
47 |
Format.eprintf "All calls are not inlined: call to node %s@.@?" |
48 |
(call_name (List.find (fun c -> not (is_arrow_call c)) m.minstances)) ; |
49 |
assert false |
50 |
) else |
51 |
Format.printf " - All calls inlined: OK@." |
52 |
|
53 |
|
54 |
|
55 |
let rec pp_conditional (m: machine_t) self fmt c tl el = |
56 |
Format.fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}" |
57 |
(pp_c_val self pp_var) c |
58 |
(Utils.pp_newline_if_non_empty tl) |
59 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) tl |
60 |
(Utils.pp_newline_if_non_empty el) |
61 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) el |
62 |
|
63 |
and pp_machine_instr (m: machine_t) self fmt instr = |
64 |
match instr with |
65 |
| MReset i -> assert false (* no reset allowed *) |
66 |
| MLocalAssign (i,v) -> |
67 |
pp_assign m self pp_var fmt i.var_type (LocalVar i) v |
68 |
| MStateAssign (i,v) (* state variable are handled as local ones *) |
69 |
-> pp_assign m self pp_var fmt i.var_type (StateVar i) v |
70 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
71 |
pp_machine_instr m self fmt (MLocalAssign (i0, Fun (i, vl))) |
72 |
| MStep (il, i, vl) -> |
73 |
assert false (* no calls *) |
74 |
| MBranch (g,hl) -> |
75 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false |
76 |
then (* boolean case, needs special treatment in C because truth value is not unique *) |
77 |
(* may disappear if we optimize code by replacing last branch test with default *) |
78 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
79 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
80 |
pp_conditional m self fmt g tl el |
81 |
else (* enum type case *) |
82 |
assert false |
83 |
|
84 |
let rec extract_init_step m instrs = |
85 |
let extract = extract_init_step m in |
86 |
let f instr = |
87 |
match instr with |
88 |
| MReset i -> assert false (* no reset allowed *) |
89 |
| MLocalAssign _ |
90 |
| MStateAssign _ -> instr, instr |
91 |
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i -> |
92 |
let instr = MLocalAssign (i0, Fun (i, vl)) in |
93 |
instr, instr |
94 |
| MStep (il, i, vl) -> ( |
95 |
let (n,_) = List.assoc i m.minstances in |
96 |
match node_name n, vl, il with |
97 |
| "_arrow", [i1; i2], [o] -> |
98 |
MLocalAssign(o, i1), MLocalAssign(o, i2) |
99 |
| _ -> assert false (* no calls allowed *) |
100 |
) |
101 |
|
102 |
| MBranch (g,hl) -> |
103 |
if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false |
104 |
then |
105 |
let tl = try List.assoc tag_true hl with Not_found -> [] in |
106 |
let el = try List.assoc tag_false hl with Not_found -> [] in |
107 |
let tl_init, tl_step = extract tl in |
108 |
let el_init, el_step = extract el in |
109 |
MBranch(g, [tag_true, tl_init; tag_false, el_init]), |
110 |
MBranch(g, [tag_true, el_init; tag_false, el_step]) |
111 |
else (* enum type case *) |
112 |
assert false |
113 |
in |
114 |
List.fold_right |
115 |
(fun i (init, step) -> let i_i, i_s = f i in i_i::init, i_s::step) |
116 |
instrs |
117 |
([], []) |
118 |
|
119 |
let rec filter_bool_assigns instrs = |
120 |
let filter_instr instr res = |
121 |
match instr with |
122 |
| MReset i -> assert false (* no reset allowed *) |
123 |
| MLocalAssign (i,v) when not (Types.is_real_type i.var_type) -> res |
124 |
| MLocalAssign _ |
125 |
| MStateAssign _ -> instr::res |
126 |
| MStep _ -> instr::res |
127 |
| MBranch (g,hl) -> MBranch(g, List.map (fun (t,il) -> t, filter_bool_assigns il) hl)::res |
128 |
in |
129 |
List.fold_right filter_instr instrs [] |
130 |
|
131 |
let pp_randomized_input fmt v = |
132 |
Format.fprintf fmt "%s = rand(-1, 1);" v.var_id |
133 |
|
134 |
let translate fmt basename normalized_prog machines = |
135 |
(* No modular compilation: require a main node *) |
136 |
let main_node = |
137 |
match !Options.main_node with |
138 |
| "" -> failwith "Main node required for riny backend" |
139 |
| main_node -> ( |
140 |
match Machine_code.get_machine_opt main_node machines with |
141 |
| None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; assert false |
142 |
| Some m -> m |
143 |
) |
144 |
in |
145 |
|
146 |
(* Verify that we have only real variables (no bool nor int) *) |
147 |
check_type_restrictions main_node; |
148 |
|
149 |
(* Project instrs to init and step versions *) |
150 |
let init, step = extract_init_step main_node main_node.mstep.step_instrs in |
151 |
let init = Optimize_machine.instrs_fusion init in |
152 |
let step = Optimize_machine.instrs_fusion step in |
153 |
(* Removing bool assigns that remain from _arrow *) |
154 |
let init = filter_bool_assigns init in |
155 |
let step = filter_bool_assigns step in |
156 |
(* Print the step instructions with all arrows to true *) |
157 |
Format.fprintf fmt "@[<v 0>%a@ @[<v 2>while (0. < 1.) {@ %a@ %a@]@ }@ @]@." |
158 |
(* Printing first loop body *) |
159 |
(Utils.fprintf_list ~sep:"@ " |
160 |
(pp_machine_instr main_node main_node.mname.node_id)) |
161 |
init |
162 |
(* Randomized inputs *) |
163 |
(Utils.fprintf_list ~sep:"@ " |
164 |
pp_randomized_input) |
165 |
main_node.mstep.step_inputs |
166 |
(* Loop body *) |
167 |
(Utils.fprintf_list ~sep:"@ " |
168 |
(pp_machine_instr main_node main_node.mname.node_id)) |
169 |
step; |
170 |
(* Print only the main node (should have been inlined) *) |
171 |
|
172 |
(* Each input is declared as a in = rand(min, max); *) |
173 |
|
174 |
|
175 |
() |
176 |
|
177 |
(* Local Variables: *) |
178 |
(* compile-command:"make -C ../../.." *) |
179 |
(* End: *) |