diff options
Diffstat (limited to 'cheri/sail_latexcc/sailccfnfastRepCheck.tex')
| -rw-r--r-- | cheri/sail_latexcc/sailccfnfastRepCheck.tex | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/cheri/sail_latexcc/sailccfnfastRepCheck.tex b/cheri/sail_latexcc/sailccfnfastRepCheck.tex new file mode 100644 index 00000000..3e4d2111 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnfastRepCheck.tex @@ -0,0 +1,23 @@ +function #\hyperref[zfastRepCheck]{fastRepCheck}#(c, i) : (CapStruct, #\hyperref[zbits]{bits}#(64)) -> bool= + let 'E = #\hyperref[zunsigned]{unsigned}#(c.E) in + if (E >= 44) then + true /* in this case representable region is whole address space */ + else + let E' = #\hyperref[zmin]{min}#(E, 43) in + let i_top = #\hyperref[zsigned]{signed}#(i[63..E+20]) in + let i_mid : #\hyperref[zbits]{bits}#(20) = i[E+19..E] in + let a_mid : #\hyperref[zbits]{bits}#(20) = (c.address)[E+19..E] in + let R : #\hyperref[zbits]{bits}#(20) = (c.B) - 0x01000 in + let diff : #\hyperref[zbits]{bits}#(20) = R - a_mid in + let diff1 : #\hyperref[zbits]{bits}#(20) = diff - 1 in + /* i_top determines 1. whether the increment is inRange + i.e. less than the size of the representable region + (2**(E+20)) and 2. whether it is positive or negative. To + satisfy 1. all top bits must be the same so we are + interested in the cases i_top is 0 or -1 */ + if (i_top == 0) then + i_mid <_u diff1 + else if (i_top == -1) then + (i_mid >=_u diff) & (R != a_mid) + else + false |