Merge pull request #8328 from tautschnig/github-no-macos-11

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

Author: tautschnig

.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 @@ 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, [email protected]
 /// \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