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 3486 commits into
Draft
tautschnig wants to merge 3486 commits into
tautschnig wants to merge 3486 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 81.02% 82.85% +1.83%
===========================================
Files 1723 1739 +16
Lines 191314 237625 +46311
Branches 73 84 +11
===========================================
+ Hits 155020 196895 +41875
- Misses 36294 40730 +4436 ☔ 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
libstdc++ 16's vprint_nonunicode(FILE *, ...), behind std::print,
formats directly into the FILE's buffer through glibc's FILE internals
(_IO_write_ptr, __overflow, __fbufsize), which CBMC's FILE does not
model; symbolic execution of `std::print("{}", 42)' did not end. N5008
[print.fun]/16 requires the formatted characters to be written to the
stream while holding its lock (not observable in a single thread): the
function is now modelled as libstdc++'s vprint_nonunicode_buffered,
formatting into a string and writing it with fwrite, which throws
system_error when the write fails (/17).
That path needs std::__throw_system_error, generic_category() and
system_category() ([syserr.errcat.objects]/1-2) and ~system_error, all
in libstdc++'s compiled library; they are modelled (with empty message
strings). A replacing model that does not type-check (another library
version's internals) now leaves the header's own body instead of none.
cpp23_probe_std_print (libstdcxx16) is CORE, about 60 s; new test
cpp11_system_error_generic_category.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
develop's syntax check now uses clang-format 18.1.8 (e9d90c3), which formats some of this branch's lines differently from clang-format 15: mostly the indentation in Parser::optAttribute and the line breaks of compound requirements and requires-expressions in the regression tests. In C++17 mode (.clang-format) clang-format 18 splits `<=>' into `<= >', which no longer compiles; the eight tests that declare an operator<=> keep it under clang-format off/on, as cpp20_concept_iterator_chain already does. cpp17_trailing_decltype_pack_redecl's desc matched a line number that the reformatting moved. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
develop's documentation check now expects doxygen 1.15.0 (0b3d3e7), which reads a backtick as the start of a code span: the `x' quoting of this branch's doc comments left spans open across whole comment blocks (245 warnings). The quotes are now `x`, as in develop's own fix (06742fb), and a few spans doxygen 1.15 still misreads (`.*`, `->`, a `#' link) are plain text. Comments only. 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
November 6, 2026 16:45
1c6fc19 to
58f2922
Compare
`--dump-c-library-models DIR' wrote each model to DIR/FUNCTION.i. The
Java models' names (`java::java.io.InputStream.read:()I') contain colons,
which the macOS CI job's upload of the preprocessed models as an artifact
rejects ("The path for one of the files in artifact is not valid ...
Colon :"), and which Windows file systems do not allow. A character
other than a letter, digit, `_', `-' or `.' is now written as `%XX' (its
hexadecimal code), when dumping and when loading with
`--c-library-models'.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…__int128 Visual Studio has no `unsigned __int128': the test was a parse error in CI's check-vs-2022-make-build-and-test. The last of the six alternatives is now `long double', which every target has; the test still fails on the binary from before the fix it guards. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
chain.sh dumped the models into models.dir in each test's directory and kept it, which the Linux CI jobs' check for a clean tree after the tests reports (check-ubuntu-24_04-cmake-gcc: "Ignored files: ... models.dir/"). The directory is now removed when the script exits. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
`reinterpret_cast<const int *>(p)' with p of type `const unsigned char (*)[8]' was rejected as casting away constness: cast_away_constness compares the two pointer chains level by level ([expr.const.cast]/6) and compared the array level with `const int'. N5008 [basic.type.qualifier]/3 puts an array's cv-qualification on its elements; an array level whose counterpart is not an array is now compared through its element type. The GCC 16 snapshot of CI's toolchain PPA reads std::any's in-place buffer this way (`reinterpret_cast<const _Tp *>(&__any->_M_storage._M_buffer)'), so _S_manage lost its body and cpp17_probe_std_any failed in check-ubuntu-24_04-cmake-gcc-16-cbmc-cpp. New test cpp11_reinterpret_cast_from_pointer_to_const_array. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
CI's GCC 16 (the toolchain PPA's snapshot 20260315) still has N5008's add_sat and saturate_cast (__cpp_lib_saturation_arithmetic 202311L); the renamed saturating_add and saturating_cast came later (202603L, GCC 16.2). The test uses whichever the library provides. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
doxygen 1.15 read `%XX` in the comment of model_file_name as the start of an unterminated <tt> (check-doxygen: "end of comment block while expecting command </tt>"). The encoding is described in words instead. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
libstdc++ declares std::__throw_bad_alloc, __throw_length_error and the other helpers of functexcept.cc __attribute__((__noreturn__)) and defines them in its compiled library. CBMC took a call of such a body-less function to return. libstdc++ 16.2's __new_allocator::allocate is `if(n > max_size()) __throw_bad_alloc(); else return ...;': the path on which the helper "returned" fell off the end of allocate with an arbitrary pointer, and with GCC 16.2's headers cpp11_ostream_integer_formatting did not finish in 900 s (24 s now, as with CI's earlier GCC 16 snapshot). Each helper is now modelled as the throw of its exception (the format of out_of_range_fmt is not applied). New test cpp11_libstdcxx_throw_helpers_do_not_return (gcc-only: GCC attribute syntax). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
In C++17 mode clang-format splits `<=>' into `<= >' (which does not compile) and does not know requires-clauses and compound requirements. CI checks only the lines a pull request changes (git-clang-format), so existing code is not reformatted. This branch's tests that declare an operator<=> no longer need clang-format off/on, and its tests with requires-clauses and compound requirements are formatted as clang-format 18.1.8 does in C++20 mode (124 files, regression/cbmc-cpp only; src is unaffected). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The postconditions of functions returning a class or a reference were
not checked (a warning). The front end checked postconditions by
rewriting each `return e;' to hold e in a variable, which would copy a
class result -- an extra copy or move constructor call and destructor
call, not allowed for `return T{x};' ([class.copy.elision]) and not
possible for a non-copyable class -- and would copy instead of bind a
reference result.
N5008 [dcl.contract.res]/1: the result name denotes the result object;
[expr.call]/9 and [stmt.return]/5: the postconditions are evaluated when
the function exits normally, after its local variables are destroyed.
They are now added by a new goto-programs pass,
instrument_cpp_postconditions, which process_goto_program runs after
elide_cpp_returned_temporaries: at END_FUNCTION, unless an exception is
in flight, on the result object -- for a class result the caller's object
reached through the hidden result parameter, otherwise the returned
value (for a reference, the pointer CBMC represents it with). The front
end marks the contract symbol (#cpp_enforce_postconditions) and gives
each postcondition its property location; preconditions and
contract_assert are unchanged. Postconditions are now also checked
after the local variables' destructors run, as the standard says
(previously before them).
New tests cpp26_postconditions_class_and_reference_results,
cpp26_postcondition_of_class_result_violated and
cpp26_postcondition_of_reference_result_violated.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
When a called function has no library model but a body in the program's own symbol table that goto conversion left out (the C++ front end makes constexpr functions macro symbols, which goto_convert skips), add_one_function converts it and then linked the result with link_goto_model: a pass over all of goto_model's symbols (linkingt::link) and over all of its functions (rename_symbols_in_function with an empty renaming). The result has no symbols to link, so this only cost time, once per such function. For std::print with libstdc++ 16 that was 1197 of 1215 links, and the library phase took 18 s of 55 s (more than type checking). The function is now added directly; the library phase takes 4 s, and std::print and std::format run about 13 s faster with the same results. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
instantiate_template looked for an existing instance under the template's plain name, but alias templates, variable templates and concepts register their instances under the name with the template-argument suffix: every use re-instantiated the specialization. For std::print with libstdc++ 16, 19,000 of 62,000 instantiations were such repeats (`enable_if_t<true, void>' 689 times, `integral<long>' 567 times, 10,000 distinct of 56,000 requests overall). N5008 [temp.alias]/2: an alias specialization is the type obtained by substituting its arguments; a variable template (or concept) specialization is likewise determined by them. An instance found under the suffixed name is now reused. A substitution failure makes no instance, so it is not cached. Type checking of std::print: 19.5 s -> 14.6 s. New test cpp20_alias_and_variable_template_instances_reused guards the results. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
release_referenced_held_back_bodies, once per round of the method-body drain, walked the value of every symbol to find references to held-back speculative instances ([temp.inst]/11). Values that are still the tree scanned in an earlier round (kept shared in a cache) are no longer walked again; the functions they refer to are remembered. For std::print: 1.5 s -> 0.2 s over 10 rounds. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
2208f5e let the Microsoft runtime's memcpy and memmove accept a null pointer with a zero length by writing the preconditions as `__CPROVER_MEMCPY_EMPTY_OK || __CPROVER_r_ok(src, n)', with the macro `0' for the other runtimes. instrument_preconditions copies the precondition to each call site with the arguments substituted, and goto_check_c then checks the argument expressions in the right operand of || under the guard `!(0 != 0)'. Guarded, these checks differ from the ones already made for the call itself, so each was made twice: for aws-c-common's aws_array_list_back 405 properties instead of 386 and 78 VCCs instead of 71, and more solver time in perf-benchcomp. The two cases are now written out separately. New test memcpy_argument_checks_not_duplicated (22 properties before, 20 now). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
cf8a92b made malloc, calloc, alloca and the contracts library's allocations record their object in __CPROVER_new_object, so that delete[] of an array made by new[] still succeeds after a malloc. Only a program with C++ code can use new[] or delete[], but C programs paid for the recording too: 5 to 43 more symex steps in 154 of the 170 aws-c-common proofs, and MiniSat is sensitive to such small changes (aws_priority_queue_pop 4.5 s -> 7.1 s, flagged by perf-benchcomp). The models are C, so `__cplusplus' cannot tell; instead the library linker now defines __CPROVER_CPP_PROGRAM in the models' prologue when the symbol table has a symbol of C++ code (has_cpp_code), and the recording is under `#ifdef __CPROVER_CPP_PROGRAM'. --dump-c-library-models also writes the models that differ for C++ programs, in that variant, to the subdirectory cpp-program, which --c-library-models uses for C++ programs; the manifest names the subdirectory, so directories dumped before are not used. All 170 proofs now have develop's steps, VCCs and properties. New tests: malloc_no_new_object_record_in_c (fails before: the object was recorded in a C program), cbmc-library-models/cpp_program_models (delete[] after malloc with dumped models). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The checks of an operand of ||, && or ?: are guarded by the operands evaluated before it. A constant one was kept as a guard: in `0 || e' the checks of e became `!(0 != 0) => check', which differs from the same check made elsewhere and so was added again (the duplicated argument checks of memcpy's preconditions, 762804c), and after `1 || ...' or `false ==> ...' the operands that are not evaluated were checked under a false guard (C17 6.5.13/4, 6.5.14/4, 6.5.15/4). A constraint that simplifies to true is now not used as a guard, one that simplifies to false ends the checking of the remaining operands, a `?:' with a constant condition checks only the operand it evaluates, and a guard `true => check' is the check itself. New test checks_under_constant_guards (5 properties before, 2 now). Updated: Bool/bool5 (10 -> 4 VCCs: memcpy's overlap checks behind `pointer_object(dst) != pointer_object(src) ||' for distinct objects), short_circuit_implies/short-circuit-memory-checks (the dereference after `false ==>' is not checked), memcpy_argument_checks_not_duplicated (20 -> 6 properties). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Each round of the deferred-member drain in typecheck_method_bodies walked every converted body to find the deferred members it refers to ([temp.inst]/11) and the classes of the objects it names ([class.dtor]/14); typecheck_method_bodies runs several times per translation unit, and the walk took 1.5 s of std::print's type checking. The results are now cached per body, with a shared copy of the value scanned: a body that is still that tree is not walked again. (A cache local to one call, tried in round 226, gained nothing: there are only one or two rounds per call.) Type checking of std::print: 14.6 s -> 13.5 s. 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>
The test of 7db162e (simplify p - p to 0), added with its upstream pull request. 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.