Merge pull request #6866 from NlightNFotis/smt_pointer_arithmetic_conversion_final

Add support for conversion of pointer arithmetic expressions to new SMT backend.

Author: NlightNFotis

regression/cbmc-incr-smt2/pointer_arithmetic/addition_compound_expr.c

@@ -0,0 +1,13 @@
+#include <stdint.h>
+
+#define NULL (void *)0
+
+int main()
+{
+  int32_t *a;
+  __CPROVER_assume(a != NULL);
+  int32_t *z = a + 2 * sizeof(int32_t);
+
+  __CPROVER_assert(a != z, "expected successful because of pointer arithmetic");
+  __CPROVER_assert(a == z, "expected failure because of pointer arithmetic");
+}

regression/cbmc-incr-smt2/pointer_arithmetic/addition_compound_expr.desc

@@ -0,0 +1,13 @@
+CORE
+addition_compound_expr.c
+--trace
+\[main\.assertion\.1\] line \d+ expected successful because of pointer arithmetic: SUCCESS
+\[main\.assertion\.2\] line \d+ expected failure because of pointer arithmetic: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing the same thing as the test in addition_simple.desc, with the
+difference being that the addition expression here is compound, containing a
+more elaborate operand in the form of a multiplication containing a sizeof
+operator.

regression/cbmc-incr-smt2/pointer_arithmetic/addition_simple.c

@@ -0,0 +1,12 @@
+#define NULL (void *)0
+
+int main()
+{
+  int *x;
+  int *y = x + 1;
+  __CPROVER_assume(x != NULL);
+  __CPROVER_assume(y != NULL);
+
+  __CPROVER_assert(y == x, "expected false after pointer manipulation");
+  __CPROVER_assert(y != x, "expected true");
+}

regression/cbmc-incr-smt2/pointer_arithmetic/addition_simple.desc

@@ -0,0 +1,12 @@
+CORE
+addition_simple.c
+--trace
+\[main\.assertion\.1\] line \d+ expected false after pointer manipulation: FAILURE
+\[main\.assertion\.2\] line \d+ expected true: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing basic pointer arithmetic by adding by incrementing a pointer's
+address and assigning that value to another pointer, then asserting that they
+don't point to the same thing.

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+int main()
+{
+  int *x = malloc(sizeof(int));
+  int *y = x + 3;
+  int z = y - x;
+  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
+  __CPROVER_assert(z == 3, "expected successful after pointer manipulation");
+  __CPROVER_assert(z != 3, "expected failure after pointer manipulation");
+}

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction.desc

@@ -0,0 +1,13 @@
+CORE
+pointer_subtraction.c
+--trace
+\[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
+\[main\.assertion\.2\] line \d+ expected successful after pointer manipulation: SUCCESS
+\[main\.assertion\.3\] line \d+ expected failure after pointer manipulation: FAILURE
+z=3
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is testing that the subtraction between two pointers (giving us the
+increment between the two pointers) works as it should.

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+int main()
+{
+  int *x = malloc(sizeof(int));
+  float *y = x + 3;
+  int z = y - x;
+  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
+  __CPROVER_assert(z == 3, "expected successful after pointer manipulation");
+  __CPROVER_assert(z != 3, "expected failure after pointer manipulation");
+}

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.desc

@@ -0,0 +1,10 @@
+CORE
+pointer_subtraction_diff_types.c
+--trace
+^Reason: only pointers of the same object type can be subtracted.
+^EXIT=(134|127)$
+^SIGNAL=0$
+--
+--
+This test is for making sure that we only subtract pointers with the
+same underlying (base) type.

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_unsigned.c

@@ -0,0 +1,15 @@
+#define NULL (void *)0
+
+int main()
+{
+  int *x;
+  unsigned int z;
+  __CPROVER_assume(z < 3);
+  __CPROVER_assume(z > 1);
+  int *y = x - z;
+  __CPROVER_assume(x != NULL);
+  __CPROVER_assume(y != NULL);
+
+  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
+  __CPROVER_assert(y != x, "expected success after pointer manipulation");
+}

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_unsigned.desc

@@ -0,0 +1,11 @@
+CORE
+pointer_subtraction_unsigned.c
+--trace
+\[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
+\[main\.assertion\.2\] line \d+ expected success after pointer manipulation: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The test is similar to the one in `pointer_subtraction.desc`, but with different
+types in the subtraction operands.

regression/cbmc-incr-smt2/pointer_arithmetic/subtraction_simple.c

@@ -0,0 +1,12 @@
+#define NULL (void *)0
+
+int main()
+{
+  int *x;
+  int *y = x - 2;
+  __CPROVER_assume(x != NULL);
+  __CPROVER_assume(y != NULL);
+
+  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
+  __CPROVER_assert(y != x, "expected successful after pointer manipulation");
+}

regression/cbmc-incr-smt2/pointer_arithmetic/subtraction_simple.desc

@@ -0,0 +1,11 @@
+CORE
+subtraction_simple.c
+--trace
+\[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
+\[main\.assertion\.2\] line \d+ expected successful after pointer manipulation: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is similar to the one in `addition_simple.desc`, but testing end-to-end
+the conversion of a subtraction case of pointer arithmetic.

src/solvers/Makefile

@@ -196,6 +196,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/construct_value_expr_from_smt.cpp \
       smt2_incremental/convert_expr_to_smt.cpp \
       smt2_incremental/object_tracking.cpp \
+      smt2_incremental/type_size_mapping.cpp \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \
       smt2_incremental/smt_core_theory.cpp \

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -587,7 +587,8 @@ static optionalt<smt_termt> try_relational_conversion(
 
 static smt_termt convert_expr_to_smt(
   const plus_exprt &plus,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const type_size_mapt &pointer_sizes)
 {
   if(std::all_of(
        plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
@@ -597,6 +598,43 @@ static smt_termt convert_expr_to_smt(
     return convert_multiary_operator_to_terms(
       plus, converted, smt_bit_vector_theoryt::add);
   }
+  else if(can_cast_type<pointer_typet>(plus.type()))
+  {
+    INVARIANT(
+      plus.operands().size() == 2,
+      "We are only handling a binary version of plus when it has a pointer "
+      "operand");
+
+    exprt pointer;
+    exprt scalar;
+    for(auto &operand : plus.operands())
+    {
+      if(can_cast_type<pointer_typet>(operand.type()))
+      {
+        pointer = operand;
+      }
+      else
+      {
+        scalar = operand;
+      }
+    }
+
+    // We need to ensure that we follow this code path only if the expression
+    // our assumptions about the structure of the addition expression hold.
+    INVARIANT(
+      !can_cast_type<pointer_typet>(scalar.type()),
+      "An addition expression with both operands being pointers when they are "
+      "not dereferenced is malformed");
+
+    const pointer_typet pointer_type =
+      *type_try_dynamic_cast<pointer_typet>(pointer.type());
+    const auto base_type = pointer_type.base_type();
+    const auto pointer_size = pointer_sizes.at(base_type);
+
+    return smt_bit_vector_theoryt::add(
+      converted.at(pointer),
+      smt_bit_vector_theoryt::multiply(converted.at(scalar), pointer_size));
+  }
   else
   {
     UNIMPLEMENTED_FEATURE(
@@ -606,17 +644,51 @@ static smt_termt convert_expr_to_smt(
 
 static smt_termt convert_expr_to_smt(
   const minus_exprt &minus,
-  const sub_expression_mapt &converted)
+  const sub_expression_mapt &converted,
+  const type_size_mapt &pointer_sizes)
 {
   const bool both_operands_bitvector =
     can_cast_type<integer_bitvector_typet>(minus.lhs().type()) &&
     can_cast_type<integer_bitvector_typet>(minus.rhs().type());
 
+  const bool lhs_is_pointer = can_cast_type<pointer_typet>(minus.lhs().type());
+  const bool rhs_is_pointer = can_cast_type<pointer_typet>(minus.rhs().type());
+
+  const bool both_operands_pointers = lhs_is_pointer && rhs_is_pointer;
+
+  // We don't really handle this - we just compute this to fall
+  // into an if-else branch that gives proper error handling information.
+  const bool one_operand_pointer = lhs_is_pointer || rhs_is_pointer;
+
   if(both_operands_bitvector)
   {
     return smt_bit_vector_theoryt::subtract(
       converted.at(minus.lhs()), converted.at(minus.rhs()));
   }
+  else if(both_operands_pointers)
+  {
+    const auto lhs_base_type = to_pointer_type(minus.lhs().type()).base_type();
+    const auto rhs_base_type = to_pointer_type(minus.rhs().type()).base_type();
+    INVARIANT(
+      lhs_base_type == rhs_base_type,
+      "only pointers of the same object type can be subtracted.");
+    return smt_bit_vector_theoryt::signed_divide(
+      smt_bit_vector_theoryt::subtract(
+        converted.at(minus.lhs()), converted.at(minus.rhs())),
+      pointer_sizes.at(lhs_base_type));
+  }
+  else if(one_operand_pointer)
+  {
+    UNIMPLEMENTED_FEATURE(
+      "convert_expr_to_smt::minus_exprt doesn't handle expressions where"
+      "only one operand is a pointer - this is because these expressions"
+      "are normally handled by convert_expr_to_smt::plus_exprt due to"
+      "transformations of the expressions by previous passes bringing"
+      "them into a form more suitably handled by that version of the function."
+      "If you are here, this is a mistake or something went wrong before."
+      "The expression that caused the problem is: " +
+      minus.pretty());
+  }
   else
   {
     UNIMPLEMENTED_FEATURE(
@@ -1299,6 +1371,7 @@ static smt_termt dispatch_expr_to_smt_conversion(
   const exprt &expr,
   const sub_expression_mapt &converted,
   const smt_object_mapt &object_map,
+  const type_size_mapt &pointer_sizes,
   const smt_object_sizet::make_applicationt &call_object_size)
 {
   if(const auto symbol = expr_try_dynamic_cast<symbol_exprt>(expr))
@@ -1415,11 +1488,11 @@ static smt_termt dispatch_expr_to_smt_conversion(
   }
   if(const auto plus = expr_try_dynamic_cast<plus_exprt>(expr))
   {
-    return convert_expr_to_smt(*plus, converted);
+    return convert_expr_to_smt(*plus, converted, pointer_sizes);
   }
   if(const auto minus = expr_try_dynamic_cast<minus_exprt>(expr))
   {
-    return convert_expr_to_smt(*minus, converted);
+    return convert_expr_to_smt(*minus, converted, pointer_sizes);
   }
   if(const auto divide = expr_try_dynamic_cast<div_exprt>(expr))
   {
@@ -1658,6 +1731,7 @@ at_scope_exitt<functiont> at_scope_exit(functiont exit_function)
 smt_termt convert_expr_to_smt(
   const exprt &expr,
   const smt_object_mapt &object_map,
+  const type_size_mapt &pointer_sizes,
   const smt_object_sizet::make_applicationt &object_size)
 {
 #ifndef CPROVER_INVARIANT_DO_NOT_CHECK
@@ -1676,7 +1750,7 @@ smt_termt convert_expr_to_smt(
     if(find_result != sub_expression_map.cend())
       return;
     smt_termt term = dispatch_expr_to_smt_conversion(
-      expr, sub_expression_map, object_map, object_size);
+      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));

src/solvers/smt2_incremental/convert_expr_to_smt.h

@@ -7,6 +7,7 @@
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/type_size_mapping.h>
 
 class exprt;
 class typet;
@@ -20,6 +21,7 @@ smt_sortt convert_type_to_smt_sort(const typet &type);
 smt_termt convert_expr_to_smt(
   const exprt &expression,
   const smt_object_mapt &object_map,
+  const type_size_mapt &pointer_sizes,
   const smt_object_sizet::make_applicationt &object_size);
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONVERT_EXPR_TO_SMT_H

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -2,13 +2,6 @@
 
 #include "smt2_incremental_decision_procedure.h"
 
-#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
-#include <solvers/smt2_incremental/convert_expr_to_smt.h>
-#include <solvers/smt2_incremental/smt_commands.h>
-#include <solvers/smt2_incremental/smt_core_theory.h>
-#include <solvers/smt2_incremental/smt_responses.h>
-#include <solvers/smt2_incremental/smt_solver_process.h>
-#include <solvers/smt2_incremental/smt_terms.h>
 #include <util/expr.h>
 #include <util/namespace.h>
 #include <util/nodiscard.h>
@@ -17,6 +10,15 @@
 #include <util/string_utils.h>
 #include <util/symbol.h>
 
+#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
+#include <solvers/smt2_incremental/convert_expr_to_smt.h>
+#include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_responses.h>
+#include <solvers/smt2_incremental/smt_solver_process.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/type_size_mapping.h>
+
 #include <stack>
 
 /// Issues a command to the solving process which is expected to optionally
@@ -163,8 +165,14 @@ smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
   track_expression_objects(expr, ns, object_map);
+  associate_pointer_sizes(
+    expr,
+    ns,
+    pointer_sizes_map,
+    object_map,
+    object_size_function.make_application);
   return ::convert_expr_to_smt(
-    expr, object_map, object_size_function.make_application);
+    expr, object_map, pointer_sizes_map, object_size_function.make_application);
 }
 
 exprt smt2_incremental_decision_proceduret::handle(const exprt &expr)
@@ -208,7 +216,10 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const
         "Objects in expressions being read should already be tracked from "
         "point of being set/handled.");
       descriptor = ::convert_expr_to_smt(
-        expr, object_map, object_size_function.make_application);
+        expr,
+        object_map,
+        pointer_sizes_map,
+        object_size_function.make_application);
     }
     else
     {

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h

@@ -12,6 +12,7 @@
 #include <solvers/smt2_incremental/object_tracking.h>
 #include <solvers/smt2_incremental/smt_object_size.h>
 #include <solvers/smt2_incremental/smt_terms.h>
+#include <solvers/smt2_incremental/type_size_mapping.h>
 #include <solvers/stack_decision_procedure.h>
 
 #include <memory>
@@ -89,6 +90,7 @@ class smt2_incremental_decision_proceduret final
   smt_object_mapt object_map;
   std::vector<bool> object_size_defined;
   smt_object_sizet object_size_function;
+  type_size_mapt pointer_sizes_map;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H