Quantifier instantiation via simplistic E-matching

doc/cprover-manual/cbmc-assertions.md

@@ -82,12 +82,7 @@ int foo(int a, int b) {
 }
 ```
 
-A future release of CPROVER will support using these pre and
-postconditions to create a function contract, which can be used for
-modular verification.
-
-
-Future CPROVER releases will support explicit quantifiers with a syntax
+CPROVER supports explicit quantifiers with a syntax
 that resembles Spec\#:
 
 ```C

regression/cbmc/Quantifiers-invalid-var-range/test.desc

@@ -1,13 +1,11 @@
-KNOWNBUG broken-smt-backend
+CORE no-new-smt
 main.c
 
 ^\*\* Results:$
-^\*\* 0 of 1 failed
+^\*\* 0 of \d+ failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This produces the expected verification result, but actually ignores some
-quantifiers.

regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.c

@@ -0,0 +1,20 @@
+int main()
+{
+  int a[2][2];
+
+  __CPROVER_assume(__CPROVER_forall {
+    unsigned i;
+    __CPROVER_forall
+    {
+      unsigned j;
+      a[i % 2][j % 2] == (i % 2) + (j % 2)
+    }
+  });
+
+  assert(a[0][0] == 0);
+  assert(a[0][1] == 1);
+  assert(a[1][0] == 1);
+  assert(a[1][1] == 2);
+
+  return 0;
+}

regression/cbmc/Quantifiers-two-dimension-array/no-upper-bound.desc

@@ -0,0 +1,11 @@
+CORE broken-cprover-smt-backend no-new-smt
+no-upper-bound.c
+--max-field-sensitivity-array-size 0
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+E-matching does not yet handle array expressions (which field sensitivity
+produces for small fixed-size arrays), so we disable field sensitivity.

regression/cbmc/Quantifiers-type/test.desc

@@ -1,14 +1,11 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend no-new-smt
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] line 12 assertion tmp_if_expr(\$\d+)?: FAILURE$
-^\*\* 1 of 1 failed
+^\[main.assertion.1\] line 10 assertion a\[(\(signed (long )*int\))?0\] == 10 && a\[(\(signed (long )*int\))?1\] == 10: FAILURE$
+^\*\* 1 of \d+ failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
---
-This produces the expected verification result, but actually ignores some
-quantifiers.

regression/cbmc/Quantifiers-unbounded-array-overflow/main.c

@@ -0,0 +1,102 @@
+#include <assert.h>
+#include <limits.h>
+#include <stdlib.h>
+#include <string.h>
+
+size_t nondet_size_t();
+
+#if UINT_MAX < SIZE_MAX
+#  define SMALLER_TYPE int
+#else
+#  define SMALLER_TYPE short
+#endif
+
+// The model has an overflow, falsified instantly with SAT,
+// takes forever with z3 because of the quantifiers
+int main()
+{
+  size_t size = nondet_size_t();
+  __CPROVER_assume(0 < size);
+  __CPROVER_assume(size <= __CPROVER_max_malloc_size / sizeof(SMALLER_TYPE));
+  // we remove this assumption, which in turn allows to cause an integer
+  // overflow in the loop body when computing i*2, because we would end up
+  // comparing i*2, which does not overflow on size_t, to the overflowed
+  // (wrap-around) value when i*2 was assigned to the int-typed array element
+  // __CPROVER_assume(size < INT_MAX / 2);
+  size_t nof_bytes = size * sizeof(SMALLER_TYPE);
+  SMALLER_TYPE *arr = malloc(nof_bytes);
+  __CPROVER_assume(arr);
+  __CPROVER_array_set(arr, 0);
+
+  // None of this should overflow because initially arr[j] == 0 for all j
+
+  // the original loop
+  // size_t i = 0;
+  // while (i < size)
+  // __CPROVER_loop_invariant(i <= size)
+  // __CPROVER_loop_invariant(__CPROVER_forall {size_t j; !(j < i) || (arr[j] == j * 2) })
+  // __CPROVER_loop_invariant(__CPROVER_forall {size_t j; !(i <= j && j < size) || (arr[j] == 0) })
+  // {
+  //     arr[i] = arr[i] + 2 * i;
+  //     i += 1;
+  // }
+
+  size_t i = 0;
+
+  // check base case
+  assert(i <= size);
+  assert(__CPROVER_forall {
+    size_t j;
+    !(j < i) || (arr[j] == j * 2)
+  });
+  assert(__CPROVER_forall {
+    size_t j;
+    !(i <= j && j < size) || (arr[j] == 0)
+  });
+
+  // jump to a nondet state
+  i = nondet_size_t();
+  __CPROVER_havoc_object(arr);
+
+  // assume loop invariant
+  __CPROVER_assume(i <= size);
+  __CPROVER_assume(i <= size);
+  __CPROVER_assume(__CPROVER_forall {
+    size_t j;
+    !(j < i) || (arr[j] == j * 2)
+  });
+  __CPROVER_assume(__CPROVER_forall {
+    size_t j;
+    !(i <= j && j < size) || (arr[j] == 0)
+  });
+
+  size_t old_i = i;
+  if(i < size)
+  {
+    arr[i] = arr[i] + i * 2;
+    i += 1;
+
+    // check loop invariant post loop step
+    assert(i <= size);
+    assert(__CPROVER_forall {
+      size_t j;
+      !(j < i) || (arr[j] == j * 2)
+    });
+    assert(__CPROVER_forall {
+      size_t j;
+      !(i <= j && j < size) || (arr[j] == 0)
+    });
+    __CPROVER_assume(0); // stop progress
+  }
+
+  // check that the loop invariant holds post loop
+  assert(__CPROVER_forall {
+    size_t j;
+    !(j < i) || (arr[j] == j * 2)
+  });
+
+  assert(__CPROVER_forall {
+    size_t j;
+    !(i <= j && j < size) || (arr[j] == 0)
+  });
+}

regression/cbmc/Quantifiers-unbounded-array-overflow/test.desc

@@ -0,0 +1,14 @@
+CORE thorough-z3-smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--no-standard-checks
+^\[main.assertion.5\] line 81 assertion __CPROVER_forall \{ size_t j; !\(j < i\) \|\| \(arr\[j\] == j \* 2\) \}: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Uses --no-standard-checks to contain verification time with MiniSat; with
+CaDiCaL this completes in under 5 seconds either way. Takes an unknown amount of
+time (has never been run to completition) when using Z3.

regression/cbmc/Quantifiers-unbounded-array/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <limits.h>
+#include <stdlib.h>
+
+size_t nondet_size_t();
+
+int main()
+{
+  size_t size = nondet_size_t();
+  __CPROVER_assume(0 < size);
+
+  // avoids overflows in the loop body on i * 2
+  __CPROVER_assume(size < INT_MAX / 2);
+  size_t nof_bytes = size * sizeof(int);
+  int *arr = malloc(nof_bytes);
+  __CPROVER_assume(arr);
+  __CPROVER_array_set(arr, 0);
+
+  // jump to a nondet state
+  size_t i = nondet_size_t();
+  __CPROVER_assume(i < size);
+  __CPROVER_havoc_object(arr);
+
+  // assume loop invariant
+  __CPROVER_assume(__CPROVER_forall {
+    size_t j;
+    !(j < i) || (arr[j] == j * 2)
+  });
+  __CPROVER_assume(__CPROVER_forall {
+    size_t j;
+    !(i <= j && j < size) || (arr[j] == 0)
+  });
+
+  arr[i] = arr[i] + i * 2;
+  i += 1;
+
+  assert(__CPROVER_forall {
+    size_t j;
+    !(i <= j && j < size) || (arr[j] == 0)
+  });
+}

regression/cbmc/Quantifiers-unbounded-array/test.desc

@@ -0,0 +1,8 @@
+CORE broken-cprover-smt-backend no-new-smt
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring