Repository navigation
[Individual PRs to follow] C++ standard support: C++11 through C++26 parser, type-checker, and STL improvements - #8878
Draft
tautschnig wants to merge 3257 commits into
Draft
tautschnig wants to merge 3257 commits into
tautschnig wants to merge 3257 commits into
Conversation
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
10 times, most recently
from
March 18, 2026 22:35
ab675bb to
4f0b085
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8878 +/- ##
===========================================
+ Coverage 80.90% 82.55% +1.64%
===========================================
Files 1718 1733 +15
Lines 190266 233014 +42748
Branches 73 82 +9
===========================================
+ Hits 153936 192355 +38419
- Misses 36330 40659 +4329 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
10 times, most recently
from
March 31, 2026 08:28
8f4e2d7 to
f3d208e
Compare
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
6 times, most recently
from
April 3, 2026 23:29
5cc8d28 to
980d519
Compare
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
2 times, most recently
from
April 28, 2026 09:27
6347e6c to
b5975fe
Compare
N5008 [temp.inst]/5: a constexpr member function of a class template specialization is instantiated when a constant expression needs its value. The inline members of a class template instance wait in deferred_typechecking until used, and a call from a constant expression was then not evaluated: the initializer `static constexpr type value = _S_make_table();' of libstdc++'s __from_chars_alnum_to_val_table<false> ran at run time, where --unwind 10 cut its loops and made the end of main in cpp17_from_chars_unsigned unreachable. Such a member is now queued with its class's template map and converted on the spot, as other deferred bodies are. With the previous commit, the table is constant-initialized, and cpp17_from_chars_unsigned is back at --unwind 10. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
A test whose bounds (--unwind, --depth) cut every path to the end of main, or whose paths all end in a failed assumption, passes whatever it asserts. A manual check found ten such tests in cbmc-cpp in round 198, one of which hid a front-end bug (the initializer_list backing array). scripts/check_vacuity.py adds an assert(0) before the last return of main in a copy of each CORE test that expects VERIFICATION SUCCESSFUL, runs cbmc with the test's options, and fails if that assertion holds (or gives no result). The new tag `no-vacuity-check' exempts a test whose main legitimately does not end (catch_reference returns inside a try block). check-ubuntu-24_04-cmake-gcc runs it over cbmc-cpp and systemc: 1124 tests reach the end of main, in 123 s with 4 jobs and CI's memory limit. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [expr.comma]/1: the left operand of a comma is a discarded-value
expression, and the type and value of the result are those of the right
operand. In a constant expression the front end kept the comma, so the
value of `static constexpr type value = (_DecOnly, _S_make_table());'
(libstdc++'s __from_chars_alnum_to_val_table) was `FALSE, {...}' rather
than the table, and its elements were not constants: an array bound or a
template argument read from them was a conversion error. In a constant
expression a left operand that simplifies to a constant has no effect;
the comma is now its right operand.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
With libstdc++'s __from_chars_alnum_to_val_table constant-initialized (f64a0c38e4), the end of the proof's main is reachable for the first time: previously --unwind 8 cut the table's run-time construction, and the proof passed in 5 s without verifying anything (156 symex steps). Verified, it takes 11037 steps, about 10 GB and 270 s, and all its assertions hold; that exceeds the CI memory limit (2.5 GB). The old build needed more than 12 GB for the same task with --unwind 257. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Tests that expect only `^EXIT=0$' or accept either verdict (`^EXIT=(0|10)$') escaped the first vacuity check. With bounds that cut every path to the end of main they passed whatever they asserted: - --unwind too low: cpp11_algorithm_verify, cpp11_string_verify (2 -> 6), cpp20_algorithm_basic (3 -> 6); - --depth: cpp11_memory_verify, cpp11_vector_probe_libcxx, cpp17_algorithm_basic, cpp17_shared_ptr, cpp20_algorithm_basic. Each now reaches the end of main and verifies in under 7 s, so it expects VERIFICATION SUCCESSFUL. On VS 2026, cpp11_algorithm_verify and cpp17_algorithm_basic needed develop's fix of the pointer-difference overflow check (diffblue#9229) to do so. Four iostream tests are conversion checks that accept either verdict and stay so, tagged no-vacuity-check with the reason: once the end of main is reachable, cpp11_iostream_cerr, its libc++ variant and cpp11_libcxx20_endl take more than 300 s, and cpp11_libcxx20_iostream reports dereference failures in libc++'s stream code (not yet investigated). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
A CORE test that expects `^EXIT=0$' requires success as much as one that expects `^VERIFICATION SUCCESSFUL$'; it is now checked too, unless its options only display the program (--show-*, --dump-c, ...). With the previous commit, 1141 tests of cbmc-cpp and systemc reach the end of main. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
from
October 23, 2026 07:06
25e5ae0 to
becbcc3
Compare
test-32.desc runs the test with --32, and <stdlib.h> then needs 32-bit
headers: the Ubuntu CI runners have none ("bits/libc-header-start.h: No
such file or directory"), and with Visual Studio the 64-bit size_t of
corecrt_malloc.h conflicts with the 32-bit one of CBMC's malloc model.
Both failed in CI run 39915638865. The test now declares malloc itself;
the previous binary still runs out of memory on it with --32.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
d0b8075c8b rewrote every comma with a constant left operand to its right operand while type-checking in a constant-expression context. The parser also represents the argument list of `(f)(a, b)' as a comma expression, and that was type-checked first: `(::std:: max)(alignof(_Ty), 16ull)' in the MSVC STL's _New_alignof became a call with one argument, and _Get_size_of_n and _Allocate were "not found", dropping allocator<T>'s allocate and deallocate. Seen in cpp11_nested_braces_user_ctor_class and cpp11_rvalue_reference_from_converting_constructor with this round's VS 2022 artifact (CI run 39915638865). The rewrite ([expr.comma]/1) now applies to the finished value of a constant-initialized variable or static data member. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
f1888b1 made test_format CORE again after checking it with libstdc++ 13; with the libstdc++ 16 headers (16-20260315, the check-ubuntu-24_04-cmake- gcc-16-cbmc-cpp job of CI run 39937905540) four functions of <format> lose their bodies, with every saved front-end build back to W170: _Seq_sink's _M_reserve and _M_span, __should_escape_ascii and __write_escaped_char. Tag it broken-libstdcxx16, as test_format_typecheck already is, and record the cause in both descs (the old note of test_format_typecheck named a KNOWNBUG that has since been fixed). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The THOROUGH job of CI run 39937905540 runs it under the 2.5 GB limit, and the SAT solver ran out of memory: verified, the proof needs about 10 GB. As for edit_distance, a proof blocked by a scaling limit is a KNOWNBUG. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
8917a213fa records which branch of a conditional ran when a branch has temporaries, so that their destructors run only on the path that created them. It did so for every temporary, also the return value of a C function call: in aws-c-common's ensure_byte_buf_has_allocated_buffer_member each `?:' got a flag, a branch and a DEAD, 14 more symex steps, and the Performance Benchmarking job of CI run 39986460423 reported a solver-time regression for aws_byte_buf_append_dynamic (14.4 s -> 23.1 s). Destroying a temporary without a destructor is only its DEAD, harmless on a path that did not create it, so the flag is now made only if some temporary has a destructor; the goto program of that proof is again the same as develop's. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The type-trait and type-transformation builtins (__is_function(T),
__add_rvalue_reference(T), __remove_cv(T), __builtin_popcountg, ...) are
keywords when followed by `(' if the preprocessor is gcc or clang. On
Windows the default preprocessor is cl (VISUAL_STUDIO), and they were
identifiers there: `static_assert(__is_function(void()), ...)' was a parse
error, and 12 cbmc-cpp tests failed on both Windows CI jobs only. The MSVC
STL uses these reserved names only as builtins, too, so they are keywords
for cl as well.
Found by emulating a Windows host on Linux (the VISUAL_STUDIO preprocessor
setting for --winx64) with this run's artifacts: the 12 tests failed there
as in CI run 39986460423, and pass with this change.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [cpp.predefined]/1: __cplusplus identifies the standard. cl defines it as 199711L for every standard unless given /Zc:__cplusplus, so `#if __cplusplus >= 201103L' sections disappeared with --cpp11 on Windows: cpp98_explicit_instantiation_of_member_function_template/test_cpp11 lost its second assertion on both Windows CI jobs (run 39986460423). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Four tests assume a 64-bit long (sizeof(long) >= sizeof(int) is strict, a long member holds 4000000000, a partial specialization for N = 8) and ran with --64, which is LP64 on Linux but LLP64 on a Windows host; on both Windows CI jobs of run 39986460423 they failed as they should in LLP64. They now say --LP64. cpp11_virtual_override_with_rvalue_reference_parameter marks a system header with a GNU line marker (`# 1 "..." 1 3'), which cl rejects (error C2019); it is tagged gnu-extensions, excluded with MSVC. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
To be reverted. CBMC_DUMP_PREPROCESSED_DIR makes c_preprocess save the input and output of each preprocessed text (the C library models) to that directory; scripts/windows_debug.ps1 collects, for the tests that fail on Windows only, the cl-preprocessed source, a verbose run with a trace, the goto functions, the symbol table and the preprocessed library models, plus small probes of the memcpy and fgetc models. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…script To be reverted. All other jobs and workflows are disabled with `if: false' (release workflows untouched); check-vs-2026-cmake-build-and-test runs the cbmc-cpp CORE tests only, then scripts/windows_debug.ps1, and uploads its output as the windows-debug artifact. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…s runtime C17 7.24.1/2 makes memcpy(d, NULL, 0) undefined, and CBMC's model checks that the source is readable. The Microsoft runtime accepts a null pointer with a zero length, as C2y does (N3322), and the MSVC STL relies on it: copying an empty std::vector calls memcpy(dest, nullptr, 0) in _Impl_copy_memmeow_tail. 14 cbmc-cpp tests reported "memcpy source region readable: FAILURE" on the Windows CI jobs (run 40122294553; the trace of cpp11_vector_probe shows _First_ch = NULL, _Byte_count = 0). When cl preprocesses the library (_MSC_VER), the models of memcpy and memmove now allow it, as the __builtin_ variants already do. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
206978d passes /Zc:__cplusplus for every standard; cl has no C++98 or C++03 mode, and with the option __cplusplus became its default 201402L, so the --cpp98 variant of cpp98_explicit_instantiation_of_member_function_ template saw its C++11 section on the Windows CI job of run 40122294553. Without the option cl's 199711L is the right value for those standards. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [dcl.attr.grammar]/1: an attribute-specifier-seq is a sequence of attribute-specifiers, of which an alignment-specifier is one kind, and [dcl.align]/4: the strictest alignment specified applies. The parser read a single alignas, so `alignas(_Loop_vals_v3_t<...>) alignas(...) alignas(...) unsigned char _Stackbuf[4096];' in VS 2026's <regex> was a parse error (Windows CI run 40122294553). Consecutive alignment-specifiers are now read, and their alignment is the largest. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
To be reverted. The invariant "fgetc type inconsistency" on Windows only names the two types' ids (both `code'); the full types show which part differs. windows_debug.ps1 now runs the affected test with --validate-goto-model, keeps cl's file-name message out of the saved preprocessed source, and drops the tests that are fixed. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [basic.def.odr]/15: an inline function defined in a header that
several translation units include has one definition. When a C++ and a C
translation unit include it, the two front ends name the members of the
header's structs differently (`_iobuf::_Placeholder' in C++, `_Placeholder'
in C), so the linker saw different parameter types and reported
"conflicting function declarations". The Windows SDK's stdio.h defines
_fprintf_s_l and similar functions inline, and the C library models are C
preprocessed by cl: linking fgetc, fwrite, fread, fflush and fclose from
the library failed for C++ programs using <fstream> on Windows, leaving
calls with the old type ("fgetc type inconsistency" with
--validate-goto-model, CI run 40167313768; reproduced on Linux by replaying
the library preprocessed on Windows). Two definitions from the same file
and line whose types differ that way are now one, as other parameter type
differences between a declaration and a definition already are.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
With the MSVC STL, std::ofstream from a string exhausts the SAT solver's memory: the three tests with that shape ran out of memory on the VS 2026 CI job of run 40172972722, once the linking failure before them was fixed. The KNOWNBUG cpp11_ofstream_from_string_msvc_stl tracks this (not yet reduced). Restore the broken-msvc-stl tag (5469a8f removed it with its last user), excluded with MSVC, and tag the three tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…onsistency" This reverts commit cca3cfd.
…bugging script" This reverts commit 455da85.
… failures" This reverts commit 1647625.
98c047f put the two variants of the preconditions under #ifdef _MSC_VER, which clang-format then indented as function-level code after memmove. A macro defined under the #ifdef now selects the condition, the preconditions keep a single form, and the whole of memmove is formatted. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This branch contains comprehensive improvements to CBMC's C++ front-end, covering parser, type-checker, template instantiation, GOTO conversion, and standard library model support for C++11 through C++26.
Summary of changes:
This branch will be split into smaller PRs for review. See CPP_SUPPORT_STATUS.md for a detailed feature matrix.