Skip to content

Commit c8613ad

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

19 files changed

+226
-71
lines changed

‎regression/ansi-c/_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/ansi-c/_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/ansi-c/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/ansi-c/constants/predefined-constants1.desc

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

‎regression/ansi-c/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/ansi-c/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+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$

‎regression/ansi-c/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/ansi-c/typeof/typeof2.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
typeof2.c
3+
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 width
587+
type.id(is_signed ? ID_custom_signedbv : ID_custom_unsignedbv);
588+
type.set(ID_size, 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_typecheck_type.cpp

+1-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_typeof_unqual)
9898
typecheck_typeof_type(type);
9999
else if(type.id() == ID_typedef_type)
100100
typecheck_typedef_type(type);

‎src/ansi-c/parser.y

+39-2
Original file line numberDiff line numberDiff line change
@@ -62,8 +62,9 @@ int yyansi_cerror(const std::string &error);
6262

6363
%token TOK_AUTO "auto"
6464
%token TOK_BOOL "bool"
65-
%token TOK_COMPLEX "complex"
65+
%token TOK_BITINT "_BitInt"
6666
%token TOK_BREAK "break"
67+
%token TOK_COMPLEX "complex"
6768
%token TOK_CASE "case"
6869
%token TOK_CHAR "char"
6970
%token TOK_CONST "const"
@@ -91,6 +92,7 @@ int yyansi_cerror(const std::string &error);
9192
%token TOK_STRUCT "struct"
9293
%token TOK_SWITCH "switch"
9394
%token TOK_TYPEDEF "typedef"
95+
%token TOK_TYPEOF_UNQUAL "typeof_unqual"
9496
%token TOK_UNION "union"
9597
%token TOK_UNSIGNED "unsigned"
9698
%token TOK_VOID "void"
@@ -344,10 +346,30 @@ string:
344346

345347
/*** Constants **********************************************************/
346348

347-
constant: integer
349+
constant:
350+
integer
348351
| floating
349352
| character
350353
| string
354+
| predefined-constant
355+
;
356+
357+
predefined-constant:
358+
TOK_FALSE
359+
{ init($$, ID_constant);
360+
stack_expr($$).set(ID_value, ID_false);
361+
stack_expr($$).type() = bool_typet{};
362+
}
363+
| TOK_TRUE
364+
{ init($$, ID_constant);
365+
stack_expr($$).set(ID_value, ID_true);
366+
stack_expr($$).type() = bool_typet{};
367+
}
368+
| TOK_NULLPTR
369+
{ init($$, ID_constant);
370+
stack_expr($$).set(ID_value, ID_NULL);
371+
stack_expr($$).type() = pointer_type(void_type());
372+
}
351373
;
352374

353375
/*** Expressions ********************************************************/
@@ -1338,6 +1360,16 @@ typeof_specifier:
13381360
parser_stack($$).id(ID_typeof);
13391361
parser_stack($$).set(ID_type_arg, parser_stack($3));
13401362
}
1363+
| TOK_TYPEOF_UNQUAL '(' comma_expression ')'
1364+
{ $$ = $1;
1365+
parser_stack($$).id(ID_typeof_unqual);
1366+
mto($$, $3);
1367+
}
1368+
| TOK_TYPEOF_UNQUAL '(' type_name ')'
1369+
{ $$ = $1;
1370+
parser_stack($$).id(ID_typeof_unqual);
1371+
parser_stack($$).set(ID_type_arg, parser_stack($3));
1372+
}
13411373
;
13421374

13431375
typeof_type_specifier:
@@ -1517,6 +1549,11 @@ basic_type_name:
15171549
| TOK_DOUBLE { $$=$1; set($$, ID_double); }
15181550
| TOK_SIGNED { $$=$1; set($$, ID_signed); }
15191551
| TOK_UNSIGNED { $$=$1; set($$, ID_unsigned); }
1552+
| TOK_BITINT '(' constant_expression ')'
1553+
{
1554+
init($$, ID_c_bitint);
1555+
parser_stack($$).add(ID_size).swap(parser_stack($3));
1556+
}
15201557
| TOK_VOID { $$=$1; set($$, ID_void); }
15211558
| TOK_BOOL { $$=$1; set($$, ID_c_bool); }
15221559
| TOK_COMPLEX { $$=$1; set($$, ID_complex); }

0 commit comments

Comments
 (0)