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 3091 commits into
Draft
tautschnig wants to merge 3091 commits into
tautschnig wants to merge 3091 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.53% +1.63%
===========================================
Files 1718 1733 +15
Lines 190266 231146 +40880
Branches 73 82 +9
===========================================
+ Hits 153939 190785 +36846
- Misses 36327 40361 +4034 ☔ 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
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [dcl.enum]/2 allows `enum class E : bool'; to_integer accepted only bit-vector underlying types, so such a constant as a template argument failed "expected to be scalar constant" (also on develop). std::ranges::subrange_kind is one; GCC 14's <format> reaches it once __literal_encoding_is_unicode is evaluated. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ized N5008 [temp.deduct.partial]/8, /11: a function parameter pack deduces from every remaining parameter of the other template, so a template whose whole parameter-type-list is one pack (libc++'s fall-back `__nat __invoke(_Args&&...)') is less specialized than one with a leading non-pack parameter (`__invoke(_Fp&&, _Args&&...)'). Partial ordering compared equal-length lists only, and the call was ambiguous (also on develop). With libc++ 19 every ranges algorithm with a projection reached it: __get_property and __estimated_width in <format> and std::apply lost their bodies (macOS CI job); with --stdlib libc++ no body of round 185's libc++ 19 translation units is dropped now. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
With the per-test timeout the macOS 14 job named the problem: no single test hangs except two libstdc++ tests that with libc++ need a std::function call model or 7.7 GB (now gcc-only); the remaining tests take about 2900 s run serially, too close to the 4800 s TIMEOUT. The CORE profile is now cbmc-cpp-1..4-CORE (add_sharded_test_pl_profile, test.pl --shard), which ctest -j runs in parallel; locally the four take 304 s wall-clock for 950 s of tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [dcl.fct]/6, [over.match.funcs]/4: a member function with an explicit object parameter has no implicit object parameter; for a const object `this Self &&self' deduces Self as const S &. member_template_object_viable rejected such a member template because it is not const-qualified. GCC 16's ranges adaptor closures (_Partial::operator()(this _Self&&, _Range&&)) are invoked on const objects by std::__invoke. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [temp.func.order]/6.4: when partial ordering leaves two function templates equally specialized, the more constrained one ([temp.constr.order]) is more specialized. The overload set of a libc++ customization point object (`template <class T> requires ... auto operator()(T &&)' next to `void operator()(auto &&) const = delete') was ambiguous; it becomes reachable once abbreviated member function templates are recognized. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [dcl.fct]/22: a function with a placeholder parameter type is an
abbreviated function template, members included. The rewrite into a
template ran for namespace-scope declarations only, so a constructor
subrange(auto __first, _Sent __last) kept an `auto' parameter and
{first, last} found no constructor. GCC 14's <format>
_M_parse_fill_and_align (`_Utf32_view<subrange<iterator>>
__uv({__first, __last})') lost its body once eede475 let
__literal_encoding_is_unicode evaluate (the gcc-14 CI job's three
failures).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
check-clang-format formats the test with the repository's style (its concept definitions differ from the c++20 style used before). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
A function whose class-type result gets a hidden result parameter changes type; only direct calls were updated. Its address taken elsewhere (N5008 [conv.func]/1, e.g. a function pointer stored in a table) kept the old type and failed --validate-goto-model. Such references now carry the new type, cast back to the original pointer type; calls through function pointers have been resolved to direct calls already. cpp17_abstract_environment_tu (CBMC's own abstract_environment.cpp, whose static map stores assume_not) verifies again and is THOROUGH. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [stmt.dcl]/3: a block-scope variable with static storage duration that is not constant-initialized ([basic.start.static]/2) is initialized the first time control passes through its declaration. An expression initializer stayed the symbol's value, so __CPROVER_initialize evaluated it at program start, with undefined parameters and `this'. It is now assigned under the guard static_local_initialization already uses for constructor calls. This was the remaining failure of std::regex_match and std::regex construction (libstdc++'s _AnyMatcher::operator(), `static auto __nul = _M_translator._M_translate(0)'); both tests verify again and are THOROUGH. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The job runs test.pl directly, so the -X broken-libstdcxx16 that regression/cbmc-cpp's CMakeLists.txt and Makefile add for gcc 16 did not apply; its four failures in CI run 4 were exactly those tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
… map
N5008 [temp.inst]/4, [dcl.spec.auto.general]/15: a member of a class
template specialization is instantiated with the class's template
arguments. A call of a static member function whose return type is
still a placeholder converted the member's body under the caller's
template map, so the class's parameters were unbound; the body's queued
entry already records the right map. GCC 11's std::visit lost
__gen_vtable_impl::__visit_invoke this way ("no match for symbol
'is_same_v'") and with it _S_apply_single_alt.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
decltype(invoke()) in the initializer of a static constexpr member, where
invoke returns a call of a member template with a deduced return type, is
not int while the class is instantiated ("template 'element' not found").
Found while reducing GCC 11's std::visit, which still drops
declval<decltype()>.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [namespace.def.general]/7: a member of an inline namespace can be
explicitly specialized as though it were a member of the enclosing
namespace. The primary template was looked up in the current scope only,
so `namespace std { template <> struct hash<K> { ... }; }' failed with
libc++, whose std::hash is std::__1::hash ("class template 'hash' not
found", four cbmc-cpp tests on macOS 14). The lookup now continues into
the inline namespaces, and the specialization is declared in the one that
holds the primary template, so it is found through either name.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [dcl.fct.def.default] and [dcl.fct.def.delete] are C++11 features that g++ and clang++ also accept in C++98 mode, as an extension with a warning. libc++ declares `exception(const exception &) _NOEXCEPT = default;' in every language mode, so any --cpp98 program that included a standard header failed to parse on macOS (cpp98_dynamic_cast_reference_throws_bad_cast). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Each virtual function in an initialized virtual table is an addressed object, and a candidate target of every call through a function pointer of its type. With libc++, <vector> and <functional> declare the locale facets through <locale> (`extern template class moneypunct_byname<char, false>;'): their virtual tables alone exceeded the 256 objects of the default --object-bits 8 (about half of the cbmc-cpp failures on macOS were "too many addressed objects"), and their destructors were all candidates of std::function's `__f_->destroy()'. A class that is never constructed (N5008 [class.virtual]: its virtual functions cannot be called) needs no table. slice_unused_virtual_tables keeps the functions and globals named in code reachable from the entry point (calls and address-taken functions alike) and in the initializers of the globals it keeps, and drops the initialization of the other virtual_table:: symbols. process_goto_program runs it before function pointer removal, so that the functions named only in the dropped tables are no longer address-taken. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
On macOS `gcc' is Apple clang, whose -dumpversion (15 or later) let the libstdcxxNN-tagged tests run against libc++; with MSVC, the gcc that Strawberry Perl ships did the same while cbmc preprocessed with cl. Tests that check libstdc++ internals (cpp11_libstdcxx_header_drops, std::__and_, the regex conversion symbol checks) failed in both places. Such tests get the tag libstdcxx, and the CMake and Makefile exclude it and the libstdcxxNN tags with MSVC or when the host gcc is clang. gcc16_optional_transform, a preprocessed libstdc++ 16 file, is gcc-only like its sibling gcc16_* tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Six tests matched the goto program against libstdc++'s spelling of std::optional's constructors; with libc++ (macOS) they are named std::__1::optional and the tests failed although the constructors were there. The patterns allow the inline namespace. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
A member of the partial specialization fn<R(Args...)> defined outside the class has no body in fn<int()>, while fn<int(int)> gets it; no error is reported. libc++ defines std::function's members this way, so with libc++ std::function<int()> cannot be called (cpp11_std_function_call_libcxx, KNOWNBUG libcxx). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…tdcxx cpp11_stream_setw, cpp11_ostream_integer_insertion_classic_locale, cpp11_stream_destructor_chain and cpp11_pair_from_function_pointer_rvalue timed out on macOS 14 (libc++), VS 2022 and VS 2026 (the MSVC STL); with the CMake profiles' -t not enforced by native Windows perl, the VS 2026 cbmc-cpp shards ran into their 4800 s limit. They get the libstdcxx tag, whose description now includes such tests, with the cause in each desc: libc++ formats integers with vsnprintf, whose library model writes a nondeterministic string (KNOWNBUG cpp11_ostream_integer_insertion_libcxx), and std::function<int()> has no call operator with libc++ (cpp11_partial_specialization_member_defined_outside_empty_pack). The MSVC STL hangs could not be reduced without its headers. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Strawberry Perl (the VS 2026 CMake job) cannot fork, so test.pl ran tests without a time limit there and a hanging test held a whole cbmc-cpp shard until ctest's 4800 s TIMEOUT, without naming it. With -t, the test now starts asynchronously (perlport: system(1, LIST) returns the process ID); test.pl polls it with waitpid(WNOHANG) and, once the time is up, ends the process tree with taskkill /T /F and reports [TIMEOUT]. MSYS perl (the make jobs) and other platforms keep their paths. Not run on Windows before this commit. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [support.initlist]/1 leaves std::initializer_list's layout to the implementation. libstdc++ and libc++ store a begin pointer and a size, the MSVC STL a begin and an end pointer (`const _Elem *_First, *_Last;'). Building one from a braced-init-list stored the element count into the second member regardless, and from_integer's precondition failed for a pointer: 26 cbmc-cpp tests on VS 2022, reproduced from the msvc-preprocessed-headers artifact. initializer_list_extent gives the end pointer for a pointer member. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The macOS 15 make and VS 2026 jobs uploaded the failed cbmc-cpp tests preprocessed with the platform's standard library, so that a failure can be reproduced on Linux (cbmc --os macos, cbmc --winx64). The steps move into scripts/preprocess_cpp_tests.sh and .ps1, and the macOS 14 cmake and VS 2022 make jobs run them too. Tests that time out on those platforms are excluded with the libstdcxx tag, or are missing from test.pl's logs when ctest ends a shard, so env.cpp-preprocess-tests lists them for preprocessing in addition to the failed ones. The .ps1 script was run with PowerShell 7 on Linux and a stub cbmc only. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
MSVC provides __builtin_bit_cast(To, from) since VS 2019 16.8, and the MSVC STL builds _Bit_cast (<type_traits>), and with it std::bit_cast and <compare>'s orderings, on it. The scanner recognised it in GCC and clang modes only, so with MSVC it was an unknown symbol and _Bit_cast lost its body: 44 such drops among the cbmc-cpp failures on VS 2022, reproduced from the msvc-preprocessed-headers artifact. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [expr.reinterpret.cast]/1: the result has the type named in the cast. conditional_cast leaves the operand alone when the types compare equal, and irept comparison ignores #c_type, so reinterpret_cast<long *> of a `long long *' kept the source type and overload resolution, which distinguishes the two, chose another function or none. On Windows int and long have the same width: the MSVC STL's `__iso_volatile_load32(reinterpret_cast<volatile int *>(&_Uses))' with a long _Uses found no match, and _Incref_nz (<memory>, 26 drops on VS 2022) and _Atomic_lock_release (<atomic>, 15) lost their bodies. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [dcl.init]/9, [dcl.init.list]/3.11: a mem-initializer `data{}'
value-initializes the array member, zero-initializing every element. For
an array of arrays the element-wise zeroing assigned an array value to
each element ("direct assignments to arrays not permitted"). The MSVC
STL's _Digit_pair_table (<xutility>, `_Elem _Data[100][2]' with
`: _Data{}') lost its constructor body.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…r pack N5008 [temp.variadic]/5: a function parameter pack `Args... args' in a definition stands for any number of parameters. Matching the out-of-class definition of a member of `template <class R, class... Args> struct fn<R(Args...)>' to the instantiated member counted it as one, so for fn<int()> and fn<int(int, int)> no definition matched and the member had no body (libc++'s std::function<int()>::operator()). The definition now matches any arity from its non-pack parameters on, and the member's parameters take the names the instantiated body uses for the pack's elements: args for one, args$0, args$1, ... otherwise. The KNOWNBUG cpp11_partial_specialization_member_defined_outside_empty_pack is now CORE as ..._parameter_pack, covering 0, 1 and 2 elements. 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
1 participant
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.