/ - Diff - LustreC

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

           f m
     let gen_files
         (print_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *))
         (print_alloc_header, print_lib_c, print_main_c, print_makefile, preprocess (* , print_cmake *))
         basename prog machines dependencies =
       let destname = !Options.dest_dir ^ "/" ^ basename in
       let machines, spec = preprocess machines in
       (* Generating H file *)
       (* Generating H alloc file *)
       let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
       with_out_file alloc_header_file (fun header_fmt ->
           print_header header_fmt basename prog machines dependencies spec);
           print_alloc_header header_fmt basename prog machines dependencies spec);
       (* Generating Lib C file *)
       let source_lib_file = c_or_cpp destname in
-...
       (*   close_out makefile_out *)
     let print_c_header basename =
       let header_m = match !Options.spec with
         | "no" ->
           C_backend_header.(module EmptyMod : MODIFIERS_HDR)
         | "acsl" ->
           C_backend_header.(module C_backend_spec.HdrMod : MODIFIERS_HDR)
         | "c" -> assert false        (* not implemented yet *)
     let translate_to_c basename prog machines dependencies =
         | _ -> assert false
       in
       let module Header = C_backend_header.Main (val header_m) in
       let destname = !Options.dest_dir ^ "/" ^ basename in
       (* Generating H file *)
       let lusic = Lusic.read_lusic destname ".lusic" in
       let header_file = destname ^ ".h" in
       with_out_file header_file (fun header_fmt ->
           assert (not lusic.obsolete);
           Header.print_header_from_header header_fmt basename lusic.contents)
     let translate_to_c generate_c_header basename prog machines dependencies =
       let header_m, source_m, source_main_m, makefile_m, preprocess =
         match !Options.spec with
         | "no" ->
-...
           fun m -> m, []
         | "acsl" ->
           C_backend_header.(module EmptyMod : MODIFIERS_HDR),
           (module C_backend_spec.SrcMod : C_backend_src.MODIFIERS_SRC),
           let open C_backend_spec in
           C_backend_header.(module HdrMod : MODIFIERS_HDR),
           C_backend_src.(module SrcMod : MODIFIERS_SRC),
           C_backend_main.(module EmptyMod : MODIFIERS_MAINSRC),
           (module C_backend_spec.MakefileMod : C_backend_makefile.MODIFIERS_MKF),
           C_backend_spec.preprocess_acsl
           C_backend_makefile.(module MakefileMod : MODIFIERS_MKF),
           preprocess_acsl
         | "c" -> assert false        (* not implemented yet *)
-...
         preprocess
         (* CMakefile.print_makefile *)
       in
       if generate_c_header then print_c_header basename;
       gen_files funs basename prog machines dependencies

     module type MODIFIERS_HDR = sig
       val print_machine_decl_prefix: Format.formatter -> machine_t -> unit
       val pp_import_standard_spec: formatter -> unit -> unit
     end
     module EmptyMod = struct
       let print_machine_decl_prefix = fun _ _ -> ()
       let pp_import_standard_spec _ _ = ()
     end
     module Main = functor (Mod: MODIFIERS_HDR) -> struct
-...
         fprintf fmt
           "#include <stdint.h>@,\
            %a\
            #include \"%s/arrow.h%s\""
            #include \"%s/arrow.h%s\"\
            %a"
           (if !Options.mpfr then
              pp_print_endcut "#include <mpfr.h>"
            else pp_print_nothing) ()
           (Arrow.arrow_top_decl ()).top_decl_owner
           (if !Options.cpp then "pp" else "")
           Mod.pp_import_standard_spec ()
       let rec print_static_val pp_var fmt v =
         match v.value_desc with
-...
            %a\
            %a\
            %a\
            %a\
            #endif\
            @]"
-...
              print_machine_struct
              ~pp_epilogue:pp_print_cutcut) machines
           (* Print specification *)
           C_backend_spec.pp_acsl_preamble spec
           (* Print the prototypes of all machines *)
           (pp_print_list
              ~pp_open_box:pp_open_vbox0

     open Lusic
     open Utils.Format
     let print_lusic_to_h basename extension =
       let module HeaderMod = C_backend_header.EmptyMod in
       let module Header = C_backend_header.Main (HeaderMod) in
       let lusic = read_lusic basename extension in
       let header_name = basename ^ ".h" in
       with_out_file header_name @@ fun h_fmt ->
       assert (not lusic.obsolete);
       (*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*)
       (* Typing.uneval_prog_generics lusic.contents;
          * Clock_calculus.uneval_prog_generics lusic.contents; *)
       Header.print_header_from_header
         h_fmt
         (Filename.basename basename)
         lusic.contents

     let preprocess_acsl machines = machines, []
     (* TODO: This preamble shall be a list of types, axiomatics, predicates, theorems *)
     let pp_acsl_preamble fmt _preamble =
       fprintf fmt "";
       ()
     (* let pp_acsl_preamble fmt _preamble =
      *   fprintf fmt "";
      *   () *)
     let pp_acsl_basic_type_desc t_desc =
       if Types.is_bool_type t_desc then
-...
       let rec aux fmt instr = match instr.instr_desc with
         | MLocalAssign (x, v)
         | MStateAssign (x, v) ->
           pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m)fmt
           pp_assign_spec m mem_out (pp_c_var_read m) mem_in (pp_c_var_read m) fmt
             (x.var_type, mk_val (Var x) x.var_type, v)
         | MStep ([i0], i, vl)
           when Basic_library.is_value_internal_fun
-...
           pp_true fmt ()
         | MStep ([_], i, _) when has_c_prototype i dependencies ->
           pp_true fmt ()
         | MStep (xs, f, ys) ->
         | MStep (xs, i, ys) ->
           begin try
               let n, _ = List.assoc f m.minstances in
               let n, _ = List.assoc i m.minstances in
                 pp_mem_trans_aux
                   pp_access' pp_access'
                   (pp_c_val m mem_in (pp_c_var_read m))
                   pp_var_decl
                   fmt
                   (node_name n, ys, [], xs, (mem_in, f), (mem_out, f))
                   (node_name n, ys, [], xs, (mem_in, i), (mem_out, i))
             with Not_found -> pp_true fmt ()
           end
         | MReset f ->
         | MReset i ->
           begin try
               let n, _ = List.assoc f m.minstances in
               let n, _ = List.assoc i m.minstances in
               pp_mem_init' fmt (node_name n, mem_out)
             with Not_found -> pp_true fmt ()
           end
-...
           then (* boolean case *)
             pp_ite (pp_c_val m mem_in (pp_c_var_read m))
               (fun fmt () ->
                  try
                    let l = List.assoc tag_true brs in
                    pp_paren (pp_and_l aux) fmt l
                  with Not_found -> pp_true fmt ())
                  match List.assoc tag_true brs with
                  | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
                  | []
                  | exception Not_found -> pp_true fmt ())
               (fun fmt () ->
                  try
                    let l = List.assoc tag_false brs in
                    pp_paren (pp_and_l aux) fmt l
                  with Not_found -> pp_true fmt ())
                  match List.assoc tag_false brs with
                  | _ :: _ as l -> pp_paren (pp_and_l aux) fmt l
                  | []
                  | exception Not_found ->
                  (* try
                   *   let l = List.assoc tag_false brs in
                   *   pp_paren (pp_and_l aux) fmt l
                   * with Not_found -> *) pp_true fmt ())
               (* (pp_paren (pp_and_l aux)) (pp_paren (pp_and_l aux)) *)
               fmt (v, (), ())
-...
     let pp_at_pre pp_p fmt p =
       pp_at pp_p fmt (p, label_pre)
     let pp_arrow_spec fmt () =
       let name = "_arrow" in
       let mem_in = "mem_in" in
       let mem_out = "mem_out" in
       let reg_first = "_reg", "_first" in
       let mem_in_first = mem_in, reg_first in
       let mem_out_first = mem_out, reg_first in
       let mem = "mem" in
       let self = "self" in
       fprintf fmt "/* ACSL arrow spec */@,%a%a%a%a%a"
         (pp_spec_line (pp_ghost pp_print_string))
         "struct _arrow_mem_ghost {struct _arrow_reg _reg;};"
         (pp_spec_cut
            (pp_predicate
               (pp_mem_valid pp_machine_decl)
               (pp_valid pp_print_string)))
         ((name, (name, "mem", "*" ^ self)), [self])
         (pp_spec_cut
            (pp_predicate
               (pp_mem_init pp_machine_decl)
               (pp_equal
                  (pp_access pp_print_string pp_access')
                  pp_print_int)))
         ((name, (name, "mem_ghost", mem_in)),
          (mem_in_first, 1))
         (pp_spec_cut
            (pp_predicate
               (pp_mem_trans_aux
                  pp_machine_decl pp_machine_decl pp_print_string pp_print_string)
               (pp_ite
                  (pp_access pp_print_string pp_access')
                  (pp_paren
                     (pp_and
                        (pp_equal
                           (pp_access pp_print_string pp_access')
                           pp_print_int)
                        (pp_equal pp_print_string pp_print_string)))
                     (pp_paren
                        (pp_and
                           (pp_equal
                              (pp_access pp_print_string pp_access')
                              (pp_access pp_print_string pp_access'))
                           (pp_equal pp_print_string pp_print_string))))))
         ((name, ["integer x"; "integer y"], [], ["_Bool out"],
           (name, "mem_ghost", mem_in), (name, "mem_ghost", mem_out)),
          (* (("out", mem_in_first), *)
          (mem_in_first, ((mem_out_first, 0), ("out", "x")),
           ((mem_out_first, mem_in_first), ("out", "y"))))
         (pp_spec_cut
            (pp_predicate
               (pp_mem_ghost pp_machine_decl pp_machine_decl)
               (pp_equal
                  (pp_access pp_print_string pp_access')
                  (pp_indirect pp_print_string pp_access'))))
         ((name, (name, "mem_ghost", mem), (name, "mem", "*" ^ self)),
         ((mem, reg_first), (self, reg_first)))
     let pp_register =
       pp_print_list
         ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
         ~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first")
         ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
         (fun fmt (i, _) -> pp_print_string fmt i)
     module HdrMod = struct
       let print_machine_decl_prefix = fun _ _ -> ()
       let pp_import_standard_spec fmt () =
         fprintf fmt "@,#include \"%s/arrow_spec.h%s\""
           (Arrow.arrow_top_decl ()).top_decl_owner
           (if !Options.cpp then "pp" else "")
     end
     module SrcMod = struct
       let pp_predicates dependencies fmt machines =
         fprintf fmt
           "%a@,%a%a%a%a"
           pp_arrow_spec ()
           "%a%a%a%a"
           (pp_print_list
              ~pp_open_box:pp_open_vbox0
              ~pp_prologue:(pp_print_endcut "/* ACSL `valid` predicates */")
-...
              (print_machine_trans_annotations machines dependencies)
              ~pp_epilogue:pp_print_cutcut) machines
       let pp_register =
         pp_print_list
           ~pp_prologue:(fun fmt () -> pp_print_string fmt "self->")
           ~pp_epilogue:(fun fmt () -> pp_print_string fmt "->_reg._first")
           ~pp_sep:(fun fmt () -> pp_print_string fmt "->")
           (fun fmt (i, _) -> pp_print_string fmt i)
       let pp_reset_spec fmt machines self m =
         let name = m.mname.node_id in
         let mem = mk_mem m in

       | _ -> false
     let generate_c_header = ref false
     (* check whether a source file has a compiled header, if not, generate the
        compiled header *)
     let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
-...
               (if from_lusi then prog else Lusic.extract_header dirname basename prog)
               destname
               lusic_ext;
             if !Options.output = "C"
             then C_backend_lusic.print_lusic_to_h destname lusic_ext
             generate_c_header := !Options.output = "C";
           end
         else (* Lusic exists and is usable. Checking compatibility *)
           begin
-...
         "C", ".lus" ->
          begin
            Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
            C_backend.translate_to_c
            C_backend.translate_to_c !generate_c_header
     	 (* alloc_header_file source_lib_file source_main_file makefile_file *)
     	 basename prog machine_code dependencies
          end
-...
     *)
       |  "C", _ ->
           begin
             C_backend.print_c_header basename;
           	Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");
           end
       | "java", _ ->

      (modules
        lusic
        c_backend_header c_backend_spec c_backend_makefile
        c_backend_lusic c_backend_mauve c_backend_src
        c_backend_mauve c_backend_src
        ada_backend ada_printer ada_backend_common ada_backend_ads ada_backend_adb
        ada_backend_wrapper
        horn_backend horn_backend_common horn_backend_printers

       contents  : top_decl list;
+    }
     module HeaderMod = C_backend_header.EmptyMod
     module Header = C_backend_header.Main (HeaderMod)
     (* extracts a header from a program representing module owner = dirname/basename *)
     let extract_header dirname basename prog =
       let owner = dirname ^ "/" ^ basename in

Project

General

Profile

CristalCaveGem » LustreC

Revision efcc8d7f

Added by Lélio Brun about 2 years ago