[486] | 1 | (* *********************************************************************) |
---|
| 2 | (* *) |
---|
| 3 | (* The Compcert verified compiler *) |
---|
| 4 | (* *) |
---|
| 5 | (* Xavier Leroy, INRIA Paris-Rocquencourt *) |
---|
| 6 | (* *) |
---|
| 7 | (* Copyright Institut National de Recherche en Informatique et en *) |
---|
| 8 | (* Automatique. All rights reserved. This file is distributed *) |
---|
| 9 | (* under the terms of the GNU General Public License as published by *) |
---|
| 10 | (* the Free Software Foundation, either version 2 of the License, or *) |
---|
| 11 | (* (at your option) any later version. This file is also distributed *) |
---|
| 12 | (* under the terms of the INRIA Non-Commercial License Agreement. *) |
---|
| 13 | (* *) |
---|
| 14 | (* *********************************************************************) |
---|
| 15 | |
---|
| 16 | (* Operations on C types and abstract syntax *) |
---|
| 17 | |
---|
| 18 | open Printf |
---|
| 19 | open Errors |
---|
| 20 | open C |
---|
| 21 | open Env |
---|
| 22 | open Machine |
---|
| 23 | |
---|
| 24 | (* Set and Map structures over identifiers *) |
---|
| 25 | |
---|
| 26 | module Ident = struct |
---|
| 27 | type t = ident |
---|
| 28 | let compare id1 id2 = Pervasives.compare id1.stamp id2.stamp |
---|
| 29 | end |
---|
| 30 | |
---|
| 31 | module IdentSet = Set.Make(Ident) |
---|
| 32 | module IdentMap = Map.Make(Ident) |
---|
| 33 | |
---|
| 34 | (* Operations on attributes *) |
---|
| 35 | |
---|
| 36 | (* Lists of attributes are kept sorted in increasing order *) |
---|
| 37 | |
---|
| 38 | let rec add_attributes (al1: attributes) (al2: attributes) = |
---|
| 39 | match al1, al2 with |
---|
| 40 | | [], _ -> al2 |
---|
| 41 | | _, [] -> al1 |
---|
| 42 | | a1 :: al1', a2 :: al2' -> |
---|
| 43 | if a1 < a2 then a1 :: add_attributes al1' al2 |
---|
| 44 | else if a1 > a2 then a2 :: add_attributes al1 al2' |
---|
| 45 | else a1 :: add_attributes al1' al2' |
---|
| 46 | |
---|
| 47 | let rec remove_attributes (al1: attributes) (al2: attributes) = |
---|
| 48 | (* viewed as sets: al1 \ al2 *) |
---|
| 49 | match al1, al2 with |
---|
| 50 | | [], _ -> [] |
---|
| 51 | | _, [] -> al1 |
---|
| 52 | | a1 :: al1', a2 :: al2' -> |
---|
| 53 | if a1 < a2 then a1 :: remove_attributes al1' al2 |
---|
| 54 | else if a1 > a2 then remove_attributes al1 al2' |
---|
| 55 | else remove_attributes al1' al2' |
---|
| 56 | |
---|
| 57 | let rec incl_attributes (al1: attributes) (al2: attributes) = |
---|
| 58 | match al1, al2 with |
---|
| 59 | | [], _ -> true |
---|
| 60 | | _ :: _, [] -> false |
---|
| 61 | | a1 :: al1', a2 :: al2' -> |
---|
| 62 | if a1 < a2 then false |
---|
| 63 | else if a1 > a2 then incl_attributes al1 al2' |
---|
| 64 | else incl_attributes al1' al2' |
---|
| 65 | |
---|
| 66 | (* Adding top-level attributes to a type. Doesn't need to unroll defns. *) |
---|
| 67 | (* Array types cannot carry attributes, so add them to the element type. *) |
---|
| 68 | |
---|
| 69 | let rec add_attributes_type attr t = |
---|
| 70 | match t with |
---|
| 71 | | TVoid a -> TVoid (add_attributes attr a) |
---|
| 72 | | TInt(ik, a) -> TInt(ik, add_attributes attr a) |
---|
| 73 | | TFloat(fk, a) -> TFloat(fk, add_attributes attr a) |
---|
| 74 | | TPtr(ty, a) -> TPtr(ty, add_attributes attr a) |
---|
| 75 | | TArray(ty, sz, a) -> TArray(add_attributes_type attr ty, sz, a) |
---|
| 76 | | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr |
---|
| 77 | a) |
---|
| 78 | | TNamed(s, a) -> TNamed(s, add_attributes attr a) |
---|
| 79 | | TStruct(s, a) -> TStruct(s, add_attributes attr a) |
---|
| 80 | | TUnion(s, a) -> TUnion(s, add_attributes attr a) |
---|
| 81 | |
---|
| 82 | (* Unrolling of typedef *) |
---|
| 83 | |
---|
| 84 | let rec unroll env t = |
---|
| 85 | match t with |
---|
| 86 | | TNamed(name, attr) -> |
---|
| 87 | let ty = Env.find_typedef env name in |
---|
| 88 | unroll env (add_attributes_type attr ty) |
---|
| 89 | | _ -> t |
---|
| 90 | |
---|
| 91 | (* Extracting the attributes of a type *) |
---|
| 92 | |
---|
| 93 | let rec attributes_of_type env t = |
---|
| 94 | match t with |
---|
| 95 | | TVoid a -> a |
---|
| 96 | | TInt(ik, a) -> a |
---|
| 97 | | TFloat(fk, a) -> a |
---|
| 98 | | TPtr(ty, a) -> a |
---|
| 99 | | TArray(ty, sz, a) -> a (* correct? *) |
---|
| 100 | | TFun(ty, params, vararg, a) -> a |
---|
| 101 | | TNamed(s, a) -> attributes_of_type env (unroll env t) |
---|
| 102 | | TStruct(s, a) -> a |
---|
| 103 | | TUnion(s, a) -> a |
---|
| 104 | |
---|
| 105 | (* Changing the attributes of a type (at top-level) *) |
---|
| 106 | (* Same hack as above for array types. *) |
---|
| 107 | |
---|
| 108 | let rec change_attributes_type env (f: attributes -> attributes) t = |
---|
| 109 | match t with |
---|
| 110 | | TVoid a -> TVoid (f a) |
---|
| 111 | | TInt(ik, a) -> TInt(ik, f a) |
---|
| 112 | | TFloat(fk, a) -> TFloat(fk, f a) |
---|
| 113 | | TPtr(ty, a) -> TPtr(ty, f a) |
---|
| 114 | | TArray(ty, sz, a) -> |
---|
| 115 | TArray(change_attributes_type env f ty, sz, a) |
---|
| 116 | | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a) |
---|
| 117 | | TNamed(s, a) -> |
---|
| 118 | let t1 = unroll env t in |
---|
| 119 | let t2 = change_attributes_type env f t1 in |
---|
| 120 | if t2 = t1 then t else t2 (* avoid useless expansion *) |
---|
| 121 | | TStruct(s, a) -> TStruct(s, f a) |
---|
| 122 | | TUnion(s, a) -> TUnion(s, f a) |
---|
| 123 | |
---|
| 124 | let remove_attributes_type env attr t = |
---|
| 125 | change_attributes_type env (fun a -> remove_attributes a attr) t |
---|
| 126 | |
---|
| 127 | let erase_attributes_type env t = |
---|
| 128 | change_attributes_type env (fun a -> []) t |
---|
| 129 | |
---|
| 130 | (* Type compatibility *) |
---|
| 131 | |
---|
| 132 | exception Incompat |
---|
| 133 | |
---|
| 134 | let combine_types ?(noattrs = false) env t1 t2 = |
---|
| 135 | |
---|
| 136 | let comp_attr a1 a2 = |
---|
| 137 | if a1 = a2 then a2 |
---|
| 138 | else if noattrs then add_attributes a1 a2 |
---|
| 139 | else raise Incompat |
---|
| 140 | and comp_base x1 x2 = |
---|
| 141 | if x1 = x2 then x2 else raise Incompat |
---|
| 142 | and comp_array_size sz1 sz2 = |
---|
| 143 | match sz1, sz2 with |
---|
| 144 | | None, _ -> sz2 |
---|
| 145 | | _, None -> sz1 |
---|
| 146 | | Some n1, Some n2 -> if n1 = n2 then Some n2 else raise Incompat |
---|
| 147 | and comp_conv (id, ty) = |
---|
| 148 | match unroll env ty with |
---|
| 149 | | TInt(kind, attr) -> |
---|
| 150 | begin match kind with |
---|
| 151 | | IBool | IChar | ISChar | IUChar | IShort | IUShort -> raise Incompat |
---|
| 152 | | _ -> () |
---|
| 153 | end |
---|
| 154 | | TFloat(kind, attr) -> |
---|
| 155 | begin match kind with |
---|
| 156 | | FFloat -> raise Incompat |
---|
| 157 | | _ -> () |
---|
| 158 | end |
---|
| 159 | | _ -> () in |
---|
| 160 | |
---|
| 161 | let rec comp t1 t2 = |
---|
| 162 | match t1, t2 with |
---|
| 163 | | TVoid a1, TVoid a2 -> |
---|
| 164 | TVoid(comp_attr a1 a2) |
---|
| 165 | | TInt(ik1, a1), TInt(ik2, a2) -> |
---|
| 166 | TInt(comp_base ik1 ik2, comp_attr a1 a2) |
---|
| 167 | | TFloat(fk1, a1), TFloat(fk2, a2) -> |
---|
| 168 | TFloat(comp_base fk1 fk2, comp_attr a1 a2) |
---|
| 169 | | TPtr(ty1, a1), TPtr(ty2, a2) -> |
---|
| 170 | TPtr(comp ty1 ty2, comp_attr a1 a2) |
---|
| 171 | | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) -> |
---|
| 172 | TArray(comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2) |
---|
| 173 | | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) -> |
---|
| 174 | let (params, vararg) = |
---|
| 175 | match params1, params2 with |
---|
| 176 | | None, None -> None, false |
---|
| 177 | | None, Some l2 -> List.iter comp_conv l2; (params2, vararg2) |
---|
| 178 | | Some l1, None -> List.iter comp_conv l1; (params1, vararg1) |
---|
| 179 | | Some l1, Some l2 -> |
---|
| 180 | if List.length l1 <> List.length l2 then raise Incompat; |
---|
| 181 | (Some(List.map2 (fun (id1, ty1) (id2, ty2) -> (id2, comp ty1 ty2)) |
---|
| 182 | l1 l2), |
---|
| 183 | comp_base vararg1 vararg2) |
---|
| 184 | in |
---|
| 185 | TFun(comp ty1 ty2, params, vararg, comp_attr a1 a2) |
---|
| 186 | | TNamed _, _ -> comp (unroll env t1) t2 |
---|
| 187 | | _, TNamed _ -> comp t1 (unroll env t2) |
---|
| 188 | | TStruct(s1, a1), TStruct(s2, a2) -> |
---|
| 189 | TStruct(comp_base s1 s2, comp_attr a1 a2) |
---|
| 190 | | TUnion(s1, a1), TUnion(s2, a2) -> |
---|
| 191 | TUnion(comp_base s1 s2, comp_attr a1 a2) |
---|
| 192 | | _, _ -> |
---|
| 193 | raise Incompat |
---|
| 194 | |
---|
| 195 | in try Some(comp t1 t2) with Incompat -> None |
---|
| 196 | |
---|
| 197 | let compatible_types ?noattrs env t1 t2 = |
---|
| 198 | match combine_types ?noattrs env t1 t2 with Some _ -> true | None -> false |
---|
| 199 | |
---|
| 200 | (* Naive placement algorithm for bit fields, might not match that |
---|
| 201 | of the compiler. *) |
---|
| 202 | |
---|
| 203 | let pack_bitfields ml = |
---|
| 204 | let rec pack nbits = function |
---|
| 205 | | [] -> |
---|
| 206 | (nbits, []) |
---|
| 207 | | m :: ms as ml -> |
---|
| 208 | match m.fld_bitfield with |
---|
| 209 | | None -> (nbits, ml) |
---|
| 210 | | Some n -> |
---|
| 211 | if n = 0 then |
---|
| 212 | (nbits, ms) (* bit width 0 means end of pack *) |
---|
| 213 | else if nbits + n > 8 * !config.sizeof_int then |
---|
| 214 | (nbits, ml) (* doesn't fit in current word *) |
---|
| 215 | else |
---|
| 216 | pack (nbits + n) ms (* add to current word *) |
---|
| 217 | in |
---|
| 218 | let (nbits, ml') = pack 0 ml in |
---|
| 219 | let sz = |
---|
| 220 | if nbits <= 8 then 1 else |
---|
| 221 | if nbits <= 16 then 2 else |
---|
| 222 | if nbits <= 32 then 4 else |
---|
| 223 | if nbits <= 64 then 8 else assert false in |
---|
| 224 | (sz, ml') |
---|
| 225 | |
---|
| 226 | (* Natural alignment, in bytes *) |
---|
| 227 | |
---|
| 228 | let alignof_ikind = function |
---|
| 229 | | IBool | IChar | ISChar | IUChar -> 1 |
---|
| 230 | | IInt | IUInt -> !config.alignof_int |
---|
| 231 | | IShort | IUShort -> !config.alignof_short |
---|
| 232 | | ILong | IULong -> !config.alignof_long |
---|
| 233 | | ILongLong | IULongLong -> !config.alignof_longlong |
---|
| 234 | |
---|
| 235 | let alignof_fkind = function |
---|
| 236 | | FFloat -> !config.alignof_float |
---|
| 237 | | FDouble -> !config.alignof_double |
---|
| 238 | | FLongDouble -> !config.alignof_longdouble |
---|
| 239 | |
---|
| 240 | (* Return natural alignment of given type, or None if the type is incomplete *) |
---|
| 241 | |
---|
| 242 | let rec alignof env t = |
---|
| 243 | match t with |
---|
| 244 | | TVoid _ -> !config.alignof_void |
---|
| 245 | | TInt(ik, _) -> Some(alignof_ikind ik) |
---|
| 246 | | TFloat(fk, _) -> Some(alignof_fkind fk) |
---|
| 247 | | TPtr(_, _) -> Some(!config.alignof_ptr) |
---|
| 248 | | TArray(ty, _, _) -> alignof env ty |
---|
| 249 | | TFun(_, _, _, _) -> !config.alignof_fun |
---|
| 250 | | TNamed(_, _) -> alignof env (unroll env t) |
---|
| 251 | | TStruct(name, _) -> |
---|
| 252 | let ci = Env.find_struct env name in ci.ci_alignof |
---|
| 253 | | TUnion(name, _) -> |
---|
| 254 | let ci = Env.find_union env name in ci.ci_alignof |
---|
| 255 | |
---|
| 256 | (* Compute the natural alignment of a struct or union. *) |
---|
| 257 | |
---|
| 258 | let alignof_struct_union env members = |
---|
| 259 | let rec align_rec al = function |
---|
| 260 | | [] -> Some al |
---|
| 261 | | m :: rem as ml -> |
---|
| 262 | if m.fld_bitfield = None then begin |
---|
| 263 | match alignof env m.fld_typ with |
---|
| 264 | | None -> None |
---|
| 265 | | Some a -> align_rec (max a al) rem |
---|
| 266 | end else begin |
---|
| 267 | let (sz, ml') = pack_bitfields ml in |
---|
| 268 | align_rec (max sz al) ml' |
---|
| 269 | end |
---|
| 270 | in align_rec 1 members |
---|
| 271 | |
---|
| 272 | let align x boundary = |
---|
| 273 | (* boundary must be a power of 2 *) |
---|
| 274 | (x + boundary - 1) land (lnot (boundary - 1)) |
---|
| 275 | |
---|
| 276 | (* Size of, in bytes *) |
---|
| 277 | |
---|
| 278 | let sizeof_ikind = function |
---|
| 279 | | IBool | IChar | ISChar | IUChar -> 1 |
---|
| 280 | | IInt | IUInt -> !config.sizeof_int |
---|
| 281 | | IShort | IUShort -> !config.sizeof_short |
---|
| 282 | | ILong | IULong -> !config.sizeof_long |
---|
| 283 | | ILongLong | IULongLong -> !config.sizeof_longlong |
---|
| 284 | |
---|
| 285 | let sizeof_fkind = function |
---|
| 286 | | FFloat -> !config.sizeof_float |
---|
| 287 | | FDouble -> !config.sizeof_double |
---|
| 288 | | FLongDouble -> !config.sizeof_longdouble |
---|
| 289 | |
---|
| 290 | (* Overflow-avoiding multiplication of an int64 and an int, with |
---|
| 291 | result in type int. *) |
---|
| 292 | |
---|
| 293 | let cautious_mul (a: int64) (b: int) = |
---|
| 294 | if b = 0 || a <= Int64.of_int (max_int / b) |
---|
| 295 | then Some(Int64.to_int a * b) |
---|
| 296 | else None |
---|
| 297 | |
---|
| 298 | (* Return size of type, in bytes, or [None] if the type is incomplete *) |
---|
| 299 | |
---|
| 300 | let rec sizeof env t = |
---|
| 301 | match t with |
---|
| 302 | | TVoid _ -> !config.sizeof_void |
---|
| 303 | | TInt(ik, _) -> Some(sizeof_ikind ik) |
---|
| 304 | | TFloat(fk, _) -> Some(sizeof_fkind fk) |
---|
| 305 | | TPtr(_, _) -> Some(!config.sizeof_ptr) |
---|
| 306 | | TArray(ty, None, _) -> None |
---|
| 307 | | TArray(ty, Some n, _) as t' -> |
---|
| 308 | begin match sizeof env ty with |
---|
| 309 | | None -> None |
---|
| 310 | | Some s -> |
---|
| 311 | match cautious_mul n s with |
---|
| 312 | | Some sz -> Some sz |
---|
| 313 | | None -> error "sizeof(%a) overflows" Cprint.typ t'; Some 1 |
---|
| 314 | end |
---|
| 315 | | TFun(_, _, _, _) -> !config.sizeof_fun |
---|
| 316 | | TNamed(_, _) -> sizeof env (unroll env t) |
---|
| 317 | | TStruct(name, _) -> |
---|
| 318 | let ci = Env.find_struct env name in ci.ci_sizeof |
---|
| 319 | | TUnion(name, _) -> |
---|
| 320 | let ci = Env.find_union env name in ci.ci_sizeof |
---|
| 321 | |
---|
| 322 | (* Compute the size of a union. |
---|
| 323 | It is the size is the max of the sizes of fields, rounded up to the |
---|
| 324 | natural alignment. *) |
---|
| 325 | |
---|
| 326 | let sizeof_union env members = |
---|
| 327 | let rec sizeof_rec sz = function |
---|
| 328 | | [] -> |
---|
| 329 | begin match alignof_struct_union env members with |
---|
| 330 | | None -> None (* should not happen? *) |
---|
| 331 | | Some al -> Some (align sz al) |
---|
| 332 | end |
---|
| 333 | | m :: rem -> |
---|
| 334 | begin match sizeof env m.fld_typ with |
---|
| 335 | | None -> None |
---|
| 336 | | Some s -> sizeof_rec (max sz s) rem |
---|
| 337 | end |
---|
| 338 | in sizeof_rec 0 members |
---|
| 339 | |
---|
| 340 | (* Compute the size of a struct. |
---|
| 341 | We lay out fields consecutively, inserting padding to preserve |
---|
| 342 | their natural alignment. *) |
---|
| 343 | |
---|
| 344 | let sizeof_struct env members = |
---|
| 345 | let rec sizeof_rec ofs = function |
---|
| 346 | | [] | [ { fld_typ = TArray(_, None, _) } ] -> |
---|
| 347 | (* C99: ty[] allowed as last field *) |
---|
| 348 | begin match alignof_struct_union env members with |
---|
| 349 | | None -> None (* should not happen? *) |
---|
| 350 | | Some al -> Some (align ofs al) |
---|
| 351 | end |
---|
| 352 | | m :: rem as ml -> |
---|
| 353 | if m.fld_bitfield = None then begin |
---|
| 354 | match alignof env m.fld_typ, sizeof env m.fld_typ with |
---|
| 355 | | Some a, Some s -> sizeof_rec (align ofs a + s) rem |
---|
| 356 | | _, _ -> None |
---|
| 357 | end else begin |
---|
| 358 | let (sz, ml') = pack_bitfields ml in |
---|
| 359 | sizeof_rec (align ofs sz + sz) ml' |
---|
| 360 | end |
---|
| 361 | in sizeof_rec 0 members |
---|
| 362 | |
---|
| 363 | (* Determine whether a type is incomplete *) |
---|
| 364 | |
---|
| 365 | let incomplete_type env t = |
---|
| 366 | match sizeof env t with None -> true | Some _ -> false |
---|
| 367 | |
---|
| 368 | (* Computing composite_info records *) |
---|
| 369 | |
---|
| 370 | let composite_info_decl env su = |
---|
| 371 | { ci_kind = su; ci_members = []; ci_alignof = None; ci_sizeof = None } |
---|
| 372 | |
---|
| 373 | let composite_info_def env su m = |
---|
| 374 | { ci_kind = su; ci_members = m; |
---|
| 375 | ci_alignof = alignof_struct_union env m; |
---|
| 376 | ci_sizeof = |
---|
| 377 | match su with |
---|
| 378 | | Struct -> sizeof_struct env m |
---|
| 379 | | Union -> sizeof_union env m } |
---|
| 380 | |
---|
| 381 | (* Type of a function definition *) |
---|
| 382 | |
---|
| 383 | let fundef_typ fd = |
---|
| 384 | TFun(fd.fd_ret, Some fd.fd_params, fd.fd_vararg, []) |
---|
| 385 | |
---|
| 386 | (* Signedness of integer kinds *) |
---|
| 387 | |
---|
| 388 | let is_signed_ikind = function |
---|
| 389 | | IBool -> false |
---|
| 390 | | IChar -> !config.char_signed |
---|
| 391 | | ISChar -> true |
---|
| 392 | | IUChar -> false |
---|
| 393 | | IInt -> true |
---|
| 394 | | IUInt -> false |
---|
| 395 | | IShort -> true |
---|
| 396 | | IUShort -> false |
---|
| 397 | | ILong -> true |
---|
| 398 | | IULong -> false |
---|
| 399 | | ILongLong -> true |
---|
| 400 | | IULongLong -> false |
---|
| 401 | |
---|
| 402 | (* Conversion to unsigned ikind *) |
---|
| 403 | |
---|
| 404 | let unsigned_ikind_of = function |
---|
| 405 | | IBool -> IBool |
---|
| 406 | | IChar | ISChar | IUChar -> IUChar |
---|
| 407 | | IInt | IUInt -> IUInt |
---|
| 408 | | IShort | IUShort -> IUShort |
---|
| 409 | | ILong | IULong -> IULong |
---|
| 410 | | ILongLong | IULongLong -> IULongLong |
---|
| 411 | |
---|
| 412 | (* Some classification functions over types *) |
---|
| 413 | |
---|
| 414 | let is_void_type env t = |
---|
| 415 | match unroll env t with |
---|
| 416 | | TVoid _ -> true |
---|
| 417 | | _ -> false |
---|
| 418 | |
---|
| 419 | let is_integer_type env t = |
---|
| 420 | match unroll env t with |
---|
| 421 | | TInt(_, _) -> true |
---|
| 422 | | _ -> false |
---|
| 423 | |
---|
| 424 | let is_arith_type env t = |
---|
| 425 | match unroll env t with |
---|
| 426 | | TInt(_, _) -> true |
---|
| 427 | | TFloat(_, _) -> true |
---|
| 428 | | _ -> false |
---|
| 429 | |
---|
| 430 | let is_pointer_type env t = |
---|
| 431 | match unroll env t with |
---|
| 432 | | TPtr _ -> true |
---|
| 433 | | _ -> false |
---|
| 434 | |
---|
| 435 | let is_scalar_type env t = |
---|
| 436 | match unroll env t with |
---|
| 437 | | TInt(_, _) -> true |
---|
| 438 | | TFloat(_, _) -> true |
---|
| 439 | | TPtr _ -> true |
---|
| 440 | | TArray _ -> true (* assume implicit decay *) |
---|
| 441 | | TFun _ -> true (* assume implicit decay *) |
---|
| 442 | | _ -> false |
---|
| 443 | |
---|
| 444 | let is_composite_type env t = |
---|
| 445 | match unroll env t with |
---|
| 446 | | TStruct _ | TUnion _ -> true |
---|
| 447 | | _ -> false |
---|
| 448 | |
---|
| 449 | let is_function_type env t = |
---|
| 450 | match unroll env t with |
---|
| 451 | | TFun _ -> true |
---|
| 452 | | _ -> false |
---|
| 453 | |
---|
| 454 | (* Ranking of integer kinds *) |
---|
| 455 | |
---|
| 456 | let integer_rank = function |
---|
| 457 | | IBool -> 1 |
---|
| 458 | | IChar | ISChar | IUChar -> 2 |
---|
| 459 | | IShort | IUShort -> 3 |
---|
| 460 | | IInt | IUInt -> 4 |
---|
| 461 | | ILong | IULong -> 5 |
---|
| 462 | | ILongLong | IULongLong -> 6 |
---|
| 463 | |
---|
| 464 | (* Ranking of float kinds *) |
---|
| 465 | |
---|
| 466 | let float_rank = function |
---|
| 467 | | FFloat -> 1 |
---|
| 468 | | FDouble -> 2 |
---|
| 469 | | FLongDouble -> 3 |
---|
| 470 | |
---|
| 471 | (* Array and function types "decay" to pointer types in many cases *) |
---|
| 472 | |
---|
| 473 | let pointer_decay env t = |
---|
| 474 | match unroll env t with |
---|
| 475 | | TArray(ty, _, _) -> TPtr(ty, []) |
---|
| 476 | | TFun _ as ty -> TPtr(ty, []) |
---|
| 477 | | t -> t |
---|
| 478 | |
---|
| 479 | (* The usual unary conversions (H&S 6.3.3) *) |
---|
| 480 | |
---|
| 481 | let unary_conversion env t = |
---|
| 482 | match unroll env t with |
---|
| 483 | (* Promotion of small integer types *) |
---|
| 484 | | TInt(kind, attr) -> |
---|
| 485 | begin match kind with |
---|
| 486 | | IBool | IChar | ISChar | IUChar | IShort | IUShort -> |
---|
| 487 | TInt(IInt, attr) |
---|
| 488 | | IInt | IUInt | ILong | IULong | ILongLong | IULongLong -> |
---|
| 489 | TInt(kind, attr) |
---|
| 490 | end |
---|
| 491 | (* Arrays and functions decay automatically to pointers *) |
---|
| 492 | | TArray(ty, _, _) -> TPtr(ty, []) |
---|
| 493 | | TFun _ as ty -> TPtr(ty, []) |
---|
| 494 | (* Other types are not changed *) |
---|
| 495 | | t -> t |
---|
| 496 | |
---|
| 497 | (* The usual binary conversions (H&S 6.3.4). |
---|
| 498 | Applies only to arithmetic types. |
---|
| 499 | Return the type to which both sides are to be converted. *) |
---|
| 500 | |
---|
| 501 | let binary_conversion env t1 t2 = |
---|
| 502 | let t1 = unary_conversion env t1 in |
---|
| 503 | let t2 = unary_conversion env t2 in |
---|
| 504 | match unroll env t1, unroll env t2 with |
---|
| 505 | | TFloat(FLongDouble, _), (TInt _ | TFloat _) -> t1 |
---|
| 506 | | (TInt _ | TFloat _), TFloat(FLongDouble, _) -> t2 |
---|
| 507 | | TFloat(FDouble, _), (TInt _ | TFloat _) -> t1 |
---|
| 508 | | (TInt _ | TFloat _), TFloat(FDouble, _) -> t2 |
---|
| 509 | | TFloat(FFloat, _), (TInt _ | TFloat _) -> t1 |
---|
| 510 | | (TInt _), TFloat(FFloat, _) -> t2 |
---|
| 511 | | TInt(k1, _), TInt(k2, _) -> |
---|
| 512 | if k1 = k2 then t1 else begin |
---|
| 513 | match is_signed_ikind k1, is_signed_ikind k2 with |
---|
| 514 | | true, true | false, false -> |
---|
| 515 | (* take the bigger of the two types *) |
---|
| 516 | if integer_rank k1 >= integer_rank k2 then t1 else t2 |
---|
| 517 | | false, true -> |
---|
| 518 | (* if rank (unsigned type) >= rank (signed type), |
---|
| 519 | take the unsigned type *) |
---|
| 520 | if integer_rank k1 >= integer_rank k2 then t1 |
---|
| 521 | (* if rank (unsigned type) < rank (signed type) |
---|
| 522 | and all values of the unsigned type can be represented |
---|
| 523 | in the signed type, take the signed type *) |
---|
| 524 | else if sizeof_ikind k2 > sizeof_ikind k1 then t2 |
---|
| 525 | (* if rank (unsigned type) < rank (signed type) |
---|
| 526 | and some values of the unsigned type cannot be represented |
---|
| 527 | in the signed type, |
---|
| 528 | take the unsigned type corresponding to the signed type *) |
---|
| 529 | else TInt(unsigned_ikind_of k2, []) |
---|
| 530 | | true, false -> |
---|
| 531 | if integer_rank k2 >= integer_rank k1 then t2 |
---|
| 532 | else if sizeof_ikind k1 > sizeof_ikind k2 then t1 |
---|
| 533 | else TInt(unsigned_ikind_of k1, []) |
---|
| 534 | end |
---|
| 535 | | _, _ -> assert false |
---|
| 536 | |
---|
| 537 | (* Conversion on function arguments (with protoypes) *) |
---|
| 538 | |
---|
| 539 | let argument_conversion env t = |
---|
| 540 | (* Arrays and functions degrade automatically to pointers *) |
---|
| 541 | (* Other types are not changed *) |
---|
| 542 | match unroll env t with |
---|
| 543 | | TArray(ty, _, _) -> TPtr(ty, []) |
---|
| 544 | | TFun _ as ty -> TPtr(ty, []) |
---|
| 545 | | _ -> t (* preserve typedefs *) |
---|
| 546 | |
---|
| 547 | (* Conversion on function arguments (old-style unprototyped, or vararg *) |
---|
| 548 | (* H&S 6.3.5 *) |
---|
| 549 | |
---|
| 550 | let default_argument_conversion env t = |
---|
| 551 | match unary_conversion env t with |
---|
| 552 | | TFloat(FFloat, attr) -> TFloat(FDouble, attr) |
---|
| 553 | | t' -> t' |
---|
| 554 | |
---|
| 555 | (** Is the type Tptr(ty, a) appropriate for pointer arithmetic? *) |
---|
| 556 | |
---|
| 557 | let pointer_arithmetic_ok env ty = |
---|
| 558 | match unroll env ty with |
---|
| 559 | | TVoid _ | TFun _ -> false |
---|
| 560 | | _ -> not (incomplete_type env ty) |
---|
| 561 | |
---|
| 562 | (** Special types *) |
---|
| 563 | |
---|
| 564 | let find_matching_unsigned_ikind sz = |
---|
| 565 | if sz = !config.sizeof_int then IUInt |
---|
| 566 | else if sz = !config.sizeof_long then IULong |
---|
| 567 | else if sz = !config.sizeof_longlong then IULongLong |
---|
| 568 | else assert false |
---|
| 569 | |
---|
| 570 | let find_matching_signed_ikind sz = |
---|
| 571 | if sz = !config.sizeof_int then IInt |
---|
| 572 | else if sz = !config.sizeof_long then ILong |
---|
| 573 | else if sz = !config.sizeof_longlong then ILongLong |
---|
| 574 | else assert false |
---|
| 575 | |
---|
| 576 | let wchar_ikind = find_matching_unsigned_ikind !config.sizeof_wchar |
---|
| 577 | let size_t_ikind = find_matching_unsigned_ikind !config.sizeof_size_t |
---|
| 578 | let ptr_t_ikind = find_matching_unsigned_ikind !config.sizeof_ptr |
---|
| 579 | let ptrdiff_t_ikind = find_matching_signed_ikind !config.sizeof_ptrdiff_t |
---|
| 580 | let enum_ikind = IInt |
---|
| 581 | |
---|
| 582 | (** The type of a constant *) |
---|
| 583 | |
---|
| 584 | let type_of_constant = function |
---|
| 585 | | CInt(_, ik, _) -> TInt(ik, []) |
---|
| 586 | | CFloat(_, fk, _) -> TFloat(fk, []) |
---|
| 587 | | CStr _ -> TPtr(TInt(IChar, []), []) (* XXX or array? const? *) |
---|
| 588 | | CWStr _ -> TPtr(TInt(wchar_ikind, []), []) (* XXX or array? const? *) |
---|
| 589 | | CEnum(_, _) -> TInt(IInt, []) |
---|
| 590 | |
---|
| 591 | (* Check that a C expression is a lvalue *) |
---|
| 592 | |
---|
| 593 | let rec is_lvalue env e = |
---|
| 594 | (* Type must not be array or function *) |
---|
| 595 | match unroll env e.etyp with |
---|
| 596 | | TFun _ | TArray _ -> false |
---|
| 597 | | _ -> |
---|
| 598 | match e.edesc with |
---|
| 599 | | EVar id -> true |
---|
| 600 | | EUnop((Oderef | Oarrow _), _) -> true |
---|
| 601 | | EUnop(Odot _, e') -> is_lvalue env e' |
---|
| 602 | | EBinop(Oindex, _, _, _) -> true |
---|
| 603 | | _ -> false |
---|
| 604 | |
---|
| 605 | (* Check that a C expression is the literal "0", which can be used |
---|
| 606 | as a pointer. *) |
---|
| 607 | |
---|
| 608 | let is_literal_0 e = |
---|
| 609 | match e.edesc with |
---|
| 610 | | EConst(CInt(0L, _, _)) -> true |
---|
| 611 | | _ -> false |
---|
| 612 | |
---|
| 613 | (* Check that an assignment is allowed *) |
---|
| 614 | |
---|
| 615 | let valid_assignment env from tto = |
---|
| 616 | match pointer_decay env from.etyp, pointer_decay env tto with |
---|
| 617 | | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true |
---|
| 618 | | TInt _, TPtr _ -> is_literal_0 from |
---|
| 619 | | TPtr(ty, _), TPtr(ty', _) -> |
---|
| 620 | incl_attributes (attributes_of_type env ty) (attributes_of_type env ty') |
---|
| 621 | && (is_void_type env ty || is_void_type env ty' |
---|
| 622 | || compatible_types env |
---|
| 623 | (erase_attributes_type env ty) |
---|
| 624 | (erase_attributes_type env ty')) |
---|
| 625 | | TStruct(s, _), TStruct(s', _) -> s = s' |
---|
| 626 | | TUnion(s, _), TUnion(s', _) -> s = s' |
---|
| 627 | | _, _ -> false |
---|
| 628 | |
---|
| 629 | (* Check that a cast is allowed *) |
---|
| 630 | |
---|
| 631 | let valid_cast env tfrom tto = |
---|
| 632 | compatible_types ~noattrs:true env tfrom tto || |
---|
| 633 | begin match unroll env tfrom, unroll env tto with |
---|
| 634 | | _, TVoid _ -> true |
---|
| 635 | (* from any int-or-pointer (with array and functions decaying to pointers) |
---|
| 636 | to any int-or-pointer *) |
---|
| 637 | | (TInt _ | TPtr _ | TArray _ | TFun _), (TInt _ | TPtr _) -> true |
---|
| 638 | (* between int and float types *) |
---|
| 639 | | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true |
---|
| 640 | | _, _ -> false |
---|
| 641 | end |
---|
| 642 | |
---|
| 643 | (* Construct an integer constant *) |
---|
| 644 | |
---|
| 645 | let intconst v ik = |
---|
| 646 | { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) } |
---|
| 647 | |
---|
| 648 | (* Construct a float constant *) |
---|
| 649 | |
---|
| 650 | let floatconst v fk = |
---|
| 651 | { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []) } |
---|
| 652 | |
---|
| 653 | (* Construct the literal "0" with void * type *) |
---|
| 654 | |
---|
| 655 | let nullconst = |
---|
| 656 | { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) } |
---|
| 657 | |
---|
| 658 | (* Construct a sequence *) |
---|
| 659 | |
---|
| 660 | let sseq loc s1 s2 = |
---|
| 661 | match s1.sdesc, s2.sdesc with |
---|
| 662 | | Sskip, _ -> s2 |
---|
| 663 | | _, Sskip -> s1 |
---|
| 664 | | _, Sblock sl -> { sdesc = Sblock(s1 :: sl); sloc = loc } |
---|
| 665 | | _, _ -> { sdesc = Sseq(s1, s2); sloc = loc } |
---|
| 666 | |
---|
| 667 | (* Construct an assignment statement *) |
---|
| 668 | |
---|
| 669 | let sassign loc lv rv = |
---|
| 670 | { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp}; |
---|
| 671 | sloc = loc } |
---|
| 672 | |
---|
| 673 | (* Empty location *) |
---|
| 674 | |
---|
| 675 | let no_loc = ("", -1) |
---|
| 676 | |
---|
| 677 | (* Dummy skip statement *) |
---|
| 678 | |
---|
| 679 | let sskip = { sdesc = Sskip; sloc = no_loc } |
---|
| 680 | |
---|
| 681 | (* Print a location *) |
---|
| 682 | |
---|
| 683 | let printloc oc (filename, lineno) = |
---|
| 684 | if filename <> "" then Printf.fprintf oc "%s:%d: " filename lineno |
---|
| 685 | |
---|
| 686 | (* Format a location *) |
---|
| 687 | |
---|
| 688 | let formatloc pp (filename, lineno) = |
---|
| 689 | if filename <> "" then Format.fprintf pp "%s:%d: " filename lineno |
---|
| 690 | |
---|
| 691 | |
---|