half_check.pl
Half checks: a check whose object was checked before at another range tests only the bound that is not already known (docs/half.md).
An access check tests that the capability is not null, that the address is at or above lower and that its end is at or below upper. When an earlier check of the same object, through a pointer at a constant distance from the same base, dominates this one, it proved the capability not null and an address range of the object. If this access starts at or above where that range started, the lower test is known; if it ends at or below where that range ended, the upper test is, since an object's upper changes only when it is freed, which sets its free flag. The check becomes
| Term | Tests |
|---|---|
half_checkupper, Lo, Hi, Rights, Align | upper, then read-only for a write, and alignment |
half_checklower, Lo, Hi, Rights, Align | lower (signed), the free flag and read-only for a write, and alignment |
reading tmpQ1, P, Q1 the earlier proof. It traps exactly where the check would, at the same access and with the same report. Nothing moves, and no fact needs a kill list: the facts it uses last as long as the object does.
The pass is selected with --checks=half, after renewal. ir.pl's validator accepts each half check by its own rule (half_known/6), and half_refines/2 checks that the only change is checks replaced in place by half checks of the same pointer, range, rights and alignment.
M is the checked module M0 with each heap check that an earlier heap check of the same object dominates, at a constant distance through one single-definition base, replaced by a half check of the bound that earlier check does not establish. Functions with a setjmp are unchanged. Every instruction keeps its index, so context sites are unchanged.
half_sources(+Blocks, +Once, +Dom, -Sources): Sources maps each single-definition base name B to s(Pre, L, I, Q1, P1, Lo1, Hi1, K1) for each heap proof Q1 of P1 in a reachable block L at index I that proves P1+[Lo1, Hi1), where Q1 and P1 have one definition and P1 is B + K1 exactly (guard_chain/3). Pre is L's preorder number in the dominator tree (dom_intervals/3), so a block's dominators come before it, and dominance is an interval test, not a walk up the tree.
a heap proof Op of Args has proven P's [Lo, Hi): a check or check_ahead of its whole range, a guarded renewal or a hoisted check, which are their checks.
| 83 | checkLo, Hi, _, _ | P | P | Lo | Hi |
| 84 | check_aheadLo, Hi, _, _, _ | P | P | Lo | Hi |
| 85 | renew_ifLo, Hi, _, _ | P, _ | P | Lo | Hi |
| 86 | check_limitLo, Hi, _, _ | P, _ | P | Lo | Hi |
known_bound(+Distance, +Lo, +Hi, +Lo1, +Hi1, -Bound): a check of [Lo, Hi) at P = P1 + Distance (modulo 2^64), after a passed check of [Lo1, Hi1) at P1, needs to test only Bound: lower when its end is at or below the earlier end (one test fewer for a write, whose flag test then covers free too), else upper when its start is at or above the earlier start. The distance is taken signed, and both differences must be far from 2^63, where an address could wrap.
M is M0 except for heap checks replaced in place by half checks of the same pointer, range, rights and alignment. A half check is its check by definition (ir.pl); whether its source establishes the bound it leaves untested is the validator's question (valid_module/1).