[Individual PRs to follow] C++ standard support: C++11 through C++26 parser, type-checker, and STL improvements#8878
Draft
tautschnig wants to merge 395 commits into
Draft
Conversation
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
10 times, most recently
from
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.55% 81.00% +0.44%
===========================================
Files 1707 1709 +2
Lines 189016 201754 +12738
Branches 73 79 +6
===========================================
+ Hits 152261 163425 +11164
- Misses 36755 38329 +1574 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
10 times, most recently
from
8f4e2d7 to
f3d208e
Compare
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
6 times, most recently
from
5cc8d28 to
980d519
Compare
tautschnig
force-pushed
the
cpp11-parser-rework-squashed
branch
from
980d519 to
883082a
Compare
The member function template scope registration fix should help resolve template operators (insert, iterators, etc.) on MSVC. Re-enable set_insert, map_insert, map_verify, map_basic, STL1, list_pushback, string_view, variant, numeric, and sort tests. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The check for keeping resolved return types when a function is redeclared with unresolved auto/decltype was in the wrong branch of the if/else chain in combine_types. When both types are ID_code, the outer if block is entered, and the else-if chain (where the fix was) is never reached. Move the check inside the outer if block, after the inner return-type-match check fails. This correctly handles the case where a function template instance exists with a resolved return type (e.g., int*) and is redeclared with an unresolved decltype return type. Fixes numeric_basic (accumulate/_Get_unwrapped). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
When a qualified name lookup fails to find a member in a class scope (e.g., allocator<int>::propagate_on_container_swap), throw without producing an error message. This is a potential SFINAE failure — the lookup might be inside a void_t check or enable_if condition where the failure should silently discard the template specialization. Previously, the error message was only suppressed when suppress_elaborate was true. But SFINAE contexts like partial specialization matching don't always set this flag. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Three improvements: 1. Make scope-not-found a silent SFINAE failure: throw without error message for all scope-not-found failures in qualified name lookup. This handles void_t SFINAE patterns where typename _Ty::member fails for types without the member. 2. Replace null_handler with error count save/restore in partial specialization matching (typecheck_template_args). 3. Fix auto/decltype return type check: move inside the outer if(both code) block where it's actually reachable. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.inst]/1, template arguments in partial specialization matching don't require complete types. Set suppress_elaborate during typecheck_template_args for partial specialization argument validation. This prevents eager elaboration of template arguments that may fail (e.g., void_t SFINAE patterns in _Get_propagate_on_container_swap). Empty and incomplete template instances are still elaborated (the suppress_elaborate logic allows this). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Before calling instantiate_template in elaborate_class_template, re-check if the symbol has already been completed by a recursive call during specialization matching. Per the C++ standard, a class template specialization that is already complete should not be re-instantiated. This prevents the second elaboration attempt from overwriting a successfully-elaborated class with a new empty struct. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.inst]/3, member function templates may reference their own template parameters during class body processing. These parameters are not in the class template map, so type resolution may throw. Catch the exception and skip the member template declaration — it will be instantiated on demand when called. This prevents function template parameter lookup failures from propagating up and killing the enclosing method body processing. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.res.general]/6 (C++23), static_assert(false) in a template body that is never meant to be called (e.g., MSVC's std::declval guard) should not be fatal. Convert to a skip so the body can continue processing. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.deduct]/8, when a template alias resolves to a non-class type during qualified name lookup (e.g., remove_reference_t<int> resolves to int), treat it as a substitution failure rather than a hard error. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [dcl.type.simple]/2, when a name with explicit template arguments resolves to a class type and no function arguments are provided, it is a type-name rather than a constructor invocation. Skip make_constructors in this case so the caller receives the type expression. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.inst]/3, member function template type-checking may fail when function template parameters are not in the class template map during instantiate_template's method processing. Catch the exception and return the template symbol so the caller can continue. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [over.match.list] and [dcl.init.list]/3.6: when a
braced-init-list is used to initialize a class type, first try
matching it as a single std::initializer_list argument. If that
fails (including via exception from the resolver), fall back to
unpacking the elements as individual constructor arguments.
This fixes brace initialization of class types like
_Uninitialized_backout_al<_Alloc> _Backout{_Dest, _Al}
where the class has no initializer_list constructor.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.res]/8, function template parameter types may reference other template parameters not yet in the template map during class body processing. If cpp_convert_plain_type fails, use the unconverted type — it will be resolved when the function template is actually instantiated. This replaces the broader catch in typecheck_compound_body that was skipping entire function template declarations. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.deduct]/8, qualified lookup failure during template instantiation is a substitution failure. Throw silently without printing an error message so that SFINAE mechanisms can handle it gracefully. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.deduct.call]/1, resolve remaining simple cpp_name types to actual types via scope lookup during function template argument deduction. This allows the deduction to match parameter types like _Zero_then_variadic_args_t against argument types. Also catch exceptions from instantiate_template during deduction — the instantiation may fail if the function body references types that can't be resolved, which should be treated as a deduction failure per [temp.deduct]/8. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…sion Per [temp.deduct]/5,8, [over.match.ctor], [temp.variadic]/5,7, [temp.deduct.call]/3, [temp.arg]/2: KEY FIXES: - Empty variadic pack removal scoped to CURRENT template's parameters only (fixes incorrect parameter removal) - Non-empty pack expansion with name substitution and targeted ellipsis removal - Pack removal applies to ALL function templates with variadic packs (not just constructors) - Store function template type/args on method symbol for method_bodies template_map restoration ([temp.inst]/1) - Single-element pack types added to type_map - Reject template-typed instantiation results in GFTA ([temp.deduct]/8) - Forwarding reference detection and const-preserving deduction ([temp.deduct.call]/3) - Apply template_map to explicit template args in GFTA and typecheck_template_args ([temp.arg]/2) - Resolve bound template parameters in typecheck_type via template_map.apply() before further processing - Variadic packs allowed as 'all_have_defaults' in GFTA (empty pack counts as having zero-arg default) - disambiguate_functions synthesizes 'this' object for member method templates with empty operand lists - Fallback template_map lookup in resolve for name 'X' is unknown — handles method template params referenced via qualified calls (e.g., this->template f<U>(u)) - Template arg cpp_name resolution via template_map first in typecheck_template_args - apply_template_args tolerates method not in struct component list (inherited from base template) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…k-squashed # Conflicts: # src/ansi-c/expr2c.cpp # src/ansi-c/goto-conversion/goto_convert_side_effect.cpp # src/cpp/cpp_instantiate_template.cpp # src/cpp/cpp_typecheck_resolve.cpp # src/goto-programs/link_goto_model.cpp
Per [temp.type]/1, template specializations are identified by their template arguments including cv-qualifiers. The template_suffix function was generating the same suffix for T and const T when T is a struct_tag or union_tag type, causing different instantiations (e.g., forward<X> and forward<const X>) to collide. This fix ensures that forward<const X> produces a different instantiation than forward<X>, allowing const-qualified lvalues to correctly match const-aware forward overloads. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [dcl.spec]/1 and [temp.deduct]/5: when cv-qualifiers are specified as attributes (C_constant/C_volatile) on struct_tag or union_tag subtypes inside a merged_type -- which occurs when template substitution replaces a cpp_name for a type template parameter with a mapped type that carries cv-qualifiers -- these qualifiers must be recognized as applying to the final declared type. Previously, ansi_c_convert_typet::read_rec only recognized cv-qualifiers via the ID_const/ID_volatile sub-nodes introduced by the parser, losing qualifiers attached as attributes during template instantiation. This broke remove_reference<const X>::type and downstream uses of std::forward<const T>. This is the C++ standard fix for the const-preservation issue in template substitution. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Per [temp.deduct.call]/3: "A forwarding reference is an rvalue reference to a cv-unqualified template parameter that does not represent a template parameter of a class template. If P is a forwarding reference and the argument is an lvalue, the type 'lvalue reference to A' is used in place of A for type deduction." Previously, CBMC only used this rule when the argument had cv-qualifiers, and fell back to T = A (bare, without reference) otherwise. This caused incorrect deduction such as T = const less<int> instead of the correct T = const less<int>& for a const-qualified lvalue. With this fix, std::forward<T>(lvalue) correctly deduces T as the lvalue-reference type, allowing reference collapsing (T&& = A& && = A&) to produce the correct overload. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The #include <util/symbol_table_base.h> appeared twice: once at the top of the file (line 15) and once after the forward declaration of try_evaluate_constexpr (line 21). The IWYU check flagged the second instance as unnecessary. Remove the redundant include. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
libc++ on macOS uses __builtin_operator_new and __builtin_operator_delete as Clang-provided intrinsics that behave like the corresponding operator versions but can be evaluated in constant-expression context. Previously CBMC did not know about these, so parsing libc++'s <new> header wrapped in templates like __libcpp_operator_new reported 'symbol unknown' during template instantiation. Add declarations to clang_builtin_headers.h so that the builtin factory can materialise these symbols on demand. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
- Apply clang-format-15 to 8 files: reflow per repository style. - Rename struct depth_guard to depth_guardt in cpp_instantiate_template.cpp (cpplint readability/identifiers requires type names ending in 't'). - Add matching braces around nested 'if' in cpp_instantiate_template.cpp (cpplint readability/braces for if-bodies with multiple statements). - Remove duplicate #include <util/symbol_table_base.h> from cpp_typecheck_resolve.cpp (cpplint build/include). - Replace __CPROVER_size_t with CPROVER_PREFIX "size_t" in cpp_internal_additions.cpp (cpplint build/deprecated), splitting the string so no line exceeds 80 columns. - Add NOLINTNEXTLINE(readability/fn_size) to cpp_typecheckt::typecheck_template_args (501 non-comment lines, just one over the 500-line threshold). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The dereference_rec path rewrites an outer address_of(x::f) by calling
address_arithmetic on the object and using the result. For pointer-
to-member-function expressions, address_arithmetic's symbol branch
constructs the replacement using the single-argument address_of_exprt
constructor, which builds a plain pointer_type(op.type()) and does
not carry over the to_member attribute. That left the operand as a
plain pointer-to-code while a NULL pointer-to-member constant compared
against it retained to_member, causing
lhs and rhs of binary relation expression should have same type
invariant failures for patterns such as !(&x::f != 0) after the
simplifier folded it to address_of(x::f) == NULL-pointer-to-member.
This manifested on macOS because Apple libc++'s assert() macro
expands to '!(cond)' around the user expression, whereas glibc's
assert uses static_cast<bool>(cond) which does not trigger the same
simplification.
Fix: in dereference_rec, save the outer pointer's to_member attribute
before calling address_arithmetic; if the rewritten expression is a
pointer that has no to_member, restore it. This keeps the pointer-
to-member-function type consistent through all downstream consumers
and eliminates the need for the gcc-only workaround on macOS for
Address_of_Method1 and Vector1.
Reproducer (fails without this fix, passes with it):
struct x { void f(); };
void x::f() {}
int main() { return !(&x::f != 0); }
verified with --validate-goto-model --validate-ssa-equation.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The test uses static_assert which is a C++11 feature. Its sibling test is_convertible_builtin already specifies -std=c++11 for the same reason. Without the flag the test relied on CBMC's default C++ standard handling, which is configuration-dependent: - With a Clang preprocessor CBMC auto-upgrades to C++14 when no explicit --cppNN flag is given (per util/config.cpp). - On some macOS runners (notably macos-14 cmake-clang) this upgrade does not take effect for goto-cc in the same way it does for other configurations, leaving static_assert not recognised as a keyword (scanner.l predicate PARSER.cpp11). The parser then treats static_assert as an identifier and reports a spurious 'parse error before __is_assignable (...)'. Adding -std=c++11 matches is_convertible_builtin and makes the test's C++ standard requirement explicit and portable. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
log_version_and_architecture writes the CBMC version banner to stdout via log.status(), but --preprocess needs to emit the preprocessed source verbatim on stdout for consumers (notably the CI pipeline that uploads preprocessed .ii files as debugging artifacts). With the banner preceding the preprocessed output, anything parsing the .ii (including cbmc itself) rejects the first line with a parse error. Move the call to after the --preprocess and --test-preprocessor short-circuits so normal runs still print the banner but preprocess- only runs produce clean output. No other behaviour changes. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The gcc-only tag was added by 4a5fdf2 ("Fix macOS failures, restore error count in linkage spec") as a workaround when cpp11_vector_size reproduced the same validate-ssa-equation failure as Vector1 on macOS. The root cause — dereference_rec's ID_address_of branch dropping the to_member attribute of pointer-to-member-function types — is fixed in be467fb. Verified by running cbmc against the Apple-preprocessed .ii file produced by the macOS CI job (macos-preprocessed-headers artifact) with --cpp11 --validate-goto-model --validate-ssa-equation: now VERIFICATION SUCCESSFUL (0 of 1264 failed). Per the branch policy introduced by 8aa188b ("Remove gcc-only tags to enable macOS/MSVC testing"), gcc-only is reserved for tests that exercise genuinely GCC-specific syntax or built-ins, not as a workaround for platform-specific bugs. Audited the other pre-existing gcc-only tests in regression/cbmc-cpp and regression/cpp; each remains tagged for a defensible reason: * Function_Arguments1 glibc memchr signature clash * cpp17_any_basic std::any method bodies not processed on libc++ (distinct from to_member); the #if in the test already guards on compiler * cpp20_coroutine_types uses libstdc++ internal namespace std::__n4861 (not present on libc++) * cpp20_modules parses on all platforms in isolation, but the Makefile applies -X gcc-only on non-GCC builds for consistency with the MSVC-incompatible tests * gcc16_* GCC 16 preprocessed headers * gcc_attributes1, gcc_builtin_file_line named for their GCC feature * complex_type_overloading __complex__ type * cpp11_thread_header libc++ iterator_traits SFINAE scope issue (ea6a8d8) * enum_attributes1 __attribute__ on enumerators * gcc_attributes1 named for it * libcxx_namespace_attr __attribute__ on namespace (not MSVC) * type_traits_builtins1 __is_trivial, __is_pod GCC builtins * using_in_statement1 __asm(".globl ...") inline asm Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Four regression tests cover sections that were either marked partial or had no dedicated coverage. Running them also doubles as a conformance audit of the claimed implementation, since each test fails loudly if the underlying rule is not implemented. * cpp11_noexcept_operator — [expr.unary.noexcept]/3. Six static_asserts exercise builtin arithmetic, literal, noexcept function call, non-noexcept function call, implicit destructor noexcept, and throw-expression. Previously the coverage doc claimed noexcept "always evaluates to false"; the implementation actually follows the spec. * cpp11_addrof_member_compare — [dcl.init.ref]/5 and [expr.eq]/3. Regression for the dereference_rec to_member preservation fix (be467fb). !(&x::f != 0) triggers the simplifier to rewrite to &x::f == 0, and the symex symbol address-of must retain the outer pointer's to_member attribute so the two operands of the resulting equality have matching types. * cpp11_forwarding_ref_deduction — [temp.deduct.call]/3. Checks lvalue → T=A&, const lvalue → T=const A&, rvalue → T=A. Uses std::is_same hence gcc-only for now. * cpp11_variadic_pack_expansion — [temp.variadic]/5,7. Empty pack expansion (X<int> a(10)) and non-empty pack expansion (X<int,int,int> b(10,20,30)) in constructor templates. Exercises the pack-parameter removal / substitution paths in cpp_instantiate_template.cpp. Update STANDARD_COVERAGE.md to mark [expr.unary.noexcept] as ✅, link the new tests to [dcl.init.ref]/5, [temp.deduct.call]/3, and [temp.variadic], and refresh the Last updated line. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
library_check.sh enumerates regression/cbmc-library/ to build the list of expected test directories and cross-checks it against the library function table. The test runner (regression/test.pl) leaves a tests.log behind in that directory after a run, and on a subsequent cmake build the entry appears in __tests without a matching __functions line, aborting the build: --- __tests +++ __functions -tests.log Tests and library functions don't match. This reliably breaks out-of-tree Docker builds after the host has run the regression suite once. Extend the egrep exclusion to skip tests.log alongside Makefile and CMakeLists.txt. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Three more tests extend coverage of the standard annotations: * cpp11_temp_point_definition (CORE) — [temp.point]/1. Forward- declare a function template, then define it. CBMC must pick the definition (which has a body) over the forward declaration; otherwise the call site sees a nondet return and the assertions fail. Regression for 32110f7. * cpp11_value_init_scalar_brace (KNOWNBUG) — [expr.type.conv]/2 and [dcl.init.list]/3.10. T{} for primitive T should perform value- initialization and return zero. CBMC currently rejects this with "cannot initialize 'signed int' with an initializer list" at type-check time, producing a CONVERSION ERROR. Discovered while writing the [temp.point] test with a T{} zero-generator. * cpp11_deduct_funcaddr (KNOWNBUG) — [temp.deduct.funcaddr]. The implementation added by 18e8464 handles the std::endl use case where the target parameter is a class-template instantiation (e.g. basic_ostream<...>&). It does not yet handle the simpler case of deducing T=int from a plain function- pointer target type like 'int (*)(int, int)' against a template 'template <class T> int id_sum(T, T)'. Update STANDARD_COVERAGE.md entries for [temp.point], [dcl.init.list]/ 3.10 (new ❌), and [temp.deduct.funcaddr] (downgraded ✅ →⚠️ with notes). Link each new test to the relevant row. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Four more tests: * cpp11_temp_inst_implicit (CORE) — [temp.inst]/1. A class template is implicitly instantiated on demand: pointer-only uses work with an incomplete type, and member access / static member access trigger full instantiation. * cpp11_class_copy_ctor (CORE) — [class.copy.ctor]/1,7,8. Implicit copy constructor copies each subobject; user-defined copy constructor runs exactly once per copy-initialisation. Regression for 204a77d. * cpp11_new_delete (CORE) — [expr.new] + [expr.delete] non-array form. new T(args) calls the constructor and delete p calls the destructor exactly once. * cpp11_array_new_ctor_call (KNOWNBUG) — array form. new T[N] should call T's default constructor once per element, and delete[] should call the destructor once per element. CBMC neither calls the element constructors for T[N] (leaving them zero-initialised in effect) nor runs the destructors under delete[]; array new with a braced-init-list crashes with an invariant violation in op0() "Precondition: operands().size() >= 1". Discovered while writing the [expr.new] positive test. Update STANDARD_COVERAGE.md: downgrade [expr.new] to⚠️ with the array-form note and cross-link, and add the three new CORE tests alongside [temp.inst]/1, [class.copy.ctor], and [expr.new]. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
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.