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 all 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…
May 22, 2018
8b65d37
use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJE…
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
12 changes: 12 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 @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com

#include "ansi_c_internal_additions.h"

#include <util/c_types.h>
#include <util/config.h>

const char gcc_builtin_headers_types[]=
Expand Down Expand Up @@ -124,13 +125,24 @@ void ansi_c_internal_additions(std::string &code)
code+=
"# 1 \"<built-in-additions>\"\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"
"__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n"
// 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"

Expand Down
7 changes: 4 additions & 3 deletions src/ansi-c/library/cprover.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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(
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
Member

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
13 changes: 9 additions & 4 deletions src/cpp/cpp_internal_additions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com

#include <ostream>

#include <util/c_types.h>
#include <util/config.h>

#include <ansi-c/ansi_c_internal_additions.h>
Expand Down Expand Up @@ -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';
Expand All @@ -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';
Expand Down