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 3353 commits into
Draft
tautschnig wants to merge 3353 commits into
tautschnig wants to merge 3353 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
A 103-line reduction of cpp20_range_adaptor_closure_invoked_through_ invoke_impl (cvise; the oracle required, in one run, the spelled-out form to be right and the pack form wrong, with g++ 13 and clang++ 18 accepting both as static_asserts). N5008 [over.match.best]/2.5, [over.ics.rank] /2.1: in decltype(_S_test<_Callable, _Args...>(0)) with the pack of __invoke, called from _Binder::_S_call, cbmc selects the C-style variadic operator() over the constrained two-parameter template. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [over.match.oper]/3, [over.over]/1, [temp.deduct.funcaddr]/1: in `o << endl' the parameter type of a candidate operator function is the target that selects from the overload set named by `endl'. The operands were type-checked before the operator was resolved, so `endl' was resolved without a target (deduce_without_call_arguments, from the first complete specialization of the stream class in the symbol table): with two stream specializations one insertion called operator<<(bool), and with libc++ `std::cerr << std::endl' did so in a file named main.cpp. resolve_overload_set_operand, run before the operands are type-checked, deduces the name against the member operator@ functions of the left operand's class whose parameter is a pointer to function, and uses the function when they agree. Not covered: non-member candidates and parameters of reference-to-function type (the earlier resolution then applies). cpp11_manipulator_overload_for_each_stream_specialization: KNOWNBUG -> CORE. cpp11_iostream_cerr_libcxx and cpp11_libcxx20_endl verify without bounds (about 7 s each) and lose no-vacuity-check. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Soundness fix (silently wrong values). N5008 [dcl.init.aggr]/2: the
elements of an aggregate are its direct bases, then its members; in
`D{{6}, 7}' ([expr.type.conv]/2) the base E is initialized from {6} and
the member w from 7. The explicit-constructor-call path reshapes the
braced list into a struct value; it skipped one empty clause per base and
paired the rest with the class's own members, so for a base with data
members (flattened into the class) the base's clause went to the first
member: `D t = D{{6}, 7};' gave t.v == 0, t.w == 6, and a thrown
`D{{6}, 7}' a wrong exception object. The comment there already said
such bases keep the constructor path; they now do, and it initializes
the base subobject.
cpp17_prvalue_aggregate_with_base_initializes_object: KNOWNBUG -> CORE
(extended with an empty and two non-empty bases).
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Soundness fix. N5008 [istream.formatted.arithmetic]/1-3: `cin >> i' extracts through the num_get facet of the stream's locale ([facet.num.get.virtuals]); [locale.general]/8: the "C" locale has one. libstdc++ creates it in its compiled library; the models answered that num_get is absent (has_facet) and use_facet left a nondeterministic facet pointer, so __check_facet called std::__throw_bad_cast (no body) and cin.fail() held on every path -- the paths on which input succeeds were missing. num_get is now provided as num_put is (classic_num_put builds a static facet object with its vtable), and libstdc++'s own do_get parses the unknown input; has_facet reports it present. cpp11_istream_integer_extraction: KNOWNBUG -> CORE for libstdc++; its assertion now follows the standard's outcomes (0 on a failed conversion, INT_MAX/INT_MIN out of range, [facet.num.get.virtuals]/3; nothing extracted when the sentry fails, [istream.formatted.reqmts]/1), checked with g++ on six inputs. The libc++ desc stays KNOWNBUG: libc++'s locale::use_facet has no model (as for its num_put). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…agnosis The failure needs a caller whose call to __invoke expands a function parameter pack followed by another argument; calling __invoke directly, or from a caller with one named parameter, selects the right operator(). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
When a function template body is instantiated, single-element packs of the template map have their names replaced by the element, and the ellipsis of each expansion over such a pack is dropped. The removal ran on every node of the body, so it also collapsed expansions of packs it did not substitute. The template map can still hold a one-element pack of the calling instantiation (`X` of `call(X... x)` calling `inv(F(), x..., 0)`), and then `count_args<C, Args...>` in inv's body, with a two-element `Args`, got one template argument. N5008 [temp.variadic]/8-9: a pack expansion is expanded by the packs named in its pattern. Drop the ellipsis only on nodes whose subtree names a substituted pack. This fixes the call result computed through libstdc++'s _Binder::_S_call in <ranges> (__invoke selected the one-parameter operator() of _Partial and the closure call lost its body): the KNOWNBUGs cpp20_call_result_through_pack_in_static_member_template and cpp20_range_adaptor_closure_invoked_through_invoke_impl are now CORE. With the libstdc++ 16 headers (g++ 16.2.0), the same drop broke cpp20_ranges_views_iota_transform_filter_drop, which now passes there and loses its broken-libstdcxx16 tag. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [except.spec]/6: an implicitly-declared constructor, or one defaulted on its first declaration, is potentially-throwing if and only if the initialization of a potentially constructed subobject (a base, a virtual base of a non-abstract class, a non-static data member, an array element) is, or, for a default constructor, a default member initializer is. The noexcept operator took every such constructor as non-throwing, so `noexcept(Holder(h))' was true for a member whose copy constructor may throw. The analysis of the noexcept operator becomes expression_is_potentially_throwing. For an implicit or defaulted default, copy or move constructor, implicit_constructor_is_potentially_throwing direct-initializes each subobject (with no argument, or from an lvalue or xvalue of the source's subobject, with its cv-qualification) in a substitution context and analyzes the resulting code; a default member initializer is type-checked in the class's scope (one that names another member cannot be, and is taken as non-throwing). Unions copy their object representation. This replaces default_construction_is_nothrow. [meta.unary.prop] Table 54: __is_nothrow_constructible(T, Args...) was true for every T with arguments. It now direct-initializes T from the arguments (a constructor or, for a scalar, a conversion function) and requires the initialization to be well-formed and non-throwing; for a reference T it is __is_constructible. The KNOWNBUGs cpp11_implicit_constructor_exception_specification and cpp11_is_nothrow_constructible_with_arguments are now CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [class.copy.ctor]/8: a class without a user-declared copy constructor, copy assignment operator, move assignment operator or destructor has an implicitly-declared move constructor, which moves each member ([class.copy.ctor]/14). The front end declares it only when a subobject is move-only, so Holder(std::move(a)) copies the member, and the noexcept operator reads the copy constructor's exception specification. Found while testing the exception specifications of implicit constructors. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [class.cdtor]/4: a virtual function called from a constructor or destructor on the object under construction or destruction is the final overrider in the constructor's or destructor's class. For a base with virtual bases, the Itanium C++ ABI (2.6.2) uses construction vtables: the base's overriders with the complete object's virtual-base offsets. Only the complete object's direct bases got them; a base-object constructor (M's, for M a base of D) left the tables its caller had installed while constructing its own base A, so A's constructor called M::id. The ABI passes M's constructor a VTT for this. Without a VTT: before a base-object constructor constructs a direct base with virtual bases, it now declares a copy of each of the base's own tables, sets the copy's virtual-base offsets from the virtual pointers in place (those of the complete object being constructed), saves the current pointers and installs the copies; after the base's construction it restores the saved pointers. full_member_initialization emits a `cpp_base_construction_vtables' statement before and after the base, expanded by typecheck_base_construction_vtables once `this' is known. Around a dynamic base without virtual bases, whose constructor installs its own tables into the shared pointers, the pointers are saved and restored as well. A base-object destructor gives the base the same tables before destroying it. Two errors on the way: do_virtual_table inserted the construction tables into the symbol table (an unordered map) while iterating over it, and virtual_table::V@M@D was skipped; and the pointers of a base subobject are now matched by subobject path, since a base class that occurs twice has renamed pointers (cpp_repeated_polymorphic_base_with_virtual_base). The KNOWNBUG cpp11_virtual_call_in_constructor_of_indirect_base_with_virtual_base is now CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
cpp_repeated_base_virtual_call_through_second_path: the virtual pointer of D's second A subobject (through C) holds a table of type virtual_table::A, which the conversion from C to the virtual base V reads as a virtual_table::C, out of bounds: V::g's dispatch through C is wrong (N5008 [class.virtual]/2). cpp_implicit_destructor_of_class_derived_from_repeated_base: E : D, with D : B, C and B, C : A polymorphic, is rejected because E's implicit destructor converts to the ambiguous base A ([class.mi]/3). Both fail the same way on the previous build; found while testing construction vtables. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [temp.spec.general]/5: every use of a variable template
specialization names the one variable. The second use of `vb<char>',
for `template <class> auto vb(7);', instantiates the specialization
again; that declaration still has the placeholder type and was rejected
("already declared with different type: original: signed int, new:
auto"). combine_types now keeps the type the first instantiation
deduced ([dcl.type.auto.deduct]/2.2.3), and the repeated initializer is
dropped: its constructor-form value would have replaced the converted
value.
The KNOWNBUG cpp14_auto_variable_template_with_parenthesized_initializer
is now CORE.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [basic.start.dynamic]/1: a variable template specialization or a static data member of a class template specialization is dynamically initialized (unordered). Such variables are mostly instantiated while function bodies are type-checked, after static_and_dynamic_initialization built the initialization procedure. Their value, a constructor call, then stayed the initial value: __CPROVER_initialize assigned the code to the object, a type-inconsistent assignment (any variable template of a class type with a constructor, or `template <class T> S X<T>::s(...)'). static_and_dynamic_initialization now runs again for the variables registered after the method bodies (and once more before the final sweep), appending to the initialization procedure. Block-scope static variables are no longer registered: [stmt.dcl]/3 initializes them at their declaration statement, and the second pass would have constructed them again (cpp98_static_local_initialized_once). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [class.mem.general]/9.4: the noexcept-specifier of a member function is a complete-class context, so `void a() noexcept(noexcept(b()))' may name a b declared later. evaluate_noexcept_expression keeps such a specifier for implicit_exception_specifications when its evaluation at the declaration fails, but a noexcept operator whose operand cannot be type-checked yields true (the front end treats the failure like a substitution failure), so the specifier was evaluated to true and never kept. The front end now counts such operands, and a member's specifier whose evaluation met one is kept. The retry with the complete class also had no `this', so `b()' did not call this->b() ([expr.prim.this]/4); it is now bound to the member function's object parameter. Not for a class template specialization: evaluating each member's specifier there instantiates templates the program does not use ([except.spec]/12 instantiates it when needed), and that broke cpp20_ranges_basic; that case is the KNOWNBUG cpp11_member_noexcept_specifier_in_class_template. The KNOWNBUG cpp11_member_noexcept_specifier_names_a_later_member is now CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…late In W<int>, `void a() noexcept(noexcept(b()))' with a later `void b() noexcept(sizeof(T) == 1)' is taken as non-throwing: the kept specifier is evaluated again without `this' for a class template specialization, so `b()' does not call W<int>::b. N5008 [class.mem.general]/9.4, [expr.prim.this]/4, [except.spec]/12. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Resolving `~D' for an object of class D (E's implicit destructor destroying its base D, with D : B, C and B, C : A polymorphic) also found the destructor thunks of D's bases, which are in the class scope. Matching a thunk's `this' (an A *) converted D to A, an ambiguous base ([class.mi]/4), and the program was rejected. A thunk is the vtable entry of an overrider for a base, not a declaration of the program: it is no longer a candidate. The KNOWNBUG cpp_implicit_destructor_of_class_derived_from_repeated_base is now CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
D's second A subobject (`D : B, C', B, C : A) has its own virtual pointer, which held a table of type virtual_table::A. Code that sees the subobject as part of C reads the pointer as a virtual_table::C: the conversion from C to the virtual base V read C's offset of V outside the table, and V::g through C was dispatched wrongly ([class.virtual]/2). do_repeated_subobject_virtual_tables now copies the direct base's whole table (C's) and vtable_pointer_value points into the copy along the members it pointed into the base's table. The copy is made also when the class declares no overriders but has virtual bases, whose offsets depend on the class (set_virtual_base_offsets). Each embedding level of the table gets its own thunk for an overrider, since the slots' `this' types differ. The KNOWNBUG cpp_repeated_base_virtual_call_through_second_path is now CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [except.spec]/12: the noexcept-specifier of a specialization of a templated function is instantiated only when it is needed. For a member of a class template specialization, implicit_exception_specifications evaluated the kept specifier when the class was complete, without `this' ([expr.prim.this]/4), so in `void a() noexcept(noexcept(b()))' `b()' did not call W<int>::b; evaluating it there with `this' would instantiate templates the program does not use (it broke cpp20_ranges_basic). Such a specifier is now kept with the class and its template arguments and evaluated, in the class's scope and with `this', when it is needed: by the noexcept operator for a callee ([except.spec]/12.1), and at the end of type checking for the instantiated definitions (/12.4; goto conversion makes a non-throwing function call std::terminate). The KNOWNBUG cpp11_member_noexcept_specifier_in_class_template is now CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…mbers
N5008 [class.copy.ctor]/8: a class without a user-declared copy
constructor, copy assignment operator, move assignment operator or
destructor has an implicitly-declared move constructor, which moves each
member (/14). The front end declared it, with the move assignment
operator, only for a class with a move-only base or member, so for
`struct Holder { M m; }' `Holder(std::move(a))' copied m, and the
noexcept operator read the copy constructor's exception specification.
They are now declared for a class with a base or member of a class that
has a move constructor (declared or implicit). For the other classes
the memberwise move initializes each subobject as the memberwise copy
does, and the implicit copy constructor keeps serving.
The KNOWNBUG cpp11_implicit_move_constructor_moves_members is now CORE.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [expr.dynamic.cast]/8: for a pointer v to a polymorphic class,
`dynamic_cast<cv void *>(v)' is a pointer to the most derived object v
points into (null for a null v, /6). dynamic_typecast reached
UNREACHABLE ("currently not supported") and cbmc aborted. The cast is
now the run-time check of runtime_dynamic_cast with the most derived
object as the target: for each candidate most derived class, v minus the
offset of v's subobject in it.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…bject N5008 [expr.delete]/3, /6: an object deleted through a pointer to a base class with a virtual destructor is the most derived object, and the deallocation function is passed the value the allocation returned, its address. convert_cpp_delete passed the operand: through a non-primary base the pointer to that subobject (`Y *p = new Z; delete p;' failed "delete argument must have offset zero"). The C++ front end attaches the address of the most derived object, computed as for dynamic_cast<void *> ([expr.dynamic.cast]/8), to a delete-expression whose operand points to a polymorphic class and has no side effects; goto conversion reads it before the destructor runs and passes it to the deallocation function. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ed object `struct B : virtual V' overrides V::g; in `struct D : B' with data members V lies at another offset from B than in a complete B. The thunk through which V's table enters B::g subtracts V's offset in a complete B from `this', so both during B's construction and after it the call reads outside the object (N5008 [class.cdtor]/4, [class.virtual]/2). The Itanium C++ ABI uses virtual thunks that read a vcall offset from V's table. Found while testing the tables of repeated base subobjects; the previous build fails it the same way. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
N5008 [class.copy.ctor]/10: the defaulted move constructor of a class is defined as deleted when a subobject's move constructor is deleted, and note 4: such a constructor is ignored by overload resolution, so an rvalue uses the copy constructor. b018b10 declared the implicit move constructor for a class with a member whose class has a move constructor, also a deleted one: `H(std::move(a))' with `M(M &&) = delete' called the bodyless move constructor ("no body for callee"). Only a move constructor that is not deleted counts now. The previous build (W189) handled this shape. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
- cpp11_is_nothrow_constructible_reference_through_conversion_function: __is_nothrow_constructible(T &, U) is __is_constructible; a throwing conversion function is not seen ([meta.unary.prop] Table 54). - cpp_delete_call_result_through_second_base: the most derived object's address is attached only to delete-expressions whose operand has no side effects, so `delete make()' still passes the base pointer ([expr.delete]/6). - cpp11_exception_ptr_rethrow: std::current_exception and std::rethrow_exception have no model ([propagation]). - cpp17_noexcept_function_pointer_of_class_template_member: the deferred noexcept-specifier of a class template member is not evaluated when its address is converted to a function pointer ([except.spec]/12.3, [conv.fctptr]); the previous build fails it the same way. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> (cherry picked from commit d0af4214a6181bc702f7ba02a557e03233b0ea9e)
With the released libstdc++ 16.2.0 headers, <chrono> loses the body of __get_leap_second_info and <format> that of __do_vformat_to<_Sink_iter<wchar_t>, ...>; four CORE tests fail with those headers (cpp11_libstdcxx_header_drops test_chrono, test_format, test_format_typecheck and cpp11_namespace_reopened_after_qualified_member_template_definition test_libstdcxx). The 16-20260315 snapshot the CI gcc-16 job installs converts both. The descs record the suppressed diagnostics. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> (cherry picked from commit 273ed85cea48f78906adcd391802a4a910e48b91)
With the MSVC STL, symbolic execution of `ss << setw(4) << 7' does not end: cpp11_stream_setw and cpp11_ostream_integer_insertion_classic_locale are libstdcxx-tagged because they time out on VS 2022 and VS 2026, and no KNOWNBUG recorded that. This one is meaningful only with the MSVC STL, like cpp11_standard_stream_objects_initialized_msvc. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> (cherry picked from commit da227cb2470d25759cf17ce56d4b5ad3035d69ec)
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.