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. 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. 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. That said - this should not end up prompting optimizer changes to make this "feature" work better. Instead I'd point to the -fanalyzer framework to implement such thing properly. 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. Richard. > > > Martin > >
