diff options
| -rw-r--r-- | cheri/Makefile | 61 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 20 | ||||
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 42 | ||||
| -rw-r--r-- | mips/mips_prelude.sail | 9 | ||||
| -rw-r--r-- | mips/prelude.sail | 9 |
5 files changed, 65 insertions, 76 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index a5df5f1e..5861dde4 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -31,9 +31,16 @@ cheri_trace: $(CHERI_SAILS) $(CHERI_MAIN) cheri.c: $(CHERI_SAILS) $(CHERI_MAIN) $(SAIL) -memo_z3 -c $^ 1> $@ -latex: $(CHERI_SAILS) +latex_128: $(MIPS_SAIL_DIR)/prelude.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail + rm -rf sail_latexcc + $(SAIL) -latex -latex_prefix sailcc -o sail_latexcc $^ + +latex_256: $(CHERI_SAILS) + rm -rf sail_latex $(SAIL) -latex $^ +latex: latex_128 latex_256 + cheri128: $(CHERI128_SAILS) $(CHERI_MAIN) $(SAIL) -ocaml -o $@ $^ @@ -69,54 +76,4 @@ C%.thy: c%.lem c%_types.lem $(MIPS_SAIL_DIR)/mips_extras.lem sed -i 's/datatype ast/datatype (plugins only: size) ast/' C$*_types.thy clean: - rm -rf cheri cheri128 _sbuild inst_*.sail cheri.c - -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 - $(call EXTRACT_INST,CGetPerms) - $(call EXTRACT_INST,CGetType) - $(call EXTRACT_INST,CGetBase) - $(call EXTRACT_INST,CGetOffset) - $(call EXTRACT_INST,CGetLen) - $(call EXTRACT_INST,CGetTag) - $(call EXTRACT_INST,CGetSealed) - $(call EXTRACT_INST,CGetAddr) - $(call EXTRACT_INST,CGetPCC) - $(call EXTRACT_INST,CGetPCCSetOffset) - $(call EXTRACT_INST,CGetCause) - $(call EXTRACT_INST,CSetCause) - $(call EXTRACT_INST,CAndPerm) - $(call EXTRACT_INST,CToPtr) - $(call EXTRACT_INST,CSub) - $(call EXTRACT_INST,CPtrCmp) - $(call EXTRACT_INST,CIncOffset) - $(call EXTRACT_INST,CIncOffsetImmediate) - $(call EXTRACT_INST,CSetOffset) - $(call EXTRACT_INST,CSetBounds) - $(call EXTRACT_INST,CSetBoundsImmediate) - $(call EXTRACT_INST,CSetBoundsExact) - $(call EXTRACT_INST,CClearTag) - $(call EXTRACT_INST,CMOVX) - $(call EXTRACT_INST,ClearRegs) - $(call EXTRACT_INST,CFromPtr) - $(call EXTRACT_INST,CBuildCap) - $(call EXTRACT_INST,CCopyType) - $(call EXTRACT_INST,CCheckPerm) - $(call EXTRACT_INST,CCheckType) - $(call EXTRACT_INST,CTestSubset) - $(call EXTRACT_INST,CSeal) - $(call EXTRACT_INST,CCSeal) - $(call EXTRACT_INST,CUnseal) - $(call EXTRACT_INST,CCall) - $(call EXTRACT_INST,CCall2) - $(call EXTRACT_INST,CReturn) - $(call EXTRACT_INST,CBtag) - $(call EXTRACT_INST,CBz) - $(call EXTRACT_INST,CJALR) - $(call EXTRACT_INST,CLoad) - $(call EXTRACT_INST,CStore) - $(call EXTRACT_INST,CSC) - $(call EXTRACT_INST,CLC) - $(call EXTRACT_INST,CReadHwr) - $(call EXTRACT_INST,CWriteHwr) - + rm -rf cheri cheri_trace cheri128 cheri128_trace _sbuild inst_*.sail cheri.c sail_latex sail_latexcc diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index 5590bbb8..babfc117 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -196,20 +196,32 @@ function sealCap(cap, otype) : (CapStruct, bits(24)) -> (bool, CapStruct) = (true, {cap with sealed=true, otype=otype}) function getCapBase(c) : CapStruct -> uint64 = unsigned(c.base) -function getCapTop(c) : CapStruct -> CapLen = unsigned(c.base) + unsigned(c.length) +function getCapTop(c) : CapStruct -> CapLen = unsigned(c.base) + unsigned(c.length) /* XXX bug here? -- should be mod 2^64 */ function getCapOffset(c) : CapStruct -> uint64 = (unsigned(c.address) - unsigned(c.base)) % (pow2(64)) function getCapLength(c) : CapStruct -> CapLen = unsigned(c.length) function getCapCursor(c) : CapStruct -> uint64 = unsigned(c.address) -function setCapOffset(c, offset) : (CapStruct, bits(64)) -> (bool, CapStruct) = +/*! +Set the offset capability of the a capability to given value and return the result, along with a boolean indicating true if the operation preserved the existing bounds of the capability. When using compressed capabilities, setting the offset far outside the capability bounds can cause the result to become unrepresentable (XXX mention guarantees). Additionally in some implementations a fast representablity check may be used that could cause the operation to return failure even though the capability would be representable (XXX provide details). + */ +val setCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct) +function setCapOffset(c, offset) = (true, {c with address=c.base + offset}) -function incCapOffset(c, delta) : (CapStruct, bits(64)) -> (bool, CapStruct) = +/*! +\function{incCapOffset} is the same as \function{setCapOffset} except that the 64-bit value is added to the current capability offset modulo $2^{64}$ (i.e. signed twos-complement arithemtic). + */ +val incCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct) +function incCapOffset(c, delta) = let newAddr : bits(64) = c.address + delta in (true, {c with address = newAddr}) -function setCapBounds(cap, base, top) : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) = +/*! +Returns a capability derived from the given capability by setting the base and top to values provided. The offset of the resulting capability is zero. In case the requested bounds are not exactly representable the returned boolean is false and the returned capability has bounds at least including the region bounded by base and top but rounded to representable values. + */ +val setCapBounds : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) +function setCapBounds(cap, base, top) = let length : bits(65) = top - (0b0 @ base) in (true, {cap with base = base, length = length[63..0], address = base}) diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index ecb98ef8..e6273281 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -128,7 +128,11 @@ let CapRegs : vector(32, dec, register(CapReg)) = let max_otype = MAX(24) /*0xffffff*/ let have_cp2 = true -function readCapReg(n) : regno -> CapStruct = +/*! +This function reads a given capability register and returns its contents converted to a CapStruct. +*/ +val readCapReg : regno -> CapStruct effect {rreg} +function readCapReg(n) = let 'i = unsigned(n) in capRegToCapStruct(reg_deref(CapRegs[i])) @@ -259,19 +263,12 @@ function pcc_access_system_regs () = val register_inaccessible : regno -> bool effect {rreg} function register_inaccessible(r) = - if (r == IDC) & inCCallDelay then true else - let is_sys_reg : bool = match r { - 0b11011 => true, - 0b11100 => true, - 0b11101 => true, - 0b11110 => true, - 0b11111 => true, - _ => false - } in - if is_sys_reg then - not (pcc_access_system_regs ()) - else - false + ((r == IDC) & inCCallDelay) | + ((r == KR1C | + r == KR2C | + r == KDC | + r == KCC | + r == EPCC) & not (pcc_access_system_regs ())) val MEMr_tag = "read_tag_bool" : bits(64) -> bool effect { rmemt } val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt } @@ -399,13 +396,20 @@ function TranslatePC (vAddr) = { else TLBTranslate(to_bits(64, absPC), Instruction) /* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps */ } + +/*! +All capability instrucitons must first check that the capability +co-processor is enabled using the following function that raises a +co-processor unusable exception if a CP0Status.CU2 is not set. This +allows the operating system to only save and restore the full +capability context for processes that use capabilities. +*/ val checkCP2usable : unit -> unit effect {rreg, wreg, escape} function checkCP2usable () = - if not ((CP0Status.CU())[2]) then - { - (CP0Cause->CE()) = 0b10; - (SignalException(CpU)); - } + if not (CP0Status.CU()[2]) then { + CP0Cause->CE() = 0b10; + SignalException(CpU); + } function init_cp2_state () = { let defaultBits = capStructToCapReg(default_cap); diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail index 9e81a5d0..f9049b5d 100644 --- a/mips/mips_prelude.sail +++ b/mips/mips_prelude.sail @@ -469,11 +469,18 @@ function int_of_AccessLevel level = Kernel => 2 } +/*! +Returns whether the first AccessLevel is sufficient to grant access at the second, required, access level. + */ val grantsAccess : (AccessLevel, AccessLevel) -> bool function grantsAccess (currentLevel, requiredLevel) = int_of_AccessLevel(currentLevel) >= int_of_AccessLevel(requiredLevel) -function getAccessLevel() : unit -> AccessLevel= +/*! +Returns the current effective access level determined by accessing the relevant parts of the MIPS status register. + */ +val getAccessLevel : unit -> AccessLevel effect {rreg} +function getAccessLevel() = if ((CP0Status.EXL()) | (CP0Status.ERL())) then Kernel else match CP0Status.KSU() diff --git a/mips/prelude.sail b/mips/prelude.sail index aa81175f..152996f1 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -87,8 +87,14 @@ function or_vec (xs, ys) = builtin_or_vec(xs, ys) overload operator | = {or_bool, or_vec} +/*! +The \function{unsigned} function converts a bit vector to an integer assuming an unsigned representation: +*/ val unsigned = {ocaml: "uint", lem: "uint"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) +/*! +The \function{signed} function converts a bit vector to an integer assuming a signed twos-complement representation: +*/ val signed = {ocaml: "sint", lem: "sint"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) val "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w) @@ -277,6 +283,9 @@ val operator *_s = "mults_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n infix 7 *_u val operator *_u = "mult_vec" : forall 'n . (bits('n), bits('n)) -> bits(2 * 'n) +/*! +\function{to\_bits} converts an integer to a bit vector of given length. If the integer is negative a twos-complement representation is used. If the integer is too large (or too negative) to fit in the requested length then it is truncated to the least significant bits. +*/ val to_bits : forall 'l.(atom('l), int) -> bits('l) function to_bits (l, n) = get_slice_int(l, n, 0) |