diff --git a/.travis.yml b/.travis.yml index 1dcbb7d02b3..a772cb400d1 100644 --- a/.travis.yml +++ b/.travis.yml @@ -158,6 +158,8 @@ install: - ccache --max-size=1G - COMMAND="make -C src minisat2-download" && eval ${PRE_COMMAND} ${COMMAND} + - COMMAND="make -C src/ansi-c library_check" && + eval ${PRE_COMMAND} ${COMMAND} - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"-Wall -Werror -pedantic -O2 -g $EXTRA_CXXFLAGS\" -j2" && eval ${PRE_COMMAND} ${COMMAND} - COMMAND="make -C src CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2 clobber.dir memory-models.dir musketeer.dir" && diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 90bdd1e6a56..f251dc3910c 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -94,14 +94,15 @@ else endif library_check: library/*.c for f in $(filter-out $(platform_unavail), $^) ; do \ + echo "Checking $$f" ; \ cp $$f __libcheck.c ; \ - sed -i 's/__builtin_[^v]/s&/' __libcheck.c ; \ - sed -i 's/__sync_/s&/' __libcheck.c ; \ - sed -i 's/__noop/s&/' __libcheck.c ; \ + perl -p -i -e 's/(__builtin_[^v])/s$$1/' __libcheck.c ; \ + perl -p -i -e 's/(__sync_)/s$$1/' __libcheck.c ; \ + perl -p -i -e 's/(__noop)/s$$1/' __libcheck.c ; \ $(CC) -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool \ -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c ; \ $(CC) -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i -o __libcheck.s \ - -Wno-unused-label -Wno-uninitialized ; \ + -Wno-unused-label ; \ ec=$$? ; \ $(RM) __libcheck.s __libcheck.i __libcheck.c ; \ [ $$ec -eq 0 ] || exit $$ec ; \ diff --git a/src/ansi-c/library/fcntl.c b/src/ansi-c/library/fcntl.c index 30f8c5e39fc..7001724c9bf 100644 --- a/src/ansi-c/library/fcntl.c +++ b/src/ansi-c/library/fcntl.c @@ -5,10 +5,12 @@ #define __CPROVER_FCNTL_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + int fcntl(int fd, int cmd, ...) { __CPROVER_HIDE:; - int return_value; + int return_value=__VERIFIER_nondet_int(); (void)fd; (void)cmd; return return_value; diff --git a/src/ansi-c/library/getopt.c b/src/ansi-c/library/getopt.c index 458f9d2e414..0045cbd105d 100644 --- a/src/ansi-c/library/getopt.c +++ b/src/ansi-c/library/getopt.c @@ -8,8 +8,11 @@ extern int optind; #define __CPROVER_STRING_H_INCLUDED #endif -inline int getopt(int argc, char * const argv[], - const char *optstring) +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +size_t __VERIFIER_nondet_size_t(); + +inline int getopt( + int argc, char * const argv[], const char *optstring) { __CPROVER_HIDE:; int result=-1; @@ -20,7 +23,7 @@ inline int getopt(int argc, char * const argv[], if(optind>=argc || argv[optind][0]!='-') return -1; - size_t result_index; + size_t result_index=__VERIFIER_nondet_size_t(); __CPROVER_assume( result_index +#define __CPROVER_GETOPT_H_INCLUDED +#endif -inline int getopt_long(int argc, char * const argv[], const char *optstring, - const struct option *longopts, int *longindex) +inline int getopt_long( + int argc, + char * const argv[], + const char *optstring, + const struct option *longopts, + int *longindex) { // trigger valid-pointer checks (if enabled), even though we don't // use the parameter in this model diff --git a/src/ansi-c/library/inet.c b/src/ansi-c/library/inet.c index 0d24a393620..88a508cc47f 100644 --- a/src/ansi-c/library/inet.c +++ b/src/ansi-c/library/inet.c @@ -2,6 +2,8 @@ #include +in_addr_t __VERIFIER_nondet_in_addr_t(); + in_addr_t inet_addr(const char *cp) { __CPROVER_HIDE:; @@ -10,12 +12,14 @@ in_addr_t inet_addr(const char *cp) __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_addr zero-termination of argument"); #endif - in_addr_t result; + in_addr_t result=__VERIFIER_nondet_in_addr_t(); return result; } /* FUNCTION: inet_aton */ +int __VERIFIER_nondet_int(); + int inet_aton(const char *cp, struct in_addr *pin) { __CPROVER_HIDE:; @@ -25,12 +29,14 @@ int inet_aton(const char *cp, struct in_addr *pin) __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_aton zero-termination of name argument"); #endif - int result; + int result=__VERIFIER_nondet_int(); return result; } /* FUNCTION: inet_network */ +in_addr_t __VERIFIER_nondet_in_addr_t(); + in_addr_t inet_network(const char *cp) { __CPROVER_HIDE:; @@ -39,6 +45,6 @@ in_addr_t inet_network(const char *cp) __CPROVER_assert(__CPROVER_is_zero_string(cp), "inet_network zero-termination of name argument"); #endif - in_addr_t result; + in_addr_t result=__VERIFIER_nondet_in_addr_t(); return result; } diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index 1af12148d83..c9f52dc8f76 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -64,22 +64,17 @@ int __CPROVER_islessgreaterd(double f, double g) { return (f < g) || (f > g); } /* FUNCTION: __CPROVER_isunorderedf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -int __CPROVER_isunorderedf(float f, float g) { return isnanf(f) || isnanf(g); } +int __CPROVER_isunorderedf(float f, float g) +{ + return __CPROVER_isnanf(f) || __CPROVER_isnanf(g); +} /* FUNCTION: __CPROVER_isunorderedd */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - -int __CPROVER_isunorderedd(double f, double g) { return isnan(f) || isnan(g); } - +int __CPROVER_isunorderedd(double f, double g) +{ + return __CPROVER_isnand(f) || __CPROVER_isnand(g); +} /* FUNCTION: isfinite */ @@ -363,10 +358,12 @@ inline int __fpclassify(double d) { /* FUNCTION: sin */ +double __VERIFIER_nondet_double(); + double sin(double x) { // gross over-approximation - double ret; + double ret=__VERIFIER_nondet_double(); if(__CPROVER_isinfd(x) || __CPROVER_isnand(x)) __CPROVER_assume(__CPROVER_isnand(ret)); @@ -382,10 +379,12 @@ double sin(double x) /* FUNCTION: sinl */ +long double __VERIFIER_nondet_long_double(); + long double sinl(long double x) { // gross over-approximation - long double ret; + long double ret=__VERIFIER_nondet_long_double(); if(__CPROVER_isinfld(x) || __CPROVER_isnanld(x)) __CPROVER_assume(__CPROVER_isnanld(ret)); @@ -401,10 +400,12 @@ long double sinl(long double x) /* FUNCTION: sinf */ +float __VERIFIER_nondet_float(); + float sinf(float x) { // gross over-approximation - float ret; + float ret=__VERIFIER_nondet_float(); if(__CPROVER_isinff(x) || __CPROVER_isnanf(x)) __CPROVER_assume(__CPROVER_isnanf(ret)); @@ -420,10 +421,12 @@ float sinf(float x) /* FUNCTION: cos */ +double __VERIFIER_nondet_double(); + double cos(double x) { // gross over-approximation - double ret; + double ret=__VERIFIER_nondet_double(); if(__CPROVER_isinfd(x) || __CPROVER_isnand(x)) __CPROVER_assume(__CPROVER_isnand(ret)); @@ -439,10 +442,12 @@ double cos(double x) /* FUNCTION: cosl */ +long double __VERIFIER_nondet_long_double(); + long double cosl(long double x) { // gross over-approximation - long double ret; + long double ret=__VERIFIER_nondet_long_double(); if(__CPROVER_isinfld(x) || __CPROVER_isnanld(x)) __CPROVER_assume(__CPROVER_isnanld(ret)); @@ -458,11 +463,13 @@ long double cosl(long double x) /* FUNCTION: cosf */ +float __VERIFIER_nondet_float(); + float cosf(float x) { __CPROVER_hide:; // gross over-approximation - float ret; + float ret=__VERIFIER_nondet_float(); if(__CPROVER_isinff(x) || __CPROVER_isnanf(x)) __CPROVER_assume(__CPROVER_isnanf(ret)); @@ -512,11 +519,6 @@ __CPROVER_hide:; /* FUNCTION: nan */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - double nan(const char *str) { // the 'str' argument is not yet used __CPROVER_hide:; @@ -526,11 +528,6 @@ double nan(const char *str) { /* FUNCTION: nanf */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - float nanf(const char *str) { // the 'str' argument is not yet used __CPROVER_hide:; @@ -540,11 +537,6 @@ float nanf(const char *str) { /* FUNCTION: nanl */ -#ifndef __CPROVER_MATH_H_INCLUDED -#include -#define __CPROVER_MATH_H_INCLUDED -#endif - long double nanl(const char *str) { // the 'str' argument is not yet used __CPROVER_hide:; @@ -552,10 +544,6 @@ long double nanl(const char *str) { return 0.0/0.0; } - - - - /* FUNCTION: nextUpf */ #ifndef __CPROVER_LIMITS_H_INCLUDED @@ -738,6 +726,8 @@ __CPROVER_hide:; float nextUpf(float f); +float __VERIFIER_nondet_float(); + float sqrtf(float f) { __CPROVER_hide:; @@ -750,7 +740,7 @@ float sqrtf(float f) return f; else if (__CPROVER_isnormalf(f)) { - float lower; // Intentionally non-deterministic + float lower=__VERIFIER_nondet_float(); __CPROVER_assume(lower > 0.0f); __CPROVER_assume(__CPROVER_isnormalf(lower)); // Tighter bounds can be given but are dependent on the @@ -795,7 +785,7 @@ float sqrtf(float f) // With respect to the algebra of floating point number // all subnormals seem to be perfect squares, thus ... - float root; // Intentionally non-deterministic + float root=__VERIFIER_nondet_float(); __CPROVER_assume(root >= 0.0f); __CPROVER_assume(root * root == f); @@ -823,6 +813,8 @@ float sqrtf(float f) double nextUp(double d); +double __VERIFIER_nondet_double(); + double sqrt(double d) { __CPROVER_hide:; @@ -835,7 +827,7 @@ double sqrt(double d) return d; else if (__CPROVER_isnormald(d)) { - double lower; // Intentionally non-deterministic + double lower=__VERIFIER_nondet_double(); __CPROVER_assume(lower > 0.0); __CPROVER_assume(__CPROVER_isnormald(lower)); @@ -867,7 +859,7 @@ double sqrt(double d) //assert(fpclassify(d) == FP_SUBNORMAL); //assert(d > 0.0); - double root; // Intentionally non-deterministic + double root=__VERIFIER_nondet_double(); __CPROVER_assume(root >= 0.0); __CPROVER_assume(root * root == d); @@ -892,6 +884,8 @@ double sqrt(double d) long double nextUpl(long double d); +long double __VERIFIER_nondet_long_double(); + long double sqrtl(long double d) { __CPROVER_hide:; @@ -904,7 +898,7 @@ long double sqrtl(long double d) return d; else if (__CPROVER_isnormalld(d)) { - long double lower; // Intentionally non-deterministic + long double lower=__VERIFIER_nondet_long_double(); __CPROVER_assume(lower > 0.0l); __CPROVER_assume(__CPROVER_isnormalld(lower)); @@ -936,7 +930,7 @@ long double sqrtl(long double d) //assert(fpclassify(d) == FP_SUBNORMAL); //assert(d > 0.0l); - long double root; // Intentionally non-deterministic + long double root=__VERIFIER_nondet_long_double(); __CPROVER_assume(root >= 0.0l); __CPROVER_assume(root * root == d); @@ -2316,7 +2310,7 @@ long double fabsl (long double d); long double copysignl(long double x, long double y) { - long double abs = fabs(x); + long double abs = fabsl(x); return (signbit(y)) ? -abs : abs; } diff --git a/src/ansi-c/library/netdb.c b/src/ansi-c/library/netdb.c index 40cb4e4eecc..d1f78941724 100644 --- a/src/ansi-c/library/netdb.c +++ b/src/ansi-c/library/netdb.c @@ -2,6 +2,8 @@ #include +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + struct hostent *gethostbyname(const char *name) { __CPROVER_HIDE:; @@ -10,7 +12,7 @@ struct hostent *gethostbyname(const char *name) __CPROVER_assert(__CPROVER_is_zero_string(name), "gethostbyname zero-termination of name argument"); #endif - __CPROVER_bool error; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); if(error) return 0; // quite restrictive, as will alias between calls @@ -22,6 +24,8 @@ struct hostent *gethostbyname(const char *name) /* FUNCTION: gethostbyaddr */ +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type) { __CPROVER_HIDE:; @@ -29,7 +33,7 @@ struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type) (void)len; (void)type; - __CPROVER_bool error; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); if(error) return 0; // quite restrictive, as will alias between calls @@ -41,11 +45,13 @@ struct hostent *gethostbyaddr(const void *addr, socklen_t len, int type) /* FUNCTION: gethostent */ +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + struct hostent *gethostent(void) { __CPROVER_HIDE:; - __CPROVER_bool error; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); if(error) return 0; // quite restrictive, as will alias between calls diff --git a/src/ansi-c/library/new.c b/src/ansi-c/library/new.c index beb4e70e1bf..81bd62b2093 100644 --- a/src/ansi-c/library/new.c +++ b/src/ansi-c/library/new.c @@ -1,5 +1,7 @@ /* FUNCTION: __new */ +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + inline void *__new(__typeof__(sizeof(int)) malloc_size) { // The constructor call is done by the front-end. @@ -12,13 +14,13 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size) __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated; // non-derministically record the object size for bounds checking - __CPROVER_bool record_malloc; + __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object; __CPROVER_malloc_size=record_malloc?malloc_size:__CPROVER_malloc_size; __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array; // detect memory leaks - __CPROVER_bool record_may_leak; + __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_memory_leak=record_may_leak?res:__CPROVER_memory_leak; return res; @@ -26,6 +28,8 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size) /* FUNCTION: __new_array */ +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size) { // The constructor call is done by the front-end. @@ -38,13 +42,13 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size) __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated; // non-deterministically record the object size for bounds checking - __CPROVER_bool record_malloc; + __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object; __CPROVER_malloc_size=record_malloc?size*count:__CPROVER_malloc_size; __CPROVER_malloc_is_new_array=record_malloc?1:__CPROVER_malloc_is_new_array; // detect memory leaks - __CPROVER_bool record_may_leak; + __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_memory_leak=record_may_leak?res:__CPROVER_memory_leak; return res; @@ -63,6 +67,8 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p) /* FUNCTION: __delete */ +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + inline void __delete(void *ptr) { __CPROVER_HIDE:; @@ -85,13 +91,18 @@ inline void __delete(void *ptr) "delete of array object"); // non-deterministically record as deallocated - __CPROVER_bool record; + __CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_deallocated=record?ptr:__CPROVER_deallocated; + + // detect memory leaks + if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0; } } /* FUNCTION: __delete_array */ +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + inline void __delete_array(void *ptr) { __CPROVER_HIDE:; @@ -114,7 +125,10 @@ inline void __delete_array(void *ptr) "delete[] of non-array object"); // non-deterministically record as deallocated - __CPROVER_bool record; + __CPROVER_bool record=__VERIFIER_nondet___CPROVER_bool(); __CPROVER_deallocated=record?ptr:__CPROVER_deallocated; + + // detect memory leaks + if(__CPROVER_memory_leak==ptr) __CPROVER_memory_leak=0; } } diff --git a/src/ansi-c/library/process.c b/src/ansi-c/library/process.c index c7de7fa5746..f1a89b9f7f4 100644 --- a/src/ansi-c/library/process.c +++ b/src/ansi-c/library/process.c @@ -1,5 +1,7 @@ /* FUNCTION: _beginthread */ +__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(); + __CPROVER_size_t _beginthread( void (*start_address)(void *), unsigned stack_size, @@ -8,12 +10,14 @@ __CPROVER_size_t _beginthread( __CPROVER_HIDE:; __CPROVER_ASYNC_1: start_address(arglist); (void)stack_size; - __CPROVER_size_t handle; + __CPROVER_size_t handle=__VERIFIER_nondet___CPROVER_size_t(); return handle; } /* FUNCTION: _beginthreadex */ +__CPROVER_size_t __VERIFIER_nondet___CPROVER_size_t(); + __CPROVER_size_t _beginthreadex( void *security, unsigned stack_size, @@ -29,6 +33,6 @@ __CPROVER_size_t _beginthreadex( (void)stack_size; (void)initflag; (void)*thrdaddr; - __CPROVER_size_t handle; + __CPROVER_size_t handle=__VERIFIER_nondet___CPROVER_size_t(); return handle; } diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c index ac3e6a18c3e..71af169c91b 100644 --- a/src/ansi-c/library/pthread_lib.c +++ b/src/ansi-c/library/pthread_lib.c @@ -5,6 +5,8 @@ #define __CPROVER_PTHREAD_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type) { __CPROVER_HIDE:; @@ -17,7 +19,7 @@ inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type) (void)type; #endif - int result; + int result=__VERIFIER_nondet_int(); return result; } @@ -28,6 +30,8 @@ inline int pthread_mutexattr_settype(pthread_mutexattr_t *attr, int type) #define __CPROVER_PTHREAD_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int pthread_cancel(pthread_t thread) { __CPROVER_HIDE:; @@ -38,7 +42,7 @@ inline int pthread_cancel(pthread_t thread) "pthread_cancel must be given valid thread ID"); #endif - int result; + int result=__VERIFIER_nondet_int(); return result; } @@ -532,12 +536,8 @@ inline int pthread_create( if(thread) { - #ifdef __APPLE__ - // pthread_t is a pointer type on the Mac + // pthread_t is a pointer type on some systems *thread=(pthread_t)this_thread_id; - #else - *thread=this_thread_id; - #endif } #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS @@ -729,6 +729,8 @@ int pthread_spin_trylock(pthread_spinlock_t *lock) #define __CPROVER_PTHREAD_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + // no pthread_barrier_t on the Mac #ifndef __APPLE__ inline int pthread_barrier_init( @@ -745,7 +747,7 @@ inline int pthread_barrier_init( __CPROVER_clear_may(barrier, "barrier-destroyed"); #endif - int result; + int result=__VERIFIER_nondet_int(); return result; } #endif @@ -757,6 +759,8 @@ inline int pthread_barrier_init( #define __CPROVER_PTHREAD_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + // no pthread_barrier_t on the Mac #ifndef __APPLE__ inline int pthread_barrier_destroy(pthread_barrier_t *barrier) @@ -773,7 +777,7 @@ inline int pthread_barrier_destroy(pthread_barrier_t *barrier) __CPROVER_set_may(barrier, "barrier-destroyed"); #endif - int result; + int result=__VERIFIER_nondet_int(); return result; } #endif @@ -785,6 +789,8 @@ inline int pthread_barrier_destroy(pthread_barrier_t *barrier) #define __CPROVER_PTHREAD_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + // no pthread_barrier_t on the Mac #ifndef __APPLE__ inline int pthread_barrier_wait(pthread_barrier_t *barrier) @@ -800,7 +806,7 @@ inline int pthread_barrier_wait(pthread_barrier_t *barrier) "pthread barrier must not be destroyed"); #endif - int result; + int result=__VERIFIER_nondet_int(); return result; } #endif diff --git a/src/ansi-c/library/setjmp.c b/src/ansi-c/library/setjmp.c index 64e99e98f8b..57c14998bb3 100644 --- a/src/ansi-c/library/setjmp.c +++ b/src/ansi-c/library/setjmp.c @@ -51,10 +51,12 @@ inline void siglongjmp(sigjmp_buf env, int val) #define __CPROVER_SETJMP_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int setjmp(jmp_buf env) { // store PC - int retval; + int retval=__VERIFIER_nondet_int(); (void)env; return retval; } diff --git a/src/ansi-c/library/signal.c b/src/ansi-c/library/signal.c index c08ec34909a..45fb723a7a4 100644 --- a/src/ansi-c/library/signal.c +++ b/src/ansi-c/library/signal.c @@ -10,10 +10,12 @@ #define __CPROVER_SIGNAL_H_INCLUDED #endif +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + int kill(pid_t pid, int sig) { (void)pid; (void)sig; - __CPROVER_bool error; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); return error ? -1 : 0; } diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index 0472908d744..a9ce6e7ec15 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -6,10 +6,13 @@ #define __CPROVER_STDIO_H_INCLUDED #endif +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + inline int putchar(int c) { - __CPROVER_bool error; - __CPROVER_HIDE: printf("%c", c); + __CPROVER_HIDE:; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); + printf("%c", c); return (error?-1:c); } @@ -20,11 +23,14 @@ inline int putchar(int c) #define __CPROVER_STDIO_H_INCLUDED #endif +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +int __VERIFIER_nondet_int(); + inline int puts(const char *s) { __CPROVER_HIDE:; - __CPROVER_bool error; - int ret; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); + int ret=__VERIFIER_nondet_int(); printf("%s\n", s); if(error) ret=-1; else __CPROVER_assume(ret>=0); return ret; @@ -52,6 +58,8 @@ inline void fclose_cleanup(void *stream) } #endif +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + inline FILE *fopen(const char *filename, const char *mode) { __CPROVER_HIDE:; @@ -64,7 +72,7 @@ inline FILE *fopen(const char *filename, const char *mode) FILE *fopen_result; - _Bool fopen_error; + __CPROVER_bool fopen_error=__VERIFIER_nondet___CPROVER_bool(); #if !defined(__linux__) || defined(__GLIBC__) fopen_result=fopen_error?NULL:malloc(sizeof(FILE)); @@ -94,7 +102,11 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f) __CPROVER_HIDE:; (void)*filename; (void)*mode; + #if !defined(__linux__) || defined(__GLIBC__) (void)*f; + #else + (void)*(char*)f; + #endif return f; } @@ -111,6 +123,8 @@ inline FILE* freopen(const char *filename, const char *mode, FILE *f) #define __CPROVER_STDLIB_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int fclose(FILE *stream) { __CPROVER_HIDE:; @@ -120,7 +134,7 @@ inline int fclose(FILE *stream) __CPROVER_clear_must(stream, "open"); __CPROVER_set_must(stream, "closed"); #endif - int return_value; + int return_value=__VERIFIER_nondet_int(); free(stream); return return_value; } @@ -160,7 +174,10 @@ inline FILE *fdopen(int handle, const char *mode) /* FUNCTION: _fdopen */ -// This is for Apple +// This is for Apple; we cannot fall back to fdopen as we need +// header files to have a definition of FILE available; the same +// header files rename fdopen to _fdopen and would thus yield +// unbounded recursion. #ifndef __CPROVER_STDIO_H_INCLUDED #include @@ -196,13 +213,20 @@ inline FILE *_fdopen(int handle, const char *mode) #define __CPROVER_STDIO_H_INCLUDED #endif +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +int __VERIFIER_nondet_int(); + char *fgets(char *str, int size, FILE *stream) { __CPROVER_HIDE:; - __CPROVER_bool error; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); (void)size; + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -221,7 +245,7 @@ char *fgets(char *str, int size, FILE *stream) #else if(size>0) { - int str_length; + int str_length=__VERIFIER_nondet_int(); __CPROVER_assume(str_length>=0 && str_length=-1 && return_value<=255); @@ -437,11 +509,18 @@ inline int fgetc(FILE *stream) #define __CPROVER_STDIO_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int getc(FILE *stream) { __CPROVER_HIDE:; - int return_value; + int return_value=__VERIFIER_nondet_int(); + + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -463,10 +542,12 @@ inline int getc(FILE *stream) #define __CPROVER_STDIO_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int getchar() { __CPROVER_HIDE:; - int return_value; + int return_value=__VERIFIER_nondet_int(); // it's a byte or EOF __CPROVER_assume(return_value>=-1 && return_value<=255); __CPROVER_input("getchar", return_value); @@ -480,11 +561,18 @@ inline int getchar() #define __CPROVER_STDIO_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int getw(FILE *stream) { __CPROVER_HIDE:; - int return_value; + int return_value=__VERIFIER_nondet_int(); + + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -504,11 +592,18 @@ inline int getw(FILE *stream) #define __CPROVER_STDIO_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int fseek(FILE *stream, long offset, int whence) { __CPROVER_HIDE:; - int return_value; + int return_value=__VERIFIER_nondet_int(); + + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif (void)offset; (void)whence; @@ -527,11 +622,18 @@ inline int fseek(FILE *stream, long offset, int whence) #define __CPROVER_STDIO_H_INCLUDED #endif +long __VERIFIER_nondet_long(); + inline long ftell(FILE *stream) { __CPROVER_HIDE:; - int return_value; + long return_value=__VERIFIER_nondet_long(); + + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -551,7 +653,12 @@ inline long ftell(FILE *stream) void rewind(FILE *stream) { __CPROVER_HIDE: + + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), @@ -566,6 +673,8 @@ void rewind(FILE *stream) #define __CPROVER_STDIO_H_INCLUDED #endif +size_t __VERIFIER_nondet_size_t(); + size_t fwrite( const void *ptr, size_t size, @@ -575,14 +684,19 @@ size_t fwrite( __CPROVER_HIDE:; (void)*(char*)ptr; (void)size; + + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS __CPROVER_assert(__CPROVER_get_must(stream, "open"), "fwrite file must be open"); #endif - size_t nwrite; + size_t nwrite=__VERIFIER_nondet_size_t(); __CPROVER_assume(nwrite<=nitems); return nwrite; } @@ -688,11 +802,17 @@ inline int sscanf(const char *restrict s, const char *restrict format, ...) #define __CPROVER_STDARG_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg) { __CPROVER_HIDE:; - int result; + int result=__VERIFIER_nondet_int(); + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif (void)*format; (void)arg; @@ -734,10 +854,12 @@ inline int vscanf(const char *restrict format, va_list arg) #define __CPROVER_STDARG_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int vsscanf(const char *restrict s, const char *restrict format, va_list arg) { __CPROVER_HIDE:; - int result; + int result=__VERIFIER_nondet_int(); (void)*s; (void)*format; (void)arg; @@ -778,12 +900,19 @@ inline int fprintf(FILE *stream, const char *restrict format, ...) #define __CPROVER_STDARG_H_INCLUDED #endif +int __VERIFIER_nondet_int(); + inline int vfprintf(FILE *stream, const char *restrict format, va_list arg) { __CPROVER_HIDE:; - int result; + int result=__VERIFIER_nondet_int(); + + #if !defined(__linux__) || defined(__GLIBC__) (void)*stream; + #else + (void)*(char*)stream; + #endif (void)*format; (void)arg; @@ -812,19 +941,23 @@ inline int vfprintf(FILE *stream, const char *restrict format, va_list arg) #define __CPROVER_STDLIB_H_INCLUDED #endif +char __VERIFIER_nondet_char(); +int __VERIFIER_nondet_int(); + inline int vasprintf(char **ptr, const char *fmt, va_list ap) { (void)*fmt; (void)ap; - int result_buffer_size; + int result_buffer_size=__VERIFIER_nondet_int(); if(result_buffer_size<=0) return -1; *ptr=malloc(result_buffer_size); - for(int i=0; i=0 && result<=2147483647); return result; } diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index bfc81bca82b..35cf46f7f66 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -55,7 +55,7 @@ __inline char *__builtin___strcat_chk(char *dst, const char *src, __CPROVER_size char ch; do { - char ch=src[j]; + ch=src[j]; dst[i]=ch; i++; j++; @@ -298,7 +298,12 @@ inline char *strncat(char *dst, const char *src, size_t n) inline int strcmp(const char *s1, const char *s2) { __CPROVER_HIDE:; + #if !defined(__linux__) || defined(__GLIBC__) if(s1!=0 && s1==s2) return 0; + #else + // musl guarantees non-null of s1 + if(s1==s2) return 0; + #endif #ifdef __CPROVER_STRING_ABSTRACTION int retval; __CPROVER_assert(__CPROVER_is_zero_string(s1), "strcmp zero-termination of 1st argument"); @@ -340,7 +345,12 @@ inline int strcmp(const char *s1, const char *s2) inline int strcasecmp(const char *s1, const char *s2) { __CPROVER_HIDE:; + #if !defined(__linux__) || defined(__GLIBC__) if(s1!=0 && s1==s2) return 0; + #else + // musl guarantees non-null of s1 + if(s1==s2) return 0; + #endif #ifdef __CPROVER_STRING_ABSTRACTION int retval; __CPROVER_assert(__CPROVER_is_zero_string(s1), "strcasecmp zero-termination of 1st argument"); @@ -385,7 +395,12 @@ inline int strcasecmp(const char *s1, const char *s2) inline int strncmp(const char *s1, const char *s2, size_t n) { __CPROVER_HIDE:; + #if !defined(__linux__) || defined(__GLIBC__) if(s1!=0 && s1==s2) return 0; + #else + // musl guarantees non-null of s1 + if(s1==s2) return 0; + #endif #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_assert(__CPROVER_is_zero_string(s1) || __CPROVER_buffer_size(s1)>=n, "strncmp zero-termination of 1st argument"); __CPROVER_assert(__CPROVER_is_zero_string(s2) || __CPROVER_buffer_size(s2)>=n, "strncmp zero-termination of 2nd argument"); @@ -424,7 +439,12 @@ inline int strncmp(const char *s1, const char *s2, size_t n) inline int strncasecmp(const char *s1, const char *s2, size_t n) { __CPROVER_HIDE:; + #if !defined(__linux__) || defined(__GLIBC__) if(s1!=0 && s1==s2) return 0; + #else + // musl guarantees non-null of s1 + if(s1==s2) return 0; + #endif #ifdef __CPROVER_STRING_ABSTRACTION int retval; __CPROVER_assert(__CPROVER_is_zero_string(s1), "strncasecmp zero-termination of 1st argument"); diff --git a/src/ansi-c/library/time.c b/src/ansi-c/library/time.c index 6c1fb1259a8..71606de0012 100644 --- a/src/ansi-c/library/time.c +++ b/src/ansi-c/library/time.c @@ -7,9 +7,11 @@ #undef time +time_t __VERIFIER_nondet_time_t(); + time_t time(time_t *tloc) { - time_t res; + time_t res=__VERIFIER_nondet_time_t(); if(!tloc) *tloc=res; return res; } @@ -105,10 +107,12 @@ struct tm *localtime_r(const time_t *clock, struct tm *result) #undef mktime +time_t __VERIFIER_nondet_time_t(); + time_t mktime(struct tm *timeptr) { (void)*timeptr; - time_t result; + time_t result=__VERIFIER_nondet_time_t(); return result; } @@ -121,10 +125,12 @@ time_t mktime(struct tm *timeptr) #undef timegm +time_t __VERIFIER_nondet_time_t(); + time_t timegm(struct tm *timeptr) { (void)*timeptr; - time_t result; + time_t result=__VERIFIER_nondet_time_t(); return result; } diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c index 00af7246882..06a5859de81 100644 --- a/src/ansi-c/library/unistd.c +++ b/src/ansi-c/library/unistd.c @@ -1,10 +1,12 @@ /* FUNCTION: sleep */ +unsigned __VERIFIER_nondet_unsigned(); + unsigned int sleep(unsigned int seconds) { __CPROVER_HIDE:; // do nothing, but return nondet value - unsigned remaining_time; + unsigned remaining_time=__VERIFIER_nondet_unsigned(); if(remaining_time>seconds) remaining_time=seconds; @@ -23,6 +25,8 @@ inline unsigned int _sleep(unsigned int seconds) /* FUNCTION: unlink */ +int __VERIFIER_nondet_int(); + int unlink(const char *s) { __CPROVER_HIDE:; @@ -30,7 +34,7 @@ int unlink(const char *s) #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_assert(__CPROVER_is_zero_string(s), "unlink zero-termination"); #endif - int retval; + int retval=__VERIFIER_nondet_int(); return retval; } @@ -46,10 +50,12 @@ extern struct __CPROVER_pipet __CPROVER_pipes[]; extern const int __CPROVER_pipe_offset; extern unsigned __CPROVER_pipe_count; +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); + int pipe(int fildes[2]) { __CPROVER_HIDE:; - char error; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); if(error) { errno=error==1 ? EMFILE : ENFILE; @@ -102,6 +108,8 @@ int close(int fildes) /* FUNCTION: _close */ +int close(int fildes); + inline int _close(int fildes) { __CPROVER_HIDE:; @@ -126,12 +134,14 @@ extern struct __CPROVER_pipet __CPROVER_pipes[]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; +ssize_t __VERIFIER_nondet_ssize_t(); + ssize_t write(int fildes, const void *buf, size_t nbyte) { __CPROVER_HIDE:; if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset) { - ssize_t retval; + ssize_t retval=__VERIFIER_nondet_ssize_t(); __CPROVER_assume(retval>=-1 && retval<=(ssize_t)nbyte); return retval; } @@ -192,12 +202,15 @@ extern struct __CPROVER_pipet __CPROVER_pipes[]; // offset to make sure we don't collide with other fds extern const int __CPROVER_pipe_offset; +__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +ssize_t __VERIFIER_nondet_ssize_t(); + ssize_t read(int fildes, void *buf, size_t nbyte) { __CPROVER_HIDE:; if((fildes>=0 && fildes<=2) || fildes < __CPROVER_pipe_offset) { - ssize_t nread; + ssize_t nread=__VERIFIER_nondet_ssize_t(); __CPROVER_assume(0<=nread && (size_t)nread<=nbyte); #if 0 @@ -212,7 +225,7 @@ ssize_t read(int fildes, void *buf, size_t nbyte) __CPROVER_array_replace((char*)buf, nondet_bytes); #endif - __CPROVER_bool error; + __CPROVER_bool error=__VERIFIER_nondet___CPROVER_bool(); return error ? -1 : nread; }