Module ops 

What an operation does to a range, forwards and backwards.

Design: spec/optimizer/10-value-ranges.md, sections 10.4 and 10.7. Section 10.4 calls this a table with an entry per opcode, and says the M4 subset is addition, subtraction, multiplication, the bitwise operations, the shifts, the comparisons, truncation, sign and zero extension, and negation. Not division, not remainder, not the overflow builtins, not the intrinsics: those are cheap to add later against the same tests and expensive to get subtly wrong now.

Forwards and backwards

Forwards is the easy direction and the one everything else is built on: given what the operands can be, what can the result be. add and the rest of the free functions here are that.

Backwards is the direction the on-demand query needs, and it is the whole reason a branch teaches the analysis anything. On the true edge of if (x < 10), the fact is not about the comparison’s result, it is about x, and getting there means running the comparison inverse: given that x < y holds and given what y can be, what can x be. narrow_for is that, and it is the one inverse that pays for itself on nearly every branch in nearly every function. backward is the rest, for the operations whose inverse is exact and cheap, and it says so when there is no inverse worth having rather than pretending.

Wrapping is an argument and not a check somewhere else

Section 10.7 names this as the way a range implementation gets a program wrong. [100, 200] + [100, 200] in eight bits is not [200, 400], and in a signed type without -fwrapv the optimizer may assume the overflow did not happen, which is a stronger fact and a different answer. So every operation that can overflow takes Flags, the same NSW and NUW the instruction carries, and there is no way to call one of these and forget. A range computed under one assumption and used under the other is a miscompilation, and the only defence against that is not having a version of the function that does not ask.

What the flags buy is the clamp. Without them the answer is the wrapping one, exact modulo 2^width. With NSW the sums that do not fit cannot have happened, so the answer is intersected with the ones that do, and if none of them fit the range is empty, which is the analysis proving the code is unreachable.

Sound, and then as sharp as there is room for

Every function here returns a range that holds every value the operation can actually produce. That is the property the tests check exhaustively at width three and four, and it is the one whose failure is a wrong program. Holding more than that is precision loss, which costs speed and not correctness, and it happens for two reasons: an answer that needs more than super::PAIRS intervals, and an operation whose exact answer is not worth computing. Both are marked where they happen.

Enums

Truth

Whether a comparison is settled, and which way.

Undo

Which operation an inverse is being asked for.

Functions

add

The sum, modulo the width, and narrowed by whatever the flags promise.

and

The bitwise and.

ashr

The value shifted right by the count with the sign bit coming in.

backward

What the operand must have been for the operation to have produced this.

compare

Whether the ranges settle the comparison.

lshr

The value shifted right by the count with zeroes coming in.

mul

The product, modulo the width, and narrowed by whatever the flags promise.

narrow_for

What the left operand can be given that the comparison holds.

neg

Zero minus it, modulo the width, and narrowed by whatever the flags promise.

not

The bitwise complement, which is exact: it reverses each interval and nothing else.

or

The bitwise or.

sext

It at the wider width with the sign bit on top.

shl

The value shifted left by the count, modulo the width.

sub

The difference, modulo the width, and narrowed by whatever the flags promise.

trunc

The low bits of it, at the narrower width.

xor

The bitwise exclusive or.

zext

It at the wider width with zeroes on top, which keeps every interval as it was.