Merge pull request #7079 from esteffin/esteffin/array-of-exprt

Translation of array_of_exprt to SMT 2 backend

Author: Enrico Steffinlongo

.github/workflows/pull-request-checks.yaml

@@ -698,13 +698,22 @@ jobs:
       - name: Fetch dependencies
         run: | 
           sudo apt-get update
-          sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3
+          sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
           # remove libgcc-s1, which isn't normally available in Ubuntu 18.04
           target=$(dpkg-query -W --showformat='${Version}\n' gcc-8-base | head -n 1)
           # libgcc1 uses an epoch, thus the extra 1:
           sudo apt-get install -y --allow-downgrades --reinstall gcc g++ libgcc-s1- libstdc++6=$target liblsan0=$target libtsan0=$target libcc1-0=$target libgcc1=1:$target gdb=8.1.1-0ubuntu1
-      - name: Confirm z3 solver is available and log the version installed
-        run: z3 --version
+      - name: Download z3 4.11.0 from the python wheel package, extract it and make sure it can be deployed
+        run: |
+          sudo apt-get install --no-install-recommends -y unzip
+          # download the z3 python wheel package
+          wget -O z3.4.11.0.whl https://github.com/Z3Prover/z3/releases/download/z3-4.11.0/z3_solver-4.11.0.0-py2.py3-none-manylinux1_x86_64.whl
+          # unpack the bundle using python
+          unzip z3.4.11.0.whl
+          # make z3 executable and move it in /usr/local/bin
+          chmod u+x ./z3_solver-4.11.0.0.data/data/bin/z3
+          mv ./z3_solver-4.11.0.0.data/data/bin/z3 /usr/local/bin/
+          z3 --version
       - name: Download cvc-5 from the releases page and make sure it can be deployed
         run: |
           wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux

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

@@ -0,0 +1,12 @@
+int main()
+{
+  int example_array[10000];
+  unsigned int index;
+  __CPROVER_assume(index < 999);
+
+  __CPROVER_array_set(example_array, 43);
+  __CPROVER_assert(example_array[index] != 43, "False array condition");
+
+  __CPROVER_array_set(example_array, 42);
+  __CPROVER_assert(example_array[index] == 42, "Valid array condition");
+}

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

@@ -0,0 +1,13 @@
+CORE
+array_of.c
+
+Passing problem to incremental SMT2 solving
+line \d+ False array condition: FAILURE
+line \d+ Valid array condition: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test using __CPROVER_array_set consisting in an `array_of` node which sets all values of a given
+array to a given value.
+This test uses a forall SMT statement.

regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc

@@ -3,7 +3,7 @@ control_flow.c
 --verbosity 10
 Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
-Sending command to SMT2 solver - \(set-logic QF_AUFBV\)
+Sending command to SMT2 solver - \(set-logic ALL\)
 Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\)
 Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool |goto_symex::&92;guard#1|\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -3,7 +3,7 @@ test.c
 --verbosity 10
 Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
-Sending command to SMT2 solver - \(set-logic QF_AUFBV\)
+Sending command to SMT2 solver - \(set-logic ALL\)
 Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
 Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -906,8 +906,10 @@ static smt_termt convert_expr_to_smt(
   const array_of_exprt &array_of,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for array of expression: " + array_of.pretty());
+  // This function is unreachable as the `array_of_exprt` nodes are already
+  // fully converted by the incremental decision procedure functions
+  // (smt2_incremental_decision_proceduret::define_array_function).
+  UNHANDLED_CASE;
 }
 
 static smt_termt convert_expr_to_smt(
@@ -1353,9 +1355,10 @@ static smt_termt convert_expr_to_smt(
   const array_exprt &array_construction,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for array construction expression: " +
-    array_construction.pretty());
+  // This function is unreachable as the `array_exprt` nodes are already fully
+  // converted by the incremental decision procedure functions
+  // (smt2_incremental_decision_proceduret::define_array_function).
+  UNHANDLED_CASE;
 }
 
 static smt_termt convert_expr_to_smt(

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -71,6 +71,7 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
     if(
       can_cast_expr<symbol_exprt>(expr_node) ||
       can_cast_expr<array_exprt>(expr_node) ||
+      can_cast_expr<array_of_exprt>(expr_node) ||
       can_cast_expr<nondet_symbol_exprt>(expr_node))
     {
       dependent_expressions.push_back(expr_node);
@@ -79,17 +80,10 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
   return dependent_expressions;
 }
 
-void smt2_incremental_decision_proceduret::define_array_function(
-  const array_exprt &array)
+void smt2_incremental_decision_proceduret::initialize_array_elements(
+  const array_exprt &array,
+  const smt_identifier_termt &array_identifier)
 {
-  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)
@@ -100,6 +94,39 @@ void smt2_incremental_decision_proceduret::define_array_function(
       convert_expr_to_smt(elements.at(i)))};
     solver_process->send(element_definition);
   }
+}
+
+void smt2_incremental_decision_proceduret::initialize_array_elements(
+  const array_of_exprt &array,
+  const smt_identifier_termt &array_identifier)
+{
+  const smt_sortt index_type =
+    convert_type_to_smt_sort(array.type().index_type());
+  const smt_identifier_termt array_index_identifier{
+    id2string(array_identifier.identifier()) + "_index", index_type};
+  const smt_termt element_value = convert_expr_to_smt(array.what());
+
+  const smt_assert_commandt elements_definition{smt_forall_termt{
+    {array_index_identifier},
+    smt_core_theoryt::equal(
+      smt_array_theoryt::select(array_identifier, array_index_identifier),
+      element_value)}};
+  solver_process->send(elements_definition);
+}
+
+template <typename t_exprt>
+void smt2_incremental_decision_proceduret::define_array_function(
+  const t_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{
+    "array_" + std::to_string(array_sequence()), array_sort};
+  solver_process->send(smt_declare_function_commandt{array_identifier, {}});
+  initialize_array_elements(array, array_identifier);
   expression_identifiers.emplace(array, array_identifier);
 }
 
@@ -168,9 +195,14 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
         solver_process->send(function);
       }
     }
-    if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
+    else if(const auto array_expr = expr_try_dynamic_cast<array_exprt>(current))
       define_array_function(*array_expr);
-    if(
+    else if(
+      const auto array_of_expr = expr_try_dynamic_cast<array_of_exprt>(current))
+    {
+      define_array_function(*array_of_expr);
+    }
+    else if(
       const auto nondet_symbol =
         expr_try_dynamic_cast<nondet_symbol_exprt>(current))
     {
@@ -213,8 +245,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
 {
   solver_process->send(
     smt_set_option_commandt{smt_option_produce_modelst{true}});
-  solver_process->send(smt_set_logic_commandt{
-    smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}});
+  solver_process->send(smt_set_logic_commandt{smt_logic_allt{}});
   solver_process->send(object_size_function.declaration);
 }
 

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -55,11 +55,29 @@ 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.
+  /// \brief Defines a function of array sort and asserts the element values
+  /// from `array_exprt` or `array_of_exprt`.
   /// \details
   ///   The new array function identifier is added to the
   ///   `expression_identifiers` map.
-  void define_array_function(const array_exprt &array);
+  /// \note Statically fails if the template type is not a `array_exprt` or
+  /// `array_of_exprt`.
+  template <typename t_exprt>
+  void define_array_function(const t_exprt &array);
+  /// \brief Generate and send to the SMT solver clauses asserting that each
+  /// array element is as specified by \p array.
+  void initialize_array_elements(
+    const array_exprt &array,
+    const smt_identifier_termt &array_identifier);
+  /// \brief Generate and send to the SMT solver clauses asserting that each
+  /// array element is as specified by \p array.
+  /// \note This function uses a forall SMT2 term. Using it in combination with
+  /// arrays, bit vectors and uninterpreted functions requires the `ALL` SMT
+  /// logic that is not in the SMT 2.6 standard, but that it has been tested
+  /// working on Z3 and CVC5.
+  void initialize_array_elements(
+    const array_of_exprt &array,
+    const smt_identifier_termt &array_identifier);
   /// \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);

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -171,9 +171,7 @@ TEST_CASE(
       test.sent_commands ==
       std::vector<smt_commandt>{
         smt_set_option_commandt{smt_option_produce_modelst{true}},
-        smt_set_logic_commandt{
-          // NOLINTNEXTLINE(whitespace/line_length)
-          smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}},
+        smt_set_logic_commandt{smt_logic_allt{}},
         test.object_size_function.declaration});
     test.sent_commands.clear();
     SECTION("Set symbol to true.")
@@ -615,5 +613,36 @@ TEST_CASE(
       smt_declare_function_commandt{index_term, {}},
       smt_assert_commandt{smt_core_theoryt::equal(
         foo_term, smt_array_theoryt::select(array_term, index_term))}};
+    REQUIRE(test.sent_commands == expected_commands);
+  }
+  SECTION("array_of_exprt - all elements set to a given value")
+  {
+    const array_of_exprt array_of_expr{
+      from_integer(42, value_type), array_type};
+    test.sent_commands.clear();
+    test.procedure.set_to(
+      equal_exprt{
+        foo.symbol_expr(), index_exprt{array_of_expr, 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 auto forall_term =
+      smt_identifier_termt{"array_0_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_forall_termt{
+        {forall_term},
+        smt_core_theoryt::equal(
+          smt_array_theoryt::select(array_term, forall_term),
+          smt_bit_vector_constant_termt{42, 8})}},
+      smt_declare_function_commandt{index_term, {}},
+      smt_assert_commandt{smt_core_theoryt::equal(
+        foo_term, smt_array_theoryt::select(array_term, index_term))}};
+    REQUIRE(test.sent_commands == expected_commands);
   }
 }