Add support for __builtin_bit_cast

This is supported by Clang and GCC (though in C++-mode only) and now
required for SIMD1 on macOS.

Author: tautschnig

regression/cbmc/__builtin_bit_cast-01/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <inttypes.h>
+
+int main()
+{
+#if defined(__clang__) || defined(_GNUC_)
+  // GCC actually only supports __builtin_bit_cast in C++ mode, but we do it for
+  // C as well.
+  float f = 1.5;
+  assert((int32_t)f == 1);
+  int32_t i = __builtin_bit_cast(int32_t, f);
+  assert(i != 1);
+  assert(__builtin_bit_cast(float, i) == f);
+#endif
+}

regression/cbmc/__builtin_bit_cast-01/test.desc

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

src/ansi-c/c_expr.cpp

@@ -83,3 +83,8 @@ exprt enum_is_in_range_exprt::lower(const namespacet &ns) const
 
   return simplify_expr(disjunction(disjuncts), ns);
 }
+
+byte_extract_exprt bit_cast_exprt::lower() const
+{
+  return make_byte_extract(op(), from_integer(0, c_index_type()), type());
+}

src/ansi-c/c_expr.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file ansi-c/c_expr.h
 /// API to expression classes that are internal to the C frontend
 
+#include <util/byte_operators.h>
 #include <util/std_code.h>
 
 /// \brief Shuffle elements of one or two vectors, modelled after Clang's
@@ -370,4 +371,51 @@ inline enum_is_in_range_exprt &to_enum_is_in_range_expr(exprt &expr)
   return ret;
 }
 
+/// \brief Reinterpret the bits of an expression of type `S` as an expression of
+/// type `T` where `S` and `T` have the same size.
+class bit_cast_exprt : public unary_exprt
+{
+public:
+  bit_cast_exprt(exprt expr, typet type)
+    : unary_exprt(ID_bit_cast, std::move(expr), std::move(type))
+  {
+  }
+
+  byte_extract_exprt lower() const;
+};
+
+template <>
+inline bool can_cast_expr<bit_cast_exprt>(const exprt &base)
+{
+  return base.id() == ID_bit_cast;
+}
+
+inline void validate_expr(const bit_cast_exprt &value)
+{
+  validate_operands(value, 1, "bit_cast must have one operand");
+}
+
+/// \brief Cast an exprt to a \ref bit_cast_exprt
+///
+/// \a expr must be known to be \ref bit_cast_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref bit_cast_exprt
+inline const bit_cast_exprt &to_bit_cast_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bit_cast);
+  const bit_cast_exprt &ret = static_cast<const bit_cast_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_bit_cast_expr(const exprt &)
+inline bit_cast_exprt &to_bit_cast_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_bit_cast);
+  bit_cast_exprt &ret = static_cast<bit_cast_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_ANSI_C_C_EXPR_H

src/ansi-c/c_typecheck_expr.cpp

@@ -497,6 +497,24 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   {
     // already type checked
   }
+  else if(auto bit_cast_expr = expr_try_dynamic_cast<bit_cast_exprt>(expr))
+  {
+    typecheck_type(expr.type());
+    if(
+      pointer_offset_bits(bit_cast_expr->type(), *this) ==
+      pointer_offset_bits(bit_cast_expr->op().type(), *this))
+    {
+      exprt tmp = bit_cast_expr->lower();
+      expr.swap(tmp);
+    }
+    else
+    {
+      error().source_location = expr.source_location();
+      error() << "bit cast from '" << to_string(bit_cast_expr->op().type())
+              << "' to '" << to_string(expr.type()) << "' not permitted" << eom;
+      throw 0;
+    }
+  }
   else
   {
     error().source_location = expr.source_location();

src/ansi-c/parser.y

@@ -236,6 +236,7 @@ int yyansi_cerror(const std::string &error);
 %token TOK_THREAD_LOCAL "_Thread_local"
 %token TOK_NULLPTR     "nullptr"
 %token TOK_CONSTEXPR   "constexpr"
+%token TOK_BIT_CAST    "__builtin_bit_cast"
 
 /*** special scanner reports ***/
 
@@ -715,6 +716,12 @@ unary_expression:
           parser_stack($$).id(ID_alignof);
           parser_stack($$).add(ID_type_arg).swap(parser_stack($3));
         }
+        | TOK_BIT_CAST '(' type_name ',' unary_expression ')'
+        { $$=$1;
+          set($$, ID_bit_cast);
+          mto($$, $5);
+          parser_stack($$).type().swap(parser_stack($3));
+        }
         ;
 
 cast_expression:

src/ansi-c/scanner.l

@@ -1305,6 +1305,13 @@ __decltype          { if(PARSER.cpp98 &&
                     return make_identifier();
                 }
 
+"__builtin_bit_cast" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC ||
+                          PARSER.mode==configt::ansi_ct::flavourt::CLANG)
+                         { loc(); return TOK_BIT_CAST; }
+                       else
+                         return make_identifier();
+                     }
+
 {CPROVER_PREFIX}"atomic"       { loc(); return TOK_CPROVER_ATOMIC; }
 {CPROVER_PREFIX}"forall"       { loc(); return TOK_FORALL; }
 {CPROVER_PREFIX}"exists"       { loc(); return TOK_EXISTS; }

src/util/irep_ids.def

@@ -914,6 +914,7 @@ IREP_ID_ONE(prophecy_rw_ok)
 IREP_ID_ONE(prophecy_r_ok)
 IREP_ID_ONE(prophecy_w_ok)
 IREP_ID_ONE(prophecy_pointer_in_range)
+IREP_ID_ONE(bit_cast)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree