Merge branch 'lustrec-seal' of https://cavale.enseeiht.fr/git/lustrec into lustrec-seal

src/backends/Ada/ada_backend.ml

@@ -42,14 +42,6 @@ let write_file destname pp_filename pp_file arg =
   close_out out
 
 
-(** Print the filename of a machine package.
-   @param extension the extension to append to the package name
-   @param fmt the formatter
-   @param machine the machine corresponding to the package
-**)
-let pp_machine_filename extension fmt machine =
-  pp_filename extension fmt (function fmt -> pp_package_name fmt machine)
-
 (** Exception raised when a machine contains a feature not supported by the
   Ada backend*)
 exception CheckFailed of string
@@ -64,13 +56,6 @@ let check machine =
     | [] -> ()
     | _ -> raise (CheckFailed "machine.mconst should be void")
 
-(** Print the name of the ada project file.
-   @param fmt the formater to print on
-   @param main_machine the machine associated to the main node
-**)
-let pp_project_name fmt main_machine =
-  fprintf fmt "%a.gpr" pp_package_name main_machine
-
 
 let get_typed_submachines machines m =
   let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in
@@ -83,7 +68,7 @@ let get_typed_submachines machines m =
 
 (** Main function of the Ada backend. It calls all the subfunction creating all
 the file and fill them with Ada code representing the machines list given.
-   @param basename useless
+   @param basename name of the lustre file
    @param prog useless
    @param prog list of machines to translate
    @param dependencies useless
@@ -98,7 +83,7 @@ let translate_to_ada basename prog machines dependencies =
 
   let _machines = List.combine typed_submachines machines in
 
-  let _pp_filename ext fmt (typed_submachines, machine) =
+  let _pp_filename ext fmt (typed_submachine, machine) =
     pp_machine_filename ext fmt machine in
 
   (* Extract the main machine if there is one *)
@@ -126,15 +111,13 @@ let translate_to_ada basename prog machines dependencies =
 
   (* If a main node is given we generate a main adb file and a project file *)
   log_str_level_two 1 "Generating wrapper files";
-  match main_machine with
-    | None -> log_str_level_two 2 "File not generated(no -node argument)";
+  (match main_machine with
+    | None -> ()
     | Some machine ->
-begin
-  let pp_main_filename fmt _ =
-    pp_filename "adb" fmt pp_main_procedure_name in
-  write_file destname pp_project_name Wrapper.pp_project_file machine;
-  write_file destname pp_main_filename Wrapper.pp_main_adb machine;
-end
+        write_file destname pp_main_filename Wrapper.pp_main_adb machine;
+        write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file machines basename) main_machine);
+  write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
+  write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file machines basename) None;
 
 
 (* Local Variables: *)

src/backends/Ada/ada_backend_adb.ml

@@ -170,13 +170,14 @@ struct
      @param fmt the formater to print on
      @param machine the machine
   **)
-  let pp_step_definition typed_submachines fmt m = pp_procedure_definition
-        pp_step_procedure_name
-        (pp_step_prototype m)
-        (pp_machine_var_decl NoMode)
-        (pp_machine_instr typed_submachines m)
-        fmt
-        (m.mstep.step_locals, m.mstep.step_instrs)
+  let pp_step_definition typed_submachines fmt m =
+    pp_procedure_definition
+      pp_step_procedure_name
+      (pp_step_prototype m)
+      (pp_machine_var_decl NoMode)
+      (pp_machine_instr typed_submachines m)
+      fmt
+      (m.mstep.step_locals, m.mstep.step_instrs)
 
   (** Print the definition of the reset procedure from a machine.
 
@@ -184,13 +185,18 @@ struct
      @param fmt the formater to print on
      @param machine the machine
   **)
-  let pp_reset_definition typed_submachines fmt m = pp_procedure_definition
-        pp_reset_procedure_name
-        (pp_reset_prototype m)
-        (pp_machine_var_decl NoMode)
-        (pp_machine_instr typed_submachines m)
-        fmt
-        ([], m.minit)
+  let pp_reset_definition typed_submachines fmt m =
+    let build_assign = function var ->
+      mkinstr (MStateAssign (var, mk_default_value var.var_type))
+    in
+    let assigns = List.map build_assign m.mmemory in
+    pp_procedure_definition
+      pp_reset_procedure_name
+      (pp_reset_prototype m)
+      (pp_machine_var_decl NoMode)
+      (pp_machine_instr typed_submachines m)
+      fmt
+      ([], assigns@m.minit)
 
   (** Print the package definition(ads) of a machine.
     It requires the list of all typed instance.

src/backends/Ada/ada_backend_ads.ml

@@ -106,8 +106,9 @@ struct
   let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
     match opt_contract with
       | None -> pp_prototype fmt
-      | Some contract -> 
-          fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
+      | Some (NodeSpec ident) -> pp_prototype fmt (*TODO*)
+      | Some (Contract contract) ->
+          fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]"
             pp_prototype
             (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
             (Utils.pp_final_char_if_non_empty ",@," contract.assume)
@@ -118,13 +119,11 @@ struct
      @param machine the machine
   **)
   let pp_step_prototype_contract fmt m =
-    ()
-      (* Temporarily disabled while waiting for the code to stabilize 
-pp_procedure_prototype_contract
-        (pp_step_prototype m)
-        fmt
-        m.mspec
-       *)
+    pp_procedure_prototype_contract
+      (pp_step_prototype m)
+      fmt
+      m.mspec
+       
     
   (** Remove duplicates from a list according to a given predicate.
      @param eq the predicate defining equality

src/backends/Ada/ada_backend_common.ml

@@ -14,10 +14,34 @@ exception Ada_not_supported of string
 
 let is_machine_statefull m = not m.mname.node_dec_stateless
 
+(*TODO Check all this function with unit test, improve this system and
+   add support for : "cbrt", "erf", "log10", "pow", "atan2".
+*)
 let ada_supported_funs =
-  [("sin", ("Ada.Numerics.Elementary_Functions", "Sin"));
-   ("cos", ("Ada.Numerics.Elementary_Functions", "Cos"));
-   ("tan", ("Ada.Numerics.Elementary_Functions", "Tan"))]
+  [("sqrt",  ("Ada.Numerics.Elementary_Functions", "Sqrt"));
+   ("log",   ("Ada.Numerics.Elementary_Functions", "Log"));
+   ("exp",   ("Ada.Numerics.Elementary_Functions", "Exp"));
+   ("pow",   ("Ada.Numerics.Elementary_Functions", "**"));
+   ("sin",   ("Ada.Numerics.Elementary_Functions", "Sin"));
+   ("cos",   ("Ada.Numerics.Elementary_Functions", "Cos"));
+   ("tan",   ("Ada.Numerics.Elementary_Functions", "Tan"));
+   ("asin",  ("Ada.Numerics.Elementary_Functions", "Arcsin"));
+   ("acos",  ("Ada.Numerics.Elementary_Functions", "Arccos"));
+   ("atan",  ("Ada.Numerics.Elementary_Functions", "Arctan"));
+   ("sinh",  ("Ada.Numerics.Elementary_Functions", "Sinh"));
+   ("cosh",  ("Ada.Numerics.Elementary_Functions", "Cosh"));
+   ("tanh",  ("Ada.Numerics.Elementary_Functions", "Tanh"));
+   ("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
+   ("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
+   ("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
+   
+   ("ceil",  ("", "Float'Ceiling"));
+   ("floor", ("", "Float'Floor"));
+   ("fmod",  ("", "Float'Remainder"));
+   ("round", ("", "Float'Rounding"));
+   ("trunc", ("", "Float'Truncation"));
+
+   ("fabs", ("", "abs"));]
 
 let is_builtin_fun ident =
   List.mem ident Basic_library.internal_funs ||
@@ -82,27 +106,25 @@ let pp_filename extension fmt pp_name =
 
 (* Package pretty print functions *)
 
+(** Return true if its the arrow machine
+   @param machine the machine to test
+*)
+let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id
+
 (** Print the name of the arrow package.
    @param fmt the formater to print on
 **)
 let pp_arrow_package_name fmt = fprintf fmt "Arrow"
 
-(** Print the name of a package associated to a node.
-   @param fmt the formater to print on
-   @param machine the machine
-**)
-let pp_package_name_from_node fmt node =
-  if String.equal Arrow.arrow_id node.node_id then
-      fprintf fmt "%t" pp_arrow_package_name
-  else
-      fprintf fmt "%a" pp_clean_ada_identifier node.node_id
-
 (** Print the name of a package associated to a machine.
    @param fmt the formater to print on
    @param machine the machine
 **)
 let pp_package_name fmt machine =
-  pp_package_name_from_node fmt machine.mname
+  if is_arrow machine then
+      fprintf fmt "%t" pp_arrow_package_name
+  else
+      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
 
 (** Print the ada package introduction sentence it can be used for body and
 declaration. Boolean parameter body should be true if it is a body delcaration.
@@ -177,7 +199,7 @@ let get_machine machines instance =
     try
       List.find (function m -> m.mname.node_id=id) machines
     with
-      Not_found -> assert false
+      Not_found -> assert false (*TODO*)
 
 
 (* Type pretty print functions *)
@@ -246,7 +268,7 @@ let pp_type fmt typ =
     | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt
     | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
     | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
-    | Types.Tunivar                  -> pp_polymorphic_type fmt typ.tid
+    | Types.Tunivar                  -> pp_polymorphic_type fmt typ.Types.tid
     | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
     | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
     | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
@@ -261,6 +283,22 @@ let pp_type fmt typ =
     (*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
   )
 
+(** Return a default ada constant for a given type.
+   @param cst_typ the constant type
+**)
+let default_ada_cst cst_typ = match cst_typ with
+  | Types.Basic.Tint  -> Const_int 0
+  | Types.Basic.Treal -> Const_real (Num.num_of_int 0, 0, "0.0")
+  | Types.Basic.Tbool -> Const_tag tag_false
+  | _ -> assert false
+
+(** Make a default value from a given type.
+   @param typ the type
+**)
+let mk_default_value typ =
+  match (Types.repr typ).Types.tdesc with
+    | Types.Tbasic t  -> mk_val (Cst (default_ada_cst t)) typ
+    | _                              -> assert false (*TODO*)
 
 (** Test if two types are the same.
    @param typ1 the first type
@@ -472,7 +510,7 @@ let pp_step_prototype m fmt =
    @param pp_name name function printer
 **)
 let pp_reset_prototype m fmt =
-  let state_mode = if is_machine_statefull m then Some InOut else None in
+  let state_mode = if is_machine_statefull m then Some Out else None in
   pp_base_prototype state_mode m.mstatic [] fmt pp_reset_procedure_name
 
 (** Print the prototype of the init procedure of a machine.
@@ -685,7 +723,8 @@ let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals,
   let pp_ada_const fmt c =
     match c with
     | Const_int i                     -> pp_print_int fmt i
-    | Const_real (c, e, s)            -> pp_print_string fmt s
+    | Const_real (c, e, s)            ->
+        fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
     | Const_tag t                     -> pp_ada_tag fmt t
     | Const_string _ | Const_modeid _ ->
       (Format.eprintf
@@ -788,3 +827,14 @@ let pp_procedure_definition pp_name pp_prototype pp_local pp_instr fmt (locals,
     | _                 ->
       raise (Ada_not_supported
                "unsupported: Ada_backend.adb.pp_value does not support this value type")
+
+
+(** Print the filename of a machine package.
+   @param extension the extension to append to the package name
+   @param fmt the formatter
+   @param machine the machine corresponding to the package
+**)
+let pp_machine_filename extension fmt machine =
+  pp_filename extension fmt (function fmt -> pp_package_name fmt machine)
+
+let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name

src/backends/Ada/ada_backend_wrapper.ml

@@ -49,7 +49,7 @@ struct
      @param machine the main machine
   **)
   let pp_main_adb fmt machine =
-    let pp_str str fmt = fprintf fmt "%s"str in
+    let pp_str str fmt = fprintf fmt "%s" str in
     (* Dependances *)
     let text_io = "Ada.Text_IO" in
     let float_io = "package Float_IO is new Ada.Text_IO.Float_IO(Float)" in
@@ -119,14 +119,80 @@ struct
       pp_with_machine machine
       (pp_main_procedure_definition machine) (locals, instrs)
 
-  (** Print the gpr project file.
+  (** Print the name of the ada project configuration file.
+     @param fmt the formater to print on
+     @param main_machine the machine associated to the main node
+  **)
+  let pp_project_configuration_name fmt basename =
+    fprintf fmt "%s.adc" basename
+
+  (** Print the project configuration file.
      @param fmt the formater to print on
      @param machine the main machine
   **)
-  let pp_project_file fmt machine =
-      fprintf fmt "project %a is@.  for Main use (\"%a\");@.end %a;"
-        pp_package_name machine
-        (pp_filename "adb") pp_main_procedure_name
-        pp_package_name machine
+  let pp_project_configuration_file fmt machine =
+    fprintf fmt "pragma SPARK_Mode (On);"
+
+  (** Print the name of the ada project file.
+     @param base_name name of the lustre file
+     @param fmt the formater to print on
+     @param machine_opt the main machine option
+  **)
+  let pp_project_name basename fmt machine_opt =
+    fprintf fmt "%s.gpr" basename
+
+  let pp_for_single name arg fmt =
+    fprintf fmt "for %s use \"%s\"" name arg
+
+  let pp_for name args fmt =
+    fprintf fmt "for %s use (@[%a@])" name
+      (Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg))
+      args
+
+  let pp_content fmt lines =
+    fprintf fmt "  @[<v>%a%t@]"
+      (Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines
+      (Utils.pp_final_char_if_non_empty ";" lines)
+
+  let pp_package name lines fmt =
+    fprintf fmt "package %s is@,%a@,end %s"
+      name
+      pp_content lines
+      name
+
+  (** Print the gpr project file, if there is a machine in machine_opt then
+        an executable project is made else it is a library.
+     @param fmt the formater to print on
+     @param machine_opt the main machine option
+  **)
+  let pp_project_file machines basename fmt machine_opt =
+    let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines)
+                  @(match machine_opt with
+                    | None -> []
+                    | Some m -> [asprintf "%a" pp_main_filename m]) in
+    let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in
+    fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name
+    pp_content
+    ((match machine_opt with
+      | None -> [
+          pp_for_single "Library_Name" basename;
+          pp_for_single "Library_Dir" "lib";
+        ]
+      | Some machine -> [
+          pp_for "Main" [asprintf "%t" pp_main_procedure_name];
+          pp_for_single "Exec_Dir" "bin";
+        ])
+    @[
+      pp_for_single "Object_Dir" "obj";
+      pp_for "Source_Files" adbs;
+      pp_package "Builder" [
+        pp_for_single "Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename);
+      ];
+      pp_package "Prove" [
+        pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"];
+      ]
+    ])
+    project_name
+
 
   end

src/backends/EMF/EMF_backend.ml

@@ -547,7 +547,7 @@ let translate fmt basename prog machines =
   fprintf fmt "\"nodes\": @[<v 0>{@ ";
   (* Previous alternative: mapping normalized lustre to EMF: 
      fprintf_list ~sep:",@ " pp_decl fmt prog; *)
-  pp_emf_list pp_machine fmt (List.rev machines);
+  pp_emf_list pp_machine fmt machines;
   fprintf fmt "}@]@ }";
   fprintf fmt "@]@ }"
 

src/backends/EMF/EMF_common.ml

@@ -236,22 +236,23 @@ let pp_tag_id fmt t =
     fprintf fmt "%i" (get_idx t const_list)
 
 let pp_cst_type c inf fmt (*infered_typ*) =
+  let pp_basic fmt s = fprintf fmt "{ \"kind\": \"%s\" }" s in
   match c with
   | Const_tag t ->
      let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
      if typ.tydef_id = "bool" then
-       fprintf fmt "\"bool\""
+       pp_basic fmt "bool"
      else
        pp_tag_type t typ inf fmt
-  | Const_int _ -> fprintf fmt "\"int\"" (*!Options.int_type*)
-  | Const_real _ -> fprintf fmt "\"real\"" (*!Options.real_type*)
-  | Const_string _ -> fprintf fmt "\"string\"" 
+  | Const_int _ -> pp_basic fmt "int" (*!Options.int_type*)
+  | Const_real _ -> pp_basic fmt "real" (*!Options.real_type*)
+  | Const_string _ -> pp_basic fmt "string" 
   | _ -> eprintf "cst: %a@." Printers.pp_const c; assert false
 
     
 let pp_emf_cst c inf fmt =
-  let pp_typ fmt =
-    fprintf fmt "\"datatype\": { \"kind\": %t } @ "
+  let pp_typ fmt = 
+    fprintf fmt "\"datatype\": %t@ "
       (pp_cst_type c inf)   
   in
   match c with