Skip to content

[SV-COMP'18 13/19] Memcpy assertions #2002

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 4 commits into from
Closed

[SV-COMP'18 13/19] Memcpy assertions #2002

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
555451c
More precise assertion in memcpy about overlap of src/dst memory.
marek-trtik Nov 9, 2017
b228fe4
SV-COMP Hotfix: memcpy - turning assert to assume to prever 3 RED re…
marek-trtik Nov 24, 2017
ec25788
use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJE…
kroening May 22, 2018
8b65d37
use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJE…
kroening May 22, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions src/ansi-c/ansi_c_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Convention: I think these are usually __CPROVER_lowercase_name

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The above seems to have been re-introduced after it got moved out into cprover_builtin_headers.h

"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"

Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/library/cprover.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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];
Expand Down
52 changes: 40 additions & 12 deletions src/ansi-c/library/string.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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");
}
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The precondition needs to be at the head of the function!

__CPROVER_size_t i=0;
char ch;
do
Expand Down Expand Up @@ -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");
Expand All @@ -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

Expand All @@ -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");
Expand All @@ -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;
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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");
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cpp_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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';
Expand Down