Adding large-step encoding for CHCs in CProver (no [required] changes to the solver)

regression/cprover/large_step/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cprover>"
+)

regression/cprover/large_step/Makefile

@@ -0,0 +1,14 @@
+default: test-no-p
+
+include ../../../src/config.inc
+include ../../../src/common
+
+test:
+	@../../test.pl -e -p -c '../../../../src/cprover/cprover --large-step'
+
+test-no-p:
+	@../../test.pl -e -c '../../../../src/cprover/cprover --large-step'
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/cprover/large_step/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/large_step/arrays/array1.desc

@@ -0,0 +1,14 @@
+CORE
+array1.c
+--text --solve --inline --no-safety
+^EXIT=10$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(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/large_step/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/large_step/arrays/array2.desc

@@ -0,0 +1,11 @@
+CORE
+array2.c
+--text --solve --inline --no-safety
+^EXIT=10$
+^SIGNAL=0$
+^\(\d+\) ∀ ς : state \. \(S13\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S14\(ς\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::i❞\)|cast\(ς\(❝main::1::i❞\), signedbv\[64\]\))\)\) = ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::j❞\)|cast\(ς\(❝main::1::j❞\), signedbv\[64\]\))\)\)\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::i❞\)|cast\(ς\(❝main::1::i❞\), signedbv\[64\]\))\)\) = ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::k❞\)|cast\(ς\(❝main::1::k❞\), signedbv\[64\]\))\)\)\)$
+^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
+^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
+--

regression/cprover/large_step/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/large_step/arrays/array4.desc

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

regression/cprover/large_step/arrays/array_literal1.c

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

regression/cprover/large_step/arrays/array_literal1.desc

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

regression/cprover/large_step/arrays/array_literal2.c

@@ -0,0 +1,8 @@
+int array[] = {'a', 'b', 'c', 'd', 'e', 'f'};
+
+int main()
+{
+  int i;
+  if(i >= 0 && i <= 5)
+    __CPROVER_assert(array[i] == 'a' + i, "property 1"); // passes
+}

regression/cprover/large_step/arrays/array_r_ok1.c

@@ -0,0 +1,7 @@
+int main()
+{
+  unsigned char array[10];
+  __CPROVER_assert(__CPROVER_r_ok(array, 10), "property 1");
+  unsigned char *array_ptr = array;
+  __CPROVER_assert(__CPROVER_r_ok(array_ptr, 10), "property 2");
+}

regression/cprover/large_step/arrays/array_r_ok1.desc

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

regression/cprover/large_step/arrays/array_set1.c

@@ -0,0 +1,8 @@
+int array[10];
+
+int main()
+{
+  __CPROVER_array_set(array, 123);
+  __CPROVER_assert(array[5l] == 123, "property 1"); // passes
+  return 0;
+}

regression/cprover/large_step/arrays/array_set1.desc

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

regression/cprover/large_step/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/large_step/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/large_step/arrays/iterate_over_array2.c

@@ -0,0 +1,31 @@
+#define size_t __CPROVER_size_t
+#define false 0
+#define true 1
+
+_Bool find_zero(const void *const array, const size_t array_len)
+{
+  const unsigned char *array_bytes = array;
+
+  // iterate over array
+  for(size_t i = 0; i < array_len; ++i)
+    // clang-format off
+    __CPROVER_loop_invariant(i >= 0 && i <= array_len)
+    __CPROVER_loop_invariant(__CPROVER_POINTER_OFFSET(array_bytes) == 0)
+    __CPROVER_loop_invariant(__CPROVER_r_ok(array_bytes, array_len))
+    // clang-format on
+    {
+      if(array_bytes[i] == 0)
+      {
+        return true;
+      }
+    }
+
+  return false;
+}
+
+int main()
+{
+  unsigned char array[10];
+  size_t array_len = 10;
+  find_zero(array, array_len);
+}

regression/cprover/large_step/arrays/iterate_over_array2.desc

@@ -0,0 +1,7 @@
+CORE
+iterate_over_array2.c
+--safety
+^EXIT=0$
+^SIGNAL=0$
+^\[find_zero\.pointer\.1\] line \d+ pointer .* safe: SUCCESS$
+--

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

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

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

@@ -0,0 +1,20 @@
+// Function: aws_array_eq_c_str
+// Source: aws-c-common/source/byte_buf.c
+
+#include <aws/common/byte_buf.h>
+
+// bool aws_array_eq_c_str(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(array, array_len, c_str);
+
+  return 0;
+}

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

@@ -0,0 +1,6 @@
+KNOWNBUG
+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/large_step/aws-c-common/aws_array_eq_c_str_ignore_case_contract.c

@@ -0,0 +1,20 @@
+// Function: aws_array_eq_c_str_ignore_case
+// Source: aws-c-common/source/byte_buf.c
+
+#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/large_step/aws-c-common/aws_array_eq_ignore_case.desc

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

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

@@ -0,0 +1,23 @@
+// Function: aws_array_eq_ignore_case
+// Source: aws-c-common/source/byte_buf.c
+
+#include <aws/common/byte_buf.h>
+
+// bool aws_array_eq_ignore_case(
+//    const void *const array_a,
+//    const size_t len_a,
+//    const void *const array_b,
+//    const size_t len_b)
+
+int main()
+{
+  const void *array_a, *array_b;
+  size_t len_a, len_b;
+
+  __CPROVER_assume(__CPROVER_r_ok(array_a, len_a));
+  __CPROVER_assume(__CPROVER_r_ok(array_b, len_b));
+
+  aws_array_eq_ignore_case(array_a, len_a, array_b, len_b);
+
+  return 0;
+}

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

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

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

@@ -0,0 +1,15 @@
+// Function: aws_hash_table_clear
+// Source: source/hash_table.c
+
+#include <aws/common/hash_table.h>
+
+// void aws_hash_table_clear(struct aws_hash_table *map)
+
+int main()
+{
+  struct aws_hash_table *map;
+
+  aws_hash_table_clear(map);
+
+  return 0;
+}

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

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

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

@@ -0,0 +1,20 @@
+// Function: aws_hash_table_eq
+// Source: source/hash_table.c
+
+#include <aws/common/hash_table.h>
+
+// bool aws_hash_table_eq(
+//   const struct aws_hash_table *a,
+//   const struct aws_hash_table *b,
+//   aws_hash_callback_eq_fn *value_eq)
+
+int main()
+{
+  const struct aws_hash_table *a;
+  const struct aws_hash_table *b;
+  aws_hash_callback_eq_fn *value_eq;
+
+  aws_hash_table_eq(a, b, value_eq);
+
+  return 0;
+}

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

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

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

@@ -0,0 +1,20 @@
+// Function: aws_hash_table_foreach
+// Source: source/hash_table.c
+
+#include <aws/common/hash_table.h>
+
+// int aws_hash_table_foreach(
+//   struct aws_hash_table *map,
+//   int (*callback)(void *context, struct aws_hash_element *pElement),
+//   void *context)
+
+int main()
+{
+  struct aws_hash_table *map;
+  int (*callback)(void *context, struct aws_hash_element *pElement);
+  void *context;
+
+  aws_hash_table_foreach(map, callback, context);
+
+  return 0;
+}

regression/cprover/large_step/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/large_step/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/large_step/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/large_step/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/large_step/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;
+}