Merge pull request #2852 from diffblue/dynamic_object_size

object_size can now do objects with dynamic size

Author: Daniel Kroening

regression/cbmc/dynamic_size1/stack_object.c

@@ -0,0 +1,24 @@
+struct S
+{
+  __CPROVER_size_t size;
+  char *p;
+};
+
+void func(struct S *s)
+{
+  char *p = s->p;
+  __CPROVER_size_t size = __CPROVER_OBJECT_SIZE(p);
+  __CPROVER_assert(size == s->size, "size ok");
+  p[80] = 123; // should be safe
+}
+
+int main()
+{
+  __CPROVER_size_t buffer_size;
+  __CPROVER_assume(buffer_size >= 100);
+  char buffer[buffer_size];
+  struct S s;
+  s.size = buffer_size;
+  s.p = buffer;
+  func(&s);
+}

regression/cbmc/dynamic_size1/stack_object.desc

@@ -0,0 +1,8 @@
+CORE
+stack_object.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -2164,6 +2164,21 @@ exprt c_typecheck_baset::do_special_functions(
 
     return typecast_exprt::conditional_cast(pointer_offset_expr, expr.type());
   }
+  else if(identifier == CPROVER_PREFIX "OBJECT_SIZE")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      err_location(f_op);
+      error() << "object_size expects one operand" << eom;
+      throw 0;
+    }
+
+    unary_exprt object_size_expr(
+      ID_object_size, expr.arguments()[0], size_type());
+    object_size_expr.add_source_location() = source_location;
+
+    return object_size_expr;
+  }
   else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
   {
     if(expr.arguments().size()!=1)

src/ansi-c/cprover_builtin_headers.h

@@ -37,6 +37,7 @@ void CBMC_trace(int lvl, const char *event, ...);
 // pointers
 __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
 __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
+__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
 void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);
 

src/solvers/flattening/bv_pointers.cpp

@@ -786,24 +786,17 @@ void bv_pointerst::do_postponed(
     {
       const exprt &expr=*it;
 
-      mp_integer object_size;
-
-      if(expr.id()==ID_symbol)
-      {
-        // just get the type
-        const typet &type=ns.follow(expr.type());
-
-        exprt size_expr=size_of_expr(type, ns);
+      if(expr.id() != ID_symbol)
+        continue;
 
-        if(size_expr.is_nil())
-          continue;
+      const exprt size_expr = size_of_expr(expr.type(), ns);
 
-        if(to_integer(size_expr, object_size))
-          continue;
-      }
-      else
+      if(size_expr.is_nil())
         continue;
 
+      const exprt object_size =
+        typecast_exprt::conditional_cast(size_expr, postponed.expr.type());
+
       // only compare object part
       bvt bv;
       encode(number, bv);
@@ -813,12 +806,13 @@ void bv_pointerst::do_postponed(
       bvt saved_bv=postponed.op;
       saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
 
+      bvt size_bv = convert_bv(object_size);
+
       POSTCONDITION(bv.size()==saved_bv.size());
       PRECONDITION(postponed.bv.size()>=1);
+      PRECONDITION(size_bv.size() == postponed.bv.size());
 
       literalt l1=bv_utils.equal(bv, saved_bv);
-
-      bvt size_bv=bv_utils.build_constant(object_size, postponed.bv.size());
       literalt l2=bv_utils.equal(postponed.bv, size_bv);
 
       prop.l_set_to(prop.limplies(l1, l2), true);