Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_common.ml @ 173a2a8f

History | View | Annotate | Download (14 KB)

1
open Format
2

    
3
open Machine_code_types
4
open Lustre_types
5
open Corelang
6
open Machine_code_common
7

    
8
open Ada_printer
9
open Misc_printer
10
open Misc_lustre_function
11

    
12
(** Exception for unsupported features in Ada backend **)
13
exception Ada_not_supported of string
14

    
15
(** Print the name of the state variable.
16
   @param fmt the formater to print on
17
**)
18
let pp_state_name fmt = fprintf fmt "state"
19
(** Print the type of the state variable.
20
   @param fmt the formater to print on
21
**)
22
let pp_state_type fmt = fprintf fmt "TState"
23
(** Print the name of the reset procedure
24
   @param fmt the formater to print on
25
**)
26
let pp_reset_procedure_name fmt = fprintf fmt "reset"
27
(** Print the name of the step procedure
28
   @param fmt the formater to print on
29
**)
30
let pp_step_procedure_name fmt = fprintf fmt "step"
31
(** Print the name of the main procedure.
32
   @param fmt the formater to print on
33
**)
34
let pp_main_procedure_name fmt = fprintf fmt "ada_main"
35
(** Print the name of the arrow package.
36
   @param fmt the formater to print on
37
**)
38
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
39
(** Print the type of a polymorphic type.
40
   @param fmt the formater to print on
41
   @param id the id of the polymorphic type
42
**)
43
let pp_polymorphic_type id fmt = fprintf fmt "T_%i" id
44

    
45
let pp_past_name nbr fmt = fprintf fmt "past_state_%i" nbr
46

    
47

    
48

    
49

    
50

    
51

    
52

    
53

    
54

    
55
(*TODO Check all this function with unit test, improve this system and
56
   add support for : "cbrt", "erf", "log10", "pow", "atan2".
57
*)
58
let ada_supported_funs =
59
  [("sqrt",  ("Ada.Numerics.Elementary_Functions", "Sqrt"));
60
   ("log",   ("Ada.Numerics.Elementary_Functions", "Log"));
61
   ("exp",   ("Ada.Numerics.Elementary_Functions", "Exp"));
62
   ("pow",   ("Ada.Numerics.Elementary_Functions", "**"));
63
   ("sin",   ("Ada.Numerics.Elementary_Functions", "Sin"));
64
   ("cos",   ("Ada.Numerics.Elementary_Functions", "Cos"));
65
   ("tan",   ("Ada.Numerics.Elementary_Functions", "Tan"));
66
   ("asin",  ("Ada.Numerics.Elementary_Functions", "Arcsin"));
67
   ("acos",  ("Ada.Numerics.Elementary_Functions", "Arccos"));
68
   ("atan",  ("Ada.Numerics.Elementary_Functions", "Arctan"));
69
   ("sinh",  ("Ada.Numerics.Elementary_Functions", "Sinh"));
70
   ("cosh",  ("Ada.Numerics.Elementary_Functions", "Cosh"));
71
   ("tanh",  ("Ada.Numerics.Elementary_Functions", "Tanh"));
72
   ("asinh", ("Ada.Numerics.Elementary_Functions", "Arcsinh"));
73
   ("acosh", ("Ada.Numerics.Elementary_Functions", "Arccosh"));
74
   ("atanh", ("Ada.Numerics.Elementary_Functions", "Arctanh"));
75
   
76
   ("ceil",  ("", "Float'Ceiling"));
77
   ("floor", ("", "Float'Floor"));
78
   ("fmod",  ("", "Float'Remainder"));
79
   ("round", ("", "Float'Rounding"));
80
   ("trunc", ("", "Float'Truncation"));
81

    
82
   ("fabs", ("", "abs"));]
83

    
84
let is_builtin_fun ident =
85
  List.mem ident Basic_library.internal_funs ||
86
    List.mem_assoc ident ada_supported_funs
87

    
88
(** Print the name of a package associated to a machine.
89
   @param fmt the formater to print on
90
   @param machine the machine
91
**)
92
let pp_package_name machine fmt =
93
  if is_arrow machine then
94
      fprintf fmt "%t" pp_arrow_package_name
95
  else
96
      fprintf fmt "%a" pp_clean_ada_identifier machine.mname.node_id
97

    
98
(** Print a type.
99
   @param fmt the formater to print on
100
   @param type the type
101
**)
102
let pp_type fmt typ = 
103
  (match (Types.repr typ).Types.tdesc with
104
    | Types.Tbasic Types.Basic.Tint  -> pp_integer_type fmt
105
    | Types.Tbasic Types.Basic.Treal -> pp_float_type fmt
106
    | Types.Tbasic Types.Basic.Tbool -> pp_boolean_type fmt
107
    | Types.Tunivar                  -> pp_polymorphic_type typ.Types.tid fmt
108
    | Types.Tbasic _                 -> eprintf "Tbasic@."; assert false (*TODO*)
109
    | Types.Tconst _                 -> eprintf "Tconst@."; assert false (*TODO*)
110
    | Types.Tclock _                 -> eprintf "Tclock@."; assert false (*TODO*)
111
    | Types.Tarrow _                 -> eprintf "Tarrow@."; assert false (*TODO*)
112
    | Types.Ttuple l                 -> eprintf "Ttuple %a @." (Utils.fprintf_list ~sep:" " Types.print_ty) l; assert false (*TODO*)
113
    | Types.Tenum _                  -> eprintf "Tenum@.";  assert false (*TODO*)
114
    | Types.Tstruct _                -> eprintf "Tstruct@.";assert false (*TODO*)
115
    | Types.Tarray _                 -> eprintf "Tarray@."; assert false (*TODO*)
116
    | Types.Tstatic _                -> eprintf "Tstatic@.";assert false (*TODO*)
117
    | Types.Tlink _                  -> eprintf "Tlink@.";  assert false (*TODO*)
118
    | Types.Tvar                     -> eprintf "Tvar@.";   assert false (*TODO*)
119
    (*| _ -> eprintf "Type error : %a@." Types.print_ty typ; assert false *)
120
  )
121

    
122
(** Return a default ada constant for a given type.
123
   @param cst_typ the constant type
124
**)
125
let default_ada_cst cst_typ = match cst_typ with
126
  | Types.Basic.Tint  -> Const_int 0
127
  | Types.Basic.Treal -> Const_real (Num.num_of_int 0, 0, "0.0")
128
  | Types.Basic.Tbool -> Const_tag tag_false
129
  | _ -> assert false
130

    
131
(** Make a default value from a given type.
132
   @param typ the type
133
**)
134
let mk_default_value typ =
135
  match (Types.repr typ).Types.tdesc with
136
    | Types.Tbasic t  -> mk_val (Cst (default_ada_cst t)) typ
137
    | _                              -> assert false (*TODO*)
138

    
139
(** Print the type of a variable.
140
   @param fmt the formater to print on
141
   @param id the variable
142
**)
143
let pp_var_type fmt id = 
144
  pp_type fmt id.var_type
145

    
146
(** Print a package name with polymorphic types specified.
147
   @param substitution correspondance between polymorphic type id and their instantiation
148
   @param fmt the formater to print on
149
   @param machine the machine
150
**)
151
let pp_package_name_with_polymorphic substitution machine fmt =
152
  let polymorphic_types = find_all_polymorphic_type machine in
153
  assert(List.length polymorphic_types = List.length substitution);
154
  let substituion = List.sort_uniq (fun x y -> fst x - fst y) substitution in
155
  assert(List.for_all2 (fun poly1 (poly2, _) -> poly1 = poly2)
156
            polymorphic_types substituion);
157
  let instantiated_types = snd (List.split substitution) in
158
  fprintf fmt "%t_inst%t%a"
159
    (pp_package_name machine)
160
    (Utils.pp_final_char_if_non_empty "_" instantiated_types)
161
    (Utils.fprintf_list ~sep:"_" pp_type) instantiated_types
162

    
163
(** Print the name of a variable.
164
   @param fmt the formater to print on
165
   @param id the variable
166
**)
167
let pp_var_name id fmt =
168
  fprintf fmt "%a" pp_clean_ada_identifier id.var_id
169

    
170
(** Print the complete name of variable.
171
   @param m the machine to check if it is memory
172
   @param fmt the formater to print on
173
   @param var the variable
174
**)
175
let pp_var env fmt var =
176
  match List.assoc_opt var.var_id env with
177
    | None -> pp_var_name var fmt
178
    | Some pp_state -> pp_access pp_state (pp_var_name var) fmt
179

    
180
(* Expression print functions *)
181

    
182
(* Printing functions for basic operations and expressions *)
183
(* TODO: refactor code -> use let rec and for basic pretty printing
184
   function *)
185
(** Printing function for Ada tags, mainly booleans.
186

    
187
    @param fmt the formater to use
188
    @param t the tag to print
189
 **)
190
let pp_ada_tag fmt t =
191
  pp_print_string fmt
192
    (if t = tag_true then "True" else if t = tag_false then "False" else t)
193

    
194
(** Printing function for machine type constants. For the moment,
195
    arrays are not supported.
196

    
197
    @param fmt the formater to use
198
    @param c the constant to print
199
 **)
200
let pp_ada_const fmt c =
201
  match c with
202
  | Const_int i                     -> pp_print_int fmt i
203
  | Const_real (c, e, s)            ->
204
      fprintf fmt "%s.0*1.0e-%i" (Num.string_of_num c) e
205
  | Const_tag t                     -> pp_ada_tag fmt t
206
  | Const_string _ | Const_modeid _ ->
207
    (Format.eprintf
208
       "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
209
     assert false)
210
  | _                               ->
211
    raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
212
    support this constant")
213

    
214
(** Printing function for expressions [v1 modulo v2]. Depends
215
    on option [integer_div_euclidean] to choose between mathematical
216
    modulo or remainder ([rem] in Ada).
217

    
218
    @param pp_value pretty printer for values
219
    @param v1 the first value in the expression
220
    @param v2 the second value in the expression
221
    @param fmt the formater to print on
222
 **)
223
let pp_mod pp_value v1 v2 fmt =
224
  if !Options.integer_div_euclidean then
225
    (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
226
    Format.fprintf fmt
227
      "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
228
      pp_value v1 pp_value v2
229
      pp_value v1 pp_value v2
230
      pp_value v2
231
  else (* Ada behavior for rem *)
232
    Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
233

    
234
(** Printing function for expressions [v1 div v2]. Depends on
235
    option [integer_div_euclidean] to choose between mathematic
236
    division or Ada division.
237

    
238
    @param pp_value pretty printer for values
239
    @param v1 the first value in the expression
240
    @param v2 the second value in the expression
241
    @param fmt the formater to print in
242
 **)
243
let pp_div pp_value v1 v2 fmt =
244
  if !Options.integer_div_euclidean then
245
    (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
246
    Format.fprintf fmt "(%a - %t) / %a"
247
      pp_value v1
248
      (pp_mod pp_value v1 v2)
249
      pp_value v2
250
  else (* Ada behavior for / *)
251
    Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
252

    
253
(** Printing function for basic lib functions.
254

    
255
    @param pp_value pretty printer for values
256
    @param i a string representing the function
257
    @param fmt the formater to print on
258
    @param vl the list of operands
259
 **)
260
let pp_basic_lib_fun pp_value ident fmt vl =
261
  match ident, vl with
262
  | "uminus", [v]    ->
263
    Format.fprintf fmt "(- %a)" pp_value v
264
  | "not", [v]       ->
265
    Format.fprintf fmt "(not %a)" pp_value v
266
  | "impl", [v1; v2] ->
267
    Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
268
  | "=", [v1; v2]    ->
269
    Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
270
  | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt
271
  | "equi", [v1; v2] ->
272
    Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
273
  | "xor", [v1; v2]  ->
274
    Format.fprintf fmt "((not %a) /= (not %a))" pp_value v1 pp_value v2
275
  | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt
276
  | "&&", [v1; v2]    ->
277
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "and then" pp_value v2
278
  | "||", [v1; v2]    ->
279
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "or else" pp_value v2
280
  | "!=", [v1; v2]    ->
281
    Format.fprintf fmt "(%a %s %a)" pp_value v1 "/=" pp_value v2
282
  | "ite", [v1; v2; v3]    ->
283
    Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3
284
  | op, [v1; v2]     ->
285
    Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
286
  | op, [v1] when  List.mem_assoc ident ada_supported_funs ->
287
    let pkg, name = try List.assoc ident ada_supported_funs
288
      with Not_found -> assert false in
289
    let pkg = pkg^(if String.equal pkg "" then "" else ".") in
290
      Format.fprintf fmt "%s%s(%a)" pkg name pp_value v1
291
  | fun_name, _      ->
292
    (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
293

    
294
(** Printing function for values.
295

    
296
    @param m the machine to know the state variable
297
    @param fmt the formater to use
298
    @param value the value to print. Should be a
299
           {!type:Machine_code_types.value_t} value
300
 **)
301
let rec pp_value env fmt value =
302
  match value.value_desc with
303
  | Cst c             -> pp_ada_const fmt c
304
  | Var var      -> pp_var env fmt var (* Find better to test if it is memory or not *)
305
  | Fun (f_ident, vl) -> pp_basic_lib_fun (pp_value env) f_ident fmt vl
306
  | _                 ->
307
    raise (Ada_not_supported
308
             "unsupported: Ada_backend.adb.pp_value does not support this value type")
309

    
310

    
311
(** Print the filename of a machine package.
312
   @param extension the extension to append to the package name
313
   @param fmt the formatter
314
   @param machine the machine corresponding to the package
315
**)
316
let pp_machine_filename extension fmt machine =
317
  pp_filename extension fmt (pp_package_name machine)
318

    
319
let pp_main_filename fmt _ = pp_filename "adb" fmt pp_main_procedure_name
320

    
321

    
322
(** Print the declaration of a state element of a subinstance of a machine.
323
   @param machine the machine
324
   @param fmt the formater to print on
325
   @param substitution correspondance between polymorphic type id and their instantiation
326
   @param ident the identifier of the subinstance
327
   @param submachine the submachine of the subinstance
328
**)
329
let build_pp_state_decl_from_subinstance mode with_statement (name, (substitution, machine)) =
330
  let pp_package = pp_package_name_with_polymorphic substitution machine in
331
  let pp_type = pp_package_access (pp_package, pp_state_type) in
332
  let pp_name fmt = pp_clean_ada_identifier fmt name in
333
  (mode, pp_name, pp_type, with_statement)
334

    
335
(** Print variable declaration for a local state variable
336
   @param fmt the formater to print on
337
   @param mode input/output mode of the parameter
338
**)
339
let build_pp_state_decl mode with_statement =
340
  (mode, pp_state_name, pp_state_type, with_statement)
341

    
342
let build_pp_var_decl mode with_statement var =
343
  let pp_name = function fmt -> pp_var_name var fmt in
344
  let pp_type = function fmt -> pp_var_type fmt var in
345
  (mode, pp_name, pp_type, with_statement)
346

    
347
let build_pp_var_decl_local with_statement var =
348
  AdaLocalVar (build_pp_var_decl AdaNoMode with_statement var)
349

    
350
let build_pp_var_decl_step_input mode with_statement m =
351
  if m.mstep.step_inputs=[] then [] else
352
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_inputs]
353

    
354
let build_pp_var_decl_step_output mode with_statement m =
355
  if m.mstep.step_outputs=[] then [] else
356
    [List.map (build_pp_var_decl mode with_statement) m.mstep.step_outputs]
357

    
358
let build_pp_var_decl_static mode with_statement m =
359
  if m.mstatic=[] then [] else
360
    [List.map (build_pp_var_decl mode with_statement) m.mstatic]
361

    
362
let build_pp_arg_step m =
363
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
364
    @ (build_pp_var_decl_step_input AdaIn None m)
365
    @ (build_pp_var_decl_step_output AdaOut None m)
366

    
367
let build_pp_arg_reset m =
368
  (if is_machine_statefull m then [[build_pp_state_decl AdaOut None]] else [])
369
    @ (build_pp_var_decl_static AdaIn None m)
370

    
371

    
372
let build_pp_arg_transition m =
373
  (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
374
    @ (build_pp_var_decl_step_input AdaIn None m)
375
    @ (build_pp_var_decl_step_output AdaOut None m)
376