Skip to content

Commit bc46c88

Browse files
tautschnigtautschnig
authored
Merge pull request #8328 from tautschnig/github-no-macos-11
Switch GitHub CI jobs from macos-11 to macos-13
2 parents 2a5151c + 4eadc8a commit bc46c88

File tree

22 files changed

+189
-22
lines changed

22 files changed

+189
-22
lines changed

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

+6-6
Original file line numberDiff line numberDiff line change
@@ -583,8 +583,8 @@ jobs:
583583
run: cd build; ctest . -V -L THOROUGH -j2
584584

585585
# This job takes approximately 39 to 69 minutes
586-
check-macos-11-make-clang:
587-
runs-on: macos-11
586+
check-macos-13-make-clang:
587+
runs-on: macos-13
588588
steps:
589589
- uses: actions/checkout@v4
590590
with:
@@ -617,8 +617,8 @@ jobs:
617617
- name: Build using Make
618618
run: |
619619
make -C src minisat2-download cadical-download
620-
make -C src -j3 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
621-
make -C jbmc/src -j3 CXX="ccache clang++"
620+
make -C src -j4 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
621+
make -C jbmc/src -j4 CXX="ccache clang++"
622622
make -C unit "CXX=ccache clang++"
623623
make -C jbmc/unit "CXX=ccache clang++"
624624
- name: Print ccache stats
@@ -630,9 +630,9 @@ jobs:
630630
- name: Run JBMC unit tests
631631
run: cd jbmc/unit; ./unit_tests
632632
- name: Run regression tests
633-
run: make -C regression test-parallel JOBS=3
633+
run: make -C regression test-parallel JOBS=4
634634
- name: Run JBMC regression tests
635-
run: make -C jbmc/regression test-parallel JOBS=3
635+
run: make -C jbmc/regression test-parallel JOBS=4
636636

637637
# This job takes approximately 66 to 85 minutes
638638
check-macos-12-cmake-clang:

‎.github/workflows/release-packages.yaml

+1-1
Original file line numberDiff line numberDiff line change
@@ -152,7 +152,7 @@ jobs:
152152
SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 20.04 package built and uploaded successfully' || 'Ubuntu 20.04 package build failed' }}"
153153

154154
homebrew-pr:
155-
runs-on: macos-11
155+
runs-on: macos-13
156156
steps:
157157
- name: Get release tag name
158158
# The GITHUB_REF we get has refs/tags/ in front of the tag name so we

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

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

‎regression/cbmc/__builtin_bit_cast-01/main.c

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
#include <inttypes.h>
3+
4+
int main()
5+
{
6+
#if defined(__clang__) || defined(_GNUC_)
7+
// GCC actually only supports __builtin_bit_cast in C++ mode, but we do it for
8+
// C as well.
9+
float f = 1.5;
10+
assert((int32_t)f == 1);
11+
int32_t i = __builtin_bit_cast(int32_t, f);
12+
assert(i != 1);
13+
assert(__builtin_bit_cast(float, i) == f);
14+
#endif
15+
}

‎regression/cbmc/__builtin_bit_cast-01/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎src/ansi-c/ansi_c_language.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,7 @@ bool ansi_c_languaget::parse(
7676
ansi_c_parser.in=&codestr;
7777
ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
7878
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
79+
ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
7980
ansi_c_parser.float16_type = config.ansi_c.float16_type;
8081
ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
8182
ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
@@ -201,6 +202,7 @@ bool ansi_c_languaget::to_expr(
201202
ansi_c_parser.in=&i_preprocessed;
202203
ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
203204
ansi_c_parser.ts_18661_3_Floatn_types=config.ansi_c.ts_18661_3_Floatn_types;
205+
ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
204206
ansi_c_parser.float16_type = config.ansi_c.float16_type;
205207
ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
206208
ansi_c_parser.fp16_type = config.ansi_c.fp16_type;

‎src/ansi-c/ansi_c_parser.h

+2
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ class ansi_c_parsert:public parsert
3636
cpp11(false),
3737
for_has_scope(false),
3838
ts_18661_3_Floatn_types(false),
39+
__float128_is_keyword(false),
3940
float16_type(false),
4041
bf16_type(false),
4142
fp16_type(false)
@@ -68,6 +69,7 @@ class ansi_c_parsert:public parsert
6869

6970
// ISO/IEC TS 18661-3:2015
7071
bool ts_18661_3_Floatn_types;
72+
bool __float128_is_keyword;
7173
bool float16_type;
7274
bool bf16_type;
7375
bool fp16_type;

‎src/ansi-c/builtin_factory.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@ static bool convert(
5252
ansi_c_parser.in=&in;
5353
ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope;
5454
ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types;
55+
ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
5556
ansi_c_parser.float16_type = config.ansi_c.float16_type;
5657
ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
5758
ansi_c_parser.fp16_type = config.ansi_c.fp16_type;

‎src/ansi-c/c_expr.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -83,3 +83,8 @@ exprt enum_is_in_range_exprt::lower(const namespacet &ns) const
8383

8484
return simplify_expr(disjunction(disjuncts), ns);
8585
}
86+
87+
byte_extract_exprt bit_cast_exprt::lower() const
88+
{
89+
return make_byte_extract(op(), from_integer(0, c_index_type()), type());
90+
}

‎src/ansi-c/c_expr.h

+48
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
/// \file ansi-c/c_expr.h
1313
/// API to expression classes that are internal to the C frontend
1414

15+
#include <util/byte_operators.h>
1516
#include <util/std_code.h>
1617

1718
/// \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)
370371
return ret;
371372
}
372373

374+
/// \brief Reinterpret the bits of an expression of type `S` as an expression of
375+
/// type `T` where `S` and `T` have the same size.
376+
class bit_cast_exprt : public unary_exprt
377+
{
378+
public:
379+
bit_cast_exprt(exprt expr, typet type)
380+
: unary_exprt(ID_bit_cast, std::move(expr), std::move(type))
381+
{
382+
}
383+
384+
byte_extract_exprt lower() const;
385+
};
386+
387+
template <>
388+
inline bool can_cast_expr<bit_cast_exprt>(const exprt &base)
389+
{
390+
return base.id() == ID_bit_cast;
391+
}
392+
393+
inline void validate_expr(const bit_cast_exprt &value)
394+
{
395+
validate_operands(value, 1, "bit_cast must have one operand");
396+
}
397+
398+
/// \brief Cast an exprt to a \ref bit_cast_exprt
399+
///
400+
/// \a expr must be known to be \ref bit_cast_exprt.
401+
///
402+
/// \param expr: Source expression
403+
/// \return Object of type \ref bit_cast_exprt
404+
inline const bit_cast_exprt &to_bit_cast_expr(const exprt &expr)
405+
{
406+
PRECONDITION(expr.id() == ID_bit_cast);
407+
const bit_cast_exprt &ret = static_cast<const bit_cast_exprt &>(expr);
408+
validate_expr(ret);
409+
return ret;
410+
}
411+
412+
/// \copydoc to_bit_cast_expr(const exprt &)
413+
inline bit_cast_exprt &to_bit_cast_expr(exprt &expr)
414+
{
415+
PRECONDITION(expr.id() == ID_bit_cast);
416+
bit_cast_exprt &ret = static_cast<bit_cast_exprt &>(expr);
417+
validate_expr(ret);
418+
return ret;
419+
}
420+
373421
#endif // CPROVER_ANSI_C_C_EXPR_H

‎src/ansi-c/c_typecheck_expr.cpp

+31-3
Original file line numberDiff line numberDiff line change
@@ -497,6 +497,24 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
497497
{
498498
// already type checked
499499
}
500+
else if(auto bit_cast_expr = expr_try_dynamic_cast<bit_cast_exprt>(expr))
501+
{
502+
typecheck_type(expr.type());
503+
if(
504+
pointer_offset_bits(bit_cast_expr->type(), *this) ==
505+
pointer_offset_bits(bit_cast_expr->op().type(), *this))
506+
{
507+
exprt tmp = bit_cast_expr->lower();
508+
expr.swap(tmp);
509+
}
510+
else
511+
{
512+
error().source_location = expr.source_location();
513+
error() << "bit cast from '" << to_string(bit_cast_expr->op().type())
514+
<< "' to '" << to_string(expr.type()) << "' not permitted" << eom;
515+
throw 0;
516+
}
517+
}
500518
else
501519
{
502520
error().source_location = expr.source_location();
@@ -2151,7 +2169,9 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
21512169
}
21522170
else if(
21532171
identifier == CPROVER_PREFIX "saturating_minus" ||
2154-
identifier == CPROVER_PREFIX "saturating_plus")
2172+
identifier == CPROVER_PREFIX "saturating_plus" ||
2173+
identifier == "__builtin_elementwise_add_sat" ||
2174+
identifier == "__builtin_elementwise_sub_sat")
21552175
{
21562176
exprt result = typecheck_saturating_arithmetic(expr);
21572177
expr.swap(result);
@@ -3824,10 +3844,18 @@ exprt c_typecheck_baset::typecheck_saturating_arithmetic(
38243844
}
38253845

38263846
exprt result;
3827-
if(identifier == CPROVER_PREFIX "saturating_minus")
3847+
if(
3848+
identifier == CPROVER_PREFIX "saturating_minus" ||
3849+
identifier == "__builtin_elementwise_sub_sat")
3850+
{
38283851
result = saturating_minus_exprt{expr.arguments()[0], expr.arguments()[1]};
3829-
else if(identifier == CPROVER_PREFIX "saturating_plus")
3852+
}
3853+
else if(
3854+
identifier == CPROVER_PREFIX "saturating_plus" ||
3855+
identifier == "__builtin_elementwise_add_sat")
3856+
{
38303857
result = saturating_plus_exprt{expr.arguments()[0], expr.arguments()[1]};
3858+
}
38313859
else
38323860
UNREACHABLE;
38333861

‎src/ansi-c/compiler_headers/gcc_builtin_headers_types.h

+6
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,9 @@ typedef short __gcc_v4hi __attribute__ ((__vector_size__ (8)));
1717
typedef short __gcc_v8hi __attribute__ ((__vector_size__ (16)));
1818
typedef short __gcc_v16hi __attribute__ ((__vector_size__ (32)));
1919
typedef short __gcc_v32hi __attribute__ ((__vector_size__ (64)));
20+
typedef __CPROVER_Float16 __gcc_v8hf __attribute__ ((__vector_size__ (16)));
21+
typedef __CPROVER_Float16 __gcc_v16hf __attribute__ ((__vector_size__ (32)));
22+
typedef __CPROVER_Float16 __gcc_v32hf __attribute__ ((__vector_size__ (64)));
2023
typedef float __gcc_v2sf __attribute__ ((__vector_size__ (8)));
2124
typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16)));
2225
typedef float __gcc_v8sf __attribute__ ((__vector_size__ (32)));
@@ -28,7 +31,10 @@ typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8)));
2831
typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16)));
2932
typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32)));
3033
typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64)));
34+
typedef unsigned short __gcc_v32uhi __attribute__ ((__vector_size__ (64)));
35+
typedef unsigned int __gcc_v16usi __attribute__ ((__vector_size__ (64)));
3136
typedef unsigned long long __gcc_di;
37+
typedef unsigned long long __gcc_v8udi __attribute__ ((__vector_size__ (64)));
3238

3339
enum __gcc_atomic_memmodels {
3440
__ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST

‎src/ansi-c/gcc_version.cpp

+6
Original file line numberDiff line numberDiff line change
@@ -162,6 +162,12 @@ void configure_gcc(const gcc_versiont &gcc_version)
162162
config.ansi_c.gcc__float128_type =
163163
gcc_version.flavor == gcc_versiont::flavort::GCC &&
164164
gcc_version.is_at_least(4u, gcc_float128_minor_version);
165+
config.ansi_c.__float128_is_keyword =
166+
gcc_version.flavor == gcc_versiont::flavort::CLANG ||
167+
(gcc_version.flavor == gcc_versiont::flavort::GCC &&
168+
config.ansi_c.arch == "arm64" &&
169+
config.ansi_c.os == configt::ansi_ct::ost::OS_MACOS &&
170+
config.ansi_c.gcc__float128_type);
165171

166172
config.ansi_c.float16_type =
167173
(gcc_version.flavor == gcc_versiont::flavort::GCC &&

‎src/ansi-c/parser.y

+7
Original file line numberDiff line numberDiff line change
@@ -236,6 +236,7 @@ int yyansi_cerror(const std::string &error);
236236
%token TOK_THREAD_LOCAL "_Thread_local"
237237
%token TOK_NULLPTR "nullptr"
238238
%token TOK_CONSTEXPR "constexpr"
239+
%token TOK_BIT_CAST "__builtin_bit_cast"
239240

240241
/*** special scanner reports ***/
241242

@@ -715,6 +716,12 @@ unary_expression:
715716
parser_stack($$).id(ID_alignof);
716717
parser_stack($$).add(ID_type_arg).swap(parser_stack($3));
717718
}
719+
| TOK_BIT_CAST '(' type_name ',' unary_expression ')'
720+
{ $$=$1;
721+
set($$, ID_bit_cast);
722+
mto($$, $5);
723+
parser_stack($$).type().swap(parser_stack($3));
724+
}
718725
;
719726

720727
cast_expression:

‎src/ansi-c/scanner.l

+12-3
Original file line numberDiff line numberDiff line change
@@ -540,6 +540,10 @@ enable_or_disable ("enable"|"disable")
540540
return make_identifier();
541541
}
542542

543+
{CPROVER_PREFIX}"Float16" {
544+
loc(); return TOK_GCC_FLOAT16;
545+
}
546+
543547
"__bf16" { if(PARSER.bf16_type)
544548
{ loc(); return TOK_GCC_FLOAT16; }
545549
else
@@ -584,9 +588,7 @@ enable_or_disable ("enable"|"disable")
584588
loc(); return TOK_GCC_FLOAT80;
585589
}
586590

587-
"__float128" { // This is a keyword for CLANG,
588-
// but a typedef for GCC
589-
if(PARSER.mode==configt::ansi_ct::flavourt::CLANG)
591+
"__float128" { if(PARSER.__float128_is_keyword)
590592
{ loc(); return TOK_GCC_FLOAT128; }
591593
else
592594
return make_identifier();
@@ -1307,6 +1309,13 @@ __decltype { if(PARSER.cpp98 &&
13071309
return make_identifier();
13081310
}
13091311

1312+
"__builtin_bit_cast" { if(PARSER.mode==configt::ansi_ct::flavourt::GCC ||
1313+
PARSER.mode==configt::ansi_ct::flavourt::CLANG)
1314+
{ loc(); return TOK_BIT_CAST; }
1315+
else
1316+
return make_identifier();
1317+
}
1318+
13101319
{CPROVER_PREFIX}"atomic" { loc(); return TOK_CPROVER_ATOMIC; }
13111320
{CPROVER_PREFIX}"forall" { loc(); return TOK_FORALL; }
13121321
{CPROVER_PREFIX}"exists" { loc(); return TOK_EXISTS; }

‎src/cpp/cpp_parser.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ bool cpp_parsert::parse()
4040
config.cpp.cpp_standard == configt::cppt::cpp_standardt::CPP17;
4141
token_buffer.ansi_c_parser.ts_18661_3_Floatn_types =
4242
false; // these are still typedefs
43+
token_buffer.ansi_c_parser.__float128_is_keyword = false;
4344
token_buffer.ansi_c_parser.float16_type = *support_float16;
4445
token_buffer.ansi_c_parser.bf16_type = *support_float16;
4546
token_buffer.ansi_c_parser.fp16_type = *support_float16;

‎src/cpp/parse.cpp

+9-5
Original file line numberDiff line numberDiff line change
@@ -772,11 +772,12 @@ bool Parser::isTypeSpecifier()
772772
|| t == TOK_SIGNED || t == TOK_UNSIGNED || t == TOK_FLOAT ||
773773
t == TOK_DOUBLE || t == TOK_INT8 || t == TOK_INT16 || t == TOK_INT32 ||
774774
t == TOK_INT64 || t == TOK_GCC_INT128 || t == TOK_PTR32 ||
775-
t == TOK_PTR64 || t == TOK_GCC_FLOAT80 || t == TOK_GCC_FLOAT128 ||
776-
t == TOK_VOID || t == TOK_BOOL || t == TOK_CPROVER_BOOL ||
777-
t == TOK_CLASS || t == TOK_STRUCT || t == TOK_UNION || t == TOK_ENUM ||
778-
t == TOK_INTERFACE || t == TOK_TYPENAME || t == TOK_TYPEOF ||
779-
t == TOK_DECLTYPE || t == TOK_UNDERLYING_TYPE;
775+
t == TOK_PTR64 || t == TOK_GCC_FLOAT16 || t == TOK_GCC_FLOAT80 ||
776+
t == TOK_GCC_FLOAT128 || t == TOK_VOID || t == TOK_BOOL ||
777+
t == TOK_CPROVER_BOOL || t == TOK_CLASS || t == TOK_STRUCT ||
778+
t == TOK_UNION || t == TOK_ENUM || t == TOK_INTERFACE ||
779+
t == TOK_TYPENAME || t == TOK_TYPEOF || t == TOK_DECLTYPE ||
780+
t == TOK_UNDERLYING_TYPE;
780781
}
781782

782783
/*
@@ -2510,6 +2511,9 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p)
25102511
case TOK_INT32: type_id=ID_int32; break;
25112512
case TOK_INT64: type_id=ID_int64; break;
25122513
case TOK_GCC_INT128: type_id=ID_gcc_int128; break;
2514+
case TOK_GCC_FLOAT16:
2515+
type_id = ID_gcc_float16;
2516+
break;
25132517
case TOK_GCC_FLOAT80: type_id=ID_gcc_float80; break;
25142518
case TOK_GCC_FLOAT128: type_id=ID_gcc_float128; break;
25152519
case TOK_BOOL:

‎src/goto-instrument/contracts/contracts_wrangler.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,7 @@ void contracts_wranglert::mangle(
145145
ansi_c_parser.in = &is;
146146
ansi_c_parser.for_has_scope = config.ansi_c.for_has_scope;
147147
ansi_c_parser.ts_18661_3_Floatn_types = config.ansi_c.ts_18661_3_Floatn_types;
148+
ansi_c_parser.__float128_is_keyword = config.ansi_c.__float128_is_keyword;
148149
ansi_c_parser.float16_type = config.ansi_c.float16_type;
149150
ansi_c_parser.bf16_type = config.ansi_c.bf16_type;
150151
ansi_c_parser.fp16_type = config.ansi_c.fp16_type;

0 commit comments

Comments
 (0)