Skip to content

Commit e54a0ee

Browse files
kroeningkroening
committed
add the CHC state encoding
This adds a CHC encoding that uses the concept of an abstract "program state", in contrast to the usual explicit enumeration of the variables that the state comprises.
1 parent c3c999a commit e54a0ee

File tree

600 files changed

+16878
-21
lines changed

Some content is hidden

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

600 files changed

+16878
-21
lines changed

Diff for: ‎.clang-format-ignore

+1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
jbmc/src/miniz/miniz.cpp
2+
src/cprover/wcwidth.c
23
src/nonstd/optional.hpp
34
unit/catch/catch.hpp

Diff for: ‎CMakeLists.txt

+3
Original file line numberDiff line numberDiff line change
@@ -150,6 +150,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
150150
"$<TARGET_FILE:unit>"
151151
"$<TARGET_FILE:goto-harness>"
152152
"$<TARGET_FILE:cbmc>"
153+
"$<TARGET_FILE:cprover>"
153154
"$<TARGET_FILE:crangler>"
154155
"$<TARGET_FILE:driver>"
155156
"$<TARGET_FILE:goto-analyzer>"
@@ -214,6 +215,8 @@ cprover_default_properties(
214215
cbmc
215216
cbmc-lib
216217
cpp
218+
cprover
219+
cprover-lib
217220
crangler
218221
crangler-lib
219222
driver

Diff for: ‎regression/cprover/Makefile

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
default: test-no-p
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
test:
7+
@../test.pl -e -p -c '../../../src/cprover/cprover'
8+
9+
test-no-p:
10+
@../test.pl -e -c '../../../src/cprover/cprover'
11+
12+
clean:
13+
$(RM) tests.log

Diff for: ‎regression/cprover/arrays/array1.c

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
int array[10];
2+
3+
int main()
4+
{
5+
array[1l] = 10;
6+
array[2l] = 20;
7+
__CPROVER_assert(array[1l] == 10, "property 1"); // passes
8+
__CPROVER_assert(array[2l] == 20, "property 2"); // passes
9+
__CPROVER_assert(array[2l] == 30, "property 3"); // fails
10+
}

Diff for: ‎regression/cprover/arrays/array1.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
array1.c
3+
--text --solve --inline --no-safety
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, 1\):=10\]\)$
7+
^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, 2\):=20\]\)$
8+
^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, 1\)\) = 10\)$
9+
^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 20\)$
10+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 30\)$
11+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
12+
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
13+
^\[main\.assertion\.3\] line \d+ property 3: REFUTED$
14+
--

Diff for: ‎regression/cprover/arrays/array2.c

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
int array[10];
4+
int i, j, k;
5+
__CPROVER_assume(i == j);
6+
__CPROVER_assert(array[i] == array[j], "property 1"); // passes
7+
__CPROVER_assert(array[i] == array[k], "property 2"); // fails
8+
}

Diff for: ‎regression/cprover/arrays/array2.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
array2.c
3+
--text --solve --inline --no-safety
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\(\d+\) ∀ ς : state \. \(S23\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)$
7+
^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
8+
^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
9+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
10+
^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
11+
--

Diff for: ‎regression/cprover/arrays/array4.c

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
int main()
2+
{
3+
int a[100];
4+
int *p = a;
5+
__CPROVER_assert(p[23] == a[23], "property 1"); // should pass
6+
return 0;
7+
}

Diff for: ‎regression/cprover/arrays/array4.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
array4.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
--

Diff for: ‎regression/cprover/arrays/array_literal1.c

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int array[10] = {0, 1, 2, 3, 4};
2+
3+
int main()
4+
{
5+
__CPROVER_assert(array[0l] == 0, "property 1"); // passes
6+
__CPROVER_assert(array[1l] == 1, "property 2"); // passes
7+
return 0;
8+
}

Diff for: ‎regression/cprover/arrays/array_literal1.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
array_literal1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
8+
--

Diff for: ‎regression/cprover/arrays/array_literal2.c

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int array[] = {'a', 'b', 'c', 'd', 'e', 'f'};
2+
3+
int main()
4+
{
5+
int i;
6+
if(i >= 0 && i <= 5)
7+
__CPROVER_assert(array[i] == 'a' + i, "property 1"); // passes
8+
}

Diff for: ‎regression/cprover/arrays/array_r_ok1.c

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
int main()
2+
{
3+
unsigned char array[10];
4+
__CPROVER_assert(__CPROVER_r_ok(array, 10), "property 1");
5+
unsigned char *array_ptr = array;
6+
__CPROVER_assert(__CPROVER_r_ok(array_ptr, 10), "property 2");
7+
}

Diff for: ‎regression/cprover/arrays/array_r_ok1.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
array_r_ok1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
8+
--

Diff for: ‎regression/cprover/arrays/array_set1.c

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int array[10];
2+
3+
int main()
4+
{
5+
__CPROVER_array_set(array, 123);
6+
__CPROVER_assert(array[5l] == 123, "property 1"); // passes
7+
return 0;
8+
}

Diff for: ‎regression/cprover/arrays/array_set1.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
KNOWNBUG
2+
array_set1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
7+
--

Diff for: ‎regression/cprover/arrays/iterate_over_array1.c

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
int array[10];
2+
3+
int main()
4+
{
5+
for(__CPROVER_size_t i = 0; i < sizeof(array) / sizeof(int); i++)
6+
array[i] = 0;
7+
}

Diff for: ‎regression/cprover/arrays/iterate_over_array1.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
iterate_over_array1.c
3+
--safety
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main\.array_bounds\.1\] line \d+ array bounds in array\[.*i\]: SUCCESS$
7+
--

Diff for: ‎regression/cprover/arrays/iterate_over_array2.c

+31
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
#define size_t __CPROVER_size_t
2+
#define false 0
3+
#define true 1
4+
5+
_Bool find_zero(const void *const array, const size_t array_len)
6+
{
7+
const unsigned char *array_bytes = array;
8+
9+
// iterate over array
10+
for(size_t i = 0; i < array_len; ++i)
11+
// clang-format off
12+
__CPROVER_loop_invariant(i >= 0 && i <= array_len)
13+
__CPROVER_loop_invariant(__CPROVER_POINTER_OFFSET(array_bytes) == 0)
14+
__CPROVER_loop_invariant(__CPROVER_r_ok(array_bytes, array_len))
15+
// clang-format on
16+
{
17+
if(array_bytes[i] == 0)
18+
{
19+
return true;
20+
}
21+
}
22+
23+
return false;
24+
}
25+
26+
int main()
27+
{
28+
unsigned char array[10];
29+
size_t array_len = 10;
30+
find_zero(array, array_len);
31+
}

Diff for: ‎regression/cprover/arrays/iterate_over_array2.desc

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
iterate_over_array2.c
3+
--safety
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[find_zero\.pointer\.1\] line \d+ pointer .* safe: SUCCESS$
7+
--

Diff for: ‎regression/cprover/aws-c-common/aws_array_eq_c_str.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
KNOWNBUG
2+
aws_array_eq_c_str_contract.c
3+
-I aws-c-common/include aws-c-common/source/byte_buf.c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--

Diff for: ‎regression/cprover/aws-c-common/aws_array_eq_c_str_contract.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Function: aws_array_eq_c_str
2+
// Source: aws-c-common/source/byte_buf.c
3+
4+
#include <aws/common/byte_buf.h>
5+
6+
// bool aws_array_eq_c_str(const void *const array, const size_t array_len, const char *const c_str)
7+
8+
int main()
9+
{
10+
const void *array;
11+
size_t array_len;
12+
const char *c_str;
13+
14+
__CPROVER_assume(__CPROVER_r_ok(array, array_len));
15+
__CPROVER_assume(__CPROVER_is_cstring(c_str));
16+
17+
aws_array_eq_c_str(array, array_len, c_str);
18+
19+
return 0;
20+
}

Diff for: ‎regression/cprover/aws-c-common/aws_array_eq_c_str_ignore_case.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
KNOWNBUG
2+
aws_array_eq_c_str_ignore_case_contract.c
3+
--safety aws-c-common/source/byte_buf.c -I aws-c-common/include
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--

Diff for: ‎regression/cprover/aws-c-common/aws_array_eq_c_str_ignore_case_contract.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Function: aws_array_eq_c_str_ignore_case
2+
// Source: aws-c-common/source/byte_buf.c
3+
4+
#include <aws/common/byte_buf.h>
5+
6+
// bool aws_array_eq_c_str_ignore_case(const void *const array, const size_t array_len, const char *const c_str)
7+
8+
int main()
9+
{
10+
const void *array;
11+
size_t array_len;
12+
const char *c_str;
13+
14+
__CPROVER_assume(__CPROVER_r_ok(array, array_len));
15+
__CPROVER_assume(__CPROVER_is_cstring(c_str));
16+
17+
aws_array_eq_c_str_ignore_case(array, array_len, c_str);
18+
19+
return 0;
20+
}

Diff for: ‎regression/cprover/aws-c-common/aws_array_eq_ignore_case.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
KNOWNBUG
2+
aws_array_eq_ignore_case_contract.c
3+
--safety aws-c-common/source/byte_buf.c -I aws-c-common/include
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--

Diff for: ‎regression/cprover/aws-c-common/aws_array_eq_ignore_case_contract.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// Function: aws_array_eq_ignore_case
2+
// Source: aws-c-common/source/byte_buf.c
3+
4+
#include <aws/common/byte_buf.h>
5+
6+
// bool aws_array_eq_ignore_case(
7+
// const void *const array_a,
8+
// const size_t len_a,
9+
// const void *const array_b,
10+
// const size_t len_b)
11+
12+
int main()
13+
{
14+
const void *array_a, *array_b;
15+
size_t len_a, len_b;
16+
17+
__CPROVER_assume(__CPROVER_r_ok(array_a, len_a));
18+
__CPROVER_assume(__CPROVER_r_ok(array_b, len_b));
19+
20+
aws_array_eq_ignore_case(array_a, len_a, array_b, len_b);
21+
22+
return 0;
23+
}

Diff for: ‎regression/cprover/aws-c-common/aws_hash_table_clear.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
KNOWNBUG
2+
aws_hash_table_clear_contract.c
3+
-I aws-c-common/include aws-c-common/source/hash_table.c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--

Diff for: ‎regression/cprover/aws-c-common/aws_hash_table_clear_contract.c

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Function: aws_hash_table_clear
2+
// Source: source/hash_table.c
3+
4+
#include <aws/common/hash_table.h>
5+
6+
// void aws_hash_table_clear(struct aws_hash_table *map)
7+
8+
int main()
9+
{
10+
struct aws_hash_table *map;
11+
12+
aws_hash_table_clear(map);
13+
14+
return 0;
15+
}

Diff for: ‎regression/cprover/aws-c-common/aws_hash_table_eq.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
KNOWNBUG
2+
aws_hash_table_eq_contract.c
3+
-I aws-c-common/include aws-c-common/source/hash_table.c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--

Diff for: ‎regression/cprover/aws-c-common/aws_hash_table_eq_contract.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Function: aws_hash_table_eq
2+
// Source: source/hash_table.c
3+
4+
#include <aws/common/hash_table.h>
5+
6+
// bool aws_hash_table_eq(
7+
// const struct aws_hash_table *a,
8+
// const struct aws_hash_table *b,
9+
// aws_hash_callback_eq_fn *value_eq)
10+
11+
int main()
12+
{
13+
const struct aws_hash_table *a;
14+
const struct aws_hash_table *b;
15+
aws_hash_callback_eq_fn *value_eq;
16+
17+
aws_hash_table_eq(a, b, value_eq);
18+
19+
return 0;
20+
}

Diff for: ‎regression/cprover/aws-c-common/aws_hash_table_foreach.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
KNOWNBUG
2+
aws_hash_table_foreach_contract.c
3+
-I aws-c-common/include aws-c-common/source/hash_table.c
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--

Diff for: ‎regression/cprover/aws-c-common/aws_hash_table_foreach_contract.c

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Function: aws_hash_table_foreach
2+
// Source: source/hash_table.c
3+
4+
#include <aws/common/hash_table.h>
5+
6+
// int aws_hash_table_foreach(
7+
// struct aws_hash_table *map,
8+
// int (*callback)(void *context, struct aws_hash_element *pElement),
9+
// void *context)
10+
11+
int main()
12+
{
13+
struct aws_hash_table *map;
14+
int (*callback)(void *context, struct aws_hash_element *pElement);
15+
void *context;
16+
17+
aws_hash_table_foreach(map, callback, context);
18+
19+
return 0;
20+
}

Diff for: ‎regression/cprover/aws-c-common/setup

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
#!/bin/sh
2+
3+
git clone https://github.com/awslabs/aws-c-common -b v0.6.13
4+
5+
echo "/* nothing */" > aws-c-common/include/aws/common/config.h
6+

Diff for: ‎regression/cprover/aws-c-common/todo/aws_array_list_mem_swap.desc

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
aws_array_list_mem_swap_contract.c
3+
--safety
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--

0 commit comments

Comments
 (0)