Skip to content
Snippets Groups Projects
Commit 61e0c3c4 authored by Guillaume DAVY's avatar Guillaume DAVY
Browse files

Ada:

  - Correct the merge with lustrec-seal
  - Improve support for builtin function(still work to do)
  - Add generation of a gpr file for lib(without main).
  - Add var initialisation in the reset, still work to do.
parent 4d2d6777
No related branches found
No related tags found
No related merge requests found
......@@ -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: *)
......
......@@ -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.
......
......@@ -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
......
......@@ -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,21 @@ 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
(** 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 +509,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 +722,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 +826,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
......@@ -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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment