Revision 59020713 src/machine_code.ml
src/machine_code.ml  

20  20  
21  21  
22  22 

23 
(* translate_<foo> : node > context > <foo> > machine code/expression *)


23 
(* translate_<foo> : vars > context > <foo> > machine code/expression *)


24  24 
(* the context contains m : state aka memory variables *) 
25  25 
(* si : initialization instructions *) 
26  26 
(* j : node aka machine instances *) 
27  27 
(* d : local variables *) 
28  28 
(* s : step instructions *) 
29 
let translate_ident node (m, si, j, d, s) id =


29 
let translate_ident vars _ (* (m, si, j, d, s) *) id =


30  30 
(* Format.eprintf "trnaslating ident: %s@." id; *) 
31 
try (* id is a node var *)


32 
let var_id = get_node_var id node in


31 
try (* id is a var that shall be visible here , ie. in vars *)


32 
let var_id = get_var id vars in


33  33 
mk_val (Var var_id) var_id.var_type 
34  34 
with Not_found > 
35  35 
try (* id is a constant *) 
36 
let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in 

36 
let vdecl = (Corelang.var_decl_of_const 

37 
(const_of_top (Hashtbl.find Corelang.consts_table id))) 

38 
in 

37  39 
mk_val (Var vdecl) vdecl.var_type 
38  40 
with Not_found > 
39  41 
(* id is a tag *) 
40 
(* DONE construire une liste des enum declarés et alors chercher dedans la liste


41 
qui contient id *)


42 
(* DONE construire une liste des enum declarés et alors chercher 

43 
dedans la liste qui contient id *)


42  44 
try 
43  45 
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in 
44  46 
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) 
45 
with Not_found > (Format.eprintf "internal error: Machine_code.translate_ident %s" id; 

47 
with Not_found > (Format.eprintf 

48 
"internal error: Machine_code.translate_ident %s" 

49 
id; 

46  50 
assert false) 
47  51  
48 
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =


52 
let rec control_on_clock vars ((m, si, j, d, s) as args) ck inst =


49  53 
match (Clocks.repr ck).cdesc with 
50  54 
 Con (ck1, cr, l) > 
51  55 
let id = Clocks.const_of_carrier cr in 
52 
control_on_clock node args ck1 (mkinstr


56 
control_on_clock vars args ck1 (mkinstr


53  57 
(* TODO il faudrait prendre le lustre 
54  58 
associé à instr et rajouter print_ck_suffix 
55  59 
ck) de clocks.ml *) 
56 
(MBranch (translate_ident node args id,


60 
(MBranch (translate_ident vars args id,


57  61 
[l, [inst]] ))) 
58  62 
 _ > inst 
59  63  
...  ...  
79  83 
 "C" > specialize_to_c expr 
80  84 
 _ > expr 
81  85  
82 
let rec translate_expr node ((m, si, j, d, s) as args) expr =


86 
let rec translate_expr vars ((m, si, j, d, s) as args) expr =


83  87 
let expr = specialize_op expr in 
88 
(* all calls are using the same arguments (vars for the variable 

89 
enviroment and args for computed memories). No fold constructs 

90 
here. We can do partial evaluation of translate_expr *) 

91 
let translate_expr = translate_expr vars args in 

84  92 
let value_desc = 
85  93 
match expr.expr_desc with 
86  94 
 Expr_const v > Cst v 
87 
 Expr_ident x > (translate_ident node args x).value_desc 

88 
 Expr_array el > Array (List.map (translate_expr node args) el) 

89 
 Expr_access (t, i) > Access (translate_expr node args t, translate_expr node args (expr_of_dimension i)) 

90 
 Expr_power (e, n) > Power (translate_expr node args e, translate_expr node args (expr_of_dimension n)) 

95 
 Expr_ident x > (translate_ident vars args x).value_desc 

96 
 Expr_array el > Array (List.map translate_expr el) 

97 
 Expr_access (t, i) > Access (translate_expr t, 

98 
translate_expr 

99 
(expr_of_dimension i)) 

100 
 Expr_power (e, n) > Power (translate_expr e, 

101 
translate_expr 

102 
(expr_of_dimension n)) 

91  103 
 Expr_tuple _ 
92 
 Expr_arrow _ 

93 
 Expr_fby _ 

94 
 Expr_pre _ > (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 

95 
 Expr_when (e1, _, _) > (translate_expr node args e1).value_desc 

104 
 Expr_arrow _ 

105 
 Expr_fby _ 

106 
 Expr_pre _ > (Printers.pp_expr 

107 
Format.err_formatter expr; 

108 
Format.pp_print_flush 

109 
Format.err_formatter (); 

110 
raise NormalizationError) 

111 


112 
 Expr_when (e1, _, _) > (translate_expr e1).value_desc 

96  113 
 Expr_merge (x, _) > raise NormalizationError 
97  114 
 Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr > 
98 
let nd = node_from_name id in 

99 
Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))


115 
let nd = node_from_name id in


116 
Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))


100  117 
 Expr_ite (g,t,e) > ( 
101  118 
(* special treatment depending on the active backend. For horn backend, ite 
102  119 
are preserved in expression. While they are removed for C or Java 
103  120 
backends. *) 
104  121 
match !Options.output with 
105  122 
 "horn" > 
106 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])


123 
Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])


107  124 
 "C"  "java"  _ > 
108  125 
(Format.eprintf "Normalization error for backend %s: %a@." 
109  126 
!Options.output 
...  ...  
114  131 
in 
115  132 
mk_val value_desc expr.expr_type 
116  133  
117 
let translate_guard node args expr =


134 
let translate_guard vars args expr =


118  135 
match expr.expr_desc with 
119 
 Expr_ident x > translate_ident node args x 

120 
 _ > (Format.eprintf "internal error: translate_guard %s %a@." node.node_id Printers.pp_expr expr;assert false) 

136 
 Expr_ident x > translate_ident vars args x 

137 
 _ > (Format.eprintf "internal error: translate_guard %a@." 

138 
Printers.pp_expr expr; 

139 
assert false) 

121  140  
122 
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = 

141 
let rec translate_act vars ((m, si, j, d, s) as args) (y, expr) = 

142 
let translate_act = translate_act vars args in 

143 
let translate_guard = translate_guard vars args in 

144 
let translate_ident = translate_ident vars args in 

145 
let translate_expr = translate_expr vars args in 

123  146 
let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in 
124  147 
match expr.expr_desc with 
125 
 Expr_ite (c, t, e) > let g = translate_guard node args c in


148 
 Expr_ite (c, t, e) > let g = translate_guard c in 

126  149 
mk_conditional ?lustre_eq:(Some eq) g 
127 
[translate_act node args (y, t)] 

128 
[translate_act node args (y, e)] 

129 
 Expr_merge (x, hl) > mkinstr ?lustre_eq:(Some eq) (MBranch (translate_ident node args x, 

130 
List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl)) 

131 
 _ > mkinstr ?lustre_eq:(Some eq) (MLocalAssign (y, translate_expr node args expr)) 

150 
[translate_act (y, t)] 

151 
[translate_act (y, e)] 

152 
 Expr_merge (x, hl) > mkinstr ?lustre_eq:(Some eq) 

153 
(MBranch (translate_ident x, 

154 
List.map (fun (t, h) > 

155 
t, [translate_act (y, h)]) 

156 
hl)) 

157 
 _ > mkinstr ?lustre_eq:(Some eq) 

158 
(MLocalAssign (y, translate_expr expr)) 

132  159  
133 
let reset_instance node args i r c =


160 
let reset_instance vars args i r c =


134  161 
match r with 
135  162 
 None > [] 
136 
 Some r > let g = translate_guard node args r in 

137 
[control_on_clock node args c (mk_conditional g [mkinstr (MReset i)] [mkinstr (MNoReset i)])] 

163 
 Some r > let g = translate_guard vars args r in 

164 
[control_on_clock 

165 
vars 

166 
args 

167 
c 

168 
(mk_conditional 

169 
g 

170 
[mkinstr (MReset i)] 

171 
[mkinstr (MNoReset i)]) 

172 
] 

173  
174 
let translate_eq vars ((m, si, j, d, s) as args) eq = 

175 
let translate_expr = translate_expr vars args in 

176 
let translate_act = translate_act vars args in 

177 
let control_on_clock = control_on_clock vars args in 

178 
let reset_instance = reset_instance vars args in 

138  179  
139 
let translate_eq node ((m, si, j, d, s) as args) eq =


140 
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)


180 
(* Format.eprintf "translate_eq %a with clock %a@."


181 
Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)


141  182 
match eq.eq_lhs, eq.eq_rhs.expr_desc with 
142  183 
 [x], Expr_arrow (e1, e2) > 
143 
let var_x = get_node_var x node in


144 
let o = new_instance node Arrow.arrow_top_decl eq.eq_rhs.expr_tag in


145 
let c1 = translate_expr node args e1 in


146 
let c2 = translate_expr node args e2 in


184 
let var_x = get_var x vars in


185 
let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in 

186 
let c1 = translate_expr e1 in 

187 
let c2 = translate_expr e2 in 

147  188 
(m, 
148  189 
mkinstr (MReset o) :: si, 
149  190 
Utils.IMap.add o (Arrow.arrow_top_decl, []) j, 
150  191 
d, 
151 
(control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s)


152 
 [x], Expr_pre e1 when VSet.mem (get_node_var x node) d >


153 
let var_x = get_node_var x node in


192 
(control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))) :: s) 

193 
 [x], Expr_pre e1 when VSet.mem (get_var x vars) d >


194 
let var_x = get_var x vars in


154  195 
(VSet.add var_x m, 
155  196 
si, 
156  197 
j, 
157  198 
d, 
158 
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1))) :: s)


159 
 [x], Expr_fby (e1, e2) when VSet.mem (get_node_var x node) d >


160 
let var_x = get_node_var x node in


199 
control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1))) :: s)


200 
 [x], Expr_fby (e1, e2) when VSet.mem (get_var x vars) d >


201 
let var_x = get_var x vars in


161  202 
(VSet.add var_x m, 
162 
mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e1)) :: si,


203 
mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e1)) :: si, 

163  204 
j, 
164  205 
d, 
165 
control_on_clock node args eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr node args e2))) :: s)


206 
control_on_clock eq.eq_rhs.expr_clock (mkinstr ?lustre_eq:(Some eq) (MStateAssign (var_x, translate_expr e2))) :: s)


166  207  
167  208 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) > 
168 
let var_p = List.map (fun v > get_node_var v node) p in


209 
let var_p = List.map (fun v > get_var v vars) p in


169  210 
let el = expr_list_of_expr arg in 
170 
let vl = List.map (translate_expr node args) el in


211 
let vl = List.map translate_expr el in


171  212 
let node_f = node_from_name f in 
172  213 
let call_f = 
173  214 
node_f, 
174  215 
NodeDep.filter_static_inputs (node_inputs node_f) el in 
175 
let o = new_instance node node_f eq.eq_rhs.expr_tag in


216 
let o = new_instance node_f eq.eq_rhs.expr_tag in 

176  217 
let env_cks = List.fold_right (fun arg cks > arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in 
177  218 
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in 
178  219 
(*Clocks.new_var true in 
...  ...  
184  225 
d, 
185  226 
(if Stateless.check_node node_f 
186  227 
then [] 
187 
else reset_instance node args o r call_ck) @


188 
(control_on_clock node args call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s)


228 
else reset_instance o r call_ck) @ 

229 
(control_on_clock call_ck (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl)))) :: s) 

189  230 
(* 
190  231 
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) 
191  232 
are preserved. While they are replaced as if g then x = t else x = e in C or Java 
...  ...  
204  245  
205  246 
*) 
206  247 
 [x], _ > ( 
207 
let var_x = get_node_var x node in


248 
let var_x = get_var x vars in


208  249 
(m, si, j, d, 
209  250 
control_on_clock 
210 
node 

211 
args 

212  251 
eq.eq_rhs.expr_clock 
213 
(translate_act node args (var_x, eq.eq_rhs)) :: s


252 
(translate_act (var_x, eq.eq_rhs)) :: s 

214  253 
) 
215  254 
) 
216  255 
 _ > 
...  ...  
235  274 
let translate_eqs node args eqs = 
236  275 
List.fold_right (fun eq args > translate_eq node args eq) eqs args;; 
237  276  
238 
let translate_decl nd sch = 

239 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 

240 
let schedule = sch.Scheduling_type.schedule in 

241 
let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in 

242 
let constant_eqs = constant_equations nd in 

243  
244 
(* In case of non functional backend (eg. C), additional local variables have 

245 
to be declared for each assert *) 

246 
let new_locals, assert_instrs, nd_node_asserts = 

277 
let process_asserts nd = 

278 


247  279 
let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in 
248  280 
if Backends.is_functional () then 
249  281 
[], [], exprl 
...  ...  
267  299 
in 
268  300 
assert_var.var_type < Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); 
269  301 
let eq = mkeq loc ([var_id], expr) in 
270 
(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)


302 
(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)


271  303 
) (1, [], [], []) exprl 
272  304 
in 
273  305 
vars, eql, assertl 
274 
in 

275 
let locals_list = nd.node_locals @ new_locals in 

306 


307 
let translate_decl nd sch = 

308 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 

309 
let schedule = sch.Scheduling_type.schedule in 

310 
let sorted_eqs = Scheduling.sort_equations_from_schedule nd schedule in 

311 
let constant_eqs = constant_equations nd in 

276  312  
313 
(* In case of non functional backend (eg. C), additional local variables have 

314 
to be declared for each assert *) 

315 
let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in 

316 
let locals_list = nd.node_locals @ new_locals in 

277  317 
let nd = { nd with node_locals = locals_list } in 
318 
let vars = get_node_vars nd in 

319 


278  320 
let init_args = VSet.empty, [], Utils.IMap.empty, List.fold_right (fun l > VSet.add l) locals_list VSet.empty, [] in 
279  321 
(* memories, init instructions, node calls, local variables (including memories), step instrs *) 
280 
let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in 

322  
323 
let m0, init0, j0, locals0, s0 = 

324 
translate_eqs vars init_args constant_eqs 

325 
in 

326  
281  327 
assert (VSet.is_empty m0); 
282  328 
assert (init0 = []); 
283  329 
assert (Utils.IMap.is_empty j0); 
284 
let m, init, j, locals, s as context_with_asserts = translate_eqs nd (m0, init0, j0, locals0, []) (assert_instrs@sorted_eqs) in 

330  
331 
let m, init, j, locals, s as context_with_asserts = 

332 
translate_eqs 

333 
vars 

334 
(m0, init0, j0, locals0, []) 

335 
(assert_instrs@sorted_eqs) 

336 
in 

285  337 
let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in 
286  338 
{ 
287  339 
mname = nd; 
...  ...  
295  347 
step_inputs = nd.node_inputs; 
296  348 
step_outputs = nd.node_outputs; 
297  349 
step_locals = VSet.elements (VSet.diff locals m); 
298 
step_checks = List.map (fun d > d.Dimension.dim_loc, translate_expr nd init_args (expr_of_dimension d)) nd.node_checks; 

350 
step_checks = List.map (fun d > d.Dimension.dim_loc, 

351 
translate_expr vars init_args 

352 
(expr_of_dimension d)) 

353 
nd.node_checks; 

299  354 
step_instrs = ( 
300  355 
(* special treatment depending on the active backend. For horn backend, 
301  356 
common branches are not merged while they are in C or Java 
...  ...  
308  363 
else 
309  364 
s 
310  365 
); 
311 
step_asserts = List.map (translate_expr nd context_with_asserts) nd_node_asserts;


366 
step_asserts = List.map (translate_expr vars context_with_asserts) nd_node_asserts;


312  367 
}; 
313  368 
mspec = nd.node_spec; 
314  369 
mannot = nd.node_annot; 
Also available in: Unified diff