Skip to content

Commit f562bcf

Browse files
TGWDBTGWDB
authored
Merge pull request #6430 from remi-delmas-3000/havoc-object-slice
Add new builtin __CPROVER_havoc_slice
2 parents eddc014 + 8ee6305 commit f562bcf

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

44 files changed

+934
-5
lines changed

‎doc/cprover-manual/api.md

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -211,6 +211,57 @@ returns true when it is safe to do both. These predicates can be given an
211211
optional size; when the size argument is not given, the size of the subtype
212212
(which must not be **void**) of the pointer type is used.
213213

214+
#### \_\_CPROVER\_havoc\_object
215+
216+
217+
This function requires a valid pointer and updates **all bytes** of the
218+
underlying object with nondeterministic values.
219+
220+
```C
221+
void __CPROVER_havoc_object(void *p);
222+
```
223+
224+
**Warning**
225+
226+
This primitive havocs object bytes before
227+
the given `p` and after `p + sizeof(*p)`:
228+
229+
```C
230+
struct foo {
231+
int x;
232+
int y;
233+
int z;
234+
};
235+
236+
struct foo thefoo = {.x = 1; .y = 2, .z = 3};
237+
238+
int* p = &thefoo.y; // pointing to thefoo.y
239+
240+
__CPROVER_havoc_object(p); // makes the whole struct nondet
241+
__CPROVER_assert(thefoo.x == 1, "fails because `thefoo.x` is now nondet");
242+
__CPROVER_assert(thefoo.y == 2, "fails because `thefoo.y` is now nondet");
243+
__CPROVER_assert(thefoo.z == 3, "fails because `thefoo.z` is now nondet");
244+
```
245+
246+
#### \_\_CPROVER\_havoc\_slice
247+
248+
This function requires requires that `__CPROVER_w_ok(p, size)` holds,
249+
and updates `size` consecutive bytes of the underlying object, starting at `p`,
250+
with nondeterministic values.
251+
252+
```C
253+
void __CPROVER_havoc_slice(void *p, __CPROVER_size_t size);
254+
```
255+
256+
**Caveat**
257+
258+
- If the slice contains bytes that can be interpreted as pointers by the
259+
program, this will cause these pointers to become invalid
260+
(i.e. they will not point to anything meaningful).
261+
- If this slice only contains bytes that are not interpreted as pointers
262+
by the program, then havocing the slice is equivalent to making the
263+
interpretation of these bytes nondeterministic.
264+
214265
### Predefined Types and Symbols
215266
216267
#### \_\_CPROVER\_bitvector

‎regression/cbmc/havoc_slice/declarations.h

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
#include <stdint.h>
2+
#include <stdlib.h>
3+
4+
// HAVOC STRUCT MEMBERS
5+
// TODO take into account plaform/pointer size in the tests
6+
typedef struct
7+
{
8+
uint16_t a; // 2 bytes
9+
uint16_t b[5]; // 10 bytes
10+
uint32_t c; // 4 bytes
11+
uint16_t *d; // 4 or 8 bytes
12+
union {
13+
uint16_t a; // 2 bytes
14+
uint16_t b[5]; // 10 bytes
15+
uint32_t c; // 4 bytes
16+
uint16_t *d; // 4 or 8 bytes
17+
} u; // 10 bytes
18+
} st; // 30 or 34 bytes total
19+
20+
// 0 2 12 16 24 34
21+
// | | | | | |
22+
// struct layout: aa bbbbbbbbbb cccc dddddddd uuuuuuuuuu
23+
// union layout : aa--------
24+
// bbbbbbbbbb
25+
// cccc------
26+
// dddddddd--

‎regression/cbmc/havoc_slice/test_array_slice_1.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
void main(void)
2+
{
3+
// INITIALIZE
4+
int a[5] = {0, 1, 2, 3, 4};
5+
int old_a[5] = {0, 1, 2, 3, 4};
6+
7+
// HAVOC ARRAY SLICE
8+
__CPROVER_havoc_slice(a + 2, 2 * sizeof(*a));
9+
10+
// POSTCONDITIONS
11+
__CPROVER_assert(a[0] == old_a[0], "expecting SUCCESS");
12+
__CPROVER_assert(a[1] == old_a[1], "expecting SUCCESS");
13+
__CPROVER_assert(a[2] == old_a[2], "expecting FAILURE");
14+
__CPROVER_assert(a[3] == old_a[3], "expecting FAILURE");
15+
__CPROVER_assert(a[4] == old_a[4], "expecting SUCCESS");
16+
return;
17+
}

‎regression/cbmc/havoc_slice/test_array_slice_1.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test_array_slice_1.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^.*expecting FAILURE: SUCCESS$
9+
^.*expecting SUCCESS: FAILURE$
10+
^.*dereference .*: FAILURE$

‎regression/cbmc/havoc_slice/test_array_slice_2.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
void main(void)
2+
{
3+
// INITIALIZE
4+
int a[5] = {0, 1, 2, 3, 4};
5+
int old_a[5] = {0, 1, 2, 3, 4};
6+
7+
// HAVOC ARRAY SLICE
8+
__CPROVER_havoc_slice(&a[2] - 1, 2 * sizeof(*a));
9+
10+
// POSTCONDITIONS
11+
__CPROVER_assert(a[0] == old_a[0], "expecting SUCCESS");
12+
__CPROVER_assert(a[1] == old_a[1], "expecting FAILURE");
13+
__CPROVER_assert(a[2] == old_a[2], "expecting FAILURE");
14+
__CPROVER_assert(a[3] == old_a[3], "expecting SUCCESS");
15+
__CPROVER_assert(a[4] == old_a[4], "expecting SUCCESS");
16+
return;
17+
}

‎regression/cbmc/havoc_slice/test_array_slice_2.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test_array_slice_2.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^.*expecting FAILURE: SUCCESS$
9+
^.*expecting SUCCESS: FAILURE$
10+
^.*dereference .*: FAILURE$

‎regression/cbmc/havoc_slice/test_array_symbolic_size.c

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
#include <stdint.h>
2+
#include <stdlib.h>
3+
4+
// byte-level comparison
5+
#define CHECK_SLICE(A, OLD_A, I, IDX, HAVOC_SIZE) \
6+
{ \
7+
__CPROVER_assert( \
8+
!(IDX <= I && I <= IDX + HAVOC_SIZE) | A[I] == OLD_A[I], \
9+
"expecting FAILURE"); \
10+
\
11+
__CPROVER_assert( \
12+
(IDX <= I && I <= IDX + HAVOC_SIZE) | A[I] == OLD_A[I], \
13+
"expecting SUCCESS"); \
14+
}
15+
16+
// ARRAY WITH SYMBOLIC SIZE.
17+
void main(void)
18+
{
19+
// INITIALIZE
20+
uint32_t size;
21+
__CPROVER_assume(5 == size);
22+
23+
char a[size];
24+
char old_a[size];
25+
26+
__CPROVER_array_set(a, 0);
27+
__CPROVER_array_set(old_a, 0);
28+
29+
uint32_t idx;
30+
__CPROVER_assume(idx < size);
31+
32+
uint32_t havoc_size;
33+
__CPROVER_assume(1 <= havoc_size && havoc_size <= size);
34+
__CPROVER_assume(idx + havoc_size <= size);
35+
36+
// HAVOC SINGLE CELL
37+
__CPROVER_havoc_slice(&a[idx], havoc_size);
38+
39+
// POSTCONDITIONS
40+
CHECK_SLICE(a, old_a, 0, idx, havoc_size);
41+
CHECK_SLICE(a, old_a, 1, idx, havoc_size);
42+
CHECK_SLICE(a, old_a, 2, idx, havoc_size);
43+
CHECK_SLICE(a, old_a, 3, idx, havoc_size);
44+
CHECK_SLICE(a, old_a, 4, idx, havoc_size);
45+
return;
46+
}

‎regression/cbmc/havoc_slice/test_array_symbolic_size.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE thorough-paths thorough-smt-backend
2+
test_array_symbolic_size.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^.*expecting FAILURE: SUCCESS$
9+
^.*expecting SUCCESS: FAILURE$
10+
^.*dereference .*: FAILURE$

‎regression/cbmc/havoc_slice/test_nondet_conditional.c

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
void main(void)
2+
{
3+
// HAVOC through nondet conditional
4+
typedef struct
5+
{
6+
int i;
7+
int j;
8+
} st;
9+
int i = 10;
10+
int old_i = 10;
11+
st s = {20, 30};
12+
st old_s = s;
13+
14+
_Bool c;
15+
16+
int *p = c ? &i : &s.i;
17+
18+
__CPROVER_havoc_slice(p, sizeof(*p));
19+
20+
if(c)
21+
{
22+
__CPROVER_assert(i == old_i, "expecting FAILURE");
23+
__CPROVER_assert(s.i == old_s.i, "expecting SUCCESS");
24+
__CPROVER_assert(s.j == old_s.j, "expecting SUCCESS");
25+
}
26+
else
27+
{
28+
__CPROVER_assert(i == old_i, "expecting SUCCESS");
29+
__CPROVER_assert(s.i == old_s.i, "expecting FAILURE");
30+
__CPROVER_assert(s.j == old_s.j, "expecting SUCCESS");
31+
}
32+
33+
return;
34+
}

‎regression/cbmc/havoc_slice/test_nondet_conditional.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test_nondet_conditional.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$
7+
--
8+
^.*expecting FAILURE: SUCCESS$
9+
^.*expecting SUCCESS: FAILURE$
10+
^.*dereference .*: FAILURE$

0 commit comments

Comments
 (0)