Revision 5538b7ac
Added by Xavier Thirioux about 11 years ago
| src/c_backend.ml | ||
|---|---|---|
| 504 | 504 |
self |
| 505 | 505 |
|
| 506 | 506 |
let print_stateless_prototype fmt (name, inputs, outputs) = |
| 507 |
match outputs with |
|
| 508 |
(* DOESN'T WORK FOR ARRAYS |
|
| 509 |
| [o] -> fprintf fmt "%a (@[<v>%a@])" |
|
| 510 |
(pp_c_type name) o.var_type |
|
| 511 |
(Utils.fprintf_list ~sep:",@ " pp_c_var) inputs |
|
| 512 |
*) |
|
| 513 |
| _ -> fprintf fmt "void %s (@[<v>@[%a%t@]@,@[%a@]@,@])" |
|
| 507 |
fprintf fmt "void %s (@[<v>@[%a%t@]@,@[%a@]@,@])" |
|
| 514 | 508 |
name |
| 515 | 509 |
(Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs |
| 516 | 510 |
(Utils.pp_final_char_if_non_empty ",@ " inputs) |
| ... | ... | |
| 530 | 524 |
(* Header Printing functions *) |
| 531 | 525 |
(********************************************************************************************) |
| 532 | 526 |
|
| 533 |
(* Removed because of "open" constructs. No more extern functions *) |
|
| 534 |
(* |
|
| 535 |
let print_prototype fmt decl = |
|
| 536 |
match decl.top_decl_desc with |
|
| 537 |
| ImportedFun m -> ( |
|
| 538 |
fprintf fmt "extern %a;@," |
|
| 539 |
print_stateless_prototype |
|
| 540 |
(m.fun_id, m.fun_inputs, m.fun_outputs) |
|
| 541 |
) |
|
| 542 |
| ImportedNode m -> ( |
|
| 543 |
if m.nodei_stateless then (* It's a function not a node *) |
|
| 544 |
fprintf fmt "extern %a;@," |
|
| 545 |
print_stateless_prototype |
|
| 546 |
(m.nodei_id, m.nodei_inputs, m.nodei_outputs) |
|
| 547 |
else ( |
|
| 548 |
let static = List.filter (fun v -> v.var_dec_const) m.nodei_inputs in |
|
| 549 |
fprintf fmt "extern %a;@," |
|
| 550 |
print_alloc_prototype (m.nodei_id, static); |
|
| 551 |
fprintf fmt "extern %a;@," |
|
| 552 |
(print_reset_prototype "self") (m.nodei_id, static); |
|
| 553 |
fprintf fmt "extern %a;@," |
|
| 554 |
(print_step_prototype "self") (m.nodei_id, m.nodei_inputs, m.nodei_outputs); |
|
| 555 |
) |
|
| 556 |
) |
|
| 557 |
| _ -> () (* We don't do anything here *) |
|
| 558 |
*) |
|
| 559 | 527 |
|
| 560 | 528 |
let print_import_standard fmt = |
| 561 | 529 |
fprintf fmt "#include \"%s/include/lustrec/arrow.h\"@.@." Version.prefix |
| 562 | 530 |
|
| 563 |
let print_prototype fmt decl = |
|
| 531 |
let print_import_prototype fmt decl =
|
|
| 564 | 532 |
match decl.top_decl_desc with |
| 565 | 533 |
| Open m -> fprintf fmt "#include \"%s.h\"@," m |
| 566 | 534 |
| _ -> () (* We don't do anything here *) |
| ... | ... | |
| 575 | 543 |
() |
| 576 | 544 |
|
| 577 | 545 |
let print_machine_struct fmt m = |
| 578 |
if m.mname.node_id != arrow_id |
|
| 579 |
then ( |
|
| 580 |
(* We don't print arrow function *) |
|
| 581 |
(* Define struct *) |
|
| 582 |
fprintf fmt "@[%a {@[%a%a%t@]};@]@."
|
|
| 583 |
pp_machine_memtype_name m.mname.node_id |
|
| 584 |
pp_registers_struct m |
|
| 585 |
(Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances |
|
| 586 |
(Utils.pp_final_char_if_non_empty "; " m.minstances) |
|
| 587 |
) |
|
| 546 |
if fst (get_stateless_status m) then |
|
| 547 |
begin |
|
| 548 |
end |
|
| 549 |
else |
|
| 550 |
begin |
|
| 551 |
(* Define struct *) |
|
| 552 |
fprintf fmt "@[%a {@[%a%a%t@]};@]@."
|
|
| 553 |
pp_machine_memtype_name m.mname.node_id |
|
| 554 |
pp_registers_struct m |
|
| 555 |
(Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances |
|
| 556 |
(Utils.pp_final_char_if_non_empty "; " m.minstances) |
|
| 557 |
end |
|
| 588 | 558 |
|
| 589 |
(* |
|
| 590 |
let pp_static_array_instance fmt m (v, m) = |
|
| 591 |
fprintf fmt "%s" (mk_addr_var m v) |
|
| 592 |
*) |
|
| 593 | 559 |
let print_static_declare_instance attr fmt (i, (m, static)) = |
| 594 | 560 |
fprintf fmt "%a(%s, %a%t%s)" |
| 595 | 561 |
pp_machine_static_declare_name (node_name m) |
| ... | ... | |
| 655 | 621 |
pp_machine_static_link_name m.mname.node_id |
| 656 | 622 |
|
| 657 | 623 |
let print_machine_decl fmt m = |
| 658 |
if m.mname.node_id <> arrow_id |
|
| 659 |
then ( |
|
| 660 |
(* We don't print arrow function *) |
|
| 661 |
(* Static allocation *) |
|
| 662 |
if !Options.static_mem |
|
| 663 |
then ( |
|
| 664 |
fprintf fmt "%a@.%a@.%a@." |
|
| 665 |
print_static_declare_macro m |
|
| 666 |
print_static_link_macro m |
|
| 667 |
print_static_alloc_macro m |
|
| 668 |
) |
|
| 669 |
else ( |
|
| 670 |
(* Dynamic allocation *) |
|
| 624 |
if fst (get_stateless_status m) then |
|
| 625 |
begin |
|
| 626 |
(* Print specification if any *) |
|
| 627 |
(match m.mspec with |
|
| 628 |
| None -> () |
|
| 629 |
| Some spec -> |
|
| 630 |
pp_acsl_spec m.mstep.step_outputs fmt spec |
|
| 631 |
); |
|
| 671 | 632 |
fprintf fmt "extern %a;@.@." |
| 672 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
|
| 673 |
); |
|
| 674 |
let self = mk_self m in |
|
| 675 |
fprintf fmt "extern %a;@.@." |
|
| 676 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic); |
|
| 677 |
(* Print specification if any *) |
|
| 678 |
(match m.mspec with |
|
| 633 |
print_stateless_prototype |
|
| 634 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
|
| 635 |
end |
|
| 636 |
else |
|
| 637 |
begin |
|
| 638 |
(* Static allocation *) |
|
| 639 |
if !Options.static_mem |
|
| 640 |
then ( |
|
| 641 |
fprintf fmt "%a@.%a@.%a@." |
|
| 642 |
print_static_declare_macro m |
|
| 643 |
print_static_link_macro m |
|
| 644 |
print_static_alloc_macro m |
|
| 645 |
) |
|
| 646 |
else ( |
|
| 647 |
(* Dynamic allocation *) |
|
| 648 |
fprintf fmt "extern %a;@.@." |
|
| 649 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
|
| 650 |
); |
|
| 651 |
let self = mk_self m in |
|
| 652 |
fprintf fmt "extern %a;@.@." |
|
| 653 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic); |
|
| 654 |
(* Print specification if any *) |
|
| 655 |
(match m.mspec with |
|
| 679 | 656 |
| None -> () |
| 680 | 657 |
| Some spec -> |
| 681 | 658 |
pp_acsl_spec m.mstep.step_outputs fmt spec |
| 682 |
); |
|
| 683 |
fprintf fmt "extern %a;@.@." |
|
| 684 |
(print_step_prototype self)
|
|
| 685 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
|
|
| 686 |
)
|
|
| 659 |
);
|
|
| 660 |
fprintf fmt "extern %a;@.@."
|
|
| 661 |
(print_step_prototype self)
|
|
| 662 |
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
|
|
| 663 |
end
|
|
| 687 | 664 |
|
| 688 | 665 |
|
| 689 | 666 |
(********************************************************************************************) |
| ... | ... | |
| 722 | 699 |
(Utils.fprintf_list ~sep:"" print_alloc_array) array_mem |
| 723 | 700 |
(Utils.fprintf_list ~sep:"" print_alloc_instance) m.minstances |
| 724 | 701 |
|
| 702 |
let print_stateless_code fmt m = |
|
| 703 |
let self = "__ERROR__" in |
|
| 704 |
if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc })
|
|
| 705 |
then |
|
| 706 |
(* C99 code *) |
|
| 707 |
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
|
|
| 708 |
print_stateless_prototype (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs) |
|
| 709 |
(* locals *) |
|
| 710 |
(Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals |
|
| 711 |
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals) |
|
| 712 |
(* check assertions *) |
|
| 713 |
(pp_c_checks self) m |
|
| 714 |
(* instrs *) |
|
| 715 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.mstep.step_instrs |
|
| 716 |
(Utils.pp_newline_if_non_empty m.mstep.step_instrs) |
|
| 717 |
(fun fmt -> fprintf fmt "return;") |
|
| 718 |
else |
|
| 719 |
(* C90 code *) |
|
| 720 |
let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in |
|
| 721 |
let gen_calls = List.map (fun e -> let (id, _, _) = call_of_expr e in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in |
|
| 722 |
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
|
|
| 723 |
print_stateless_prototype (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs) |
|
| 724 |
(* locals *) |
|
| 725 |
(Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals |
|
| 726 |
(Utils.pp_final_char_if_non_empty ";" base_locals) |
|
| 727 |
(* check assertions *) |
|
| 728 |
(pp_c_checks self) m |
|
| 729 |
(* instrs *) |
|
| 730 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.mstep.step_instrs |
|
| 731 |
(Utils.pp_newline_if_non_empty m.mstep.step_instrs) |
|
| 732 |
(fun fmt -> fprintf fmt "return;") |
|
| 733 |
|
|
| 725 | 734 |
let print_step_code fmt m self = |
| 726 | 735 |
if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc })
|
| 727 | 736 |
then |
| ... | ... | |
| 758 | 767 |
(fun fmt -> fprintf fmt "return;") |
| 759 | 768 |
|
| 760 | 769 |
let print_machine fmt m = |
| 761 |
if m.mname.node_id <> arrow_id |
|
| 762 |
then ( |
|
| 763 |
(* We don't print arrow function *) |
|
| 764 |
(* Alloc function, only if non static mode *) |
|
| 765 |
if (not !Options.static_mem) then |
|
| 766 |
( |
|
| 767 |
fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
|
|
| 768 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
|
| 769 |
print_alloc_code m; |
|
| 770 |
); |
|
| 771 |
let self = mk_self m in |
|
| 772 |
(* Reset function *) |
|
| 773 |
fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@."
|
|
| 774 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic) |
|
| 775 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.minit |
|
| 776 |
(Utils.pp_newline_if_non_empty m.minit); |
|
| 777 |
(* Step function *) |
|
| 778 |
print_step_code fmt m self |
|
| 779 |
) |
|
| 770 |
if fst (get_stateless_status m) then |
|
| 771 |
begin |
|
| 772 |
(* Step function *) |
|
| 773 |
print_stateless_code fmt m |
|
| 774 |
end |
|
| 775 |
else |
|
| 776 |
begin |
|
| 777 |
(* Alloc function, only if non static mode *) |
|
| 778 |
if (not !Options.static_mem) then |
|
| 779 |
( |
|
| 780 |
fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
|
|
| 781 |
print_alloc_prototype (m.mname.node_id, m.mstatic) |
|
| 782 |
print_alloc_code m; |
|
| 783 |
); |
|
| 784 |
let self = mk_self m in |
|
| 785 |
(* Reset function *) |
|
| 786 |
fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@."
|
|
| 787 |
(print_reset_prototype self) (m.mname.node_id, m.mstatic) |
|
| 788 |
(Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) m.minit |
|
| 789 |
(Utils.pp_newline_if_non_empty m.minit); |
|
| 790 |
(* Step function *) |
|
| 791 |
print_step_code fmt m self |
|
| 792 |
end |
|
| 780 | 793 |
|
| 781 | 794 |
(********************************************************************************************) |
| 782 | 795 |
(* Main related functions *) |
| ... | ... | |
| 972 | 985 |
(* Print the prototype of imported nodes *) |
| 973 | 986 |
fprintf source_fmt "/* Imported nodes declarations */@."; |
| 974 | 987 |
fprintf source_fmt "@[<v>"; |
| 975 |
List.iter (print_prototype source_fmt) prog; |
|
| 988 |
List.iter (print_import_prototype source_fmt) prog;
|
|
| 976 | 989 |
fprintf source_fmt "@]@."; |
| 977 | 990 |
(* Print consts *) |
| 978 | 991 |
fprintf source_fmt "/* Global constants (definitions) */@."; |
Also available in: Unified diff
Added declaration/definition of stateless/stateful nodes.
The 'function' keyword is for stateless nodes only,
the 'node' keyword is any kind of node.
Improves compilation and paves the way for more optimizations.