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. 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. > > > > 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 > > > > > >
