SMT cache values and handle z3 errors

regression/cbmc/Float-div3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 main.c
 --floatbv
 ^EXIT=0$

regression/cbmc/Quantifiers-assertion/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-assignment/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-if/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-initialisation2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-not-exists/fixed.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 fixed.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-not/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 main.c
 
 ^\*\* Results:$

regression/cbmc/enum-trace1/test_json.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --json-ui --function test --trace
 activate-multi-line-match

regression/cbmc/json-interface1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 --json-interface
 < test.json
 activate-multi-line-match

regression/cbmc/json1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --json-ui --stop-on-fail
 activate-multi-line-match

regression/cbmc/union10/union_list2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 union_list2.c
 
 ^EXIT=0$

regression/cbmc/union11/union_list.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-z3-smt-backend
 union_list.c
 
 ^EXIT=0$

regression/cbmc/z3/Issue5970.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+void main()
+{
+  unsigned A, x[64];
+  // clang-format off
+  __CPROVER_assume(0 <= A && A < 64);
+  __CPROVER_assume(__CPROVER_forall { int i ; (0 <= i && i < A) ==> x[i] >= 1 });
+  // clang-format on
+  assert(x[0] > 0);
+}

regression/cbmc/z3/Issue5970.desc

@@ -0,0 +1,12 @@
+CORE smt-backend broken-cprover-smt-backend
+Issue5970.c
+--z3
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line [0-9]+ assertion x\[0\] > 0: FAILURE$
+--
+invalid get-value term, term must be ground and must not contain quantifiers
+^\[main\.assertion\.1\] line [0-9]+ assertion x\[0\] > 0: ERROR$
+--
+This tests that attempts to "(get-value |XXX|)" from z3 sat results
+are handled and do not cause an error message or ERROR result.

regression/cbmc/z3/trace-char.c

@@ -0,0 +1,5 @@
+void main(int argc, char **argv)
+{
+  char arr[] = {'0', '1', '2', '3', '4', '5', '6', '7'};
+  assert(arr[0] == '2');
+}

regression/cbmc/z3/trace-char.desc

@@ -0,0 +1,13 @@
+CORE smt-backend broken-cprover-smt-backend
+trace-char.c
+--trace --smt2 --z3
+^EXIT=10$
+^SIGNAL=0$
+arr=\{ arr
+arr=\{ '0', '1', '2', '3', '4', '5', '6', '7' \}
+--
+arr=(assignment removed)
+error running SMT2 solver
+--
+Run cbmc with the --z3 and --trace options with arrays to confirm that
+char arrays are displayed in traces.

regression/cbmc/z3/trace.c

@@ -0,0 +1,5 @@
+void main(int argc, char **argv)
+{
+  int arr[] = {0, 1, 2, 3, 4, 5, 6, 17};
+  assert(arr[0] == 2);
+}

regression/cbmc/z3/trace.desc

@@ -0,0 +1,13 @@
+CORE smt-backend broken-cprover-smt-backend
+trace.c
+--trace --smt2 --z3
+^EXIT=10$
+^SIGNAL=0$
+arr=\{ arr
+arr=\{ 0, 1, 2, 3, 4, 5, 6, 17 \}
+--
+arr=(assignment removed)
+error running SMT2 solver
+--
+Run cbmc with the --z3 and --trace options with arrays to confirm that
+int arrays are displayed in traces.

src/solvers/smt2/smt2_conv.cpp

@@ -283,6 +283,7 @@ exprt smt2_convt::get(const exprt &expr) const
 
     if(it!=identifier_map.end())
       return it->second.value;
+    return expr;
   }
   else if(expr.id()==ID_nondet_symbol)
   {
@@ -319,6 +320,15 @@ exprt smt2_convt::get(const exprt &expr) const
   }
   else if(expr.is_constant())
     return expr;
+  else if(const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
+  {
+    exprt array_copy = *array;
+    for(auto &element : array_copy.operands())
+    {
+      element = get(element);
+    }
+    return array_copy;
+  }
 
   return nil_exprt();
 }
@@ -464,31 +474,85 @@ constant_exprt smt2_convt::parse_literal(
 exprt smt2_convt::parse_array(
   const irept &src,
   const array_typet &type)
+{
+  std::unordered_map<int64_t, exprt> operands_map;
+  walk_array_tree(&operands_map, src, type);
+  exprt::operandst operands;
+  // Try to find the default value, if there is none then set it
+  auto maybe_default_op = operands_map.find(-1);
+  exprt default_op;
+  if(maybe_default_op == operands_map.end())
+    default_op = nil_exprt();
+  else
+    default_op = maybe_default_op->second;
+  int64_t i = 0;
+  auto maybe_size = numeric_cast<std::int64_t>(type.size());
+  if(maybe_size.has_value())
+  {
+    while(i < maybe_size.value())
+    {
+      auto found_op = operands_map.find(i);
+      if(found_op != operands_map.end())
+        operands.emplace_back(found_op->second);
+      else
+        operands.emplace_back(default_op);
+      i++;
+    }
+  }
+  else
+  {
+    // Array size is unknown, keep adding with known indexes in order
+    // until we fail to find one.
+    auto found_op = operands_map.find(i);
+    while(found_op != operands_map.end())
+    {
+      operands.emplace_back(found_op->second);
+      i++;
+      found_op = operands_map.find(i);
+    }
+    operands.emplace_back(default_op);
+  }
+  return array_exprt(operands, type);
+}
+
+void smt2_convt::walk_array_tree(
+  std::unordered_map<int64_t, exprt> *operands_map,
+  const irept &src,
+  const array_typet &type)
 {
   if(src.get_sub().size()==4 && src.get_sub()[0].id()=="store")
   {
+    // This is the SMT syntax being parsed here
     // (store array index value)
-    if(src.get_sub().size()!=4)
-      return nil_exprt();
-
-    exprt array=parse_array(src.get_sub()[1], type);
-    exprt index=parse_rec(src.get_sub()[2], type.size().type());
-    exprt value=parse_rec(src.get_sub()[3], type.subtype());
-
-    return with_exprt(array, index, value);
+    // Recurse
+    walk_array_tree(operands_map, src.get_sub()[1], type);
+    const auto index_expr = parse_rec(src.get_sub()[2], type.size().type());
+    const constant_exprt index_constant = to_constant_expr(index_expr);
+    mp_integer tempint;
+    bool failure = to_integer(index_constant, tempint);
+    if(failure)
+      return;
+    long index = tempint.to_long();
+    exprt value = parse_rec(src.get_sub()[3], type.subtype());
+    operands_map->emplace(index, value);
+  }
+  else if(src.get_sub().size() == 3 && src.get_sub()[0].id() == "let")
+  {
+    // This is produced by Z3
+    // (let (....) (....))
+    walk_array_tree(
+      operands_map, src.get_sub()[1].get_sub()[0].get_sub()[1], type);
+    walk_array_tree(operands_map, src.get_sub()[2], type);
   }
   else if(src.get_sub().size()==2 &&
           src.get_sub()[0].get_sub().size()==3 &&
           src.get_sub()[0].get_sub()[0].id()=="as" &&
           src.get_sub()[0].get_sub()[1].id()=="const")
   {
-    // This is produced by Z3.
-    // ((as const (Array (_ BitVec 64) (_ BitVec 8))) #x00)))
-    exprt value=parse_rec(src.get_sub()[1], type.subtype());
-    return array_of_exprt(value, type);
+    // (as const type_info default_value)
+    exprt default_value = parse_rec(src.get_sub()[1], type.subtype());
+    operands_map->emplace(-1, default_value);
   }
-  else
-    return nil_exprt();
 }
 
 exprt smt2_convt::parse_union(
@@ -4351,6 +4415,7 @@ void smt2_convt::set_to(const exprt &expr, bool value)
     // This is a converted expression, we can just assert the literal name
     // since the expression is already defined
     out << found_literal->second;
+    set_values[found_literal->second] = value;
   }
   else
   {

src/solvers/smt2/smt2_conv.h

@@ -159,8 +159,23 @@ class smt2_convt : public stack_decision_proceduret
   constant_exprt parse_literal(const irept &, const typet &type);
   struct_exprt parse_struct(const irept &s, const struct_typet &type);
   exprt parse_union(const irept &s, const union_typet &type);
+  /// This function is for parsing array output from SMT solvers
+  /// when "(get-value |???|)" returns an array object.
+  /// \param s: is the irept parsed from the SMT output
+  /// \param type: is the expected type
+  /// \returns an exprt that represents the array
   exprt parse_array(const irept &s, const array_typet &type);
   exprt parse_rec(const irept &s, const typet &type);
+  /// This function walks the SMT output and populates a
+  /// map with index/value pairs for the array
+  /// \param operands_map: is a map of the operands to the array
+  ///    being constructed indexed by their index.
+  /// \param src: is the irept source for the SMT output
+  /// \param type: is the type of the array
+  void walk_array_tree(
+    std::unordered_map<int64_t, exprt> *operands_map,
+    const irept &src,
+    const array_typet &type);
 
   // we use this to build a bit-vector encoding of the FPA theory
   void convert_floatbv(const exprt &expr);
@@ -235,6 +250,10 @@ class smt2_convt : public stack_decision_proceduret
 
   typedef std::map<exprt, irep_idt> defined_expressionst;
   defined_expressionst defined_expressions;
+  /// The values which boolean identifiers have been `smt2_convt::set_to` or
+  /// in other words those which are asserted as true / false in the output
+  /// smt2 formula.
+  std::unordered_map<irep_idt, bool> set_values;
 
   defined_expressionst object_sizes;