Skip to content

Commit 54026f1

Browse files
kroeningkroening
committed
C23 keywords
This adds scanner, parser and typechecker support for the new C23 keywords.
1 parent cbdab7f commit 54026f1

21 files changed

+287
-72
lines changed

‎regression/cbmc/_BitInt/_BitInt1.c

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
// _BitInt is a C23 feature
2+
#include <assert.h>
3+
4+
int main()
5+
{
6+
// sizeof
7+
assert(sizeof(_BitInt(32)) == 4);
8+
assert(sizeof(_BitInt(33)) == 8);
9+
assert(sizeof(_BitInt(65)) == 16);
10+
assert(sizeof(_BitInt(128)) == 16);
11+
12+
// casts
13+
//assert((_BitInt(4))17 == 1);
14+
//assert((_BitInt(4)) - 1 == -1);
15+
//assert((unsigned _BitInt(4)) - 1 == 15);
16+
17+
// promotion (or lack thereof)
18+
//assert((unsigned _BitInt(4))15 + (unsigned _BitInt(4))1 == 0);
19+
assert((unsigned _BitInt(4))15 + (unsigned _BitInt(5))1 == 16);
20+
//assert((unsigned _BitInt(4))15 + (signed _BitInt(5))1 == -16);
21+
assert((unsigned _BitInt(4))15 + 1 == 16);
22+
23+
// pointers
24+
_BitInt(3) x, *p = &x;
25+
*p = 1;
26+
27+
return 0;
28+
}

‎regression/cbmc/_BitInt/_BitInt1.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
_BitInt1.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎regression/cbmc/constants/predefined-constants1.c

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
int main()
2+
{
3+
// C23 predefined constants
4+
__CPROVER_assert(!false, "false");
5+
__CPROVER_assert(true, "true");
6+
__CPROVER_assert(nullptr == 0, "nullptr");
7+
}

‎regression/cbmc/constants/predefined-constants1.desc

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

‎regression/cbmc/static_assert/static_assert1.c

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// C23 introduces the "static_assert" keyword.
2+
3+
struct S
4+
{
5+
// Visual Studio does not support static_assert in compound bodies.
6+
#ifndef _MSC_VER
7+
static_assert(1, "in struct");
8+
#endif
9+
int x;
10+
} asd;
11+
12+
static_assert(1, "global scope");
13+
14+
int main()
15+
{
16+
static_assert(1, "in function");
17+
}

‎regression/cbmc/static_assert/static_assert1.desc

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

‎regression/cbmc/typeof/typeof2.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
typedef int INTTYPE;
2+
3+
int func1();
4+
5+
// C23 typeof
6+
typeof(int) v1;
7+
typeof(INTTYPE) v2;
8+
typeof(v2) v3;
9+
typeof(1 + 1) v4;
10+
typeof(1 + 1 + func1()) v5;
11+
const typeof(int) v6;
12+
typeof(int) const v7;
13+
static typeof(int) const v8;
14+
static typeof(int) const *v9;
15+
static volatile typeof(int) const *v10;
16+
17+
void func2(typeof(int) *some_arg)
18+
{
19+
}
20+
21+
int main()
22+
{
23+
}

‎regression/cbmc/typeof/typeof2.desc

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

‎src/ansi-c/ansi_c_convert_type.cpp

+42-29
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,13 @@ void ansi_c_convert_typet::read_rec(const typet &type)
7777
int32_cnt++;
7878
else if(type.id()==ID_int64)
7979
int64_cnt++;
80+
else if(type.id() == ID_c_bitint)
81+
{
82+
bitint_cnt++;
83+
const exprt &size_expr = static_cast<const exprt &>(type.find(ID_size));
84+
85+
bv_width = size_expr;
86+
}
8087
else if(type.id()==ID_gcc_float16)
8188
gcc_float16_cnt++;
8289
else if(type.id()==ID_gcc_float32)
@@ -290,15 +297,13 @@ void ansi_c_convert_typet::write(typet &type)
290297

291298
if(!other.empty())
292299
{
293-
if(double_cnt || float_cnt || signed_cnt ||
294-
unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
295-
short_cnt || char_cnt || complex_cnt || long_cnt ||
296-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
297-
gcc_float16_cnt ||
298-
gcc_float32_cnt || gcc_float32x_cnt ||
299-
gcc_float64_cnt || gcc_float64x_cnt ||
300-
gcc_float128_cnt || gcc_float128x_cnt ||
301-
gcc_int128_cnt || bv_cnt)
300+
if(
301+
double_cnt || float_cnt || signed_cnt || unsigned_cnt || int_cnt ||
302+
c_bool_cnt || proper_bool_cnt || bitint_cnt || short_cnt || char_cnt ||
303+
complex_cnt || long_cnt || int8_cnt || int16_cnt || int32_cnt ||
304+
int64_cnt || gcc_float16_cnt || gcc_float32_cnt || gcc_float32x_cnt ||
305+
gcc_float64_cnt || gcc_float64x_cnt || gcc_float128_cnt ||
306+
gcc_float128x_cnt || gcc_int128_cnt || bv_cnt)
302307
{
303308
log.error().source_location = source_location;
304309
log.error() << "illegal type modifier for defined type" << messaget::eom;
@@ -373,10 +378,10 @@ void ansi_c_convert_typet::write(typet &type)
373378
gcc_float64_cnt || gcc_float64x_cnt ||
374379
gcc_float128_cnt || gcc_float128x_cnt)
375380
{
376-
if(signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
377-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
378-
gcc_int128_cnt || bv_cnt ||
379-
short_cnt || char_cnt)
381+
if(
382+
signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
383+
bitint_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
384+
gcc_int128_cnt || bv_cnt || short_cnt || char_cnt)
380385
{
381386
log.error().source_location = source_location;
382387
log.error() << "cannot combine integer type with floating-point type"
@@ -415,10 +420,10 @@ void ansi_c_convert_typet::write(typet &type)
415420
}
416421
else if(double_cnt || float_cnt)
417422
{
418-
if(signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
419-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
420-
gcc_int128_cnt|| bv_cnt ||
421-
short_cnt || char_cnt)
423+
if(
424+
signed_cnt || unsigned_cnt || int_cnt || c_bool_cnt || proper_bool_cnt ||
425+
bitint_cnt || int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
426+
gcc_int128_cnt || bv_cnt || short_cnt || char_cnt)
422427
{
423428
log.error().source_location = source_location;
424429
log.error() << "cannot combine integer type with floating-point type"
@@ -460,10 +465,10 @@ void ansi_c_convert_typet::write(typet &type)
460465
}
461466
else if(c_bool_cnt)
462467
{
463-
if(signed_cnt || unsigned_cnt || int_cnt || short_cnt ||
464-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
465-
gcc_float128_cnt || bv_cnt || proper_bool_cnt ||
466-
char_cnt || long_cnt)
468+
if(
469+
signed_cnt || unsigned_cnt || int_cnt || short_cnt || bitint_cnt ||
470+
int8_cnt || int16_cnt || int32_cnt || int64_cnt || gcc_float128_cnt ||
471+
bv_cnt || proper_bool_cnt || char_cnt || long_cnt)
467472
{
468473
log.error().source_location = source_location;
469474
log.error() << "illegal type modifier for C boolean type"
@@ -475,10 +480,10 @@ void ansi_c_convert_typet::write(typet &type)
475480
}
476481
else if(proper_bool_cnt)
477482
{
478-
if(signed_cnt || unsigned_cnt || int_cnt || short_cnt ||
479-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
480-
gcc_float128_cnt || bv_cnt ||
481-
char_cnt || long_cnt)
483+
if(
484+
signed_cnt || unsigned_cnt || int_cnt || short_cnt || bitint_cnt ||
485+
int8_cnt || int16_cnt || int32_cnt || int64_cnt || gcc_float128_cnt ||
486+
bv_cnt || char_cnt || long_cnt)
482487
{
483488
log.error().source_location = source_location;
484489
log.error() << "illegal type modifier for proper boolean type"
@@ -496,9 +501,9 @@ void ansi_c_convert_typet::write(typet &type)
496501
}
497502
else if(char_cnt)
498503
{
499-
if(int_cnt || short_cnt || long_cnt ||
500-
int8_cnt || int16_cnt || int32_cnt || int64_cnt ||
501-
gcc_float128_cnt || bv_cnt || proper_bool_cnt)
504+
if(
505+
int_cnt || short_cnt || long_cnt || bitint_cnt || int8_cnt || int16_cnt ||
506+
int32_cnt || int64_cnt || gcc_float128_cnt || bv_cnt || proper_bool_cnt)
502507
{
503508
log.error().source_location = source_location;
504509
log.error() << "illegal type modifier for char type" << messaget::eom;
@@ -537,7 +542,9 @@ void ansi_c_convert_typet::write(typet &type)
537542

538543
if(int8_cnt || int16_cnt || int32_cnt || int64_cnt)
539544
{
540-
if(long_cnt || char_cnt || short_cnt || gcc_int128_cnt || bv_cnt)
545+
if(
546+
long_cnt || char_cnt || short_cnt || bitint_cnt || gcc_int128_cnt ||
547+
bv_cnt)
541548
{
542549
log.error().source_location = source_location;
543550
log.error() << "conflicting type modifiers" << messaget::eom;
@@ -574,6 +581,12 @@ void ansi_c_convert_typet::write(typet &type)
574581
else
575582
type=gcc_unsigned_int128_type();
576583
}
584+
else if(bitint_cnt)
585+
{
586+
// explicitly-given expression for the number of bits
587+
type.id(is_signed ? ID_c_signed_bitint : ID_c_unsigned_bitint);
588+
type.set(ID_width, bv_width);
589+
}
577590
else if(bv_cnt)
578591
{
579592
// explicitly-given expression for width

‎src/ansi-c/ansi_c_convert_type.h

+3-4
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,8 @@ class message_handlert;
2424
class ansi_c_convert_typet
2525
{
2626
public:
27-
unsigned unsigned_cnt, signed_cnt, char_cnt,
28-
int_cnt, short_cnt, long_cnt,
29-
double_cnt, float_cnt, c_bool_cnt,
30-
proper_bool_cnt, complex_cnt;
27+
unsigned unsigned_cnt, signed_cnt, char_cnt, int_cnt, short_cnt, long_cnt,
28+
double_cnt, float_cnt, c_bool_cnt, proper_bool_cnt, complex_cnt, bitint_cnt;
3129

3230
// extensions
3331
unsigned int8_cnt, int16_cnt, int32_cnt, int64_cnt,
@@ -87,6 +85,7 @@ class ansi_c_convert_typet
8785
c_bool_cnt(0),
8886
proper_bool_cnt(0),
8987
complex_cnt(0),
88+
bitint_cnt(0),
9089
int8_cnt(0),
9190
int16_cnt(0),
9291
int32_cnt(0),

‎src/ansi-c/ansi_c_language.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,11 @@ bool ansi_c_languaget::parse(
8080
ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
8181
ansi_c_parser.cpp98=false; // it's not C++
8282
ansi_c_parser.cpp11=false; // it's not C++
83+
ansi_c_parser.c17 =
84+
config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C17 ||
85+
config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C23;
86+
ansi_c_parser.c23 =
87+
config.ansi_c.c_standard == configt::ansi_ct::c_standardt::C23;
8388
ansi_c_parser.mode=config.ansi_c.mode;
8489

8590
ansi_c_scanner_init(ansi_c_parser);

‎src/ansi-c/builtin_factory.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,8 @@ static bool convert(
5858
ansi_c_parser.fp16_type = config.ansi_c.fp16_type;
5959
ansi_c_parser.cpp98=false; // it's not C++
6060
ansi_c_parser.cpp11=false; // it's not C++
61+
ansi_c_parser.c17 = false; // we do C11 for now
62+
ansi_c_parser.c23 = false; // we do C11 for now
6163
ansi_c_parser.mode=config.ansi_c.mode;
6264

6365
ansi_c_scanner_init(ansi_c_parser);

‎src/ansi-c/c_preprocess.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -602,10 +602,10 @@ bool c_preprocess_gcc_clang(
602602
case configt::ansi_ct::c_standardt::C23:
603603
#if defined(__OpenBSD__)
604604
if(preprocessor == configt::ansi_ct::preprocessort::CLANG)
605-
argv.push_back("-std=c23");
605+
argv.push_back("-std=c2x");
606606
else
607607
#endif
608-
argv.push_back("-std=gnu23");
608+
argv.push_back("-std=gnu2x");
609609
break;
610610
}
611611
}

‎src/ansi-c/c_typecast.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -799,7 +799,7 @@ c_typecastt::check_address_can_be_taken(const typet &type)
799799
if(width % config.ansi_c.char_width != 0)
800800
{
801801
return std::string(
802-
"bitvector must have width that is a multiple of CHAR_BIT");
802+
"bitvector must have width that is a multiple of CHAR_BIT"+std::to_string(width));
803803
}
804804
else
805805
return {};

‎src/ansi-c/c_typecheck_base.h

+1
Original file line numberDiff line numberDiff line change
@@ -265,6 +265,7 @@ class c_typecheck_baset:
265265
virtual void typecheck_array_type(array_typet &type);
266266
virtual void typecheck_vector_type(typet &type);
267267
virtual void typecheck_custom_type(typet &type);
268+
virtual void typecheck_bitint_type(typet &);
268269
virtual void adjust_function_parameter(typet &type) const;
269270
virtual bool is_complete_type(const typet &type) const;
270271

‎src/ansi-c/c_typecheck_type.cpp

+57-1
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,7 @@ void c_typecheck_baset::typecheck_type(typet &type)
9494
typecheck_c_enum_tag_type(to_c_enum_tag_type(type));
9595
else if(type.id()==ID_c_bit_field)
9696
typecheck_c_bit_field_type(to_c_bit_field_type(type));
97-
else if(type.id()==ID_typeof)
97+
else if(type.id() == ID_typeof || type.id() == ID_c_typeof_unqual)
9898
typecheck_typeof_type(type);
9999
else if(type.id() == ID_typedef_type)
100100
typecheck_typedef_type(type);
@@ -116,6 +116,10 @@ void c_typecheck_baset::typecheck_type(typet &type)
116116
type.id()==ID_custom_floatbv ||
117117
type.id()==ID_custom_fixedbv)
118118
typecheck_custom_type(type);
119+
else if(type.id() == ID_c_signed_bitint || type.id() == ID_c_unsigned_bitint)
120+
{
121+
typecheck_bitint_type(type);
122+
}
119123
else if(type.id()==ID_gcc_attribute_mode)
120124
{
121125
// get that mode
@@ -417,6 +421,58 @@ void c_typecheck_baset::typecheck_custom_type(typet &type)
417421
UNREACHABLE;
418422
}
419423

424+
void c_typecheck_baset::typecheck_bitint_type(typet &type)
425+
{
426+
// they all have a width
427+
exprt size_expr = static_cast<const exprt &>(type.find(ID_width));
428+
429+
typecheck_expr(size_expr);
430+
source_locationt source_location = size_expr.source_location();
431+
make_constant_index(size_expr);
432+
433+
mp_integer size_int;
434+
if(to_integer(to_constant_expr(size_expr), size_int))
435+
{
436+
throw errort().with_location(source_location)
437+
<< "failed to convert _BitInt width to constant";
438+
}
439+
440+
bool is_signed = type.id() == ID_c_signed_bitint;
441+
442+
// Must have at least one bit if unsigned, and at least two if signed
443+
if(!is_signed)
444+
{
445+
if(size_int < 1)
446+
{
447+
throw errort().with_location(source_location)
448+
<< "unsigned _BitInt must have at least one bit";
449+
}
450+
}
451+
else
452+
{
453+
if(size_int < 2)
454+
{
455+
throw errort().with_location(source_location)
456+
<< "signed _BitInt must have at least two bits";
457+
}
458+
}
459+
460+
// These get padded up, much like _Bool
461+
auto bytes = (size_int % 8) == 0 ? size_int / 8 : size_int / 8 + 1;
462+
463+
auto bytes_padded = power(2, address_bits(bytes));
464+
465+
auto width = 8 * bytes_padded;
466+
467+
type.set(ID_width, integer2string(width));
468+
type.set(ID_C_c_type, type.id());
469+
type.id(is_signed ? ID_signedbv : ID_unsignedbv);
470+
471+
// We remember the original number of bits before padding,
472+
// since these determine semantics
473+
type.set(ID_C_bitint_bits, integer2string(size_int));
474+
}
475+
420476
void c_typecheck_baset::typecheck_code_type(code_typet &type)
421477
{
422478
// the return type is still 'subtype()'

0 commit comments

Comments
 (0)