This paper describes the design and an implementation exploration for symbolic contracts: contract assertions whose predicate has, by default, no run-time representation at all, and whose truth is instead established and consumed purely by the compiler's own static reasoning about the program. We explain what a symbolic function is, the escape hatch for predicates that are known to be unprovable in context, how the static analysis of symbolic contracts relates to the concerns raised in P3362, and, perhaps counterintuitively given the "no run-time representation" framing, how symbolic contracts also support an entirely optional, opt-in run-time checking mode that works across translation units.
P3362, "Static analysis and 'safety' of Contracts, P2900 vs. P2680/P3285", argued, alongside P2680 and P3285, that the Contracts MVP (P2900) should be changed to incorporate a stricter flavor of contract, one for which the committee could make stronger safety guarantees than ordinary contracts provide. EWG polled that direction in November 2024 and the result leaned against changing the MVP itself: 10 SF, 6 F, 3 N, 14 A, 16 SA. The largest single bucket was "strongly against".
That poll is not revisited here. This paper does not ask for the language's ordinary contracts to become stricter, nor for the MVP to be reopened. Instead, it explores a different, additive route to much of the same underlying motivation: can a programmer, today, obtain contracts that a compiler can actually verify, rather than merely check at run time? Symbolic contracts are entirely separate from, and compose with, ordinary contracts; adopting them requires no change whatsoever to what P2900 already specifies.
P2680 asked for contract predicate evaluation to be free of side effects and free of undefined behavior, as seen from outside its own "cone of evaluation". A symbolic contract satisfies both properties unconditionally, not as a rule the programmer must follow when writing the predicate, but as a structural consequence of the predicate not being written at all - see below.
A symbolic function is declared with a new context-sensitive
keyword, symbolic, in place of a function body. A
symbolic function has no definition, anywhere; attempting to define
one is ill-formed. It exists purely to be named, as a predicate, from
within a contract.
struct io_facility { bool is_opened(io_facility*) const symbolic; void open() post<symbolic_assert_v>(is_opened(this)); void write_data(span<char> buffer) pre<symbolic_assert_v>(is_opened(this)); };
is_opened is not backed by a bit anywhere in
io_facility. There need not be a bit for it to be backed
by: whether a facility is "opened" is exactly the kind of logical,
per-object state that a class's authors reason about constantly but
that has no single canonical bit-level representation, especially
once the facility wraps a file descriptor, a handle, a half-open
connection, or nothing at all until first use. A symbolic function
lets that state be named and reasoned about without inventing a
representation for it, and without the invented representation itself
becoming one more thing that can be constructed incorrectly, go
stale, or be read before it is written.
A symbolic member function must be const, with no other
qualifier. A predicate never changes the state it describes, and an
overload differing in qualification would be a different predicate,
with facts of its own: requiring const means the contracts
of a const and a non-const member function
name the same one.
A contract control object opts in to this facility by declaring an additional static member:
static constexpr bool is_symbolic(const assertion_static_info&);
The library's std::contracts::symbolic_assert_v, used
in the example above, is such a control object. A control object that
does not declare it is treated as not
symbolic, exactly as a control object predating is_conveyor
is treated as not conveyor. A pre or post
that names a symbolic control object is a symbolic contract. By
default, the compiler generates no run-time code for it at all: no
predicate wrapper, no invocation of the control object's
operator(). The compiler does, however, keep the contract
for the static analysis described next. That analysis can run on the
front end's syntax trees or on GIMPLE, GCC's intermediate
representation (see the companion paper on strict contracts,
P4423R0); for the
latter, a marker records where in the function the contract is, and the
analysis removes it once done, so the generated code is the same either
way.
Symbolic contracts are checked by a dedicated, opt-in static analysis, requested with a flag analogous to the one already used for the proof-based analysis of UB-freedom:
-fcontract-symbolic-proofs
This checks, for every symbolic precondition, that it is established by an earlier call's own symbolic postcondition on the same object, and that the established fact has not been invalidated since - either by reassigning the object, or by any other call that takes its address. Each obligation reaches one of three outcomes: proven (silently discharged), proven false (a hard error, since this is a confirmed contradiction, not a mere absence of proof), or left unknown (a warning, since the code may still be correct at run time even though the analysis could not establish that from what it can see).
The invalidation rules are deliberately the same ones already used
for the UB-freedom analysis performed on ordinary, run-time-backed
"conveyor" contracts: a symbolic fact about an object is invalidated
by the same operations that invalidate a conveyor fact about that
object, re-established by the same kind of operation that
re-establishes one. Symbolic contracts are not conveyor contracts -
they promise nothing at run time, where a conveyor postcondition
genuinely holds when execution reaches it - but they reuse the same
notion of what it means for a fact about an object to remain live
across statements, calls, and branches. Calling
write_data before open is rejected not
because some bit was read and found false, but because no
symbolic postcondition establishing is_opened(this) is
live at that program point, by the same reasoning that would reject a
conveyor-checked use of an invalidated pointer.
A symbolic postcondition is itself checked against the body of the
function that declares it, conjunct by conjunct. A call of a symbolic
function can't be checked - there is no body to check it against -
so it is trusted, as the axiom it is: open is taken at its
word that it establishes is_opened(this). Any other
conjunct, such as a range of a member (m_value >= 0.0),
is proven from the function's body, as a conveyor postcondition's
would be, and an unprovable one is reported. A symbolic
contract_assert is not an axiom:
contract_assert<symbolic_assert_v>(is_opened(f)) claims
something about state that earlier code must have produced, so, like a
precondition, it must be established by an earlier symbolic
postcondition, and is reported otherwise. To assert such a fact without
proof, the assertion uses never_proven_symbolic_v, which is
trusted and establishes it.
This analysis is, by construction, confined to a single translation unit: it reasons about the calls, assignments, and branches that are actually visible in the function being analyzed. That scope is exactly what the next section's run-time layer exists to extend.
Some symbolic facts are established in contexts the static analysis
cannot usefully reach at all - deep in generic code, across a
boundary the analysis does not cross, or simply in code whose
correctness here relies on an invariant established far away in a way
no local analysis is going to reconstruct. For exactly this situation
there is a second, "never-proven" flavor of a symbolic control
object, std::contracts::never_proven_symbolic_v,
mirroring the already-existing never_proven_conveyor_v
used by the library's own internal, defensive assertions. A
pre or post written against this control
object is exempt from ever being checked against the ambient static
facts - no "cannot verify" warning, no contradiction error, ever -
while still establishing itself as a trusted fact for whatever code
follows, exactly as an ordinary symbolic postcondition would. It is
the symbolic-contract equivalent of telling the analysis "trust me
here", scoped to exactly the one assertion that needs it, rather than
disabling the analysis wholesale.
It would be reasonable to assume that a mechanism explicitly designed to have "no run-time representation" is static-analysis-only by definition. It isn't. Once a symbolic fact has no user-written predicate body to go wrong, the compiler is in a position to generate a run-time check for it that a programmer's own incorrect implementation could never have undermined - because there is no programmer-supplied implementation at all. This is requested with a second, independent flag:
-fcontract-symbolic-runtime-checks
With this enabled, a symbolic postcondition, at run time, records
that it was established - associated with the object it was
established for (this, or whichever object the
predicate's argument denotes). A symbolic precondition, at run time,
consults that record, via the control object's operator(),
exactly as an ordinary contract would invoke it - rather than ever
evaluating the original predicate expression directly, which for a
symbolic function is not even possible, since the function has no
body anywhere to evaluate. The record is shared across translation
units and across threads: a postcondition establishing
is_opened(this) in one TU can be consulted by a
precondition checking it in a completely different TU, for the same
io_facility*.
That cross-TU reach is the real distinction between this layer and
everything described above it. The static analysis in the previous
section is a single-TU, compile-time proof; this is a run-time record
that outlives any one TU's view of the program, the same way the
object itself does. The two are independent of each other -
-fcontract-symbolic-proofs and
-fcontract-symbolic-runtime-checks may be used
separately or together - because they answer different questions.
The static analysis answers "does this translation unit's own code
already guarantee this symbolic fact holds here?" at compile time,
for the calls it can see. The run-time layer answers "did some call,
anywhere in the program, actually establish this fact for this
object?" at the one place and time that matters: the call that is
about to rely on it.
A fact outliving any one TU's view of the program must not outlive the object it was established for: a later, unrelated object that happens to reuse the same address - most commonly two sequential, non-overlapping automatic objects at the same stack offset, or a heap allocation reusing freed storage - would otherwise inherit a fact it never established itself. So the record follows the object's lifetime, for an object of any type that has a class declaring a symbolic predicate anywhere inside it: the object's own class, a base, a member, or an array element.
io_facility, whose destructor
is trivial, needs no destructor of its own, and its triviality,
visible through std::is_trivially_destructible and to
the ABI, is unchanged. The implementation uses the machinery
destructor calls already use: a cleanup run on every exit from the
scope, and on the exception path only when something in the scope can
throw.new, and so an
allocator's construct, included - clears them before
constructing. Storage reused without its previous objects' lifetimes
visibly ending, such as a container's or a pool's, doesn't pass their
facts on.memcpy, memmove and memset
create the objects they write anew: writing one of these objects
through them clears its records too.A class declaring a symbolic predicate also clears the records for
this when its destructor begins - the point the
implementation already treats "this object is no longer of a
more-derived type" as taking effect for virtual table pointers - which
covers an explicit destructor call on an object whose storage is then
reused.
Both require -fcontract-control-objects, the same
prerequisite ordinary contract control objects already need; neither
introduces a new dependency beyond that.
P3362 asked the committee to make the language's contracts stricter, as a single, uniform property of the facility, so that programmers (and the tools reasoning about their code) could rely on that strictness everywhere contracts are used. EWG's response was, in effect, that this is not a property the committee is currently willing to impose on contracts in general.
Symbolic contracts take the opposite shape: strictness is not a
property of contracts in general, it is a property a programmer can
buy, one declaration at a time, by writing symbolic
instead of a body, and by opting a specific precondition or
postcondition into a symbolic control object instead of an ordinary
one. Nothing about ordinary, run-time-checked P2900 contracts changes.
What's added is a second, narrower facility that happens to satisfy,
for the contracts that use it, much of what P3362 and P2680 were
actually after: a predicate that is unconditionally free of side
effects and undefined behavior (because it has no body to have
either), and whose truth the compiler - not just the running
program, at one specific moment - can be asked to establish. Where
P3362 would have made that a mandatory property of contracts broadly,
symbolic contracts make it an available property of the specific
contracts a programmer chooses to mark this way, which is a
materially easier thing for EWG to evaluate than a change to the
already-adopted MVP's baseline semantics.
The design is implemented in a GCC branch: the symbolic
specifier, is_symbolic on contract control objects,
-fcontract-symbolic-proofs's static analysis (in both of
the implementation's analysis engines, which agree on all of its
tests),
-fcontract-symbolic-runtime-checks's cross-TU record, and
the lifetime-based clearing of that record described above. The predicate
named by a symbolic contract's condition can be a free function, a
static member function, or a non-static member function, whose object
is either left implicit (is_opened()) or, as in this
paper's examples, also passed explicitly
(is_opened(this)). What it can't currently be is a
relation between two objects: a non-static member predicate given a
different object than its own (is_linked(other)), or a
predicate taking more than one object. The static analysis reports a
precondition like that as unverifiable, saying why, and
-fcontract-symbolic-runtime-checks rejects the contract;
see the To do section.
The examples below are runnable on Compiler Explorer with the
"x86-64 gcc (P4324 contracts, and profiles)" compiler, using
-std=c++26 -fcontracts -fcontract-control-objects
-fcontract-symbolic-runtime-checks:
main:
each one's io_facility is an automatic object at the
same stack address, with a trivial destructor, and the second
function's violated precondition is caught:
https://godbolt.org/z/TsGq3ae3xnew in a
pool's storage, never destroyed: the new object starts without the
old one's fact, and the precondition of its write is caught:
https://godbolt.org/z/M5eEeoKr7To be supplied.