Project

General

Profile

« Previous | Next » 

Revision efcc8d7f

Added by LĂ©lio Brun about 2 years ago

move arrow spec in its own header

View differences:

dune
20 20
   include/lustrec_math.h
21 21
   include/arrow.c
22 22
   include/arrow.h
23
   include/arrow_spec.h
23 24
   include/arrow.cpp
24 25
   include/arrow.hpp
25 26
   include/io_frontend.c
src/backends/C/c_backend.ml
42 42
      f m
43 43

  
44 44
let gen_files
45
    (print_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *))
45
    (print_alloc_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *))
46 46
    basename prog machines dependencies =
47 47
  let destname = !Options.dest_dir ^ "/" ^ basename in
48 48
  
49 49
  let machines, spec = preprocess machines in
50
  
51
  (* Generating H file *)
50

  
51
  (* Generating H alloc file *)
52 52
  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
53 53
  with_out_file alloc_header_file (fun header_fmt ->
54
      print_header header_fmt basename prog machines dependencies spec);
54
      print_alloc_header header_fmt basename prog machines dependencies spec);
55 55

  
56 56
  (* Generating Lib C file *)
57 57
  let source_lib_file = c_or_cpp destname in
......
104 104
    
105 105
  (*   close_out makefile_out *)
106 106
  
107
let print_c_header basename =
108
  let header_m = match !Options.spec with
109
    | "no" ->
110
      C_backend_header.(module EmptyMod : MODIFIERS_HDR)
111

  
112
    | "acsl" ->
113
      C_backend_header.(module C_backend_spec.HdrMod : MODIFIERS_HDR)
114

  
115
    | "c" -> assert false        (* not implemented yet *)
107 116

  
108
let translate_to_c basename prog machines dependencies =
117
    | _ -> assert false
118
  in
119
  let module Header = C_backend_header.Main (val header_m) in
120
  let destname = !Options.dest_dir ^ "/" ^ basename in
121
  (* Generating H file *)
122
  let lusic = Lusic.read_lusic destname ".lusic" in
123
  let header_file = destname ^ ".h" in
124
  with_out_file header_file (fun header_fmt ->
125
      assert (not lusic.obsolete);
126
      Header.print_header_from_header header_fmt basename lusic.contents)
127

  
128
let translate_to_c generate_c_header basename prog machines dependencies =
109 129
  let header_m, source_m, source_main_m, makefile_m, preprocess =
110 130
    match !Options.spec with
111 131
    | "no" ->
......
116 136
      fun m -> m, []
117 137

  
118 138
    | "acsl" ->
119
      C_backend_header.(module EmptyMod : MODIFIERS_HDR),
120
      (module C_backend_spec.SrcMod : C_backend_src.MODIFIERS_SRC),
139
      let open C_backend_spec in
140
      C_backend_header.(module HdrMod : MODIFIERS_HDR),
141
      C_backend_src.(module SrcMod : MODIFIERS_SRC),
121 142
      C_backend_main.(module EmptyMod : MODIFIERS_MAINSRC),
122
      (module C_backend_spec.MakefileMod : C_backend_makefile.MODIFIERS_MKF),
123
      C_backend_spec.preprocess_acsl
143
      C_backend_makefile.(module MakefileMod : MODIFIERS_MKF),
144
      preprocess_acsl
124 145

  
125 146
    | "c" -> assert false        (* not implemented yet *)
126 147

  
......
139 160
    preprocess
140 161
    (* CMakefile.print_makefile *)
141 162
  in
163
  if generate_c_header then print_c_header basename;
142 164
  gen_files funs basename prog machines dependencies
143 165

  
144 166

  
src/backends/C/c_backend_header.ml
23 23

  
24 24
module type MODIFIERS_HDR = sig
25 25
  val print_machine_decl_prefix: Format.formatter -> machine_t -> unit
26
  val pp_import_standard_spec: formatter -> unit -> unit
26 27
end
27 28

  
28 29
module EmptyMod = struct
29 30
  let print_machine_decl_prefix = fun _ _ -> ()
31
  let pp_import_standard_spec _ _ = ()
30 32
end
31 33

  
32 34
module Main = functor (Mod: MODIFIERS_HDR) -> struct
......
36 38
    fprintf fmt
37 39
      "#include <stdint.h>@,\
38 40
       %a\
39
       #include \"%s/arrow.h%s\""
41
       #include \"%s/arrow.h%s\"\
42
       %a"
40 43
      (if !Options.mpfr then
41 44
         pp_print_endcut "#include <mpfr.h>"
42 45
       else pp_print_nothing) ()
43 46
      (Arrow.arrow_top_decl ()).top_decl_owner
44 47
      (if !Options.cpp then "pp" else "")
48
      Mod.pp_import_standard_spec ()
45 49

  
46 50
  let rec print_static_val pp_var fmt v =
47 51
    match v.value_desc with
......
324 328
       %a\
325 329
       %a\
326 330
       %a\
327
       %a\
328 331
       #endif\
329 332
       @]"
330 333

  
......
358 361
         print_machine_struct
359 362
         ~pp_epilogue:pp_print_cutcut) machines
360 363

  
361
      (* Print specification *)
362
      C_backend_spec.pp_acsl_preamble spec
363

  
364 364
      (* Print the prototypes of all machines *)
365 365
      (pp_print_list
366 366
         ~pp_open_box:pp_open_vbox0
src/backends/C/c_backend_lusic.ml
1
open Lusic
2
open Utils.Format
3

  
4
let print_lusic_to_h basename extension =
5
  let module HeaderMod = C_backend_header.EmptyMod in
6
  let module Header = C_backend_header.Main (HeaderMod) in
7
  let lusic = read_lusic basename extension in
8
  let header_name = basename ^ ".h" in
9
  with_out_file header_name @@ fun h_fmt ->
10
  assert (not lusic.obsolete);
11
  (*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*)
12
  (* Typing.uneval_prog_generics lusic.contents;
13
     * Clock_calculus.uneval_prog_generics lusic.contents; *)
14
  Header.print_header_from_header
15
    h_fmt
16
    (Filename.basename basename)
17
    lusic.contents
src/backends/C/c_backend_spec.ml
135 135
let preprocess_acsl machines = machines, []
136 136
                          
137 137
(* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *)
138
let pp_acsl_preamble fmt _preamble =
139
  fprintf fmt "";
140
  ()
138
(* let pp_acsl_preamble fmt _preamble =
139
 *   fprintf fmt "";
140
 *   () *)
141 141

  
142 142
let pp_acsl_basic_type_desc t_desc =
143 143
  if Types.is_bool_type t_desc then
......
679 679
  let rec aux fmt instr = match instr.instr_desc with
680 680
    | MLocalAssign (x, v)
681 681
    | MStateAssign (x, v) ->
682
      pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m)fmt
682
      pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m) fmt
683 683
        (x.var_type, mk_val (Var x) x.var_type, v)
684 684
    | MStep ([i0], i, vl)
685 685
      when Basic_library.is_value_internal_fun
......
689 689
      pp_true fmt ()
690 690
    | MStep ([_], i, _) when has_c_prototype i dependencies ->
691 691
      pp_true fmt ()
692
    | MStep (xs, f, ys) ->
692
    | MStep (xs, i, ys) ->
693 693
      begin try
694
          let n, _ = List.assoc f m.minstances in
694
          let n, _ = List.assoc i m.minstances in
695 695
            pp_mem_trans_aux
696 696
              pp_access' pp_access'
697 697
              (pp_c_val m mem_in (pp_c_var_read m))
698 698
              pp_var_decl
699 699
              fmt
700
              (node_name n, ys, [], xs, (mem_in, f), (mem_out, f))
700
              (node_name n, ys, [], xs, (mem_in, i), (mem_out, i))
701 701
        with Not_found -> pp_true fmt ()
702 702
      end
703
    | MReset f ->
703
    | MReset i ->
704 704
      begin try
705
          let n, _ = List.assoc f m.minstances in
705
          let n, _ = List.assoc i m.minstances in
706 706
          pp_mem_init' fmt (node_name n, mem_out)
707 707
        with Not_found -> pp_true fmt ()
708 708
      end
......
711 711
      then (* boolean case *)
712 712
        pp_ite (pp_c_val m mem_in (pp_c_var_read m))
713 713
          (fun fmt () ->
714
             try
715
               let l = List.assoc tag_true brs in
716
               pp_paren (pp_and_l aux) fmt l
717
             with Not_found -> pp_true fmt ())
714
             match List.assoc tag_true brs with
715
             | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
716
             | []
717
             | exception Not_found -> pp_true fmt ())
718 718
          (fun fmt () ->
719
             try
720
               let l = List.assoc tag_false brs in
721
               pp_paren (pp_and_l aux) fmt l
722
             with Not_found -> pp_true fmt ())
719
             match List.assoc tag_false brs with
720
             | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
721
             | []
722
             | exception Not_found ->
723
             (* try
724
              *   let l = List.assoc tag_false brs in
725
              *   pp_paren (pp_and_l aux) fmt l
726
              * with Not_found -> *) pp_true fmt ())
723 727
          
724 728
          (* (pp_paren (pp_and_l aux)) (pp_paren (pp_and_l aux)) *)
725 729
          fmt (v, (), ())
......
795 799
let pp_at_pre pp_p fmt p =
796 800
  pp_at pp_p fmt (p, label_pre)
797 801

  
798
let pp_arrow_spec fmt () =
799
  let name = "_arrow" in
800
  let mem_in = "mem_in" in
801
  let mem_out = "mem_out" in
802
  let reg_first = "_reg", "_first" in
803
  let mem_in_first = mem_in, reg_first in
804
  let mem_out_first = mem_out, reg_first in
805
  let mem = "mem" in
806
  let self = "self" in
807
  fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a%a"
808

  
809
    (pp_spec_line (pp_ghost pp_print_string))
810
    "struct _arrow_mem_ghost {struct _arrow_reg _reg;};"
811

  
812
    (pp_spec_cut
813
       (pp_predicate
814
          (pp_mem_valid pp_machine_decl)
815
          (pp_valid pp_print_string)))
816
    ((name, (name, "mem", "*" ^ self)), [self])
817

  
818
    (pp_spec_cut
819
       (pp_predicate
820
          (pp_mem_init pp_machine_decl)
821
          (pp_equal
822
             (pp_access pp_print_string pp_access')
823
             pp_print_int)))
824
    ((name, (name, "mem_ghost", mem_in)),
825
     (mem_in_first, 1))
826

  
827
    (pp_spec_cut
828
       (pp_predicate
829
          (pp_mem_trans_aux
830
             pp_machine_decl pp_machine_decl pp_print_string pp_print_string)
831
          (pp_ite
832
             (pp_access pp_print_string pp_access')
833
             (pp_paren
834
                (pp_and
835
                   (pp_equal
836
                      (pp_access pp_print_string pp_access')
837
                      pp_print_int)
838
                   (pp_equal pp_print_string pp_print_string)))
839
                (pp_paren
840
                   (pp_and
841
                      (pp_equal
842
                         (pp_access pp_print_string pp_access')
843
                         (pp_access pp_print_string pp_access'))
844
                      (pp_equal pp_print_string pp_print_string))))))
845
    ((name, ["integer x"; "integer y"], [], ["_Bool out"],
846
      (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
847
     (* (("out", mem_in_first), *)
848
     (mem_in_first, ((mem_out_first, 0), ("out", "x")),
849
      ((mem_out_first, mem_in_first), ("out", "y"))))
850

  
851
    (pp_spec_cut
852
       (pp_predicate
853
          (pp_mem_ghost pp_machine_decl pp_machine_decl)
854
          (pp_equal
855
             (pp_access pp_print_string pp_access')
856
             (pp_indirect pp_print_string pp_access'))))
857
    ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
858
    ((mem, reg_first), (self, reg_first)))
802
let pp_register =
803
  pp_print_list
804
    ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
805
    ~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first")
806
    ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
807
    (fun fmt (i, _) -> pp_print_string fmt i)
808

  
809
module HdrMod = struct
810

  
811
  let print_machine_decl_prefix = fun _ _ -> ()
812

  
813
  let pp_import_standard_spec fmt () =
814
    fprintf fmt "@,#include \"%s/arrow_spec.h%s\""
815
      (Arrow.arrow_top_decl ()).top_decl_owner
816
      (if !Options.cpp then "pp" else "")
817

  
818
end
859 819

  
860 820
module SrcMod = struct
861 821

  
862 822
  let pp_predicates dependencies fmt machines =
863 823
    fprintf fmt
864
      "%a@,%a%a%a%a"
865
      pp_arrow_spec ()
824
      "%a%a%a%a"
866 825
      (pp_print_list
867 826
         ~pp_open_box:pp_open_vbox0
868 827
         ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
......
887 846
         (print_machine_trans_annotations machines dependencies)
888 847
         ~pp_epilogue:pp_print_cutcut) machines
889 848

  
890
  let pp_register =
891
    pp_print_list
892
      ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
893
      ~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first")
894
      ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
895
      (fun fmt (i, _) -> pp_print_string fmt i)
896

  
897 849
  let pp_reset_spec fmt machines self m =
898 850
    let name = m.mname.node_id in
899 851
    let mem = mk_mem m in
src/compiler_stages.ml
11 11
  | _ -> false
12 12

  
13 13

  
14
let generate_c_header = ref false
15

  
14 16
(* check whether a source file has a compiled header, if not, generate the
15 17
   compiled header *)
16 18
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
......
36 38
          (if from_lusi then prog else Lusic.extract_header dirname basename prog)
37 39
          destname
38 40
          lusic_ext;
39
        if !Options.output = "C"
40
        then C_backend_lusic.print_lusic_to_h destname lusic_ext
41
        generate_c_header := !Options.output = "C";
41 42
      end
42 43
    else (* Lusic exists and is usable. Checking compatibility *)
43 44
      begin
......
280 281
    "C", ".lus" -> 
281 282
     begin
282 283
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
283
       C_backend.translate_to_c
284
       C_backend.translate_to_c !generate_c_header
284 285
	 (* alloc_header_file source_lib_file source_main_file makefile_file *)
285 286
	 basename prog machine_code dependencies
286 287
     end
......
295 296
*)
296 297
  |  "C", _ -> 
297 298
      begin
299
        C_backend.print_c_header basename;
298 300
      	Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");
299 301
      end
300 302
  | "java", _ ->
src/dune
79 79
 (modules
80 80
   lusic
81 81
   c_backend_header c_backend_spec c_backend_makefile
82
   c_backend_lusic c_backend_mauve c_backend_src
82
   c_backend_mauve c_backend_src
83 83
   ada_backend ada_printer ada_backend_common ada_backend_ads ada_backend_adb
84 84
   ada_backend_wrapper
85 85
   horn_backend horn_backend_common horn_backend_printers
src/lusic.ml
23 23
  contents  : top_decl list;
24 24
}
25 25

  
26
module HeaderMod = C_backend_header.EmptyMod
27
module Header = C_backend_header.Main (HeaderMod)
28

  
29 26
(* extracts a header from a program representing module owner = dirname/basename *)
30 27
let extract_header dirname basename prog =
31 28
  let owner = dirname ^ "/" ^ basename in

Also available in: Unified diff