;; The discharge rules.
;;
;; `spec/safe-memory/07-check-elimination.md` section 7.7 asks for every elimination of a safety
;; check to be data in a `safety/` namespace rather than a condition somebody wrote inside a pass,
;; and gives the reason: an unsound elimination produces a correct answer on every test and an
;; undetected vulnerability in production, and nothing observes it. A rule a solver has to agree
;; with before the build finishes is the only mechanism in the specification that catches that
;; class, and it only catches it if the rule is written before the pass rather than fitted to it
;; afterwards.
;;
;; These are not rewrite rules and this table is not matched against the IR. A pattern here is a
;; question, built by `crate::discharge` out of what its walk over the dominator tree has worked
;; out, and a rule that fires is the answer yes. That is why the kind is `discharge` and not
;; `simplify`: a table of these in the simplifier would be matched against instructions, and there
;; is no instruction here to match.
;;
;; # What is proved and what is not
;;
;; Section 7.7 splits it, and the split is the design rather than a shortcut. The walk that
;; establishes the context is ordinary code: which check dominates which, which pointer was
;; computed from which, and how far apart the two addresses are. Nothing here proves any of that,
;; and section 7.7 says as much, that the analysis is the weak point and that the differential
;; check accounting of section 14.3 is what covers it. What is proved is the step from the context
;; to the removal, which is the part that is arithmetic and is therefore the part a person gets
;; wrong quietly and stays wrong about.
;;
;; So the obligation a rule here discharges reads: given an access that has been checked, and a
;; second access a constant distance further along whose size the compiler has in hand as a number,
;; the second access's bytes are inside the first access's bytes. What the pass may then conclude,
;; and this step is document 07 section 7.3's rather than a rule's, is that a check which passed on
;; the first range cannot refuse the second, because a bounds check asks whether the bytes it is
;; about lie inside one storage instance and a subset of those bytes lies inside the same instance.
;;
;; The last rule in the file is about the other conjunct of the same check and so reads differently.
;; A bounds check asks where the bytes are and also asks whether the access starts where it says it
;; does, and the second of those is row S7 rather than row S1. The obligation there is that an
;; address the walk found a divisor of divides by what the access needs, and the split is the same
;; one: finding the divisor is the walk's and is not proved, and getting from it to the access's own
;; number is arithmetic and is.
;;
;; # Why the guard carries bounds that look unnecessary
;;
;; A guard is read twice. The compiler reads it in `i128`, where adding two byte counts does not
;; wrap, and the solver reads it in the sixty four bits the rule runs in, where it does. The two
;; agree while the numbers stay small and part company at the ends of the type, and a rule proved
;; under the solver's reading and run under the compiler's is a rule proved about arithmetic that
;; is not happening. So each distance and each size is bounded, at four gigabytes, which is past
;; any access a real program makes and far short of anywhere the two readings differ. An access
;; beyond it is not refused: it is not discharged, and its check stays.
;; A bounds check on bytes a dominating bounds check has already covered.
;;
;; `at` and `span` are the address and the size of the access that was checked, `delta` is how far
;; past that address the one being asked about starts, and `reach` is its size. The guard is
;; containment of one interval in another, in byte counts, which is the arithmetic the pass does.
;; The claim is containment of one byte range in another, in addresses, which is what document 07
;; section 7.3 writes the removal condition in. Proving that the first implies the second at sixty
;; four bits is the whole of what this rule is for, and it is not the guard said twice: an interval
;; inside another interval says nothing on its own about two address ranges, either of which could
;; run off the end of the address space.
(rule (discharge (covered.i64 (value.i64 at)
(iconst.i64 span)
(iconst.i64 delta)
(iconst.i64 reach)))
(if (and (>= delta 0) (<= delta 4294967296)
(>= reach 0) (<= reach 4294967296)
(>= span 0)
(<= (+ delta reach) span)))
(iconst.i64 1)
(spec (= (ite (or (bvugt at (bvadd at span))
(and (bvuge (bvadd at delta) at)
(bvule (bvadd (bvadd at delta) reach) (bvadd at span))))
1
0)
(result))))
;; A bounds check whose address is walked by a step the ranges bound, inside an object of a known
;; size.
;;
;; `at` and `span` are the address and the size of the object, which is either a local read off its
;; `alloca`, a global the module knows the extent of, or a range some earlier check established.
;; `delta` and `width` are the two ends of what the ranges said about the step, as the low end and
;; how much higher it can go, and `reach` is the size of the access. `step` is the distance the
;; program actually walks, and it is the one thing here the compiler does not have as a number.
;;
;; The guard is containment in byte counts again, of the far end of the range of accesses in the
;; object. What the rule adds is that the far end fitting is enough for all of them, which is the
;; step the pass would otherwise be taking on its own. It is the same addition the rule above makes
;; about a loop, and it is a separate rule for a reason worth stating: the loop's range starts at
;; the address that was checked, and this one starts wherever the program's arithmetic put the low
;; end of the step. Shifting the address along by `delta` to reuse the other rule would be doing
;; arithmetic on the claim inside the pass, which is what section 7.7 is written to stop.
;;
;; The bounds on the numbers are the file comment's, and they mean a range wider than four
;; gigabytes keeps its check. A step whose range is the whole of its type is exactly that case, and
;; it is the common one: an index nothing has bounded says nothing about where the access lands.
(rule (discharge (reached.i64 (value.i64 at)
(iconst.i64 span)
(iconst.i64 delta)
(iconst.i64 width)
(iconst.i64 reach)
(value.i64 step)))
(if (and (>= delta 0) (<= delta 4294967296)
(>= width 0) (<= width 4294967296)
(>= reach 0) (<= reach 4294967296)
(>= span 0)
(<= (+ delta (+ width reach)) span)))
(iconst.i64 1)
(spec (= (ite (or (bvugt at (bvadd at span))
(bvult step delta)
(bvugt step (bvadd delta width))
(and (bvuge (bvadd at step) at)
(bvule (bvadd (bvadd at step) reach) (bvadd at span))))
1
0)
(result))))
;; A bounds check inside a loop whose bytes one check in front of the loop has already covered.
;;
;; `at` and `span` are the address and the size of the check the pass is about to put in the
;; preheader, `far` is how far past that address the last iteration reads, and `reach` is the size
;; of the access inside the loop. `delta` is which iteration, and it is the one thing here the
;; compiler does not have as a number, which is the point: the rule is asked once and the answer
;; covers every iteration.
;;
;; The guard is the same containment in byte counts the rule above is guarded by, and it is the same
;; because it is the same question asked of the furthest iteration. What the rule adds is that the
;; furthest one fitting is enough for all of them, and that is the step the pass would otherwise be
;; making on its own with nobody checking it.
;;
;; The bounds on the numbers are there for the reason the file comment gives. Four gigabytes is past
;; the extent of any loop a real program writes and far short of where the compiler's `i128` reading
;; of the guard and the solver's sixty four bit reading part company. A loop that sweeps further
;; than that keeps its check.
(rule (discharge (swept.i64 (value.i64 at)
(iconst.i64 span)
(iconst.i64 far)
(iconst.i64 reach)
(value.i64 delta)))
(if (and (>= far 0) (<= far 4294967296)
(>= reach 0) (<= reach 4294967296)
(>= span 0)
(<= (+ far reach) span)))
(iconst.i64 1)
(spec (= (ite (or (bvugt at (bvadd at span))
(bvugt delta far)
(and (bvuge (bvadd at delta) at)
(bvule (bvadd (bvadd at delta) reach) (bvadd at span))))
1
0)
(result))))
;; The same, for a loop whose extent the program works out rather than the compiler.
;;
;; `span` and `far` are values here and not numbers. The pass that asks this has a trip count it
;; cannot evaluate, so it builds the two of them in the preheader out of that count and puts the
;; result on the hoisted check as an operand, and what it has to say about them can only be said as
;; a hypothesis inside the formula rather than as a guard on the numbers.
;;
;; The three hypotheses are the three things the pass promises about what it built. `far` and
;; `reach` added do not wrap, `span` is at least that sum, and `delta` is somewhere between zero and
;; `far`. The first two are what the pass establishes by bounding the arithmetic before it emits
;; any of it: the count comes from a value narrower than the arithmetic, the step and the reach are
;; numbers, and the largest the whole thing can be is worked out in wider arithmetic and refused if
;; it does not fit. The third is the same statement about which iteration as in the rule above.
;;
;; No four gigabyte limit, because there is no `i128` reading of these to part company with the
;; solver's. Everything about `span` and `far` that the pass knows is written above, and the
;; solver's arithmetic on them is the machine's.
(rule (discharge (swept.sym.i64 (value.i64 at)
(value.i64 span)
(value.i64 far)
(iconst.i64 reach)
(value.i64 delta)))
(if (>= reach 0))
(iconst.i64 1)
(spec (= (ite (or (bvugt at (bvadd at span))
(bvult (bvadd far reach) far)
(bvult span (bvadd far reach))
(bvugt delta far)
(and (bvuge (bvadd at delta) at)
(bvule (bvadd (bvadd at delta) reach) (bvadd at span))))
1
0)
(result))))
;; The same again, for a loop whose address walks from high to low.
;;
;; The mirror of the rule above and it is a mirror in every part, which is the point of writing it
;; this way round rather than as a rule about a negative step. `at` is the end of the first access
;; rather than its start, the object runs from `at - span` up to `at`, and the access on iteration
;; `delta` is the `reach` bytes ending at `at - delta`. Everything moves down where the rule above
;; moves up, and nothing else changes.
;;
;; The hypotheses are the same three and they are earned in the same places. `at - span` does not
;; wrap below zero, which is the mirror of `at + span` not wrapping above the top. `far` and `reach`
;; added do not wrap and `span` is at least that sum, which is what the pass establishes by working
;; the window out as `span - reach` and refusing when the subtraction leaves nothing. And `delta` is
;; somewhere between zero and `far`, which is the guard the pass carries round the loop.
;;
;; What follows is the two ends of the access. The low end is `at - delta - reach` and it is at or
;; above `at - span`, and the high end is `at - delta` and it is at or below `at`, which together
;; say the access is inside the object.
(rule (discharge (swept.down.sym.i64 (value.i64 at)
(value.i64 span)
(value.i64 far)
(iconst.i64 reach)
(value.i64 delta)))
(if (>= reach 0))
(iconst.i64 1)
(spec (= (ite (or (bvult at (bvsub at span))
(bvult (bvadd far reach) far)
(bvult span (bvadd far reach))
(bvugt delta far)
(and (bvule (bvsub at delta) at)
(bvuge (bvsub (bvsub at delta) reach) (bvsub at span))))
1
0)
(result))))
;; The alignment conjunct of a bounds check, for an address the walk found a divisor of.
;;
;; `at` is the address, `known` is what the walk over where the pointer came from worked out the
;; address is a multiple of, and `claim` is what the access needs. The guard is the test the pass
;; makes, which is that the claim is no larger than what is known, and the claim proved is that the
;; address is a multiple of the claim. Those two are not the same statement and that is the whole
;; reason this is a rule: being larger is being divisible by only for powers of two, and every
;; number that reaches here is one for a reason the head above writes out.
;;
;; The bounds on the numbers are the file comment's, and an alignment past four gigabytes is not a
;; thing a C program asks for. Zero is refused rather than bounded, because it is what the walk
;; answers with when it could read nothing and there is no address it says anything about.
(rule (discharge (aligned.i64 (value.i64 at) (iconst.i64 known) (iconst.i64 claim)))
(if (and (>= claim 1) (<= claim 4294967296)
(>= known claim) (<= known 4294967296)))
(iconst.i64 1)
(spec (= (ite (or (= known 0)
(= claim 0)
(not (= (bvand known (bvsub known 1)) 0))
(not (= (bvand claim (bvsub claim 1)) 0))
(not (= (bvand at (bvsub known 1)) 0))
(= (bvand at (bvsub claim 1)) 0))
1
0)
(result))))