Revision 75c459f4
Added by LĂ©lio Brun 9 months ago
src/machine_code.ml  

12  12 
open Lustre_types 
13  13 
open Machine_code_types 
14  14 
open Machine_code_common 
15 
open Spec_types 

16 
open Spec_common 

15  17 
open Corelang 
16  18 
open Clocks 
17  19 
open Causality 
20 
open Utils 

18  21  
19  22 
exception NormalizationError 
20  23  
...  ...  
58  61  
59  62 
let translate_ident env id = 
60  63 
(* Format.eprintf "trnaslating ident: %s@." id; *) 
61 
try (* id is a var that shall be visible here , ie. in vars *) 

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

65 
try 

62  66 
let var_id = env.get_var id in 
63  67 
mk_val (Var var_id) var_id.var_type 
64  68 
with Not_found > 
65 
try (* id is a constant *) 

69  
70 
(* id is a constant *) 

71 
try 

66  72 
let vdecl = (Corelang.var_decl_of_const 
67  73 
(const_of_top (Hashtbl.find Corelang.consts_table id))) 
68  74 
in 
69  75 
mk_val (Var vdecl) vdecl.var_type 
70  76 
with Not_found > 
71 
(* id is a tag, getting its type in the list of declared enums *) 

77  
78 
(* id is a tag, getting its type in the list of declared enums *) 

72  79 
try 
73  80 
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in 
74  81 
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) 
...  ...  
76  83 
Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id; 
77  84 
assert false 
78  85  
79 
let rec control_on_clock env ck inst = 

80 
match (Clocks.repr ck).cdesc with 

81 
 Con (ck1, cr, l) > 

82 
let id = Clocks.const_of_carrier cr in 

83 
control_on_clock env ck1 

84 
(mkinstr (MBranch (translate_ident env id, [l, [inst]]))) 

85 
 _ > inst 

86  
87  86  
88  87 
(* specialize predefined (polymorphic) operators wrt their instances, 
89  88 
so that the C semantics is preserved *) 
...  ...  
158  157 
[translate_act (y, t)] 
159  158 
[translate_act (y, e)] 
160  159 
 Expr_merge (x, hl) > 
161 
mkinstr ~lustre_eq 

162 
(MBranch (translate_ident x, 

163 
List.map (fun (t, h) > t, [translate_act (y, h)]) hl)) 

164 
 _ > mkinstr ~lustre_eq (MLocalAssign (y, translate_expr expr)) 

165  
166 
let reset_instance env i r c = 

167 
match r with 

168 
 Some r > 

169 
[control_on_clock env c 

170 
(mk_conditional 

171 
(translate_guard env r) 

172 
[mkinstr (MReset i)] 

173 
[mkinstr (MNoReset i)])] 

174 
 None > [] 

175  
160 
mk_branch ~lustre_eq 

161 
(translate_ident x) 

162 
(List.map (fun (t, h) > t, [translate_act (y, h)]) hl) 

163 
 _ > 

164 
mk_assign ~lustre_eq y (translate_expr expr) 

176  165  
177  166 
(* Datastructure updated while visiting equations *) 
178  167 
type machine_ctx = { 
179 
m: VSet.t; (* Memories *) 

168 
(* Memories *) 

169 
m: VSet.t; 

170 
(* Reset instructions *) 

180  171 
si: instr_t list; 
181 
j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t; 

172 
(* Instances *) 

173 
j: (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t; 

174 
(* Step instructions *) 

182  175 
s: instr_t list; 
176 
(* Memory pack spec *) 

177 
mp: mc_formula_t list; 

178 
(* Clocked spec *) 

179 
c: mc_formula_t IMap.t; 

180 
(* Transition spec *) 

181 
t: mc_formula_t list; 

183  182 
} 
184  183  
185 
let ctx_init = { m = VSet.empty; (* memories *) 

186 
si = []; (* init instr *) 

187 
j = Utils.IMap.empty; 

188 
s = [] } 

184 
let ctx_init = { 

185 
m = VSet.empty; 

186 
si = []; 

187 
j = IMap.empty; 

188 
s = []; 

189 
mp = []; 

190 
c = IMap.empty; 

191 
t = [] 

192 
} 

189  193  
190  194 
(****************************************************************) 
191  195 
(* Main function to translate equations into this machine context we 
192  196 
are building *) 
193  197 
(****************************************************************) 
194  198  
199 
let mk_control id vs v l inst = 

200 
mkinstr 

201 
(Imply (mk_clocked_on id vs, inst.instr_spec)) 

202 
(MBranch (v, [l, [inst]])) 

203  
204 
let control_on_clock env ctx ck inst = 

205 
let rec aux (ck_ids, vs, ctx, inst as acc) ck = 

206 
match (Clocks.repr ck).cdesc with 

207 
 Con (ck, cr, l) > 

208 
let id = Clocks.const_of_carrier cr in 

209 
let v = translate_ident env id in 

210 
let ck_ids' = String.concat "_" ck_ids in 

211 
let id' = id ^ "_" ^ ck_ids' in 

212 
let ck_spec = mk_condition v l in 

213 
aux (id :: ck_ids, 

214 
v :: vs, 

215 
{ ctx 

216 
with c = IMap.add id ck_spec 

217 
(IMap.add id' 

218 
(And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c) 

219 
}, 

220 
mk_control id' (v :: vs) v l inst) ck 

221 
 _ > acc 

222 
in 

223 
let _, _, ctx, inst = aux ([], [], ctx, inst) ck in 

224 
ctx, inst 

225  
226 
let reset_instance env i r c = 

227 
match r with 

228 
 Some r > 

229 
[snd (control_on_clock env ctx_init c 

230 
(mk_conditional 

231 
(translate_guard env r) 

232 
[mkinstr True (MReset i)] 

233 
[mkinstr True (MNoReset i)]))] 

234 
 None > [] 

195  235  
196  236  
197  237 
let translate_eq env ctx eq = 
198  238 
let translate_expr = translate_expr env in 
199  239 
let translate_act = translate_act env in 
200 
let control_on_clock = control_on_clock env in 

240 
let control_on_clock ck inst = 

241 
let ctx, ins = control_on_clock env ctx ck inst in 

242 
{ ctx with s = ins :: ctx.s } 

243 
in 

201  244 
let reset_instance = reset_instance env in 
202 
let mkinstr' = mkinstr ~lustre_eq:eq in 

245 
let mkinstr' = mkinstr ~lustre_eq:eq True in


203  246 
let ctl ?(ck=eq.eq_rhs.expr_clock) instr = 
204  247 
control_on_clock ck (mkinstr' instr) in 
205  248  
...  ...  
211  254 
let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in 
212  255 
let c1 = translate_expr e1 in 
213  256 
let c2 = translate_expr e2 in 
257 
let ctx = ctl (MStep ([var_x], o, [c1;c2])) in 

214  258 
{ ctx with 
215 
si = mkinstr (MReset o) :: ctx.si; 

216 
j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j; 

217 
s = ctl (MStep ([var_x], o, [c1;c2])) :: ctx.s 

259 
si = mkinstr True (MReset o) :: ctx.si; 

260 
j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j; 

218  261 
} 
219  262 
 [x], Expr_pre e1 when env.is_local x > 
220  263 
let var_x = env.get_var x in 
264 
let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in 

221  265 
{ ctx with 
222  266 
m = VSet.add var_x ctx.m; 
223 
s = ctl (MStateAssign (var_x, translate_expr e1)) :: ctx.s 

224  267 
} 
225  268 
 [x], Expr_fby (e1, e2) when env.is_local x > 
226  269 
let var_x = env.get_var x in 
270 
let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in 

227  271 
{ ctx with 
228  272 
m = VSet.add var_x ctx.m; 
229  273 
si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si; 
230 
s = ctl (MStateAssign (var_x, translate_expr e2)) :: ctx.s 

231  274 
} 
232  275 
 p, Expr_appl (f, arg, r) 
233  276 
when not (Basic_library.is_expr_internal_fun eq.eq_rhs) > 
...  ...  
241  284 
el [eq.eq_rhs.expr_clock] in 
242  285 
let call_ck = Clock_calculus.compute_root_clock 
243  286 
(Clock_predef.ck_tuple env_cks) in 
287 
let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in 

244  288 
(*Clocks.new_var true in 
245  289 
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; 
246  290 
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*) 
247  291 
{ ctx with 
248  292 
si = if Stateless.check_node node_f 
249 
then ctx.si else mkinstr (MReset o) :: ctx.si; 

250 
j = Utils.IMap.add o call_f ctx.j;


293 
then ctx.si else mkinstr True (MReset o) :: ctx.si;


294 
j = IMap.add o call_f ctx.j; 

251  295 
s = (if Stateless.check_node node_f 
252 
then [] else reset_instance o r call_ck)


253 
@ ctl ~ck:call_ck (MStep (var_p, o, vl))


254 
:: ctx.s


296 
then [] 

297 
else reset_instance o r call_ck)


298 
@ ctx.s


255  299 
} 
256  300 
 [x], _ > 
257  301 
let var_x = env.get_var x in 
258 
{ ctx with 

259 
s = control_on_clock eq.eq_rhs.expr_clock 

260 
(translate_act (var_x, eq.eq_rhs)) 

261 
:: ctx.s 

262 
} 

302 
control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs)) 

263  303 
 _ > 
264  304 
Format.eprintf "internal error: Machine_code.translate_eq %a@?" 
265  305 
Printers.pp_node_eq eq; 
...  ...  
270  310 
if vdecl.var_dec_const 
271  311 
then 
272  312 
{ eq_lhs = [vdecl.var_id]; 
273 
eq_rhs = Utils.desome vdecl.var_dec_value;


313 
eq_rhs = desome vdecl.var_dec_value; 

274  314 
eq_loc = vdecl.var_loc 
275  315 
} :: eqs 
276  316 
else eqs) 
...  ...  
326  366 
let ctx0 = translate_eqs env ctx_init constant_eqs in 
327  367 
assert (VSet.is_empty ctx0.m); 
328  368 
assert (ctx0.si = []); 
329 
assert (Utils.IMap.is_empty ctx0.j);


369 
assert (IMap.is_empty ctx0.j); 

330  370  
331  371 
(* Compute ctx for all eqs *) 
332  372 
let ctx = translate_eqs env ctx_init sorted_eqs in 
...  ...  
371  411 
let l = VSet.elements (VSet.diff locals ctx.m) in 
372  412 
List.fold_left (fun res v > if List.mem v.var_id unused then res else v::res) [] l 
373  413 
in 
374 
let mmap = Utils.IMap.bindings ctx.j in


414 
let mmap = IMap.bindings ctx.j in 

375  415 
{ 
376  416 
mname = nd; 
377  417 
mmemory = VSet.elements ctx.m; 
...  ...  
417  457 
List.map 
418  458 
(fun decl > 
419  459 
let node = node_of_top decl in 
420 
let sch = Utils.IMap.find node.node_id node_schs in


460 
let sch = IMap.find node.node_id node_schs in 

421  461 
translate_decl node sch 
422  462 
) nodes 
423  463 
in 
Also available in: Unified diff
start with Spec AST generation