Merge pull request #7078 from thomasspriggs/tas/smt_array_trace_printing_extended

Add array trace printing to incremental SMT2 decision procedure

Author: thomasspriggs

regression/cbmc-incr-smt2/arrays_traces/array_read.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int example_array[1025];
+  unsigned int index;
+  __CPROVER_assume(index < 1025);
+  __CPROVER_assert(example_array[index] != 42, "Array condition");
+}

regression/cbmc-incr-smt2/arrays_traces/array_read.desc

@@ -0,0 +1,15 @@
+CORE
+array_read.c
+--trace
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ Array condition: FAILURE
+^Trace for main\.assertion\.1
+example_array=\{ (\d+, )*42
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of reading a value at a non-deterministic index of an array.
+Similar to the test in ../arrays/array_read.c, but we want to assert
+the value of the array that comes back in the trace to make sure we're
+observing the correct values.

regression/cbmc-incr-smt2/arrays_traces/array_write.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int example_array[1025];
+  unsigned int index;
+  __CPROVER_assume(index < 1025);
+  example_array[index] = 42;
+  __CPROVER_assert(example_array[index] == 42, "Array condition");
+  __CPROVER_assert(example_array[index] != 42, "Array condition");
+}

regression/cbmc-incr-smt2/arrays_traces/array_write.desc

@@ -0,0 +1,12 @@
+CORE
+array_write.c
+--trace
+Passing problem to incremental SMT2 solving
+^Trace for main\.assertion\.2
+example_array\[\d{1,4}ll?\]=42
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of writing a value at a non-deterministic index of an array, then asserting
+the value we expect.

src/solvers/smt2_incremental/response_or_error.h

@@ -0,0 +1,64 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H
+
+#include <util/invariant.h>
+#include <util/optional.h>
+
+#include <string>
+#include <vector>
+
+/// Holds either a valid parsed response or response sub-tree of type \tparam
+/// smtt or a collection of message strings explaining why the given input was
+/// not valid.
+template <class smtt>
+class response_or_errort final
+{
+public:
+  explicit response_or_errort(smtt smt) : smt{std::move(smt)}
+  {
+  }
+
+  explicit response_or_errort(std::string message)
+    : messages{std::move(message)}
+  {
+  }
+
+  explicit response_or_errort(std::vector<std::string> messages)
+    : messages{std::move(messages)}
+  {
+  }
+
+  /// \brief Gets the smt response if the response is valid, or returns nullptr
+  ///   otherwise.
+  const smtt *get_if_valid() const
+  {
+    INVARIANT(
+      smt.has_value() == messages.empty(),
+      "The response_or_errort class must be in the valid state or error state, "
+      "exclusively.");
+    return smt.has_value() ? &smt.value() : nullptr;
+  }
+
+  /// \brief Gets the error messages if the response is invalid, or returns
+  ///   nullptr otherwise.
+  const std::vector<std::string> *get_if_error() const
+  {
+    INVARIANT(
+      smt.has_value() == messages.empty(),
+      "The response_or_errort class must be in the valid state or error state, "
+      "exclusively.");
+    return smt.has_value() ? nullptr : &messages;
+  }
+
+private:
+  // The below two fields could be a single `std::variant` field, if there was
+  // an implementation of it available in the cbmc repository. However at the
+  // time of writing we are targeting C++11, `std::variant` was introduced in
+  // C++17 and we have no backported version.
+  optionalt<smtt> smt;
+  std::vector<std::string> messages;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_RESPONSE_OR_ERROR_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -27,12 +27,13 @@
 /// return a success status followed by the actual response of interest.
 static smt_responset get_response_to_command(
   smt_base_solver_processt &solver_process,
-  const smt_commandt &command)
+  const smt_commandt &command,
+  const std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   solver_process.send(command);
-  auto response = solver_process.receive_response();
+  auto response = solver_process.receive_response(identifier_table);
   if(response.cast<smt_success_responset>())
-    return solver_process.receive_response();
+    return solver_process.receive_response(identifier_table);
   else
     return response;
 }
@@ -84,6 +85,7 @@ void smt2_incremental_decision_proceduret::initialize_array_elements(
   const array_exprt &array,
   const smt_identifier_termt &array_identifier)
 {
+  identifier_table.emplace(array_identifier.identifier(), array_identifier);
   const std::vector<exprt> &elements = array.operands();
   const typet &index_type = array.type().index_type();
   for(std::size_t i = 0; i < elements.size(); ++i)
@@ -135,13 +137,15 @@ void send_function_definition(
   const irep_idt &symbol_identifier,
   const std::unique_ptr<smt_base_solver_processt> &solver_process,
   std::unordered_map<exprt, smt_identifier_termt, irep_hash>
-    &expression_identifiers)
+    &expression_identifiers,
+  std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
   const smt_declare_function_commandt function{
     smt_identifier_termt(
       symbol_identifier, convert_type_to_smt_sort(expr.type())),
     {}};
   expression_identifiers.emplace(expr, function.identifier());
+  identifier_table.emplace(symbol_identifier, function.identifier());
   solver_process->send(function);
 }
 
@@ -183,7 +187,8 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
           *symbol_expr,
           symbol_expr->get_identifier(),
           solver_process,
-          expression_identifiers);
+          expression_identifiers,
+          identifier_table);
       }
       else
       {
@@ -192,6 +197,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         const smt_define_function_commandt function{
           symbol->name, {}, convert_expr_to_smt(symbol->value)};
         expression_identifiers.emplace(*symbol_expr, function.identifier());
+        identifier_table.emplace(identifier, function.identifier());
         solver_process->send(function);
       }
     }
@@ -210,7 +216,8 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         *nondet_symbol,
         nondet_symbol->get_identifier(),
         solver_process,
-        expression_identifiers);
+        expression_identifiers,
+        identifier_table);
     }
     to_be_defined.pop();
   }
@@ -263,12 +270,36 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   smt_define_function_commandt function{
     "B" + std::to_string(handle_sequence()), {}, convert_expr_to_smt(expr)};
   expression_handle_identifiers.emplace(expr, function.identifier());
+  identifier_table.emplace(
+    function.identifier().identifier(), function.identifier());
   solver_process->send(function);
 }
 
+void smt2_incremental_decision_proceduret::define_index_identifiers(
+  const exprt &expr)
+{
+  expr.visit_pre([&](const exprt &expr_node) {
+    if(!can_cast_type<array_typet>(expr_node.type()))
+      return;
+    if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
+    {
+      const auto index_expr = with_expr->where();
+      const auto index_term = convert_expr_to_smt(index_expr);
+      const auto index_identifier = "index_" + std::to_string(index_sequence());
+      const auto index_definition =
+        smt_define_function_commandt{index_identifier, {}, index_term};
+      expression_identifiers.emplace(index_expr, index_definition.identifier());
+      identifier_table.emplace(index_identifier, index_definition.identifier());
+      solver_process->send(
+        smt_define_function_commandt{index_identifier, {}, index_term});
+    }
+  });
+}
+
 smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
+  define_index_identifiers(expr);
   const exprt substituted =
     substitute_identifiers(expr, expression_identifiers);
   track_expression_objects(substituted, ns, object_map);
@@ -310,13 +341,82 @@ static optionalt<smt_termt> get_identifier(
   return {};
 }
 
+array_exprt smt2_incremental_decision_proceduret::get_expr(
+  const smt_termt &array,
+  const array_typet &type) const
+{
+  INVARIANT(
+    type.is_complete(), "Array size is required for getting array values.");
+  const auto size = numeric_cast<std::size_t>(get(type.size()));
+  INVARIANT(
+    size,
+    "Size of array must be convertible to std::size_t for getting array value");
+  std::vector<exprt> elements;
+  const auto index_type = type.index_type();
+  elements.reserve(*size);
+  for(std::size_t index = 0; index < size; ++index)
+  {
+    elements.push_back(get_expr(
+      smt_array_theoryt::select(
+        array,
+        ::convert_expr_to_smt(
+          from_integer(index, index_type),
+          object_map,
+          pointer_sizes_map,
+          object_size_function.make_application)),
+      type.element_type()));
+  }
+  return array_exprt{elements, type};
+}
+
+exprt smt2_incremental_decision_proceduret::get_expr(
+  const smt_termt &descriptor,
+  const typet &type) const
+{
+  const smt_get_value_commandt get_value_command{descriptor};
+  const smt_responset response = get_response_to_command(
+    *solver_process, get_value_command, identifier_table);
+  const auto get_value_response = response.cast<smt_get_value_responset>();
+  if(!get_value_response)
+  {
+    throw analysis_exceptiont{
+      "Expected get-value response from solver, but received - " +
+      response.pretty()};
+  }
+  if(get_value_response->pairs().size() > 1)
+  {
+    throw analysis_exceptiont{
+      "Expected single valuation pair in get-value response from solver, but "
+      "received multiple pairs - " +
+      response.pretty()};
+  }
+  return construct_value_expr_from_smt(
+    get_value_response->pairs()[0].get().value(), type);
+}
+
 exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
 {
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {
     debug << "`get` - \n  " + expr.pretty(2, 0) << messaget::eom;
   });
-  optionalt<smt_termt> descriptor =
-    get_identifier(expr, expression_handle_identifiers, expression_identifiers);
+  auto descriptor = [&]() -> optionalt<smt_termt> {
+    if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
+    {
+      const auto array = get_identifier(
+        index_expr->array(),
+        expression_handle_identifiers,
+        expression_identifiers);
+      const auto index = get_identifier(
+        index_expr->index(),
+        expression_handle_identifiers,
+        expression_identifiers);
+      if(!array || !index)
+        return {};
+      return smt_array_theoryt::select(*array, *index);
+    }
+    return get_identifier(
+      expr, expression_handle_identifiers, expression_identifiers);
+  }();
   if(!descriptor)
   {
     if(gather_dependent_expressions(expr).empty())
@@ -349,25 +449,13 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
       return expr;
     }
   }
-  const smt_get_value_commandt get_value_command{*descriptor};
-  const smt_responset response =
-    get_response_to_command(*solver_process, get_value_command);
-  const auto get_value_response = response.cast<smt_get_value_responset>();
-  if(!get_value_response)
-  {
-    throw analysis_exceptiont{
-      "Expected get-value response from solver, but received - " +
-      response.pretty()};
-  }
-  if(get_value_response->pairs().size() > 1)
+  if(const auto array_type = type_try_dynamic_cast<array_typet>(expr.type()))
   {
-    throw analysis_exceptiont{
-      "Expected single valuation pair in get-value response from solver, but "
-      "received multiple pairs - " +
-      response.pretty()};
+    if(array_type->is_incomplete())
+      return expr;
+    return get_expr(*descriptor, *array_type);
   }
-  return construct_value_expr_from_smt(
-    get_value_response->pairs()[0].get().value(), expr.type());
+  return get_expr(*descriptor, expr.type());
 }
 
 void smt2_incremental_decision_proceduret::print_assignment(
@@ -464,8 +552,8 @@ decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve()
 {
   ++number_of_solver_calls;
   define_object_sizes();
-  const smt_responset result =
-    get_response_to_command(*solver_process, smt_check_sat_commandt{});
+  const smt_responset result = get_response_to_command(
+    *solver_process, smt_check_sat_commandt{}, identifier_table);
   if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
   {
     if(check_sat_response->kind().cast<smt_unknown_responset>())

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -52,6 +52,12 @@ class smt2_incremental_decision_proceduret final
   void push() override;
   void pop() override;
 
+  /// Gets the value of \p descriptor from the solver and returns the solver
+  /// response expressed as an exprt of type \p type. This is an implementation
+  /// detail of the `get(exprt)` member function.
+  exprt get_expr(const smt_termt &descriptor, const typet &type) const;
+  array_exprt get_expr(const smt_termt &array, const array_typet &type) const;
+
 protected:
   // Implementation of protected decision_proceduret member function.
   resultt dec_solve() override;
@@ -85,6 +91,7 @@ class smt2_incremental_decision_proceduret final
   /// \brief Add objects in \p expr to object_map if needed and convert to smt.
   /// \note This function is non-const because it mutates the object_map.
   smt_termt convert_expr_to_smt(const exprt &expr);
+  void define_index_identifiers(const exprt &expr);
   /// Sends the solver the definitions of the object sizes.
   void define_object_sizes();
 
@@ -112,7 +119,7 @@ class smt2_incremental_decision_proceduret final
     {
       return next_id++;
     }
-  } handle_sequence, array_sequence;
+  } handle_sequence, array_sequence, index_sequence;
   /// When the `handle(exprt)` member function is called, the decision procedure
   /// commands the SMT solver to define a new function corresponding to the
   /// given expression. The mapping of the expressions to the function
@@ -131,6 +138,7 @@ class smt2_incremental_decision_proceduret final
   /// array expressions when support for them is implemented.
   std::unordered_map<exprt, smt_identifier_termt, irep_hash>
     expression_identifiers;
+  std::unordered_map<irep_idt, smt_identifier_termt> identifier_table;
   /// This map is used to track object related state. See documentation in
   /// object_tracking.h for details.
   smt_object_mapt object_map;