From 555451cfa265a0714f67163959acd6715c76d226 Mon Sep 17 00:00:00 2001 From: marek-trtik Date: Thu, 9 Nov 2017 18:09:47 +0000 Subject: [PATCH 1/4] More precise assertion in memcpy about overlap of src/dst memory. --- src/ansi-c/ansi_c_internal_additions.cpp | 9 +++++ src/ansi-c/library/cprover.h | 2 +- src/ansi-c/library/string.c | 47 ++++++++++++++++++------ src/cpp/cpp_internal_additions.cpp | 2 +- 4 files changed, 46 insertions(+), 14 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 845e2197e84..2f3c2d6366c 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -131,6 +131,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 + "unsigned __CPROVER_POINTER_OBJECT(const void *p);\n" + "signed long int __CPROVER_POINTER_OFFSET(const void *p);\n" + "__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\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..b96fd3dea3b 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -54,7 +54,7 @@ void CBMC_trace(int lvl, const char *event, ...); // pointers unsigned __CPROVER_POINTER_OBJECT(const void *p); -signed __CPROVER_POINTER_OFFSET(const void *p); +signed long int __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]; diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 8781b77c35d..8889cd95c1c 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,11 @@ 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"); + __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), + "memcpy src/dst overlap"); (void)*(char *)dst; // check that the memory is accessible (void)*(const char *)src; // check that the memory is accessible @@ -618,6 +631,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 +651,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 +685,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 +724,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 +765,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..f1a559f8c38 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -84,7 +84,7 @@ void cpp_internal_additions(std::ostream &out) // 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\" signed long int __CPROVER_POINTER_OFFSET(const void *p);" << '\n'; out << "extern \"C\" bool __CPROVER_DYNAMIC_OBJECT(const void *p);" << '\n'; // NOLINTNEXTLINE(whitespace/line_length) out << "extern \"C\" extern unsigned char __CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n'; From b228fe48b6f9854fd99a8ee3dd8f9824025ac543 Mon Sep 17 00:00:00 2001 From: Marek Trtik Date: Fri, 24 Nov 2017 11:03:08 +0000 Subject: [PATCH 2/4] SV-COMP Hotfix: memcpy - turning assert to assume to prever 3 RED results. --- src/ansi-c/library/string.c | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c index 8889cd95c1c..5b5988ad24a 100644 --- a/src/ansi-c/library/string.c +++ b/src/ansi-c/library/string.c @@ -605,11 +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( + // 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), - "memcpy src/dst overlap"); + __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 From ec25788e615f8280718f2774ae4604676274c160 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 20:53:12 +0100 Subject: [PATCH 3/4] use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJECT/OFFSET --- src/ansi-c/ansi_c_internal_additions.cpp | 9 ++++++--- src/cpp/cpp_internal_additions.cpp | 13 +++++++++---- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 2f3c2d6366c..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" @@ -136,9 +139,9 @@ void ansi_c_internal_additions(std::string &code) "void CBMC_trace(int lvl, const char *event, ...);\n" // pointers - "unsigned __CPROVER_POINTER_OBJECT(const void *p);\n" - "signed long int __CPROVER_POINTER_OFFSET(const void *p);\n" - "__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\n" + "__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/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index f1a559f8c38..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 long int __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'; From 8b65d37cbd9372c17e13bbc215cb8db9873862e7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 20:56:07 +0100 Subject: [PATCH 4/4] use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJECT/OFFSET --- src/ansi-c/library/cprover.h | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index b96fd3dea3b..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 long int __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(