Merge pull request #4697 from tautschnig/fix-value-set-filtering

Value-set filtering: gracefully handle pointer arithmetic

Author: tautschnig

regression/cbmc/Pointer_Arithmetic16/main.c

@@ -0,0 +1,10 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *ptr = malloc(sizeof(int) * 2);
+  int *other_ptr;
+  if(ptr + 1 == other_ptr)
+    return 0;
+  __CPROVER_assert(0, "");
+}

regression/cbmc/Pointer_Arithmetic16/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Value-set filtering did not take into account arithemetic over pointers and thus
+spuriously failed an invariant.

src/goto-symex/symex_goto.cpp

@@ -70,10 +70,9 @@ void goto_symext::apply_goto_condition(
 /// Try to evaluate a simple pointer comparison.
 /// \param operation: ID_equal or ID_not_equal
 /// \param symbol_expr: The symbol expression in the condition
-/// \param other_operand: The other expression in the condition - must pass
-///   goto_symex_is_constant, and since it is pointer-typed it must therefore
-///   be an address of expression, a typecast of an address of expression or a
-///   null pointer
+/// \param other_operand: The other expression in the condition; we only support
+///   an address of expression, a typecast of an address of expression or a
+///   null pointer, and return an empty optionalt in all other cases
 /// \param value_set: The value-set for looking up what the symbol can point to
 /// \param language_mode: The language mode
 /// \param ns: A namespace
@@ -90,12 +89,12 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
   const constant_exprt *constant_expr =
     expr_try_dynamic_cast<constant_exprt>(other_operand);
 
-  INVARIANT(
-    skip_typecast(other_operand).id() == ID_address_of ||
-      (constant_expr && constant_expr->get_value() == ID_NULL),
-    "An expression that passes goto_symex_is_constant and has "
-    "pointer-type must be an address of expression (possibly with some "
-    "typecasts) or a null pointer");
+  if(
+    skip_typecast(other_operand).id() != ID_address_of &&
+    (!constant_expr || constant_expr->get_value() != ID_NULL))
+  {
+    return {};
+  }
 
   const ssa_exprt *ssa_symbol_expr =
     expr_try_dynamic_cast<ssa_exprt>(symbol_expr);