;; What the terms in the safety rules mean.
;;
;; The IR half is the one account of the IR that every rule set is read against, so it is included
;; rather than repeated. What is added here are heads rather than instructions. The first is the
;; question the discharge pass asks about two checks its walk has already worked out are about one
;; address a fixed distance apart. The second is the question the hoist pass asks about a check
;; inside a loop whose address the walk has worked out is somewhere in a known range. The third is
;; the same question the discharge pass asks when the walk got past a step it could not read and
;; what it has is a range of distances rather than one. The next two are the question the split pass
;; asks about a loop whose extent is a value the program works out rather than a number, once for a
;; walk that goes up and once for a walk that goes down. The last is the alignment half of a bounds
;; check, which is a different question about the same address and is asked of the same pass.
(include crates/rucc-ir/rules/ir.model)
;; Whether the bytes one access reads are inside the bytes another access reads.
;;
;; `at` is the address the access whose check has already happened reads from, and `span` is how
;; many bytes it reads. `delta` is how far past that address the access being asked about starts,
;; and `reach` is how many bytes that one reads. Both sizes are byte counts, because that is what
;; the payload a check carries holds, and `delta` is a byte count for the same reason: `ptr_add`
;; takes bytes.
;;
;; It answers one when the later access's bytes are inside the earlier access's bytes, and that is
;; the whole of what may be concluded from a check that passed. A check that passed does not say
;; where the object starts or how big it is. It says the bytes it was about are inside some one
;; storage instance, and document 07 section 7.3 writes the removal condition against exactly that:
;; an established range, and a later range contained in it.
;;
;; The first disjunct is an assumption, and it is written where it can be read rather than left
;; out. An access whose byte range runs off the top of the address space and wraps round to the
;; bottom is not inside anything in the containment order, so the claim would be false for one. No
;; such access exists: the allocator hands out storage instances that do not wrap, per document 05,
;; and an access that passed a bounds check is inside one of them. Writing it as a disjunct rather
;; than leaving it unsaid is what makes it something a reviewer can disagree with, and the pass
;; leans on it in the same words.
(semantics (covered.i64 at span delta reach)
(ite (or (bvugt at (bvadd at span))
(and (bvuge (bvadd at delta) at)
(bvule (bvadd (bvadd at delta) reach) (bvadd at span))))
1
0))
;; Whether the bytes an access somewhere in a range reads are inside a range that has been checked.
;;
;; The same shape as the head above, and the difference is the whole reason it is a second head.
;; There the distance between the two accesses is a number the compiler has. Here it is not: the
;; access is inside a loop, it happens once per iteration at a different address each time, and what
;; the walk knows is that every one of those addresses is somewhere between the first and a furthest
;; one it can name. `far` is that furthest distance and `delta` is whichever iteration is being
;; asked about, so `delta` is a value and not a number.
;;
;; That is what makes this worth proving rather than reading off. The claim is not about one
;; distance, it is about every distance from zero to `far` at once, and a person writing the pass
;; would reason that if the furthest access fits then the nearer ones do. That is true, and it is
;; true because adding a distance no larger than one that already fitted cannot carry an address
;; past where it started, which is a fact about sixty four bit arithmetic rather than about loops.
;; The second disjunct is where `delta` being inside what the walk established is written down: a
;; distance beyond `far` is a distance the walk never claimed anything about, and the answer for one
;; is yes because there is nothing to be wrong about, not because such an access would be safe.
;;
;; The first disjunct is the same assumption the head above makes, in the same words. An access
;; whose byte range runs off the top of the address space and wraps is not inside anything in the
;; containment order, and no such access exists, because document 05's allocator hands out storage
;; instances that do not wrap and a check that passed put its bytes inside one.
(semantics (swept.i64 at span far reach delta)
(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))
;; Whether the bytes an access somewhere in a range reads are inside an object of a known size.
;;
;; The third head, and it is here because the walk that turns an address into a base and a distance
;; can now get past a step it cannot read. When it does, what it has is not one distance but a
;; range of them: the ranges of document 10 bounded the step, so the access happens at some
;; `step` between `delta` and `delta` plus `width` from the object's own address, and which one is
;; not something the compiler is going to find out.
;;
;; `at` is the address of the object, `span` is how many bytes it is, `reach` is how many bytes the
;; access reads, and `step` is the distance it actually goes, which is a value and not a number for
;; the same reason `delta` is a value in the head above.
;;
;; The difference from that one is where the range starts. There the accesses run from the address
;; that was checked out to a furthest one, so the near end is zero. Here the near end is `delta`,
;; because the low end of a step's range is wherever the program's arithmetic put it and there is
;; no reason for it to be the start of the object. Saying it as its own head rather than shifting
;; `at` along by `delta` and reusing the one above is the point: that shift is arithmetic, it is
;; arithmetic on the thing being proved, and doing it in the pass would be exactly the quiet step
;; section 7.7 is written to stop.
;;
;; The two middle disjuncts are where the bound on the step is written down, and they are vacuous
;; answers in the same way the `far` disjunct above is. A step outside what the ranges said is a
;; step nobody claimed anything about, and the answer for one is yes because there is nothing to be
;; wrong about rather than because such an access would be safe.
;;
;; The first disjunct is the same assumption as the other two heads, in the same words. An object
;; whose byte range runs off the top of the address space and wraps is not inside anything in the
;; containment order, and document 05's allocator hands out storage instances that do not wrap.
(semantics (reached.i64 at span delta width reach step)
(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))
;; The same question about a loop whose extent is a value rather than a number.
;;
;; Three of the five disjuncts here are hypotheses and not claims, which is the difference between
;; this head and the one above. There the pass had `span` and `far` as numbers and could check the
;; containment between them before it asked anything, so the guard on the rule said it. Here it has
;; two instructions it emitted and a bound on how large what they compute can get, so what it knows
;; has to be said in the same arithmetic the question is asked in.
;;
;; A reader should be clear about what that means. `(bvult (bvadd far reach) far)` and
;; `(bvult span (bvadd far reach))` are cases the rule answers yes to vacuously, exactly as the
;; distance beyond `far` is above. They are not cases where such an access would be safe. They are
;; cases where the pass has said something the check it emitted does not bear out, and the whole
;; weight of them is on the pass having bounded its own arithmetic before emitting it.
(semantics (swept.sym.i64 at span far reach delta)
(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))
;; The same question again, about a loop whose address walks from high to low.
;;
;; The mirror of the head above, and it is a mirror in every part. `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`. Every addition above is a
;; subtraction here and the direction of every comparison on an address turns over with it.
;;
;; The three hypotheses are the three above, read the same way and with the same warning attached.
;; They are cases this answers yes to vacuously rather than cases where such an access would be
;; safe, and the whole weight of them is on the pass having bounded its own arithmetic before
;; emitting it.
(semantics (swept.down.sym.i64 at span far reach delta)
(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))
;; Whether an address known to be a multiple of one number is a multiple of a smaller one.
;;
;; The alignment half of a bounds check, which is row S7 and the one conjunct in the check that is
;; not about where the bytes are. `at` is the address the access uses, `known` is what the walk over
;; the pointer's origin worked out the address is a multiple of, and `claim` is what the access
;; itself needs. Both numbers are byte counts and both are powers of two.
;;
;; What makes this worth a head rather than a comparison somebody writes in the pass is that the
;; comparison is not the claim. The pass tests `known >= claim`, and being larger is not being
;; divisible by: eight is larger than six and an address that is a multiple of eight is not a
;; multiple of six. The two coincide only because both numbers are powers of two, and a person
;; writing `>=` there is one step away from being right for a reason nobody wrote down.
;;
;; The first four disjuncts are hypotheses and not claims, in the manner of the two heads above.
;; They say the two numbers are powers of two and neither is zero, and they are cases this answers
;; yes to vacuously rather than cases where such an access would be aligned. What carries them is
;; where the numbers come from: a claim is the alignment on an access, which the front end takes off
;; a type, and `known` is the smallest of an `alloca`'s alignment, what an allocator promises, and
;; the largest power of two dividing each step taken from there. Every one of those is a power of
;; two, and a zero is what the pass answers with when it could read nothing, which fails the guard
;; rather than reaching here.
;;
;; The fifth is the fact the walk established, and the last is the claim. Both are written as a mask
;; and not as a remainder, because that is the arithmetic a machine does to answer the question and
;; because a remainder by a value nothing knows is a term no solver settles quickly.
(semantics (aligned.i64 at known claim)
(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))