C23 keywords #8623

kroening · 2025-04-09T17:16:31Z

This adds scanner, parser and typechecker support for the new C23 keywords.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2025-04-09T17:37:41Z

Asking here so as not to delay #8621 any further:

In loc(); return conditional_keyword(...); the use of loc(); is unnecessary, we should clean that up.
In make_identifier and also MSC_cpp_keyword we have if(PARSER.cpp98 ... - which seems insufficient as it would not cover the case of PARSER.cpp11 being set instead.

tautschnig · 2025-04-09T17:41:24Z

Also, while working on this piece of code we might fix #8308?

kroening · 2025-04-09T18:09:38Z

Also, while working on this piece of code we might fix #8308?

#8624

kroening · 2025-04-09T18:12:28Z

In loc(); return conditional_keyword(...); the use of loc(); is unnecessary, we should clean that up.

Yes, some tokens come with an IREP and some don't -- and it's prone to error to keep that in sync. I am minded to give an IREP to all identifier-like tokens to remove that ambiguity.

In make_identifier and also MSC_cpp_keyword we have if(PARSER.cpp98 ... - which seems insufficient as it would not cover the case of PARSER.cpp11 being set instead.

For clarity, could be renamed to cpp98_or_above, but more verbose, or could write cpp98 || cpp11 || ....

tautschnig · 2025-04-09T18:35:35Z

In loc(); return conditional_keyword(...); the use of loc(); is unnecessary, we should clean that up.

Yes, some tokens come with an IREP and some don't -- and it's prone to error to keep that in sync. I am minded to give an IREP to all identifier-like tokens to remove that ambiguity.

Yes, but not what I was after: conditional_keyword invokes loc() on the if branch, or else make_identifier, which in turn invokes loc() right away. So doing loc(); return conditional_keyword(...) makes that first loc(); call redundant.

kroening · 2025-04-09T21:13:57Z

Yes, but not what I was after: conditional_keyword invokes loc() on the if branch, or else make_identifier, which in turn invokes loc() right away. So doing loc(); return conditional_keyword(...) makes that first loc(); call redundant.

#8626

codecov · 2025-04-09T23:09:49Z

Codecov Report

Attention: Patch coverage is 78.06452% with 34 lines in your changes missing coverage. Please review.

Project coverage is 80.37%. Comparing base (0b000a3) to head (b1808c3).
Report is 2 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/ansi-c/expr2c.cpp	40.00%	12 Missing ⚠️
src/ansi-c/scanner.l	70.83%	7 Missing ⚠️
src/ansi-c/c_typecheck_type.cpp	78.57%	6 Missing ⚠️
src/ansi-c/parser.y	76.92%	6 Missing ⚠️
src/ansi-c/gcc_version.cpp	50.00%	2 Missing ⚠️
src/util/config.cpp	75.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8623      +/-   ##
===========================================
- Coverage    80.38%   80.37%   -0.02%     
===========================================
  Files         1686     1686              
  Lines       206764   206872     +108     
  Branches        75       73       -2     
===========================================
+ Hits        166207   166268      +61     
- Misses       40557    40604      +47

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

regression/cbmc/_BitInt/_BitInt1.c

regression/cbmc/constants/predefined-constants1.c

tautschnig · 2025-04-10T10:46:25Z

regression/cbmc/static_assert/static_assert1.c

+// C23 introduces the "static_assert" keyword.
+
+struct S
+{
+  // Visual Studio does not support static_assert in compound bodies.
+#ifndef _MSC_VER
+  static_assert(1, "in struct");
+#endif
+  int x;
+} asd;
+
+static_assert(1, "global scope");
+
+int main()
+{
+  static_assert(1, "in function");
+}


Shouldn't this go in the ansi-c regression test folder instead of cbmc?

Yes, that was my first attempt. But we run various compilers over that folder, and they don't do C23.

tautschnig · 2025-04-10T10:47:03Z

regression/cbmc/typeof/typeof2.c

+typedef int INTTYPE;
+
+int func1();
+
+// C23 typeof
+typeof(int) v1;
+typeof(INTTYPE) v2;
+typeof(v2) v3;
+typeof(1 + 1) v4;
+typeof(1 + 1 + func1()) v5;
+const typeof(int) v6;
+typeof(int) const v7;
+static typeof(int) const v8;
+static typeof(int) const *v9;
+static volatile typeof(int) const *v10;
+
+void func2(typeof(int) *some_arg)
+{
+}
+
+int main()
+{
+}


Should probably go in ansi-c?

tautschnig · 2025-04-10T10:51:12Z

src/ansi-c/expr2c.cpp

+      return integer2string(binary2integer(binary, false));
+    }
+    else
+      return convert_norep(src, precedence);


I think previously this would handle __CPROVER_bitvector in some way?

Those map to signedbv/unsignedv.

doc/man/cbmc.1

This adds scanner, parser and typechecker support for the new C23 keywords.

tautschnig · 2025-04-10T22:17:47Z

src/ansi-c/goto-conversion/goto_convert.cpp

    exprt assertion =
      typecast_exprt::conditional_cast(code.op0(), bool_typet());
    simplify(assertion, ns);
    INVARIANT_WITH_DIAGNOSTICS(
      !assertion.is_false(),
-      "static assertion " + id2string(get_string_constant(code.op1())),
+      "static assertion is false",


Hmm, shouldn't we keep the message when there is one?

This should never be executed, and is presumably dead code.

kroening added enhancement C Front End labels Apr 9, 2025

kroening requested review from tautschnig, peterschrammel and remi-delmas-3000 as code owners April 9, 2025 17:16

kroening force-pushed the c23-2 branch 2 times, most recently from cbba9f8 to b949d48 Compare April 9, 2025 17:25

kroening force-pushed the c23-2 branch from b949d48 to c8613ad Compare April 9, 2025 18:05

kroening force-pushed the c23-2 branch 2 times, most recently from 67cd3f5 to 1de6619 Compare April 9, 2025 18:27

kroening force-pushed the c23-2 branch 3 times, most recently from 54026f1 to 7c8b661 Compare April 9, 2025 22:20

kroening force-pushed the c23-2 branch 4 times, most recently from ddec5f3 to a556e81 Compare April 10, 2025 01:51

tautschnig reviewed Apr 10, 2025

View reviewed changes

regression/cbmc/_BitInt/_BitInt1.c Outdated Show resolved Hide resolved

tautschnig reviewed Apr 10, 2025

View reviewed changes

kroening force-pushed the c23-2 branch 4 times, most recently from 45c3fe6 to 5a39bdd Compare April 10, 2025 14:22

kroening requested review from jimgrundy and TGWDB as code owners April 10, 2025 14:22

kroening force-pushed the c23-2 branch 2 times, most recently from 669e233 to 0c3d48c Compare April 10, 2025 14:43

tautschnig reviewed Apr 10, 2025

View reviewed changes

doc/man/cbmc.1 Show resolved Hide resolved

kroening force-pushed the c23-2 branch 4 times, most recently from 6ee8f9d to d070209 Compare April 10, 2025 18:44

C23 keywords

b1808c3

This adds scanner, parser and typechecker support for the new C23 keywords.

kroening force-pushed the c23-2 branch from d070209 to b1808c3 Compare April 10, 2025 19:32

tautschnig approved these changes Apr 10, 2025

View reviewed changes

kroening merged commit 5dc709d into develop Apr 11, 2025
39 of 41 checks passed

kroening deleted the c23-2 branch April 11, 2025 14:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

C23 keywords #8623

C23 keywords #8623

kroening commented Apr 9, 2025

tautschnig commented Apr 9, 2025

tautschnig commented Apr 9, 2025

kroening commented Apr 9, 2025

kroening commented Apr 9, 2025

tautschnig commented Apr 9, 2025

kroening commented Apr 9, 2025

codecov bot commented Apr 9, 2025 •

edited

Loading

tautschnig Apr 10, 2025

kroening Apr 10, 2025

tautschnig Apr 10, 2025

tautschnig Apr 10, 2025

kroening Apr 10, 2025

tautschnig Apr 10, 2025

kroening Apr 10, 2025

C23 keywords #8623

C23 keywords #8623

Conversation

kroening commented Apr 9, 2025

tautschnig commented Apr 9, 2025

tautschnig commented Apr 9, 2025

kroening commented Apr 9, 2025

kroening commented Apr 9, 2025

tautschnig commented Apr 9, 2025

kroening commented Apr 9, 2025

codecov bot commented Apr 9, 2025 • edited Loading

Codecov Report

tautschnig Apr 10, 2025

Choose a reason for hiding this comment

kroening Apr 10, 2025

Choose a reason for hiding this comment

tautschnig Apr 10, 2025

Choose a reason for hiding this comment

tautschnig Apr 10, 2025

Choose a reason for hiding this comment

kroening Apr 10, 2025

Choose a reason for hiding this comment

tautschnig Apr 10, 2025

Choose a reason for hiding this comment

kroening Apr 10, 2025

Choose a reason for hiding this comment

codecov bot commented Apr 9, 2025 •

edited

Loading