diff options
-rw-r--r-- | cfrontend/C2C.ml | 4 | ||||
-rw-r--r-- | cparser/Ceval.ml | 2 | ||||
-rw-r--r-- | cparser/Cutil.ml | 32 | ||||
-rw-r--r-- | cparser/Cutil.mli | 12 | ||||
-rw-r--r-- | cparser/Elab.ml | 16 | ||||
-rw-r--r-- | cparser/GCC.ml | 46 | ||||
-rw-r--r-- | cparser/Machine.ml | 42 | ||||
-rw-r--r-- | cparser/PackedStructs.ml | 2 |
8 files changed, 88 insertions, 68 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 584c265a..fddbfd30 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -137,8 +137,8 @@ let builtins_generic = { (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [AConst], []); - TInt(Cutil.size_t_ikind, []); - TInt(Cutil.size_t_ikind, [])], + TInt(IUInt, []); + TInt(IUInt, [])], false); (* Annotations *) "__builtin_annot", diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml index 39cda58c..ba7cdabc 100644 --- a/cparser/Ceval.ml +++ b/cparser/Ceval.ml @@ -102,7 +102,7 @@ let cast env ty_to ty_from v = then v else raise Notconst | TPtr(ty, _), I n -> - I (normalize_int n ptr_t_ikind) + I (normalize_int n (ptr_t_ikind ())) | TPtr(ty, _), (S _ | WS _) -> v | TEnum(_, _), I n -> diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 9093b230..9e7f102e 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -707,41 +707,34 @@ let type_of_member env fld = (** Special types *) let find_matching_unsigned_ikind sz = + assert (sz > 0); if sz = !config.sizeof_int then IUInt else if sz = !config.sizeof_long then IULong else if sz = !config.sizeof_longlong then IULongLong else assert false let find_matching_signed_ikind sz = + assert (sz > 0); if sz = !config.sizeof_int then IInt else if sz = !config.sizeof_long then ILong else if sz = !config.sizeof_longlong then ILongLong else assert false -let wchar_ikind = +let wchar_ikind () = if !config.wchar_signed then find_matching_signed_ikind !config.sizeof_wchar else find_matching_unsigned_ikind !config.sizeof_wchar -let size_t_ikind = find_matching_unsigned_ikind !config.sizeof_size_t -let ptr_t_ikind = find_matching_unsigned_ikind !config.sizeof_ptr -let ptrdiff_t_ikind = find_matching_signed_ikind !config.sizeof_ptrdiff_t - -(** The wchar_t type. Try to get it from a typedef in the environment, - otherwise use the integer type described in !config. *) - -let wchar_type env = - try - let (id, def) = Env.lookup_typedef env "wchar_t" in TNamed(id, []) - with Env.Error _ -> - TInt(wchar_ikind, []) +let size_t_ikind () = find_matching_unsigned_ikind !config.sizeof_size_t +let ptr_t_ikind () = find_matching_unsigned_ikind !config.sizeof_ptr +let ptrdiff_t_ikind () = find_matching_signed_ikind !config.sizeof_ptrdiff_t (** The type of a constant *) -let type_of_constant env = function +let type_of_constant = function | CInt(_, ik, _) -> TInt(ik, []) | CFloat(_, fk) -> TFloat(fk, []) | CStr _ -> TPtr(TInt(IChar, []), []) - | CWStr _ -> TPtr(wchar_type env, []) + | CWStr _ -> TPtr(TInt(wchar_ikind(), []), []) | CEnum(_, _) -> TInt(IInt, []) (* Check that a C expression is a lvalue *) @@ -829,15 +822,14 @@ let floatconst0 = { edesc = EConst(CFloat({hex=false; intPart="0"; fracPart="0"; exp="0"}, FDouble)); etyp = TFloat(FDouble, []) } -(* Construct the literal "0" with void * type *) - -let nullconst = - { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) } - (* Construct a cast expression *) let ecast ty e = { edesc = ECast(ty, e); etyp = ty } +(* Construct the literal "0" with void * type *) + +let nullconst = ecast (TPtr(TVoid [], [])) (intconst 0L IInt) + (* Construct an assignment expression *) let eassign e1 e2 = { edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp } diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 53bcfcea..bd52badf 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -156,20 +156,20 @@ val default_argument_conversion : Env.t -> typ -> typ (* Special types *) val enum_ikind : ikind (* Integer kind for enum values. Always [IInt]. *) -val wchar_ikind : ikind - (* Integer kind for wchar_t type. Unsigned. *) -val size_t_ikind : ikind +val wchar_ikind : unit -> ikind + (* Integer kind for wchar_t type. *) +val size_t_ikind : unit -> ikind (* Integer kind for size_t type. Unsigned. *) -val ptr_t_ikind : ikind +val ptr_t_ikind : unit -> ikind (* Integer kind for ptr_t type. Smallest unsigned kind large enough to contain a pointer without information loss. *) -val ptrdiff_t_ikind : ikind +val ptrdiff_t_ikind : unit -> ikind (* Integer kind for ptrdiff_t type. Smallest signed kind large enough to contain the difference between two pointers. *) (* Helpers for type-checking *) -val type_of_constant : Env.t -> constant -> typ +val type_of_constant : constant -> typ (* Return the type of the given constant. *) val type_of_member : Env.t -> field -> typ (* Return the type of accessing the given field [fld]. diff --git a/cparser/Elab.ml b/cparser/Elab.ml index faffc36f..bad92cf6 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1198,7 +1198,7 @@ let elab_expr loc env a = | CONSTANT cst -> let cst' = elab_constant loc cst in - { edesc = EConst cst'; etyp = type_of_constant env cst' } + { edesc = EConst cst'; etyp = type_of_constant cst' } (* 6.5.2 Postfix expressions *) @@ -1339,31 +1339,31 @@ let elab_expr loc env a = match b1.edesc with | EConst(CStr s) -> let sz = String.length s + 1 in - EConst(CInt(Int64.of_int sz, size_t_ikind, "")) + EConst(CInt(Int64.of_int sz, size_t_ikind(), "")) | EConst(CWStr s) -> let sz = (!config).sizeof_wchar * (List.length s + 1) in - EConst(CInt(Int64.of_int sz, size_t_ikind, "")) + EConst(CInt(Int64.of_int sz, size_t_ikind(), "")) | _ -> ESizeof b1.etyp in - { edesc = bdesc; etyp = TInt(size_t_ikind, []) } + { edesc = bdesc; etyp = TInt(size_t_ikind(), []) } | TYPE_SIZEOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then err "incomplete type %a" Cprint.typ ty; - { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []) } + { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) } | EXPR_ALIGNOF a1 -> let b1 = elab a1 in if wrap incomplete_type loc env b1.etyp then err "incomplete type %a" Cprint.typ b1.etyp; - { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind, []) } + { edesc = EAlignof b1.etyp; etyp = TInt(size_t_ikind(), []) } | TYPE_ALIGNOF (spec, dcl) -> let (ty, env') = elab_type loc env spec dcl in if wrap incomplete_type loc env' ty then err "incomplete type %a" Cprint.typ ty; - { edesc = EAlignof ty; etyp = TInt(size_t_ikind, []) } + { edesc = EAlignof ty; etyp = TInt(size_t_ikind(), []) } | UNARY(PLUS, a1) -> let b1 = elab a1 in @@ -1465,7 +1465,7 @@ let elab_expr loc env a = err "illegal pointer arithmetic in binary '-'"; if wrap sizeof loc env ty1 = Some 0 then err "subtraction between two pointers to zero-sized objects"; - (TPtr(ty1, []), TInt(ptrdiff_t_ikind, [])) + (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), [])) | _, _ -> error "type error in binary '-'" end in { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres } diff --git a/cparser/GCC.ml b/cparser/GCC.ml index 1bcbbbc8..030f300b 100644 --- a/cparser/GCC.ml +++ b/cparser/GCC.ml @@ -35,7 +35,7 @@ let voidConstPtrType = TPtr(TVoid [AConst], []) let charPtrType = TPtr(TInt(IChar, []), []) let charConstPtrType = TPtr(TInt(IChar, [AConst]), []) let intPtrType = TPtr(TInt(IInt, []), []) -let sizeType = TInt(size_t_ikind, []) +let sizeType() = TInt(size_t_ikind(), []) let builtins = { Builtins.typedefs = [ @@ -43,22 +43,22 @@ let builtins = { ]; Builtins.functions = [ "__builtin___fprintf_chk", (intType, [ voidPtrType; intType; charConstPtrType ], true) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *); - "__builtin___memcpy_chk", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false); - "__builtin___memmove_chk", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false); - "__builtin___mempcpy_chk", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false); - "__builtin___memset_chk", (voidPtrType, [ voidPtrType; intType; sizeType; sizeType ], false); + "__builtin___memcpy_chk", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false); + "__builtin___memmove_chk", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false); + "__builtin___mempcpy_chk", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false); + "__builtin___memset_chk", (voidPtrType, [ voidPtrType; intType; sizeType(); sizeType() ], false); "__builtin___printf_chk", (intType, [ intType; charConstPtrType ], true); - "__builtin___snprintf_chk", (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType ], true); - "__builtin___sprintf_chk", (intType, [ charPtrType; intType; sizeType; charConstPtrType ], true); - "__builtin___stpcpy_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false); - "__builtin___strcat_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false); - "__builtin___strcpy_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false); - "__builtin___strncat_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false); - "__builtin___strncpy_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false); + "__builtin___snprintf_chk", (intType, [ charPtrType; sizeType(); intType; sizeType(); charConstPtrType ], true); + "__builtin___sprintf_chk", (intType, [ charPtrType; intType; sizeType(); charConstPtrType ], true); + "__builtin___stpcpy_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false); + "__builtin___strcat_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false); + "__builtin___strcpy_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false); + "__builtin___strncat_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType(); sizeType() ], false); + "__builtin___strncpy_chk", (charPtrType, [ charPtrType; charConstPtrType; sizeType(); sizeType() ], false); "__builtin___vfprintf_chk", (intType, [ voidPtrType; intType; charConstPtrType; voidPtrType ], false) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *); "__builtin___vprintf_chk", (intType, [ intType; charConstPtrType; voidPtrType ], false); - "__builtin___vsnprintf_chk", (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType; voidPtrType ], false); - "__builtin___vsprintf_chk", (intType, [ charPtrType; intType; sizeType; charConstPtrType; voidPtrType ], false); + "__builtin___vsnprintf_chk", (intType, [ charPtrType; sizeType(); intType; sizeType(); charConstPtrType; voidPtrType ], false); + "__builtin___vsprintf_chk", (intType, [ charPtrType; intType; sizeType(); charConstPtrType; voidPtrType ], false); "__builtin_acos", (doubleType, [ doubleType ], false); "__builtin_acosf", (floatType, [ floatType ], false); @@ -124,8 +124,8 @@ let builtins = { "__builtin_inf", (doubleType, [], false); "__builtin_inff", (floatType, [], false); "__builtin_infl", (longDoubleType, [], false); - "__builtin_memcpy", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false); - "__builtin_mempcpy", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false); + "__builtin_memcpy", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType() ], false); + "__builtin_mempcpy", (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType() ], false); "__builtin_fmod", (doubleType, [ doubleType ], false); "__builtin_fmodf", (floatType, [ floatType ], false); @@ -162,7 +162,7 @@ let builtins = { "__builtin_nansf", (floatType, [ charConstPtrType ], false); "__builtin_nansl", (longDoubleType, [ charConstPtrType ], false); "__builtin_next_arg", (voidPtrType, [], false); - "__builtin_object_size", (sizeType, [ voidPtrType; intType ], false); + "__builtin_object_size", (sizeType(), [ voidPtrType; intType ], false); "__builtin_parity", (intType, [ uintType ], false); "__builtin_parityl", (intType, [ ulongType ], false); @@ -196,9 +196,9 @@ let builtins = { "__builtin_strcmp", (intType, [ charConstPtrType; charConstPtrType ], false); "__builtin_strcpy", (charPtrType, [ charPtrType; charConstPtrType ], false); "__builtin_strcspn", (uintType, [ charConstPtrType; charConstPtrType ], false); - "__builtin_strncat", (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false); - "__builtin_strncmp", (intType, [ charConstPtrType; charConstPtrType; sizeType ], false); - "__builtin_strncpy", (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false); + "__builtin_strncat", (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false); + "__builtin_strncmp", (intType, [ charConstPtrType; charConstPtrType; sizeType() ], false); + "__builtin_strncpy", (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false); "__builtin_strspn", (intType, [ charConstPtrType; charConstPtrType ], false); "__builtin_strpbrk", (charPtrType, [ charConstPtrType; charConstPtrType ], false); "__builtin_tan", (doubleType, [ doubleType ], false); @@ -217,9 +217,7 @@ let builtins = { "__builtin_va_start", (voidType, [ voidPtrType; voidPtrType ], false); "__builtin_stdarg_start", (voidType, [ voidPtrType ], false); (* When we parse builtin_va_arg, type argument becomes sizeof type *) - "__builtin_va_arg", (voidType, [ voidPtrType; sizeType ], false); - "__builtin_va_copy", (voidType, [ voidPtrType; - voidPtrType ], - false) + "__builtin_va_arg", (voidType, [ voidPtrType; sizeType() ], false); + "__builtin_va_copy", (voidType, [ voidPtrType; voidPtrType ], false) ] } diff --git a/cparser/Machine.ml b/cparser/Machine.ml index 6a7f5054..b215505b 100644 --- a/cparser/Machine.ml +++ b/cparser/Machine.ml @@ -173,10 +173,40 @@ let gcc_extensions c = { c with sizeof_void = Some 1; sizeof_fun = Some 1; alignof_void = Some 1; alignof_fun = Some 1 } -(* Default configuration *) +(* Undefined configuration *) -let config = - ref (match Sys.word_size with - | 32 -> if Sys.os_type = "Win32" then win32 else ilp32ll64 - | 64 -> if Sys.os_type = "Win32" then win64 else i32lpll64 - | _ -> assert false) +let undef = { + name = "UNDEFINED"; + char_signed = false; + sizeof_ptr = 0; + sizeof_short = 0; + sizeof_int = 0; + sizeof_long = 0; + sizeof_longlong = 0; + sizeof_float = 0; + sizeof_double = 0; + sizeof_longdouble = 0; + sizeof_void = None; + sizeof_fun = None; + sizeof_wchar = 0; + wchar_signed = true; + sizeof_size_t = 0; + sizeof_ptrdiff_t = 0; + alignof_ptr = 0; + alignof_short = 0; + alignof_int = 0; + alignof_long = 0; + alignof_longlong = 0; + alignof_float = 0; + alignof_double = 0; + alignof_longdouble = 0; + alignof_void = None; + alignof_fun = None; + bigendian = false; + bitfields_msb_first = false; + struct_return_as_int = 0 +} + +(* The current configuration. Must be initialized before use. *) + +let config = ref undef diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml index 686a7d39..1f602fc1 100644 --- a/cparser/PackedStructs.ml +++ b/cparser/PackedStructs.ml @@ -138,7 +138,7 @@ let accessor_type loc env ty = match unroll env ty with | TInt(ik,_) -> (8 * sizeof_ikind ik, TInt(unsigned_ikind_of ik,[])) | TEnum(_,_) -> (8 * sizeof_ikind enum_ikind, TInt(unsigned_ikind_of enum_ikind,[])) - | TPtr _ -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind,[])) + | TPtr _ -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind(),[])) | _ -> error "%a: unsupported type for byte-swapped field access" formatloc loc; (32, TVoid []) |