Comment #0 by qs.il.paperinik — 2023-06-16T16:51:42Z
Add a pragma with the identifier assume. It takes 1 argument that must be an expression convertible to `bool` and (depending on decisions) 1 optional additional argument that must be a string or multiple that are used to make a string.
The `bool` expression is not evaluated.
There are 2 ways to use `pragma(assume)`:
* `pragma(assume, x > 0);` The optimizer may freely assume that `x > 0` and use this information even backwards in time. (This is the strongest usage.)
* `pragma(assume, x > 0) NoScopeStatement` The optimizer may assume that `x > 0` in the code generation for the `NoScopeStatement`, which may be a single statement or a block statement. After the `NoScopeStatement`, the assumption must not be used anymore (except, of course, it was redundant and the information could be derived from elsewhere).
An example could be that a function with an unknown implementation is known by its specification to return non-negative values or -1 (an example is `indexOf`). After handling the `-1` case, its result is known to be non-negative.
It’s essentially impossible to provide real-world use-cases as they depend on the very details of the optimizer. C++23 formally added `assume` as an attribute as to streamline various compiler extensions.
Practically, an assumption should not be put in code unless profiling revealed that it made a difference. One reason is that assumptions cause undefined behavior (UB) if they’re violated.
For D, a consideration is `@safe`. A D compiler may definitely make use of an assumption in `@system` code as much as it wants; it may also make use of them in `@safe` code if either we accept it causing UB there (despite what `@safe` advertises, it’s an intentional loophole like `@trusted` is) or in cases where using the assumption leads to different code-gen without causing UB. A trivial example of the latter would be: `pragma(assume, x == 3) writeln(x)` Even if `x` is not `3`, replacing `writeln(x)` by `writeln(3)` does not constitute UB.
Comment #1 by elpenguino+D — 2023-06-16T17:34:24Z
I think assert(expr) could provide this functionality. Maybe with a -checkaction=assume switch? It would also work for contracts, invariants, etc then, while also making it trivial to test the assumptions.
Comment #2 by timon.gehr — 2023-06-16T20:28:40Z
`assert(expr)` does not fit the bill because it is `@safe`. -checkaction=assume can still happen in principle (as a similarly unsafe flag like -noboundscheck), but it's orthogonal.
Comment #3 by maxhaton — 2023-06-16T22:33:32Z
Should be an intrinsic or a UDA, pragmas are an anti-pattern.
Comment #4 by qs.il.paperinik — 2023-06-16T23:22:52Z
(In reply to mhh from comment #3)
> Should be an intrinsic or a UDA, pragmas are an anti-pattern.
Could you elaborate how it should look like?
I don't see how a UDA would work syntactically.
An intrinsic must be protected by `version` to ensure the compiler supports it.
How is a pragma an anti-pattern? Inline is a pragma.
In C++, it was an intrinsic, but every compiler had a different one, so in C++23, it became part of the standard so that it's not an intrinsic anymore.
Comment #5 by qs.il.paperinik — 2023-06-20T14:30:16Z
(In reply to elpenguino+D from comment #1)
> I think assert(expr) could provide this functionality. Maybe with a
> -checkaction=assume switch? It would also work for contracts, invariants,
> etc then, while also making it trivial to test the assumptions.
I’d say this is really bad design. An assertion and an assumption mean totally different things. With a compiler flag, you control all of them at once.
Just for an example, an assumption can be used to inform the compiler about a truth that its optimization routines can make use of and that its optimization routines could not figure out themselves.
An assert might be used to validate function input, e.g. `isPrime(int x)` might `assert(x > 0)`.
Comment #6 by elpenguino+D — 2023-06-20T15:31:39Z
(In reply to Bolpat from comment #5)
> (In reply to elpenguino+D from comment #1)
> > I think assert(expr) could provide this functionality. Maybe with a
> > -checkaction=assume switch? It would also work for contracts, invariants,
> > etc then, while also making it trivial to test the assumptions.
>
> I’d say this is really bad design. An assertion and an assumption mean
> totally different things. With a compiler flag, you control all of them at
> once.
>
> Just for an example, an assumption can be used to inform the compiler about
> a truth that its optimization routines can make use of and that its
> optimization routines could not figure out themselves.
> An assert might be used to validate function input, e.g. `isPrime(int x)`
> might `assert(x > 0)`.
An assertion is just an enforced assumption. They both mean the same thing.
assert():
- code following is optimized with the assumption that the condition is true
- undefined behaviour if condition is false
pragma(assume):
- code following is optimized with the assumption that the condition is true
- undefined behaviour if condition is false
It is legal for assert() to influence the optimizer without actively checking the condition, and this proposal would also allow a compiler to actively check and enforce the condition in pragma(assume) - it is undefined behaviour, and it might be useful to prove your assumptions while debugging.
Enabling assertions to be treated as unchecked assumptions additionally allows for invariants and contracts to influence optimizations, though current compilers don't appear to be capable of optimizing invariants...
Comment #7 by timon.gehr — 2023-06-20T15:50:52Z
(In reply to elpenguino+D from comment #6)
> (In reply to Bolpat from comment #5)
> > (In reply to elpenguino+D from comment #1)
> ...
> An assertion is just an enforced assumption. They both mean the same thing.
> ...
They are dual. An assertion is a proof obligation, an assumption is an axiom.
It's more obvious in a verifier. Standard definitions in Hoare logic:
{ P ∧ Q } assert(P) { Q }
{ Q } assume(P) { P ∧ Q }
In D, `assert` is `@safe`, `assume` has to be `@system`. You can't do hard optimizations based on unchecked assumptions (in particular in `@safe` code) while following the D specification, any flag that does so deviates from the specification of `@safe`. This is why this enhancement is important, it enables actually giving `@trusted` optimization hints in a sound manner.
Comment #8 by robert.schadek — 2024-12-13T19:29:42Z