Skip to content

Commit 2bba498

Browse files
tautschnigtautschnig
authored
Merge pull request #8627 from tautschnig/simp_mult_offset
Simplify multiple-of-element size access to arrays
2 parents c524281 + 78839a9 commit 2bba498

File tree

12 files changed

+510
-19
lines changed

12 files changed

+510
-19
lines changed

‎regression/cbmc/Array_operations4/main.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
int main()
2+
{
3+
char source[8];
4+
int int_source[2];
5+
int target[4];
6+
int n;
7+
if(n >= 0 && n < 3)
8+
{
9+
__CPROVER_array_replace(&target[n], source);
10+
__CPROVER_array_replace(&target[n], int_source);
11+
__CPROVER_assert(target[n] == int_source[0], "");
12+
__CPROVER_assert(target[n + 1] == int_source[1], "");
13+
}
14+
}

‎regression/cbmc/Array_operations4/program-only.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE paths-lifo-expected-failure
2+
main.c
3+
--program-only
4+
target!0@1#2 ==
5+
target!0@1#3 ==
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
byte_update_
10+
--
11+
This test demonstrates that we can simplify byte_update expressions to, e.g.,
12+
WITH expressions.
13+
Disabled for paths-lifo mode, which does not support --program-only.

‎regression/cbmc/Array_operations4/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--

‎regression/cbmc/havoc_slice/functional.c

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
#include <stdint.h>
2+
#include <stdlib.h>
3+
4+
/*
5+
6+
When translating to SMT, structs are represented by algebraic datatypes (ADTs)
7+
and arrays of structs by arrays of ADTs.
8+
9+
When forming a pointer ranging over an array of struct using a nondeterministic
10+
index, the pointer offset appears completely non-deterministic to CBMC, and
11+
in-place updates made using assignments or __CPROVER_array_replace then expand
12+
into large sequences of byte_updates ranging over the whole array.
13+
14+
If we could somehow track the fact that a pointer formed using arr[i] is still
15+
aligned on array cell boundaries, i.e. is of the form i*sizeof(T) where T is the
16+
type of the array, across intermediate variables and assignments then we would
17+
be able to encode these cases in SMT more optimally:
18+
19+
T arr[N];
20+
size_t i = nondetd_size_t();
21+
if (i < N) {
22+
T *ai = &arr[i];
23+
T v = nondet_T();
24+
*ai = v;
25+
// here we have ai of the form &a[0] + i*sizeof(T) assigned with a value of
26+
size sizeof(T)
27+
// can be modeled as a functional array update at index i.
28+
}
29+
30+
size_t k = nondet_size_t();
31+
if (k < N) {
32+
size_t S = N-k;
33+
T nondet[S];
34+
T *ak = &a[k];
35+
__CPROVER_array_replace(ak, nondet);
36+
// here we have ai of the form &a[0] + k*sizeof(T) updated in place with a
37+
value of size k*sizeof(T)
38+
// can be modeled as a functional slice update at index k with k elements.
39+
}
40+
41+
At the moment these constructs blow up with --z3 and --bitwuzla
42+
*/
43+
44+
// #define N 4 // use 8, 16, ... to see the blowup
45+
#define K 4
46+
47+
typedef struct
48+
{
49+
int32_t coeffs[N];
50+
} vec_N;
51+
52+
typedef struct
53+
{
54+
vec_N vec[K];
55+
} vec_K_N;
56+
57+
unsigned int __VERIFIER_nondet_unsigned_int();
58+
vec_N __VERIFIER_nondet_vec_N();
59+
60+
int main(void)
61+
{
62+
vec_K_N *v = malloc(sizeof(vec_K_N));
63+
__CPROVER_assume(v);
64+
65+
unsigned int i = __VERIFIER_nondet_unsigned_int();
66+
67+
// models a nondet loop step from an arbitrary state
68+
if(i < K)
69+
{
70+
#ifdef ASSIGN_DIRECT
71+
// nondet assignment without indirection through a
72+
// simplifies to a functional update
73+
v->vec[i] = __VERIFIER_nondet_vec_N();
74+
#endif
75+
76+
// simulates how symex models argument passing for a function call
77+
vec_N *__arg = &v->vec[i];
78+
vec_N *a = __arg;
79+
80+
#ifdef ASSIGN
81+
// nondet assignment with indirection through a
82+
// currently does NOT simplifies to a functional update but ultimately
83+
// should
84+
*a = __VERIFIER_nondet_vec_N();
85+
#endif
86+
87+
#ifdef SLICE_BYTES
88+
// Modeled as a byte slice operation without indirection
89+
// does NOT simplify to a functional array update due to lack of pattern
90+
// matching on the pointer offset expression.
91+
// We could realize the pointer offset is of the form i*16 and that the
92+
// new value is of size 16 too but we currently don't.
93+
char nondet[sizeof(vec_N)];
94+
__CPROVER_array_replace((char *)a, nondet);
95+
#endif
96+
97+
#ifdef SLICE_TYPED
98+
// Modeled as a typed slice operation without indirection.
99+
// Does NOT simplify to a functional array update due to lack of pattern
100+
// matching on the pointer offset expression and types.
101+
// We could realize the pointer offset is of the form i*16 and that the
102+
// new value is of size 16 too but we currently don't.
103+
vec_N nondet[1];
104+
__CPROVER_array_replace(a, nondet);
105+
#endif
106+
__CPROVER_assert(a->coeffs[0] > 0, "expected to fail");
107+
}
108+
return 0;
109+
}

‎regression/cbmc/havoc_slice/functional.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE broken-cprover-smt-backend no-new-smt
2+
functional.c
3+
-DN=4 -DASSIGN_DIRECT
4+
^VERIFICATION FAILED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/cbmc/havoc_slice/functional_assign.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
functional.c
3+
-DN=4 -DASSIGN --program-only
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
byte_update
8+
--
9+
We want these tests not to produce any byte_update expressions, but instead want
10+
updates at specific array indices.

‎regression/cbmc/havoc_slice/functional_assign_direct.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
functional.c
3+
-DN=4 -DASSIGN_DIRECT --program-only
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
byte_update
8+
--
9+
We want these tests not to produce any byte_update expressions, but instead want
10+
updates at specific array indices.

‎regression/cbmc/havoc_slice/functional_slice_bytes.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
functional.c
3+
-DN=4 -DSLICE_BYTES --program-only
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
byte_update
8+
--
9+
We want these tests not to produce any byte_update expressions, but instead want
10+
updates at specific array indices.

‎regression/cbmc/havoc_slice/functional_slice_typed.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
functional.c
3+
-DN=4 -DSLICE_TYPED --program-only
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
byte_update
8+
--
9+
We want these tests not to produce any byte_update expressions, but instead want
10+
updates at specific array indices.

‎regression/validate-trace-xml-schema/check.py

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,9 +35,14 @@
3535
['show_properties1', 'test.desc'],
3636
# program-only instead of trace
3737
['vla1', 'program-only.desc'],
38+
['Array_operations4', 'program-only.desc'],
3839
['Pointer_Arithmetic19', 'test.desc'],
3940
['Quantifiers-simplify', 'simplify_not_forall.desc'],
4041
['array-cell-sensitivity15', 'test.desc'],
42+
['havoc_slice', 'functional_assign.desc'],
43+
['havoc_slice', 'functional_assign_direct.desc'],
44+
['havoc_slice', 'functional_slice_bytes.desc'],
45+
['havoc_slice', 'functional_slice_typed.desc'],
4146
['saturating_arithmetric', 'output-formula.desc'],
4247
# these test for invalid command line handling
4348
['bad_option', 'test_multiple.desc'],

0 commit comments

Comments
 (0)