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

This adds checks to the C front-end that prohibit taking the address of
objects that cannot be addressed with byte-granularity pointers.  This
includes proper Booleans (not to be confused with _Bool) and
__CPROVER_bitvector-typed objects whose width is not a multiple of 8.

Fixes #7104.

Author: kroening

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(
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_bv || type.id() == ID_floatbv)
+  {
+    // 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, kroening@kroening.com
 #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;
 

src/ansi-c/c_typecheck_expr.cpp

@@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "builtin_factory.h"
 #include "c_expr.h"
 #include "c_qualifiers.h"
+#include "c_typecast.h"
 #include "c_typecheck_base.h"
 #include "expr2c.h"
 #include "padding.h"
@@ -1187,6 +1188,16 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   }
   else if(op_type.id()==ID_array)
   {
+    // This is the promotion from an array
+    // to a pointer to the first element.
+    auto error_opt = c_typecastt::check_address_can_be_taken(op_type);
+    if(error_opt.has_value())
+    {
+      error().source_location = expr.source_location();
+      error() << *error_opt << eom;
+      throw 0;
+    }
+
     index_exprt index(op, from_integer(0, c_index_type()));
     op=address_of_exprt(index);
   }
@@ -1710,17 +1721,12 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
 {
   exprt &op = to_unary_expr(expr).op();
 
-  if(op.type().id()==ID_c_bit_field)
-  {
-    error().source_location = expr.source_location();
-    error() << "cannot take address of a bit field" << eom;
-    throw 0;
-  }
+  auto error_opt = c_typecastt::check_address_can_be_taken(op.type());
 
-  if(op.is_boolean())
+  if(error_opt.has_value())
   {
     error().source_location = expr.source_location();
-    error() << "cannot take address of a single bit" << eom;
+    error() << *error_opt << eom;
     throw 0;
   }