Improve array bounds checks

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

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -3,7 +3,7 @@ main.c
 --bounds-check --32
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.array_bounds\.5\] array.List upper bound in .*: FAILURE$
-^\*\* 1 of 9 failed (2 iterations)$
+array\.List dynamic object upper bound in p->List\[2\]: FAILURE
+\*\* 1 of 11 failed (2 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;
@@ -1029,63 +1036,62 @@ void goto_checkt::pointer_validity_check(
         expr,
         guard);
 
-    if(mode != ID_java)
-    {
-      if(flags.is_unknown() || flags.is_dynamic_heap())
-        add_guarded_claim(
-          not_exprt(deallocated(pointer, ns)),
-          "dereference failure: deallocated dynamic object",
-          "pointer dereference",
-          expr.find_source_location(),
-          expr,
-          guard);
+    if(flags.is_unknown() || flags.is_dynamic_heap())
+      add_guarded_claim(
+        not_exprt(deallocated(pointer, ns)),
+        "dereference failure: deallocated dynamic object",
+        "pointer dereference",
+        expr.find_source_location(),
+        expr,
+        guard);
 
-      if(flags.is_unknown() || flags.is_dynamic_local())
-        add_guarded_claim(
-          not_exprt(dead_object(pointer, ns)),
-          "dereference failure: dead object",
-          "pointer dereference",
-          expr.find_source_location(),
-          expr,
-          guard);
-    }
+    if(flags.is_unknown() || flags.is_dynamic_local())
+      add_guarded_claim(
+        not_exprt(dead_object(pointer, ns)),
+        "dereference failure: dead object",
+        "pointer dereference",
+        expr.find_source_location(),
+        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);
     }
   }
 }
@@ -1133,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)
@@ -1193,6 +1199,8 @@ void goto_checkt::bounds_check(
     }
   }
 
+  exprt type_matches_size=true_exprt();
+
   if(ode.root_object().id()==ID_dereference)
   {
     const exprt &pointer=
@@ -1218,13 +1226,18 @@ void goto_checkt::bounds_check(
 
     add_guarded_claim(
       precond,
-      name+" upper bound",
+      name+" dynamic object upper bound",
       "array bounds",
       expr.find_source_location(),
       expr,
       guard);
 
-    return;
+    exprt type_size=size_of_expr(ode.root_object().type(), ns);
+    if(type_size.is_not_nil())
+      type_matches_size=
+        equal_exprt(
+          size,
+          typecast_exprt(type_size, size.type()));
   }
 
   const exprt &size=array_type.id()==ID_array ?
@@ -1257,7 +1270,7 @@ void goto_checkt::bounds_check(
       inequality.op1().make_typecast(inequality.op0().type());
 
     add_guarded_claim(
-      inequality,
+      implies_exprt(type_matches_size, inequality),
       name+" upper bound",
       "array bounds",
       expr.find_source_location(),
@@ -1430,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);
@@ -1487,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);