From d984199b927037b2599dbb0eca46f399885aa449 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Nov 2021 12:06:41 +0000 Subject: [PATCH 1/5] __CPROVER_llabs returns a long long Fixes the declaration in builtin_headers.h. Type checking actually ignored this declaration and would always generate the expression of the correct type. --- regression/cbmc-library/__builtin_llabs-01/main.c | 10 +++++++--- regression/cbmc-library/__builtin_llabs-01/test.desc | 4 ++-- regression/cbmc-library/llabs-01/main.c | 5 +++-- regression/cbmc-library/llabs-01/test.desc | 4 ++-- src/ansi-c/cprover_builtin_headers.h | 2 +- 5 files changed, 15 insertions(+), 10 deletions(-) diff --git a/regression/cbmc-library/__builtin_llabs-01/main.c b/regression/cbmc-library/__builtin_llabs-01/main.c index ad96055c481..6a0f074faaa 100644 --- a/regression/cbmc-library/__builtin_llabs-01/main.c +++ b/regression/cbmc-library/__builtin_llabs-01/main.c @@ -1,9 +1,13 @@ #include -#include + +#include + +#ifndef __GNUC__ +long long __builtin_llabs(long long); +#endif int main() { - __builtin_llabs(); - assert(0); + assert(__builtin_llabs(LLONG_MIN + 1) == LLONG_MAX); return 0; } diff --git a/regression/cbmc-library/__builtin_llabs-01/test.desc b/regression/cbmc-library/__builtin_llabs-01/test.desc index 9542d988e8d..f456d4fb459 100644 --- a/regression/cbmc-library/__builtin_llabs-01/test.desc +++ b/regression/cbmc-library/__builtin_llabs-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--pointer-check --bounds-check --signed-overflow-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-library/llabs-01/main.c b/regression/cbmc-library/llabs-01/main.c index 6b34245e1eb..84822acaefe 100644 --- a/regression/cbmc-library/llabs-01/main.c +++ b/regression/cbmc-library/llabs-01/main.c @@ -1,9 +1,10 @@ #include #include +#include + int main() { - llabs(); - assert(0); + assert(llabs(LLONG_MIN + 1) == LLONG_MAX); return 0; } diff --git a/regression/cbmc-library/llabs-01/test.desc b/regression/cbmc-library/llabs-01/test.desc index 9542d988e8d..f456d4fb459 100644 --- a/regression/cbmc-library/llabs-01/test.desc +++ b/regression/cbmc-library/llabs-01/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---pointer-check --bounds-check +--pointer-check --bounds-check --signed-overflow-check ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index e673dc59848..51de0f7bbfb 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -84,7 +84,7 @@ int __CPROVER_isunorderedd(double f, double g); // absolute value int __CPROVER_abs(int x); long int __CPROVER_labs(long int x); -long int __CPROVER_llabs(long long int x); +long long int __CPROVER_llabs(long long int x); double __CPROVER_fabs(double x); long double __CPROVER_fabsl(long double x); float __CPROVER_fabsf(float x); From 1a355b678a4b01173c3e0f306a6bbdac7d755c1f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Nov 2021 12:16:53 +0000 Subject: [PATCH 2/5] C library: make all branches of sqrt{,f,l} explicitly return Makes GCC happier when doing library validation. Our C front-end would implicitly generate nondet return values of the correct type, so this does not actually change any verification behaviour. --- src/ansi-c/library/math.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index 69aa6ea4aa8..9b600d62dca 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -758,7 +758,7 @@ float sqrtf(float f) case FE_TOWARDZERO : return (f - lowerSquare == 0.0f) ? lower : upper; break; default:; - //assert(0); + return __VERIFIER_nondet_float(); } } @@ -835,7 +835,7 @@ double sqrt(double d) case FE_TOWARDZERO: return (d - lowerSquare == 0.0) ? lower : upper; break; default:; - //assert(0); + return __VERIFIER_nondet_double(); } } @@ -906,7 +906,7 @@ long double sqrtl(long double d) case FE_TOWARDZERO: return (d - lowerSquare == 0.0l) ? lower : upper; break; default:; - //assert(0); + return __VERIFIER_nondet_long_double(); } } From 25a71fcf38000255d54c7420881b6defd31397ab Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Nov 2021 12:19:16 +0000 Subject: [PATCH 3/5] C library/fread: use __VERIFIER_nondet_char The uninitialised local variable can trip up GCC's validation. Use a __VERIFIER_nondet_ function as is already done elsewhere. --- src/ansi-c/library/stdio.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index d280ac15e90..59250dacae2 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -330,6 +330,7 @@ char *fgets(char *str, int size, FILE *stream) #define __CPROVER_STDIO_H_INCLUDED #endif +char __VERIFIER_nondet_char(); size_t __VERIFIER_nondet_size_t(); inline size_t fread( @@ -359,8 +360,7 @@ inline size_t fread( for(size_t i=0; i Date: Tue, 30 Nov 2021 12:21:32 +0000 Subject: [PATCH 4/5] C library: add __builtin_unreachable to functions that do not return These calls are wrapped in #ifdef LIBRARY_CHECK and exist for the sole purpose of making library_check.sh not warn about `noreturn` functions seemingly returning. --- src/ansi-c/library/pthread_lib.c | 3 +++ src/ansi-c/library/setjmp.c | 9 +++++++++ src/ansi-c/library/stdlib.c | 9 +++++++++ src/ansi-c/library_check.sh | 1 + 4 files changed, 22 insertions(+) diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index b792ba6df0f..80c97a1060c 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -314,6 +314,9 @@ inline void pthread_exit(void *value_ptr) #endif __CPROVER_threads_exited[__CPROVER_thread_id]=1; __CPROVER_assume(0); +#ifdef LIBRARY_CHECK + __builtin_unreachable(); +#endif } /* FUNCTION: pthread_join */ diff --git a/src/ansi-c/library/setjmp.c b/src/ansi-c/library/setjmp.c index 1aee3b6c47f..7ee26630129 100644 --- a/src/ansi-c/library/setjmp.c +++ b/src/ansi-c/library/setjmp.c @@ -13,6 +13,9 @@ inline void longjmp(jmp_buf env, int val) (void)val; __CPROVER_assert(0, "longjmp requires instrumentation"); __CPROVER_assume(0); +#ifdef LIBRARY_CHECK + __builtin_unreachable(); +#endif } /* FUNCTION: _longjmp */ @@ -29,6 +32,9 @@ inline void _longjmp(jmp_buf env, int val) (void)val; __CPROVER_assert(0, "_longjmp requires instrumentation"); __CPROVER_assume(0); +#ifdef LIBRARY_CHECK + __builtin_unreachable(); +#endif } /* FUNCTION: siglongjmp */ @@ -47,6 +53,9 @@ inline void siglongjmp(sigjmp_buf env, int val) (void)val; __CPROVER_assert(0, "siglongjmp requires instrumentation"); __CPROVER_assume(0); +#ifdef LIBRARY_CHECK + __builtin_unreachable(); +#endif } #endif diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c index 211e8d07985..bb3cd940290 100644 --- a/src/ansi-c/library/stdlib.c +++ b/src/ansi-c/library/stdlib.c @@ -36,6 +36,9 @@ inline void exit(int status) { (void)status; __CPROVER_assume(0); +#ifdef LIBRARY_CHECK + __builtin_unreachable(); +#endif } /* FUNCTION: _Exit */ @@ -46,6 +49,9 @@ inline void _Exit(int status) { (void)status; __CPROVER_assume(0); +#ifdef LIBRARY_CHECK + __builtin_unreachable(); +#endif } /* FUNCTION: abort */ @@ -55,6 +61,9 @@ inline void _Exit(int status) inline void abort(void) { __CPROVER_assume(0); +#ifdef LIBRARY_CHECK + __builtin_unreachable(); +#endif } /* FUNCTION: calloc */ diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh index bb362dc023a..ae49c0551d3 100755 --- a/src/ansi-c/library_check.sh +++ b/src/ansi-c/library_check.sh @@ -7,6 +7,7 @@ for f in "$@"; do echo "Checking ${f}" cp "${f}" __libcheck.c perl -p -i -e 's/(__builtin_[^v])/s$1/' __libcheck.c + perl -p -i -e 's/s(__builtin_unreachable)/$1/' __libcheck.c perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c From 52958450aafde6732d8afb8d509f937956f97dad Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 30 Nov 2021 12:23:02 +0000 Subject: [PATCH 5/5] C library check: use cprover_builtin_library.h library/cprover.h exists for the sole purpose of syntax-checking the C library using the system's C compiler. The declarations in there, however, did not always match those of the authoritative cprover_builtin_library.h. To avoid this split-brain problem, just include cprover_builtin_library.h after providing a few declarations otherwise generated by ansi_c_internal_additions.cpp. --- src/ansi-c/library/cprover.h | 158 ++------------------- src/ansi-c/library/module_dependencies.txt | 1 + 2 files changed, 13 insertions(+), 146 deletions(-) diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index dbd542748b7..beeb1501d9a 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: +Module: C library check Author: Daniel Kroening, kroening@kroening.com @@ -9,170 +9,36 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANSI_C_LIBRARY_CPROVER_H #define CPROVER_ANSI_C_LIBRARY_CPROVER_H +/// \file +/// CPROVER built-in declarations to perform library checks. This file is only +/// used by library_check.sh. + +// NOLINTNEXTLINE(readability/identifiers) typedef __typeof__(sizeof(int)) __CPROVER_size_t; +// NOLINTNEXTLINE(readability/identifiers) +typedef signed long long __CPROVER_ssize_t; + void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); extern const void *__CPROVER_deallocated; extern const void *__CPROVER_new_object; -extern _Bool __CPROVER_malloc_is_new_array; +extern __CPROVER_bool __CPROVER_malloc_is_new_array; extern const void *__CPROVER_memory_leak; extern int __CPROVER_malloc_failure_mode; extern __CPROVER_size_t __CPROVER_max_malloc_size; -extern _Bool __CPROVER_malloc_may_fail; +extern __CPROVER_bool __CPROVER_malloc_may_fail; // malloc failure modes extern int __CPROVER_malloc_failure_mode_return_null; extern int __CPROVER_malloc_failure_mode_assert_then_assume; -void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__)); -void __CPROVER_assert(__CPROVER_bool assertion, const char *description); -void __CPROVER_precondition(__CPROVER_bool assertion, const char *description); -void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description); - -_Bool __CPROVER_is_zero_string(const void *); -__CPROVER_size_t __CPROVER_zero_string_length(const void *); -__CPROVER_size_t __CPROVER_buffer_size(const void *); -__CPROVER_bool __CPROVER_r_ok(); -__CPROVER_bool __CPROVER_w_ok(); -__CPROVER_bool __CPROVER_rw_ok(); - -#if 0 -__CPROVER_bool __CPROVER_equal(); -__CPROVER_bool __CPROVER_same_object(const void *, const void *); - -const unsigned __CPROVER_constant_infinity_uint; -typedef void __CPROVER_integer; -typedef void __CPROVER_rational; -void __CPROVER_initialize(void); -void __CPROVER_cover(__CPROVER_bool condition); -#endif - -void __CPROVER_printf(const char *format, ...); -void __CPROVER_input(const char *id, ...); -void __CPROVER_output(const char *id, ...); - -// concurrency-related -void __CPROVER_atomic_begin(); -void __CPROVER_atomic_end(); -void __CPROVER_fence(const char *kind, ...); -#if 0 -__CPROVER_thread_local unsigned long __CPROVER_thread_id=0; -__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint]; -unsigned long __CPROVER_next_thread_id=0; - -// traces -void CBMC_trace(int lvl, const char *event, ...); -#endif - -// pointers -unsigned __CPROVER_POINTER_OBJECT(const void *p); -signed __CPROVER_POINTER_OFFSET(const void *p); -__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p); -#if 0 -extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint]; -void __CPROVER_allocated_memory( - __CPROVER_size_t address, __CPROVER_size_t extent); - -// this is ANSI-C -extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint]; - -// this is GCC -extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint]; -extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint]; -#endif - -// float stuff -int __CPROVER_fpclassify(int, int, int, int, int, ...); -__CPROVER_bool __CPROVER_isfinite(double f); -__CPROVER_bool __CPROVER_isinf(double f); -__CPROVER_bool __CPROVER_isnormal(double f); -__CPROVER_bool __CPROVER_sign(double f); -__CPROVER_bool __CPROVER_isnanf(float f); -__CPROVER_bool __CPROVER_isnand(double f); -__CPROVER_bool __CPROVER_isnanld(long double f); -__CPROVER_bool __CPROVER_isfinitef(float f); -__CPROVER_bool __CPROVER_isfinited(double f); -__CPROVER_bool __CPROVER_isfiniteld(long double f); -__CPROVER_bool __CPROVER_isinff(float f); -__CPROVER_bool __CPROVER_isinfd(double f); -__CPROVER_bool __CPROVER_isinfld(long double f); -__CPROVER_bool __CPROVER_isnormalf(float f); -__CPROVER_bool __CPROVER_isnormald(double f); -__CPROVER_bool __CPROVER_isnormalld(long double f); -__CPROVER_bool __CPROVER_signf(float f); -__CPROVER_bool __CPROVER_signd(double f); -__CPROVER_bool __CPROVER_signld(long double f); -double __CPROVER_inf(void); -float __CPROVER_inff(void); -long double __CPROVER_infl(void); -//extern int __CPROVER_thread_local __CPROVER_rounding_mode; -int __CPROVER_isgreaterd(double f, double g); - -// absolute value -int __CPROVER_abs(int); -long int __CPROVER_labs(long int); -long long int __CPROVER_llabs(long long int); -double __CPROVER_fabs(double); -long double __CPROVER_fabsl(long double); -float __CPROVER_fabsf(float); - -// modulo and remainder -double __CPROVER_fmod(double, double); -float __CPROVER_fmodf(float, float); -long double __CPROVER_fmodl(long double, long double); -double __CPROVER_remainder(double, double); -float __CPROVER_remainderf(float, float); -long double __CPROVER_remainderl(long double, long double); - -// arrays -//__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2); -void __CPROVER_array_copy(const void *dest, const void *src); -void __CPROVER_array_set(const void *dest, ...); -void __CPROVER_array_replace(const void *dest, const void *src); - -#if 0 -// k-induction -void __CPROVER_k_induction_hint(unsigned min, unsigned max, -unsigned step, unsigned loop_free); - -// manual specification of predicates -void __CPROVER_predicate(__CPROVER_bool predicate); -void __CPROVER_parameter_predicates(); -void __CPROVER_return_predicates(); -#endif - -// pipes, write, read, close struct __CPROVER_pipet { _Bool widowed; char data[4]; short next_avail; short next_unread; }; -#if 0 -extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint]; -// offset to make sure we don't collide with other fds -extern const int __CPROVER_pipe_offset; -extern unsigned __CPROVER_pipe_count; -#endif - -void __CPROVER_set_must(const void *, const char *); -void __CPROVER_set_may(const void *, const char *); -void __CPROVER_clear_must(const void *, const char *); -void __CPROVER_clear_may(const void *, const char *); -void __CPROVER_cleanup(const void *, void (*)(void *)); -__CPROVER_bool __CPROVER_get_must(const void *, const char *); -__CPROVER_bool __CPROVER_get_may(const void *, const char *); - -#define __CPROVER_danger_number_of_ops 1 -#define __CPROVER_danger_max_solution_size 1 -#define __CPROVER_danger_number_of_vars 1 -#define __CPROVER_danger_number_of_consts 1 -// detect overflow -__CPROVER_bool __CPROVER_overflow_minus(); -__CPROVER_bool __CPROVER_overflow_mult(); -__CPROVER_bool __CPROVER_overflow_plus(); -__CPROVER_bool __CPROVER_overflow_shl(); -__CPROVER_bool __CPROVER_overflow_unary_minus(); +#include "../cprover_builtin_headers.h" #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H diff --git a/src/ansi-c/library/module_dependencies.txt b/src/ansi-c/library/module_dependencies.txt index 646fc1e7b82..22abfa3386e 100644 --- a/src/ansi-c/library/module_dependencies.txt +++ b/src/ansi-c/library/module_dependencies.txt @@ -1,2 +1,3 @@ +.. ansi-c ansi-c/library