Revision 0d065e73 src/machine_code.ml
src/machine_code.ml  

81  81 
} 
82  82  
83  83 
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory 
84  
84  85 
let pp_step fmt s = 
85  86 
Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ " 
86  87 
(Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs 
...  ...  
318  319 
(* special treatment depending on the active backend. For horn backend, ite 
319  320 
are preserved in expression. While they are removed for C or Java 
320  321 
backends. *) 
321 
match !Options.output with  "horn" > 

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

322 
match !Options.output with 

323 
 "horn" > 

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

323  325 
 "C"  "java"  _ > 
324 
(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError) 

326 
(Format.eprintf "Normalization error for backend %s: %a@." 

327 
!Options.output 

328 
Printers.pp_expr expr; 

329 
raise NormalizationError) 

325  330 
) 
326  331 
 _ > raise NormalizationError 
327  332 
in 
...  ...  
488  493  
489  494 
let sorted_eqs = sort_equations_from_schedule nd sch in 
490  495 
let constant_eqs = constant_equations nd in 
491 


492 
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l > ISet.add l) nd.node_locals ISet.empty, [] in 

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

498 
to be declared for each assert *) 

499 
let new_locals, assert_instrs, nd_node_asserts = 

500 
let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in 

501 
if Corelang.functional_backend () then 

502 
[], [], exprl 

503 
else (* Each assert(e) is associated to a fresh variable v and declared as 

504 
v=e; assert (v); *) 

505 
let _, vars, eql, assertl = 

506 
List.fold_left (fun (i, vars, eqlist, assertlist) expr > 

507 
let loc = expr.expr_loc in 

508 
let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in 

509 
let assert_var = 

510 
mkvar_decl 

511 
loc 

512 
~orig:false (* fresh var *) 

513 
(var_id, 

514 
mktyp loc Tydec_bool, 

515 
mkclock loc Ckdec_any, 

516 
false, (* not a constant *) 

517 
None (* no default value *) 

518 
) 

519 
in 

520 
assert_var.var_type < Types.new_ty (Types.Tbool); 

521 
let eq = mkeq loc ([var_id], expr) in 

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

523 
) (1, [], [], []) exprl 

524 
in 

525 
vars, eql, assertl 

526 
in 

527 
let locals_list = nd.node_locals @ new_locals in 

528  
529 
let nd = { nd with node_locals = locals_list } in 

530 
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l > ISet.add l) locals_list ISet.empty, [] in 

493  531 
(* memories, init instructions, node calls, local variables (including memories), step instrs *) 
494  532 
let m0, init0, j0, locals0, s0 = translate_eqs nd init_args constant_eqs in 
495  533 
assert (ISet.is_empty m0); 
496  534 
assert (init0 = []); 
497  535 
assert (Utils.IMap.is_empty j0); 
498 
let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) sorted_eqs in


536 
let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) (sorted_eqs@assert_instrs) in


499  537 
let mmap = Utils.IMap.fold (fun i n res > (i, n)::res) j [] in 
500  538 
{ 
501  539 
mname = nd; 
...  ...  
518  556 
(*  "horn" > s TODO 16/12 *) 
519  557 
 "C"  "java"  _ > join_guards_list s 
520  558 
); 
521 
step_asserts = 

522 
let exprl = List.map (fun assert_ > assert_.assert_expr ) nd.node_asserts in 

523 
List.map (translate_expr nd init_args) exprl 

524 
; 

559 
step_asserts = List.map (translate_expr nd init_args) nd_node_asserts; 

525  560 
}; 
526  561 
mspec = nd.node_spec; 
527  562 
mannot = nd.node_annot; 
...  ...  
578  613 
 Dimension.Dident v > value_of_ident m v 
579  614 
 Dimension.Dappl (f, args) > let typ = if Basic_library.is_numeric_operator f then Type_predef.type_int else Type_predef.type_bool 
580  615 
in mk_val (Fun (f, List.map (value_of_dimension m) args)) typ 
581 
 Dimension.Dite (i, t, e) > let [vi; vt; ve] = List.map (value_of_dimension m) [i; t; e] in 

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

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

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

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

619 
 _ > assert false (* could not happen *) 

620 
) 

583  621 
 Dimension.Dlink dim' > value_of_dimension m dim' 
584  622 
 _ > assert false 
585  623 
Also available in: Unified diff