Revision 61e0c3c4
Added by Guillaume DAVY about 4 years ago
src/backends/Ada/ada_backend.ml | ||
---|---|---|
42 | 42 |
close_out out |
43 | 43 |
|
44 | 44 |
|
45 |
(** Print the filename of a machine package. |
|
46 |
@param extension the extension to append to the package name |
|
47 |
@param fmt the formatter |
|
48 |
@param machine the machine corresponding to the package |
|
49 |
**) |
|
50 |
let pp_machine_filename extension fmt machine = |
|
51 |
pp_filename extension fmt (function fmt -> pp_package_name fmt machine) |
|
52 |
|
|
53 | 45 |
(** Exception raised when a machine contains a feature not supported by the |
54 | 46 |
Ada backend*) |
55 | 47 |
exception CheckFailed of string |
... | ... | |
64 | 56 |
| [] -> () |
65 | 57 |
| _ -> raise (CheckFailed "machine.mconst should be void") |
66 | 58 |
|
67 |
(** Print the name of the ada project file. |
|
68 |
@param fmt the formater to print on |
|
69 |
@param main_machine the machine associated to the main node |
|
70 |
**) |
|
71 |
let pp_project_name fmt main_machine = |
|
72 |
fprintf fmt "%a.gpr" pp_package_name main_machine |
|
73 |
|
|
74 | 59 |
|
75 | 60 |
let get_typed_submachines machines m = |
76 | 61 |
let instances = List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls in |
... | ... | |
83 | 68 |
|
84 | 69 |
(** Main function of the Ada backend. It calls all the subfunction creating all |
85 | 70 |
the file and fill them with Ada code representing the machines list given. |
86 |
@param basename useless
|
|
71 |
@param basename name of the lustre file
|
|
87 | 72 |
@param prog useless |
88 | 73 |
@param prog list of machines to translate |
89 | 74 |
@param dependencies useless |
... | ... | |
98 | 83 |
|
99 | 84 |
let _machines = List.combine typed_submachines machines in |
100 | 85 |
|
101 |
let _pp_filename ext fmt (typed_submachines, machine) =
|
|
86 |
let _pp_filename ext fmt (typed_submachine, machine) = |
|
102 | 87 |
pp_machine_filename ext fmt machine in |
103 | 88 |
|
104 | 89 |
(* Extract the main machine if there is one *) |
... | ... | |
126 | 111 |
|
127 | 112 |
(* If a main node is given we generate a main adb file and a project file *) |
128 | 113 |
log_str_level_two 1 "Generating wrapper files"; |
129 |
match main_machine with |
|
130 |
| None -> log_str_level_two 2 "File not generated(no -node argument)";
|
|
114 |
(match main_machine with
|
|
115 |
| None -> ()
|
|
131 | 116 |
| Some machine -> |
132 |
begin |
|
133 |
let pp_main_filename fmt _ = |
|
134 |
pp_filename "adb" fmt pp_main_procedure_name in |
|
135 |
write_file destname pp_project_name Wrapper.pp_project_file machine; |
|
136 |
write_file destname pp_main_filename Wrapper.pp_main_adb machine; |
|
137 |
end |
|
117 |
write_file destname pp_main_filename Wrapper.pp_main_adb machine; |
|
118 |
write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file machines basename) main_machine); |
|
119 |
write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename; |
|
120 |
write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file machines basename) None; |
|
138 | 121 |
|
139 | 122 |
|
140 | 123 |
(* Local Variables: *) |
src/backends/Ada/ada_backend_adb.ml | ||
---|---|---|
170 | 170 |
@param fmt the formater to print on |
171 | 171 |
@param machine the machine |
172 | 172 |
**) |
173 |
let pp_step_definition typed_submachines fmt m = pp_procedure_definition |
|
174 |
pp_step_procedure_name |
|
175 |
(pp_step_prototype m) |
|
176 |
(pp_machine_var_decl NoMode) |
|
177 |
(pp_machine_instr typed_submachines m) |
|
178 |
fmt |
|
179 |
(m.mstep.step_locals, m.mstep.step_instrs) |
|
173 |
let pp_step_definition typed_submachines fmt m = |
|
174 |
pp_procedure_definition |
|
175 |
pp_step_procedure_name |
|
176 |
(pp_step_prototype m) |
|
177 |
(pp_machine_var_decl NoMode) |
|
178 |
(pp_machine_instr typed_submachines m) |
|
179 |
fmt |
|
180 |
(m.mstep.step_locals, m.mstep.step_instrs) |
|
180 | 181 |
|
181 | 182 |
(** Print the definition of the reset procedure from a machine. |
182 | 183 |
|
... | ... | |
184 | 185 |
@param fmt the formater to print on |
185 | 186 |
@param machine the machine |
186 | 187 |
**) |
187 |
let pp_reset_definition typed_submachines fmt m = pp_procedure_definition |
|
188 |
pp_reset_procedure_name |
|
189 |
(pp_reset_prototype m) |
|
190 |
(pp_machine_var_decl NoMode) |
|
191 |
(pp_machine_instr typed_submachines m) |
|
192 |
fmt |
|
193 |
([], m.minit) |
|
188 |
let pp_reset_definition typed_submachines fmt m = |
|
189 |
let build_assign = function var -> |
|
190 |
mkinstr (MStateAssign (var, mk_default_value var.var_type)) |
|
191 |
in |
|
192 |
let assigns = List.map build_assign m.mmemory in |
|
193 |
pp_procedure_definition |
|
194 |
pp_reset_procedure_name |
|
195 |
(pp_reset_prototype m) |
|
196 |
(pp_machine_var_decl NoMode) |
|
197 |
(pp_machine_instr typed_submachines m) |
|
198 |
fmt |
|
199 |
([], assigns@m.minit) |
|
194 | 200 |
|
195 | 201 |
(** Print the package definition(ads) of a machine. |
196 | 202 |
It requires the list of all typed instance. |
src/backends/Ada/ada_backend_ads.ml | ||
---|---|---|
106 | 106 |
let pp_procedure_prototype_contract pp_prototype fmt opt_contract = |
107 | 107 |
match opt_contract with |
108 | 108 |
| None -> pp_prototype fmt |
109 |
| Some contract -> |
|
110 |
fprintf fmt "@[<v 2>%t with@,%a%t%a@]" |
|
109 |
| Some (NodeSpec ident) -> pp_prototype fmt (*TODO*) |
|
110 |
| Some (Contract contract) -> |
|
111 |
fprintf fmt "@[<v 2>%t with@,Global => null;@,%a%t%a@]" |
|
111 | 112 |
pp_prototype |
112 | 113 |
(Utils.fprintf_list ~sep:",@," pp_pre) contract.assume |
113 | 114 |
(Utils.pp_final_char_if_non_empty ",@," contract.assume) |
... | ... | |
118 | 119 |
@param machine the machine |
119 | 120 |
**) |
120 | 121 |
let pp_step_prototype_contract fmt m = |
121 |
() |
|
122 |
(* Temporarily disabled while waiting for the code to stabilize |
|
123 |
pp_procedure_prototype_contract |
|
124 |
(pp_step_prototype m) |
|
125 |
fmt |
|
126 |
m.mspec |
|
127 |
*) |
|
122 |
pp_procedure_prototype_contract |
|
123 |
(pp_step_prototype m) |
|
124 |
fmt |
|
125 |
m.mspec |
|
126 |
|
|
128 | 127 |
|
129 | 128 |
(** Remove duplicates from a list according to a given predicate. |
130 | 129 |
@param eq the predicate defining equality |
src/backends/Ada/ada_backend_common.ml | ||
---|---|---|
14 | 14 |
|
15 | 15 |
let is_machine_statefull m = not m.mname.node_dec_stateless |
16 | 16 |
|
17 |
(*TODO Check all this function with unit test, improve this system and |
|
18 |
add support for : "cbrt", "erf", "log10", "pow", "atan2". |
|
19 |
*) |
|
17 | 20 |
let ada_supported_funs = |
18 |
[("sin", ("Ada.Numerics.Elementary_Functions", "Sin")); |
|
19 |
("cos", ("Ada.Numerics.Elementary_Functions", "Cos")); |
|
20 |
("tan", ("Ada.Numerics.Elementary_Functions", "Tan"))] |
|
21 |
[("sqrt", ("Ada.Numerics.Elementary_Functions", "Sqrt")); |
|
22 |
("log", ("Ada.Numerics.Elementary_Functions", "Log")); |
|
23 |
("exp", ("Ada.Numerics.Elementary_Functions", "Exp")); |
|
24 |
("pow", ("Ada.Numerics.Elementary_Functions", "**")); |
|
25 |
("sin", ("Ada.Numerics.Elementary_Functions", "Sin")); |
|
26 |
("cos", ("Ada.Numerics.Elementary_Functions", "Cos")); |
|
27 |
("tan", ("Ada.Numerics.Elementary_Functions", "Tan")); |
|
28 |
("asin", ("Ada.Numerics.Elementary_Functions", "Arcsin")); |
|
29 |
("acos", ("Ada.Numerics.Elementary_Functions", "Arccos")); |
|
30 |
("atan", ("Ada.Numerics.Elementary_Functions", "Arctan")); |
|
31 |
("sinh", ("Ada.Numerics.Elementary_Functions", "Sinh")); |
|
32 |
("cosh", ("Ada.Numerics.Elementary_Functions", "Cosh")); |
|
33 |
("tanh", ("Ada.Numerics.Elementary_Functions", "Tanh")); |
|
34 |
("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh")); |
|
35 |
("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh")); |
|
36 |
("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh")); |
|
37 |
|
|
38 |
("ceil", ("", "Float'Ceiling")); |
|
39 |
("floor", ("", "Float'Floor")); |
|
40 |
("fmod", ("", "Float'Remainder")); |
|
41 |
("round", ("", "Float'Rounding")); |
|
42 |
("trunc", ("", "Float'Truncation")); |
|
43 |
|
|
44 |
("fabs", ("", "abs"));] |
|
21 | 45 |
|
22 | 46 |
let is_builtin_fun ident = |
23 | 47 |
List.mem ident Basic_library.internal_funs || |
... | ... | |
82 | 106 |
|
83 | 107 |
(* Package pretty print functions *) |
84 | 108 |
|
109 |
(** Return true if its the arrow machine |
|
110 |
@param machine the machine to test |
|
111 |
*) |
|
112 |
let is_arrow machine = String.equal Arrow.arrow_id machine.mname.node_id |
|
113 |
|
|
85 | 114 |
(** Print the name of the arrow package. |
86 | 115 |
@param fmt the formater to print on |
87 | 116 |
**) |
88 | 117 |
let pp_arrow_package_name fmt = fprintf fmt "Arrow" |
89 | 118 |
|
90 |
(** Print the name of a package associated to a node. |
|
91 |
@param fmt the formater to print on |
|
92 |
@param machine the machine |
|
93 |
**) |
|
94 |
let pp_package_name_from_node fmt node = |
|
95 |
if String.equal Arrow.arrow_id node.node_id then |
|
96 |
fprintf fmt "%t" pp_arrow_package_name |
|
97 |
else |
|
98 |
fprintf fmt "%a" pp_clean_ada_identifier node.node_id |
|
99 |
|
|
100 | 119 |
(** Print the name of a package associated to a machine. |
101 | 120 |
@param fmt the formater to print on |
102 | 121 |
@param machine the machine |
103 | 122 |
**) |
104 | 123 |
let pp_package_name fmt machine = |
105 |
pp_package_name_from_node fmt machine.mname |
|
124 |
if is_arrow machine then |
|
125 |
fprintf fmt "%t" pp_arrow_package_name |
|
126 |
else |
|
127 |
fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id |
|
106 | 128 |
|
107 | 129 |
(** Print the ada package introduction sentence it can be used for body and |
108 | 130 |
declaration. Boolean parameter body should be true if it is a body delcaration. |
... | ... | |
177 | 199 |
try |
178 | 200 |
List.find (function m -> m.mname.node_id=id) machines |
179 | 201 |
with |
180 |
Not_found -> assert false |
|
202 |
Not_found -> assert false (*TODO*)
|
|
181 | 203 |
|
182 | 204 |
|
183 | 205 |
(* Type pretty print functions *) |
... | ... | |
246 | 268 |
| Types.Tbasic Types.Basic.Tint -> pp_integer_type fmt |
247 | 269 |
| Types.Tbasic Types.Basic.Treal -> pp_float_type fmt |
248 | 270 |
| Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt |
249 |
| Types.Tunivar -> pp_polymorphic_type fmt typ.tid |
|
271 |
| Types.Tunivar -> pp_polymorphic_type fmt typ.Types.tid
|
|
250 | 272 |
| Types.Tbasic _ -> eprintf "Tbasic@."; assert false (*TODO*) |
251 | 273 |
| Types.Tconst _ -> eprintf "Tconst@."; assert false (*TODO*) |
252 | 274 |
| Types.Tclock _ -> eprintf "Tclock@."; assert false (*TODO*) |
... | ... | |
261 | 283 |
(*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *) |
262 | 284 |
) |
263 | 285 |
|
286 |
(** Return a default ada constant for a given type. |
|
287 |
@param cst_typ the constant type |
|
288 |
**) |
|
289 |
let default_ada_cst cst_typ = match cst_typ with |
|
290 |
| Types.Basic.Tint -> Const_int 0 |
|
291 |
| Types.Basic.Treal -> Const_real (Num.num_of_int 0, 0, "0.0") |
|
292 |
| Types.Basic.Tbool -> Const_tag tag_false |
|
293 |
|
|
294 |
(** Make a default value from a given type. |
|
295 |
@param typ the type |
|
296 |
**) |
|
297 |
let mk_default_value typ = |
|
298 |
match (Types.repr typ).Types.tdesc with |
|
299 |
| Types.Tbasic t -> mk_val (Cst (default_ada_cst t)) typ |
|
300 |
| _ -> assert false (*TODO*) |
|
264 | 301 |
|
265 | 302 |
(** Test if two types are the same. |
266 | 303 |
@param typ1 the first type |
... | ... | |
472 | 509 |
@param pp_name name function printer |
473 | 510 |
**) |
474 | 511 |
let pp_reset_prototype m fmt = |
475 |
let state_mode = if is_machine_statefull m then Some InOut else None in
|
|
512 |
let state_mode = if is_machine_statefull m then Some Out else None in |
|
476 | 513 |
pp_base_prototype state_mode m.mstatic [] fmt pp_reset_procedure_name |
477 | 514 |
|
478 | 515 |
(** Print the prototype of the init procedure of a machine. |
... | ... | |
685 | 722 |
let pp_ada_const fmt c = |
686 | 723 |
match c with |
687 | 724 |
| Const_int i -> pp_print_int fmt i |
688 |
| Const_real (c, e, s) -> pp_print_string fmt s |
|
725 |
| Const_real (c, e, s) -> |
|
726 |
fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e |
|
689 | 727 |
| Const_tag t -> pp_ada_tag fmt t |
690 | 728 |
| Const_string _ | Const_modeid _ -> |
691 | 729 |
(Format.eprintf |
... | ... | |
788 | 826 |
| _ -> |
789 | 827 |
raise (Ada_not_supported |
790 | 828 |
"unsupported: Ada_backend.adb.pp_value does not support this value type") |
829 |
|
|
830 |
|
|
831 |
(** Print the filename of a machine package. |
|
832 |
@param extension the extension to append to the package name |
|
833 |
@param fmt the formatter |
|
834 |
@param machine the machine corresponding to the package |
|
835 |
**) |
|
836 |
let pp_machine_filename extension fmt machine = |
|
837 |
pp_filename extension fmt (function fmt -> pp_package_name fmt machine) |
|
838 |
|
|
839 |
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name |
src/backends/Ada/ada_backend_wrapper.ml | ||
---|---|---|
49 | 49 |
@param machine the main machine |
50 | 50 |
**) |
51 | 51 |
let pp_main_adb fmt machine = |
52 |
let pp_str str fmt = fprintf fmt "%s"str in |
|
52 |
let pp_str str fmt = fprintf fmt "%s" str in
|
|
53 | 53 |
(* Dependances *) |
54 | 54 |
let text_io = "Ada.Text_IO" in |
55 | 55 |
let float_io = "package Float_IO is new Ada.Text_IO.Float_IO(Float)" in |
... | ... | |
119 | 119 |
pp_with_machine machine |
120 | 120 |
(pp_main_procedure_definition machine) (locals, instrs) |
121 | 121 |
|
122 |
(** Print the gpr project file. |
|
122 |
(** Print the name of the ada project configuration file. |
|
123 |
@param fmt the formater to print on |
|
124 |
@param main_machine the machine associated to the main node |
|
125 |
**) |
|
126 |
let pp_project_configuration_name fmt basename = |
|
127 |
fprintf fmt "%s.adc" basename |
|
128 |
|
|
129 |
(** Print the project configuration file. |
|
123 | 130 |
@param fmt the formater to print on |
124 | 131 |
@param machine the main machine |
125 | 132 |
**) |
126 |
let pp_project_file fmt machine = |
|
127 |
fprintf fmt "project %a is@. for Main use (\"%a\");@.end %a;" |
|
128 |
pp_package_name machine |
|
129 |
(pp_filename "adb") pp_main_procedure_name |
|
130 |
pp_package_name machine |
|
133 |
let pp_project_configuration_file fmt machine = |
|
134 |
fprintf fmt "pragma SPARK_Mode (On);" |
|
135 |
|
|
136 |
(** Print the name of the ada project file. |
|
137 |
@param base_name name of the lustre file |
|
138 |
@param fmt the formater to print on |
|
139 |
@param machine_opt the main machine option |
|
140 |
**) |
|
141 |
let pp_project_name basename fmt machine_opt = |
|
142 |
fprintf fmt "%s.gpr" basename |
|
143 |
|
|
144 |
let pp_for_single name arg fmt = |
|
145 |
fprintf fmt "for %s use \"%s\"" name arg |
|
146 |
|
|
147 |
let pp_for name args fmt = |
|
148 |
fprintf fmt "for %s use (@[%a@])" name |
|
149 |
(Utils.fprintf_list ~sep:",@ " (fun fmt arg -> fprintf fmt "\"%s\"" arg)) |
|
150 |
args |
|
151 |
|
|
152 |
let pp_content fmt lines = |
|
153 |
fprintf fmt " @[<v>%a%t@]" |
|
154 |
(Utils.fprintf_list ~sep:";@," (fun fmt pp -> fprintf fmt "%t" pp)) lines |
|
155 |
(Utils.pp_final_char_if_non_empty ";" lines) |
|
156 |
|
|
157 |
let pp_package name lines fmt = |
|
158 |
fprintf fmt "package %s is@,%a@,end %s" |
|
159 |
name |
|
160 |
pp_content lines |
|
161 |
name |
|
162 |
|
|
163 |
(** Print the gpr project file, if there is a machine in machine_opt then |
|
164 |
an executable project is made else it is a library. |
|
165 |
@param fmt the formater to print on |
|
166 |
@param machine_opt the main machine option |
|
167 |
**) |
|
168 |
let pp_project_file machines basename fmt machine_opt = |
|
169 |
let adbs = (List.map (asprintf "%a" (pp_machine_filename "adb")) machines) |
|
170 |
@(match machine_opt with |
|
171 |
| None -> [] |
|
172 |
| Some m -> [asprintf "%a" pp_main_filename m]) in |
|
173 |
let project_name = basename^(if machine_opt=None then "_lib" else "_exe") in |
|
174 |
fprintf fmt "%sproject %s is@,%a@,end %s;" (if machine_opt=None then "library " else "") project_name |
|
175 |
pp_content |
|
176 |
((match machine_opt with |
|
177 |
| None -> [ |
|
178 |
pp_for_single "Library_Name" basename; |
|
179 |
pp_for_single "Library_Dir" "lib"; |
|
180 |
] |
|
181 |
| Some machine -> [ |
|
182 |
pp_for "Main" [asprintf "%t" pp_main_procedure_name]; |
|
183 |
pp_for_single "Exec_Dir" "bin"; |
|
184 |
]) |
|
185 |
@[ |
|
186 |
pp_for_single "Object_Dir" "obj"; |
|
187 |
pp_for "Source_Files" adbs; |
|
188 |
pp_package "Builder" [ |
|
189 |
pp_for_single "Global_Configuration_Pragmas" (asprintf "%a" pp_project_configuration_name basename); |
|
190 |
]; |
|
191 |
pp_package "Prove" [ |
|
192 |
pp_for "Switches" ["--mode=prove"; "--report=statistics"; "--proof=per_check"; "--warnings=continue"]; |
|
193 |
] |
|
194 |
]) |
|
195 |
project_name |
|
196 |
|
|
131 | 197 |
|
132 | 198 |
end |
Also available in: Unified diff
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.