Merge pull request #6905 from NlightNFotis/relational_operators_pointer_support

Relational operators support for pointers in new SMT backend

Author: NlightNFotis

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c

@@ -0,0 +1,27 @@
+#include <stdlib.h>
+
+int main()
+{
+  int x;
+  int *y = &x;
+  int *z = &x;
+
+  if(x)
+  {
+    y++;
+  }
+  else
+  {
+    z++;
+  }
+
+  __CPROVER_assume(y >= z);
+  __CPROVER_assert(x != y, "x != y: expected successful");
+  __CPROVER_assert(x == y, "x == y: expected failure");
+
+  __CPROVER_assume(z >= x);
+
+  __CPROVER_assert(z >= x, "z >= x: expected successful");
+  __CPROVER_assert(z <= y, "z <= y: expected successful");
+  __CPROVER_assert(z <= x, "z <= x: expected failure");
+}

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc

@@ -0,0 +1,14 @@
+CORE
+pointers_assume.c
+--trace
+\[main\.assertion\.1\] line \d+ x != y: expected successful: SUCCESS
+\[main\.assertion\.2\] line \d+ x == y: expected failure: FAILURE
+\[main\.assertion\.3\] line \d+ z >= x: expected successful: SUCCESS
+\[main\.assertion\.4\] line \d+ z <= y: expected successful: SUCCESS
+\[main\.assertion\.5\] line \d+ z <= x: expected failure: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing basic pointer relational operator support for three objects
+defined in the function's stack frame.

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.c

@@ -0,0 +1,19 @@
+#define NULL (void *)0
+
+int main()
+{
+  int i = 12;
+  int *x = &i;
+  int *y = x + 1;
+  int *z = x - 1;
+
+  // Assertions on y's relation to x
+  __CPROVER_assert(y != x, "y != x: expected successful");
+  __CPROVER_assert(y > x, "y > x: expected successful");
+  __CPROVER_assert(y < x, "y < x: expected failure");
+
+  // Assertions on z's relation to x
+  __CPROVER_assert(z != x, "z != x: expected successful");
+  __CPROVER_assert(z > x, "z > x: expected failure");
+  __CPROVER_assert(z < x, "z < x: expected success");
+}

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.desc

@@ -0,0 +1,15 @@
+CORE
+pointers_stack_lessthan.c
+--trace
+\[main\.assertion\.1] line \d+ y != x: expected successful: SUCCESS
+\[main\.assertion\.2] line \d+ y > x: expected successful: SUCCESS
+\[main\.assertion\.3] line \d+ y < x: expected failure: FAILURE
+\[main\.assertion\.4] line \d+ z != x: expected successful: SUCCESS
+\[main\.assertion\.5] line \d+ z > x: expected failure: FAILURE
+\[main\.assertion\.6] line \d+ z < x: expected success: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing basic pointer relational operator support for three objects
+defined in the function's stack frame.

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.c

@@ -0,0 +1,17 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *a = malloc(sizeof(int) * 5);
+
+  for(int i = 0; i < 5; i++)
+    *(a + i) = i;
+
+  for(int i = 0; i < 5; i++)
+  {
+    __CPROVER_assert(*(a + i) >= i, "*(a + i) >= i: expected successful");
+    __CPROVER_assert(*(a + i) <= i, "*(a + i) <= i: expected successful");
+    __CPROVER_assert(*(a + i) == i, "*(a + i) <= i: expected successful");
+    __CPROVER_assert(*(a + i) != i, "*(a + i) <= i: expected failure");
+  }
+}

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.desc

@@ -0,0 +1,13 @@
+CORE
+pointers_stack_malloc.c
+--trace
+\[main\.assertion\.1\] line \d+ \*\(a \+ i\) >= i: expected successful: SUCCESS
+\[main\.assertion\.2\] line \d+ \*\(a \+ i\) <= i: expected successful: SUCCESS
+\[main\.assertion\.3\] line \d+ \*\(a \+ i\) <= i: expected successful: SUCCESS
+\[main\.assertion\.4\] line \d+ \*\(a \+ i\) <= i: expected failure: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing the support for relational operators as applied to pointer objects
+backed by a malloc and initialised to some values.

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -530,13 +530,31 @@ static smt_termt convert_relational_to_smt(
   const auto &lhs = converted.at(binary_relation.lhs());
   const auto &rhs = converted.at(binary_relation.rhs());
   const typet operand_type = binary_relation.lhs().type();
-  if(lhs.get_sort().cast<smt_bit_vector_sortt>())
+  if(can_cast_type<pointer_typet>(operand_type))
+  {
+    // The code here is operating under the assumption that the comparison
+    // operands have types for which the comparison makes sense.
+
+    // We already know this is the case given that we have followed
+    // the if statement branch, but including the same check here
+    // for consistency (it's cheap).
+    const auto lhs_type_is_pointer =
+      can_cast_type<pointer_typet>(binary_relation.lhs().type());
+    const auto rhs_type_is_pointer =
+      can_cast_type<pointer_typet>(binary_relation.rhs().type());
+    INVARIANT(
+      lhs_type_is_pointer && rhs_type_is_pointer,
+      "pointer comparison requires that both operand types are pointers.");
+    return unsigned_factory(lhs, rhs);
+  }
+  else if(lhs.get_sort().cast<smt_bit_vector_sortt>())
   {
     if(can_cast_type<unsignedbv_typet>(operand_type))
       return unsigned_factory(lhs, rhs);
     if(can_cast_type<signedbv_typet>(operand_type))
       return signed_factory(lhs, rhs);
   }
+
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for relational expression: " +
     binary_relation.pretty());

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -327,6 +327,51 @@ TEST_CASE(
   }
 }
 
+TEST_CASE(
+  "expr to smt conversion for relational operators as applied to pointers",
+  "[core][smt2_incremental]")
+{
+  auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386);
+  // Pointer variables, used for comparisons
+  const std::size_t pointer_width = 32;
+  const auto pointer_type = pointer_typet(signedbv_typet{32}, pointer_width);
+  const symbol_exprt pointer_a("a", pointer_type);
+  const symbol_exprt pointer_b("b", pointer_type);
+  // SMT terms needed for pointer comparisons
+  const smt_termt smt_term_a =
+    smt_identifier_termt{"a", smt_bit_vector_sortt{pointer_width}};
+  const smt_termt smt_term_b =
+    smt_identifier_termt{"b", smt_bit_vector_sortt{pointer_width}};
+
+  SECTION("Greater than on pointers")
+  {
+    CHECK(
+      test.convert(greater_than_exprt{pointer_a, pointer_b}) ==
+      smt_bit_vector_theoryt::unsigned_greater_than(smt_term_a, smt_term_b));
+  }
+
+  SECTION("Greater than or equal on pointer operands")
+  {
+    CHECK(
+      test.convert(greater_than_or_equal_exprt{pointer_a, pointer_b}) ==
+      smt_bit_vector_theoryt::unsigned_greater_than_or_equal(
+        smt_term_a, smt_term_b));
+  }
+  SECTION("Less than on pointer operands")
+  {
+    CHECK(
+      test.convert(less_than_exprt{pointer_a, pointer_b}) ==
+      smt_bit_vector_theoryt::unsigned_less_than(smt_term_a, smt_term_b));
+  }
+  SECTION("Less than or equal on pointer operands")
+  {
+    CHECK(
+      test.convert(less_than_or_equal_exprt{pointer_a, pointer_b}) ==
+      smt_bit_vector_theoryt::unsigned_less_than_or_equal(
+        smt_term_a, smt_term_b));
+  }
+}
+
 TEST_CASE(
   "expr to smt conversion for arithmetic operators",
   "[core][smt2_incremental]")