Quantifier instantiation via simplistic E-matching

Use E-matching on index expressions to instantiate quantifiers when
eager instantiation (aka enumerative instantiation) cannot be applied.

Author: tautschnig

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-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,96 @@
+#include <assert.h>
+#include <limits.h>
+#include <stdlib.h>
+#include <string.h>
+
+size_t nondet_size_t();
+
+// 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);
+  // we remove this assumption, which in turn allows to cause an integer
+  // overflow in the loop body when computing i*2
+  // __CPROVER_assume(size < INT32_MAX / 2);
+  size_t nof_bytes = size * sizeof(int);
+  int *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);
+    // fails with SAT backend but passes with --smt2
+    assert(__CPROVER_forall {
+      size_t j;
+      !(j < i) || (arr[j] == j * 2)
+    });
+    // fails with SAT backend but passes with --smt2
+    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
+  // fails with SAT backend but passes with --smt2
+  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,12 @@
+CORE thorough-z3-smt-backend no-new-smt
+main.c
+--no-standard-checks
+^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

src/solvers/flattening/boolbv_quantifier.cpp

@@ -6,12 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#include "boolbv.h"
-
 #include <util/arith_tools.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/simplify_expr.h>
+#include <util/ssa_expr.h>
+
+#include "boolbv.h"
 
 /// A method to detect equivalence between experts that can contain typecast
 static bool expr_eq(const exprt &expr1, const exprt &expr2)
@@ -285,10 +286,110 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
 
 void boolbvt::finish_eager_conversion_quantifiers()
 {
-  if(quantifier_list.empty())
-    return;
-
-  // we do not yet have any elaborate post-processing
   for(const auto &q : quantifier_list)
-    conversion_failed(q.expr);
+  {
+    const auto &q_expr = to_quantifier_expr(q.expr);
+
+    // we don't yet do nested quantifiers
+    if(can_cast_expr<quantifier_exprt>(q_expr.where()))
+    {
+      conversion_failed(q.expr);
+      continue;
+    }
+
+    // we don't yet handle multiple bound variables
+    if(q_expr.variables().size() > 1)
+    {
+      conversion_failed(q.expr);
+      continue;
+    }
+
+    // find the context in which any of the bound variables are used
+    std::unordered_set<irep_idt, irep_id_hash> bound_variables;
+    for(const auto &v : q_expr.variables())
+      bound_variables.insert(v.get_identifier());
+
+    bool required_context = false;
+    std::unordered_set<index_exprt, irep_hash> index_contexts;
+    auto context_finder =
+      [&bound_variables, &required_context, &index_contexts](const exprt &e) {
+        if(auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(e))
+        {
+          required_context |=
+            bound_variables.find(symbol_expr->get_identifier()) !=
+            bound_variables.end();
+        }
+        else if(required_context)
+        {
+          if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
+          {
+            index_contexts.insert(*index_expr);
+            required_context = false;
+          }
+        }
+      };
+    q_expr.where().visit_post(context_finder);
+    // make sure we found some context for instantiation
+    if(index_contexts.empty())
+    {
+      conversion_failed(q.expr);
+      continue;
+    }
+
+    // match the contexts against expressions that we have cached
+    std::unordered_set<exprt, irep_hash> instantiation_candidates;
+    for(const auto &cache_entry : bv_cache)
+    {
+      // consider re-organizing the cache to use expression ids at the top level
+      if(
+        auto index_expr = expr_try_dynamic_cast<index_exprt>(cache_entry.first))
+      {
+        for(const auto &index_context : index_contexts)
+        {
+          if(
+            auto ssa_context =
+              expr_try_dynamic_cast<ssa_exprt>(index_context.array()))
+          {
+            if(
+              auto ssa_array =
+                expr_try_dynamic_cast<ssa_exprt>(index_expr->array()))
+            {
+              if(
+                ssa_context->get_l1_object_identifier() ==
+                ssa_array->get_l1_object_identifier())
+              {
+                instantiation_candidates.insert(index_expr->index());
+                break;
+              }
+            }
+          }
+          else if(index_expr->array() == index_context.array())
+          {
+            instantiation_candidates.insert(index_expr->index());
+            break;
+          }
+        }
+      }
+    }
+
+    if(instantiation_candidates.empty())
+    {
+      conversion_failed(q.expr);
+      continue;
+    }
+
+    exprt::operandst instantiations;
+    instantiations.reserve(instantiation_candidates.size());
+    for(const auto &e : instantiation_candidates)
+    {
+      exprt::operandst values{
+        {typecast_exprt::conditional_cast(e, q_expr.symbol().type())}};
+      instantiations.push_back(q_expr.instantiate(values));
+    }
+    exprt result_expr = q_expr.id() == ID_exists ? disjunction(instantiations)
+                                                 : conjunction(instantiations);
+    literalt result_lit = convert(result_expr);
+
+    prop.l_set_to_true(prop.lequal(q.l, result_lit));
+  }
 }