Revision 0d065e73
Added by Pierre-Loïc Garoche about 5 years ago
| 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
Solved a bug in the compilation of asserts. Now different behavior depending on the backend:
functional: keep it as is
non func: introduce a fresh local var v and replace assert(e) by v=e; assert (v);