Merge pull request #6988 from esteffin/tas/array_index_of

Add array read and update function to SMT2 backend

Author: NlightNFotis

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

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

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

@@ -0,0 +1,10 @@
+CORE
+array_read.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ Array condition: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of reading an index of an array.

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

@@ -0,0 +1,9 @@
+int main()
+{
+  int example_array[10000];
+  unsigned int index;
+  __CPROVER_assume(index < 10000);
+  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/array_write.desc

@@ -0,0 +1,11 @@
+CORE
+array_write.c
+
+Passing problem to incremental SMT2 solving
+\[main\.assertion\.1\] line \d+ Array condition: SUCCESS
+\[main\.assertion\.2\] line \d+ Array condition: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of updating the value at an index of an array.

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_UFBV\)
+Sending command to SMT2 solver - \(set-logic QF_AUFBV\)
 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_UFBV\)
+Sending command to SMT2 solver - \(set-logic QF_AUFBV\)
 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

@@ -18,6 +18,7 @@
 
 #include <solvers/prop/literal_expr.h>
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/smt_array_theory.h>
 #include <solvers/smt2_incremental/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
 
@@ -89,6 +90,13 @@ static smt_sortt convert_type_to_smt_sort(const bitvector_typet &type)
   return smt_bit_vector_sortt{type.get_width()};
 }
 
+static smt_sortt convert_type_to_smt_sort(const array_typet &type)
+{
+  return smt_array_sortt{
+    convert_type_to_smt_sort(type.index_type()),
+    convert_type_to_smt_sort(type.element_type())};
+}
+
 smt_sortt convert_type_to_smt_sort(const typet &type)
 {
   if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
@@ -99,6 +107,10 @@ smt_sortt convert_type_to_smt_sort(const typet &type)
   {
     return convert_type_to_smt_sort(*bitvector_type);
   }
+  if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
+  {
+    return convert_type_to_smt_sort(*array_type);
+  }
   UNIMPLEMENTED_FEATURE("Generation of SMT formula for type: " + type.pretty());
 }
 
@@ -906,11 +918,12 @@ static smt_termt convert_expr_to_smt(
 }
 
 static smt_termt convert_expr_to_smt(
-  const index_exprt &index,
+  const index_exprt &index_of,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for index expression: " + index.pretty());
+  const smt_termt &array = converted.at(index_of.array());
+  const smt_termt &index = converted.at(index_of.index());
+  return smt_array_theoryt::select(array, index);
 }
 
 template <typename factoryt, typename shiftt>
@@ -978,10 +991,29 @@ static smt_termt convert_expr_to_smt(
     "Generation of SMT formula for shift expression: " + shift.pretty());
 }
 
+static smt_termt convert_array_update_to_smt(
+  const exprt &old,
+  const exprt &index,
+  const exprt &new_value,
+  const sub_expression_mapt &converted)
+{
+  const smt_termt &old_array_term = converted.at(old);
+  const smt_termt &index_term = converted.at(index);
+  const smt_termt &value_term = converted.at(new_value);
+  return smt_array_theoryt::store(old_array_term, index_term, value_term);
+}
+
 static smt_termt convert_expr_to_smt(
   const with_exprt &with,
   const sub_expression_mapt &converted)
 {
+  if(const auto array_type = type_try_dynamic_cast<array_typet>(with.type()))
+  {
+    return convert_array_update_to_smt(
+      with.old(), with.where(), with.new_value(), converted);
+  }
+  // 'with' expression is also used to update struct fields, but for now we do
+  // not support them, so we fail.
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for with expression: " + with.pretty());
 }

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -140,7 +140,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_uninterpreted_functions_bit_vectorst{}});
+    smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}});
   solver_process->send(object_size_function.declaration);
 }
 

src/solvers/smt2_incremental/smt_logics.def

@@ -10,5 +10,5 @@ LOGIC_ID(quantifier_free_uninterpreted_functions, QF_UF)
 LOGIC_ID(quantifier_free_bit_vectors, QF_BV)
 LOGIC_ID(quantifier_free_uninterpreted_functions_bit_vectors, QF_UFBV)
 LOGIC_ID(quantifier_free_bit_vectors_arrays, QF_ABV)
-LOGIC_ID(quantifier_free_uninterpreted_functions_bit_vectors_arrays, QF_AUFBV)
+LOGIC_ID(quantifier_free_arrays_uninterpreted_functions_bit_vectors, QF_AUFBV)
 LOGIC_ID(all, ALL)

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -14,6 +14,7 @@
 
 #include <solvers/smt2_incremental/convert_expr_to_smt.h>
 #include <solvers/smt2_incremental/object_tracking.h>
+#include <solvers/smt2_incremental/smt_array_theory.h>
 #include <solvers/smt2_incremental/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_terms.h>
@@ -96,6 +97,20 @@ expr_to_smt_conversion_test_environmentt::convert(const exprt &expression) const
     object_size_function.make_application);
 }
 
+TEST_CASE("\"array_typet\" to smt sort conversion", "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+
+  const auto array_type =
+    array_typet{signedbv_typet{8}, from_integer(8, c_index_type())};
+  INFO("Type being converted: " + array_type.pretty(2, 0));
+  const auto conversion_result = convert_type_to_smt_sort(array_type);
+  CHECK(
+    conversion_result ==
+    smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{8}});
+}
+
 TEST_CASE("\"symbol_exprt\" to smt term conversion", "[core][smt2_incremental]")
 {
   auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);
@@ -1126,6 +1141,52 @@ TEST_CASE(
   }
 }
 
+TEST_CASE(
+  "expr to smt conversion for index_exprt expressions",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  const typet value_type = signedbv_typet{8};
+  const exprt array = symbol_exprt{
+    "my_array", array_typet{value_type, from_integer(10, signed_size_type())}};
+  const exprt index = from_integer(42, unsignedbv_typet{64});
+  const index_exprt index_expr{array, index};
+  INFO("Expression being converted: " + index_expr.pretty(2, 0));
+  const smt_termt expected = smt_array_theoryt::select(
+    smt_identifier_termt{
+      "my_array",
+      smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{8}}},
+    smt_bit_vector_constant_termt{42, 64});
+  CHECK(test.convert(index_expr) == expected);
+}
+
+TEST_CASE(
+  "expr to smt conversion for with_exprt expressions",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  SECTION("Array types")
+  {
+    const typet value_type = signedbv_typet{8};
+    const exprt array = symbol_exprt{
+      "my_array",
+      array_typet{value_type, from_integer(10, signed_size_type())}};
+    const exprt index = from_integer(42, unsignedbv_typet{64});
+    const exprt value = from_integer(12, value_type);
+    const with_exprt with{array, index, value};
+    INFO("Expression being converted: " + with.pretty(2, 0));
+    const smt_termt expected = smt_array_theoryt::store(
+      smt_identifier_termt{
+        "my_array",
+        smt_array_sortt{smt_bit_vector_sortt{64}, smt_bit_vector_sortt{8}}},
+      smt_bit_vector_constant_termt{42, 64},
+      smt_bit_vector_constant_termt{12, 8});
+    CHECK(test.convert(with) == expected);
+  }
+}
+
 TEST_CASE(
   "expr to smt conversion for extract bits expressions",
   "[core][smt2_incremental]")