/*========================================================================*/ /* */ /* Copyright (c) 2015-2017 Robert M. Norton */ /* Copyright (c) 2015-2017 Kathyrn Gray */ /* All rights reserved. */ /* */ /* This software was developed by the University of Cambridge Computer */ /* Laboratory as part of the Rigorous Engineering of Mainstream Systems */ /* (REMS) project, funded by EPSRC grant EP/K008528/1. */ /* */ /* Redistribution and use in source and binary forms, with or without */ /* modification, are permitted provided that the following conditions */ /* are met: */ /* 1. Redistributions of source code must retain the above copyright */ /* notice, this list of conditions and the following disclaimer. */ /* 2. Redistributions in binary form must reproduce the above copyright */ /* notice, this list of conditions and the following disclaimer in */ /* the documentation and/or other materials provided with the */ /* distribution. */ /* */ /* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ /* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ /* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ /* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ /* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ /* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ /* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ /* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ /* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ /* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ /* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ /* SUCH DAMAGE. */ /*========================================================================*/ /* 128 bit cap + tag */ type CapReg = bits(129) struct CapStruct = { tag : bool , uperms : bits(4) , access_system_regs : bool , permit_unseal : bool , permit_ccall : bool , permit_seal : bool , permit_store_local_cap : bool , permit_store_cap : bool , permit_load_cap : bool , permit_store : bool , permit_load : bool , permit_execute : bool , global : bool , reserved : bits(2) , E : bits(6) , sealed : bool , B : bits(20), T : bits(20), otype : bits(24), address : bits(64) } let null_cap : CapStruct = struct { tag = false, uperms = zeros(), access_system_regs = false, permit_unseal = false, permit_ccall = false, permit_seal = false, permit_store_local_cap = false, permit_store_cap = false, permit_load_cap = false, permit_store = false, permit_load = false, permit_execute = false, global = false, reserved = zeros(), E = 0b110000, /* 48, encoded as 0 in memory due to xor */ sealed = false, B = zeros(), T = 0x10000, otype = zeros(), address = zeros() } let default_cap : CapStruct = struct { tag = true, uperms = ones(), access_system_regs = true, permit_unseal = true, permit_ccall = true, permit_seal = true, permit_store_local_cap = true, permit_store_cap = true, permit_load_cap = true, permit_store = true, permit_load = true, permit_execute = true, global = true, reserved = zeros(), E = 0b110000, /* 48, encoded as 0 in memory due to xor */ sealed = false, B = zeros(), T = 0x10000, otype = zeros(), address = zeros() } let 'cap_size = 16 function capRegToCapStruct(c) : CapReg -> CapStruct = let s : bool = c[104] in let Bc : bits(20) = if s then c[103..96] @ 0x000 else c[103..84] in let Tc : bits(20) = if s then c[83..76] @ 0x000 else c[83..64] in let otype : bits(24) = if s then c[95..84] @ c[75..64] else zeros() in struct { tag = c[128], uperms = c[127..124], access_system_regs = c[123], permit_unseal = c[122], permit_ccall = c[121], permit_seal = c[120], permit_store_local_cap = c[119], permit_store_cap = c[118], permit_load_cap = c[117], permit_store = c[116], permit_load = c[115], permit_execute = c[114], global = c[113], reserved = c[112..111], E = c[110..105], sealed = s, B = Bc, T = Tc, otype = otype, address = c[63..0] } function getCapHardPerms(cap) : CapStruct -> bits(11) = (cap.access_system_regs @ cap.permit_unseal @ cap.permit_ccall @ cap.permit_seal @ cap.permit_store_local_cap @ cap.permit_store_cap @ cap.permit_load_cap @ cap.permit_store @ cap.permit_load @ cap.permit_execute @ cap.global) function capStructToMemBits128(cap) : CapStruct -> bits(128) = let b : bits(20) = if cap.sealed then (cap.B)[19..12] @ (cap.otype)[23..12] else cap.B in let t : bits(20) = if cap.sealed then (cap.T)[19..12] @ (cap.otype)[11..0] else cap.T in ( cap.uperms @ getCapHardPerms(cap) @ cap.reserved @ cap.E @ cap.sealed @ b @ t @ cap.address ) function capStructToCapReg(cap) : CapStruct -> CapReg = (cap.tag @ capStructToMemBits128(cap)) /* Reverse of above used when reading from memory */ function memBitsToCapBits128(tag, b) : (bool, bits(128)) -> CapReg= (tag @ b) /* When saving/restoring capabilities xor them with bits of null_cap -- this ensures that canonical null_cap is always all-zeros in memory even though it may have bits set logically (e.g. length or exponent */ let null_cap_bits : bits(128) = capStructToMemBits128(null_cap) function capStructToMemBits(cap) : CapStruct -> bits(128) = capStructToMemBits128(cap) ^ null_cap_bits function memBitsToCapBits(tag, b) : (bool, bits(128)) -> bits(129) = memBitsToCapBits128(tag, b ^ null_cap_bits) function getCapPerms(cap) : CapStruct -> bits(31) = let perms : bits(15) = zero_extend(getCapHardPerms(cap)) in (0x000 /* uperms 30-19 */ @ cap.uperms @ perms) function setCapPerms(cap, perms) : (CapStruct, bits(31)) -> CapStruct = { cap with uperms = perms[18..15], /* 14..11 reserved -- ignore */ access_system_regs = perms[10], permit_unseal = perms[9], permit_ccall = perms[8], permit_seal = perms[7], permit_store_local_cap = perms[6], permit_store_cap = perms[5], permit_load_cap = perms[4], permit_store = perms[3], permit_load = perms[2], permit_execute = perms[1], global = perms[0] } function sealCap(cap, otype) : (CapStruct, bits(24)) -> (bool, CapStruct) = if (((cap.T)[11..0] == zeros()) & ((cap.B)[11..0] == zeros())) then (true, {cap with sealed=true, otype=otype}) else (false, cap /* XXX should be undefined? */ ) function a_top_correction(a_mid, R, bound) : (bits(20), bits(20), bits(20)) -> bits(65) = match (a_mid <_u R, bound <_u R) { (false, false) => zeros(), (false, true) => zero_extend(0b1), (true, false) => ones(), (true, true) => zeros() } function getCapBase(c) : CapStruct -> uint64 = let E = min(unsigned(c.E), 48) in let Bc : bits(20) = c.B in let a : bits(65) = zero_extend(c.address) in let R : bits(20) = Bc - 0x01000 in /* wraps */ let a_mid : bits(20) = mask(a >> E) in let correction = a_top_correction(a_mid, R, Bc) in let a_top = a >> E+20 in let base : bits(64) = mask(((a_top + correction) @ Bc) << E) in unsigned(base) function getCapTop (c) : CapStruct -> CapLen = let E = min(unsigned(c.E), 48) in let Bc : bits(20) = c.B in let T : bits(20) = c.T in let a : bits(65) = zero_extend(c.address) in let R : bits(20) = Bc - 0x01000 in /* wraps */ let a_mid : bits(20) = mask(a >> E) in let correction = a_top_correction(a_mid, R, T) in let a_top = a >> E+20 in let top1 : bits(65) = mask((a_top + correction) @ T) in unsigned(top1 << E) function getCapOffset(c) : CapStruct -> uint64 = let base = getCapBase(c) in (unsigned(c.address) - base) % pow2(64) function getCapLength(c) : CapStruct -> CapLen = let 'top = getCapTop(c) in let 'base = getCapBase(c) in { assert (top >= base); top - base } function getCapCursor(cap) : CapStruct -> uint64 = unsigned(cap.address) function fastRepCheck(c, i) : (CapStruct, bits(64)) -> bool= let 'E = unsigned(c.E) in if (E >= 44) then true /* in this case representable region is whole address space */ else let E' = min(E, 43) in let i_top = signed(i[63..E+20]) in let i_mid : bits(20) = i[E+19..E] in let a_mid : bits(20) = (c.address)[E+19..E] in let R : bits(20) = (c.B) - 0x01000 in let diff : bits(20) = R - a_mid in let diff1 : 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 function setCapOffset(c, offset) : (CapStruct, bits(64)) -> (bool, CapStruct) = let base : bits(64) = to_bits(64, getCapBase(c)) in let newAddress : bits(64) = base + offset in let newCap = { c with address = newAddress } in let representable = fastRepCheck(c, (newAddress - c.address)) in (representable, newCap) function incCapOffset(c, delta) : (CapStruct, bits(64)) -> (bool, CapStruct) = let newAddress : bits(64) = c.address + delta in let newCap = { c with address = newAddress } in let representable = fastRepCheck(c, delta) in (representable, newCap) /** FUNCTION:integer HighestSetBit(bits(N) x) */ val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))} function HighestSetBit x = { foreach (i from ('N - 1) to 0 by 1 in dec) if [x[i]] == 0b1 then return (true, i); return (false, 0) } /* hw rounds up E to multiple of 4 */ function roundUp(e) : range(0, 45) -> range(0, 48) = let 'r = e % 4 in if (r == 0) then e else (e - r + 4) function computeE (rlength) : bits(65) -> range(0, 48) = let (nonzero, 'msb) = HighestSetBit((rlength + (rlength >> 6)) >> 19) in if nonzero then /* above will always return <= 45 because 19 bits of zero are shifted in from right */ {assert(0 <= msb & msb <= 45); roundUp (min(msb,45)) } else 0 function setCapBounds(cap, base, top) : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) = /* {cap with base=base; length=(bits(64)) length; offset=0} */ let 'e = computeE(top - (0b0 @ base)) in let Bc : bits(20) = mask(base >> e) in let T : bits(20) = mask(top >> e) in let e_mask : bits(65) = zero_extend(replicate_bits(0b1, e)) in let e_bits = top & e_mask in let T2 : bits(20) = T + (if unsigned(e_bits) == 0 then 0x00000 else 0x00001) in let newCap = {cap with address=base, E=to_bits(6, e), B=Bc, T=T2} in let newBase = getCapBase(newCap) in let newTop = getCapTop(newCap) in let exact = (unsigned(base) == newBase) & (unsigned(top) == newTop) in (exact, newCap) function int_to_cap (offset) : bits(64) -> CapStruct = {null_cap with address = offset}