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

Diff for: 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

Diff for: 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;
+}

Diff for: 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.

Diff for: 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.

Diff for: regression/cbmc/Quantifiers-unbounded-array-overflow/main.c

@@ -0,0 +1,94 @@
+#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);
+  __CPROVER_assume(size <= __CPROVER_max_malloc_size / sizeof(int));
+  // we remove this assumption, which in turn allows to cause an integer
+  // overflow in the loop body when computing 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);
+
+  // 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)
+  });
+}

Diff for: 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.

Diff for: 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)
+  });
+}

Diff for: 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

Diff for: src/solvers/flattening/boolbv_quantifier.cpp

@@ -6,12 +6,13 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#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)
@@ -280,12 +281,119 @@ literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
   return quantifier_list.back().l;
 }
 
-void boolbvt::finish_eager_conversion_quantifiers()
+/// Eliminate the quantifier in \p q_expr via E-matching in \p context_map.
+/// \return Quantifier-free expression, if quantifier elimination was
+///   successful, else nullopt.
+static std::optional<exprt> finish_one_quantifier(
+  const quantifier_exprt &q_expr,
+  const std::unordered_map<const exprt, bvt, irep_hash> &context_map)
 {
-  if(quantifier_list.empty())
-    return;
+  if(q_expr.variables().size() > 1)
+  {
+    // Rewrite Qx,y.P(x,y) as Qy.Qx.P(x,y), just like
+    // eager_quantifier_instantiation does.
+    auto new_variables = q_expr.variables();
+    new_variables.pop_back();
+    quantifier_exprt new_expression{
+      q_expr.id(),
+      q_expr.variables().back(),
+      quantifier_exprt{q_expr.id(), new_variables, q_expr.where()}};
+    return finish_one_quantifier(new_expression, context_map);
+  }
+
+  // find the contexts in which the bound variable is used
+  const irep_idt &bound_variable_id = q_expr.symbol().get_identifier();
+  bool required_context = false;
+  std::unordered_set<index_exprt, irep_hash> index_contexts;
+  auto context_finder =
+    [&bound_variable_id, &required_context, &index_contexts](const exprt &e) {
+      if(auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(e))
+      {
+        required_context |= bound_variable_id == symbol_expr->get_identifier();
+      }
+      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())
+    return {};
+
+  // match the contexts against expressions that we have cached
+  std::unordered_set<exprt, irep_hash> instantiation_candidates;
+  for(const auto &cache_entry : context_map)
+  {
+    // 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())
+    return {};
+
+  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));
+  }
 
-  // we do not yet have any elaborate post-processing
+  if(q_expr.id() == ID_exists)
+    return disjunction(instantiations);
+  else
+    return conjunction(instantiations);
+}
+
+void boolbvt::finish_eager_conversion_quantifiers()
+{
   for(const auto &q : quantifier_list)
-    conversion_failed(q.expr);
+  {
+    auto result_opt =
+      finish_one_quantifier(to_quantifier_expr(q.expr), bv_cache);
+    if(!result_opt.has_value())
+    {
+      conversion_failed(q.expr);
+      continue;
+    }
+
+    // Nested quantifiers may yield additional entries in quantifier_list via
+    // convert; the range-for remains safe to use as long as quantifier_list is
+    // a std::list.
+    literalt result_lit = convert(*result_opt);
+    prop.l_set_to_true(prop.lequal(q.l, result_lit));
+  }
 }