Project

General

Profile

Download (11.1 KB) Statistics
| Branch: | Tag: | Revision:
1 f20d8ac7 Christophe Garion
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
12 48a6309c Guillaume DAVY
open Format
13 bdc471f3 Guillaume DAVY
14 48a6309c Guillaume DAVY
open Machine_code_types
15
open Lustre_types
16
open Corelang
17
open Machine_code_common
18 bdc471f3 Guillaume DAVY
open Ada_backend_common
19
20 768f60f0 Christophe Garion
(** Main module for generating packages bodies
21
 **)
22 f20d8ac7 Christophe Garion
module Main =
23
struct
24 48a6309c Guillaume DAVY
25 c85c2e3d Christophe Garion
  (* Printing functions for basic operations and expressions *)
26
  (* TODO: refactor code -> use let rec and for basic pretty printing
27
     function *)
28
  (** Printing function for Ada tags, mainly booleans.
29
30
      @param fmt the formater to use
31
      @param t the tag to print
32
   **)
33
  let pp_ada_tag fmt t =
34
    pp_print_string fmt
35
      (if t = tag_true then "True" else if t = tag_false then "Flase" else t)
36
37
  (** Printing function for machine type constants. For the moment,
38
      arrays are not supported.
39
40
      @param fmt the formater to use
41
      @param c the constant to print
42
   **)
43
  let pp_ada_const fmt c =
44
    match c with
45
    | Const_int i                     -> pp_print_int fmt i
46
    | Const_real (c, e, s)            -> pp_print_string fmt s
47
    | Const_tag t                     -> pp_ada_tag fmt t
48
    | Const_string _ | Const_modeid _ ->
49
      (Format.eprintf
50
         "internal error: Ada_backend_adb.pp_ada_const cannot print string or modeid.";
51
       assert false)
52
    | _                               ->
53
      raise (Ada_not_supported "unsupported: Ada_backend_adb.pp_ada_const does not
54
      support this constant")
55 768f60f0 Christophe Garion
56
  (** Printing function for expressions [v1 modulo v2]. Depends
57
      on option [integer_div_euclidean] to choose between mathematical
58
      modulo or remainder ([rem] in Ada).
59
60 c85c2e3d Christophe Garion
      @param pp_value pretty printer for values
61 768f60f0 Christophe Garion
      @param v1 the first value in the expression
62
      @param v2 the second value in the expression
63
      @param fmt the formater to print on
64
   **)
65 c85c2e3d Christophe Garion
  let pp_mod pp_value v1 v2 fmt =
66 768f60f0 Christophe Garion
    if !Options.integer_div_euclidean then
67
      (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
68
      Format.fprintf fmt
69
        "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
70 c85c2e3d Christophe Garion
        pp_value v1 pp_value v2
71
        pp_value v1 pp_value v2
72
        pp_value v2
73 768f60f0 Christophe Garion
    else (* Ada behavior for rem *)
74 c85c2e3d Christophe Garion
      Format.fprintf fmt "(%a rem %a)" pp_value v1 pp_value v2
75 768f60f0 Christophe Garion
76
  (** Printing function for expressions [v1 div v2]. Depends on
77
      option [integer_div_euclidean] to choose between mathematic
78
      division or Ada division.
79
80 c85c2e3d Christophe Garion
      @param pp_value pretty printer for values
81 768f60f0 Christophe Garion
      @param v1 the first value in the expression
82
      @param v2 the second value in the expression
83
      @param fmt the formater to print in
84
   **)
85 c85c2e3d Christophe Garion
  let pp_div pp_value v1 v2 fmt =
86 768f60f0 Christophe Garion
    if !Options.integer_div_euclidean then
87
      (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
88
      Format.fprintf fmt "(%a - %t) / %a"
89 c85c2e3d Christophe Garion
        pp_value v1
90
        (pp_mod pp_value v1 v2)
91
        pp_value v2
92
    else (* Ada behavior for / *)
93
      Format.fprintf fmt "(%a / %a)" pp_value v1 pp_value v2
94 768f60f0 Christophe Garion
95
  (** Printing function for basic lib functions.
96
97 c85c2e3d Christophe Garion
      @param pp_value pretty printer for values
98 768f60f0 Christophe Garion
      @param i a string representing the function
99
      @param fmt the formater to print on
100
      @param vl the list of operands
101
   **)
102 c85c2e3d Christophe Garion
  let pp_basic_lib_fun pp_value ident fmt vl =
103
    match ident, vl with
104
    | "uminus", [v]    ->
105
      Format.fprintf fmt "(- %a)" pp_value v
106
    | "not", [v]       ->
107
      Format.fprintf fmt "(not %a)" pp_value v
108
    | "impl", [v1; v2] ->
109
      Format.fprintf fmt "(not %a or else %a)" pp_value v1 pp_value v2
110
    | "=", [v1; v2]    ->
111
      Format.fprintf fmt "(%a = %a)" pp_value v1 pp_value v2
112
    | "mod", [v1; v2]  -> pp_mod pp_value v1 v2 fmt
113
    | "equi", [v1; v2] ->
114
      Format.fprintf fmt "((not %a) = (not %a))" pp_value v1 pp_value v2
115
    | "xor", [v1; v2]  ->
116
      Format.fprintf fmt "((not %a) \\= (not %a))" pp_value v1 pp_value v2
117
    | "/", [v1; v2]    -> pp_div pp_value v1 v2 fmt
118
    | op, [v1; v2]     ->
119
      Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
120
    | fun_name, _      ->
121
      (Format.eprintf "internal compilation error: basic function %s@." fun_name; assert false)
122
123
  (** Printing function for values.
124
125
      @param fmt the formater to use
126
      @param value the value to print. Should be a
127
             {!type:Machine_code_types.value_t} value
128
   **)
129
  let rec pp_value fmt value =
130
    match value.value_desc with
131
    | Cst c             -> pp_ada_const fmt c
132
    | Var var_name      -> pp_var_name fmt var_name
133
    | Fun (f_ident, vl) -> pp_basic_lib_fun pp_value f_ident fmt vl
134
    | _                 ->
135
      raise (Ada_not_supported
136
               "unsupported: Ada_backend.adb.pp_value does not support this value type")
137 768f60f0 Christophe Garion
138
  (** Printing function for basic assignement [var_name := value;].
139
140
      @param fmt the formater to print on
141
      @param var_name the name of the variable
142
      @param value the value to be assigned
143
   **)
144 c85c2e3d Christophe Garion
  let pp_basic_assign fmt var_name value =
145
    fprintf fmt "%a := %a"
146
      pp_var_name var_name
147
      pp_value value
148 768f60f0 Christophe Garion
149
  (** Printing function for assignement. For the moment, only use
150
      [pp_basic_assign] function.
151
152
      @param pp_var pretty printer for variables
153
      @param fmt the formater to print on
154
      @param var_name the name of the variable
155
      @param value the value to be assigned
156
   **)
157
  let pp_assign pp_var fmt var_name value = pp_basic_assign
158
159 fd8aeeac Christophe Garion
  (* Printing function for reset function *)
160
  (* TODO: clean the call to extract_node *)
161
  (** Printing function for reset function name.
162
163
      @param fmt the formater to use
164
      @param encapsulated_node the node encapsulated in a pair
165
             [(instance, (node, static))]
166
   **)
167
  let pp_machine_reset_name fmt encapsulated_node =
168
    fprintf fmt "%a.reset" pp_package_name (extract_node encapsulated_node)
169
170
  (** Printing function for reset function.
171
172
      @param machine the considered machine
173
      @param fmt the formater to use
174
      @param instance the considered instance
175
   **)
176
  let pp_machine_reset (machine: machine_t) fmt instance =
177
    let (node, static) =
178
      try
179
        List.assoc instance machine.minstances
180
      with Not_found -> (Format.eprintf "internal error: pp_machine_reset %s %s:@." machine.mname.node_id instance; raise Not_found) in
181 c85c2e3d Christophe Garion
    fprintf fmt "%a(state.%s)"
182 fd8aeeac Christophe Garion
      pp_machine_reset_name (instance, (node, static))
183
      instance
184
185 768f60f0 Christophe Garion
  (** Printing function for instruction. See
186
      {!type:Machine_code_types.instr_t} for more details on
187
      machine types.
188
189
      @param machine the current machine
190
      @param fmt the formater to print on
191
      @param instr the instruction to print
192
   **)
193
  let pp_machine_instr machine fmt instr =
194
    match get_instr_desc instr with
195
    (* no reset *)
196
    | MNoReset _ -> ()
197
    (* reset  *)
198 c85c2e3d Christophe Garion
    | MReset ident ->
199
      pp_machine_reset machine fmt ident
200
    | MLocalAssign (ident, value) ->
201
      pp_basic_assign fmt ident value
202 768f60f0 Christophe Garion
    | MStateAssign (i,v) ->
203
      fprintf fmt "MStateAssign"
204
    (* pp_assign
205
       *   m self (pp_c_var_read m) fmt
206
       *   i.var_type (mk_val (Var i) i.var_type) v *)
207
    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun
208
          (mk_val (Fun (i, vl)) i0.var_type)  ->
209
      fprintf fmt "MStep basic"
210
    (* pp_machine_instr dependencies m self fmt
211
     *   (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type))) *)
212
    | MStep (il, i, vl) -> fprintf fmt "MStep"
213
214
    (* pp_basic_instance_call m self fmt i vl il *)
215
    | MBranch (_, []) -> fprintf fmt "MBranch []"
216
217
    (* (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false) *)
218
    | MBranch (g, hl) -> fprintf fmt "MBranch gen"
219
    (* if let t = fst (List.hd hl) in t = tag_true || t = tag_false
220
     * then (\* boolean case, needs special treatment in C because truth value is not unique *\)
221
     *   (\* may disappear if we optimize code by replacing last branch test with default *\)
222
     *   let tl = try List.assoc tag_true  hl with Not_found -> [] in
223
     *   let el = try List.assoc tag_false hl with Not_found -> [] in
224
     *   pp_conditional dependencies m self fmt g tl el
225
     * else (\* enum type case *\)
226
     *   (\*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*\)
227
     *   fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
228
     *     (pp_c_val m self (pp_c_var_read m)) g
229
     *     (Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl *)
230
    | MComment s  ->
231
      fprintf fmt "-- %s@ " s
232
    | _ -> fprintf fmt "Don't  know"
233
234 3d85297f Guillaume DAVY
235
(** Keep only the MReset from an instruction list.
236
  @param list to filter
237
**)
238
let filter_reset instr_list = List.map
239 768f60f0 Christophe Garion
    (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false)
240 3d85297f Guillaume DAVY
  instr_list
241
242
(** Print the definition of the init procedure from a machine.
243
   @param fmt the formater to print on
244
   @param machine the machine
245
**)
246 fd834769 Guillaume DAVY
let pp_init_definition fmt m = pp_procedure_definition
247
      pp_init_procedure_name
248
      (pp_init_prototype m)
249 4ba20be4 Guillaume DAVY
      (pp_machine_var_decl NoMode)
250 fd834769 Guillaume DAVY
      (pp_machine_instr m)
251
      fmt
252
      ([], m.minit)
253 3d85297f Guillaume DAVY
254
(** Print the definition of the step procedure from a machine.
255
   @param fmt the formater to print on
256
   @param machine the machine
257
**)
258 fd834769 Guillaume DAVY
let pp_step_definition fmt m = pp_procedure_definition
259
      pp_step_procedure_name
260
      (pp_step_prototype m)
261 4ba20be4 Guillaume DAVY
      (pp_machine_var_decl NoMode)
262 fd834769 Guillaume DAVY
      (pp_machine_instr m)
263
      fmt
264 4ba20be4 Guillaume DAVY
      (m.mstep.step_locals, m.mstep.step_instrs)
265 3d85297f Guillaume DAVY
266
(** Print the definition of the reset procedure from a machine.
267
   @param fmt the formater to print on
268
   @param machine the machine
269
**)
270 fd834769 Guillaume DAVY
let pp_reset_definition fmt m = pp_procedure_definition
271
      pp_reset_procedure_name
272
      (pp_reset_prototype m)
273 4ba20be4 Guillaume DAVY
      (pp_machine_var_decl NoMode)
274 fd834769 Guillaume DAVY
      (pp_machine_instr m)
275
      fmt
276
      ([], m.minit)
277 3d85297f Guillaume DAVY
278
(** Print the definition of the clear procedure from a machine.
279
   @param fmt the formater to print on
280
   @param machine the machine
281
**)
282 fd834769 Guillaume DAVY
let pp_clear_definition fmt m = pp_procedure_definition
283
      pp_clear_procedure_name
284
      (pp_clear_prototype m)
285 4ba20be4 Guillaume DAVY
      (pp_machine_var_decl NoMode)
286 fd834769 Guillaume DAVY
      (pp_machine_instr m)
287
      fmt
288 69cd79c6 Guillaume DAVY
      ([], m.minit)
289 3d85297f Guillaume DAVY
290
(** Print the package definition(adb) of a machine.
291
   @param fmt the formater to print on
292
   @param machine the machine
293 7cbb6d8a Guillaume DAVY
**)
294 fd834769 Guillaume DAVY
let pp_file fmt machine =
295 3d85297f Guillaume DAVY
  fprintf fmt "%a@,  @[<v>@,%a;@,@,%a;@,@,%a;@,@,%a;@,@]@,%a;@."
296
    (pp_begin_package true) machine (*Begin the package*)
297
    pp_init_definition machine (*Define the init procedure*)
298
    pp_step_definition machine (*Define the step procedure*)
299
    pp_reset_definition machine (*Define the reset procedure*)
300
    pp_clear_definition machine (*Define the clear procedure*)
301
    pp_end_package machine  (*End the package*)
302 48a6309c Guillaume DAVY
303 f20d8ac7 Christophe Garion
end
304 768f60f0 Christophe Garion
305
(* Local Variables: *)
306
(* compile-command: "make -C ../../.." *)
307
(* End: *)