Merge pull request #7090 from esteffin/esteffin/address-of-array-index

Add address_of(array[index]) support to incremental SMT2 backend

Author: Enrico Steffinlongo

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

@@ -0,0 +1,8 @@
+int main()
+{
+  int example_array[10000];
+  __CPROVER_assert(
+    __CPROVER_OBJECT_SIZE(example_array) == 40000, "Array condition 1");
+  __CPROVER_assert(
+    __CPROVER_OBJECT_SIZE(example_array) == 40001, "Array condition 2");
+}

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

@@ -0,0 +1,11 @@
+CORE
+array_address_of.c
+
+Passing problem to incremental SMT2 solving
+line \d+ Array condition 1: SUCCESS
+line \d+ Array condition 2: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Test of getting the size of an array resulting in a address_of(array[0]) expression.

regression/cbmc-primitives/exists_assume_6231/test2.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 test2.c
 --pointer-check
 ^EXIT=10$

regression/cbmc-primitives/implication_statement_checks_1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 --div-by-zero-check
 test.c
 ^EXIT=0$

regression/cbmc-primitives/r_w_ok_valid/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --pointer-check --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/same-object-01/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/same-object-02/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$

regression/cbmc-primitives/same-object-04/test-no-cp.desc

@@ -1,4 +1,4 @@
-CORE
+CORE new-smt-backend
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1813,6 +1813,25 @@ at_scope_exitt<functiont> at_scope_exit(functiont exit_function)
 }
 #endif
 
+exprt lower_address_of_array_index(exprt expr)
+{
+  expr.visit_pre([](exprt &expr) {
+    const auto address_of_expr = expr_try_dynamic_cast<address_of_exprt>(expr);
+    if(!address_of_expr)
+      return;
+    const auto array_index_expr =
+      expr_try_dynamic_cast<index_exprt>(address_of_expr->object());
+    if(!array_index_expr)
+      return;
+    expr = plus_exprt{
+      address_of_exprt{
+        array_index_expr->array(),
+        type_checked_cast<pointer_typet>(address_of_expr->type())},
+      array_index_expr->index()};
+  });
+  return expr;
+}
+
 smt_termt convert_expr_to_smt(
   const exprt &expr,
   const smt_object_mapt &object_map,
@@ -1830,13 +1849,14 @@ smt_termt convert_expr_to_smt(
   const auto end_conversion = at_scope_exit([&]() { in_conversion = false; });
 #endif
   sub_expression_mapt sub_expression_map;
-  expr.visit_post([&](const exprt &expr) {
+  const auto lowered_expr = lower_address_of_array_index(expr);
+  lowered_expr.visit_post([&](const exprt &expr) {
     const auto find_result = sub_expression_map.find(expr);
     if(find_result != sub_expression_map.cend())
       return;
     smt_termt term = dispatch_expr_to_smt_conversion(
       expr, sub_expression_map, object_map, pointer_sizes, object_size);
     sub_expression_map.emplace_hint(find_result, expr, std::move(term));
   });
-  return std::move(sub_expression_map.at(expr));
+  return std::move(sub_expression_map.at(lowered_expr));
 }

src/solvers/smt2_incremental/convert_expr_to_smt.h

@@ -16,6 +16,11 @@ class typet;
 ///   stored as sort ast (abstract syntax tree).
 smt_sortt convert_type_to_smt_sort(const typet &type);
 
+/// \brief Lower the `address_of(array[idx])` sub expressions in \p expr to
+///   `idx + address_of(array)`, so that it can be fed to
+///   `convert_expr_to_smt`.
+exprt lower_address_of_array_index(exprt expr);
+
 /// \brief Converts the \p expression to an smt encoding of the same expression
 ///   stored as term ast (abstract syntax tree).
 smt_termt convert_expr_to_smt(

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1590,3 +1590,62 @@ TEST_CASE(
       smt_bit_vector_theoryt::extract(63, 64 - object_bits)(
         smt_bit_vector_theoryt::concat(object, offset))}));
 }
+
+TEST_CASE(
+  "lower_address_of_array_index works correctly",
+  "[core][smt2_incremental]")
+{
+  auto test =
+    expr_to_smt_conversion_test_environmentt::make(test_archt::x86_64);
+  const symbol_tablet symbol_table;
+  const namespacet ns{symbol_table};
+  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};
+  const address_of_exprt address_of_expr{index_expr};
+  const plus_exprt lowered{
+    address_of_exprt{
+      array, type_checked_cast<pointer_typet>(address_of_expr.type())},
+    index};
+  SECTION("Lowering address_of(array[idx])")
+  {
+    CHECK(lower_address_of_array_index(address_of_expr) == lowered);
+  }
+  SECTION("Lowering expression containing address_of(array[idx])")
+  {
+    const symbol_exprt symbol{"a_symbol", address_of_expr.type()};
+    const equal_exprt assignment{symbol, address_of_expr};
+    const equal_exprt expected{symbol, lowered};
+    CHECK(lower_address_of_array_index(assignment) == expected);
+  }
+  SECTION("Lowering does not lower other expressions")
+  {
+    const symbol_exprt symbol{"a_symbol", index_expr.type()};
+    const equal_exprt assignment{symbol, index_expr};
+    CHECK(lower_address_of_array_index(assignment) == assignment);
+  }
+  SECTION("Lowering is done during convert_to_smt")
+  {
+    const symbol_exprt symbol{"a_symbol", address_of_expr.type()};
+    const equal_exprt assignment{symbol, address_of_expr};
+    track_expression_objects(assignment, ns, test.object_map);
+    associate_pointer_sizes(
+      assignment,
+      ns,
+      test.pointer_sizes,
+      test.object_map,
+      test.object_size_function.make_application);
+    const smt_termt expected = smt_core_theoryt::equal(
+      smt_identifier_termt(symbol.get_identifier(), smt_bit_vector_sortt{64}),
+      smt_bit_vector_theoryt::add(
+        smt_bit_vector_theoryt::concat(
+          smt_bit_vector_constant_termt{2, 8},
+          smt_bit_vector_constant_termt{0, 56}),
+        smt_bit_vector_theoryt::multiply(
+          smt_bit_vector_constant_termt{42, 64},
+          smt_bit_vector_constant_termt{1, 64})));
+    CHECK(test.convert(assignment) == expected);
+  }
+}