Revision 01d48bb0 src/machine_code.ml
src/machine_code.ml  

83  83 
minstances: (ident * static_call) list; (* submap of mcalls, from stateful instance to node *) 
84  84 
minit: instr_t list; 
85  85 
mstatic: var_decl list; (* static inputs only *) 
86 
mconst: instr_t list; (* assignments of node constant locals *) 

86  87 
mstep: step_t; 
87  88 
mspec: node_annot option; 
88  89 
mannot: expr_annot list; 
...  ...  
105  106  
106  107 
let pp_machine fmt m = 
107  108 
Format.fprintf fmt 
108 
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ " 

109 
"@[<v 2>machine %s@ mem : %a@ instances: %a@ init : %a@ const : %a@ step :@ @[<v 2>%a@]@ @ spec : @[%t@]@ annot : @[%a@]@]@ "


109  110 
m.mname.node_id 
110  111 
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory 
111  112 
(Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) > Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances 
112  113 
(Utils.fprintf_list ~sep:"@ " pp_instr) m.minit 
114 
(Utils.fprintf_list ~sep:"@ " pp_instr) m.mconst 

113  115 
pp_step m.mstep 
114  116 
(fun fmt > match m.mspec with  None > ()  Some spec > Printers.pp_spec fmt spec) 
115  117 
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot 
...  ...  
137  139 
var_dec_type = dummy_type_dec; 
138  140 
var_dec_clock = dummy_clock_dec; 
139  141 
var_dec_const = false; 
142 
var_dec_value = None; 

140  143 
var_type = typ; 
141  144 
var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true; 
142  145 
var_loc = Location.dummy_loc 
...  ...  
183  186 
mcalls = []; 
184  187 
minstances = []; 
185  188 
minit = [MStateAssign(var_state, Cst (const_of_bool true))]; 
189 
mconst = []; 

186  190 
mstatic = []; 
187  191 
mstep = { 
188  192 
step_inputs = arrow_desc.node_inputs; 
...  ...  
215  219 
o 
216  220 
end 
217  221  
222  
218  223 
(* translate_<foo> : node > context > <foo> > machine code/expression *) 
219  224 
(* the context contains m : state aka memory variables *) 
220  225 
(* si : initialization instructions *) 
...  ...  
284  289 
 "C" > specialize_to_c expr 
285  290 
 _ > expr 
286  291  
287 
let rec translate_expr node ((m, si, j, d, s) as args) expr = 

292 
let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =


288  293 
let expr = specialize_op expr in 
289  294 
match expr.expr_desc with 
290  295 
 Expr_const v > Cst v 
...  ...  
305  310 
(* special treatment depending on the active backend. For horn backend, ite 
306  311 
are preserved in expression. While they are removed for C or Java 
307  312 
backends. *) 
308 
match !Options.output with  "horn" > 

313 
match !Options.output with 

314 
 "horn" 

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

309  316 
Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e]) 
310 
 "C"  "java"  _ >


317 
 _ > 

311  318 
(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 
312  319 
) 
313  320 
 _ > raise NormalizationError 
...  ...  
433  440 
to the computed schedule [sch] 
434  441 
*) 
435  442 
let sort_equations_from_schedule nd sch = 
436 
(* Format.eprintf "%s schedule: %a@."


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

437  444 
nd.node_id 
438  445 
(Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*) 
439  446 
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in 
...  ...  
459  466 
List.rev eqs_rev 
460  467 
end 
461  468  
469 
let constant_equations nd = 

470 
List.fold_right (fun vdecl eqs > 

471 
if vdecl.var_dec_const 

472 
then 

473 
{ eq_lhs = [vdecl.var_id]; 

474 
eq_rhs = Utils.desome vdecl.var_dec_value; 

475 
eq_loc = vdecl.var_loc 

476 
} :: eqs 

477 
else eqs) 

478 
nd.node_locals [] 

479  
462  480 
let translate_eqs node args eqs = 
463  481 
List.fold_right (fun eq args > translate_eq node args eq) eqs args;; 
464  482  
...  ...  
466  484 
(*Log.report ~level:1 (fun fmt > Printers.pp_node fmt nd);*) 
467  485  
468  486 
let sorted_eqs = sort_equations_from_schedule nd sch in 
469  
487 
let constant_eqs = constant_equations nd in 

488 


470  489 
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l > ISet.add l) nd.node_locals ISet.empty, [] in 
471  490 
(* memories, init instructions, node calls, local variables (including memories), step instrs *) 
472 
let m, init, j, locals, s = translate_eqs nd init_args sorted_eqs in 

491 
let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in 

492 
assert (ISet.is_empty m0); 

493 
assert (init0 = []); 

494 
assert (Utils.IMap.is_empty j0); 

495 
let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, s0) sorted_eqs in 

473  496 
let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in 
474  497 
{ 
475  498 
mname = nd; 
...  ...  
477  500 
mcalls = mmap; 
478  501 
minstances = List.filter (fun (_, (n,_)) > not (Stateless.check_node n)) mmap; 
479  502 
minit = init; 
503 
mconst = s0; 

480  504 
mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs; 
481  505 
mstep = { 
482  506 
step_inputs = nd.node_inputs; 
...  ...  
500  524 
mannot = nd.node_annot; 
501  525 
} 
502  526  
503 
(** takes the global delcarations and the scheduling associated to each node *)


527 
(** takes the global declarations and the scheduling associated to each node *)


504  528 
let translate_prog decls node_schs = 
505  529 
let nodes = get_nodes decls in 
506  530 
List.map 
...  ...  
518  542 
 None > if m.mname.node_id = name then Some m else None) 
519  543 
None machines 
520  544  
545 
let get_const_assign m id = 

546 
try 

547 
match (List.find (fun instr > match instr with MLocalAssign (v, _) > v == id  _ > false) m.mconst) with 

548 
 MLocalAssign (_, e) > e 

549 
 _ > assert false 

550 
with Not_found > assert false 

551  
552  
553 
let value_of_ident m id = 

554 
(* is is a state var *) 

555 
try 

556 
StateVar (List.find (fun v > v.var_id = id) m.mmemory) 

557 
with Not_found > 

558 
try (* id is a node var *) 

559 
LocalVar (get_node_var id m.mname) 

560 
with Not_found > 

561 
try (* id is a constant *) 

562 
LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) 

563 
with Not_found > 

564 
(* id is a tag *) 

565 
Cst (Const_tag id) 

566  
567 
let rec value_of_dimension m dim = 

568 
match dim.Dimension.dim_desc with 

569 
 Dimension.Dbool b > Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false)) 

570 
 Dimension.Dint i > Cst (Const_int i) 

571 
 Dimension.Dident v > value_of_ident m v 

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

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

574 
 Dimension.Dlink dim' > value_of_dimension m dim' 

575 
 _ > assert false 

576  
577 
let rec dimension_of_value value = 

578 
match value with 

579 
 Cst (Const_tag t) when t = Corelang.tag_true > Dimension.mkdim_bool Location.dummy_loc true 

580 
 Cst (Const_tag t) when t = Corelang.tag_false > Dimension.mkdim_bool Location.dummy_loc false 

581 
 Cst (Const_int i) > Dimension.mkdim_int Location.dummy_loc i 

582 
 LocalVar v > Dimension.mkdim_ident Location.dummy_loc v.var_id 

583 
 Fun (f, args) > Dimension.mkdim_appl Location.dummy_loc f (List.map dimension_of_value args) 

584 
 _ > assert false 

521  585  
522  586 
(* Local Variables: *) 
523  587 
(* compilecommand:"make C .." *) 
Also available in: Unified diff