state encoding

Author: kroening

.clang-format-ignore

@@ -1,3 +1,4 @@
 jbmc/src/miniz/miniz.cpp
+src/cprover/wcwidth.c
 src/nonstd/optional.hpp
 unit/catch/catch.hpp

regression/cprover/Makefile

@@ -0,0 +1,13 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c '../../../src/cprover/cprover'
+
+tests.log:
+	@../test.pl -e -p -c '../../../src/cprover/cprover'
+
+clean:
+	$(RM) tests.log

regression/cprover/arrays/array1.c

@@ -0,0 +1,10 @@
+int array[10];
+
+int main()
+{
+  array[1l] = 10;
+  array[2l] = 20;
+  __CPROVER_assert(array[1l] == 10, "property 1"); // passes
+  __CPROVER_assert(array[2l] == 20, "property 2"); // passes
+  __CPROVER_assert(array[2l] == 30, "property 3"); // fails
+}

regression/cprover/arrays/array1.desc

@@ -0,0 +1,14 @@
+CORE
+array1.c
+--text --solve
+^EXIT=10$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, 1\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, 2\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, 1\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 20\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, 2\)\) = 30\)$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
+^\[main\.assertion\.3\] line \d+ property 3: REFUTED$
+--

regression/cprover/arrays/array2.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int array[10];
+  int i, j, k;
+  __CPROVER_assume(i == j);
+  __CPROVER_assert(array[i] == array[j], "property 1"); // passes
+  __CPROVER_assert(array[i] == array[k], "property 2"); // fails
+}

regression/cprover/arrays/array2.desc

@@ -0,0 +1,11 @@
+CORE
+array2.c
+--text --solve
+^EXIT=10$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. \(S23\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)$
+^\(\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\]\)\)\)\)$
+^\(\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\]\)\)\)\)$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
+--

regression/cprover/arrays/array4.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int a[100];
+  int *p = a;
+  __CPROVER_assert(p[23] == a[23], "property 1"); // should pass
+  return 0;
+}

regression/cprover/arrays/array4.desc

@@ -0,0 +1,7 @@
+CORE
+array4.c
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+--

regression/cprover/arrays/iterate_over_array1.c

@@ -0,0 +1,7 @@
+int array[10];
+
+int main()
+{
+  for(__CPROVER_size_t i = 0; i < sizeof(array) / sizeof(int); i++)
+    array[i] = 0;
+}

regression/cprover/arrays/iterate_over_array1.desc

@@ -0,0 +1,7 @@
+CORE
+iterate_over_array1.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.array_bounds\.1\] line \d+ array bounds in array\[.*i\]: SUCCESS$
+--

regression/cprover/aws-c-common/aws_array_eq_c_str.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+aws_array_eq_c_str_contract.c
+--safety -I aws-c-common/include aws-c-common/source/byte_buf.c
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/aws_array_eq_c_str_contract.c

@@ -0,0 +1,19 @@
+// Function: aws_array_eq_c_str
+
+#include <aws/common/byte_buf.h>
+
+// bool aws_array_eq_c_str_ignore_case(const void *const array, const size_t array_len, const char *const c_str)
+
+int main()
+{
+  const void *array;
+  size_t array_len;
+  const char *c_str;
+
+  __CPROVER_assume(__CPROVER_r_ok(array, array_len));
+  __CPROVER_assume(__CPROVER_is_cstring(c_str));
+
+  aws_array_eq_c_str_ignore_case(array, array_len, c_str);
+
+  return 0;
+}

regression/cprover/aws-c-common/setup

@@ -0,0 +1,6 @@
+#!/bin/sh
+
+git clone https://github.com/awslabs/aws-c-common -b v0.6.13
+
+echo "/* nothing */" > aws-c-common/include/aws/common/config.h
+

regression/cprover/aws-c-common/todo/aws_array_eq_c_str_ignore_case.desc

@@ -0,0 +1,6 @@
+CORE
+aws_array_eq_c_str_ignore_case_contract.c
+--safety aws-c-common/source/byte_buf.c -I aws-c-common/include
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/aws_array_eq_c_str_ignore_case_contract.c

@@ -0,0 +1,7 @@
+// Function: aws_array_eq_c_str_ignore_case
+// Source: aws-c-common/source/byte_buf.c
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_array_eq_ignore_case.desc

@@ -0,0 +1,6 @@
+CORE
+aws_array_eq_ignore_case_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/aws_array_eq_ignore_case_contract.c

@@ -0,0 +1,6 @@
+// Function: aws_array_eq_ignore_case
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_array_list_mem_swap.desc

@@ -0,0 +1,6 @@
+CORE
+aws_array_list_mem_swap_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/aws_array_list_mem_swap_contract.c

@@ -0,0 +1,6 @@
+// Function: aws_array_list_mem_swap
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_byte_buf_append_with_lookup.desc

@@ -0,0 +1,6 @@
+CORE
+aws_byte_buf_append_with_lookup_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/aws_byte_buf_append_with_lookup_contract.c

@@ -0,0 +1,6 @@
+// Function: aws_byte_buf_append_with_lookup
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_hash_array_ignore_case.desc

@@ -0,0 +1,6 @@
+CORE
+aws_hash_array_ignore_case_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/aws_hash_array_ignore_case_contract.c

@@ -0,0 +1,6 @@
+// Function: aws_hash_array_ignore_case
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_hash_table_clear.desc

@@ -0,0 +1,6 @@
+CORE
+aws_hash_table_clear_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/aws_hash_table_clear_contract.c

@@ -0,0 +1,6 @@
+// Function: aws_hash_table_clear
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_hash_table_eq.desc

@@ -0,0 +1,6 @@
+CORE
+aws_hash_table_eq_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/aws_hash_table_eq_contract.c

@@ -0,0 +1,6 @@
+// Function: aws_hash_table_eq
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/aws_hash_table_foreach.desc

@@ -0,0 +1,6 @@
+CORE
+aws_hash_table_foreach_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/aws_hash_table_foreach_contract.c

@@ -0,0 +1,6 @@
+// Function: aws_hash_table_foreach
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/hashlittle2.desc

@@ -0,0 +1,6 @@
+CORE
+hashlittle2_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/hashlittle2_contract.c

@@ -0,0 +1,6 @@
+// Function: hashlittle2
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/memcpy_using_uint64_impl.desc

@@ -0,0 +1,6 @@
+CORE
+memcpy_using_uint64_impl_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/memcpy_using_uint64_impl_contract.c

@@ -0,0 +1,6 @@
+// Function: memcpy_using_uint64_impl
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/memset_override_0_impl.desc

@@ -0,0 +1,6 @@
+CORE
+memset_override_0_impl_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/memset_override_0_impl_contract.c

@@ -0,0 +1,6 @@
+// Function: memset_override_0_impl
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/memset_using_uint64_impl.desc

@@ -0,0 +1,6 @@
+CORE
+memset_using_uint64_impl_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/memset_using_uint64_impl_contract.c

@@ -0,0 +1,6 @@
+// Function: memset_using_uint64_impl
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/s_find_entry1.desc

@@ -0,0 +1,6 @@
+CORE
+s_find_entry1_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/s_find_entry1_contract.c

@@ -0,0 +1,6 @@
+// Function: s_find_entry1
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/s_get_next_element.desc

@@ -0,0 +1,6 @@
+CORE
+s_get_next_element_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/s_get_next_element_contract.c

@@ -0,0 +1,6 @@
+// Function: s_get_next_element
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/s_sift_down.desc

@@ -0,0 +1,6 @@
+CORE
+s_sift_down_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/s_sift_down_contract.c

@@ -0,0 +1,6 @@
+// Function: s_sift_down
+
+int main()
+{
+  return 0;
+}

regression/cprover/aws-c-common/todo/s_sift_up.desc

@@ -0,0 +1,6 @@
+CORE
+s_sift_up_contract.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cprover/aws-c-common/todo/s_sift_up_contract.c

@@ -0,0 +1,6 @@
+// Function: s_sift_up
+
+int main()
+{
+  return 0;
+}

regression/cprover/basic/assume1.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int x;
+
+  __CPROVER_assume(x >= 10);
+  __CPROVER_assert(x >= 5, "property 1");  // should pass
+  __CPROVER_assert(x >= 15, "property 2"); // should fail
+}

regression/cprover/basic/assume1.desc

@@ -0,0 +1,15 @@
+CORE
+assume1.c
+--text --solve
+^EXIT=10$
+^SIGNAL=0$
+^ \(\d+\) ∀ ς : state \. true ⇒ SInitial\(ς\)$
+^ \(\d+\) S0 = SInitial$
+^ \(\d+\) S1 = S0$
+^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$
+^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
+^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
+^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝return'❞:=nondet::S25\]\)$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
+--

regression/cprover/basic/basic1.c

@@ -0,0 +1,8 @@
+int x;
+
+int main()
+{
+  x = 1;
+  __CPROVER_assert(x == 1, "property 1");
+  return 0;
+}