pub struct Bound { /* private fields */ }Expand description
How many times a loop runs at most, and what that rests on.
For correctness. A pass that deletes an iteration, peels one off, or decides a memory access is in bounds needs one of these. The count cannot be read without the assumptions, which is section 7.7’s defence against a caller proving two of three and forgetting the third.
Implementations§
Source§impl Bound
impl Bound
Sourcepub fn parts(&self) -> (Count, &[Assumption])
pub fn parts(&self) -> (Count, &[Assumption])
The count and everything it rests on, together, because they cannot be asked for apart.
Sourcepub fn reading(&self) -> Reading
pub fn reading(&self) -> Reading
How the value a symbolic count is built out of has to be read.
Meaningless on a count that is a number, since a number has already been read.
Sourcepub fn assumptions(&self) -> &[Assumption]
pub fn assumptions(&self) -> &[Assumption]
What has to be proved before the count means anything.
Sourcepub fn proven(&self) -> Option<Count>
pub fn proven(&self) -> Option<Count>
The count, for a caller with nothing left to prove.
None does not mean the count is unknown. It means there are assumptions and this is not
the accessor for reading a count that has them.
Sourcepub fn under_undefined_overflow(&self) -> Option<Count>
pub fn under_undefined_overflow(&self) -> Option<Count>
The count, for a caller compiling a language where signed overflow is undefined.
Bound::proven answers nothing for any for (int i = 0; i < n; i++) in any C program,
because solve puts Assumption::StrictOverflow on every count taken from a signed
test, and a pass built on proven alone is a pass that never fires. What that assumption
says is that the count rests on signed overflow being undefined, and -fwrapv is
implemented in rucc-lower by not setting nsw rather than by a flag anything down here
reads. So an increment that still carries nsw under -fwrapv does not exist, and a bound
with StrictOverflow and nothing else on it is a bound whose counter the front end
promised does not wrap. That promise is exactly what the assumption wanted.
Assumption::NoWrap is the case where there is no such promise, and it is refused here.
So is Assumption::Approaching, though only in passing, because it never appears on a
count that is a number.