Merge pull request #7444 from diffblue/pointer-to-bit

prohibit pointers to bit-vectors that are not byte-aligned

Author: kroening

regression/ansi-c/Pointer-to-non-byte/pointer-to-bool.c

@@ -0,0 +1,6 @@
+__CPROVER_bool x;
+
+int main()
+{
+  void *p = &x; // should error
+}

regression/ansi-c/Pointer-to-non-byte/pointer-to-bool.desc

@@ -0,0 +1,7 @@
+CORE
+pointer-to-bool.c
+
+cannot take address of a proper Boolean$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--

regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array1.c

@@ -0,0 +1,6 @@
+__CPROVER_bitvector[123] z[10];
+
+int main()
+{
+  void *p = z; // should error
+}

regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array1.desc

@@ -0,0 +1,7 @@
+CORE
+pointer-to-bv-array1.c
+
+bitvector must have width that is a multiple of CHAR_BIT$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--

regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array2.c

@@ -0,0 +1,6 @@
+__CPROVER_bitvector[123] z[10];
+
+int main()
+{
+  void *p = (int *)z; // should error
+}

regression/ansi-c/Pointer-to-non-byte/pointer-to-bv-array2.desc

@@ -0,0 +1,7 @@
+CORE
+pointer-to-bv-array2.c
+
+bitvector must have width that is a multiple of CHAR_BIT$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--

regression/ansi-c/Pointer-to-non-byte/pointer-to-bv.c

@@ -0,0 +1,6 @@
+__CPROVER_bitvector[15] y;
+
+int main()
+{
+  void *p = &y; // should error
+}

regression/ansi-c/Pointer-to-non-byte/pointer-to-bv.desc

@@ -0,0 +1,7 @@
+CORE
+pointer-to-bv.c
+
+bitvector must have width that is a multiple of CHAR_BIT$
+^EXIT=(1|64)$
+^SIGNAL=0$
+--

src/ansi-c/c_typecast.cpp

@@ -739,6 +739,15 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
 
   if(src_type.id()==ID_array)
   {
+    // This is the promotion from an array
+    // to a pointer to the first element.
+    auto error_opt = check_address_can_be_taken(expr.type());
+    if(error_opt.has_value())
+    {
+      errors.push_back(error_opt.value());
+      return;
+    }
+
     index_exprt index(expr, from_integer(0, c_index_type()));
     expr = typecast_exprt::conditional_cast(address_of_exprt(index), dest_type);
     return;
@@ -765,3 +774,31 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
     }
   }
 }
+
+optionalt<std::string>
+c_typecastt::check_address_can_be_taken(const typet &type)
+{
+  if(type.id() == ID_c_bit_field)
+    return std::string("cannot take address of a bit field");
+
+  if(type.id() == ID_bool)
+    return std::string("cannot take address of a proper Boolean");
+
+  if(can_cast_type<bitvector_typet>(type))
+  {
+    // The width of the bitvector must be a multiple of CHAR_BIT.
+    auto width = to_bitvector_type(type).get_width();
+    if(width % config.ansi_c.char_width != 0)
+    {
+      return std::string(
+        "bitvector must have width that is a multiple of CHAR_BIT");
+    }
+    else
+      return {};
+  }
+
+  if(type.id() == ID_array)
+    return check_address_can_be_taken(to_array_type(type).element_type());
+
+  return {}; // ok
+}

src/ansi-c/c_typecast.h

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANSI_C_C_TYPECAST_H
 #define CPROVER_ANSI_C_C_TYPECAST_H
 
+#include <util/optional.h>
+
 #include <list>
 #include <string>
 
@@ -65,6 +67,10 @@ class c_typecastt
   std::list<std::string> errors;
   std::list<std::string> warnings;
 
+  /// \return empty when address can be taken,
+  /// error message otherwise
+  static optionalt<std::string> check_address_can_be_taken(const typet &);
+
 protected:
   const namespacet &ns;