Project

General

Profile

Revision 5538b7ac src/c_backend.ml

View differences:

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