The SM86 index + 1 of the instruction the branch at `index` jumps to (its
SM86 displacement counts whole instructions), or 0 when that would precede
the program; a target past its end has no label and is refused when the
schedule is relocated.
1437def sm121LowerBranchTarget =
1438 (lambda unrestricted low : Nat .
1439 (lambda unrestricted high : Nat .
1440 (lambda unrestricted index : Nat .
1441 (let unrestricted displacement =
1442 (nat-add
1443 (sm121LowerField low sm121LowerBranchOffsetPlace sm121LowerHalfWordSpan)
1444 (nat-multiply (sm121LowerField high 1 sm121LowerBranchHighSpan) sm121LowerHalfWordSpan)) in
1445 (let unrestricted next = (succ index) in
1446 (naturalSelect (nat-less-than displacement sm121LowerBranchHalf)
1447 (succ (nat-add next (nat-divide displacement sm121LowerInstructionBytes)))
1448 (let unrestricted back =
1449 (nat-divide (nat-subtract sm121LowerBranchSpan displacement) sm121LowerInstructionBytes) in
1450 (naturalSelect (nat-less-than next back) zero (succ (nat-subtract next back))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.