Properly checks struct members in alias expression

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

regression/contracts/assigns_enforce_structs_04/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct pair
+{
+  int x;
+  int y;
+};
+
+void f1(struct pair *p) __CPROVER_assigns(p->x)
+{
+  p->y = 2;
+}
+
+void f2(struct pair *p) __CPROVER_assigns(p->y)
+{
+  p->x = 2;
+}
+
+void f3(struct pair *p) __CPROVER_assigns(p->y)
+{
+  p->y = 0;
+}
+
+void f4(struct pair *p) __CPROVER_assigns(*p)
+{
+  p = NULL;
+}
+
+int main()
+{
+  struct pair p = {0};
+  f1(&p);
+  f2(&p);
+  assert(p.y == 2);
+  assert(p.x == 2);
+  f3(&p);
+  assert(p.y == 0);
+  f4(&p);
+  return 0;
+}

regression/contracts/assigns_enforce_structs_04/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$
+^\[f2.\d+\] line \d+ Check that p\-\>x is assignable\: FAILURE$
+^\[f3.\d+\] line \d+ Check that p\-\>y is assignable\: SUCCESS$
+^\[f4.\d+\] line \d+ Check that p is assignable\: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+Checks whether CBMC properly evaluates write set of members
+from the same object.

regression/contracts/assigns_enforce_structs_05/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+
+struct pair
+{
+  int x[3];
+  int y;
+};
+
+int f1(struct pair *p) __CPROVER_assigns(p->x)
+{
+  p->y = 2;
+  p->x[0] = 0;
+  p->x[1] = 1;
+  p->x[2] = 2;
+  return 0;
+}
+
+int main()
+{
+  struct pair p = {0};
+  f1(&p);
+  assert(p.y == 2);
+  assert(p.x[0] == 0);
+  assert(p.x[1] == 1);
+  assert(p.x[2] == 2);
+  return 0;
+}

regression/contracts/assigns_enforce_structs_05/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[f1.\d+\] line \d+ Check that p\-\>y is assignable\: FAILURE$
+^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)0\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)1\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>x\[\(.*\)2\] is assignable\: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Checks whether CBMC properly evaluates write set of members
+from the same object. In this case, we have an assigns clause 
+with a struct member `x[3]` and an assignment to the struct member `y`.
+CBMC must considers only the region of `x[3]` is assignable.

regression/contracts/assigns_enforce_structs_06/main.c

@@ -0,0 +1,46 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+struct pair
+{
+  uint8_t *buf;
+  size_t size;
+};
+
+void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
+{
+  p->buf[0] = 0;
+  p->buf[1] = 1;
+  p->buf[2] = 2;
+  p->size = 4;
+}
+
+void f2(struct pair *p) __CPROVER_assigns(p->size)
+{
+  p->buf[0] = 0;
+  p->size = 0;
+}
+
+void f3(struct pair *p) __CPROVER_assigns(*p)
+{
+  p->buf = NULL;
+  p->size = 0;
+}
+
+int main()
+{
+  struct pair *p = malloc(sizeof(*p));
+  p->size = 3;
+  p->buf = malloc(p->size);
+  f1(p);
+  assert(p->buf[0] == 0);
+  assert(p->buf[1] == 1);
+  assert(p->buf[2] == 2);
+  f2(p);
+  assert(p->size == 0);
+  f3(p);
+  assert(p->buf == NULL);
+  assert(p->size == 0);
+  return 0;
+}

regression/contracts/assigns_enforce_structs_06/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)1\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>buf\[\(.*\)2\] is assignable\: SUCCESS$
+^\[f1.\d+\] line \d+ Check that p\-\>size is assignable\: FAILURE$
+^\[f2.\d+\] line \d+ Check that p\-\>buf\[\(.*\)0\] is assignable\: FAILURE$
+^\[f2.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$
+^\[f3.\d+\] line \d+ Check that p\-\>buf is assignable\: SUCCESS$
+^\[f3.\d+\] line \d+ Check that p\-\>size is assignable\: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+Checks whether CBMC properly evaluates write set of members
+from the same object. In this case, we have a dynamic object
+as one of the struct members.

src/goto-instrument/contracts/assigns.cpp

@@ -31,7 +31,6 @@ assigns_clause_targett::assigns_clause_targett(
   INVARIANT(
     pointer_object.type().id() == ID_pointer,
     "Assigns clause targets should be stored as pointer expressions.");
-
   const symbolt &function_symbol = contract.ns.lookup(function_id);
 
   // Declare a new symbol to stand in for the reference
@@ -60,15 +59,49 @@ std::vector<symbol_exprt> assigns_clause_targett::temporary_declarations() const
   return result;
 }
 
-exprt assigns_clause_targett::alias_expression(const exprt &ptr)
+exprt assigns_clause_targett::alias_expression(const exprt &lhs)
 {
-  return same_object(ptr, local_target);
+  exprt::operandst condition;
+  exprt lhs_ptr = (lhs.id() == ID_address_of) ? to_address_of_expr(lhs).object()
+                                              : pointer_for(lhs);
+
+  // __CPROVER_same_object(lhs, target)
+  condition.push_back(same_object(lhs_ptr, target));
+
+  // If assigns target was a dereference, comparing objects is enough
+  if(target_id == ID_dereference)
+  {
+    return conjunction(condition);
+  }
+
+  const exprt lhs_offset = pointer_offset(lhs_ptr);
+  const exprt target_offset = pointer_offset(target);
+
+  // __CPROVER_offset(lhs) >= __CPROVER_offset(target)
+  condition.push_back(binary_relation_exprt(lhs_offset, ID_ge, target_offset));
+
+  const exprt region_lhs = plus_exprt(
+    typecast_exprt::conditional_cast(
+      size_of_expr(lhs.type(), contract.ns).value(), lhs_offset.type()),
+    lhs_offset);
+
+  const exprt region_target = plus_exprt(
+    typecast_exprt::conditional_cast(
+      size_of_expr(dereference_exprt(local_target).type(), contract.ns).value(),
+      target_offset.type()),
+    target_offset);
+
+  // (sizeof(lhs) + __CPROVER_offset(lhs)) <=
+  // (sizeof(target) + __CPROVER_offset(target))
+  condition.push_back(binary_relation_exprt(region_lhs, ID_le, region_target));
+
+  return conjunction(condition);
 }
 
 exprt assigns_clause_targett::compatible_expression(
   const assigns_clause_targett &called_target)
 {
-  return alias_expression(called_target.get_direct_pointer());
+  return same_object(called_target.get_direct_pointer(), local_target);
 }
 
 goto_programt
@@ -107,9 +140,9 @@ assigns_clauset::assigns_clauset(
     function_id(function_id),
     log(log_parameter)
 {
-  for(exprt current_operation : assigns_expr.operands())
+  for(exprt target : assigns_expr.operands())
   {
-    add_target(current_operation);
+    add_target(target);
   }
 }
 
@@ -121,17 +154,17 @@ assigns_clauset::~assigns_clauset()
   }
 }
 
-assigns_clause_targett *assigns_clauset::add_target(exprt current_operation)
+assigns_clause_targett *assigns_clauset::add_target(exprt target)
 {
-  assigns_clause_targett *target = new assigns_clause_targett(
-    (current_operation.id() == ID_address_of)
-      ? to_index_expr(to_address_of_expr(current_operation).object()).array()
-      : current_operation,
+  assigns_clause_targett *new_target = new assigns_clause_targett(
+    (target.id() == ID_address_of)
+      ? to_index_expr(to_address_of_expr(target).object()).array()
+      : target,
     parent,
     log,
     function_id);
-  targets.push_back(target);
-  return target;
+  targets.push_back(new_target);
+  return new_target;
 }
 
 assigns_clause_targett *
@@ -239,28 +272,18 @@ goto_programt assigns_clauset::havoc_code(
 
 exprt assigns_clauset::alias_expression(const exprt &lhs)
 {
+  // If write set is empty, no assignment is allowed.
   if(targets.empty())
   {
     return false_exprt();
   }
 
-  exprt left_ptr = assigns_clause_targett::pointer_for(lhs);
-
-  bool first_iter = true;
-  exprt result = false_exprt();
+  exprt::operandst condition;
   for(assigns_clause_targett *target : targets)
   {
-    if(first_iter)
-    {
-      result = target->alias_expression(left_ptr);
-      first_iter = false;
-    }
-    else
-    {
-      result = or_exprt(result, target->alias_expression(left_ptr));
-    }
+    condition.push_back(target->alias_expression(lhs));
   }
-  return result;
+  return disjunction(condition);
 }
 
 exprt assigns_clauset::compatible_expression(

src/goto-instrument/contracts/assigns.h

@@ -16,6 +16,9 @@ Date: July 2021
 
 #include "contracts.h"
 
+#include <ansi-c/expr2c.h>
+#include <util/pointer_offset_size.h>
+
 /// \brief A base class for assigns clause targets
 class assigns_clause_targett
 {
@@ -57,7 +60,7 @@ class assigns_clauset
     messaget log_parameter);
   ~assigns_clauset();
 
-  assigns_clause_targett *add_target(exprt current_operation);
+  assigns_clause_targett *add_target(exprt target);
   assigns_clause_targett *add_pointer_target(exprt current_operation);
   goto_programt init_block(source_locationt location);
   goto_programt &temporary_declarations(