diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/Makefile | 9 | ||||
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 375 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 3 | ||||
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 12 | ||||
| -rw-r--r-- | cheri/cheri_types.sail | 1 |
5 files changed, 214 insertions, 186 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index 26bc84ef..1ec835db 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -9,13 +9,16 @@ SAIL_LIB_HEADERS:=$(SAIL_LIB_DIR)/flow.sail CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail -CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail +CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail cheri: $(CHERI_SAILS) - $(SAIL) -ocaml -o cheri $(CHERI_SAILS) + $(SAIL) -ocaml -o $@ $^ + +cheri128: $(CHERI128_SAILS) + $(SAIL) -ocaml -o $@ $^ clean: - rm -rf cheri _sbuild + rm -rf cheri cheri128 _sbuild EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^ //;1d;$$d' > inst_$1.sail extract: cheri_insts.sail diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index 23881f03..47f181c0 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -35,123 +35,145 @@ /* 128 bit cap + tag */ type CapReg = bits(129) +/* val cast_bool_bit : cast extern bool -> bit effect pure val cast_boolvec_bitvec : cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure val cast_range_bitvec : cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v) val not : extern bool -> bool effect pure +*/ + +struct CapStruct = { + tag : bool , + uperms : bits(4) , + access_system_regs : bool , + perm_reserved9 : 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) +} -type uint64 = range<0, (2** 64) - 1> - -type CapStruct = const struct { - bool tag; - bits(4) uperms; - bool access_system_regs; - bool perm_reserved9; - 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; - bits(2) reserved; - bits(6) E; - bool sealed; - bits(20) B; - bits(20) T; - bits(24) otype; - bits(64) address; +let null_cap : CapStruct = struct { + tag = false, + uperms = zeros(), + access_system_regs = false, + perm_reserved9 = 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 null_cap : CapStruct = { - tag = false; - uperms = 0; - access_system_regs = false; - perm_reserved9 = 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 = 0; - E = 48; /* encoded as 0 in memory due to xor */ - sealed = false; - B = 0; - T = 0x10000; - otype = 0; - address = 0; +let default_cap : CapStruct = struct { + tag = true, + uperms = ones(), + access_system_regs = true, + perm_reserved9 = 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() } -def Nat cap_size_t = 16 /* cap size in bytes */ -let cap_size : [:cap_size_t:] = 16 +let 'cap_size = 16 -function CapStruct capRegToCapStruct((CapReg) c) = +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 0 in - { - tag = c[128]; - uperms = c[127..124]; - access_system_regs = c[123]; - perm_reserved9 = 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] ^ 0b110000; - sealed = s; - B = Bc; - T = Tc; - otype = otype; - address = c[63..0]; + 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], + perm_reserved9 = 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] ^ 0b110000, + sealed = s, + B = Bc, + T = Tc, + otype = otype, + address = c[63..0] } -function (bits(11)) getCapHardPerms((CapStruct) cap) = - ([cap.access_system_regs] - : [cap.perm_reserved9] - : [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 (bits(128)) capStructToMemBits128((CapStruct) cap) = - 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 +function getCapHardPerms(cap) : CapStruct -> bits(11) = + (cap.access_system_regs + @ cap.perm_reserved9 + @ 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 ^ 0b110000) /* XXX brackets required otherwise sail interpreter error */ - : [cap.sealed] - : b - : t - : cap.address + @ getCapHardPerms(cap) + @ cap.reserved + @ cap.E ^ 0b110000 + @ cap.sealed + @ b + @ t + @ cap.address ) -function (CapReg) capStructToCapReg((CapStruct) cap) = - ([cap.tag] : capStructToMemBits128(cap)) +function capStructToCapReg(cap) : CapStruct -> CapReg = + (cap.tag @ capStructToMemBits128(cap)) /* Reverse of above used when reading from memory */ -function (CapReg) memBitsToCapBits128((bool) tag, (bits(128)) b) = - ([tag] : b) +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 @@ -159,85 +181,91 @@ function (CapReg) memBitsToCapBits128((bool) tag, (bits(128)) b) = let null_cap_bits : bits(128) = capStructToMemBits128(null_cap) -function (bits(128)) capStructToMemBits((CapStruct) cap) = +function capStructToMemBits(cap) : CapStruct -> bits(128) = capStructToMemBits128(cap) ^ null_cap_bits -function (bits(129)) memBitsToCapBits((bool) tag, (bits(128)) b) = +function memBitsToCapBits(tag, b) : (bool, bits(128)) -> bits(129) = memBitsToCapBits128(tag, b ^ null_cap_bits) -function (bits(31)) getCapPerms((CapStruct) cap) = +function getCapPerms(cap) : CapStruct -> bits(31) = let perms : bits(15) = EXTS(getCapHardPerms(cap)) in /* NB access_system copied into 14-11 */ (0x000 /* uperms 30-19 */ - : cap.uperms - : perms) + @ cap.uperms + @ perms) -function CapStruct setCapPerms((CapStruct) cap, (bits(31)) perms) = +function setCapPerms(cap, perms) : (CapStruct, bits(31)) -> CapStruct = { cap with - uperms = perms[18..15]; + uperms = perms[18..15], /* 14..11 reserved -- ignore */ - access_system_regs = perms[10]; - perm_reserved9 = 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]; + access_system_regs = perms[10], + perm_reserved9 = 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 (bool, CapStruct) sealCap((CapStruct) cap, (bits(24)) otype) = - if (((cap.T)[11..0] == 0) & ((cap.B)[11..0] == 0)) then - (true, {cap with sealed=true; otype=otype}) +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 /* was undefined but ocaml shallow embedding can't handle it */ ) - -function [|-1:1|] a_top_correction((bits(20)) a_mid, (bits(20)) R, (bits(20)) bound) = - match a_mid < R, bound < R { - (false, false) => 0 - (false, true) => 1 - (true, false) => -1 - (true, true) => 0 + (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) => EXTZ(0b1), + (true, false) => ones(), + (true, true) => zeros() } -function uint64 getCapBase((CapStruct) c) = - let E : [|48|] = min(unsigned(c.E), 48) in +function getCapBase(c) : CapStruct -> uint64 = + let E = min(unsigned(c.E), 48) in let Bc : bits(20) = c.B in let a : bits(65) = EXTZ(c.address) in let R : bits(20) = Bc - 0x01000 in /* wraps */ - let a_mid : bits(20) = mask(a >> E) in + let a_mid : bits(20) = mask(shiftr(a, E)) in let correction = a_top_correction(a_mid, R, Bc) in - let a_top = a >> (E+20) in - let base : bits(64) = EXTZ((a_top + correction) : Bc) << E in + let a_top = shiftr(a, E+20) in + let base : bits(64) = mask(shiftl((a_top + correction) @ Bc, E)) in unsigned(base) -function CapLen getCapTop ((CapStruct) c) = - let E : [|45|] = min(unsigned(c.E), 48) in +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) = EXTZ(c.address) in let R : bits(20) = Bc - 0x01000 in /* wraps */ - let a_mid : bits(20) = mask(a >> E) in + let a_mid : bits(20) = mask(shiftr(a, E)) in let correction = a_top_correction(a_mid, R, T) in - let a_top = a >> (E+20) in - let top1 : bits(65) = EXTZ((a_top + correction) : T) in - (CapLen) (top1 << E) + let a_top = shiftr(a, E+20) in + let top1 : bits(65) = mask((a_top + correction) @ T) in + unsigned(shiftl(top1, E)) -function uint64 getCapOffset((CapStruct) c) = +function getCapOffset(c) : CapStruct -> uint64 = let base = getCapBase(c) in - unsigned(c.address) - base + (unsigned(c.address) - base) % pow2(64) -function CapLen getCapLength((CapStruct) c) = getCapTop(c) - getCapBase(c) +function getCapLength(c) : CapStruct -> CapLen = + let 'top = getCapTop(c) in + let 'base = getCapBase(c) in { + assert (top >= base); + top - base + } -function uint64 getCapCursor((CapStruct) cap) = unsigned(cap.address) +function getCapCursor(cap) : CapStruct -> uint64 = unsigned(cap.address) -function bool fastRepCheck((CapStruct) c, (bits(64)) i) = - if ((c.E) >= 44) then +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(unsigned(c.E), 43) in + 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 @@ -252,18 +280,18 @@ function bool fastRepCheck((CapStruct) c, (bits(64)) i) = if (i_top == 0) then i_mid <_u diff1 else if (i_top == -1) then - unsigned(i_mid) >= unsigned(diff) & (R != a_mid) /* XXX sail missing unsigned >= */ + (i_mid >=_u diff) & (R != a_mid) else false -function (bool, CapStruct) setCapOffset((CapStruct) c, (bits(64)) offset) = - let base : bits(64) = (bits(64)) (getCapBase(c)) in +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 (bool, CapStruct) incCapOffset((CapStruct) c, (bits(64)) delta) = +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 @@ -271,46 +299,41 @@ function (bool, CapStruct) incCapOffset((CapStruct) c, (bits(64)) delta) = /** FUNCTION:integer HighestSetBit(bits(N) x) */ -function forall Nat 'N. option([|0:('N + -1)|]) HighestSetBit((bits('N)) x) = { - let N = (length(x)) in { - ([|('N + -1)|]) result = 0; - (bool) break = false; - foreach (i from (N - 1) downto 0) - if ~(break) & x[i] == 1 then { - result = i; - break = true; - }; - - if break then Some(result) else None; -}} +val HighestSetBit : forall 'N , 'N >= 2. bits('N) -> {'n, -1 <= 'n < 'N . atom('n)} +function HighestSetBit x = { + foreach (i from ('N - 1) to 0 by 1 in dec) + if [x[i]] == 0b1 then return i else (); + return -1 +} /* hw rounds up E to multiple of 4 */ -function [|48|] roundUp(([|45|]) e) = - let r = e mod 4 in +function roundUp(e) : range(0, 45) -> range(0, 48) = + let 'r = e % 4 in if (r == 0) then e else (e - r + 4) - -function [|48|] computeE ((bits(65)) rlength) = - let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in +function computeE (rlength) : bits(65) -> range(0, 48) = + let msb = HighestSetBit(shiftr(rlength + shiftr(rlength, 6), 19)) in match msb { + -1 => 0, /* above will always return <= 45 because 19 bits of zero are shifted in from right */ - (Some(b)) => {assert(b <= 45, None); roundUp (min(b,45)) } - None => 0 + 'b => {assert(0 <= b & b <= 45); roundUp (min(b,45)) } } -function (bool, CapStruct) setCapBounds((CapStruct) cap, (bits(64)) base, (bits(65)) top) = +function setCapBounds(cap, base, top) : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) = /* {cap with base=base; length=(bits(64)) length; offset=0} */ - let e : [|48|] = computeE(top - (0b0 : base)) in - let Bc : bits(20) = base[19+e..e] in - let T : bits(20) = top[19+e..e] in - let T2 : bits(20) = T + if (top[(e - 1)..0] == 0) then 0 else 1 in - let newCap = {cap with E=(bits(6)) e; B=Bc; T=T2} in + let 'e = computeE(top - (0b0 @ base)) in + let Bc : bits(20) = mask(shiftr(base, e)) in + let T : bits(20) = mask(shiftr(top, e)) in + let e_mask : bits(65) = EXTZ(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 E=to_bits(6, e), B=Bc, T=T2} in let newBase = getCapBase(newCap) in let newTop = getCapTop(newCap) in - let exact = (base == newBase) & (top == newTop) in + let exact = (unsigned(base) == newBase) & (unsigned(top) == newTop) in (exact, newCap) -function CapStruct int_to_cap ((bits(64)) offset) = +function int_to_cap (offset) : bits(64) -> CapStruct = {null_cap with address = offset} diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index c75f588e..3af7ee28 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -42,8 +42,6 @@ val cast_range_bitvec : forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v) val not : extern bool -> bool effect pure */ -type uint64 = range(0, (2 ^ 64) - 1) - struct CapStruct = { tag : bool , padding : bits(8) , @@ -114,7 +112,6 @@ let default_cap : CapStruct = struct { } let 'cap_size = 32 -let cap_addr_mask = to_bits(64, pow2(64) - cap_size) function capRegToCapStruct(capReg) : CapReg -> CapStruct = struct { diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index 02a6d408..0a491145 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -300,6 +300,8 @@ function MEMw_tagged_conditional(addr, tag, data) = success; } +let cap_addr_mask = to_bits(64, pow2(64) - cap_size) + val MEMw_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {escape, wmv, wmvt, wreg, eamem} function MEMw_wrapper(addr, size, data) = let ledata = reverse_endianness(data) in @@ -400,8 +402,9 @@ function cp2_next_pc () = { }; } -val capToString : CapStruct -> string -function capToString cap = +val capToString : CapStruct -> string effect {escape} +function capToString cap = { + skip_escape(); /* because cheri128 getCapX functions contain asserts but cheri256 ones do not */ concat_str(" t:", concat_str(if cap.tag then "1" else "0", concat_str(" s:", @@ -414,11 +417,12 @@ function capToString cap = concat_str(BitStr(to_bits(64, getCapOffset(cap))), concat_str(" base:", concat_str(BitStr(to_bits(64, getCapBase(cap))), - concat_str(" length:", BitStr(to_bits(64, getCapLength(cap)))))))))))))))) + concat_str(" length:", BitStr(to_bits(64, min(getCapLength(cap), MAX(64))))))))))))))))) + } function dump_cp2_state () = { print(concat_str("DEBUG CAP PCC", capToString(capRegToCapStruct(PCC)))); foreach(i from 0 to 31) { print(concat_str("DEBUG CAP REG ", concat_str(string_of_int(i), capToString(readCapReg(to_bits(5, i)))))) } -}
\ No newline at end of file +} diff --git a/cheri/cheri_types.sail b/cheri/cheri_types.sail index 18043fa0..af23bcb4 100644 --- a/cheri/cheri_types.sail +++ b/cheri/cheri_types.sail @@ -33,6 +33,7 @@ /*========================================================================*/ type CapLen = range(0, 2 ^ 65) +type uint64 = range(0, (2 ^ 64) - 1) enum CPtrCmpOp = { CEQ, |