diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 845e2197e84..399c3fd66fe 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ansi_c_internal_additions.h" +#include #include const char gcc_builtin_headers_types[]= @@ -124,6 +125,8 @@ void ansi_c_internal_additions(std::string &code) code+= "# 1 \"\"\n" "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n" + "typedef "+c_type_as_string(signed_size_type().get(ID_C_c_type))+ + " __CPROVER_ssize_t;\n" "const unsigned __CPROVER_constant_infinity_uint;\n" "typedef void __CPROVER_integer;\n" "typedef void __CPROVER_rational;\n" @@ -131,6 +134,15 @@ void ansi_c_internal_additions(std::string &code) // NOLINTNEXTLINE(whitespace/line_length) "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n" "unsigned long __CPROVER_next_thread_id=0;\n" + + // traces + "void CBMC_trace(int lvl, const char *event, ...);\n" + + // pointers + "__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);\n" + "__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);\n" + "__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);\n" + "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n" // NOLINTNEXTLINE(whitespace/line_length) "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n" diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 7fce070860a..22d051f65b5 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_ANSI_C_LIBRARY_CPROVER_H typedef __typeof__(sizeof(int)) __CPROVER_size_t; +typedef signed long long __CPROVER_size_t; void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero); extern const void *__CPROVER_deallocated; extern const void *__CPROVER_malloc_object; @@ -53,9 +54,9 @@ 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); +__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *); +__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *); +__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *); #if 0 extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint]; void __CPROVER_allocated_memory( diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 8781b77c35d..5b5988ad24a 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -14,9 +14,11 @@ inline char *__builtin___strcpy_chk(char *dst, const char *src, __CPROVER_size_t __CPROVER_is_zero_string(dst)=1; __CPROVER_zero_string_length(dst)=__CPROVER_zero_string_length(src); #else - __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!= - __CPROVER_POINTER_OBJECT(src), - "strcpy src/dst overlap"); + __CPROVER_precondition( + __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) || + __CPROVER_POINTER_OFFSET(src) + s <= __CPROVER_POINTER_OFFSET(dst) || + __CPROVER_POINTER_OFFSET(dst) + s <= __CPROVER_POINTER_OFFSET(src), + "strcpy src/dst overlap"); __CPROVER_size_t i=0; char ch; do @@ -140,9 +142,16 @@ inline char *strcpy(char *dst, const char *src) __CPROVER_is_zero_string(dst)=1; __CPROVER_zero_string_length(dst)=__CPROVER_zero_string_length(src); #else - __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!= - __CPROVER_POINTER_OBJECT(src), - "strcpy src/dst overlap"); + { + unsigned long n; + for(n = 0U; *(src + n) != 0; ++n) + ; + __CPROVER_precondition( + __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) || + __CPROVER_POINTER_OFFSET(src) + n < __CPROVER_POINTER_OFFSET(dst) || + __CPROVER_POINTER_OFFSET(dst) + n < __CPROVER_POINTER_OFFSET(src), + "strcpy src/dst overlap"); + } __CPROVER_size_t i=0; char ch; do @@ -578,6 +587,8 @@ inline char *strdup(const char *str) void *memcpy(void *dst, const void *src, size_t n) { __CPROVER_HIDE: + if(n==0U) + return dst; #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_precondition(__CPROVER_buffer_size(src)>=n, "memcpy buffer overflow"); @@ -594,9 +605,16 @@ void *memcpy(void *dst, const void *src, size_t n) n <= __CPROVER_zero_string_length(dst))) __CPROVER_is_zero_string(dst)=0; #else - __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!= - __CPROVER_POINTER_OBJECT(src), - "memcpy src/dst overlap"); + // TODO: This should be assert rather that assume. However, due to uninitialised + // variables in SV-COMP benchmarks + // linux-4.2-rc1.tar.xz-32_7a-drivers--media--usb--dvb-usb--dvb-usb-opera.ko-entry_point_true-unreach-call.cil.out.c + // linux-4.2-rc1.tar.xz-43_2a-drivers--media--usb--s2255--s2255drv.ko-entry_point_true-unreach-call.cil.out.c + // linux-4.2-rc1.tar.xz-43_2a-drivers--usb--serial--digi_acceleport.ko-entry_point_true-unreach-call.cil.out.c + // the memcpy_guard function does not work. + __CPROVER_assume( + __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) || + __CPROVER_POINTER_OFFSET(src) + n <= __CPROVER_POINTER_OFFSET(dst) || + __CPROVER_POINTER_OFFSET(dst) + n <= __CPROVER_POINTER_OFFSET(src)); (void)*(char *)dst; // check that the memory is accessible (void)*(const char *)src; // check that the memory is accessible @@ -618,6 +636,8 @@ void *memcpy(void *dst, const void *src, size_t n) void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __CPROVER_size_t size) { __CPROVER_HIDE: + if(size==0U) + return dst; #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_precondition(__CPROVER_buffer_size(src)>=n, "memcpy buffer overflow"); @@ -636,9 +656,11 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C n <= __CPROVER_zero_string_length(dst))) __CPROVER_is_zero_string(dst)=0; #else - __CPROVER_precondition(__CPROVER_POINTER_OBJECT(dst)!= - __CPROVER_POINTER_OBJECT(src), - "memcpy src/dst overlap"); + __CPROVER_precondition( + __CPROVER_POINTER_OBJECT(dst) != __CPROVER_POINTER_OBJECT(src) || + __CPROVER_POINTER_OFFSET(src) + n <= __CPROVER_POINTER_OFFSET(dst) || + __CPROVER_POINTER_OFFSET(dst) + n <= __CPROVER_POINTER_OFFSET(src), + "__builtin___memcpy_chk src/dst overlap"); (void)*(char *)dst; // check that the memory is accessible (void)*(const char *)src; // check that the memory is accessible (void)size; @@ -668,6 +690,8 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C void *memset(void *s, int c, size_t n) { __CPROVER_HIDE:; + if(n==0U) + return s; #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_precondition(__CPROVER_buffer_size(s)>=n, "memset buffer overflow"); @@ -705,6 +729,8 @@ void *memset(void *s, int c, size_t n) void *__builtin_memset(void *s, int c, __CPROVER_size_t n) { __CPROVER_HIDE:; + if(n==0U) + return s; #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_precondition(__CPROVER_buffer_size(s)>=n, "memset buffer overflow"); @@ -744,6 +770,8 @@ void *__builtin_memset(void *s, int c, __CPROVER_size_t n) void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_t size) { __CPROVER_HIDE:; + if(n==0U) + return s; #ifdef __CPROVER_STRING_ABSTRACTION __CPROVER_precondition(__CPROVER_buffer_size(s)>=n, "memset buffer overflow"); diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 19260f6ac24..7facbbaf3f1 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include @@ -62,7 +63,11 @@ void cpp_internal_additions(std::ostream &out) // types out << "typedef __typeof__(sizeof(int)) __CPROVER::size_t;" << '\n'; - out << "typedef __typeof__(sizeof(int)) __CPROVER_size_t;" << '\n'; + out << "typedef __CPROVER::size_t __CPROVER_size_t;" << '\n'; + out << "typedef " + << c_type_as_string(signed_size_type().get(ID_C_c_type)) + << " __CPROVER::ssize_t;" << '\n'; + out << "typedef __CPROVER::ssize_t __CPROVER_ssize_t;" << '\n'; // assume/assert out << "extern \"C\" void assert(bool assertion);" << '\n'; @@ -83,9 +88,9 @@ void cpp_internal_additions(std::ostream &out) out << "extern \"C\" void __CPROVER::atomic_end();" << '\n'; // pointers - out << "extern \"C\" unsigned __CPROVER_POINTER_OBJECT(const void *p);\n"; - out << "extern \"C\" signed __CPROVER_POINTER_OFFSET(const void *p);" << '\n'; - out << "extern \"C\" bool __CPROVER_DYNAMIC_OBJECT(const void *p);" << '\n'; + out << "extern \"C\" __CPROVER::size_t __CPROVER_POINTER_OBJECT(const void *);\n"; + out << "extern \"C\" __CPROVER::ssize_t __CPROVER_POINTER_OFFSET(const void *);" << '\n'; + out << "extern \"C\" bool __CPROVER_DYNAMIC_OBJECT(const void *);" << '\n'; // NOLINTNEXTLINE(whitespace/line_length) out << "extern \"C\" extern unsigned char __CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n'; out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n';