On Mon, Oct 26, 2026 at 10:27 AM Martin Uecker <[email protected]> wrote:
>
> Am Montag, dem 26.10.2026 um 09:59 +0100 schrieb Richard Biener via Gcc:
> > On Mon, Oct 26, 2026 at 9:52 AM Martin Uecker <[email protected]> wrote:
> > >
> > > Am Montag, dem 26.10.2026 um 08:40 +0100 schrieb Richard Biener:
> > > > On Sun, Oct 25, 2026 at 9:35 AM Martin Uecker via Gcc <[email protected]>
> > > > wrote:
> > > > >
> > > > >
> > > > > Hi all,
> > > > >
> > > > > I am experimenting with some hack that allows me to misuse
> > > > > GCC's optimizer in combination with certain sanitizers to
> > > > > prove specific safety properties statically.
> > > > >
> > > > >
> > > > > For example, the shift sanitizers can find the bug in
> > > > >
> > > > > uint8_t start = -1;
> > > > > uint64_t result = start << 24;
> > > > >
> > > > > (a real bug in a crypto library a long time ago), and
> > > > > the signed-integer-overflow sanitizer finds the missing
> > > > > error case in
> > > > >
> > > > > static int divide(int a, int b)
> > > > > {
> > > > > if (b == 0)
> > > > > error("divide by zero");
> > > > >
> > > > > return a / b;
> > > > > }
> > > > >
> > > > > and much more.
> > > > >
> > > > > A limitation of sanitizers is that they only find problems
> > > > > exercised in the tests or by fuzzing, they do not ensure
> > > > > that there are no remaining edge cases in the program.
> > > > >
> > > > >
> > > > > But there is a neat and simple trick on how to ensure
> > > > > (for small code snippets) that there is no such issue left.
> > > > >
> > > > >
> > > > > 1. Use certain UBSan sanitizers in trapping mode
> > > > > 2. Use optimization -O2
> > > > > 3. Add the following declaration:
> > > > >
> > > > > [[gnu::warning("UNSAFE")]] void __builtin_trap();
> > > > >
> > > > >
> > > > > This method then reliably pinpoints the remaining
> > > > > problems. See for yourself:
> > > > >
> > > > > https://godbolt.org/z/E9jqM53xr
> > > > > https://godbolt.org/z/3ov3GPM74
> > > > >
> > > > >
> > > > > What happens is that the sanitizer annotates the program
> > > > > with __builtin_trap() where there is a potential problem,
> > > > > while the optimizer then removes all traps it can show
> > > > > to be unreachable.
> > > > >
> > > > > The remaining ones are either real issues or false positives
> > > > > (cases where the optimizer can not see that the trap is
> > > > > unreachable). Those issue can then be fixed, annotated,
> > > > > or one can add explicit run-time checks or assertions.
> > > > >
> > > > >
> > > > > It does not work with all UB sanitizers (e.g. object-size
> > > > > only opportunistically adds bound checking where a bound
> > > > > is known) and sometimes there are also missing edge cases.
> > > > > But for many this works already very well and I find it
> > > > > useful.
> > > > >
> > > > >
> > > > > Similar ideas are also explored (or already used) by others,
> > > > > e.g. there is a related proposal for a "compile_assert" for
> > > > > manually added assertions
> > > > >
> > > > > https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3950.pdf
> > > > >
> > > > > or work by Anthropic that where they use Asan and then
> > > > > prove that the generated RISC-V code does not trap (but
> > > > > this then is conditional on the specifics of the generated
> > > > > code)
> > > > >
> > > > > https://www.anthropic.com/research/formal-verification
> > > > >
> > > > >
> > > > > Considering that this is already - by accident - working in
> > > > > a way that turns out to be useful, I think it would be cool
> > > > > if this could become a proper GCC feature.
> > > > >
> > > > >
> > > > > The nice thing is that this can be build on functionality we
> > > > > already have, and works together with the optimizer and not
> > > > > against it. The better the optimizer becomes, the more useful
> > > > > is this feature.
> > > > >
> > > > >
> > > > > The main issues I see is that there is currently no user friendly
> > > > > interface to this. A user friendly version for this should allow
> > > > > the user to selectively turn this on for some part of the code
> > > > > (because turning it on for a large program produces too
> > > > > many false positives) and also give the user some control over
> > > > > which properties are checked, while also limiting the features
> > > > > to specific sanitizers where it can work reliably. For example,
> > > > > I could then turn this on for a snipped of crypto code, where
> > > > > I want to make sure that there is no possibility for signed
> > > > > integer overflow.
> > > > >
> > > > >
> > > > > I could imagine a new pragma that turns this on and off
> > > > > similar to the diagnostic pragmas we currently already have
> > > > > (and perhaps using the same mechanism), possibly gated by a
> > > > > global command-line flag that ensures that it does not collide
> > > > > with any incompatible use of sanitizers or other features.
> > > > >
> > > > >
> > > > > I would like to work on such a feature, but I want to
> > > > > hear first what others think about this?
> > > >
> > > > Isn't this more-or-less what static analyzers do? I realize
> > > > you want to twist GCC to do sth similar.
> > >
> > > SA model checker such as cbmc can prove absence
> > > of undefined behavior, but cbmc is based on unrolling the code,
> > > forming statements to prove, and using a SMT solver to prove
> > > them. This is computationally extremely costly. For example,
> > > I started cbmc on coreutils's cat and it now already runs for
> > > a month and uses half a TB of memory ;-) (people tell me one
> > > has to break a program into small parts to use it effectively,
> > > which I haven't done)
> > >
> > > So the strategy is different. A model checker would not give up and
> > > tries to prove safety no matter what. I (also) want something which
> > > is fast and points to all potential issues (so can have no false
> > > negatives).
> > >
> > > Using the optimizer seems ideal for this, because the optimizer
> > > uses a set of very specific algorithms all written with a trade-off
> > > between computational cost and benefit in mind. And it is already
> > > really good at removing unreachable code.
> > >
> > >
> > > > So, if we'd want to
> > > > expose sth like your implementation idea I'd say we'd maybe
> > > > want a function attribute like
> > > >
> > > > [[gnu::diag_dynamic_sanitize]]
> > > >
> > > > that would diagnose any remaining dynamic sanitizing code
> > > > in a function [as late as possible]? There is some complication
> > > > from inlining, but I guess inlining into should be covered and
> > > > inlining such a function would only be more constrained, thus
> > > > a diagnosis free outline copy is good enough.
> > >
> > > I would prefer pragmas because this would allow me to mark-up code
> > > ranges on a fine level.
> >
> > Sure, but then this might punch holes into your "no false negatives"
> > approach because all the late (not in frontend) instrumentation code
> > is eventually prone to losing association to the original block/scope
> > that was marked, prompting "fixes" that I would not like to see.
>
> I see. We should use an attribute then for now.
>
> > Fixes not related to better optimizing but to hack in things similar
> > to that recently proposed tracking of
> > originally-CSEd-from-inline-copy-of-other-call
> > debug stuff for AFDO. I can see a UB earlier non-attributed shift
> > to be the prevailing expression for a later same attributed one
> > -> false negative and boom to your guarantee.
>
> Ok, but at least conceptually here is my counter argument
> (reality may disagree):
>
> What we are interested in detecting is source-level UB
> any (trapping) instrumentation done by a sanitizer for it to be
> correct and complete needs to be done early on all relevant source
> constructs before optimization. Any correct optimization can then
> not break this anymore.
Counter-example:
int foo (int a, int b)
{
int c = a + b;
#pragma GCC XXX
{
int d = a + b;
}
return (unsigned)c + (unsigned)d;
}
so you'd sanitize the computation of 'd' in the frontend, but
not that of 'c' (because, region). Optimizers will conclude
a + b doesn't overflow because ... the earier a + b would
invoke UB. The runtime sanitization is optimized away
and you have your false negative.
That means your #pragma would have to be an information
barrier of some sorts (but that also hides user written runtime
checks). Function boundaries are a working barrier for this,
more so if you put noipa on it and prevent inlining to avoid
the exact situation above. That is, I say it's way easier
to get what you want when not bothering with arbitrary
sub-regions.
> Where this is currently not the case, it is a deficiency of the
> sanitizer. So at least in the long run I think one should work
> towards this direction of moving sanitizer instrumentation into
> the frond-end (or early passes).
That I agree to. I think sanitizer instrumentations are reasonably
early (but after foldings, thus the many !sanitized checks there).
> (UB Sanitizers in diagnostic modes are a weird thing, the should
> emit a run-time diagnostic and then continue with a program
> that has UB. It is not clearly defined what this even means.
> I guess a clean way to implement this is to always transform
> the code during instrumentation into something thas has
> defined behavior. Then later passes would also not have to
> care at all.)
I agree. I'd just axe this "feature". A more modern way
would be to throw() so a sanitizer error can be catched
(maybe that already works?))
Richard.
>
> Martin
>
> >
> > > >
> > > > You'd use the attribute together with -fsanitize= or other
> > > > "sanitizers" (I'd say it should cover isolate-errorneous-paths
> > > > and other trap()/unreachable() inserters). The inserted
> > > > error calls/stmts can be marked so we do not mis-represent
> > > > user inserted traps.
> > >
> > > Yes.
> > >
> > > > That said - this should not end up prompting optimizer changes
> > > > to make this "feature" work better.
> > >
> > > I understand the concern. If we would add this I am sure
> > > we would get user requests to improve it.
> > >
> > > But any failure to optimize away an unreachable trap would also
> > > indicate some area where the optimizer could be improved
> > > in general also helping other code, so I am not entirely
> > > sure whether I would see it as a problem.
> > >
> > > > Instead I'd point to the
> > > > -fanalyzer framework to implement such thing properly.
> > >
> > > My understanding is that it is designed for a different
> > > task, not proving absence of UB. It works based on
> > > symbolic execution and therefor needs to be limited to
> > > avoid path explosion, and then has false negatives.
> > >
> > > But if this can be implemented as a mode for the analyzer,
> > > this is also something I would be interested in.
> > >
> > > Maybe David could comment on this?
> > >
> > >
> > > > So a more general attribute would be maybe
> > > > [[gnu::strictly_preconditioned]]
> > > > that asserts the user has everything checked and thus there are
> > > > no possible error paths in the function so we can [fatally] diagnose
> > > > any we find.
> > >
> > > Yes, I agree .
> > >
> > >
> > > Martin
> > >
> > > >
> > > > Richard.
> > > >
> > > > >
> > > > >
> > > > > Martin
> > > > >
> > > > >
