Revision ca7ff3f7
Added by Lélio Brun 8 months 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