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: *)
|