Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/features/machine_types/machine_types.ml | ||
---|---|---|
3 | 3 |
In each node, node local annotations can specify the actual type of the |
4 | 4 |
implementation uintXX, intXX, floatXX ... |
5 | 5 |
|
6 |
The module provide utility functions to query the model: |
|
7 |
- get_var_machine_type varid nodeid returns the string denoting the actual type |
|
8 |
|
|
9 |
The actual type is used at different stages of the coompilation |
|
10 |
- early stage: limited typing, ie validity of operation are checked |
|
11 |
- a first version ensures that the actual type is a subtype of the declared/infered ones |
|
12 |
eg uint8 is a valid subtype of int |
|
13 |
- a future implementation could ensures that operations are valid |
|
14 |
- each standard or unspecified operation should be homogeneous : |
|
15 |
op: real -> real -> real is valid for any same subtype t of real: op: t -> t -> t |
|
16 |
- specific nodes that explicitely defined subtypes could be used to perform casts |
|
17 |
eg. a int2uint8 (i: int) returns (j: int) with annotations specifying i as int and j as uint8 |
|
18 |
- C backend: any print of a typed variable should rely on the actual machine type when provided |
|
19 |
- EMF backend: idem |
|
20 |
- Horn backend: an option could enforce the bounds provided by the machine |
|
21 |
type or implement the cycling behavior for integer subtypes |
|
22 |
- Salsa plugin: the information should be propagated to the plugin. |
|
23 |
One can also imagine that results of the analysis could specify or |
|
24 |
substitute a type by a subtype. Eg. the analysis detects that a float32 is enough for variable z and |
|
25 |
the annotation is added to the node. |
|
26 |
|
|
27 |
|
|
28 |
A posisble behavior could be |
|
29 |
- an option to ensure type checking |
|
30 |
- dedicated conversion functions that, in C, would generate cast or calls to simple identity functions (to be inlined) |
|
31 |
|
|
32 |
|
|
33 |
|
|
34 |
TODO |
|
35 |
EMF: rajouter les memoires dans les caracteristiques du node |
|
36 |
gerer les types plus finement: |
|
37 |
propager les types machines aux variables fraiches creees par la normalisation |
|
38 |
|
|
39 |
*) |
|
6 |
The module provide utility functions to query the model: - |
|
7 |
get_var_machine_type varid nodeid returns the string denoting the actual type |
|
8 |
|
|
9 |
The actual type is used at different stages of the coompilation - early |
|
10 |
stage: limited typing, ie validity of operation are checked - a first version |
|
11 |
ensures that the actual type is a subtype of the declared/infered ones eg |
|
12 |
uint8 is a valid subtype of int - a future implementation could ensures that |
|
13 |
operations are valid - each standard or unspecified operation should be |
|
14 |
homogeneous : op: real -> real -> real is valid for any same subtype t of |
|
15 |
real: op: t -> t -> t - specific nodes that explicitely defined subtypes |
|
16 |
could be used to perform casts eg. a int2uint8 (i: int) returns (j: int) with |
|
17 |
annotations specifying i as int and j as uint8 - C backend: any print of a |
|
18 |
typed variable should rely on the actual machine type when provided - EMF |
|
19 |
backend: idem - Horn backend: an option could enforce the bounds provided by |
|
20 |
the machine type or implement the cycling behavior for integer subtypes - |
|
21 |
Salsa plugin: the information should be propagated to the plugin. One can |
|
22 |
also imagine that results of the analysis could specify or substitute a type |
|
23 |
by a subtype. Eg. the analysis detects that a float32 is enough for variable |
|
24 |
z and the annotation is added to the node. |
|
25 |
|
|
26 |
A posisble behavior could be - an option to ensure type checking - dedicated |
|
27 |
conversion functions that, in C, would generate cast or calls to simple |
|
28 |
identity functions (to be inlined) |
|
29 |
|
|
30 |
TODO EMF: rajouter les memoires dans les caracteristiques du node gerer les |
|
31 |
types plus finement: propager les types machines aux variables fraiches |
|
32 |
creees par la normalisation *) |
|
40 | 33 |
open Lustre_types |
41 | 34 |
|
42 | 35 |
let is_active = false |
43 |
|
|
44 |
let keyword = ["machine_types"] |
|
45 | 36 |
|
46 |
module MT = |
|
47 |
struct |
|
37 |
let keyword = [ "machine_types" ] |
|
48 | 38 |
|
39 |
module MT = struct |
|
49 | 40 |
type int_typ = |
50 | 41 |
| Tint8_t |
51 | 42 |
| Tint16_t |
... | ... | |
58 | 49 |
|
59 | 50 |
let pp_int fmt t = |
60 | 51 |
match t with |
61 |
| Tint8_t -> Format.fprintf fmt "int8" |
|
62 |
| Tint16_t -> Format.fprintf fmt "int16" |
|
63 |
| Tint32_t -> Format.fprintf fmt "int32" |
|
64 |
| Tint64_t -> Format.fprintf fmt "int64" |
|
65 |
| Tuint8_t -> Format.fprintf fmt "uint8" |
|
66 |
| Tuint16_t -> Format.fprintf fmt "uint16" |
|
67 |
| Tuint32_t -> Format.fprintf fmt "uint32" |
|
68 |
| Tuint64_t -> Format.fprintf fmt "uint64" |
|
52 |
| Tint8_t -> |
|
53 |
Format.fprintf fmt "int8" |
|
54 |
| Tint16_t -> |
|
55 |
Format.fprintf fmt "int16" |
|
56 |
| Tint32_t -> |
|
57 |
Format.fprintf fmt "int32" |
|
58 |
| Tint64_t -> |
|
59 |
Format.fprintf fmt "int64" |
|
60 |
| Tuint8_t -> |
|
61 |
Format.fprintf fmt "uint8" |
|
62 |
| Tuint16_t -> |
|
63 |
Format.fprintf fmt "uint16" |
|
64 |
| Tuint32_t -> |
|
65 |
Format.fprintf fmt "uint32" |
|
66 |
| Tuint64_t -> |
|
67 |
Format.fprintf fmt "uint64" |
|
69 | 68 |
|
70 | 69 |
let pp_c_int fmt t = |
71 | 70 |
match t with |
72 |
| Tint8_t -> Format.fprintf fmt "int8_t" |
|
73 |
| Tint16_t -> Format.fprintf fmt "int16_t" |
|
74 |
| Tint32_t -> Format.fprintf fmt "int32_t" |
|
75 |
| Tint64_t -> Format.fprintf fmt "int64_t" |
|
76 |
| Tuint8_t -> Format.fprintf fmt "uint8_t" |
|
77 |
| Tuint16_t -> Format.fprintf fmt "uint16_t" |
|
78 |
| Tuint32_t -> Format.fprintf fmt "uint32_t" |
|
79 |
| Tuint64_t -> Format.fprintf fmt "uint64_t" |
|
71 |
| Tint8_t -> |
|
72 |
Format.fprintf fmt "int8_t" |
|
73 |
| Tint16_t -> |
|
74 |
Format.fprintf fmt "int16_t" |
|
75 |
| Tint32_t -> |
|
76 |
Format.fprintf fmt "int32_t" |
|
77 |
| Tint64_t -> |
|
78 |
Format.fprintf fmt "int64_t" |
|
79 |
| Tuint8_t -> |
|
80 |
Format.fprintf fmt "uint8_t" |
|
81 |
| Tuint16_t -> |
|
82 |
Format.fprintf fmt "uint16_t" |
|
83 |
| Tuint32_t -> |
|
84 |
Format.fprintf fmt "uint32_t" |
|
85 |
| Tuint64_t -> |
|
86 |
Format.fprintf fmt "uint64_t" |
|
80 | 87 |
|
81 | 88 |
type t = |
82 | 89 |
| MTint of int_typ option |
... | ... | |
85 | 92 |
| MTstring |
86 | 93 |
|
87 | 94 |
open Format |
95 |
|
|
88 | 96 |
let pp fmt t = |
89 | 97 |
match t with |
90 | 98 |
| MTint None -> |
91 |
fprintf fmt "int"
|
|
99 |
fprintf fmt "int" |
|
92 | 100 |
| MTint (Some s) -> |
93 |
fprintf fmt "%a" pp_int s
|
|
101 |
fprintf fmt "%a" pp_int s |
|
94 | 102 |
| MTreal None -> |
95 |
fprintf fmt "real"
|
|
103 |
fprintf fmt "real" |
|
96 | 104 |
| MTreal (Some s) -> |
97 |
fprintf fmt "%s" s
|
|
105 |
fprintf fmt "%s" s |
|
98 | 106 |
| MTbool -> |
99 |
fprintf fmt "bool"
|
|
107 |
fprintf fmt "bool" |
|
100 | 108 |
| MTstring -> |
101 |
fprintf fmt "string"
|
|
109 |
fprintf fmt "string" |
|
102 | 110 |
|
103 | 111 |
let pp_c fmt t = |
104 | 112 |
match t with |
105 | 113 |
| MTint (Some s) -> |
106 |
fprintf fmt "%a" pp_c_int s
|
|
114 |
fprintf fmt "%a" pp_c_int s |
|
107 | 115 |
| MTreal (Some s) -> |
108 |
fprintf fmt "%s" s |
|
109 |
| MTint None |
|
110 |
| MTreal None |
|
111 |
| MTbool |
|
112 |
| MTstring -> assert false |
|
113 |
|
|
114 |
|
|
115 |
let is_scalar_type t = |
|
116 |
match t with |
|
117 |
| MTbool |
|
118 |
| MTint _ |
|
119 |
| MTreal _ -> true |
|
120 |
| _ -> false |
|
116 |
fprintf fmt "%s" s |
|
117 |
| MTint None | MTreal None | MTbool | MTstring -> |
|
118 |
assert false |
|
121 | 119 |
|
120 |
let is_scalar_type t = |
|
121 |
match t with MTbool | MTint _ | MTreal _ -> true | _ -> false |
|
122 | 122 |
|
123 |
let is_numeric_type t = |
|
124 |
match t with |
|
125 |
| MTint _ |
|
126 |
| MTreal _ -> true |
|
127 |
| _ -> false |
|
123 |
let is_numeric_type t = match t with MTint _ | MTreal _ -> true | _ -> false |
|
128 | 124 |
|
129 | 125 |
let is_int_type t = match t with MTint _ -> true | _ -> false |
126 |
|
|
130 | 127 |
let is_real_type t = match t with MTreal _ -> true | _ -> false |
128 |
|
|
131 | 129 |
let is_bool_type t = t = MTbool |
132 |
|
|
133 |
let is_dimension_type t = |
|
134 |
match t with |
|
135 |
| MTint _ |
|
136 |
| MTbool -> true |
|
137 |
| _ -> false |
|
130 |
|
|
131 |
let is_dimension_type t = match t with MTint _ | MTbool -> true | _ -> false |
|
138 | 132 |
|
139 | 133 |
let type_int_builder = MTint None |
134 |
|
|
140 | 135 |
let type_real_builder = MTreal None |
136 |
|
|
141 | 137 |
let type_bool_builder = MTbool |
138 |
|
|
142 | 139 |
let type_string_builder = MTstring |
143 | 140 |
|
144 | 141 |
let unify _ _ = () |
142 |
|
|
145 | 143 |
let is_unifiable b1 b2 = |
146 | 144 |
match b1, b2 with |
147 |
| MTint _ , MTint _
|
|
145 |
| MTint _, MTint _ |
|
148 | 146 |
| MTreal _, MTreal _ |
149 | 147 |
| MTstring, MTstring |
150 |
| MTbool, MTbool -> true |
|
151 |
| _ -> false |
|
148 |
| MTbool, MTbool -> |
|
149 |
true |
|
150 |
| _ -> |
|
151 |
false |
|
152 | 152 |
|
153 | 153 |
let is_exportable b = |
154 | 154 |
match b with |
155 |
| MTstring |
|
156 |
| MTbool |
|
157 |
| MTreal None |
|
158 |
| MTint None -> false |
|
159 |
| _ -> true |
|
155 |
| MTstring | MTbool | MTreal None | MTint None -> |
|
156 |
false |
|
157 |
| _ -> |
|
158 |
true |
|
160 | 159 |
end |
161 | 160 |
|
162 | 161 |
module MTypes = Types.Make (MT) |
163 | 162 |
|
164 | 163 |
let type_uint8 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint8_t))) |
164 |
|
|
165 | 165 |
let type_uint16 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint16_t))) |
166 |
|
|
166 | 167 |
let type_uint32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint32_t))) |
168 |
|
|
167 | 169 |
let type_uint64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint64_t))) |
170 |
|
|
168 | 171 |
let type_int8 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint8_t))) |
172 |
|
|
169 | 173 |
let type_int16 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint16_t))) |
174 |
|
|
170 | 175 |
let type_int32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint32_t))) |
176 |
|
|
171 | 177 |
let type_int64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint64_t))) |
172 | 178 |
|
173 |
|
|
174 |
module ConvTypes = |
|
175 |
struct |
|
176 |
type type_expr = MTypes.type_expr |
|
177 |
|
|
178 |
let map_type_basic f_basic = |
|
179 |
let rec map_type_basic e = |
|
180 |
{ MTypes.tid = e.Types.tid; |
|
181 |
MTypes.tdesc = map_type_basic_desc (Types.type_desc e) |
|
182 |
} |
|
183 |
and map_type_basic_desc td = |
|
184 |
let mape = map_type_basic in |
|
185 |
match td with |
|
186 |
| Types.Tbasic b -> f_basic b |
|
187 |
| Types.Tconst c -> MTypes.Tconst c |
|
188 |
| Types.Tenum e -> MTypes.Tenum e |
|
189 |
| Types.Tvar -> MTypes.Tvar |
|
190 |
| Types.Tunivar -> MTypes.Tunivar |
|
191 |
|
|
192 |
| Types.Tclock te -> MTypes.Tclock (mape te) |
|
193 |
| Types.Tarrow (te1, te2) -> MTypes.Tarrow (mape te1, mape te2) |
|
194 |
| Types.Ttuple tel -> MTypes.Ttuple (List.map mape tel) |
|
195 |
| Types.Tstruct id_te_l -> MTypes.Tstruct (List.map (fun (id, te) -> id, mape te) id_te_l) |
|
196 |
| Types.Tarray (de, te) -> MTypes.Tarray (de, mape te) |
|
197 |
| Types.Tstatic (de, te) -> MTypes.Tstatic (de, mape te) |
|
198 |
| Types.Tlink te -> MTypes.Tlink (mape te) |
|
199 |
in |
|
200 |
map_type_basic |
|
201 |
|
|
202 |
let import main_typ = |
|
203 |
let import_basic b = |
|
204 |
if Types.BasicT.is_int_type b then MTypes.type_int else |
|
205 |
if Types.BasicT.is_real_type b then MTypes.type_real else |
|
206 |
if Types.BasicT.is_bool_type b then MTypes.type_bool else |
|
207 |
(Format.eprintf "importing %a with issues!@.@?" Types.print_ty main_typ; assert false) |
|
208 |
in |
|
209 |
map_type_basic import_basic main_typ |
|
210 |
|
|
211 |
|
|
212 |
let map_mtype_basic f_basic = |
|
213 |
let rec map_mtype_basic e = |
|
214 |
{ Types.tid = e.MTypes.tid; |
|
215 |
Types.tdesc = map_mtype_basic_desc (MTypes.type_desc e) |
|
216 |
} |
|
217 |
and map_mtype_basic_desc td = |
|
218 |
let mape = map_mtype_basic in |
|
219 |
match td with |
|
220 |
| MTypes.Tbasic b -> |
|
221 |
(* Format.eprintf "supposely basic mtype: %a@." MTypes.BasicT.pp b; *) |
|
222 |
f_basic b |
|
223 |
| MTypes.Tconst c -> Types.Tconst c |
|
224 |
| MTypes.Tenum e -> Types.Tenum e |
|
225 |
| MTypes.Tvar -> Types.Tvar |
|
226 |
| MTypes.Tunivar -> Types.Tunivar |
|
227 |
|
|
228 |
| MTypes.Tclock te -> Types.Tclock (mape te) |
|
229 |
| MTypes.Tarrow (te1, te2) -> Types.Tarrow (mape te1, mape te2) |
|
230 |
| MTypes.Ttuple tel -> Types.Ttuple (List.map mape tel) |
|
231 |
| MTypes.Tstruct id_te_l -> Types.Tstruct (List.map (fun (id, te) -> id, mape te) id_te_l) |
|
232 |
| MTypes.Tarray (de, te) -> Types.Tarray (de, mape te) |
|
233 |
| MTypes.Tstatic (de, te) -> Types.Tstatic (de, mape te) |
|
234 |
| MTypes.Tlink te -> Types.Tlink (mape te) |
|
235 |
in |
|
236 |
map_mtype_basic |
|
237 |
|
|
238 |
let export machine_type = |
|
239 |
let export_basic b = |
|
240 |
if MTypes.BasicT.is_int_type b then Types.type_int else |
|
241 |
if MTypes.BasicT.is_real_type b then Types.type_real else |
|
242 |
if MTypes.BasicT.is_bool_type b then Types.type_bool else |
|
243 |
( |
|
244 |
Format.eprintf "unhandled basic mtype is %a. Issues while dealing with basic type %a@.@?" MTypes.print_ty machine_type MTypes.BasicT.pp b; |
|
245 |
assert false |
|
246 |
) |
|
247 |
in |
|
248 |
map_mtype_basic export_basic machine_type |
|
249 |
|
|
250 |
end |
|
179 |
module ConvTypes = struct |
|
180 |
type type_expr = MTypes.type_expr |
|
181 |
|
|
182 |
let map_type_basic f_basic = |
|
183 |
let rec map_type_basic e = |
|
184 |
{ |
|
185 |
MTypes.tid = e.Types.tid; |
|
186 |
MTypes.tdesc = map_type_basic_desc (Types.type_desc e); |
|
187 |
} |
|
188 |
and map_type_basic_desc td = |
|
189 |
let mape = map_type_basic in |
|
190 |
match td with |
|
191 |
| Types.Tbasic b -> |
|
192 |
f_basic b |
|
193 |
| Types.Tconst c -> |
|
194 |
MTypes.Tconst c |
|
195 |
| Types.Tenum e -> |
|
196 |
MTypes.Tenum e |
|
197 |
| Types.Tvar -> |
|
198 |
MTypes.Tvar |
|
199 |
| Types.Tunivar -> |
|
200 |
MTypes.Tunivar |
|
201 |
| Types.Tclock te -> |
|
202 |
MTypes.Tclock (mape te) |
|
203 |
| Types.Tarrow (te1, te2) -> |
|
204 |
MTypes.Tarrow (mape te1, mape te2) |
|
205 |
| Types.Ttuple tel -> |
|
206 |
MTypes.Ttuple (List.map mape tel) |
|
207 |
| Types.Tstruct id_te_l -> |
|
208 |
MTypes.Tstruct (List.map (fun (id, te) -> id, mape te) id_te_l) |
|
209 |
| Types.Tarray (de, te) -> |
|
210 |
MTypes.Tarray (de, mape te) |
|
211 |
| Types.Tstatic (de, te) -> |
|
212 |
MTypes.Tstatic (de, mape te) |
|
213 |
| Types.Tlink te -> |
|
214 |
MTypes.Tlink (mape te) |
|
215 |
in |
|
216 |
map_type_basic |
|
217 |
|
|
218 |
let import main_typ = |
|
219 |
let import_basic b = |
|
220 |
if Types.BasicT.is_int_type b then MTypes.type_int |
|
221 |
else if Types.BasicT.is_real_type b then MTypes.type_real |
|
222 |
else if Types.BasicT.is_bool_type b then MTypes.type_bool |
|
223 |
else ( |
|
224 |
Format.eprintf "importing %a with issues!@.@?" Types.print_ty main_typ; |
|
225 |
assert false) |
|
226 |
in |
|
227 |
map_type_basic import_basic main_typ |
|
228 |
|
|
229 |
let map_mtype_basic f_basic = |
|
230 |
let rec map_mtype_basic e = |
|
231 |
{ |
|
232 |
Types.tid = e.MTypes.tid; |
|
233 |
Types.tdesc = map_mtype_basic_desc (MTypes.type_desc e); |
|
234 |
} |
|
235 |
and map_mtype_basic_desc td = |
|
236 |
let mape = map_mtype_basic in |
|
237 |
match td with |
|
238 |
| MTypes.Tbasic b -> |
|
239 |
(* Format.eprintf "supposely basic mtype: %a@." MTypes.BasicT.pp b; *) |
|
240 |
f_basic b |
|
241 |
| MTypes.Tconst c -> |
|
242 |
Types.Tconst c |
|
243 |
| MTypes.Tenum e -> |
|
244 |
Types.Tenum e |
|
245 |
| MTypes.Tvar -> |
|
246 |
Types.Tvar |
|
247 |
| MTypes.Tunivar -> |
|
248 |
Types.Tunivar |
|
249 |
| MTypes.Tclock te -> |
|
250 |
Types.Tclock (mape te) |
|
251 |
| MTypes.Tarrow (te1, te2) -> |
|
252 |
Types.Tarrow (mape te1, mape te2) |
|
253 |
| MTypes.Ttuple tel -> |
|
254 |
Types.Ttuple (List.map mape tel) |
|
255 |
| MTypes.Tstruct id_te_l -> |
|
256 |
Types.Tstruct (List.map (fun (id, te) -> id, mape te) id_te_l) |
|
257 |
| MTypes.Tarray (de, te) -> |
|
258 |
Types.Tarray (de, mape te) |
|
259 |
| MTypes.Tstatic (de, te) -> |
|
260 |
Types.Tstatic (de, mape te) |
|
261 |
| MTypes.Tlink te -> |
|
262 |
Types.Tlink (mape te) |
|
263 |
in |
|
264 |
map_mtype_basic |
|
265 |
|
|
266 |
let export machine_type = |
|
267 |
let export_basic b = |
|
268 |
if MTypes.BasicT.is_int_type b then Types.type_int |
|
269 |
else if MTypes.BasicT.is_real_type b then Types.type_real |
|
270 |
else if MTypes.BasicT.is_bool_type b then Types.type_bool |
|
271 |
else ( |
|
272 |
Format.eprintf |
|
273 |
"unhandled basic mtype is %a. Issues while dealing with basic type \ |
|
274 |
%a@.@?" |
|
275 |
MTypes.print_ty machine_type MTypes.BasicT.pp b; |
|
276 |
assert false) |
|
277 |
in |
|
278 |
map_mtype_basic export_basic machine_type |
|
279 |
end |
|
251 | 280 |
|
252 | 281 |
module Typing = Typing.Make (MTypes) (ConvTypes) |
253 |
|
|
282 |
|
|
254 | 283 |
(* Associate to each (node_id, var_id) its machine type *) |
255 |
let machine_type_table : (var_decl, MTypes.type_expr) Hashtbl.t = Hashtbl.create 13 |
|
284 |
let machine_type_table : (var_decl, MTypes.type_expr) Hashtbl.t = |
|
285 |
Hashtbl.create 13 |
|
256 | 286 |
|
257 | 287 |
(* Store the node signatures, with machine types when available *) |
258 | 288 |
let typing_env = ref Env.initial |
259 |
|
|
289 |
|
|
260 | 290 |
let is_specified v = |
261 | 291 |
(* Format.eprintf "looking for var %a@." Printers.pp_var v; *) |
262 | 292 |
Hashtbl.mem machine_type_table v |
... | ... | |
264 | 294 |
let pp_table fmt = |
265 | 295 |
Format.fprintf fmt "@[<v 0>["; |
266 | 296 |
Hashtbl.iter |
267 |
(fun v typ -> Format.fprintf fmt "%a -> %a,@ " Printers.pp_var v MTypes.print_ty typ ) |
|
297 |
(fun v typ -> |
|
298 |
Format.fprintf fmt "%a -> %a,@ " Printers.pp_var v MTypes.print_ty typ) |
|
268 | 299 |
machine_type_table; |
269 | 300 |
Format.fprintf fmt "@]" |
270 | 301 |
|
271 |
|
|
272 | 302 |
let get_specified_type v = |
273 | 303 |
(* Format.eprintf "Looking for variable %a in table [%t]@.@?" *) |
274 | 304 |
(* Printers.pp_var v *) |
275 | 305 |
(* pp_table; *) |
276 |
Hashtbl.find machine_type_table v
|
|
306 |
Hashtbl.find machine_type_table v |
|
277 | 307 |
|
278 | 308 |
let is_exportable v = |
279 |
is_specified v && ( |
|
280 |
let typ = get_specified_type v in |
|
281 |
match (MTypes.dynamic_type typ).MTypes.tdesc with |
|
282 |
| MTypes.Tbasic b -> MT.is_exportable b |
|
283 |
| MTypes.Tconst _ -> false (* Enumerated types are not "machine type" customizeable *) |
|
284 |
| _ -> assert false (* TODO deal with other constructs *) |
|
285 |
) |
|
309 |
is_specified v |
|
310 |
&& |
|
311 |
let typ = get_specified_type v in |
|
312 |
match (MTypes.dynamic_type typ).MTypes.tdesc with |
|
313 |
| MTypes.Tbasic b -> |
|
314 |
MT.is_exportable b |
|
315 |
| MTypes.Tconst _ -> |
|
316 |
false (* Enumerated types are not "machine type" customizeable *) |
|
317 |
| _ -> |
|
318 |
assert false |
|
319 |
|
|
320 |
(* TODO deal with other constructs *) |
|
286 | 321 |
(* could depend on the actual computed type *) |
287 | 322 |
|
288 |
let type_name typ =
|
|
323 |
let type_name typ = |
|
289 | 324 |
MTypes.print_ty Format.str_formatter typ; |
290 |
Format.flush_str_formatter ()
|
|
325 |
Format.flush_str_formatter () |
|
291 | 326 |
|
292 | 327 |
let pp_var_type fmt v = |
293 | 328 |
let typ = get_specified_type v in |
... | ... | |
296 | 331 |
let pp_c_var_type fmt v = |
297 | 332 |
let typ = get_specified_type v in |
298 | 333 |
MTypes.print_ty_param MT.pp_c fmt typ |
299 |
|
|
334 |
|
|
300 | 335 |
(************** Checking types ******************) |
301 |
|
|
336 |
|
|
302 | 337 |
let erroneous_annotation loc = |
303 | 338 |
Format.eprintf "Invalid annotation for machine_type at loc %a@." |
304 | 339 |
Location.pp_loc loc; |
305 | 340 |
assert false |
306 | 341 |
|
307 |
|
|
308 | 342 |
let valid_subtype subtype typ = |
309 | 343 |
let mismatch subtyp typ = |
310 |
Format.eprintf "Subtype mismatch %a vs %a@." MTypes.print_ty subtyp Types.print_ty typ; false |
|
344 |
Format.eprintf "Subtype mismatch %a vs %a@." MTypes.print_ty subtyp |
|
345 |
Types.print_ty typ; |
|
346 |
false |
|
311 | 347 |
in |
312 | 348 |
match (MTypes.dynamic_type subtype).MTypes.tdesc with |
313 |
| MTypes.Tconst c -> Types.is_const_type typ c |
|
314 |
| MTypes.Tbasic MT.MTint _ -> Types.is_int_type typ |
|
315 |
| MTypes.Tbasic MT.MTreal _ -> Types.is_real_type typ |
|
316 |
| MTypes.Tbasic MT.MTbool -> Types.is_bool_type typ |
|
317 |
| _ -> mismatch subtype typ |
|
318 |
|
|
349 |
| MTypes.Tconst c -> |
|
350 |
Types.is_const_type typ c |
|
351 |
| MTypes.Tbasic (MT.MTint _) -> |
|
352 |
Types.is_int_type typ |
|
353 |
| MTypes.Tbasic (MT.MTreal _) -> |
|
354 |
Types.is_real_type typ |
|
355 |
| MTypes.Tbasic MT.MTbool -> |
|
356 |
Types.is_bool_type typ |
|
357 |
| _ -> |
|
358 |
mismatch subtype typ |
|
359 |
|
|
319 | 360 |
let type_of_name name = |
320 | 361 |
match name with |
321 |
| "uint8" -> type_uint8 |
|
322 |
| "uint16" -> type_uint16 |
|
323 |
| "uint32" -> type_uint32 |
|
324 |
| "uint64" -> type_uint64 |
|
325 |
| "int8" -> type_int8 |
|
326 |
| "int16" -> type_int16 |
|
327 |
| "int32" -> type_int32 |
|
328 |
| "int64" -> type_int64 |
|
329 |
| _ -> assert false (* unknown custom machine type *) |
|
330 |
|
|
362 |
| "uint8" -> |
|
363 |
type_uint8 |
|
364 |
| "uint16" -> |
|
365 |
type_uint16 |
|
366 |
| "uint32" -> |
|
367 |
type_uint32 |
|
368 |
| "uint64" -> |
|
369 |
type_uint64 |
|
370 |
| "int8" -> |
|
371 |
type_int8 |
|
372 |
| "int16" -> |
|
373 |
type_int16 |
|
374 |
| "int32" -> |
|
375 |
type_int32 |
|
376 |
| "int64" -> |
|
377 |
type_int64 |
|
378 |
| _ -> |
|
379 |
assert false |
|
380 |
(* unknown custom machine type *) |
|
381 |
|
|
331 | 382 |
let register_var var typ = |
332 | 383 |
(* let typ = type_of_name type_name in *) |
333 |
if valid_subtype typ var.var_type then ( |
|
334 |
Hashtbl.add machine_type_table var typ |
|
335 |
) |
|
336 |
else |
|
337 |
erroneous_annotation var.var_loc |
|
338 |
|
|
384 |
if valid_subtype typ var.var_type then Hashtbl.add machine_type_table var typ |
|
385 |
else erroneous_annotation var.var_loc |
|
386 |
|
|
339 | 387 |
(* let register_var_opt var type_name_opt = *) |
340 | 388 |
(* match type_name_opt with *) |
341 | 389 |
(* | None -> () *) |
342 | 390 |
(* | Some type_name -> register_var var type_name *) |
343 |
|
|
391 |
|
|
344 | 392 |
(************** Registering annotations ******************) |
345 | 393 |
|
346 |
|
|
347 | 394 |
let register_node vars annots = |
348 |
List.fold_left (fun accu annot -> |
|
349 |
let annl = annot.annots in |
|
350 |
List.fold_left (fun accu (kwd, value) -> |
|
351 |
if kwd = keyword then |
|
352 |
let expr = value.eexpr_qfexpr in |
|
353 |
match Corelang.expr_list_of_expr expr with |
|
354 |
| [var_id; type_name] -> ( |
|
355 |
match var_id.expr_desc, type_name.expr_desc with |
|
356 |
| Expr_ident var_id, Expr_const (Const_string type_name) -> |
|
357 |
let var = List.find (fun v -> v.var_id = var_id) vars in |
|
358 |
Log.report ~level:2 (fun fmt -> |
|
359 |
Format.fprintf fmt "Recorded type %s for variable %a (parent node is %s)@ " |
|
360 |
type_name |
|
361 |
Printers.pp_var var |
|
362 |
(match var.var_parent_nodeid with Some id -> id | None -> "unknown") |
|
363 |
); |
|
364 |
let typ = type_of_name type_name in |
|
365 |
register_var var typ; |
|
366 |
var::accu |
|
367 |
| _ -> erroneous_annotation expr.expr_loc |
|
368 |
) |
|
369 |
| _ -> erroneous_annotation expr.expr_loc |
|
370 |
else |
|
371 |
accu |
|
372 |
) accu annl |
|
373 |
) [] annots |
|
374 |
|
|
395 |
List.fold_left |
|
396 |
(fun accu annot -> |
|
397 |
let annl = annot.annots in |
|
398 |
List.fold_left |
|
399 |
(fun accu (kwd, value) -> |
|
400 |
if kwd = keyword then |
|
401 |
let expr = value.eexpr_qfexpr in |
|
402 |
match Corelang.expr_list_of_expr expr with |
|
403 |
| [ var_id; type_name ] -> ( |
|
404 |
match var_id.expr_desc, type_name.expr_desc with |
|
405 |
| Expr_ident var_id, Expr_const (Const_string type_name) -> |
|
406 |
let var = List.find (fun v -> v.var_id = var_id) vars in |
|
407 |
Log.report ~level:2 (fun fmt -> |
|
408 |
Format.fprintf fmt |
|
409 |
"Recorded type %s for variable %a (parent node is %s)@ " |
|
410 |
type_name Printers.pp_var var |
|
411 |
(match var.var_parent_nodeid with |
|
412 |
| Some id -> |
|
413 |
id |
|
414 |
| None -> |
|
415 |
"unknown")); |
|
416 |
let typ = type_of_name type_name in |
|
417 |
register_var var typ; |
|
418 |
var :: accu |
|
419 |
| _ -> |
|
420 |
erroneous_annotation expr.expr_loc) |
|
421 |
| _ -> |
|
422 |
erroneous_annotation expr.expr_loc |
|
423 |
else accu) |
|
424 |
accu annl) |
|
425 |
[] annots |
|
375 | 426 |
|
376 | 427 |
let check_node nd vars = |
377 |
(* TODO check that all access to vars are valid *) |
|
428 |
(* TODO check that all access to vars are valid *)
|
|
378 | 429 |
() |
379 |
|
|
430 |
|
|
380 | 431 |
let type_of_vlist vars = |
381 |
let tyl = List.map (fun v -> if is_specified v then get_specified_type v else |
|
382 |
ConvTypes.import v.var_type |
|
383 |
) vars in |
|
432 |
let tyl = |
|
433 |
List.map |
|
434 |
(fun v -> |
|
435 |
if is_specified v then get_specified_type v |
|
436 |
else ConvTypes.import v.var_type) |
|
437 |
vars |
|
438 |
in |
|
384 | 439 |
MTypes.type_of_type_list tyl |
385 | 440 |
|
386 |
|
|
387 | 441 |
let load prog = |
388 | 442 |
let init_env = |
389 |
Env.fold (fun id typ env ->
|
|
390 |
Env.add_value env id (ConvTypes.import typ)
|
|
391 |
)
|
|
392 |
Basic_library.type_env Env.initial in
|
|
443 |
Env.fold |
|
444 |
(fun id typ env -> Env.add_value env id (ConvTypes.import typ))
|
|
445 |
Basic_library.type_env Env.initial
|
|
446 |
in |
|
393 | 447 |
let env = |
394 |
List.fold_left (fun type_env top -> |
|
395 |
match top.top_decl_desc with |
|
396 |
| Node nd -> |
|
397 |
(* Format.eprintf "Registeing node %s@." nd.node_id; *) |
|
398 |
let vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in |
|
399 |
let constrained_vars = register_node vars nd.node_annot in |
|
400 |
check_node nd constrained_vars; |
|
401 |
|
|
402 |
(* Computing the node type *) |
|
403 |
let ty_ins = type_of_vlist nd.node_inputs in |
|
404 |
let ty_outs = type_of_vlist nd.node_outputs in |
|
405 |
let ty_node = MTypes.new_ty (MTypes.Tarrow (ty_ins,ty_outs)) in |
|
406 |
Typing.generalize ty_node; |
|
407 |
let env = Env.add_value type_env nd.node_id ty_node in |
|
408 |
(* Format.eprintf "Env: %a" (Env.pp_env MTypes.print_ty) env; *) |
|
409 |
env |
|
410 |
|
|
411 |
| _ -> type_env |
|
412 |
(* | ImportedNode ind -> *) |
|
413 |
(* let vars = ind.nodei_inputs @ ind.nodei_outputs in *) |
|
414 |
(* register_node ind.nodei_id vars ind.nodei_annot *) |
|
415 |
(* | _ -> () TODO: shall we load something for Open statements? *) |
|
416 |
) init_env prog |
|
448 |
List.fold_left |
|
449 |
(fun type_env top -> |
|
450 |
match top.top_decl_desc with |
|
451 |
| Node nd -> |
|
452 |
(* Format.eprintf "Registeing node %s@." nd.node_id; *) |
|
453 |
let vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in |
|
454 |
let constrained_vars = register_node vars nd.node_annot in |
|
455 |
check_node nd constrained_vars; |
|
456 |
|
|
457 |
(* Computing the node type *) |
|
458 |
let ty_ins = type_of_vlist nd.node_inputs in |
|
459 |
let ty_outs = type_of_vlist nd.node_outputs in |
|
460 |
let ty_node = MTypes.new_ty (MTypes.Tarrow (ty_ins, ty_outs)) in |
|
461 |
Typing.generalize ty_node; |
|
462 |
let env = Env.add_value type_env nd.node_id ty_node in |
|
463 |
(* Format.eprintf "Env: %a" (Env.pp_env MTypes.print_ty) env; *) |
|
464 |
env |
|
465 |
| _ -> |
|
466 |
type_env |
|
467 |
(* | ImportedNode ind -> *) |
|
468 |
(* let vars = ind.nodei_inputs @ ind.nodei_outputs in *) |
|
469 |
(* register_node ind.nodei_id vars ind.nodei_annot *) |
|
470 |
(* | _ -> () TODO: shall we load something for Open statements? *)) |
|
471 |
init_env prog |
|
417 | 472 |
in |
418 | 473 |
typing_env := env |
419 | 474 |
|
... | ... | |
421 | 476 |
let init_env = !typing_env in |
422 | 477 |
(* Format.eprintf "Init env: %a@." (Env.pp_env MTypes.print_ty) init_env; *) |
423 | 478 |
(* Rebuilding the variables environment from accumulated knowledge *) |
424 |
let env,vars = (* First, we add non specified variables *) |
|
425 |
List.fold_left (fun (env, vars) v -> |
|
426 |
if not (is_specified v) then |
|
427 |
let env = Env.add_value env v.var_id (ConvTypes.import v.var_type) in |
|
428 |
env, v::vars |
|
429 |
else |
|
430 |
env, vars |
|
431 |
) (init_env, []) init_vars |
|
479 |
let env, vars = |
|
480 |
(* First, we add non specified variables *) |
|
481 |
List.fold_left |
|
482 |
(fun (env, vars) v -> |
|
483 |
if not (is_specified v) then |
|
484 |
let env = Env.add_value env v.var_id (ConvTypes.import v.var_type) in |
|
485 |
env, v :: vars |
|
486 |
else env, vars) |
|
487 |
(init_env, []) init_vars |
|
432 | 488 |
in |
433 |
|
|
489 |
|
|
434 | 490 |
(* Then declared ones *) |
435 | 491 |
let env, vars = |
436 |
Hashtbl.fold (fun vdecl machine_type (env, vds) ->
|
|
437 |
if vdecl.var_parent_nodeid = Some parentid then (
|
|
438 |
(* Format.eprintf "Adding variable %a to the environement@.@?" Printers.pp_var vdecl; *)
|
|
439 |
let env = Env.add_value env vdecl.var_id machine_type in
|
|
440 |
env, vdecl::vds
|
|
441 |
)
|
|
442 |
else
|
|
443 |
env, vds
|
|
444 |
) machine_type_table (env, vars)
|
|
492 |
Hashtbl.fold |
|
493 |
(fun vdecl machine_type (env, vds) ->
|
|
494 |
if vdecl.var_parent_nodeid = Some parentid then
|
|
495 |
(* Format.eprintf "Adding variable %a to the environement@.@?"
|
|
496 |
Printers.pp_var vdecl; *)
|
|
497 |
let env = Env.add_value env vdecl.var_id machine_type in
|
|
498 |
env, vdecl :: vds
|
|
499 |
else env, vds)
|
|
500 |
machine_type_table (env, vars)
|
|
445 | 501 |
in |
446 | 502 |
|
447 |
|
|
448 |
(* Format.eprintf "env with local vars: %a@." (Env.pp_env MTypes.print_ty) env; *)
|
|
503 |
(* Format.eprintf "env with local vars: %a@." (Env.pp_env MTypes.print_ty) |
|
504 |
env; *)
|
|
449 | 505 |
(* Format.eprintf "expr = %a@." Printers.pp_expr expr; *) |
450 | 506 |
(* let res = *) |
451 |
Typing.type_expr |
|
452 |
(env,vars) |
|
453 |
false (* not in main node *) |
|
454 |
false (* no a constant *) |
|
455 |
expr |
|
456 |
(* in *) |
|
457 |
(* Format.eprintf "typing ok = %a@." MTypes.print_ty res; *) |
|
458 |
(* res *) |
|
459 |
|
|
460 |
(* Typing the expression (vars = expr) in node |
|
461 |
|
|
462 |
*) |
|
507 |
Typing.type_expr (env, vars) false (* not in main node *) false |
|
508 |
(* no a constant *) expr |
|
509 |
|
|
510 |
(* in *) |
|
511 |
(* Format.eprintf "typing ok = %a@." MTypes.print_ty res; *) |
|
512 |
(* res *) |
|
513 |
|
|
514 |
(* Typing the expression (vars = expr) in node *) |
|
463 | 515 |
let type_def node vars expr = |
464 | 516 |
(* Format.eprintf "Typing def %a = %a@.@." *) |
465 | 517 |
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) vars *) |
466 | 518 |
(* Printers.pp_expr expr *) |
467 | 519 |
(* ; *) |
468 |
let typ = type_expr node expr in
|
|
469 |
(* Format.eprintf "Type is %a. Saving stuff@.@." MTypes.print_ty typ; *)
|
|
470 |
let typ = MTypes.type_list_of_type typ in
|
|
471 |
List.iter2 register_var vars typ
|
|
520 |
let typ = type_expr node expr in |
|
521 |
(* Format.eprintf "Type is %a. Saving stuff@.@." MTypes.print_ty typ; *) |
|
522 |
let typ = MTypes.type_list_of_type typ in
|
|
523 |
List.iter2 register_var vars typ
|
|
472 | 524 |
|
473 | 525 |
let has_machine_type () = |
474 | 526 |
let annl = Annotations.get_expr_annotations keyword in |
475 | 527 |
(* Format.eprintf "has _mchine _type annotations: %i@." (List.length annl); *) |
476 | 528 |
List.length annl > 0 |
477 |
|
|
529 |
|
|
478 | 530 |
(* Local Variables: *) |
479 | 531 |
(* compile-command:"make -C ../.." *) |
480 | 532 |
(* End: *) |
481 |
|
Also available in: Unified diff
reformatting