Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_backend_adb.ml @ fd8aeeac

History | View | Annotate | Download (9.9 KB)

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 768f60f0 Christophe Garion
  (* Printing functions for basic operations *)
26
27
  (** Printing function for expressions [v1 modulo v2]. Depends
28
      on option [integer_div_euclidean] to choose between mathematical
29
      modulo or remainder ([rem] in Ada).
30
31
      @param pp_val pretty printer for values
32
      @param v1 the first value in the expression
33
      @param v2 the second value in the expression
34
      @param fmt the formater to print on
35
   **)
36
  let pp_mod pp_val v1 v2 fmt =
37
    if !Options.integer_div_euclidean then
38
      (* (a rem b) + (a rem b < 0 ? abs(b) : 0) *)
39
      Format.fprintf fmt
40
        "((%a rem %a) + (if (%a rem %a) < 0 then abs(%a) else 0))"
41
        pp_val v1 pp_val v2
42
        pp_val v1 pp_val v2
43
        pp_val v2
44
    else (* Ada behavior for rem *)
45
      Format.fprintf fmt "(%a rem %a)" pp_val v1 pp_val v2
46
47
  (** Printing function for expressions [v1 div v2]. Depends on
48
      option [integer_div_euclidean] to choose between mathematic
49
      division or Ada division.
50
51
      @param pp_val pretty printer for values
52
      @param v1 the first value in the expression
53
      @param v2 the second value in the expression
54
      @param fmt the formater to print in
55
   **)
56
  let pp_div pp_val v1 v2 fmt =
57
    if !Options.integer_div_euclidean then
58
      (* (a - ((a rem b) + (if a rem b < 0 then abs (b) else 0))) / b) *)
59
      Format.fprintf fmt "(%a - %t) / %a"
60
        pp_val v1
61
        (pp_mod pp_val v1 v2)
62
        pp_val v2
63
    else (* Ada behovior for / *)
64
      Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
65
66
  (** Printing function for basic lib functions.
67
68
      @param is_int boolean to choose between integer
69
                    division (resp. remainder) or Ada division
70
                    (resp. remainder)
71
      @param i a string representing the function
72
      @param pp_val the pretty printer for values
73
      @param fmt the formater to print on
74
      @param vl the list of operands
75
   **)
76
  let pp_basic_lib_fun is_int i pp_val fmt vl =
77
    match i, vl with
78
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
79
    | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
80
    | "impl", [v1; v2] -> Format.fprintf fmt "(not %a or else %a)" pp_val v1 pp_val v2
81
    | "=", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
82
    | "mod", [v1; v2] ->
83
      if is_int then
84
        pp_mod pp_val v1 v2 fmt
85
      else
86
        Format.fprintf fmt "(%a rem %a)" pp_val v1 pp_val v2
87
    | "equi", [v1; v2] -> Format.fprintf fmt "((not %a) = (not %a))" pp_val v1 pp_val v2
88
    | "xor", [v1; v2] -> Format.fprintf fmt "((not %a) \\= (not %a))" pp_val v1 pp_val v2
89
    | "/", [v1; v2] ->
90
      if is_int then
91
        pp_div pp_val v1 v2 fmt
92
      else
93
        Format.fprintf fmt "(%a / %a)" pp_val v1 pp_val v2
94
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
95
    | _ -> (Format.eprintf "internal compilation error: basic function %s@." i; assert false)
96
97
  (** Printing function for basic assignement [var_name := value;].
98
99
      @param pp_var pretty printer for variables
100
      @param fmt the formater to print on
101
      @param var_name the name of the variable
102
      @param value the value to be assigned
103
   **)
104 fd8aeeac Christophe Garion
  (* TODO remove pp_var *)
105 768f60f0 Christophe Garion
  let pp_basic_assign pp_var fmt var_name value =
106
    fprintf fmt "%a := %a;"
107
      pp_var var_name
108
      pp_var value
109
110
  (** Printing function for assignement. For the moment, only use
111
      [pp_basic_assign] function.
112
113
      @param pp_var pretty printer for variables
114
      @param fmt the formater to print on
115
      @param var_name the name of the variable
116
      @param value the value to be assigned
117
   **)
118
  let pp_assign pp_var fmt var_name value = pp_basic_assign
119
120 fd8aeeac Christophe Garion
  (* Printing function for reset function *)
121
  (* TODO: clean the call to extract_node *)
122
  (** Printing function for reset function name.
123
124
      @param fmt the formater to use
125
      @param encapsulated_node the node encapsulated in a pair
126
             [(instance, (node, static))]
127
   **)
128
  let pp_machine_reset_name fmt encapsulated_node =
129
    fprintf fmt "%a.reset" pp_package_name (extract_node encapsulated_node)
130
131
  (** Printing function for reset function.
132
133
      @param machine the considered machine
134
      @param fmt the formater to use
135
      @param instance the considered instance
136
   **)
137
  let pp_machine_reset (machine: machine_t) fmt instance =
138
    let (node, static) =
139
      try
140
        List.assoc instance machine.minstances
141
      with Not_found -> (Format.eprintf "internal error: pp_machine_reset %s %s:@." machine.mname.node_id instance; raise Not_found) in
142
    fprintf fmt "%a(state.%s);"
143
      pp_machine_reset_name (instance, (node, static))
144
      instance
145
146 768f60f0 Christophe Garion
  (** Printing function for instruction. See
147
      {!type:Machine_code_types.instr_t} for more details on
148
      machine types.
149
150
      @param machine the current machine
151
      @param fmt the formater to print on
152
      @param instr the instruction to print
153
   **)
154
  let pp_machine_instr machine fmt instr =
155
    match get_instr_desc instr with
156
    (* no reset *)
157
    | MNoReset _ -> ()
158
    (* reset  *)
159
    | MReset i ->
160 fd8aeeac Christophe Garion
      pp_machine_reset machine fmt i
161 768f60f0 Christophe Garion
    | MLocalAssign (i,v) ->
162 fd8aeeac Christophe Garion
      fprintf fmt "MLocalAssign @"
163
      (* pp_basic_assign pp_var_name fmt i v *)
164 768f60f0 Christophe Garion
      (* pp_assign
165
       *   machine self (pp_c_var_read m) fmt
166
       *   i.var_type (mk_val (Var i) i.var_type) v *)
167
    | MStateAssign (i,v) ->
168
      fprintf fmt "MStateAssign"
169
    (* pp_assign
170
       *   m self (pp_c_var_read m) fmt
171
       *   i.var_type (mk_val (Var i) i.var_type) v *)
172
    | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun
173
          (mk_val (Fun (i, vl)) i0.var_type)  ->
174
      fprintf fmt "MStep basic"
175
    (* pp_machine_instr dependencies m self fmt
176
     *   (update_instr_desc instr (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type))) *)
177
    | MStep (il, i, vl) -> fprintf fmt "MStep"
178
179
    (* pp_basic_instance_call m self fmt i vl il *)
180
    | MBranch (_, []) -> fprintf fmt "MBranch []"
181
182
    (* (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." (pp_instr m) instr; assert false) *)
183
    | MBranch (g, hl) -> fprintf fmt "MBranch gen"
184
    (* if let t = fst (List.hd hl) in t = tag_true || t = tag_false
185
     * then (\* boolean case, needs special treatment in C because truth value is not unique *\)
186
     *   (\* may disappear if we optimize code by replacing last branch test with default *\)
187
     *   let tl = try List.assoc tag_true  hl with Not_found -> [] in
188
     *   let el = try List.assoc tag_false hl with Not_found -> [] in
189
     *   pp_conditional dependencies m self fmt g tl el
190
     * else (\* enum type case *\)
191
     *   (\*let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in*\)
192
     *   fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
193
     *     (pp_c_val m self (pp_c_var_read m)) g
194
     *     (Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl *)
195
    | MComment s  ->
196
      fprintf fmt "-- %s@ " s
197
    | _ -> fprintf fmt "Don't  know"
198
199 3d85297f Guillaume DAVY
200
(** Keep only the MReset from an instruction list.
201
  @param list to filter
202
**)
203
let filter_reset instr_list = List.map
204 768f60f0 Christophe Garion
    (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false)
205 3d85297f Guillaume DAVY
  instr_list
206
207
(** Print the definition of the init procedure from a machine.
208
   @param fmt the formater to print on
209
   @param machine the machine
210
**)
211 fd834769 Guillaume DAVY
let pp_init_definition fmt m = pp_procedure_definition
212
      pp_init_procedure_name
213
      (pp_init_prototype m)
214 4ba20be4 Guillaume DAVY
      (pp_machine_var_decl NoMode)
215 fd834769 Guillaume DAVY
      (pp_machine_instr m)
216
      fmt
217
      ([], m.minit)
218 3d85297f Guillaume DAVY
219
(** Print the definition of the step procedure from a machine.
220
   @param fmt the formater to print on
221
   @param machine the machine
222
**)
223 fd834769 Guillaume DAVY
let pp_step_definition fmt m = pp_procedure_definition
224
      pp_step_procedure_name
225
      (pp_step_prototype m)
226 4ba20be4 Guillaume DAVY
      (pp_machine_var_decl NoMode)
227 fd834769 Guillaume DAVY
      (pp_machine_instr m)
228
      fmt
229 4ba20be4 Guillaume DAVY
      (m.mstep.step_locals, m.mstep.step_instrs)
230 3d85297f Guillaume DAVY
231
(** Print the definition of the reset procedure from a machine.
232
   @param fmt the formater to print on
233
   @param machine the machine
234
**)
235 fd834769 Guillaume DAVY
let pp_reset_definition fmt m = pp_procedure_definition
236
      pp_reset_procedure_name
237
      (pp_reset_prototype m)
238 4ba20be4 Guillaume DAVY
      (pp_machine_var_decl NoMode)
239 fd834769 Guillaume DAVY
      (pp_machine_instr m)
240
      fmt
241
      ([], m.minit)
242 3d85297f Guillaume DAVY
243
(** Print the definition of the clear procedure from a machine.
244
   @param fmt the formater to print on
245
   @param machine the machine
246
**)
247 fd834769 Guillaume DAVY
let pp_clear_definition fmt m = pp_procedure_definition
248
      pp_clear_procedure_name
249
      (pp_clear_prototype m)
250 4ba20be4 Guillaume DAVY
      (pp_machine_var_decl NoMode)
251 fd834769 Guillaume DAVY
      (pp_machine_instr m)
252
      fmt
253 69cd79c6 Guillaume DAVY
      ([], m.minit)
254 3d85297f Guillaume DAVY
255
(** Print the package definition(adb) of a machine.
256
   @param fmt the formater to print on
257
   @param machine the machine
258 7cbb6d8a Guillaume DAVY
**)
259 fd834769 Guillaume DAVY
let pp_file fmt machine =
260 3d85297f Guillaume DAVY
  fprintf fmt "%a@,  @[<v>@,%a;@,@,%a;@,@,%a;@,@,%a;@,@]@,%a;@."
261
    (pp_begin_package true) machine (*Begin the package*)
262
    pp_init_definition machine (*Define the init procedure*)
263
    pp_step_definition machine (*Define the step procedure*)
264
    pp_reset_definition machine (*Define the reset procedure*)
265
    pp_clear_definition machine (*Define the clear procedure*)
266
    pp_end_package machine  (*End the package*)
267 48a6309c Guillaume DAVY
268 f20d8ac7 Christophe Garion
end
269 768f60f0 Christophe Garion
270
(* Local Variables: *)
271
(* compile-command: "make -C ../../.." *)
272
(* End: *)