diff options
Diffstat (limited to 'cheri/sail_latexcc/sailccfngetCapTop.tex')
| -rw-r--r-- | cheri/sail_latexcc/sailccfngetCapTop.tex | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/cheri/sail_latexcc/sailccfngetCapTop.tex b/cheri/sail_latexcc/sailccfngetCapTop.tex new file mode 100644 index 00000000..1be5af24 --- /dev/null +++ b/cheri/sail_latexcc/sailccfngetCapTop.tex @@ -0,0 +1,11 @@ +function #\hyperref[zgetCapTop]{getCapTop}# (c) : CapStruct -> CapLen = + let E = #\hyperref[zmin]{min}#(#\hyperref[zunsigned]{unsigned}#(c.E), 48) in + let Bc : #\hyperref[zbits]{bits}#(20) = c.B in + let T : #\hyperref[zbits]{bits}#(20) = c.T in + let a : #\hyperref[zbits]{bits}#(65) = #\hyperref[zzzerozyextend]{zero\_extend}#(c.address) in + let R : #\hyperref[zbits]{bits}#(20) = Bc - 0x01000 in /* wraps */ + let a_mid : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(a >> E) in + let correction = #\hyperref[zazytopzycorrection]{a\_top\_correction}#(a_mid, R, T) in + let a_top = a >> E+20 in + let top1 : #\hyperref[zbits]{bits}#(65) = #\hyperref[zmask]{mask}#((a_top + correction) @ T) in + #\hyperref[zunsigned]{unsigned}#(top1 << E) |