comparisons of pointers to symbols

Author: jezhiggins

regression/goto-analyzer/pointer-comparison-equality-array-of-struct-members/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int main()
+{
+  struct int_pair
+  {
+    int a;
+    int b;
+  };
+  struct int_pair x[2];
+
+  int *pa = &(x[0].a);
+
+  assert(pa == &(x[0].a));
+  assert(pa != &(x[0].a));
+  assert(pa == &(x[0].b));
+  assert(pa != &(x[0].b));
+  assert(pa == &(x[1].a));
+  assert(pa != &(x[1].a));
+  assert(pa == &(x[1].b));
+  assert(pa != &(x[1].b));
+}

regression/goto-analyzer/pointer-comparison-equality-array-of-struct-members/test-constants.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion pa == &\(x\[0\].a\): SUCCESS
+^\[main.assertion.2\] .* assertion pa != &\(x\[0\].a\): FAILURE
+^\[main.assertion.3\] .* assertion pa == &\(x\[0\].b\): FAILURE
+^\[main.assertion.4\] .* assertion pa != &\(x\[0\].b\): SUCCESS
+^\[main.assertion.5\] .* assertion pa == &\(x\[1\].a\): FAILURE
+^\[main.assertion.6\] .* assertion pa != &\(x\[1\].a\): SUCCESS
+^\[main.assertion.7\] .* assertion pa == &\(x\[1\].b\): FAILURE
+^\[main.assertion.8\] .* assertion pa != &\(x\[1\].b\): SUCCESS

regression/goto-analyzer/pointer-comparison-equality-array-of-struct-members/test-top-bottom.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion pa == &\(x\[0\].a\): UNKNOWN
+^\[main.assertion.2\] .* assertion pa != &\(x\[0\].a\): UNKNOWN
+^\[main.assertion.3\] .* assertion pa == &\(x\[0\].b\): UNKNOWN
+^\[main.assertion.4\] .* assertion pa != &\(x\[0\].b\): UNKNOWN
+^\[main.assertion.5\] .* assertion pa == &\(x\[1\].a\): UNKNOWN
+^\[main.assertion.6\] .* assertion pa != &\(x\[1\].a\): UNKNOWN
+^\[main.assertion.7\] .* assertion pa == &\(x\[1\].b\): UNKNOWN
+^\[main.assertion.8\] .* assertion pa != &\(x\[1\].b\): UNKNOWN

regression/goto-analyzer/pointer-comparison-equality-array-of-struct-members/test-value-set.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion pa == &\(x\[0\].a\): SUCCESS
+^\[main.assertion.2\] .* assertion pa != &\(x\[0\].a\): FAILURE
+^\[main.assertion.3\] .* assertion pa == &\(x\[0\].b\): FAILURE
+^\[main.assertion.4\] .* assertion pa != &\(x\[0\].b\): SUCCESS
+^\[main.assertion.5\] .* assertion pa == &\(x\[1\].a\): FAILURE
+^\[main.assertion.6\] .* assertion pa != &\(x\[1\].a\): SUCCESS
+^\[main.assertion.7\] .* assertion pa == &\(x\[1\].b\): FAILURE
+^\[main.assertion.8\] .* assertion pa != &\(x\[1\].b\): SUCCESS

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -81,10 +81,16 @@ bool constant_pointer_abstract_objectt::same_target(
   if(value_stack.is_top_value() || cast_other->value_stack.is_top_value())
     return false;
 
-  bool matching_pointer = value_stack.target_expression() ==
-                          cast_other->value_stack.target_expression();
+  if(value_stack.depth() != cast_other->value_stack.depth())
+    return false;
+
+  for(size_t d = 0; d != value_stack.depth() - 1; ++d)
+    if(
+      value_stack.target_expression(d) !=
+      cast_other->value_stack.target_expression(d))
+      return false;
 
-  return matching_pointer;
+  return true;
 }
 
 exprt constant_pointer_abstract_objectt::offset() const
@@ -319,6 +325,21 @@ exprt struct_member_ptr_comparison_expr(
   return nil_exprt();
 }
 
+exprt symbol_ptr_comparison_expr(
+  irep_idt const &id,
+  exprt const &lhs,
+  exprt const &rhs)
+{
+  auto const &lhs_identifier = to_symbol_expr(lhs).get_identifier();
+  auto const &rhs_identifier = to_symbol_expr(rhs).get_identifier();
+
+  if(id == ID_equal)
+    return to_bool_expr(lhs_identifier == rhs_identifier);
+  if(id == ID_notequal)
+    return to_bool_expr(lhs_identifier != rhs_identifier);
+  return nil_exprt();
+}
+
 exprt constant_pointer_abstract_objectt::ptr_comparison_expr(
   const exprt &expr,
   const std::vector<abstract_object_pointert> &operands,
@@ -347,6 +368,8 @@ exprt constant_pointer_abstract_objectt::ptr_comparison_expr(
     if(lhs_offset.id() == ID_member)
       return struct_member_ptr_comparison_expr(
         expr.id(), lhs_offset, rhs_offset);
+    if(lhs_offset.id() == ID_symbol)
+      return symbol_ptr_comparison_expr(expr.id(), lhs_offset, rhs_offset);
 
     return binary_relation_exprt(lhs_offset, expr.id(), rhs_offset);
   }

src/analyses/variable-sensitivity/write_stack.cpp

@@ -202,18 +202,23 @@ exprt write_stackt::to_expression() const
   return std::move(top_expr);
 }
 
-exprt write_stackt::target_expression() const
+size_t write_stackt::depth() const
+{
+  return stack.size();
+}
+
+exprt write_stackt::target_expression(size_t depth) const
 {
   PRECONDITION(!is_top_value());
-  return stack[0]->get_access_expr();
+  return stack[depth]->get_access_expr();
 }
 
 exprt write_stackt::offset_expression() const
 {
   PRECONDITION(!is_top_value());
   auto const &access = stack.back()->get_access_expr();
 
-  if(access.id() == ID_member)
+  if(access.id() == ID_member || access.id() == ID_symbol)
     return access;
 
   if(access.id() == ID_index)

src/analyses/variable-sensitivity/write_stack.h

@@ -29,7 +29,9 @@ class write_stackt
     const namespacet &ns);
 
   exprt to_expression() const;
-  exprt target_expression() const;
+
+  size_t depth() const;
+  exprt target_expression(size_t depth) const;
   exprt offset_expression() const;
   bool is_top_value() const;