Switch GitHub CI jobs from macos-11 to macos-13

.github/workflows/pull-request-checks.yaml

@@ -583,8 +583,8 @@ jobs:
         run: cd build; ctest . -V -L THOROUGH -j2
 
   # This job takes approximately 39 to 69 minutes
-  check-macos-11-make-clang:
-    runs-on: macos-11
+  check-macos-13-make-clang:
+    runs-on: macos-13
     steps:
       - uses: actions/checkout@v4
         with:
@@ -617,8 +617,8 @@ jobs:
       - name: Build using Make
         run: |
           make -C src minisat2-download cadical-download
-          make -C src -j3 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
-          make -C jbmc/src -j3 CXX="ccache clang++"
+          make -C src -j4 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
+          make -C jbmc/src -j4 CXX="ccache clang++"
           make -C unit "CXX=ccache clang++"
           make -C jbmc/unit "CXX=ccache clang++"
       - name: Print ccache stats
@@ -630,9 +630,9 @@ jobs:
       - name: Run JBMC unit tests
         run: cd jbmc/unit; ./unit_tests
       - name: Run regression tests
-        run: make -C regression test-parallel JOBS=3
+        run: make -C regression test-parallel JOBS=4
       - name: Run JBMC regression tests
-        run: make -C jbmc/regression test-parallel JOBS=3
+        run: make -C jbmc/regression test-parallel JOBS=4
 
   # This job takes approximately 66 to 85 minutes
   check-macos-12-cmake-clang:

.github/workflows/release-packages.yaml

@@ -152,7 +152,7 @@ jobs:
           SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 20.04 package built and uploaded successfully' || 'Ubuntu 20.04 package build failed' }}"
 
   homebrew-pr:
-    runs-on: macos-11
+    runs-on: macos-13
     steps:
       - name: Get release tag name
         # The GITHUB_REF we get has refs/tags/ in front of the tag name so we

jbmc/regression/jbmc-strings/StringIndexOf/test_thorough.desc

@@ -1,7 +1,13 @@
-CORE
+THOROUGH
 Test
---function Test.check --unwind 10 --no-unwinding-assertions --max-nondet-string-length 10 --java-assume-inputs-non-null
+--function Test.check --unwind 10 --no-unwinding-assertions --max-nondet-string-length 10 --java-assume-inputs-non-null --sat-solver cadical
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
+--
+This test completes in less than 3 seconds with CaDiCaL
+--
+This test completes in less than 3 seconds with CaDiCaL, but may flip between
+seconds and several minutes with MiniSat even just changing the order of
+equations.

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/ansi_c_language.cpp

@@ -76,6 +76,7 @@ bool ansi_c_languaget::parse(
   ansi_c_parser.in=&codestr;
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
+  ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
   ansi_c_parser.float16_type = config.ansi_c.float16_type;
   ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
   ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
@@ -201,6 +202,7 @@ bool ansi_c_languaget::to_expr(
   ansi_c_parser.in=&i_preprocessed;
   ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
+  ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
   ansi_c_parser.float16_type = config.ansi_c.float16_type;
   ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
   ansi_c_parser.fp16_type = config.ansi_c.fp16_type;

src/ansi-c/ansi_c_parser.h

@@ -36,6 +36,7 @@ class ansi_c_parsert:public parsert
       cpp11(false),
       for_has_scope(false),
       ts_18661_3_Floatn_types(false),
+      __float128_is_keyword(false),
       float16_type(false),
       bf16_type(false),
       fp16_type(false)
@@ -68,6 +69,7 @@ class ansi_c_parsert:public parsert
 
   // ISO/IEC TS 18661-3:2015
   bool ts_18661_3_Floatn_types;
+  bool __float128_is_keyword;
   bool float16_type;
   bool bf16_type;
   bool fp16_type;

src/ansi-c/builtin_factory.cpp

@@ -52,6 +52,7 @@ static bool convert(
   ansi_c_parser.in=∈
   ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types;
+  ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
   ansi_c_parser.float16_type = config.ansi_c.float16_type;
   ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
   ansi_c_parser.fp16_type = config.ansi_c.fp16_type;

src/ansi-c/c_expr.cpp

@@ -83,3 +83,8 @@
 
   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 @@
 /// \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 @@
   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 @@
   {
     // 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();
@@ -2151,7 +2169,9 @@
       }
       else if(
         identifier == CPROVER_PREFIX "saturating_minus" ||
-        identifier == CPROVER_PREFIX "saturating_plus")
+        identifier == CPROVER_PREFIX "saturating_plus" ||
+        identifier == "__builtin_elementwise_add_sat" ||
+        identifier == "__builtin_elementwise_sub_sat")
       {
         exprt result = typecheck_saturating_arithmetic(expr);
         expr.swap(result);
@@ -3824,10 +3844,18 @@
   }
 
   exprt result;
-  if(identifier == CPROVER_PREFIX "saturating_minus")
+  if(
+    identifier == CPROVER_PREFIX "saturating_minus" ||
+    identifier == "__builtin_elementwise_sub_sat")
+  {
     result = saturating_minus_exprt{expr.arguments()[0], expr.arguments()[1]};
-  else if(identifier == CPROVER_PREFIX "saturating_plus")
+  }
+  else if(
+    identifier == CPROVER_PREFIX "saturating_plus" ||
+    identifier == "__builtin_elementwise_add_sat")
+  {
     result = saturating_plus_exprt{expr.arguments()[0], expr.arguments()[1]};
+  }
   else
     UNREACHABLE;
 

src/ansi-c/compiler_headers/gcc_builtin_headers_types.h

@@ -17,6 +17,9 @@ typedef short  __gcc_v4hi  __attribute__ ((__vector_size__ (8)));
 typedef short  __gcc_v8hi  __attribute__ ((__vector_size__ (16)));
 typedef short  __gcc_v16hi __attribute__ ((__vector_size__ (32)));
 typedef short  __gcc_v32hi __attribute__ ((__vector_size__ (64)));
+typedef __CPROVER_Float16  __gcc_v8hf  __attribute__ ((__vector_size__ (16)));
+typedef __CPROVER_Float16  __gcc_v16hf  __attribute__ ((__vector_size__ (32)));
+typedef __CPROVER_Float16  __gcc_v32hf  __attribute__ ((__vector_size__ (64)));
 typedef float  __gcc_v2sf  __attribute__ ((__vector_size__ (8)));
 typedef float  __gcc_v4sf  __attribute__ ((__vector_size__ (16)));
 typedef float  __gcc_v8sf  __attribute__ ((__vector_size__ (32)));
@@ -28,7 +31,10 @@ typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8)));
 typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16)));
 typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32)));
 typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64)));
+typedef unsigned short __gcc_v32uhi __attribute__ ((__vector_size__ (64)));
+typedef unsigned int __gcc_v16usi  __attribute__ ((__vector_size__ (64)));
 typedef unsigned long long __gcc_di;
+typedef unsigned long long __gcc_v8udi __attribute__ ((__vector_size__ (64)));
 
 enum __gcc_atomic_memmodels {
   __ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST

src/ansi-c/gcc_version.cpp

@@ -162,6 +162,12 @@
   config.ansi_c.gcc__float128_type =
     gcc_version.flavor == gcc_versiont::flavort::GCC &&
     gcc_version.is_at_least(4u, gcc_float128_minor_version);
+  config.ansi_c.__float128_is_keyword =
+    gcc_version.flavor == gcc_versiont::flavort::CLANG ||
+    (gcc_version.flavor == gcc_versiont::flavort::GCC &&
+     config.ansi_c.arch == "arm64" &&
+     config.ansi_c.os == configt::ansi_ct::ost::OS_MACOS &&
+     config.ansi_c.gcc__float128_type);
 
   config.ansi_c.float16_type =
     (gcc_version.flavor == gcc_versiont::flavort::GCC &&

src/ansi-c/parser.y

@@ -236,6 +236,7 @@
 %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 @@
           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

@@ -540,6 +540,10 @@
                     return make_identifier();
                 }
 
+{CPROVER_PREFIX}"Float16" {
+                  loc(); return TOK_GCC_FLOAT16;
+                }
+
 "__bf16"        { if(PARSER.bf16_type)
                   { loc(); return TOK_GCC_FLOAT16; }
                   else
@@ -584,9 +588,7 @@
                   loc(); return TOK_GCC_FLOAT80;
                 }
 
-"__float128"    { // This is a keyword for CLANG,
-                  // but a typedef for GCC
-                  if(PARSER.mode==configt::ansi_ct::flavourt::CLANG)
+"__float128"    { if(PARSER.__float128_is_keyword)
                   { loc(); return TOK_GCC_FLOAT128; }
                   else
                     return make_identifier();
@@ -1307,6 +1309,13 @@
                     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/cpp/cpp_parser.cpp

@@ -40,6 +40,7 @@ bool cpp_parsert::parse()
     config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
   token_buffer.ansi_c_parser.ts_18661_3_Floatn_types =
     false; // these are still typedefs
+  token_buffer.ansi_c_parser.__float128_is_keyword = false;
   token_buffer.ansi_c_parser.float16_type = *support_float16;
   token_buffer.ansi_c_parser.bf16_type = *support_float16;
   token_buffer.ansi_c_parser.fp16_type = *support_float16;

src/cpp/parse.cpp

@@ -772,11 +772,12 @@
          || t == TOK_SIGNED || t == TOK_UNSIGNED || t == TOK_FLOAT ||
          t == TOK_DOUBLE || t == TOK_INT8 || t == TOK_INT16 || t == TOK_INT32 ||
          t == TOK_INT64 || t == TOK_GCC_INT128 || t == TOK_PTR32 ||
-         t == TOK_PTR64 || t == TOK_GCC_FLOAT80 || t == TOK_GCC_FLOAT128 ||
-         t == TOK_VOID || t == TOK_BOOL || t == TOK_CPROVER_BOOL ||
-         t == TOK_CLASS || t == TOK_STRUCT || t == TOK_UNION || t == TOK_ENUM ||
-         t == TOK_INTERFACE || t == TOK_TYPENAME || t == TOK_TYPEOF ||
-         t == TOK_DECLTYPE || t == TOK_UNDERLYING_TYPE;
+         t == TOK_PTR64 || t == TOK_GCC_FLOAT16 || t == TOK_GCC_FLOAT80 ||
+         t == TOK_GCC_FLOAT128 || t == TOK_VOID || t == TOK_BOOL ||
+         t == TOK_CPROVER_BOOL || t == TOK_CLASS || t == TOK_STRUCT ||
+         t == TOK_UNION || t == TOK_ENUM || t == TOK_INTERFACE ||
+         t == TOK_TYPENAME || t == TOK_TYPEOF || t == TOK_DECLTYPE ||
+         t == TOK_UNDERLYING_TYPE;
 }
 
 /*
@@ -2510,6 +2511,9 @@
     case TOK_INT32: type_id=ID_int32; break;
     case TOK_INT64: type_id=ID_int64; break;
     case TOK_GCC_INT128: type_id=ID_gcc_int128; break;
+    case TOK_GCC_FLOAT16:
+      type_id = ID_gcc_float16;
+      break;
     case TOK_GCC_FLOAT80: type_id=ID_gcc_float80; break;
     case TOK_GCC_FLOAT128: type_id=ID_gcc_float128; break;
     case TOK_BOOL:

src/goto-instrument/contracts/contracts_wrangler.cpp

@@ -145,6 +145,7 @@ void contracts_wranglert::mangle(
   ansi_c_parser.in = &is;
   ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
   ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types;
+  ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
   ansi_c_parser.float16_type = config.ansi_c.float16_type;
   ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
   ansi_c_parser.fp16_type = config.ansi_c.fp16_type;