diff --git a/src/kernel_internals/runtime/machdeps.ml b/src/kernel_internals/runtime/machdeps.ml index 3c9da30d57534a6e73ebe343faebe911a21929a6..e0600a7d1a86c11d91df32dc7b6a85bba75c8e02 100644 --- a/src/kernel_internals/runtime/machdeps.ml +++ b/src/kernel_internals/runtime/machdeps.ml @@ -56,7 +56,7 @@ let x86_16 = { sizeof_float = 4; sizeof_double = 8; sizeof_longdouble = 16; - sizeof_void = 1; + sizeof_void = -1; sizeof_fun = -1; size_t = "unsigned int"; wchar_t = "int"; @@ -83,7 +83,7 @@ let x86_16 = { let gcc_x86_16 = { x86_16 with compiler = "gcc"; - sizeof_fun = 1; alignof_fun = 1; + sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1; } let x86_32 = { @@ -98,7 +98,7 @@ let x86_32 = { sizeof_float = 4; sizeof_double = 8; sizeof_longdouble = 12; - sizeof_void = 1; + sizeof_void = -1; sizeof_fun = -1; size_t = "unsigned int"; wchar_t = "int"; @@ -123,7 +123,7 @@ let x86_32 = { let gcc_x86_32 = { x86_32 with compiler = "gcc"; - sizeof_fun = 1; alignof_fun = 1; + sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1; } let x86_64 = { @@ -138,7 +138,7 @@ let x86_64 = { sizeof_float = 4; sizeof_double = 8; sizeof_longdouble = 16; - sizeof_void = 1; + sizeof_void = -1; sizeof_fun = -1; size_t = "unsigned long"; wchar_t = "int"; @@ -163,7 +163,7 @@ let x86_64 = { let gcc_x86_64 = { x86_64 with compiler = "gcc"; - sizeof_fun = 1; alignof_fun = 1; + sizeof_void = 1; sizeof_fun = 1; alignof_fun = 1; } let ppc_32 = { diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index abef0cd1e877e52d087bb3309d2412a71142397f..c3a8e705137c062ef5eecc69a34f5eb13eb21ad6 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1336,6 +1336,15 @@ let canDropStatement (s: stmt) : bool = ignore (visitCilStmt vis s); !pRes +let fail_if_incompatible_sizeof ~ensure_complete op typ = + if Cil.isFunctionType typ && Cil.theMachine.theMachine.sizeof_fun < 0 then + Kernel.error ~current:true "%s called on function only allowed for GCC" op; + let is_void = Cil.isVoidType typ in + if is_void && Cil.theMachine.theMachine.sizeof_void < 0 then + Kernel.error ~current:true "%s on void type only allowed for GCC/MSVC" op; + if ensure_complete && not (Cil.isCompleteType typ) && not is_void then + Kernel.error ~current:true + "%s on incomplete type '%a'" op Cil_printer.pp_typ typ (******** CASTS *********) @@ -6022,14 +6031,8 @@ and doExp local_env | A.TYPE_SIZEOF (bt, dt) -> let typ = doOnlyType local_env.is_ghost bt dt in - let res = - if Cil.isCompleteType typ then new_exp ~loc (SizeOf typ) - else begin - Kernel.error ~once:true ~current:true - "sizeof on incomplete type '%a'" Cil_printer.pp_typ typ; - new_exp ~loc (Const (CStr ("booo sizeof(incomplete)"))) - end - in + fail_if_incompatible_sizeof ~ensure_complete:true "sizeof" typ; + let res = new_exp ~loc (SizeOf typ) in finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf | A.EXPR_SIZEOF e -> @@ -6038,9 +6041,7 @@ and doExp local_env let (_, se, e', lvt) = doExp (no_paren_local_env local_env) CNoConst e AExpLeaveArrayFun in - if Cil.isFunctionType lvt && Cil.theMachine.theMachine.sizeof_fun < 0 then - Kernel.abort ~current:true - "sizeof() called on function"; + fail_if_incompatible_sizeof ~ensure_complete:false "sizeof()" lvt; let scope_chunk = drop_chunk "sizeof" se e e' in let size = match e'.enode with @@ -6057,16 +6058,15 @@ and doExp local_env | A.TYPE_ALIGNOF (bt, dt) -> let typ = doOnlyType local_env.is_ghost bt dt in - finishExp [] (unspecified_chunk empty) (new_exp ~loc (AlignOf(typ))) - theMachine.typeOfSizeOf + fail_if_incompatible_sizeof ~ensure_complete:true "alignof" typ; + let res = new_exp ~loc (AlignOf typ) in + finishExp [] (unspecified_chunk empty) res theMachine.typeOfSizeOf | A.EXPR_ALIGNOF e -> let (_, se, e', lvt) = doExp (no_paren_local_env local_env) CNoConst e AExpLeaveArrayFun in - if Cil.isFunctionType lvt && Cil.theMachine.theMachine.alignof_fun < 0 - then - Kernel.abort ~current:true "alignof() called on a function."; + fail_if_incompatible_sizeof ~ensure_complete:false "alignof()" lvt; let scope_chunk = drop_chunk "alignof" se e e' in let e'' = match e'.enode with (* If we are taking the alignof an diff --git a/src/kernel_services/abstract_interp/base.ml b/src/kernel_services/abstract_interp/base.ml index 0c7e3ba7eeca445689d0faa9b82e4ac3955e2788..22e566fe3b5226f1f86be4dcabb8ec69c0ebf17f 100644 --- a/src/kernel_services/abstract_interp/base.ml +++ b/src/kernel_services/abstract_interp/base.ml @@ -349,13 +349,15 @@ let is_aligned_by b alignment = if Int.is_zero alignment then false else - match b with - | Var (v,_) | Allocated(v,_,_) -> - Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf v.vtype)) alignment) - | CLogic_Var (_, ty, _) -> - Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf ty)) alignment) - | Null -> true - | String _ -> Int.is_one alignment + try + match b with + | Var (v,_) | Allocated(v,_,_) -> + Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf v.vtype)) alignment) + | CLogic_Var (_, ty, _) -> + Int.is_zero (Int.e_rem (Int.of_int (Cil.bytesAlignOf ty)) alignment) + | Null -> true + | String _ -> Int.is_one alignment + with Cil.SizeOfError _ -> false let is_any_formal_or_local v = match v with diff --git a/src/kernel_services/analysis/bit_utils.ml b/src/kernel_services/analysis/bit_utils.ml index 5af81b797eb191fe248f54761c7d5580eeead488..05491e1df7a2c74275341269f94c4385630e1bbd 100644 --- a/src/kernel_services/analysis/bit_utils.ml +++ b/src/kernel_services/analysis/bit_utils.ml @@ -219,8 +219,11 @@ let rec pretty_bits_internal env bfinfo typ ~align ~start ~stop = | TVoid _ | TBuiltin_va_list _ | TNamed _ | TFun (_, _, _, _) as typ -> let size = match bfinfo with - | Other -> Integer.of_int (bitsSizeOf typ) - | Bitfield i -> Integer.of_int64 i + | Other -> begin + try Integer.of_int (bitsSizeOf typ) + with Cil.SizeOfError _ -> Integer.zero + end + | Bitfield i -> Integer.of_int64 i in (if Integer.is_zero start && Integer.equal size req_size then diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 81f75901401bc71cf31618912dfa25307599e761..23900b640933ece2d12960901d2e8f5bce7b1697 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -4051,7 +4051,11 @@ let rec bytesAlignOf t = | TFun _ when not (msvcMode ()) -> theMachine.theMachine.alignof_fun | TFun _ as t -> raise (SizeOfError ("Undefined sizeof on a function.", t)) - | TVoid _ as t -> raise (SizeOfError ("Undefined sizeof(void).", t)) + | TVoid _ as t -> + if theMachine.theMachine.sizeof_void > 0 then + theMachine.theMachine.sizeof_void + else + raise (SizeOfError ("Undefined sizeof(void).", t)) in process_aligned_attribute ~may_reduce:false (fun fmt -> !pp_typ_ref fmt t) @@ -4409,7 +4413,11 @@ and bitsSizeOf t = sz' (*WAS: addTrailing sz' (8 * bytesAlignOf t)*) | _ -> raise (SizeOfError ("Array with non-constant length.", t)) end) - | TVoid _ -> 8 * theMachine.theMachine.sizeof_void + | TVoid _ -> + if theMachine.theMachine.sizeof_void >= 0 then + 8 * theMachine.theMachine.sizeof_void + else + raise (SizeOfError ("Undefined sizeof(void).", t)) | TFun _ -> if theMachine.theMachine.sizeof_fun >= 0 then 8 * theMachine.theMachine.sizeof_fun @@ -4545,7 +4553,10 @@ and constFold (machdep: bool) (e: exp) : exp = | SizeOfStr s when machdep -> kinteger ~loc theMachine.kindOfSizeOf (1 + String.length s) | AlignOf t when machdep -> - kinteger ~loc theMachine.kindOfSizeOf (bytesAlignOf t) + begin + try kinteger ~loc theMachine.kindOfSizeOf (bytesAlignOf t) + with SizeOfError _ -> e + end | AlignOfE e when machdep -> begin (* The alignment of an expression is not always the alignment of its * type. I know that for strings this is not true *) @@ -5223,7 +5234,11 @@ let rec constFoldTermNodeAtTop = function (try integer_lconstant (bytesSizeOf typ) with SizeOfError _ -> t) | TSizeOfStr str -> integer_lconstant (String.length str + 1) - | TAlignOf typ -> integer_lconstant (bytesAlignOf typ) + | TAlignOf typ as t -> + begin + try integer_lconstant (bytesAlignOf typ) + with SizeOfError _ -> t + end | TSizeOfE { term_type= Ctype typ } -> constFoldTermNodeAtTop (TSizeOf typ) | TAlignOfE { term_type= Ctype typ } -> constFoldTermNodeAtTop (TAlignOf typ) diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index 02f54e2f020e25934ad25cddffb08a467da39b65..2613a70e4cf8cc0f4e924d611b0c57aa3f0ff9f6 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -2183,7 +2183,8 @@ val sizeOf: loc:location -> typ -> exp (** The minimum alignment (in bytes) for a type. This function is * architecture dependent, so you should only call this after you call - * {!Cil.initCIL}. *) + * {!Cil.initCIL}. + * Raises {!SizeOfError} when it cannot compute the alignment. *) val bytesAlignOf: typ -> int (** [intOfAttrparam a] tries to const-fold [a] into a numeric value. diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index 5d1fcf6df5ba8b1b970c07a1839698788108074b..8d5ce416adc74c1837981b6b097af5aed429dc8f 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -272,7 +272,7 @@ let print_machdep fmt (m : Cil_types.mach) = "double", m.sizeof_double, m.alignof_double ; "long double", m.sizeof_longdouble, m.alignof_longdouble ; "pointer", m.sizeof_ptr, m.alignof_ptr ; - "void", m.sizeof_void, 1 ; + "void", m.sizeof_void, m.sizeof_void ; "function", m.sizeof_fun, m.alignof_fun ; ] ; List.iter diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml index ab451611348a7ad2d828eb43eeac5f8de28ae100..4668403ccdd3a40572022f3df66406c9e02ca0e0 100644 --- a/src/plugins/e-acsl/src/analyses/interval.ml +++ b/src/plugins/e-acsl/src/analyses/interval.ml @@ -406,7 +406,9 @@ let infer_sizeof ty = try singleton_of_int (Cil.bytesSizeOf ty) with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf -let infer_alignof ty = singleton_of_int (Cil.bytesAlignOf ty) +let infer_alignof ty = + try singleton_of_int (Cil.bytesAlignOf ty) + with Cil.SizeOfError _ -> interv_of_typ Cil.theMachine.Cil.typeOfSizeOf let rec infer t = let get_cty t = match t.term_type with Ctype ty -> ty | _ -> assert false in diff --git a/tests/constant_propagation/oracle/array_pointers.res.oracle b/tests/constant_propagation/oracle/array_pointers.res.oracle index 13db6ccd08dd6658eb48720410f5beed80842700..fb141388d4db6867146e35d35b88e5b0da06c19d 100644 --- a/tests/constant_propagation/oracle/array_pointers.res.oracle +++ b/tests/constant_propagation/oracle/array_pointers.res.oracle @@ -12,7 +12,7 @@ [eva:final-states] Values at end of function main: q ∈ {{ &p + {4} }} r ∈ {{ &p + {8} }} - s ∈ {1} + s ∈ [--..--] [scf] beginning constant propagation [kernel] tests/constant_propagation/array_pointers.i:10: Warning: using size of 'void' diff --git a/tests/misc/oracle/function_ptr_alignof.res.oracle b/tests/misc/oracle/function_ptr_alignof.res.oracle index b7d7520c167f71b7acb3867d646ea49253ae84a3..7e77e91ce97bcc58d4f6a4336b282e51c09b84d1 100644 --- a/tests/misc/oracle/function_ptr_alignof.res.oracle +++ b/tests/misc/oracle/function_ptr_alignof.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/misc/function_ptr_alignof.i (no preprocessing) [kernel] tests/misc/function_ptr_alignof.i:13: User Error: - alignof() called on a function. + alignof() called on function only allowed for GCC [kernel] User Error: stopping on file "tests/misc/function_ptr_alignof.i" that has errors. [kernel] Frama-C aborted: invalid user input. diff --git a/tests/misc/oracle/function_ptr_sizeof.res.oracle b/tests/misc/oracle/function_ptr_sizeof.res.oracle index bc70a4785cb896cff2b3bae69cb194831acdcab9..689d2ad92fa90c5ef6b31140efaaaa65cee65b6b 100644 --- a/tests/misc/oracle/function_ptr_sizeof.res.oracle +++ b/tests/misc/oracle/function_ptr_sizeof.res.oracle @@ -1,5 +1,5 @@ [kernel] Parsing tests/misc/function_ptr_sizeof.i (no preprocessing) [kernel] tests/misc/function_ptr_sizeof.i:13: User Error: - sizeof() called on function + sizeof() called on function only allowed for GCC [kernel] User Error: stopping on file "tests/misc/function_ptr_sizeof.i" that has errors. [kernel] Frama-C aborted: invalid user input. diff --git a/tests/misc/oracle/print_machdep.res.oracle b/tests/misc/oracle/print_machdep.res.oracle index e0ef03b220dadd48a509cd8d00a25151499d3f9b..7c9a04850ea7f793b0235931ec0b95c651c2cead 100644 --- a/tests/misc/oracle/print_machdep.res.oracle +++ b/tests/misc/oracle/print_machdep.res.oracle @@ -7,7 +7,7 @@ Machine: gcc 4.0.3 AMD64 sizeof double = 8 (64 bits, aligned on 64 bits) sizeof long double = 16 (128 bits, aligned on 128 bits) sizeof pointer = 8 (64 bits, aligned on 64 bits) - sizeof void = 1 (8 bits, aligned on 8 bits) + sizeof void = error (alignof error) sizeof function = error (alignof error) typeof sizeof(T) = unsigned long typeof wchar_t = int diff --git a/tests/syntax/oracle/sizeof_void.0.res.oracle b/tests/syntax/oracle/sizeof_void.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..f4d8b52e9da0396bbc147a9c32e187c15cc803f4 --- /dev/null +++ b/tests/syntax/oracle/sizeof_void.0.res.oracle @@ -0,0 +1,12 @@ +[kernel] Parsing tests/syntax/sizeof_void.c (with preprocessing) +[kernel] tests/syntax/sizeof_void.c:9: User Error: + sizeof on void type only allowed for GCC/MSVC +[kernel] tests/syntax/sizeof_void.c:16: User Error: + sizeof() on void type only allowed for GCC/MSVC +[kernel] tests/syntax/sizeof_void.c:21: User Error: + alignof on void type only allowed for GCC/MSVC +[kernel] tests/syntax/sizeof_void.c:28: User Error: + alignof() on void type only allowed for GCC/MSVC +[kernel] User Error: stopping on file "tests/syntax/sizeof_void.c" that has errors. Add + '-kernel-msg-key pp' for preprocessing command. +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/oracle/sizeof_void.1.res.oracle b/tests/syntax/oracle/sizeof_void.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..c572fd18bd548997a5a8eee152b664ac80569653 --- /dev/null +++ b/tests/syntax/oracle/sizeof_void.1.res.oracle @@ -0,0 +1,39 @@ +[kernel] Parsing tests/syntax/sizeof_void.c (with preprocessing) +/* Generated by Frama-C */ +int f(void) +{ + int __retres; + int x = (int)sizeof(void); + __retres = 0; + return __retres; +} + +int g(void) +{ + int __retres; + void *p; + int x = (int)sizeof(p); + int y = (int)sizeof(*p); + __retres = 0; + return __retres; +} + +int h(void) +{ + int __retres; + int x = (int)__alignof__(void); + __retres = 0; + return __retres; +} + +int i(void) +{ + int __retres; + void *p; + int x = (int)__alignof__(p); + int y = (int)__alignof__(*p); + __retres = 0; + return __retres; +} + + diff --git a/tests/syntax/sizeof_void.c b/tests/syntax/sizeof_void.c new file mode 100644 index 0000000000000000000000000000000000000000..8a0d451a8d0204744ca6fb53155600ffc47933ea --- /dev/null +++ b/tests/syntax/sizeof_void.c @@ -0,0 +1,30 @@ +/* run.config + EXIT: 1 + STDOPT: +"-machdep x86_64" + EXIT: 0 + STDOPT: +"-machdep gcc_x86_64" +*/ + +int f () { + int x = sizeof(void); + return 0; +} + +int g () { + void *p; + int x = sizeof(p); + int y = sizeof(*p); + return 0; +} + +int h () { + int x = __alignof__(void); + return 0; +} + +int i () { + void *p; + int x = __alignof__(p); + int y = __alignof__(*p); + return 0; +} diff --git a/tests/value/oracle/sizeof.res.oracle b/tests/value/oracle/sizeof.res.oracle index aa8dc50d410df0a8961e66ac04949f144fedee20..a65bbd389ff12c6b8e20b028bcf535cfb0ffd3f9 100644 --- a/tests/value/oracle/sizeof.res.oracle +++ b/tests/value/oracle/sizeof.res.oracle @@ -10,14 +10,14 @@ s1 ∈ {0} i ∈ [--..--] [eva] computing for function main1 <- main. - Called from tests/value/sizeof.i:40. + Called from tests/value/sizeof.i:51. [eva] tests/value/sizeof.i:10: assertion got status valid. [eva] tests/value/sizeof.i:14: assertion got status valid. [eva] tests/value/sizeof.i:17: assertion got status valid. [eva] Recording results for main1 [eva] Done for function main1 [eva] computing for function main2 <- main. - Called from tests/value/sizeof.i:41. + Called from tests/value/sizeof.i:52. [eva:alarm] tests/value/sizeof.i:32: Warning: pointer downcast. assert (unsigned int)(&s1) ≤ 2147483647; [eva] tests/value/sizeof.i:32: @@ -37,8 +37,12 @@ assert \valid(&p->t[(unsigned int)(sizeof(int [10]) - (unsigned int)i)]); [eva] Recording results for main2 [eva] Done for function main2 +[eva] computing for function sizeof_void <- main. + Called from tests/value/sizeof.i:53. +[eva] Recording results for sizeof_void +[eva] Done for function sizeof_void [eva] computing for function f <- main. - Called from tests/value/sizeof.i:42. + Called from tests/value/sizeof.i:54. [eva] Recording results for f [eva] Done for function f [eva] Recording results for main @@ -54,6 +58,13 @@ [eva:final-states] Values at end of function main2: s1 ∈ [--..--] p ∈ {{ &s1 + [-36..36] }} +[eva:final-states] Values at end of function sizeof_void: + size_void ∈ {1} + size_ptr ∈ {4} + size_void_expr ∈ {1} + align_void ∈ {1} + align_ptr ∈ {4} + align_void_expr ∈ {1} [eva:final-states] Values at end of function main: sz_str ∈ {4} sz_typ ∈ {1} @@ -66,6 +77,8 @@ [from] Done for function main1 [from] Computing for function main2 [from] Done for function main2 +[from] Computing for function sizeof_void +[from] Done for function sizeof_void [from] Computing for function main [from] Done for function main [from] ====== DEPENDENCIES COMPUTED ====== @@ -79,6 +92,8 @@ align_typ FROM \nothing [from] Function main2: s1 FROM i (and SELF) +[from] Function sizeof_void: + NO EFFECTS [from] Function main: sz_str FROM \nothing sz_typ FROM \nothing @@ -98,6 +113,10 @@ s1; p [inout] Inputs for function main2: i +[inout] Out (internal) for function sizeof_void: + size_void; size_ptr; size_void_expr; align_void; align_ptr; align_void_expr +[inout] Inputs for function sizeof_void: + \nothing [inout] Out (internal) for function main: sz_str; sz_typ; align_str; align_typ; s1 [inout] Inputs for function main: @@ -149,6 +168,18 @@ void main2(void) return; } +void sizeof_void(void) +{ + void *p; + int size_void = (int)sizeof(void); + int size_ptr = (int)sizeof(p); + int size_void_expr = (int)sizeof(*p); + int align_void = (int)__alignof__(void); + int align_ptr = (int)__alignof__(p); + int align_void_expr = (int)__alignof__(*p); + return; +} + void f(int sz) { return; @@ -158,6 +189,7 @@ void main(int *p, int *q, int j) { main1(); main2(); + sizeof_void(); f((int)(sizeof(*p) * (unsigned int)j)); return; } diff --git a/tests/value/sizeof.i b/tests/value/sizeof.i index 3a577f9de29f1c069071aff16b5058930f8e7612..1d46bd7630e07456a36da83c5c9b969f897e8743 100644 --- a/tests/value/sizeof.i +++ b/tests/value/sizeof.i @@ -1,5 +1,5 @@ /* run.config* - STDOPT: +"-print" + STDOPT: +"-print -machdep gcc_x86_32" */ int sz_str,sz_typ,align_str,align_typ; @@ -34,10 +34,22 @@ void main2() { p->t[sizeof(s1.t)-i] = 2; } +/* Tests sizeof and alignof on void. Only valid in gcc machdeps. */ +void sizeof_void () { + void *p; + int size_void = sizeof(void); + int size_ptr = sizeof(p); + int size_void_expr = sizeof(*p); + int align_void = __alignof__(void); + int align_ptr = __alignof__(p); + int align_void_expr = __alignof__(*p); +} + void f(int sz) {} void main(int *p, int *q, int j) { main1(); main2(); + sizeof_void(); f(sizeof(*p) * j); // must not crash with equality domain }