pub enum Assumption {
Entered,
Approaching,
NoWrap(Chrec),
StrictOverflow,
}Expand description
Something that has to be true for a trip count to be the right answer.
Section 7.5 asks for exactly this: not a trip count but a trip count plus a predicate under which it holds, so the consumer either proves the predicate, emits a runtime check for it, or gives up. These are the predicates.
Variants§
Entered
The loop is entered at all, so the distance from the counter to its limit is a number that is not negative.
for (i = 0; i < n; i++) with n of zero runs no times and the distance is zero, but n
of minus one also runs no times and the distance is minus one, so a count taken from the
distance has to be told which case it is in.
What it does not say anything about is whether the loop comes back. A counter stepping
toward a limit under an ordering test either reaches it or is already past it, and either
way that is a finite number of steps, so a caller whose question is whether the loop ends
may have this one for nothing. crate::hoist discharges it by clamping the count at zero
and crate::loop_delete by never reading the count. That is the whole of why this is a
separate assumption from Assumption::Approaching rather than the same one worded to
cover both.
Only ever present on a symbolic count. When the distance is a number the sign of it is there to be read, so this is settled rather than assumed.
Approaching
The limit is somewhere the counter is heading, which for a loop ending on != is what
makes it end at all.
A counter stepping away from its limit never arrives, and one stepping past it keeps going until it wraps, so what is unproven here is termination rather than which number the count is. Nothing discharges it by clamping, because there is no number to clamp when the loop does not come back. Document 17.2 says rucc does not take out a loop that might not end, so a pass that deletes loops refuses this one outright.
Only ever present on a symbolic count, for the same reason Assumption::Entered is.
NoWrap(Chrec)
The induction variable does not wrap in its own type before the exit is taken.
Present whenever the increment did not carry the matching nsw or nuw flag. With the
flag there is nothing to assume, because the flag is the promise.
StrictOverflow
Signed overflow is undefined here, which is what makes for (int i = 0; i <= n; i++)
finite.
GCC infers loop bounds from this in infer_loop_bounds_from_signedness, and it is the
single most common source of a report that the compiler broke a working program. It is
recorded rather than assumed silently so that -fwrapv can withdraw the count and so that
a dump can name it.
Implementations§
Source§impl Assumption
impl Assumption
Sourcepub fn describe(&self) -> String
pub fn describe(&self) -> String
What it says, in a line, for a dump to print.
Section 7.5 asks that every inference of this kind be dumpable and say what it rests on, because a user who has been bitten by one deserves a command that tells them which line the compiler used against them. This is the sentence that command prints.