Skip to content

Add new builtin __CPROVER_havoc_slice #6430

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

Merged
TGWDB merged 1 commit into from
Nov 18, 2021
Merged

Add new builtin __CPROVER_havoc_slice #6430

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
51 changes: 51 additions & 0 deletions doc/cprover-manual/api.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,6 +211,57 @@ returns true when it is safe to do both. These predicates can be given an
optional size; when the size argument is not given, the size of the subtype
(which must not be **void**) of the pointer type is used.

#### \_\_CPROVER\_havoc\_object
Copy link
Collaborator

@tautschnig tautschnig Nov 17, 2021

Choose a reason for hiding this comment

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

Random place for comment: it would be great if the commit message also answered the "Why?" question. See https://chris.beams.io/posts/git-commit/ as linked from the pull-request template. On this occasion, it would be good to answer the "why did __CPROVER_havoc_object not suffice" question.



This function requires a valid pointer and updates **all bytes** of the
underlying object with nondeterministic values.

```C
void __CPROVER_havoc_object(void *p);
Copy link
Contributor

@danielsn danielsn Nov 4, 2021 •
edited
Loading

Choose a reason for hiding this comment

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

When you say "object", what do you mean?
For example, should this assertion pass or fail?

struct foo {
  int x;
  int y;
};

struct foo thefoo = {.x = 1; .y = 12};
int* p = &thefoo.y;
__CPROVER_havoc_object(p);
assert(thefoo.x == 1);

Copy link
Collaborator Author

@remi-delmas-3000 remi-delmas-3000 Nov 4, 2021

Choose a reason for hiding this comment

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

the object in that case is the blob of memory that holds the whole struct thefoo so this assertion should fail.
on the other it passes when using __CPROVER_havoc_object_slice(p, sizeof(*p))

Copy link
Contributor

@danielsn danielsn Nov 8, 2021

Choose a reason for hiding this comment

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

This seems like it could lead to a foot gun:

int foo_stub(int* p) {
   __CPROVER_havoc_object(p);
   return *p;
}

struct foo { int x; int y; };

int main() [
  struct foo thefoo = {.x = 1; .y = 12};
  int v = foo_stub(&thefoo.y);
  assert(thefoo.x == 1);
  assert(thefoo.y == v);
}

I think the user would expect that foo_stub wouldn't modify memory which it doesn't have a valid pointer to. Maybe we need a different name:

__CPROVER_havoc_entire_allocation()

Copy link
Collaborator Author

@remi-delmas-3000 remi-delmas-3000 Nov 10, 2021

Choose a reason for hiding this comment

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

Agreed, we could name __CPROVER_havoc_object differently but it was introduced some time ago so this could be a breaking change for existing users of the primitive.

Copy link
Collaborator

@jimgrundy jimgrundy Nov 11, 2021

Choose a reason for hiding this comment

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

Can we just add a more explicit warning to the document about havoc_object that it will havoc enclosing structs.

```

**Warning**

This primitive havocs object bytes before
the given `p` and after `p + sizeof(*p)`:

```C
struct foo {
int x;
int y;
int z;
};

struct foo thefoo = {.x = 1; .y = 2, .z = 3};

int* p = &thefoo.y; // pointing to thefoo.y

__CPROVER_havoc_object(p); // makes the whole struct nondet
__CPROVER_assert(thefoo.x == 1, "fails because `thefoo.x` is now nondet");
__CPROVER_assert(thefoo.y == 2, "fails because `thefoo.y` is now nondet");
__CPROVER_assert(thefoo.z == 3, "fails because `thefoo.z` is now nondet");
```

#### \_\_CPROVER\_havoc\_slice

This function requires requires that `__CPROVER_w_ok(p, size)` holds,
and updates `size` consecutive bytes of the underlying object, starting at `p`,
with nondeterministic values.

```C
void __CPROVER_havoc_slice(void *p, __CPROVER_size_t size);
```

**Caveat**

- If the slice contains bytes that can be interpreted as pointers by the
program, this will cause these pointers to become invalid
(i.e. they will not point to anything meaningful).
- If this slice only contains bytes that are not interpreted as pointers
by the program, then havocing the slice is equivalent to making the
interpretation of these bytes nondeterministic.

### Predefined Types and Symbols

#### \_\_CPROVER\_bitvector
Expand Down
26 changes: 26 additions & 0 deletions regression/cbmc/havoc_slice/declarations.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
#include <stdint.h>
#include <stdlib.h>

// HAVOC STRUCT MEMBERS
// TODO take into account plaform/pointer size in the tests
typedef struct
{
uint16_t a; // 2 bytes
uint16_t b[5]; // 10 bytes
uint32_t c; // 4 bytes
uint16_t *d; // 4 or 8 bytes
union {
uint16_t a; // 2 bytes
uint16_t b[5]; // 10 bytes
uint32_t c; // 4 bytes
uint16_t *d; // 4 or 8 bytes
} u; // 10 bytes
} st; // 30 or 34 bytes total

// 0 2 12 16 24 34
// | | | | | |
// struct layout: aa bbbbbbbbbb cccc dddddddd uuuuuuuuuu
// union layout : aa--------
// bbbbbbbbbb
// cccc------
// dddddddd--
17 changes: 17 additions & 0 deletions regression/cbmc/havoc_slice/test_array_slice_1.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
void main(void)
{
// INITIALIZE
int a[5] = {0, 1, 2, 3, 4};
int old_a[5] = {0, 1, 2, 3, 4};

// HAVOC ARRAY SLICE
__CPROVER_havoc_slice(a + 2, 2 * sizeof(*a));

// POSTCONDITIONS
__CPROVER_assert(a[0] == old_a[0], "expecting SUCCESS");
__CPROVER_assert(a[1] == old_a[1], "expecting SUCCESS");
__CPROVER_assert(a[2] == old_a[2], "expecting FAILURE");
__CPROVER_assert(a[3] == old_a[3], "expecting FAILURE");
__CPROVER_assert(a[4] == old_a[4], "expecting SUCCESS");
return;
}
10 changes: 10 additions & 0 deletions regression/cbmc/havoc_slice/test_array_slice_1.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test_array_slice_1.c

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^.*expecting FAILURE: SUCCESS$
^.*expecting SUCCESS: FAILURE$
^.*dereference .*: FAILURE$
17 changes: 17 additions & 0 deletions regression/cbmc/havoc_slice/test_array_slice_2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
void main(void)
{
// INITIALIZE
int a[5] = {0, 1, 2, 3, 4};
int old_a[5] = {0, 1, 2, 3, 4};

// HAVOC ARRAY SLICE
__CPROVER_havoc_slice(&a[2] - 1, 2 * sizeof(*a));

// POSTCONDITIONS
__CPROVER_assert(a[0] == old_a[0], "expecting SUCCESS");
__CPROVER_assert(a[1] == old_a[1], "expecting FAILURE");
__CPROVER_assert(a[2] == old_a[2], "expecting FAILURE");
__CPROVER_assert(a[3] == old_a[3], "expecting SUCCESS");
__CPROVER_assert(a[4] == old_a[4], "expecting SUCCESS");
return;
}
10 changes: 10 additions & 0 deletions regression/cbmc/havoc_slice/test_array_slice_2.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test_array_slice_2.c

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^.*expecting FAILURE: SUCCESS$
^.*expecting SUCCESS: FAILURE$
^.*dereference .*: FAILURE$
46 changes: 46 additions & 0 deletions regression/cbmc/havoc_slice/test_array_symbolic_size.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
#include <stdint.h>
#include <stdlib.h>

// byte-level comparison
#define CHECK_SLICE(A, OLD_A, I, IDX, HAVOC_SIZE) \
{ \
__CPROVER_assert( \
!(IDX <= I && I <= IDX + HAVOC_SIZE) | A[I] == OLD_A[I], \
"expecting FAILURE"); \
\
__CPROVER_assert( \
(IDX <= I && I <= IDX + HAVOC_SIZE) | A[I] == OLD_A[I], \
"expecting SUCCESS"); \
}

// ARRAY WITH SYMBOLIC SIZE.
void main(void)
{
// INITIALIZE
uint32_t size;
__CPROVER_assume(5 == size);

char a[size];
char old_a[size];

__CPROVER_array_set(a, 0);
__CPROVER_array_set(old_a, 0);

uint32_t idx;
__CPROVER_assume(idx < size);

uint32_t havoc_size;
__CPROVER_assume(1 <= havoc_size && havoc_size <= size);
__CPROVER_assume(idx + havoc_size <= size);

// HAVOC SINGLE CELL
__CPROVER_havoc_slice(&a[idx], havoc_size);

// POSTCONDITIONS
CHECK_SLICE(a, old_a, 0, idx, havoc_size);
CHECK_SLICE(a, old_a, 1, idx, havoc_size);
CHECK_SLICE(a, old_a, 2, idx, havoc_size);
CHECK_SLICE(a, old_a, 3, idx, havoc_size);
CHECK_SLICE(a, old_a, 4, idx, havoc_size);
return;
}
10 changes: 10 additions & 0 deletions regression/cbmc/havoc_slice/test_array_symbolic_size.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE thorough-paths thorough-smt-backend
test_array_symbolic_size.c

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^.*expecting FAILURE: SUCCESS$
^.*expecting SUCCESS: FAILURE$
^.*dereference .*: FAILURE$
34 changes: 34 additions & 0 deletions regression/cbmc/havoc_slice/test_nondet_conditional.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
void main(void)
{
// HAVOC through nondet conditional
typedef struct
{
int i;
int j;
} st;
int i = 10;
int old_i = 10;
st s = {20, 30};
st old_s = s;

_Bool c;

int *p = c ? &i : &s.i;

__CPROVER_havoc_slice(p, sizeof(*p));

if(c)
{
__CPROVER_assert(i == old_i, "expecting FAILURE");
__CPROVER_assert(s.i == old_s.i, "expecting SUCCESS");
__CPROVER_assert(s.j == old_s.j, "expecting SUCCESS");
}
else
{
__CPROVER_assert(i == old_i, "expecting SUCCESS");
__CPROVER_assert(s.i == old_s.i, "expecting FAILURE");
__CPROVER_assert(s.j == old_s.j, "expecting SUCCESS");
}

return;
}
10 changes: 10 additions & 0 deletions regression/cbmc/havoc_slice/test_nondet_conditional.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test_nondet_conditional.c

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^.*expecting FAILURE: SUCCESS$
^.*expecting SUCCESS: FAILURE$
^.*dereference .*: FAILURE$
32 changes: 32 additions & 0 deletions regression/cbmc/havoc_slice/test_struct_a.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
#include "declarations.h"

void main(void)
{
// INITIALIZE
uint16_t a = 1;
st old_s = {
.a = 1, .b = {0, 1, 2, 3, 4}, .c = 2, .d = &a, .u.b = {0, 1, 2, 3, 4}};
st s = old_s;

// HAVOC FIRST MEMBER
__CPROVER_havoc_slice(&s.a, sizeof(s.a));

// POSTCONDITION
__CPROVER_assert(s.a == old_s.a, "expecting FAILURE");
__CPROVER_assert(s.b[0] == old_s.b[0], "expecting SUCCESS");
__CPROVER_assert(s.b[1] == old_s.b[1], "expecting SUCCESS");
__CPROVER_assert(s.b[2] == old_s.b[2], "expecting SUCCESS");
__CPROVER_assert(s.b[3] == old_s.b[3], "expecting SUCCESS");
__CPROVER_assert(s.b[4] == old_s.b[4], "expecting SUCCESS");
__CPROVER_assert(s.c == old_s.c, "expecting SUCCESS");
__CPROVER_assert(s.d == old_s.d, "expecting SUCCESS");
__CPROVER_assert(s.u.a == old_s.u.a, "expecting SUCCESS");
__CPROVER_assert(s.u.b[0] == old_s.u.b[0], "expecting SUCCESS");
__CPROVER_assert(s.u.b[1] == old_s.u.b[1], "expecting SUCCESS");
__CPROVER_assert(s.u.b[2] == old_s.u.b[2], "expecting SUCCESS");
__CPROVER_assert(s.u.b[3] == old_s.u.b[3], "expecting SUCCESS");
__CPROVER_assert(s.u.b[4] == old_s.u.b[4], "expecting SUCCESS");
__CPROVER_assert(s.u.c == old_s.u.c, "expecting SUCCESS");
__CPROVER_assert(s.u.d == old_s.u.d, "expecting SUCCESS");
return;
}
10 changes: 10 additions & 0 deletions regression/cbmc/havoc_slice/test_struct_a.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test_struct_a.c

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^.*expecting FAILURE: SUCCESS$
^.*expecting SUCCESS: FAILURE$
^.*dereference .*: FAILURE$
31 changes: 31 additions & 0 deletions regression/cbmc/havoc_slice/test_struct_b.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
#include "declarations.h"

void main(void)
{
// INITIALIZE
uint16_t a = 1;
st old_s = {
.a = 1, .b = {0, 1, 2, 3, 4}, .c = 2, .d = &a, .u.b = {0, 1, 2, 3, 4}};
st s = old_s;

// HAVOC WHOLE SECOND MEMBER
__CPROVER_havoc_slice(s.b, sizeof(s.b));

// POSTCONDITION
__CPROVER_assert(s.a == old_s.a, "expecting SUCCESS");
__CPROVER_assert(s.b[0] == old_s.b[0], "expecting FAILURE");
__CPROVER_assert(s.b[1] == old_s.b[1], "expecting FAILURE");
__CPROVER_assert(s.b[2] == old_s.b[2], "expecting FAILURE");
__CPROVER_assert(s.b[3] == old_s.b[3], "expecting FAILURE");
__CPROVER_assert(s.b[4] == old_s.b[4], "expecting FAILURE");
__CPROVER_assert(s.c == old_s.c, "expecting SUCCESS");
__CPROVER_assert(s.d == old_s.d, "expecting SUCCESS");
__CPROVER_assert(s.u.a == old_s.u.a, "expecting SUCCESS");
__CPROVER_assert(s.u.b[0] == old_s.u.b[0], "expecting SUCCESS");
__CPROVER_assert(s.u.b[1] == old_s.u.b[1], "expecting SUCCESS");
__CPROVER_assert(s.u.b[2] == old_s.u.b[2], "expecting SUCCESS");
__CPROVER_assert(s.u.b[3] == old_s.u.b[3], "expecting SUCCESS");
__CPROVER_assert(s.u.b[4] == old_s.u.b[4], "expecting SUCCESS");
__CPROVER_assert(s.u.c == old_s.u.c, "expecting SUCCESS");
__CPROVER_assert(s.u.d == old_s.u.d, "expecting SUCCESS");
}
10 changes: 10 additions & 0 deletions regression/cbmc/havoc_slice/test_struct_b.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test_struct_b.c

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^.*expecting FAILURE: SUCCESS$
^.*expecting SUCCESS: FAILURE$
^.*dereference .*: FAILURE$
32 changes: 32 additions & 0 deletions regression/cbmc/havoc_slice/test_struct_b_slice.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
#include "declarations.h"

void main(void)
{
// INITIALIZE
uint16_t a = 1;
st old_s = {
.a = 1, .b = {0, 1, 2, 3, 4}, .c = 2, .d = &a, .u.b = {0, 1, 2, 3, 4}};
st s = old_s;

// HAVOC SECOND MEMBER SLICE
__CPROVER_havoc_slice(s.b + 1, 2 * sizeof(*s.b));

// POSTCONDITIONS
__CPROVER_assert(s.a == old_s.a, "expecting SUCCESS");
__CPROVER_assert(s.b[0] == old_s.b[0], "expecting SUCCESS");
__CPROVER_assert(s.b[1] == old_s.b[1], "expecting FAILURE");
__CPROVER_assert(s.b[2] == old_s.b[2], "expecting FAILURE");
__CPROVER_assert(s.b[3] == old_s.b[3], "expecting SUCCESS");
__CPROVER_assert(s.b[4] == old_s.b[4], "expecting SUCCESS");
__CPROVER_assert(s.c == old_s.c, "expecting SUCCESS");
__CPROVER_assert(s.d == old_s.d, "expecting SUCCESS");
__CPROVER_assert(s.u.a == old_s.u.a, "expecting SUCCESS");
__CPROVER_assert(s.u.b[0] == old_s.u.b[0], "expecting SUCCESS");
__CPROVER_assert(s.u.b[1] == old_s.u.b[1], "expecting SUCCESS");
__CPROVER_assert(s.u.b[2] == old_s.u.b[2], "expecting SUCCESS");
__CPROVER_assert(s.u.b[3] == old_s.u.b[3], "expecting SUCCESS");
__CPROVER_assert(s.u.b[4] == old_s.u.b[4], "expecting SUCCESS");
__CPROVER_assert(s.u.c == old_s.u.c, "expecting SUCCESS");
__CPROVER_assert(s.u.d == old_s.u.d, "expecting SUCCESS");
return;
}
10 changes: 10 additions & 0 deletions regression/cbmc/havoc_slice/test_struct_b_slice.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE broken-smt-backend
test_struct_b_slice.c

^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
^.*expecting FAILURE: SUCCESS$
^.*expecting SUCCESS: FAILURE$
^.*dereference .*: FAILURE$
Loading