Merge pull request #7004 from thomasspriggs/tas/smt_array_exprt

Add support for array_exprt to incremental smt2 decision procedure

Author: thomasspriggs

regression/cbmc-incr-smt2/arrays/array_literal.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int example_array[] = {5, 4, 3, 2, 1};
+  unsigned int index;
+  __CPROVER_assume(index < 5);
+  __CPROVER_assert(example_array[index] != 42, "Non-existent element");
+  __CPROVER_assert(example_array[index] != 5, "Index 0");
+  __CPROVER_assert(example_array[index] != 4, "Index 1");
+  __CPROVER_assert(example_array[index] != 3, "Index 2");
+  __CPROVER_assert(example_array[index] != 2, "Index 3");
+  __CPROVER_assert(example_array[index] != 1, "Index 4");
+  __CPROVER_assert(example_array[index] == 5 - index, "Index value relation");
+}

regression/cbmc-incr-smt2/arrays/array_literal.desc

@@ -0,0 +1,16 @@
+CORE
+array_literal.c
+
+Passing problem to incremental SMT2 solving
+line \d+ Non-existent element: SUCCESS
+line \d+ Index 0: FAILURE
+line \d+ Index 1: FAILURE
+line \d+ Index 2: FAILURE
+line \d+ Index 3: FAILURE
+line \d+ Index 4: FAILURE
+line \d+ Index value relation: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of reading an array which is initialised using an array literal.

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -2,6 +2,7 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
+#include <util/arith_tools.h>
 #include <util/expr.h>
 #include <util/namespace.h>
 #include <util/nodiscard.h>
@@ -12,6 +13,7 @@
 
 #include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/smt_array_theory.h>
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_responses.h>
@@ -64,14 +66,40 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
 {
   std::vector<exprt> dependent_expressions;
   expr.visit_pre([&](const exprt &expr_node) {
-    if(can_cast_expr<symbol_exprt>(expr_node))
+    if(
+      can_cast_expr<symbol_exprt>(expr_node) ||
+      can_cast_expr<array_exprt>(expr_node))
     {
       dependent_expressions.push_back(expr_node);
     }
   });
   return dependent_expressions;
 }
 
+void smt2_incremental_decision_proceduret::define_array_function(
+  const array_exprt &array)
+{
+  const smt_sortt array_sort = convert_type_to_smt_sort(array.type());
+  INVARIANT(
+    array_sort.cast<smt_array_sortt>(),
+    "Converting array typed expression to SMT should result in a term of array "
+    "sort.");
+  const smt_identifier_termt array_identifier = smt_identifier_termt{
+    "array_" + std::to_string(array_sequence()), array_sort};
+  solver_process->send(smt_declare_function_commandt{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)
+  {
+    const smt_termt index = convert_expr_to_smt(from_integer(i, index_type));
+    const smt_assert_commandt element_definition{smt_core_theoryt::equal(
+      smt_array_theoryt::select(array_identifier, index),
+      convert_expr_to_smt(elements.at(i)))};
+    solver_process->send(element_definition);
+  }
+  expression_identifiers.emplace(array, array_identifier);
+}
+
 /// \brief Defines any functions which \p expr depends on, which have not yet
 ///   been defined, along with their dependencies in turn.
 void smt2_incremental_decision_proceduret::define_dependent_functions(
@@ -123,10 +151,29 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         solver_process->send(function);
       }
     }
+    if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
+      define_array_function(*array_expr);
     to_be_defined.pop();
   }
 }
 
+/// Replaces the sub expressions of \p expr which have been defined as separate
+/// functions in the smt solver, using the \p expression_identifiers map.
+static exprt substitute_identifiers(
+  exprt expr,
+  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
+    &expression_identifiers)
+{
+  expr.visit_pre([&](exprt &node) -> void {
+    auto find_result = expression_identifiers.find(node);
+    if(find_result == expression_identifiers.cend())
+      return;
+    const auto type = find_result->first.type();
+    node = symbol_exprt{find_result->second.identifier(), type};
+  });
+  return expr;
+}
+
 smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
   const namespacet &_ns,
   std::unique_ptr<smt_base_solver_processt> _solver_process,
@@ -164,15 +211,20 @@ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
 smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
-  track_expression_objects(expr, ns, object_map);
+  const exprt substituted =
+    substitute_identifiers(expr, expression_identifiers);
+  track_expression_objects(substituted, ns, object_map);
   associate_pointer_sizes(
-    expr,
+    substituted,
     ns,
     pointer_sizes_map,
     object_map,
     object_size_function.make_application);
   return ::convert_expr_to_smt(
-    expr, object_map, pointer_sizes_map, object_size_function.make_application);
+    substituted,
+    object_map,
+    pointer_sizes_map,
+    object_size_function.make_application);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -55,6 +55,11 @@ class smt2_incremental_decision_proceduret final
 protected:
   // Implementation of protected decision_proceduret member function.
   resultt dec_solve() override;
+  /// \brief Defines a function of array sort and asserts the element values.
+  /// \details
+  ///   The new array function identifier is added to the
+  ///   `expression_identifiers` map.
+  void define_array_function(const array_exprt &array);
   /// \brief Defines any functions which \p expr depends on, which have not yet
   ///   been defined, along with their dependencies in turn.
   void define_dependent_functions(const exprt &expr);
@@ -81,7 +86,7 @@ class smt2_incremental_decision_proceduret final
     {
       return next_id++;
     }
-  } handle_sequence;
+  } handle_sequence, array_sequence;
 
   std::unordered_map<exprt, smt_identifier_termt, irep_hash>
     expression_handle_identifiers;

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -9,6 +9,7 @@
 #include <util/symbol_table.h>
 
 #include <solvers/smt2_incremental/smt2_incremental_decision_procedure.h>
+#include <solvers/smt2_incremental/smt_array_theory.h>
 #include <solvers/smt2_incremental/smt_commands.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_responses.h>
@@ -517,3 +518,45 @@ TEST_CASE(
     }
   }
 }
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret array commands.",
+  "[core][smt2_incremental]")
+{
+  auto test = decision_procedure_test_environmentt::make();
+  const auto index_type = signedbv_typet{32};
+  const symbolt index = make_test_symbol("index", index_type);
+  const auto value_type = signedbv_typet{8};
+  const symbolt foo = make_test_symbol("foo", value_type);
+  const auto array_type = array_typet{value_type, from_integer(2, index_type)};
+  SECTION("array_exprt - list of literal array elements")
+  {
+    const array_exprt array_literal{
+      {from_integer(9, value_type), from_integer(12, value_type)}, array_type};
+    test.sent_commands.clear();
+    test.procedure.set_to(
+      equal_exprt{
+        foo.symbol_expr(), index_exprt{array_literal, index.symbol_expr()}},
+      true);
+    const auto foo_term = smt_identifier_termt{"foo", smt_bit_vector_sortt{8}};
+    const auto array_term = smt_identifier_termt{
+      "array_0",
+      smt_array_sortt{smt_bit_vector_sortt{32}, smt_bit_vector_sortt{8}}};
+    const auto index_term =
+      smt_identifier_termt{"index", smt_bit_vector_sortt{32}};
+    const std::vector<smt_commandt> expected_commands{
+      smt_declare_function_commandt{foo_term, {}},
+      smt_declare_function_commandt{array_term, {}},
+      smt_assert_commandt{smt_core_theoryt::equal(
+        smt_array_theoryt::select(
+          array_term, smt_bit_vector_constant_termt{0, 32}),
+        smt_bit_vector_constant_termt{9, 8})},
+      smt_assert_commandt{smt_core_theoryt::equal(
+        smt_array_theoryt::select(
+          array_term, smt_bit_vector_constant_termt{1, 32}),
+        smt_bit_vector_constant_termt{12, 8})},
+      smt_declare_function_commandt{index_term, {}},
+      smt_assert_commandt{smt_core_theoryt::equal(
+        foo_term, smt_array_theoryt::select(array_term, index_term))}};
+  }
+}