Revision c226a3ba
Added by Lélio Brun over 3 years ago
| src/backends/C/c_backend_src.ml | ||
|---|---|---|
| 17 | 17 |
open C_backend_common |
| 18 | 18 |
|
| 19 | 19 |
module type MODIFIERS_SRC = sig |
| 20 |
val pp_predicates: dep_t list -> formatter -> machine_t list -> unit |
|
| 21 |
val pp_reset_spec: formatter -> ident -> machine_t -> unit |
|
| 22 |
val pp_step_spec: formatter -> ident -> machine_t -> unit |
|
| 23 |
val pp_step_instr_spec: machine_t -> ident -> formatter -> (int * instr_t) -> unit |
|
| 20 | 24 |
end |
| 21 | 25 |
|
| 22 | 26 |
module EmptyMod = struct |
| 27 |
let pp_predicates _ _ _ = () |
|
| 28 |
let pp_reset_spec _ _ _ = () |
|
| 29 |
let pp_step_spec _ _ _ = () |
|
| 30 |
let pp_step_instr_spec _ _ _ _ = () |
|
| 23 | 31 |
end |
| 24 | 32 |
|
| 25 | 33 |
module Main = functor (Mod: MODIFIERS_SRC) -> struct |
| ... | ... | |
| 274 | 282 |
let pp_machine_clear = |
| 275 | 283 |
pp_machine_ pp_machine_clear_name "pp_machine_clear" |
| 276 | 284 |
|
| 277 |
let has_c_prototype funname dependencies = |
|
| 278 |
(* We select the last imported node with the name funname. |
|
| 279 |
The order of evaluation of dependencies should be |
|
| 280 |
compatible with overloading. (Not checked yet) *) |
|
| 281 |
let imported_node_opt = |
|
| 282 |
List.fold_left |
|
| 283 |
(fun res dep -> |
|
| 284 |
match res with |
|
| 285 |
| Some _ -> res |
|
| 286 |
| None -> |
|
| 287 |
let decls = dep.content in |
|
| 288 |
let matched = fun t -> match t.top_decl_desc with |
|
| 289 |
| ImportedNode nd -> nd.nodei_id = funname |
|
| 290 |
| _ -> false |
|
| 291 |
in |
|
| 292 |
if List.exists matched decls then |
|
| 293 |
match (List.find matched decls).top_decl_desc with |
|
| 294 |
| ImportedNode nd -> Some nd |
|
| 295 |
| _ -> assert false |
|
| 296 |
else |
|
| 297 |
None) None dependencies in |
|
| 298 |
match imported_node_opt with |
|
| 299 |
| None -> false |
|
| 300 |
| Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false) |
|
| 301 |
|
|
| 302 | 285 |
let pp_call m self pp_read pp_write fmt i |
| 303 | 286 |
(inputs: Machine_code_types.value_t list) (outputs: var_decl list) = |
| 304 | 287 |
try (* stateful node instance *) |
| ... | ... | |
| 406 | 389 |
(pp_print_list ~pp_open_box:pp_open_vbox0 |
| 407 | 390 |
(pp_machine_instr dependencies m self)) h |
| 408 | 391 |
|
| 392 |
let pp_machine_nospec_instr dependencies m self fmt _i instr = |
|
| 393 |
pp_machine_instr dependencies m self fmt instr |
|
| 394 |
|
|
| 395 |
let pp_machine_step_instr dependencies m self fmt i instr = |
|
| 396 |
fprintf fmt "%a%a%a" |
|
| 397 |
(if i = 0 then |
|
| 398 |
(fun fmt () -> Mod.pp_step_instr_spec m self fmt (i-1, instr)) |
|
| 399 |
else |
|
| 400 |
pp_print_nothing) () |
|
| 401 |
(pp_machine_instr dependencies m self) instr |
|
| 402 |
(Mod.pp_step_instr_spec m self) (i, instr) |
|
| 409 | 403 |
|
| 410 | 404 |
(********************************************************************************************) |
| 411 | 405 |
(* C file Printing functions *) |
| ... | ... | |
| 474 | 468 |
_alloc = (%a *) malloc(sizeof(%a));@,\ |
| 475 | 469 |
assert(_alloc);@,\ |
| 476 | 470 |
%a%areturn _alloc;" |
| 477 |
pp_machine_memtype_name m.mname.node_id
|
|
| 478 |
pp_machine_memtype_name m.mname.node_id
|
|
| 479 |
pp_machine_memtype_name m.mname.node_id
|
|
| 471 |
(pp_machine_memtype_name ~ghost:false) m.mname.node_id
|
|
| 472 |
(pp_machine_memtype_name ~ghost:false) m.mname.node_id
|
|
| 473 |
(pp_machine_memtype_name ~ghost:false) m.mname.node_id
|
|
| 480 | 474 |
(pp_print_list ~pp_sep:pp_print_nothing print_alloc_array) (array_mems m) |
| 481 | 475 |
(pp_print_list ~pp_sep:pp_print_nothing print_alloc_instance) m.minstances |
| 482 | 476 |
|
| ... | ... | |
| 524 | 518 |
|
| 525 | 519 |
let pp_print_function |
| 526 | 520 |
~pp_prototype ~prototype |
| 521 |
?(pp_spec=pp_print_nothing) |
|
| 527 | 522 |
?(pp_local=pp_print_nothing) ?(base_locals=[]) |
| 528 | 523 |
?(pp_array_mem=pp_print_nothing) ?(array_mems=[]) |
| 529 | 524 |
?(pp_init_mpfr_local=pp_print_nothing) |
| ... | ... | |
| 531 | 526 |
?(mpfr_locals=[]) |
| 532 | 527 |
?(pp_check=pp_print_nothing) ?(checks=[]) |
| 533 | 528 |
?(pp_extra=pp_print_nothing) |
| 534 |
?(pp_instr=pp_print_nothing) ?(instrs=[])
|
|
| 529 |
?(pp_instr=fun fmt _ _ -> pp_print_nothing fmt ()) ?(instrs=[])
|
|
| 535 | 530 |
fmt = |
| 536 | 531 |
fprintf fmt |
| 537 |
"@[<v 2>%a {@,\
|
|
| 532 |
"%a@[<v 2>%a {@,\
|
|
| 538 | 533 |
%a%a\ |
| 539 | 534 |
%a%a%a%a%areturn;@]@,\ |
| 540 | 535 |
}" |
| 536 |
pp_spec () |
|
| 541 | 537 |
pp_prototype prototype |
| 542 | 538 |
(* locals *) |
| 543 | 539 |
(pp_print_list |
| ... | ... | |
| 560 | 556 |
(* check assertions *) |
| 561 | 557 |
(pp_print_list pp_check) checks |
| 562 | 558 |
(* instrs *) |
| 563 |
(pp_print_list |
|
| 559 |
(pp_print_list_i
|
|
| 564 | 560 |
~pp_open_box:pp_open_vbox0 |
| 565 | 561 |
~pp_epilogue:pp_print_cut |
| 566 | 562 |
pp_instr) instrs |
| ... | ... | |
| 593 | 589 |
~mpfr_locals:m.mstep.step_locals |
| 594 | 590 |
~pp_check:(pp_c_check m self) |
| 595 | 591 |
~checks:m.mstep.step_checks |
| 596 |
~pp_instr:(pp_machine_instr dependencies m self) |
|
| 592 |
~pp_instr:(pp_machine_nospec_instr dependencies m self)
|
|
| 597 | 593 |
~instrs:m.mstep.step_instrs |
| 598 | 594 |
fmt |
| 599 | 595 |
else |
| ... | ... | |
| 615 | 611 |
~mpfr_locals:m.mstep.step_locals |
| 616 | 612 |
~pp_check:(pp_c_check m self) |
| 617 | 613 |
~checks:m.mstep.step_checks |
| 618 |
~pp_instr:(pp_machine_instr dependencies m self) |
|
| 614 |
~pp_instr:(pp_machine_nospec_instr dependencies m self)
|
|
| 619 | 615 |
~instrs:m.mstep.step_instrs |
| 620 | 616 |
fmt |
| 621 | 617 |
|
| 622 | 618 |
let print_reset_code dependencies self fmt m = |
| 623 | 619 |
pp_print_function |
| 620 |
~pp_spec:(fun fmt () -> Mod.pp_reset_spec fmt self m) |
|
| 624 | 621 |
~pp_prototype:(print_reset_prototype self) |
| 625 | 622 |
~prototype:(m.mname.node_id, m.mstatic) |
| 626 | 623 |
~pp_local:(pp_c_decl_local_var m) |
| 627 | 624 |
~base_locals:(const_locals m) |
| 628 |
~pp_instr:(pp_machine_instr dependencies m self) |
|
| 625 |
~pp_instr:(pp_machine_nospec_instr dependencies m self)
|
|
| 629 | 626 |
~instrs:m.minit |
| 630 | 627 |
fmt |
| 631 | 628 |
|
| ... | ... | |
| 670 | 667 |
then |
| 671 | 668 |
(* C99 code *) |
| 672 | 669 |
pp_print_function |
| 670 |
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m) |
|
| 673 | 671 |
~pp_prototype:(print_step_prototype self) |
| 674 | 672 |
~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
| 675 | 673 |
~pp_local:(pp_c_decl_local_var m) |
| ... | ... | |
| 681 | 679 |
~mpfr_locals:m.mstep.step_locals |
| 682 | 680 |
~pp_check:(pp_c_check m self) |
| 683 | 681 |
~checks:m.mstep.step_checks |
| 684 |
~pp_instr:(pp_machine_instr dependencies m self) |
|
| 682 |
~pp_instr:(pp_machine_step_instr dependencies m self)
|
|
| 685 | 683 |
~instrs:m.mstep.step_instrs |
| 686 | 684 |
fmt |
| 687 | 685 |
else |
| ... | ... | |
| 692 | 690 |
let id, _, _ = call_of_expr e in |
| 693 | 691 |
mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in |
| 694 | 692 |
pp_print_function |
| 693 |
~pp_spec:(fun fmt () -> Mod.pp_step_spec fmt self m) |
|
| 695 | 694 |
~pp_prototype:(print_step_prototype self) |
| 696 | 695 |
~prototype:(m.mname.node_id, |
| 697 | 696 |
m.mstep.step_inputs @ gen_locals @ gen_calls, |
| ... | ... | |
| 703 | 702 |
~mpfr_locals:m.mstep.step_locals |
| 704 | 703 |
~pp_check:(pp_c_check m self) |
| 705 | 704 |
~checks:m.mstep.step_checks |
| 706 |
~pp_instr:(pp_machine_instr dependencies m self) |
|
| 705 |
~pp_instr:(pp_machine_step_instr dependencies m self)
|
|
| 707 | 706 |
~instrs:m.mstep.step_instrs |
| 708 | 707 |
fmt |
| 709 | 708 |
|
| ... | ... | |
| 834 | 833 |
(* Clear function *) |
| 835 | 834 |
(print_clear_code self) m |
| 836 | 835 |
|
| 837 |
|
|
| 838 | 836 |
(* TODO: ACSL |
| 839 | 837 |
- a contract machine shall not be directly printed in the C source |
| 840 | 838 |
- but a regular machine associated to a contract machine shall integrate |
| ... | ... | |
| 849 | 847 |
print_stateless_code dependencies fmt m |
| 850 | 848 |
else |
| 851 | 849 |
let self = mk_self m in |
| 852 |
fprintf fmt "@[<v>%a%a@,%a%a@]" |
|
| 850 |
fprintf fmt "@[<v>%a%a@,@,%a%a@]"
|
|
| 853 | 851 |
print_alloc_function m |
| 854 | 852 |
(* Reset function *) |
| 855 | 853 |
(print_reset_code dependencies self) m |
| ... | ... | |
| 889 | 887 |
%a\ |
| 890 | 888 |
%a\ |
| 891 | 889 |
%a\ |
| 890 |
%a\ |
|
| 892 | 891 |
@]@." |
| 893 | 892 |
print_import_standard () |
| 894 | 893 |
print_import_prototype |
| ... | ... | |
| 967 | 966 |
print_machine_struct |
| 968 | 967 |
~pp_epilogue:pp_print_cutcut) machines |
| 969 | 968 |
|
| 969 |
(* Print the spec predicates *) |
|
| 970 |
(Mod.pp_predicates dependencies) machines |
|
| 971 |
|
|
| 970 | 972 |
(* Print nodes one by one (in the previous order) *) |
| 971 | 973 |
(pp_print_list |
| 972 | 974 |
~pp_open_box:pp_open_vbox0 |
Also available in: Unified diff
start generating ACSL spec