[Individual PRs to follow] C++ standard support: C++11 through C++26 parser, type-checker, and STL improvements#8878
Draft
tautschnig wants to merge 481 commits into
Draft
Conversation
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% 80.94% +0.39%
===========================================
Files 1707 1711 +4
Lines 189016 202627 +13611
Branches 73 79 +6
===========================================
+ Hits 152261 164017 +11756
- Misses 36755 38610 +1855 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
8f4e2d7 to
f3d208e
Compare
5cc8d28 to
980d519
Compare
980d519 to
883082a
Compare
…tion When a constrained class template partial specialization is selected, evaluate its requires clause by directly interpreting built-in type traits (__is_pointer, __is_integral, __is_signed, __remove_pointer). If the clause evaluates to false, fall back to a less constrained specialization or the primary template. Also include requires clause in class_template_identifier so that constrained specializations with the same argument pattern get distinct symbols. Promotes cpp20_concepts_ordering from KNOWNBUG to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…> member During elaboration of `std::chrono::duration<Rep, Period>`, MSVC's `<chrono>` header declares several operator overloads whose return type is `common_type_t<duration>`. This is a metafunction specialization keyed on the very class currently being elaborated, so its type cannot be resolved until duration itself is complete. Previously `typecheck_type` would throw on this unresolved reference, and the uncaught exception would abandon the rest of the class-body loop — silently dropping the remaining 15+ members (operator++, operator--, compound assignments, static zero/min/max accessors, and the private `_MyRep` data member). With `duration` elaborated this way, `cpp_constructor` later emitted "non-POD type has no constructor" / CONVERSION ERROR on any attempt to construct a duration value, tripping MSVC's chrono preprocessed-header tests. Narrow the fix to exactly this case: * Only when `symbol.name` matches `chrono::tag-duration<…>` (so broader mitigations do not mask genuine typecheck failures in unrelated template instantiations, where they would otherwise corrupt downstream shared irepts — observed breaking MSVC's `<filesystem>` preprocessed-header run). * Only when the offending member declaration type is itself `common_type<T>` / `common_type_t<T>` with `T` referring to `duration`. * On typecheck failure, `continue` rather than preserving the unresolved `cpp_name` — the later re-elaboration of the `duration` class instance (via `elaborate_class_template`) picks the member back up cleanly once `common_type<duration>` can resolve. Also soften the `PRECONDITION(cpp_is_pod(pod))` in `typecheck_side_effect_function_call`'s pod_constructor branch so that a partially-elaborated template instance that happens to reach this path falls back to an explicit typecast instead of crashing with an invariant violation. Effect: * MSVC `cpp14_chrono_basic` preprocessed-header run: CONVERSION ERROR → VERIFICATION SUCCESSFUL. * CORE Linux `cpp14_chrono_basic` and all CORE regressions remain green. * MSVC `<filesystem>` preprocessed-header runs regress (the additional duration members now elaborated expose a pre- existing latent issue in the system_error/xfilesystem_abi path); this is outside CI. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Mark `cpp14_chrono_basic` as fixed in CI_KNOWN_FAILURES.md and note the filesystem trade-off: the now-more-elaborated duration members expose a pre-existing latent crash in MSVC's `<filesystem>` preprocessed-header run. Both CORE filesystem tests continue to pass on Linux, so the trade-off is limited to manual MSVC preprocessed-header runs outside CI. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…guard
Several MSVC `<type_traits>` template aliases form SFINAE-guarded
mutual-recursion chains whose body re-resolves the same alias with
the same arguments. Canonical cycle:
add_rvalue_reference_t<T>
→ _Add_reference<T, void_t<T&>>::_Rvalue // pick specialisation
→ void_t<T&> // evaluate T&
→ resolves T // requires T's decl
→ re-enters add_rvalue_reference_t<T> // ← same args ← cycle
When T is a partially-elaborated class-template instance (observed
for `std::chrono::duration<...>` after commit 2e8e74f enabled
duration's full body to elaborate), CBMC's resolver has no
per-alias memoization and drives this into unbounded recursion.
The stack eventually overflows inside a `sharing_treet::detach()`
prologue — the SIGSEGV manifests at `mov %rdi,0x8(%rsp)` when
attempting to spill `this`, which is a stack exhaustion symptom
rather than a null-pointer deref.
Break the cycle deterministically: maintain a thread-local set of
`(base_name, full_template_args)` pairs currently being resolved.
A re-entry with the same pair returns `empty_typet{}` — the most
conservative placeholder that matches how `void_t<...>` composes.
Effect:
* MSVC `cpp17_filesystem_basic` and `cpp17_filesystem_path_ops`
preprocessed-header runs: stack-overflow SIGSEGV → VERIFICATION
SUCCESSFUL.
* Full MSVC preprocessed-header pass rate: 24/26 → 26/26.
* All CORE and KNOWNBUG regressions remain green.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Three weeks of targeted fixes on `cpp11-parser-rework-squashed` have uncovered a pattern: most fixes work around the same handful of architectural issues in different guises. This document steps back and argues for re-architecting three subsystems, with standard citations and concrete sites: 1. Class-body elaboration is eager and all-or-nothing — it should be lazy per [temp.inst]/3. 2. SFINAE context is implicit, encoded by 95 hand-rolled handler swap/catch patterns that independently try to implement [temp.deduct]/8's "immediate context" rule. Should be a first-class RAII type. 3. Overload resolution has no target-type propagation — the pipeline flows forward only, so [temp.deduct.funcaddr], [temp.deduct.conv], and brace-init-list matching each need the target type retrofitted via probe+retry. Should flow from callee to arguments on first pass. Secondary issues: template-alias memoization, POI tracking, two-phase name lookup, irep sharing discipline under template recursion. Includes a roadmap (short/medium/long-term), migration cost estimates, and validation criteria anchored on the dog-food metric (currently 10/117 = 8.5% OK_CLEAN, targeting ≥ 80%). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Consolidate the hand-rolled `null_message_handlert` + error-count
save/restore patterns that were scattered across the C++ front end
behind a single RAII primitive `sfinae_contextt` that explicitly
marks a SFINAE immediate context per N5008 [temp.deduct]/8:
> Invalid types and expressions can result in a deduction failure
> only in the immediate context of the deduction substitution
> loci.
The same semantics apply to [temp.constr.atomic], [temp.alias], and
the per-candidate substitution steps of [temp.deduct.call] and
[temp.deduct.conv]; all of those call sites can now opt in to the
primitive uniformly.
Construction:
* swaps the typechecker's `message_handlert` to a `null_message_handlert`
(silencing diagnostics emitted during substitution);
* captures the outer error count at entry.
Destruction (runs on normal exit *and* exception propagation):
* restores the previous handler;
* resets the error count to the pre-guard value.
This eliminates the ~20 independent hand-rolled variants that each
re-derived the same boundary (some with subtly different edge-case
behaviour — e.g. the P1-tail leak was "the guard was at the wrong
level"). Sites converted in this commit:
* cpp_typecheck_resolve.cpp per-candidate guess
* cpp_typecheck_template.cpp default-TYPE-template-arg + non-type default
* cpp_typecheck_function.cpp system-header body (std::optional-gated)
* cpp_typecheck_compound_type.cpp two constexpr-initializer sites
* cpp_typecheck_conversions.cpp user-defined template-ctor conversion
* cpp_typecheck_expr.cpp [expr.unary.noexcept] evaluation
* cpp_typecheck.cpp system-header item convert
* cpp_typecheck_namespace.cpp system-header namespace item
* cpp_instantiate_template.cpp specialisation-matching (2 sites),
concept-body evaluation (3 sites:
atomic constraint, requires-clause
param type, {type,simple,compound}
requirement), post-primary concept check
Every converted site carries an updated comment citing the specific
standard clause the guard implements ([temp.deduct]/8,
[temp.constr.atomic]/3, [expr.prim.req.{type,simple,compound}]/1,
[over.ics.user], [expr.unary.noexcept]/3).
Remaining `null_message_handlert` references in the tree are all in
comments that cite the primitive by name. The `errors_before`
save/restore pattern in resolve.cpp remains intentionally untouched
because its comment explicitly notes the null handler alters
error-count-dependent behaviour in that path; a separate audit will
revisit it as part of the medium-term SFINAE-return-type reshape.
All CORE + KNOWNBUG regressions green; MSVC preprocessed headers
26/26; lint + clang-format-15 clean.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Attempted step #2 of the short-term roadmap (replace the thread- local active-set with a real memoization cache per [temp.alias]/2) regressed three CORE tests (cpp11_deque_pushback, cpp11_string_default_arg_sstream, cpp17_deque_basic): CBMC's `irept`-level argument lists are *not* scope-agnostic — a `cpp_name` argument may resolve to different symbols in different class-body scopes, so two textually-identical `(alias, full_args)` keys can legitimately denote different result types. Revert to the minimal cycle-break (active-set only, from commit 09e5625), expand the comment to record the finding, and defer a proper scope-keyed memo to the medium-term lazy-elaboration work where the right scope anchor will be available alongside the rest of the elaboration machinery. Also pick up a clang-format touchup on cpp_typecheck_function.cpp from the preceding sfinae_contextt refactor. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Record the outcomes of the three short-term roadmap items: * Item 1 (SFINAE guard consolidation) ✅ landed (`7160102bc3`). * Item 2 (template-alias cache) 🟡 deferred — a scope-agnostic cache regressed three CORE tests; need scope-keyed memoization which belongs with the medium-term lazy-elaboration work. * Item 3 (shared-irep audit) ❌ hypothesis falsified. The two recent `detach()` SIGSEGVs traced to stack exhaustion and a null-deref, not shallow-copy races. §4.4 rewritten to reflect the actual findings. Net effect: 1 retired concern, 1 deferred with rationale, 1 hypothesis corrected. All CORE + KNOWNBUG regressions remain green; MSVC preprocessed headers still 26/26. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ntextt Three more SFINAE-semantic sites were using the error-count save/restore idiom in place of the `null_message_handlert` pattern. All three are immediate-context substitution points per N5008: * cpp_instantiate_template.cpp partial-specialization argument typecheck: [temp.inst]/1 + [temp.deduct]/8 — substitution failure in partial-spec matching is SFINAE, the candidate is discarded. * cpp_instantiate_template.cpp compound-member declarator typecheck during template instantiation: [temp.inst]/2 + [temp.deduct]/8 — a failed compound-member type-check means this member can't be completed but doesn't invalidate the enclosing specialization; bail out to the caller with the template symbol. * cpp_typecheck_code.cpp `if constexpr` branch-discard: [stmt.if]/2 — the discarded substatement is not instantiated, so a failure to elaborate it is semantically a SFINAE-like soft-failure; the if/else is replaced by `code_skipt`. Each site now uses `sfinae_contextt` and carries an updated comment citing the clause it implements. All CORE + KNOWNBUG regressions green; MSVC preprocessed headers 26/26; cpplint + clang-format-15 clean. Remaining `get_message_count(messaget::M_ERROR)` call sites in `src/cpp/` are either public API (error reporting in cpp_typecheck.cpp lines 372+406), already covered by the primitive itself (cpp_sfinae_context.cpp), or serve a different purpose (post-typecheck result queries rather than SFINAE probes). They are not part of this consolidation. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The P3a fix (commit 2e8e74f) hard-coded the `chrono::tag-duration<...>` class and `common_type_t<duration>` member-type patterns. On re-reading [temp.inst]/3: > The implicit instantiation of a class template specialization > causes the implicit instantiation of the declarations, but not > of the definitions, of the non-deleted class member functions … the standard already expects a compiler to be tolerant of incomplete member declarations during class-body elaboration. The "member type refers to a metafunction over the class currently being elaborated" pattern isn't duration-specific — it recurs in allocator::rebind, iterator_traits::difference_type specializations, and similar cases. Generalize the guard: * compute the current class's unqualified base name once from `symbol.name`; * detect any `cpp_name` in the member's type whose base matches the current class's base name (`ref_to_self`); * on typecheck_type failure, skip the declaration via the sfinae_contextt guard introduced in commit 7160102. This removes the hardcoded `chrono::tag-duration`, `common_type`, `common_type_t`, and `duration` string literals, and lets the same protection apply to any similarly-shaped pattern. Regression tests and MSVC preprocessed headers are unchanged (26/26 still green); dog-food `--expand` stays at 10 OK_CLEAN / 4 OK_NOISY / 103 FAIL. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Refactoring-only change (no behaviour change): extract the inline 80-line target-type-driven deduction blob from `typecheck_side_effect_function_call` into a named helper `deduce_function_address_args_from_target`. The helper is the principled shape the probe-and-retry should have had from the start: a clearly-scoped pre-pass that implements [temp.deduct.funcaddr]/1 against the outer callee's parameter types, with per-step comments tying each decision to the clause it is implementing ([conv.func]/1, [temp.deduct.type], [temp.deduct]/8). The separation makes three things easier: * The call site in `typecheck_side_effect_function_call` now reads as "forward-deduce function-address args, then typecheck the call as normal" — no longer an 80-line digression in the middle of the call-typecheck flow. * The helper's docstring makes explicit that it is a workaround for CBMC's "typecheck args before callee" pipeline, and will collapse into the main path once §3.3 target-type threading lands. * Future target-type-driven deduction cases (e.g. [temp.deduct.conv], [over.ics.list] brace-init-list matching) can sit alongside as peer helpers with the same standard- anchored structure. `cpp11_deduct_funcaddr` still passes as CORE; all CORE + KNOWNBUG regressions green; MSVC preprocessed 26/26. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Attempt to incrementally introduce lazy class-body elaboration by wrapping per-member typecheck in try/catch + skip-on-failure produced a net-negative dog-food trade-off (10 OK_CLEAN to 8): * Succeeds for the "typedef of unordered_map<...> followed by unrelated methods" pattern (string_containert). * Regresses for files whose OK status depended on the body loop exiting early at the first throw (e.g. validate_expressions.cpp). The learning: "errors emitted" is anti-monotone in "members registered", so this approach can't work as an incremental patch. The right shape is register-names-eagerly / resolve-on-use, which requires changing every caller of `components()` that expects fully-resolved types to go through a new `ensure_member_complete` helper. That's the 2-3-week refactor estimate and not amenable to incremental patching. Attempt reverted (no source changes landed). Documented in §6 so we don't repeat the experiment. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Pure formatting fix — from `a5a4b9f156`. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ecomp) Flesh out the medium-term items from cpp-frontend-review.md §6 into standalone, reviewable plans. Each plan contains: * Motivation anchored on measured dog-food / CI data. * Current state vs target state with specific file/function touches. * Phased migration (commit-level granularity) with per-phase regression gates. * Risk matrix and rollback strategy. * Explicit success criteria. * Dependencies and ordering relative to the sibling plans. The three plans are: 1. `cpp-frontend-plan-lazy-elaboration.md` — 5-phase refactor of `typecheck_compound_body` to register member names eagerly and resolve types on demand per [temp.inst]/3. Target: dog-food `--expand` from 10/103 to 50%+ OK_CLEAN; retire 4 accumulated narrow workarounds. 2. `cpp-frontend-plan-target-type-threading.md` — 6-phase introduction of a `target_typet` parameter to `typecheck_expr` covering [temp.deduct.funcaddr], [temp.deduct.conv], and [over.ics.list]/[dcl.init.list]. Retires the `deduce_function_address_args_from_target` probe-retry and the `typecheck_side_effect_function_call` 500+-line readability finding CI flagged on the 2026-05-13 push. 3. `cpp-frontend-plan-pr-decomposition.md` — tiered migration plan for landing the 465+ integration-branch commits onto `develop` as a series of reviewable PRs (Tier A infrastructure → Tier B focused bugfixes → Tier C harness → Tier D bulk history → Tier E future work). These are planning documents; no code changes. They explicitly reference one another and the parent review in §10 / "Dependencies and ordering" of each. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
bd209b4 added a `value.operands().empty()` zero-initializer path to do_initializer_list to support C++11 `T{}` value-initialization per [dcl.init.list]/3.10. That path also fired for C, where the empty initializer-list `{}` is a syntax error in C99/C11/C17 and only became valid in C23 ([dcl.init]/11). The unintended consequence: `regression/ansi-c/anonymous_member2/ not_permitted.desc` (CORE gcc-only, on develop since 2020 via 5d3e9a8) now silently succeeds when it expects a CONVERSION ERROR. Inside `struct c { struct a; void *d; }` initialised with `{ {}, 0 }`, the anonymous member is skipped per the matching front-end change, leaving `{}` paired with `void *d`. Pre- bd209b4 CBMC rejected this with "cannot initialize 'void *' with an initializer list"; post-bd209b448e it value-initialised the pointer to (void*)0 and reported VERIFICATION SUCCESSFUL, breaking 13 platforms in CI. Add a virtual hook `empty_brace_value_initializes_scalar()` on `c_typecheck_baset` that gates the empty-brace branch: * default implementation: true iff `config.ansi_c.c_standard >= configt::ansi_ct::c_standardt::C23` (matches C [dcl.init]/11); * `cpp_typecheckt` override: always true (C++ [dcl.init.list]/3.10 is a C++11 feature, but CBMC accepts it across all `--cppNN` modes for consistency with other permissive extensions). This restores the C-mode rejection that anonymous_member2 depends on while keeping the C++ value-initialization fix `bd209b448e` introduced. Local verification: * regression/ansi-c (goto-cc, gcc-only): 19 skipped, all green including anonymous_member2/not_permitted.desc and ./test.desc; * regression/cbmc-cpp (cbmc, libcxx excluded as CI does): 83 skipped, all green including cpp11_value_init_scalar_brace (the test bd209b4 was originally added for) and cpp11_temp_point_definition; * regression/cpp (goto-cc): all green, 7 skipped; * regression/cbmc (cbmc): all green, 49 skipped; * clang-format-15 clean; * cpplint via .github/workflows/pull-request-check-cpplint.sh clean (with the related findings in this commit-pair). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
CI's `check-cpplint` (run via .github/workflows/pull-request-check- cpplint.sh, which lints only diff lines against develop) flagged two findings on the 2026-05-13 push (HEAD bf79ab8): 1. src/cpp/cpp_typecheck_resolve.cpp:2797 readability/identifiers: `struct Guard` inside resolve_template_alias should be `guardt` per the CBMC naming convention (introduced by my 09e5625 active-set RAII guard for [temp.alias] mutual-recursion). Trivial rename. 2. src/cpp/cpp_typecheck_expr.cpp:3619 readability/fn_size: typecheck_side_effect_function_call() is 905 non-comment lines (threshold 500). Pre-existing largeness; my a5a4b9f target-type helper extraction pushed cpplint's diff window onto the closing-brace line. The principled fix for (2) is to split the function along its natural target-type boundaries (SystemC range handling, builtin dispatch, target-type-driven call resolution, per-argument conversion+rewriting) — this is already tracked as a §7 success criterion in `doc/architectural/cpp-frontend-plan-target-type- threading.md`, where the function decomposition falls out of threading the target type forward through typecheck_expr_main. Until that refactor lands, attach a `// NOLINT(readability/ fn_size)` to the closing brace and a documenting comment at the function head pointing readers to the plan. The NOLINT makes CI green; the comment ensures the lint suppression doesn't outlive the planned cleanup. Verified via `./scripts/run_diff.sh CPPLINT $(git merge-base origin/develop HEAD)`: 0 errors after these changes (was 1 fn_size + 1 readability/identifiers before). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
First commit of the target-type-threading refactor described in
`doc/architectural/cpp-frontend-plan-target-type-threading.md`.
Several C++ deduction and conversion paths require the typechecker
to know the *target type* of an expression while typechecking it,
rather than computing the operand's type in isolation and then
fixing things up after the fact. The standard requirements are:
* [temp.deduct.funcaddr]/1 — deducing template arguments when
taking the address of a function template;
* [temp.deduct.conv]/1 — deducing template arguments for a
user-defined conversion-function template;
* [over.ics.list] / [dcl.init.list] — initializer-list
arguments are matched against the target type.
Today CBMC works around this with the
`deduce_function_address_args_from_target` probe-retry helper
(commit a5a4b9f, refactored from d612fe6) and several
post-hoc `implicit_typecast` patches scattered through
`typecheck_function_call_arguments`. The probe-retry covers
[temp.deduct.funcaddr] only; [temp.deduct.conv] and
[over.ics.list] need a forward-driven approach.
This commit establishes the API surface without changing any
behaviour. It introduces:
* `src/cpp/cpp_target_type.h` — a non-owning `target_typet`
holding an optional `const typet *`. The default-constructed
instance carries no constraint and matches today's isolated
typecheck.
* a new overload
`cpp_typecheckt::typecheck_expr(exprt &, const target_typet &)`
that accepts a target but currently forwards to the existing
`typecheck_expr(exprt &)` and discards the target.
No call site passes a target yet; subsequent phases (1B internal
dispatch, 2 [temp.deduct.funcaddr], 3 retire probe-retry,
4 [temp.deduct.conv], 5 [over.ics.list]/[dcl.init.list], 6 audit)
add the threading and consumption.
Verified: full `regression/cbmc-cpp` CORE (libcxx excluded as CI
does) passes, 83 skipped, no FAILED. Build clean with
clang-format-15.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Second commit of the target-type-threading refactor. Adds
`target_typet`-taking forwarding overloads for the C++ front end's
per-kind expression handlers. Each new overload accepts a target
and currently discards it, calling the existing no-target
implementation; behaviour is unchanged.
Handlers updated:
* `typecheck_expr_main(exprt &, const target_typet &)`
* `typecheck_expr_address_of(exprt &, const target_typet &)`
* `typecheck_side_effect_function_call(
side_effect_expr_function_callt &, const target_typet &)`
These are the three per-kind sites where Phase 2 will start
consuming the target:
* `typecheck_side_effect_function_call` resolves the callee and
can pass each parameter's type as the target for the matching
argument's typecheck;
* `typecheck_expr_address_of` will use a pointer-to-function
target to drive [temp.deduct.funcaddr]/1 forward;
* `typecheck_expr_main` is the dispatch boundary that threads
the target down the operand recursion.
`typecheck_expr_initializer_list` lives only in the C base class
(`do_initializer_list`) and is not overridden in `cpp_typecheckt`;
its target-type integration is deferred to Phase 5
([over.ics.list]/[dcl.init.list]).
Verified: full `regression/cbmc-cpp` CORE (libcxx excluded as CI
does) passes, 83 skipped, no FAILED. Build clean with
clang-format-15.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Third commit of the target-type-threading refactor. Adds an optional `target_typet target` field to `cpp_typecheck_fargst` so the resolver can see the enclosing call's target without changing every `resolve` signature. The field is default-constructed (no target) and is not consumed by any code path in this commit; behaviour is unchanged. Phase 2 will add the producer side (`typecheck_side_effect_function_call` populating the field) and the consumer side (`resolve` and the deduction routines reading it for [temp.deduct.funcaddr]/1). Phase 4 will extend it to [temp.deduct.conv]/1. This completes Phase 1 of the refactor: API surface and threading points are all in place; subsequent phases land actual behaviour changes one consumer at a time. Verified: full `regression/cbmc-cpp` CORE (libcxx excluded) passes, 83 skipped, no FAILED. Build clean; clang-format-15 clean. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Mechanical refactor extracting the per-argument [temp.deduct.funcaddr]/1 deduction logic out of `deduce_function_address_args_from_target` into a new private helper `deduce_funcaddr_against_target(name_or_addressof, target_fn_pointer_type)` -> exprt. The new helper takes a single source argument (either a bare `cpp_name` or an `address_of` of one) and a target pointer-to- function type, runs the [temp.deduct.funcaddr] deduction with synthesised fargs, and returns either a typed `address_of` expression on success or `nil_exprt` on substitution failure (silent per [temp.deduct]/8). The existing iterating helper `deduce_function_address_args_from_ target` now calls the per-argument helper in a loop; the algorithm is unchanged. This separation enables Phase 2E to call the per-argument helper directly from the new target-typet-driven path (`typecheck_expr_address_of(exprt &, const target_typet &)` and `typecheck_expr(exprt &, const target_typet &)` for plain cpp_name arguments) without going through the iterating helper. Phase 3 then deletes the iterating helper. No behaviour change. Verified: full `regression/cbmc-cpp` CORE (libcxx excluded as CI does) passes, 83 skipped, no FAILED. `cpp11_deduct_funcaddr` (the CORE test that exercises this exact path) passes. Build clean with clang-format-15. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
… cpp_name
Wire the target-typet overloads of `typecheck_expr_address_of`
and `typecheck_expr` (introduced in Phases 1A/1B as no-ops) to
actually drive forward [temp.deduct.funcaddr]/1 deduction when
the target is a pointer-to-function and the source is a cpp_name
or `address_of(cpp_name)`.
* `typecheck_expr_address_of(exprt &, const target_typet &)`:
when expr is `&cpp_name` and target is pointer-to-function,
call `deduce_funcaddr_against_target` (Phase 2D helper). On
success, swap in the typed `address_of(specialisation)`.
* `typecheck_expr(exprt &, const target_typet &)`: when expr is
a bare `cpp_name` and target is pointer-to-function, do the
same. This handles the `f(template_name)` case where the
function-to-pointer is implicit per [conv.func]/1.
On failure (substitution failure or non-matching shape), fall
through to the existing isolated typecheck path so real
mismatches still surface as user-visible errors.
No caller passes a non-empty target_typet yet, so behaviour is
unchanged. Phase 2F switches `typecheck_side_effect_function_call`
from the iterating helper to the new forward path; Phase 3 then
deletes the iterating helper.
Verified: full `regression/cbmc-cpp` CORE (libcxx excluded as CI
does) passes, 83 skipped, no FAILED. Build clean with
clang-format-15.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…rward path
Switch `typecheck_side_effect_function_call` from the iterating
helper `deduce_function_address_args_from_target` to a forward-
driven loop that calls `typecheck_expr(arg, target_typet{ptype})`
for each deferred argument.
Also extend `typecheck_expr(exprt &, const target_typet &)` to
recognise the explicit `&cpp_name` argument shape in addition to
the bare `cpp_name`. Both shapes route to
`deduce_funcaddr_against_target` (the per-argument helper from
Phase 2D) on success; on failure they fall through to the
isolated path so real mismatches still surface as user-visible
errors.
The new producer loop mirrors the iterating helper's structure:
* probe the callee with empty fargs to obtain its parameter
types ([temp.deduct.funcaddr]/1 requires the parameter type
as the deduction target P);
* for each deferred argument (nil-typed by the deferred-typecheck
path in `typecheck_expr` ID_arguments branch), call
`typecheck_expr(arg, target_typet{params[i].type()})`.
The iterating helper `deduce_function_address_args_from_target`
is now unused at this call site (its only caller). It will be
deleted in Phase 3, in a separate commit so that this one is
purely a behavioural-equivalence refactor.
Verified:
* `cpp11_deduct_funcaddr` (the CORE test that exercises this
exact path) passes;
* full `regression/cbmc-cpp` CORE (libcxx excluded) passes,
83 skipped, no FAILED;
* full `regression/cpp` (goto-cc) passes, 7 skipped;
* full `regression/ansi-c` (goto-cc) passes, 19 skipped;
* dog-food `--baseline` (irep_hash.cpp gate) holds.
Build clean with clang-format-15.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…om_target
Delete the iterating helper
`cpp_typecheckt::deduce_function_address_args_from_target`. Its
sole call site (in `typecheck_side_effect_function_call`) was
switched to a forward-driven loop in Phase 2F. The per-argument
deduction logic that it used to contain now lives in
`deduce_funcaddr_against_target` (Phase 2D extraction), called
through `typecheck_expr(exprt &, const target_typet &)` from the
new producer in Phase 2F.
This completes Phases 2 + 3 of the target-type-threading refactor:
* 2D — extract per-argument helper;
* 2E — wire `typecheck_expr_address_of(target)` and
`typecheck_expr(target)` to call the helper;
* 2F — switch `typecheck_side_effect_function_call` from the
iterating helper to the new forward loop;
* 3 — delete the now-unused iterating helper (this commit).
[temp.deduct.funcaddr]/1 is now driven forward from the target in
the C++ front end, matching the standard's "deduce template
arguments from the target context" semantics rather than the
previous probe-then-retry pattern.
Also refresh the comment on `typecheck_side_effect_function_call(
exprt &, const target_typet &)` to reflect that it is now the
Phase-4 carrier for [temp.deduct.conv]/1, not a Phase-1B no-op
forwarder.
Verified:
* `cpp11_deduct_funcaddr` (the CORE test for this exact path)
passes;
* full `regression/cbmc-cpp` CORE (libcxx excluded) passes,
83 skipped, no FAILED.
Build clean with clang-format-15.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
First commit of Phase 4 ([temp.deduct.conv]/1). Adds a structural
carrier to thread the active target type from the
`typecheck_side_effect_function_call(exprt &, const target_typet &)`
overload through to the `cpp_typecheck_fargst` consumed by the
resolver and the user-defined-conversion code path.
Concretely:
* Add `std::vector<target_typet> call_target_stack` to
`cpp_typecheckt` — a per-instance stack of currently-active
target types for nested calls.
* `typecheck_side_effect_function_call(exprt &,
const target_typet &)` is no longer a no-op forwarder: it
pushes the target on the stack, calls the no-target body, and
pops on completion (with exception-safe cleanup).
* The no-target body's call to
`typecheck_function_expr(expr.function(), cpp_typecheck_fargst(expr))`
now reads the stack top into `fargs.target` before dispatch.
This commit only routes the target; nothing reads `fargs.target`
yet (Phase 1C added the field; Phase 4B will add the consumer in
`user_defined_conversion_sequence` for [temp.deduct.conv]/1).
No call site passes a non-empty target_typet to the overload, so
behaviour is unchanged.
Verified: full `regression/cbmc-cpp` CORE (libcxx excluded) passes,
83 skipped, no FAILED. Build clean with clang-format-15.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Stake out the [temp.deduct.conv]/1 implementation gap with a
targeted regression test before the implementation lands. The
test exercises a `template <class T> operator T() const` template
conversion operator on a struct, asserting that conversions to
`int` and `long` deduce T from the destination type.
CBMC's current `user_defined_conversion_sequence` rejects both
with `invalid implicit conversion from 'struct any_t' to ...`
because the function only iterates `components()` for non-template
cast operators; template ones are stored separately by
`convert_template_declaration` and never considered.
Marked KNOWNBUG with a detailed description in the test.desc
documenting the exact mechanism and pointing at the plan's Phase
4B for the implementation. Once Phase 4B's producer-side
tracking and consumer-side deduction land, the test promotes to
CORE in the same commit.
Also expand the Phase 4 section of
`doc/architectural/cpp-frontend-plan-target-type-threading.md` to
distinguish 4A (target carrier — landed in commit a62079307f) from
4B (actual deduction — pending), and break out the three
implementation pieces 4B needs:
* producer-side `has_template_conversion_operator` flag in
`typecheck_compound_body`;
* consumer-side deduction loop in
`user_defined_conversion_sequence` calling
`instantiate_template` with target type as deduction P;
* SFINAE wrapping per [temp.deduct]/8 and [over.ics.user].
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…on operators Producer-side step of Phase 4B ([temp.deduct.conv]/1). In `cpp_typecheck_compound_type.cpp::typecheck_compound_body`, when a template member declaration's type is `cpp-cast-operator`, set `has_template_conversion_operator` on the enclosing class. This mirrors the existing `has_template_constructor` flag set in the same block when the template member is a constructor. The flag is set but not yet read; Phase 4B-2 (forthcoming) adds the consumer in `cpp_typecheck_conversions.cpp::user_defined_conversion_sequence`, which looks up the source class's template conversion operators and instantiates each against the destination type as deduction target P per [temp.deduct.conv]/1. No behaviour change: producer-only. Verified: full `regression/cbmc-cpp` CORE (libcxx excluded) passes, 84 skipped (the new `cpp11_deduct_conv` KNOWNBUG test correctly skipped under -C), no FAILED. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ction
Implements the consumer side of Phase 4B: deduce template
arguments for a conversion-function template by matching the
template's return type (P) against the destination conversion-
type-id (A), per C++26 N5008 [temp.deduct.conv]/1.
Implementation:
* `cpp_typecheckt::deduce_conversion_template` (new helper in
`cpp_typecheck_conversions.cpp`):
- Checks the source class for the
`has_template_conversion_operator` flag (set by Phase 4B-1
in `cpp_typecheck_compound_type.cpp`).
- Walks the symbol_table for class-member symbols whose type
is a template `cpp_declaration` with `cpp-cast-operator`
inside.
- For each candidate, applies the [temp.deduct.conv] P/A
transformation rules:
* /2: P-reference -> use referred type;
* /3 (when A is not a reference): P array→pointer,
function→pointer, drop top-level cv from P;
* /4: A-reference -> use referred type, drop top-level cv
from A.
- SFINAE-wraps the deduction in `sfinae_contextt` and
try/catch per [temp.deduct]/8.
- Calls `cpp_typecheck_resolvet::guess_template_args(P, A)` to
populate the template_map, then
`template_map.build_template_args(decl.template_type())` to
extract the deduced argument tuple.
- Instantiates via `instantiate_template` (which adds the new
cast-operator component to the source class via
`typecheck_compound_declarator`).
- Builds the conversion call as a direct symbol_exprt-driven
`side_effect_expr_function_callt` (`cpp_symbol_expr` of the
instance + address-of source as `this` argument), bypassing
the cpp_name resolver.
- Validates the result via `standard_conversion_sequence`,
requiring rank == 0 per [over.ics.user]/3 (Exact Match for
the second standard conversion sequence after a template
specialisation).
- Returns false on ambiguity (multiple successful candidates)
— strict over-approximation pending implementation of
[over.match.best] partial ordering for conversion templates.
* `user_defined_conversion_sequence` (call site):
- After the existing non-template cast-operator loop, if no
match was found, calls `deduce_conversion_template` and
returns its result.
- The non-template loop now skips components carrying the new
`#is_template_specialization` marker so a previously-
instantiated specialisation cannot shadow a fresh deduction
for a different destination type
([over.ics.user]/3 + [over.match.conv]).
* `deduce_conversion_template` marks the freshly-instantiated
component with the marker so subsequent conversion attempts go
through deduction again rather than finding the previous
specialisation in `components()`.
Tests:
* `regression/cbmc-cpp/cpp11_deduct_conv/`: promoted from
KNOWNBUG to CORE. Exercises
`template<class T> operator T() const` with two distinct
destination types in the same translation unit (deduces
T = int and T = long).
* `regression/cbmc-cpp/cpp11_deduct_conv_ptr/`: new CORE.
Exercises [temp.deduct.conv]/3 with P = pointer-to-T and
A = `int*`.
* `regression/cbmc-cpp/cpp11_deduct_conv_cv/`: new CORE.
Exercises [temp.deduct.conv]/4 (top-level cv on A is ignored
for deduction).
* `regression/cbmc-cpp/cpp11_deduct_conv_undeducible/`: new
CORE. Verifies that [temp.deduct]/8 still applies — when T
cannot be deduced from the return type, the template is not
a candidate and the conversion is rejected.
Limitations (left for follow-ups):
* Reference-target conversions: `reference_binding` has its own
path that does not yet invoke `deduce_conversion_template`,
so `template<class T> operator T&()` deduction is not yet
exercised. [temp.deduct.conv]/2 (P-reference) would also
need the reference-binding entry point.
* Multiple competing template conversion operators (e.g.,
`operator T()` + `operator T*()`): currently flagged as
ambiguous and rejected. [over.match.best]/2 partial
ordering for conversion-function templates would let CBMC
pick the more specialised one; not implemented.
Verified:
* cbmc-cpp regression suite: all CORE tests pass (libcxx
excluded), 83 skipped (was 84 — the new CORE tests are now
running).
* regression/cpp baseline preserved: 258 pre-existing failures,
unchanged.
* cbmc regression suite: all CORE tests pass.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…ction templates
Implements [temp.deduct.partial]/3.2 + [over.match.best]/2 for
the case where two or more conversion-function templates of the
source class both deduce a viable specialisation for the same
destination type. Until now `deduce_conversion_template`
flagged this as ambiguity and rejected the conversion.
Concrete example:
struct any_t {
template<class T> operator T() const { ... }
template<class U> operator U*() const { ... }
};
int x = a; // only operator T() is viable: pick it.
int *p = a; // both templates deduce: T = int*, U = int.
// Partial ordering picks operator U*() because
// it is more specialised than operator T().
Implementation:
* New private member `conversion_template_at_least_as_specialised`
on `cpp_typecheckt` (declared in `cpp_typecheck.h`):
- Per [temp.deduct.partial]/2 + /8: deduces G's parameters
using F's pattern as the argument template (A) and G's
pattern as the parameter template (P). If G's parameters
all bind, F's type is at-least-as-specialised as G's.
- Per [temp.deduct.partial]/5 + /7: drops references and
top-level cv on both P and A before deduction.
- Per [temp.deduct.partial]/2 [Note 1] (transformed-type
substitution): in CBMC, F's and G's template parameter
symbols are disjoint by construction (different scope
prefixes), so F's parameters appearing in A are treated as
concrete by `guess_template_args` without an explicit
substitution pass.
- SFINAE-wrapped per [temp.deduct]/8.
* `deduce_conversion_template` refactored from a "deduce-and-
instantiate per candidate, bail on second success" loop into
three explicit phases:
- **Phase 1** (deduce-only): try [temp.deduct.conv]/1 deduction
for every template cast operator candidate, collect surviving
`(cand_sym, guessed_args, P)` triples without instantiating.
- **Phase 2** (partial ordering): when more than one candidate
survives, run the at-least-as-specialised pairwise check and
find the unique most-specialised one. Genuine ambiguity
(no unique winner) still returns false.
- **Phase 3** (instantiate winner): instantiate exactly the
chosen specialisation, build the call expression, and
enforce [over.ics.user]/3's Exact Match requirement on the
second standard conversion sequence.
This avoids polluting the symbol table with the side-effects
of losing candidates' instantiations, which mattered both for
cleanliness and for keeping the `#is_template_specialization`
marker meaningful.
Test:
* `regression/cbmc-cpp/cpp11_deduct_conv_partial/`: new CORE
test exercising the operator T() / operator U*() case. Both
the `int x = a` (single-viable) and `int *p = a` (partial-
ordering-disambiguated) paths must pass.
Verified:
* The new test passes.
* All existing cbmc-cpp CORE tests still pass (libcxx
excluded), 83 skipped.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
…on deduction
Implements [temp.deduct.conv]/2 + [over.match.ref] for the
case where the destination of an implicit conversion is a
reference type. Reference binding goes through `reference_binding`
rather than `user_defined_conversion_sequence`, so this commit
adds a parallel template-deduction entry point on the reference
path.
Concrete example:
struct holder {
int storage;
template <class T> operator T &() { return reinterpret_cast<T&>(storage); }
};
holder h;
h.storage = 42;
int &r = h; // deduces T = int via [temp.deduct.conv]/2 + /4
r = 99; // mutation visible in h.storage
Implementation:
* Refactored `deduce_conversion_template` to extract a shared
helper `find_template_conversion_specialisation(expr, to)`
that does deduction + partial ordering + instantiation. The
helper handles both value and reference destination types via
the existing [temp.deduct.conv]/2-/4 transformations:
/2 strips a reference from P;
/4 strips a reference from A and drops top-level cv from A;
/3 (drop cv from P, array→pointer, function→pointer) is
applied only when A is non-reference.
The helper also handles the parser-internal
`ID_frontend_pointer` representation used for as-yet-untyped
reference types (template cast operator return types come
from the parser unprocessed, with references encoded as
`ID_frontend_pointer + ID_C_reference`).
* Added `deduce_conversion_template_for_reference` wrapper that
calls the shared helper, validates the instantiated cast
operator returns a reference type per [over.match.ref], and
builds the conversion expression via
`add_implicit_dereference` + `reference_compatible` (mirroring
the non-template reference-conversion path in
`reference_binding`). Per [over.ics.user]/3, the
reference_compatible check must succeed without adding rank
beyond identity.
* Wired the new helper into `reference_binding` after its
existing non-template cast-operator loop. The non-template
loop now also skips components carrying the
`#is_template_specialization` marker, so a previously-
instantiated specialisation cannot shadow a fresh deduction
for a different reference type
([over.ics.user]/3 + [over.match.conv]).
Test:
* `regression/cbmc-cpp/cpp11_deduct_conv_ref/`: new CORE test
exercising `template<class T> operator T &()`. Verifies the
reference binds to the source object by mutating through the
reference and observing the change in the source.
Limitations (still open):
* When two reference-returning template cast operators on the
same class share their template-symbol identifier (CBMC's
`function_template_identifier` collapses both
`template<class T> operator T&()` and
`template<class U> operator U*&()` to the same name because
both have base_name "operatorfrontend_pointer" and an empty
function signature), the second is squashed into
`sfinae_alternatives` and is not reachable for direct
instantiation. This is a pre-existing CBMC limitation in
template-symbol naming, not a Phase 4B issue, and outside
the scope of this commit.
Verified:
* All cbmc-cpp CORE tests pass (libcxx excluded), 83 skipped.
* cpp baseline preserved: 258 pre-existing failures unchanged.
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
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.