Revision 3b2bd83d src/machine_code.ml
src/machine_code.ml  

21  21  
22  22 
module ISet = Set.Make(OrdVarDecl) 
23  23  
24 
type value_t = 

25 
 Cst of constant 

26 
 LocalVar of var_decl 

27 
 StateVar of var_decl 

28 
 Fun of ident * value_t list 

29 
 Array of value_t list 

30 
 Access of value_t * value_t 

31 
 Power of value_t * value_t 

32  
33 
type instr_t = 

34 
 MLocalAssign of var_decl * value_t 

35 
 MStateAssign of var_decl * value_t 

36 
 MReset of ident 

37 
 MStep of var_decl list * ident * value_t list 

38 
 MBranch of value_t * (label * instr_t list) list 

39  
40  24 
let rec pp_val fmt v = 
41 
match v with 

42 
 Cst c > Printers.pp_const fmt c 

25 
match v.value_desc with


26 
 Cst c > Printers.pp_const fmt c


43  27 
 LocalVar v > Format.pp_print_string fmt v.var_id 
44  28 
 StateVar v > Format.pp_print_string fmt v.var_id 
45  29 
 Array vl > Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl 
...  ...  
52  36 
 MLocalAssign (i,v) > Format.fprintf fmt "%s<l %a" i.var_id pp_val v 
53  37 
 MStateAssign (i,v) > Format.fprintf fmt "%s<s %a" i.var_id pp_val v 
54  38 
 MReset i > Format.fprintf fmt "reset %s" i 
39 
 MNoReset i > Format.fprintf fmt "noreset %s" i 

55  40 
 MStep (il, i, vl) > 
56  41 
Format.fprintf fmt "%a = %s (%a)" 
57  42 
(Utils.fprintf_list ~sep:", " (fun fmt v > Format.pp_print_string fmt v.var_id)) il 
...  ...  
61  46 
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]" 
62  47 
pp_val g 
63  48 
(Utils.fprintf_list ~sep:"@," pp_branch) hl 
49 
 MComment s > Format.pp_print_string fmt s 

64  50  
65  51 
and pp_branch fmt (t, h) = 
66  52 
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h 
...  ...  
119  105 
(fun fmt > match m.mspec with  None > ()  Some spec > Printers.pp_spec fmt spec) 
120  106 
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot 
121  107  
108 
let rec is_const_value v = 

109 
match v.value_desc with 

110 
 Cst _ > true 

111 
 Fun (id, args) > Basic_library.is_value_internal_fun v && List.for_all is_const_value args 

112 
 _ > false 

113  
122  114 
(* Returns the declared stateless status and the computed one. *) 
123  115 
let get_stateless_status m = 
124  116 
(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless) 
...  ...  
144  136 
var_dec_const = false; 
145  137 
var_dec_value = None; 
146  138 
var_type = typ; 
147 
var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;


139 
var_clock = Clocks.new_ck Clocks.Cvar true;


148  140 
var_loc = Location.dummy_loc 
149  141 
} 
150  142  
...  ...  
177  169 
top_decl_loc = Location.dummy_loc 
178  170 
} 
179  171  
172 
let mk_val v t = { value_desc = v; 

173 
value_type = t; 

174 
value_annot = None } 

175  
180  176 
let arrow_machine = 
181  177 
let state = "_first" in 
182  178 
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in 
183  179 
let var_input1 = List.nth arrow_desc.node_inputs 0 in 
184  180 
let var_input2 = List.nth arrow_desc.node_inputs 1 in 
185  181 
let var_output = List.nth arrow_desc.node_outputs 0 in 
182 
let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in 

183 
let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *) 

186  184 
{ 
187  185 
mname = arrow_desc; 
188  186 
mmemory = [var_state]; 
189  187 
mcalls = []; 
190  188 
minstances = []; 
191 
minit = [MStateAssign(var_state, Cst (const_of_bool true))]; 

192 
mconst = []; 

189 
minit = [MStateAssign(var_state, cst true)]; 

193  190 
mstatic = []; 
191 
mconst = []; 

194  192 
mstep = { 
195  193 
step_inputs = arrow_desc.node_inputs; 
196  194 
step_outputs = arrow_desc.node_outputs; 
197  195 
step_locals = []; 
198  196 
step_checks = []; 
199 
step_instrs = [conditional (StateVar var_state) 

200 
[MStateAssign(var_state, Cst (const_of_bool false)); 

201 
MLocalAssign(var_output, LocalVar var_input1)] 

202 
[MLocalAssign(var_output, LocalVar var_input2)] ]; 

197 
step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool) 

198 
[MStateAssign(var_state, cst false); 

199 
MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)] 

200 
[MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)] ]; 

201 
step_asserts = []; 

202 
}; 

203 
mspec = None; 

204 
mannot = []; 

205 
} 

206  
207 
let empty_desc = 

208 
{ 

209 
node_id = arrow_id; 

210 
node_type = Types.bottom; 

211 
node_clock = Clocks.bottom; 

212 
node_inputs= []; 

213 
node_outputs= []; 

214 
node_locals= []; 

215 
node_gencalls = []; 

216 
node_checks = []; 

217 
node_asserts = []; 

218 
node_stmts= []; 

219 
node_dec_stateless = true; 

220 
node_stateless = Some true; 

221 
node_spec = None; 

222 
node_annot = []; } 

223  
224 
let empty_machine = 

225 
{ 

226 
mname = empty_desc; 

227 
mmemory = []; 

228 
mcalls = []; 

229 
minstances = []; 

230 
minit = []; 

231 
mstatic = []; 

232 
mconst = []; 

233 
mstep = { 

234 
step_inputs = []; 

235 
step_outputs = []; 

236 
step_locals = []; 

237 
step_checks = []; 

238 
step_instrs = []; 

203  239 
step_asserts = []; 
204  240 
}; 
205  241 
mspec = None; 
...  ...  
233  269 
try (* id is a node var *) 
234  270 
let var_id = get_node_var id node in 
235  271 
if ISet.exists (fun v > v.var_id = id) m 
236 
then StateVar var_id


237 
else LocalVar var_id


272 
then mk_val (StateVar var_id) var_id.var_type


273 
else mk_val (LocalVar var_id) var_id.var_type


238  274 
with Not_found > 
239  275 
try (* id is a constant *) 
240 
LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) 

276 
let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in 

277 
mk_val (LocalVar vdecl) vdecl.var_type 

241  278 
with Not_found > 
242  279 
(* id is a tag *) 
243 
Cst (Const_tag id) 

280 
(* DONE construire une liste des enum declarés et alors chercher dedans la liste 

281 
qui contient id *) 

282 
try 

283 
let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in 

284 
mk_val (Cst (Const_tag id)) (Type_predef.type_const typ) 

285 
with Not_found > (Format.eprintf "internal error: Machine_code.translate_ident %s" id; 

286 
assert false) 

244  287  
245  288 
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst = 
246  289 
match (Clocks.repr ck).cdesc with 
...  ...  
292  335 
 "C" > specialize_to_c expr 
293  336 
 _ > expr 
294  337  
295 
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =


338 
let rec translate_expr node ((m, si, j, d, s) as args) expr = 

296  339 
let expr = specialize_op expr in 
297 
match expr.expr_desc with


298 
 Expr_const v > Cst v


299 
 Expr_ident x > translate_ident node args x


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


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


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


303 
 Expr_tuple _


304 
 Expr_arrow _


305 
 Expr_fby _


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


307 
 Expr_when (e1, _, _) > translate_expr node args e1


308 
 Expr_merge (x, _) > raise NormalizationError


309 
 Expr_appl (id, e, _) when Basic_library.is_internal_fun id >


310 
let nd = node_from_name id in


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


312 
 Expr_ite (g,t,e) > (


313 
(* special treatment depending on the active backend. For horn backend, ite


314 
are preserved in expression. While they are removed for C or Java


315 
backends. *)


316 
match !Options.output with


317 
 "horn" >


318 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])


319 
 ("C"  "java") when ite >


320 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])


321 
 _ >


322 
(Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)


323 
)


324 
 _ > raise NormalizationError


340 
let value_desc =


341 
match expr.expr_desc with


342 
 Expr_const v > Cst v


343 
 Expr_ident x > (translate_ident node args x).value_desc


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


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


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


347 
 Expr_tuple _


348 
 Expr_arrow _


349 
 Expr_fby _


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


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


352 
 Expr_merge (x, _) > raise NormalizationError


353 
 Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr >


354 
let nd = node_from_name id in


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


356 
(* Expr_ite (g,t,e) > (


357 
(* special treatment depending on the active backend. For horn backend, ite


358 
are preserved in expression. While they are removed for C or Java


359 
backends. *)


360 
match !Options.output with  "horn" >


361 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])


362 
 "C"  "java"  _ >


363 
(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)


364 
)*)


365 
 _ > raise NormalizationError


366 
in


367 
mk_val value_desc expr.expr_type


325  368  
326  369 
let translate_guard node args expr = 
327  370 
match expr.expr_desc with 
...  ...  
331  374 
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) = 
332  375 
match expr.expr_desc with 
333  376 
 Expr_ite (c, t, e) > let g = translate_guard node args c in 
334 
conditional g [translate_act node args (y, t)] 

377 
conditional g 

378 
[translate_act node args (y, t)] 

335  379 
[translate_act node args (y, e)] 
336 
 Expr_merge (x, hl) > MBranch (translate_ident node args x, List.map (fun (t, h) > t, [translate_act node args (y, h)]) hl)


337 
 _ >


338 
MLocalAssign (y, translate_expr node args expr)


380 
 Expr_merge (x, hl) > MBranch (translate_ident node args x, 

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


382 
 _ > MLocalAssign (y, translate_expr node args expr)


339  383  
340  384 
let reset_instance node args i r c = 
341  385 
match r with 
342  386 
 None > [] 
343  387 
 Some r > let g = translate_guard node args r in 
344 
[control_on_clock node args c (conditional g [MReset i] [])] 

388 
[control_on_clock node args c (conditional g [MReset i] [MNoReset i])]


345  389  
346  390 
let translate_eq node ((m, si, j, d, s) as args) eq = 
347  391 
(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *) 
...  ...  
371  415 
d, 
372  416 
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s) 
373  417  
374 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) >


418 
 p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >


375  419 
let var_p = List.map (fun v > get_node_var v node) p in 
376  420 
let el = expr_list_of_expr arg in 
377  421 
let vl = List.map (translate_expr node args) el in 
...  ...  
393  437 
then [] 
394  438 
else reset_instance node args o r call_ck) @ 
395  439 
(control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s) 
396  
440 
(* 

397  441 
(* special treatment depending on the active backend. For horn backend, x = ite (g,t,e) 
398  442 
are preserved. While they are replaced as if g then x = t else x = e in C or Java 
399  443 
backends. *) 
...  ...  
409  453 
(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s) 
410  454 
) 
411  455  
456 
*) 

412  457 
 [x], _ > ( 
413  458 
let var_x = get_node_var x node in 
414  459 
(m, si, j, d, 
...  ...  
421  466 
) 
422  467 
 _ > 
423  468 
begin 
424 
Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq;


469 
Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;


425  470 
assert false 
426  471 
end 
427  472  
...  ...  
444  489 
to the computed schedule [sch] 
445  490 
*) 
446  491 
let sort_equations_from_schedule nd sch = 
447 
(*Format.eprintf "%s schedule: %a@."


448 
nd.node_id


449 
(Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)


492 
(* Format.eprintf "%s schedule: %a@." *)


493 
(* nd.node_id *)


494 
(* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *)


450  495 
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in 
451  496 
let eqs_rev, remainder = 
452  497 
List.fold_left 
...  ...  
515  560 
(* special treatment depending on the active backend. For horn backend, 
516  561 
common branches are not merged while they are in C or Java 
517  562 
backends. *) 
518 
match !Options.output with 

563 
(*match !Options.output with


519  564 
 "horn" > s 
520 
 "C"  "java"  _ > join_guards_list s 

565 
 "C"  "java"  _ >*) join_guards_list s


521  566 
); 
522  567 
step_asserts = 
523  568 
let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in 
...  ...  
554  599 
with Not_found > assert false 
555  600  
556  601  
557 
let value_of_ident m id = 

602 
let value_of_ident loc m id =


558  603 
(* is is a state var *) 
559  604 
try 
560 
StateVar (List.find (fun v > v.var_id = id) m.mmemory) 

605 
let v = List.find (fun v > v.var_id = id) m.mmemory 

606 
in mk_val (StateVar v) v.var_type 

561  607 
with Not_found > 
562 
try (* id is a node var *) 

563 
LocalVar (get_node_var id m.mname) 

608 
try (* id is a node var *) 

609 
let v = get_node_var id m.mname 

610 
in mk_val (LocalVar v) v.var_type 

564  611 
with Not_found > 
565  612 
try (* id is a constant *) 
566 
LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) 

613 
let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)) 

614 
in mk_val (LocalVar c) c.var_type 

567  615 
with Not_found > 
568  616 
(* id is a tag *) 
569 
Cst (Const_tag id) 

617 
let t = Const_tag id 

618 
in mk_val (Cst t) (Typing.type_const loc t) 

619  
620 
(* type of internal fun used in dimension expression *) 

621 
let type_of_value_appl f args = 

622 
if List.mem f Basic_library.arith_funs 

623 
then (List.hd args).value_type 

624 
else Type_predef.type_bool 

570  625  
571  626 
let rec value_of_dimension m dim = 
572  627 
match dim.Dimension.dim_desc with 
573 
 Dimension.Dbool b > Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false)) 

574 
 Dimension.Dint i > Cst (Const_int i) 

575 
 Dimension.Dident v > value_of_ident m v 

576 
 Dimension.Dappl (f, args) > Fun (f, List.map (value_of_dimension m) args) 

577 
 Dimension.Dite (i, t, e) > Fun ("ite", List.map (value_of_dimension m) [i; t; e]) 

628 
 Dimension.Dbool b > 

629 
mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool 

630 
 Dimension.Dint i > 

631 
mk_val (Cst (Const_int i)) Type_predef.type_int 

632 
 Dimension.Dident v > value_of_ident dim.Dimension.dim_loc m v 

633 
 Dimension.Dappl (f, args) > 

634 
let vargs = List.map (value_of_dimension m) args 

635 
in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) 

636 
 Dimension.Dite (i, t, e) > 

637 
(match List.map (value_of_dimension m) [i; t; e] with 

638 
 [vi; vt; ve] > mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type 

639 
 _ > assert false) 

578  640 
 Dimension.Dlink dim' > value_of_dimension m dim' 
579  641 
 _ > assert false 
580  642  
581  643 
let rec dimension_of_value value = 
582 
match value with 

644 
match value.value_desc with


583  645 
 Cst (Const_tag t) when t = Corelang.tag_true > Dimension.mkdim_bool Location.dummy_loc true 
584  646 
 Cst (Const_tag t) when t = Corelang.tag_false > Dimension.mkdim_bool Location.dummy_loc false 
585  647 
 Cst (Const_int i) > Dimension.mkdim_int Location.dummy_loc i 
Also available in: Unified diff