Limit dereferencing checks to actual access size

For member accesses, access to other components need not be valid as
shown in the included regression test Malloc23.

Also do not require --bounds-check for full dereferencing checks.

Fixes #219.

Author: tautschnig

regression/cbmc/Function5/test.desc

@@ -3,6 +3,6 @@ main.c
 --pointer-check --bounds-check
 ^SIGNAL=0$
 ^EXIT=10$
-^\[.*\] dereference failure: object bounds in \*p: FAILURE$
+^\[.*\] dereference failure: pointer outside object bounds in \*p: FAILURE$
 --
 ^warning: ignoring

regression/cbmc/Malloc23/main.c

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main()
+{
+  struct A *p=malloc(sizeof(int));
+  p->x=0; // OK
+  p->y=0; // out of bounds
+
+  struct A o=*p; // out of bounds
+
+  int *p2=malloc(sizeof(int));
+  p2[0]=0; // OK
+  p2[1]=0; // out of bounds
+
+  ++p2;
+  p2[0]=0; // out of bounds
+
+  return 0;
+}

regression/cbmc/Malloc23/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+pointer outside dynamic object bounds in \*p: FAILURE
+pointer outside dynamic object bounds in \*p: FAILURE
+pointer outside dynamic object bounds in p2\[(signed long int)1\]: FAILURE
+pointer outside dynamic object bounds in p2\[(signed long int)0\]: FAILURE
+\*\* 4 of 36 failed (3 iterations)
+--
+^warning: ignoring

src/analyses/goto_check.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_types.h>
 #include <util/guard.h>
 #include <util/base_type.h>
+#include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 #include <util/cprover_prefix.h>
 #include <util/options.h>
@@ -73,7 +74,11 @@ class goto_checkt
   void undefined_shift_check(const shift_exprt &expr, const guardt &guard);
   void pointer_rel_check(const exprt &expr, const guardt &guard);
   void pointer_overflow_check(const exprt &expr, const guardt &guard);
-  void pointer_validity_check(const dereference_exprt &expr, const guardt &guard);
+  void pointer_validity_check(
+    const dereference_exprt &expr,
+    const guardt &guard,
+    const exprt &access_lb,
+    const exprt &access_ub);
   void integer_overflow_check(const exprt &expr, const guardt &guard);
   void conversion_check(const exprt &expr, const guardt &guard);
   void float_overflow_check(const exprt &expr, const guardt &guard);
@@ -966,7 +971,9 @@ Function: goto_checkt::pointer_validity_check
 
 void goto_checkt::pointer_validity_check(
   const dereference_exprt &expr,
-  const guardt &guard)
+  const guardt &guard,
+  const exprt &access_lb,
+  const exprt &access_ub)
 {
   if(!enable_pointer_check)
     return;
@@ -1047,42 +1054,44 @@ void goto_checkt::pointer_validity_check(
         expr,
         guard);
 
-    if(enable_bounds_check)
+    if(flags.is_unknown() || flags.is_dynamic_heap())
     {
-      if(flags.is_unknown() || flags.is_dynamic_heap())
-      {
-        exprt dynamic_bounds=
-          or_exprt(dynamic_object_lower_bound(pointer),
-                   dynamic_object_upper_bound(pointer, dereference_type, ns));
+      exprt dynamic_bounds=
+        or_exprt(dynamic_object_lower_bound(pointer, ns, access_lb),
+                 dynamic_object_upper_bound(
+                   pointer,
+                   dereference_type,
+                   ns,
+                   access_ub));
 
-        add_guarded_claim(
-          implies_exprt(malloc_object(pointer, ns), not_exprt(dynamic_bounds)),
-          "dereference failure: dynamic object bounds",
-          "pointer dereference",
-          expr.find_source_location(),
-          expr,
-          guard);
-      }
+      add_guarded_claim(
+        implies_exprt(malloc_object(pointer, ns), not_exprt(dynamic_bounds)),
+        "dereference failure: pointer outside dynamic object bounds",
+        "pointer dereference",
+        expr.find_source_location(),
+        expr,
+        guard);
     }
 
-    if(enable_bounds_check)
+    if(flags.is_unknown() ||
+       flags.is_dynamic_local() ||
+       flags.is_static_lifetime())
     {
-      if(flags.is_unknown() ||
-         flags.is_dynamic_local() ||
-         flags.is_static_lifetime())
-      {
-        exprt object_bounds=
-          or_exprt(object_lower_bound(pointer),
-                   object_upper_bound(pointer, dereference_type, ns));
+      exprt object_bounds=
+        or_exprt(object_lower_bound(pointer, ns, access_lb),
+                 object_upper_bound(
+                   pointer,
+                   dereference_type,
+                   ns,
+                   access_ub));
 
-        add_guarded_claim(
-          or_exprt(dynamic_object(pointer), not_exprt(object_bounds)),
-          "dereference failure: object bounds",
-          "pointer dereference",
-          expr.find_source_location(),
-          expr,
-          guard);
-      }
+      add_guarded_claim(
+        or_exprt(dynamic_object(pointer), not_exprt(object_bounds)),
+        "dereference failure: pointer outside object bounds",
+        "pointer dereference",
+        expr.find_source_location(),
+        expr,
+        guard);
     }
   }
 }
@@ -1130,7 +1139,7 @@ void goto_checkt::bounds_check(
   typet array_type=ns.follow(expr.array().type());
 
   if(array_type.id()==ID_pointer)
-    return; // done by the pointer code
+    throw "index got pointer as array type";
   else if(array_type.id()==ID_incomplete_array)
     throw "index got incomplete array";
   else if(array_type.id()!=ID_array && array_type.id()!=ID_vector)
@@ -1434,6 +1443,27 @@ void goto_checkt::check_rec(
 
     return;
   }
+  else if(expr.id()==ID_member &&
+          to_member_expr(expr).struct_op().id()==ID_dereference)
+  {
+    const member_exprt &member=to_member_expr(expr);
+    const dereference_exprt &deref=
+      to_dereference_expr(member.struct_op());
+
+    check_rec(deref.op0(), guard, false);
+
+    exprt access_ub=nil_exprt();
+
+    exprt member_offset=member_offset_expr(member, ns);
+    exprt size=size_of_expr(expr.type(), ns);
+
+    if(member_offset.is_not_nil() && size.is_not_nil())
+      access_ub=plus_exprt(member_offset, size);
+
+    pointer_validity_check(deref, guard, member_offset, access_ub);
+
+    return;
+  }
 
   forall_operands(it, expr)
     check_rec(*it, guard, false);
@@ -1491,7 +1521,11 @@ void goto_checkt::check_rec(
           expr.id()==ID_ge || expr.id()==ID_gt)
     pointer_rel_check(expr, guard);
   else if(expr.id()==ID_dereference)
-    pointer_validity_check(to_dereference_expr(expr), guard);
+    pointer_validity_check(
+      to_dereference_expr(expr),
+      guard,
+      nil_exprt(),
+      size_of_expr(expr.type(), ns));
 }
 
 /*******************************************************************\

src/pointer-analysis/value_set_dereference.cpp

@@ -425,7 +425,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
           // check lower bound
           guardt tmp_guard(guard);
           tmp_guard.add(is_malloc_object);
-          tmp_guard.add(dynamic_object_lower_bound(pointer_expr));
+          tmp_guard.add(
+            dynamic_object_lower_bound(
+              pointer_expr,
+              ns,
+              nil_exprt()));
           dereference_callback.dereference_failure(
             "pointer dereference",
             "dynamic object lower bound", tmp_guard);
@@ -439,7 +443,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
           guardt tmp_guard(guard);
           tmp_guard.add(is_malloc_object);
-          tmp_guard.add(dynamic_object_upper_bound(pointer_expr, dereference_type, ns));
+          tmp_guard.add(
+            dynamic_object_upper_bound(
+              pointer_expr,
+              dereference_type,
+              ns,
+              size_of_expr(dereference_type, ns)));
           dereference_callback.dereference_failure(
             "pointer dereference",
             "dynamic object upper bound", tmp_guard);

src/util/pointer_predicates.cpp

@@ -241,8 +241,15 @@ exprt good_pointer_def(
   exprt good_dynamic_tmp1=
     or_exprt(
       not_exprt(malloc_object(pointer, ns)),
-      and_exprt(not_exprt(dynamic_object_lower_bound(pointer)),
-                not_exprt(dynamic_object_upper_bound(pointer, dereference_type, ns))));
+      and_exprt(not_exprt(dynamic_object_lower_bound(
+                    pointer,
+                    ns,
+                    nil_exprt())),
+                not_exprt(dynamic_object_upper_bound(
+                    pointer,
+                    dereference_type,
+                    ns,
+                    size_of_expr(dereference_type, ns)))));
 
   exprt good_dynamic_tmp2=
     and_exprt(not_exprt(deallocated(pointer, ns)),
@@ -259,8 +266,12 @@ exprt good_pointer_def(
     not_exprt(invalid_pointer(pointer));
 
   exprt bad_other=
-    or_exprt(object_lower_bound(pointer),
-             object_upper_bound(pointer, dereference_type, ns));
+    or_exprt(object_lower_bound(pointer, ns, nil_exprt()),
+             object_upper_bound(
+               pointer,
+               dereference_type,
+               ns,
+               size_of_expr(dereference_type, ns)));
 
   exprt good_other=
     or_exprt(dynamic_object(pointer),
@@ -357,9 +368,12 @@ Function: dynamic_object_lower_bound
 
 \*******************************************************************/
 
-exprt dynamic_object_lower_bound(const exprt &pointer)
+exprt dynamic_object_lower_bound(
+  const exprt &pointer,
+  const namespacet &ns,
+  const exprt &offset)
 {
-  return object_lower_bound(pointer);
+  return object_lower_bound(pointer, ns, offset);
 }
 
 /*******************************************************************\
@@ -377,25 +391,31 @@ Function: dynamic_object_upper_bound
 exprt dynamic_object_upper_bound(
   const exprt &pointer,
   const typet &dereference_type,
-  const namespacet &ns)
+  const namespacet &ns,
+  const exprt &access_size)
 {
   // this is
-  // POINTER_OFFSET(p)+size>__CPROVER_malloc_size
+  // POINTER_OFFSET(p)+access_size>__CPROVER_malloc_size
 
   exprt malloc_size=dynamic_size(ns);
 
   exprt object_offset=pointer_offset(pointer);
 
-  exprt size=size_of_expr(dereference_type, ns);
-
   // need to add size
-  exprt sum=plus_exprt(object_offset, size);
+  irep_idt op=ID_ge;
+  exprt sum=object_offset;
+
+  if(access_size.is_not_nil())
+  {
+    op=ID_gt;
+    sum=plus_exprt(object_offset, access_size);
+  }
 
   if(ns.follow(sum.type())!=
      ns.follow(malloc_size.type()))
     sum.make_typecast(malloc_size.type());
 
-  return binary_relation_exprt(sum, ID_gt, malloc_size);
+  return binary_relation_exprt(sum, op, malloc_size);
 }
 
 /*******************************************************************\
@@ -413,25 +433,32 @@ Function: object_upper_bound
 exprt object_upper_bound(
   const exprt &pointer,
   const typet &dereference_type,
-  const namespacet &ns)
+  const namespacet &ns,
+  const exprt &access_size)
 {
   // this is
-  // POINTER_OFFSET(p)+size>OBJECT_SIZE(pointer)
+  // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer)
 
   exprt object_size_expr=object_size(pointer);
 
   exprt object_offset=pointer_offset(pointer);
 
-  exprt size=size_of_expr(dereference_type, ns);
-
   // need to add size
-  exprt sum=plus_exprt(object_offset, size);
+  irep_idt op=ID_ge;
+  exprt sum=object_offset;
+
+  if(access_size.is_not_nil())
+  {
+    op=ID_gt;
+    sum=plus_exprt(object_offset, access_size);
+  }
+
 
   if(ns.follow(sum.type())!=
      ns.follow(object_size_expr.type()))
     sum.make_typecast(object_size_expr.type());
 
-  return binary_relation_exprt(sum, ID_gt, object_size_expr);
+  return binary_relation_exprt(sum, op, object_size_expr);
 }
 
 /*******************************************************************\
@@ -446,12 +473,24 @@ Function: object_lower_bound
 
 \*******************************************************************/
 
-exprt object_lower_bound(const exprt &pointer)
+exprt object_lower_bound(
+  const exprt &pointer,
+  const namespacet &ns,
+  const exprt &offset)
 {
-  exprt offset=pointer_offset(pointer);
+  exprt p_offset=pointer_offset(pointer);
 
-  exprt zero=from_integer(0, offset.type());
+  exprt zero=from_integer(0, p_offset.type());
   assert(zero.is_not_nil());
 
-  return binary_relation_exprt(offset, ID_lt, zero);
+  if(offset.is_not_nil())
+  {
+    if(ns.follow(p_offset.type())!=ns.follow(offset.type()))
+      p_offset=
+        plus_exprt(p_offset, typecast_exprt(offset, p_offset.type()));
+    else
+      p_offset=plus_exprt(p_offset, offset);
+  }
+
+  return binary_relation_exprt(p_offset, ID_lt, zero);
 }