Merge pull request #6215 from TGWDB/SMT-cache-values-and-handle-z3-errors

SMT cache values and handle z3 errors

Author: TGWDB

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.

src/solvers/smt2/smt2_conv.cpp

@@ -4415,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

@@ -250,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;
 

src/solvers/smt2/smt2_dec.cpp

@@ -139,7 +139,7 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
   boolean_assignment.resize(no_boolean_variables, false);
 
   typedef std::unordered_map<irep_idt, irept> valuest;
-  valuest values;
+  valuest parsed_values;
 
   while(in)
   {
@@ -167,37 +167,69 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
       // ( (|some_integer| 0) )
       // ( (|some_integer| (- 10)) )
 
-      values[s0.id()]=s1;
+      parsed_values[s0.id()] = s1;
     }
     else if(
       parsed.id().empty() && parsed.get_sub().size() == 2 &&
       parsed.get_sub().front().id() == "error")
     {
       // We ignore errors after UNSAT because get-value after check-sat
       // returns unsat will give an error.
-      if(res!=resultt::D_UNSATISFIABLE)
+      if(res != resultt::D_UNSATISFIABLE)
       {
-        messaget log{message_handler};
-        log.error() << "SMT2 solver returned error message:\n"
-                    << "\t\"" << parsed.get_sub()[1].id() << "\""
-                    << messaget::eom;
-        return decision_proceduret::resultt::D_ERROR;
+        const auto &message = id2string(parsed.get_sub()[1].id());
+        // Special case error handling
+        if(
+          solver == solvert::Z3 &&
+          message.find("must not contain quantifiers") != std::string::npos)
+        {
+          // We tried to "(get-value |XXXX|)" where |XXXX| is determined to
+          // include a quantified expression
+          // Nothing to do, this should be caught and value assigned by the
+          // set_to defaults later.
+        }
+        // Unhandled error, log the error and report it back up to caller
+        else
+        {
+          messaget log{message_handler};
+          log.error() << "SMT2 solver returned error message:\n"
+                      << "\t\"" << message << "\"" << messaget::eom;
+          return decision_proceduret::resultt::D_ERROR;
+        }
       }
     }
   }
 
+  // If the result is not satisfiable don't bother updating the assignments and
+  // values (since we didn't get any), just return.
+  if(res != resultt::D_SATISFIABLE)
+    return res;
+
   for(auto &assignment : identifier_map)
   {
-    std::string conv_id=convert_identifier(assignment.first);
-    const irept &value=values[conv_id];
-    assignment.second.value=parse_rec(value, assignment.second.type);
+    std::string conv_id = convert_identifier(assignment.first);
+    const irept &value = parsed_values[conv_id];
+    assignment.second.value = parse_rec(value, assignment.second.type);
   }
 
   // Booleans
   for(unsigned v=0; v<no_boolean_variables; v++)
   {
-    const irept &value=values["B"+std::to_string(v)];
-    boolean_assignment[v]=(value.id()==ID_true);
+    const std::string boolean_identifier = "B" + std::to_string(v);
+    boolean_assignment[v] = [&]() {
+      const auto found_parsed_value = parsed_values.find(boolean_identifier);
+      if(found_parsed_value != parsed_values.end())
+        return found_parsed_value->second.id() == ID_true;
+      // Work out the value based on what set_to was called with.
+      const auto found_set_value =
+        set_values.find('|' + boolean_identifier + '|');
+      if(found_set_value != set_values.end())
+        return found_set_value->second;
+      // Old code used the computation
+      // const irept &value=values["B"+std::to_string(v)];
+      // boolean_assignment[v]=(value.id()==ID_true);
+      return parsed_values[boolean_identifier].id() == ID_true;
+    }();
   }
 
   return res;