Merge pull request #126 from tautschnig/malloc-bugfix

malloc(sizeof(T)*n) for non-const n should still yield an array of subtype T

Author: Daniel Kroening

regression/cbmc/Malloc22/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+#include <stdlib.h>
+
+unsigned nondet_unsigned();
+
+int main() {
+  unsigned n = nondet_unsigned();
+  __CPROVER_assume(n>0);
+  unsigned pA[n];
+  unsigned *p = (unsigned *)malloc(sizeof(unsigned) * n);
+
+  for (int i=0; i<n; i++) {
+    p[i] = i;
+    pA[i] = i;
+  }
+  assert(p[n-1] == n-1);
+  assert(pA[n-1] == n-1);
+  assert(0);
+
+  return 0;
+}
+

regression/cbmc/Malloc22/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--unwind 2 --smt2 --outfile main.smt2
+^EXIT=0$
+^SIGNAL=0$
+--
+^Invalid expression: failed to get width of byte_update

regression/cbmc/big-endian-array1/main.c

@@ -15,7 +15,13 @@ int main()
 
   char *p=(char *)array;
   char p0=p[0];
+  char p1=p[1];
+  char p2=p[2];
+  char p3=p[3];
   __CPROVER_assert(p0==1, "p[0] matches");
+  __CPROVER_assert(p1==2, "p[1] matches");
+  __CPROVER_assert(p2==3, "p[2] matches");
+  __CPROVER_assert(p3==4, "p[3] matches");
 
   unsigned short *q=(unsigned short *)array;
   unsigned short q0=q[0];

src/ansi-c/expr2c.cpp

@@ -1914,6 +1914,15 @@ std::string expr2ct::convert_symbol(
     }
 
     dest=id2string(entry->second);
+
+    #if 0
+    if(has_prefix(id2string(id), "symex_dynamic::dynamic_object"))
+    {
+      if(sizeof_nesting++ == 0)
+        dest+=" /*"+convert(src.type());
+      if(--sizeof_nesting == 0) dest+="*/";
+    }
+    #endif
   }
 
   if(src.id()==ID_next_symbol)

src/goto-symex/symex_builtin_functions.cpp

@@ -94,8 +94,26 @@ void goto_symext::symex_malloc(
         // Did the size get multiplied?
         mp_integer elem_size=pointer_offset_size(tmp_type, ns);
         mp_integer alloc_size;
-        if(elem_size<0 || to_integer(tmp_size, alloc_size))
+
+        if(elem_size<0)
+        {
+        }
+        else if(to_integer(tmp_size, alloc_size) &&
+                tmp_size.id()==ID_mult &&
+                tmp_size.operands().size()==2 &&
+                (tmp_size.op0().is_constant() ||
+                 tmp_size.op1().is_constant()))
         {
+          exprt s=tmp_size.op0();
+          if(s.is_constant())
+          {
+            s=tmp_size.op1();
+            assert(c_sizeof_type_rec(tmp_size.op0())==tmp_type);
+          }
+          else
+            assert(c_sizeof_type_rec(tmp_size.op1())==tmp_type);
+
+          object_type=array_typet(tmp_type, s);
         }
         else
         {

src/solvers/flattening/flatten_byte_operators.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
 #include <util/pointer_offset_size.h>
+#include <util/byte_operators.h>
+#include <util/namespace.h>
 
 #include "flatten_byte_operators.h"
 
@@ -28,11 +30,9 @@ Function: flatten_byte_extract
 \*******************************************************************/
 
 exprt flatten_byte_extract(
-  const exprt &src,
+  const byte_extract_exprt &src,
   const namespacet &ns)
 {
-  assert(src.id()==ID_byte_extract_little_endian ||
-         src.id()==ID_byte_extract_big_endian);
   assert(src.operands().size()==2);
 
   bool little_endian;
@@ -47,39 +47,45 @@ exprt flatten_byte_extract(
   mp_integer size_bits=pointer_offset_bits(src.type(), ns);
   if(size_bits<0)
     throw "byte_extract flatting with non-constant size: "+src.pretty();
-  std::size_t width_bits=integer2unsigned(size_bits);
-
-  std::size_t width_bytes=width_bits/8+(width_bits%8==0?0:1);
-  
-  const typet &t=src.op0().type();
 
-  if(t.id()==ID_array)
+  if(src.op0().type().id()==ID_array)
   {
-    const array_typet &array_type=to_array_type(t);
+    const exprt &root=src.op0();
+    const exprt &offset=src.op1();
+
+    const array_typet &array_type=to_array_type(root.type());
     const typet &subtype=array_type.subtype();
+
+    mp_integer element_width=pointer_offset_bits(subtype, ns);
+    if(element_width<0) // failed
+      throw "failed to flatten array with unknown element width";
+
+    mp_integer num_elements=
+      size_bits/element_width+((size_bits%element_width==0)?0:1);
+
+    const typet &offset_type=ns.follow(offset.type());
 
     // byte-array?
-    if((subtype.id()==ID_unsignedbv ||
-        subtype.id()==ID_signedbv) &&
-       to_bitvector_type(subtype).get_width()==8)
+    if(element_width==8)
     {
       // get 'width'-many bytes, and concatenate
+      std::size_t width_bytes=integer2unsigned(num_elements);
       exprt::operandst op;
-      op.resize(width_bytes);
+      op.reserve(width_bytes);
 
       for(std::size_t i=0; i<width_bytes; i++)
       {
         // the most significant byte comes first in the concatenation!
-        std::size_t offset_i=
+        std::size_t offset_int=
           little_endian?(width_bytes-i-1):i;
 
-        plus_exprt offset(from_integer(offset_i, src.op1().type()), src.op1());
-        index_exprt index_expr(subtype);
-        index_expr.array()=src.op0();
-        index_expr.index()=offset;
-        op[i]=index_expr;
+        plus_exprt offset_i(from_integer(offset_int, offset_type), offset);
+        index_exprt index_expr(root, offset_i);
+        op.push_back(index_expr);
       }
 
+      // TODO this doesn't seem correct if size_bits%8!=0 as more
+      // bits than the original expression will be returned.
       if(width_bytes==1)
         return op[0];
       else // width_bytes>=2
@@ -91,44 +97,36 @@ exprt flatten_byte_extract(
     }
     else // non-byte array
     {
-      const exprt &root=src.op0();
-      const exprt &offset=src.op1();
-      const typet &array_type=ns.follow(root.type());
-      const typet &offset_type=ns.follow(offset.type());
-      const typet &element_type=ns.follow(array_type.subtype());
-      mp_integer element_width=pointer_offset_size(element_type, ns);
-      
-      if(element_width==-1) // failed
-        throw "failed to flatten non-byte array with unknown element width";
-
-      mp_integer result_width=pointer_offset_size(src.type(), ns);
-      mp_integer num_elements=(element_width+result_width-2)/element_width+1;
+      // add an extra element as the access need not be aligned with
+      // element boundaries and could thus stretch over extra elements
+      ++num_elements;
 
       // compute new root and offset
       concatenation_exprt concat(
-        unsignedbv_typet(integer2unsigned(element_width*8*num_elements)));
+        unsignedbv_typet(integer2unsigned(element_width*num_elements)));
 
+      assert(element_width%8==0);
       exprt first_index=
-        (element_width==1)?offset 
-        : div_exprt(offset, from_integer(element_width, offset_type)); // 8*offset/el_w
+        div_exprt(offset, from_integer(element_width/8, offset_type));
 
-      for(mp_integer i=num_elements; i>0; --i)
+      // byte extract will do the appropriate mapping, thus MSB comes
+      // last here (as opposed to the above, where no further byte
+      // extract is involved)
+      for(mp_integer i=0; i<num_elements; ++i)
       {
-        plus_exprt index(first_index, from_integer(i-1, offset_type));
+        // the most significant byte comes first in the concatenation!
+        plus_exprt index(first_index, from_integer(i, offset_type));
         concat.copy_to_operands(index_exprt(root, index));
       }
 
-      // the new offset is width%offset
-      exprt new_offset;
-      
-      if(element_width==1)
-        new_offset=from_integer(0, offset_type);
-      else
-        new_offset=mod_exprt(offset, from_integer(element_width, offset_type));
+      // the new offset is offset%width
+      mod_exprt new_offset(offset,
+                           from_integer(element_width/8, offset_type));
 
       // build new byte-extract expression
-      exprt tmp(src.id(), src.type());
-      tmp.copy_to_operands(concat, new_offset);
+      byte_extract_exprt tmp(src);
+      tmp.op()=concat;
+      tmp.offset()=new_offset;
 
       return tmp;
     }
@@ -166,7 +164,7 @@ exprt flatten_byte_extract(
 
     extractbits.src()=left_shift;
     extractbits.type()=src.type();
-    extractbits.upper()=from_integer(width_bits-1, offset_type);
+    extractbits.upper()=from_integer(size_bits-1, offset_type);
     extractbits.lower()=from_integer(0, offset_type);
 
     return extractbits;
@@ -186,11 +184,9 @@ Function: flatten_byte_update
 \*******************************************************************/
 
 exprt flatten_byte_update(
-  const exprt &src,
+  const byte_update_exprt &src,
   const namespacet &ns)
 {
-  assert(src.id()==ID_byte_update_little_endian ||
-         src.id()==ID_byte_update_big_endian);
   assert(src.operands().size()==3);
 
   mp_integer element_size=
@@ -233,7 +229,7 @@ exprt flatten_byte_update(
           }
           else
           {
-            exprt byte_extract_expr(
+            byte_extract_exprt byte_extract_expr(
               src.id()==ID_byte_update_little_endian?ID_byte_extract_little_endian:
               src.id()==ID_byte_update_big_endian?ID_byte_extract_big_endian:
               throw "unexpected src.id() in flatten_byte_update",
@@ -265,7 +261,7 @@ exprt flatten_byte_update(
 
           index_exprt index_expr(src.op0(), div_offset, array_type.subtype());
 
-          exprt byte_update_expr(src.id(), array_type.subtype());
+          byte_update_exprt byte_update_expr(src.id(), array_type.subtype());
           byte_update_expr.copy_to_operands(index_expr, mod_offset, src.op2());
 
           // Call recurisvely, the array is gone!            
@@ -380,10 +376,10 @@ exprt flatten_byte_operators(const exprt &src, const namespacet &ns)
 
   if(src.id()==ID_byte_update_little_endian ||
      src.id()==ID_byte_update_big_endian)
-    return flatten_byte_update(tmp, ns);
+    return flatten_byte_update(to_byte_update_expr(tmp), ns);
   else if(src.id()==ID_byte_extract_little_endian ||
           src.id()==ID_byte_extract_big_endian)
-    return flatten_byte_extract(tmp, ns);
+    return flatten_byte_extract(to_byte_extract_expr(tmp), ns);
   else
     return tmp;
 }

src/solvers/flattening/flatten_byte_operators.h

@@ -9,11 +9,17 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_FLATTEN_BYTE_OPERATORS_H
 #define CPROVER_FLATTEN_BYTE_OPERATORS_H
 
-#include <util/expr.h>
-#include <util/namespace.h>
+class byte_extract_exprt;
+class byte_update_exprt;
+class exprt;
+class namespacet;
 
-exprt flatten_byte_extract(const exprt &src, const namespacet &ns);
-exprt flatten_byte_update(const exprt &src, const namespacet &ns);
+exprt flatten_byte_extract(
+  const byte_extract_exprt &src,
+  const namespacet &ns);
+exprt flatten_byte_update(
+  const byte_update_exprt &src,
+  const namespacet &ns);
 exprt flatten_byte_operators(const exprt &src, const namespacet &ns);
 bool has_byte_operator(const exprt &src);
 

src/solvers/smt1/smt1_conv.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/base_type.h>
 #include <util/ieee_float.h>
+#include <util/byte_operators.h>
 
 #include <ansi-c/string_constant.h>
 
@@ -470,7 +471,7 @@ Function: smt1_convt::convert_byte_extract
 \*******************************************************************/
 
 void smt1_convt::convert_byte_extract(
-  const exprt &expr,
+  const byte_extract_exprt &expr,
   bool bool_as_bv)
 {
   // we just run the flattener
@@ -1183,7 +1184,7 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
   else if(expr.id()==ID_byte_extract_little_endian ||
           expr.id()==ID_byte_extract_big_endian)
   {
-    convert_byte_extract(expr, bool_as_bv);
+    convert_byte_extract(to_byte_extract_expr(expr), bool_as_bv);
   }
   else if(expr.id()==ID_byte_update_little_endian ||
           expr.id()==ID_byte_update_big_endian)

src/solvers/smt1/smt1_conv.h

@@ -20,6 +20,7 @@ Revision: Roberto Bruttomesso, [email protected]
 #include <solvers/flattening/pointer_logic.h>
 #include <solvers/flattening/boolbv_width.h>
 
+class byte_extract_exprt;
 class typecast_exprt;
 class constant_exprt;
 class index_exprt;
@@ -77,7 +78,9 @@ class smt1_convt:public prop_convt
 
   // specific expressions go here
   void convert_byte_update(const exprt &expr, bool bool_as_bv);
-  void convert_byte_extract(const exprt &expr, bool bool_as_bv);
+  void convert_byte_extract(
+    const byte_extract_exprt &expr,
+    bool bool_as_bv);
   void convert_typecast(const typecast_exprt &expr, bool bool_as_bv);
   void convert_struct(const exprt &expr);
   void convert_union(const exprt &expr);

src/util/byte_operators.h

@@ -127,6 +127,12 @@ class byte_update_exprt:public exprt
     operands().resize(3);
   }
 
+  inline byte_update_exprt(irep_idt _id, const typet &_type):
+    exprt(_id, _type)
+  {
+    operands().resize(3);
+  }
+
   inline byte_update_exprt(
     irep_idt _id,
     const exprt &_op, const exprt &_offset, const exprt &_value):