diff options
| -rw-r--r-- | cheri/Makefile | 22 | ||||
| -rw-r--r-- | cheri/cheri_insts.sail | 1106 | ||||
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 264 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 382 | ||||
| -rw-r--r-- | cheri/cheri_prelude_common.sail | 501 | ||||
| -rw-r--r-- | cheri/cheri_types.sail | 87 | ||||
| -rw-r--r-- | mips_new_tc/mips_insts.sail | 1 | ||||
| -rw-r--r-- | mips_new_tc/prelude.sail | 8 |
8 files changed, 1219 insertions, 1152 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index 813902a2..a443d123 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -1,5 +1,25 @@ -EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^ //;1d;$$d' > inst_$1.sail +THIS_MAKEFILE := $(realpath $(lastword $(MAKEFILE_LIST))) +SAIL_DIR:=$(realpath $(dir $(THIS_MAKEFILE))..) +export SAIL_DIR +SAIL_LIB_DIR:=$(SAIL_DIR)/lib +MIPS_SAIL_DIR:=$(SAIL_DIR)/mips_new_tc +CHERI_SAIL_DIR:=$(SAIL_DIR)/cheri +SAIL:=$(SAIL_DIR)/sail +SAIL_LIB_HEADERS:=$(SAIL_LIB_DIR)/flow.sail + +MIPS_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.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 + +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 +cheri: $(CHERI_SAILS) + $(SAIL) -ocaml -o cheri $(CHERI_SAILS) + +clean: + rm -rf _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 $(call EXTRACT_INST,CGetPerms) $(call EXTRACT_INST,CGetType) diff --git a/cheri/cheri_insts.sail b/cheri/cheri_insts.sail index f6b8818e..3d27fde3 100644 --- a/cheri/cheri_insts.sail +++ b/cheri/cheri_insts.sail @@ -1,309 +1,307 @@ -(*========================================================================*) -(* *) -(* 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. *) -(*========================================================================*) - -(* Old encodings *) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b000) = Some(CGetPerm(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b001) = Some(CGetType(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetBase(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b011) = Some(CGetLen(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b101) = Some(CGetTag(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000000 : 0b110) = Some(CGetSealed(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd)) - -function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn) - -function clause decode (0b010010 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetOffset(rd, cb)) (* NB encoding does not follow pattern *) -function clause decode (0b010010 : 0b00100 : 0b00000 : 0b00000 : (regno) rt : 0b000 : 0b100) = Some(CSetCause(rt)) -function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CAndPerm(cd, cb, rt)) -function clause decode (0b010010 : 0b01100 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CToPtr(rd, cb, ct)) - -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CPtrCmp(rd, cb, ct, CEQ)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b001) = Some(CPtrCmp(rd, cb, ct, CNE)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b010) = Some(CPtrCmp(rd, cb, ct, CLT)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b011) = Some(CPtrCmp(rd, cb, ct, CLE)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b100) = Some(CPtrCmp(rd, cb, ct, CLTU)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b101) = Some(CPtrCmp(rd, cb, ct, CLEU)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b110) = Some(CPtrCmp(rd, cb, ct, CEXEQ)) -function clause decode (0b010010 : 0b01110 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b111) = Some(CPtrCmp(rd, cb, ct, CNEXEQ)) -function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CIncOffset(cd, cb, rt)) -function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b001) = Some(CSetOffset(cd, cb, rt)) -function clause decode (0b010010 : 0b00001 : (regno) cd : (regno) cb : (regno) rt : 0b000000) = Some(CSetBounds(cd, cb, rt)) - -function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : 0b00000 : 0b000: 0b101) = Some(CClearTag(cd, cb)) -function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000: 0b111) = Some(CFromPtr(cd, cb, rt)) -function clause decode (0b010010 : 0b01011 : (regno) cs : 0b00000 : (regno) rt : 0b000: 0b000) = Some(CCheckPerm(cs, rt)) -function clause decode (0b010010 : 0b01011 : (regno) cs : (regno) cb : 0b00000 : 0b000: 0b001) = Some(CCheckType(cs, cb)) -function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CSeal(cd, cs, ct)) -function clause decode (0b010010 : 0b00011 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CUnseal(cd, cs, ct)) -function clause decode (0b010010 : 0b00111 : (regno) cd : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(cd, cb, true)) (* CJALR *) -function clause decode (0b010010 : 0b01000 : 0b00000 : (regno) cb : 0b00000 : 0b000000) = Some(CJALR(0b00000, cb, false)) (* CJR *) - - -(* +/*========================================================================*/ +/* */ +/* 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. */ +/*========================================================================*/ + +/* Old encodings */ +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b000) = Some(CGetPerm(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b001) = Some(CGetType(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b010) = Some(CGetBase(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b011) = Some(CGetLen(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b101) = Some(CGetTag(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000000 @ 0b110) = Some(CGetSealed(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ 0b00000 @ 0b00000000 @ 0b100) = Some(CGetCause(rd)) + +function clause decode (0b010010 @ 0b00110 @ 0b000000000000000000000) = Some(CReturn) + +function clause decode (0b010010 @ 0b01101 @ rd : regno @ cb : regno @ 0b00000000 @ 0b010) = Some(CGetOffset(rd, cb)) /* NB encoding does not follow pattern */ +function clause decode (0b010010 @ 0b00100 @ 0b00000 @ 0b00000 @ rt : regno @ 0b000 @ 0b100) = Some(CSetCause(rt)) +function clause decode (0b010010 @ 0b00100 @ cd : regno @ cb : regno @ rt : regno @ 0b000 @ 0b000) = Some(CAndPerm(cd, cb, rt)) +function clause decode (0b010010 @ 0b01100 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b000) = Some(CToPtr(rd, cb, ct)) + +function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b000) = Some(CPtrCmp(rd, cb, ct, CEQ)) +function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b001) = Some(CPtrCmp(rd, cb, ct, CNE)) +function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b010) = Some(CPtrCmp(rd, cb, ct, CLT)) +function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b011) = Some(CPtrCmp(rd, cb, ct, CLE)) +function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b100) = Some(CPtrCmp(rd, cb, ct, CLTU)) +function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b101) = Some(CPtrCmp(rd, cb, ct, CLEU)) +function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b110) = Some(CPtrCmp(rd, cb, ct, CEXEQ)) +function clause decode (0b010010 @ 0b01110 @ rd : regno @ cb : regno @ ct : regno @ 0b000 @ 0b111) = Some(CPtrCmp(rd, cb, ct, CNEXEQ)) +function clause decode (0b010010 @ 0b01101 @ cd : regno @ cb : regno @ rt : regno @ 0b000 @ 0b000) = Some(CIncOffset(cd, cb, rt)) +function clause decode (0b010010 @ 0b01101 @ cd : regno @ cb : regno @ rt : regno @ 0b000 @ 0b001) = Some(CSetOffset(cd, cb, rt)) +function clause decode (0b010010 @ 0b00001 @ cd : regno @ cb : regno @ rt : regno @ 0b000000) = Some(CSetBounds(cd, cb, rt)) + +function clause decode (0b010010 @ 0b00100 @ cd : regno @ cb : regno @ 0b00000 @ 0b000@ 0b101) = Some(CClearTag(cd, cb)) +function clause decode (0b010010 @ 0b00100 @ cd : regno @ cb : regno @ rt : regno @ 0b000@ 0b111) = Some(CFromPtr(cd, cb, rt)) +function clause decode (0b010010 @ 0b01011 @ cs : regno @ 0b00000 @ rt : regno @ 0b000@ 0b000) = Some(CCheckPerm(cs, rt)) +function clause decode (0b010010 @ 0b01011 @ cs : regno @ cb : regno @ 0b00000 @ 0b000@ 0b001) = Some(CCheckType(cs, cb)) +function clause decode (0b010010 @ 0b00010 @ cd : regno @ cs : regno @ ct : regno @ 0b000@ 0b000) = Some(CSeal(cd, cs, ct)) +function clause decode (0b010010 @ 0b00011 @ cd : regno @ cs : regno @ ct : regno @ 0b000@ 0b000) = Some(CUnseal(cd, cs, ct)) +function clause decode (0b010010 @ 0b00111 @ cd : regno @ cb : regno @ 0b00000 @ 0b000000) = Some(CJALR(cd, cb, true)) /* CJALR */ +function clause decode (0b010010 @ 0b01000 @ 0b00000 @ cb : regno @ 0b00000 @ 0b000000) = Some(CJALR(0b00000, cb, false)) /* CJR */ + + +/* New encodings as per CHERI ISA Appendix B.2. NB: Must be careful about order of matching because unused register fields are re-used as additional function codes. -*) - -(* One arg *) -function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00001 : 0b11111 : 0b111111) = Some(CGetCause(rd)) -function clause decode (0b010010 : 0b00000 : (regno) rs : 0b00010 : 0b11111 : 0b111111) = Some(CSetCause(rs)) -function clause decode (0b010010 : 0b00000 : (regno) cd : 0b00000 : 0b11111 : 0b111111) = Some(CGetPCC(cd)) -function clause decode (0b010010 : 0b00000 : (regno) cb : 0b00011 : 0b11111 : 0b111111) = Some(CJALR(0b00000, cb, false)) (* CJR *) - -(* Two arg *) -function clause decode (0b010010 : 0b00000 : (regno) cs : (regno) rt : 0b01000 : 0b111111) = Some(CCheckPerm(cs, rt)) -function clause decode (0b010010 : 0b00000 : (regno) cs : (regno) cb : 0b01001 : 0b111111) = Some(CCheckType(cs, cb)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : 0b01011 : 0b111111) = Some(CClearTag(cd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : 0b01010 : 0b111111) = Some(CMOVX(cd, cs, 0b00000, false)) (* CMOVE *) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : 0b01100 : 0b111111) = Some(CJALR(cd, cb, true)) (* CJALR *) - -(* Capability Inspection *) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00000 : 0b111111) = Some(CGetPerm(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00001 : 0b111111) = Some(CGetType(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00010 : 0b111111) = Some(CGetBase(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00011 : 0b111111) = Some(CGetLen(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00100 : 0b111111) = Some(CGetTag(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00101 : 0b111111) = Some(CGetSealed(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : 0b00110 : 0b111111) = Some(CGetOffset(rd, cb)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) rs : 0b00111 : 0b111111) = Some(CGetPCCSetOffset(cd, rs)) - -(* Three operand *) - -(* Capability Modification *) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b001011) = Some(CSeal(cd, cs, ct)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b001100) = Some(CUnseal(cd, cs, ct)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001101) = Some(CAndPerm(cd, cs, rt)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001111) = Some(CSetOffset(cd, cs, rt)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001000) = Some(CSetBounds(cd, cs, rt)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rt : 0b001001) = Some(CSetBoundsExact(cd, cs, rt)) - - -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b010001) = Some(CIncOffset(cd, cb, rt)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) ct : 0b011101) = Some(CBuildCap(cd, cb, ct)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) ct : 0b011110) = Some(CCopyType(cd, cb, ct)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) ct : 0b011111) = Some(CCSeal(cd, cs, ct)) - -(* Pointer Arithmetic *) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b010010) = Some(CToPtr(rd, cb, ct)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rs : 0b010011) = Some(CFromPtr(cd, cb, rs)) -function clause decode (0b010010 : 0b00000 : (regno) rt : (regno) cb : (regno) cs : 0b001010) = Some(CSub(rt, cb, cs)) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rs : 0b011011) = Some(CMOVX(cd, cs, rs, false)) (* CMOVZ *) -function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cs : (regno) rs : 0b011100) = Some(CMOVX(cd, cs, rs, true)) (* CMOVN *) - -(* Pointer Comparison *) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010100) = Some(CPtrCmp(rd, cb, cs, CEQ)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010101) = Some(CPtrCmp(rd, cb, cs, CNE)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010110) = Some(CPtrCmp(rd, cb, cs, CLT)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b010111) = Some(CPtrCmp(rd, cb, cs, CLE)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011000) = Some(CPtrCmp(rd, cb, cs, CLTU)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011001) = Some(CPtrCmp(rd, cb, cs, CLEU)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b011010) = Some(CPtrCmp(rd, cb, cs, CEXEQ)) -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) cs : 0b100001) = Some(CPtrCmp(rd, cb, cs, CNEXEQ)) - -function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b100000) = Some(CTestSubset(rd, cb, ct)) - -function clause decode (0b010010 : 0b01001 : (regno) cd : (bit[16]) imm) = Some(CBX(cd, imm, true)) (* CBTU *) -function clause decode (0b010010 : 0b01010 : (regno) cd : (bit[16]) imm) = Some(CBX(cd, imm, false)) (* CBTS *) -function clause decode (0b010010 : 0b10001 : (regno) cd : (bit[16]) imm) = Some(CBZ(cd, imm, false)) (* CBEZ *) -function clause decode (0b010010 : 0b10010 : (regno) cd : (bit[16]) imm) = Some(CBZ(cd, imm, true)) (* CBNZ *) - -function clause decode (0b010010 : 0b00101 : 0b00000 : 0b00000 : 0b11111111111) = Some(CReturn) -function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb, selector)) - -function clause decode (0b010010 : 0b01111 : 0b00000 : (bit[16]) imm) = Some(ClearRegs(GPLo, imm)) -function clause decode (0b010010 : 0b01111 : 0b00001 : (bit[16]) imm) = Some(ClearRegs(GPHi, imm)) -function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(ClearRegs(CLo, imm)) -function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi, imm)) - -function clause decode (0b010010 : 0b10011 : (regno) cd : (regno) cb : (bit[11]) imm) = Some(CIncOffsetImmediate(cd, cb, imm)) -function clause decode (0b010010 : 0b10100 : (regno) cd : (regno) cb : (bit[11]) imm) = Some(CSetBoundsImmediate(cd, cb, imm)) - -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CLoad(rd, cb, rt, offset, false, B, false)) (* CLBU *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b00) = Some(CLoad(rd, cb, rt, offset, true, B, false)) (* CLB *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CLoad(rd, cb, rt, offset, false, H, false)) (* CLHU *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b01) = Some(CLoad(rd, cb, rt, offset, true, H, false)) (* CLH *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CLoad(rd, cb, rt, offset, false, W, false)) (* CLWU *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b1 : 0b10) = Some(CLoad(rd, cb, rt, offset, true, W, false)) (* CLW *) -function clause decode (0b110010 : (regno) rd : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CLoad(rd, cb, rt, offset, false, D, false)) (* CLD *) - -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, B, true)) (* CLLBU *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, B, true)) (* CLLB *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, H, true)) (* CLLHU *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, H, true)) (* CLLH *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, W, true)) (* CLLWU *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b1 : 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, W, true)) (* CLLW *) -function clause decode (0b010010 : 0b10000 : (regno) rd : (regno) cb : 0b00000001 : 0b0 : 0b11) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, D, true)) (* CLLD *) - -function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b00) = Some(CStore(rs, cb, rt, 0b00000, offset, B, false)) (* CSB *) -function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b01) = Some(CStore(rs, cb, rt, 0b00000, offset, H, false)) (* CSH *) -function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b10) = Some(CStore(rs, cb, rt, 0b00000, offset, W, false)) (* CSW *) -function clause decode (0b111010 : (regno) rs : (regno) cb: (regno) rt : (bit[8]) offset : 0b0 : 0b11) = Some(CStore(rs, cb, rt, 0b00000, offset, D, false)) (* CSD *) - -function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b00) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, B, true)) (* CSCB *) -function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b01) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, H, true)) (* CSCH *) -function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b10) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, W, true)) (* CSCW *) -function clause decode (0b010010 : 0b10000 : (regno) rs : (regno) cb : (regno) rd : 0b0000 : 0b11) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, D, true)) (* CSCD *) - -function clause decode (0b111110 : (regno) cs : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CSC(cs, cb, rt, 0b00000, offset, false)) -function clause decode (0b010010 : 0b10000 : (regno) cs : (regno) cb: (regno) rd : 0b00 : 0b0111) = Some(CSC(cs, cb, 0b00000, rd, 0b00000000000, true)) - -function clause decode (0b110110 : (regno) cd : (regno) cb: (regno) rt : (bit[11]) offset) = Some(CLC(cd, cb, rt, offset, false)) -function clause decode (0b010010 : 0b10000 : (regno) cd : (regno) cb: 0b0000000 : 0b1111) = Some(CLC(cd, cb, 0b00000, 0b00000000000, true)) - -function clause decode (0b010010 : 0b00100 : (regno) rt : 0x0006) = Some(C2Dump(rt)) - -(* Operations that extract parts of a capability into GPR *) - -union ast member (regno, regno) CGetPerm -union ast member (regno, regno) CGetType -union ast member (regno, regno) CGetBase -union ast member (regno, regno) CGetLen -union ast member (regno, regno) CGetTag -union ast member (regno, regno) CGetSealed -union ast member (regno, regno) CGetOffset +*/ + +/* One arg */ +function clause decode (0b010010 @ 0b00000 @ rd : regno @ 0b00001 @ 0b11111 @ 0b111111) = Some(CGetCause(rd)) +function clause decode (0b010010 @ 0b00000 @ rs : regno @ 0b00010 @ 0b11111 @ 0b111111) = Some(CSetCause(rs)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ 0b00000 @ 0b11111 @ 0b111111) = Some(CGetPCC(cd)) +function clause decode (0b010010 @ 0b00000 @ cb : regno @ 0b00011 @ 0b11111 @ 0b111111) = Some(CJALR(0b00000, cb, false)) /* CJR */ + +/* Two arg */ +function clause decode (0b010010 @ 0b00000 @ cs : regno @ rt : regno @ 0b01000 @ 0b111111) = Some(CCheckPerm(cs, rt)) +function clause decode (0b010010 @ 0b00000 @ cs : regno @ cb : regno @ 0b01001 @ 0b111111) = Some(CCheckType(cs, cb)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ 0b01011 @ 0b111111) = Some(CClearTag(cd, cb)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ 0b01010 @ 0b111111) = Some(CMOVX(cd, cs, 0b00000, false)) /* CMOVE */ +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ 0b01100 @ 0b111111) = Some(CJALR(cd, cb, true)) /* CJALR */ + +/* Capability Inspection */ +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00000 @ 0b111111) = Some(CGetPerm(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00001 @ 0b111111) = Some(CGetType(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00010 @ 0b111111) = Some(CGetBase(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00011 @ 0b111111) = Some(CGetLen(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00100 @ 0b111111) = Some(CGetTag(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00101 @ 0b111111) = Some(CGetSealed(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ 0b00110 @ 0b111111) = Some(CGetOffset(rd, cb)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ rs : regno @ 0b00111 @ 0b111111) = Some(CGetPCCSetOffset(cd, rs)) + +/* Three operand */ + +/* Capability Modification */ +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ ct : regno @ 0b001011) = Some(CSeal(cd, cs, ct)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ ct : regno @ 0b001100) = Some(CUnseal(cd, cs, ct)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rt : regno @ 0b001101) = Some(CAndPerm(cd, cs, rt)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rt : regno @ 0b001111) = Some(CSetOffset(cd, cs, rt)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rt : regno @ 0b001000) = Some(CSetBounds(cd, cs, rt)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rt : regno @ 0b001001) = Some(CSetBoundsExact(cd, cs, rt)) + + +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ rt : regno @ 0b010001) = Some(CIncOffset(cd, cb, rt)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ ct : regno @ 0b011101) = Some(CBuildCap(cd, cb, ct)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ ct : regno @ 0b011110) = Some(CCopyType(cd, cb, ct)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ ct : regno @ 0b011111) = Some(CCSeal(cd, cs, ct)) + +/* Pointer Arithmetic */ +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ ct : regno @ 0b010010) = Some(CToPtr(rd, cb, ct)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cb : regno @ rs : regno @ 0b010011) = Some(CFromPtr(cd, cb, rs)) +function clause decode (0b010010 @ 0b00000 @ rt : regno @ cb : regno @ cs : regno @ 0b001010) = Some(CSub(rt, cb, cs)) +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rs : regno @ 0b011011) = Some(CMOVX(cd, cs, rs, false)) /* CMOVZ */ +function clause decode (0b010010 @ 0b00000 @ cd : regno @ cs : regno @ rs : regno @ 0b011100) = Some(CMOVX(cd, cs, rs, true)) /* CMOVN */ + +/* Pointer Comparison */ +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b010100) = Some(CPtrCmp(rd, cb, cs, CEQ)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b010101) = Some(CPtrCmp(rd, cb, cs, CNE)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b010110) = Some(CPtrCmp(rd, cb, cs, CLT)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b010111) = Some(CPtrCmp(rd, cb, cs, CLE)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b011000) = Some(CPtrCmp(rd, cb, cs, CLTU)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b011001) = Some(CPtrCmp(rd, cb, cs, CLEU)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b011010) = Some(CPtrCmp(rd, cb, cs, CEXEQ)) +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ cs : regno @ 0b100001) = Some(CPtrCmp(rd, cb, cs, CNEXEQ)) + +function clause decode (0b010010 @ 0b00000 @ rd : regno @ cb : regno @ ct : regno @ 0b100000) = Some(CTestSubset(rd, cb, ct)) + +function clause decode (0b010010 @ 0b01001 @ cd : regno @ imm : bits(16)) = Some(CBX(cd, imm, true)) /* CBTU */ +function clause decode (0b010010 @ 0b01010 @ cd : regno @ imm : bits(16)) = Some(CBX(cd, imm, false)) /* CBTS */ +function clause decode (0b010010 @ 0b10001 @ cd : regno @ imm : bits(16)) = Some(CBZ(cd, imm, false)) /* CBEZ */ +function clause decode (0b010010 @ 0b10010 @ cd : regno @ imm : bits(16)) = Some(CBZ(cd, imm, true)) /* CBNZ */ + +function clause decode (0b010010 @ 0b00101 @ 0b00000 @ 0b00000 @ 0b11111111111) = Some(CReturn) +function clause decode (0b010010 @ 0b00101 @ cs : regno @ cb : regno @ selector : bits(11)) = Some(CCall(cs, cb, selector)) + +function clause decode (0b010010 @ 0b01111 @ 0b00000 @ imm : bits(16)) = Some(ClearRegs(GPLo, imm)) +function clause decode (0b010010 @ 0b01111 @ 0b00001 @ imm : bits(16)) = Some(ClearRegs(GPHi, imm)) +function clause decode (0b010010 @ 0b01111 @ 0b00010 @ imm : bits(16)) = Some(ClearRegs(CLo, imm)) +function clause decode (0b010010 @ 0b01111 @ 0b00011 @ imm : bits(16)) = Some(ClearRegs(CHi, imm)) + +function clause decode (0b010010 @ 0b10011 @ cd : regno @ cb : regno @ imm : bits(11)) = Some(CIncOffsetImmediate(cd, cb, imm)) +function clause decode (0b010010 @ 0b10100 @ cd : regno @ cb : regno @ imm : bits(11)) = Some(CSetBoundsImmediate(cd, cb, imm)) + +function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b00) = Some(CLoad(rd, cb, rt, offset, false, B, false)) /* CLBU */ +function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b1 @ 0b00) = Some(CLoad(rd, cb, rt, offset, true, B, false)) /* CLB */ +function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b01) = Some(CLoad(rd, cb, rt, offset, false, H, false)) /* CLHU */ +function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b1 @ 0b01) = Some(CLoad(rd, cb, rt, offset, true, H, false)) /* CLH */ +function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b10) = Some(CLoad(rd, cb, rt, offset, false, W, false)) /* CLWU */ +function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b1 @ 0b10) = Some(CLoad(rd, cb, rt, offset, true, W, false)) /* CLW */ +function clause decode (0b110010 @ rd : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b11) = Some(CLoad(rd, cb, rt, offset, false, D, false)) /* CLD */ + +function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b0 @ 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, B, true)) /* CLLBU */ +function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b1 @ 0b00) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, B, true)) /* CLLB */ +function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b0 @ 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, H, true)) /* CLLHU */ +function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b1 @ 0b01) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, H, true)) /* CLLH */ +function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b0 @ 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, W, true)) /* CLLWU */ +function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b1 @ 0b10) = Some(CLoad(rd, cb, 0b00000, 0b00000000, true, W, true)) /* CLLW */ +function clause decode (0b010010 @ 0b10000 @ rd : regno @ cb : regno @ 0b00000001 @ 0b0 @ 0b11) = Some(CLoad(rd, cb, 0b00000, 0b00000000, false, D, true)) /* CLLD */ + +function clause decode (0b111010 @ rs : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b00) = Some(CStore(rs, cb, rt, 0b00000, offset, B, false)) /* CSB */ +function clause decode (0b111010 @ rs : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b01) = Some(CStore(rs, cb, rt, 0b00000, offset, H, false)) /* CSH */ +function clause decode (0b111010 @ rs : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b10) = Some(CStore(rs, cb, rt, 0b00000, offset, W, false)) /* CSW */ +function clause decode (0b111010 @ rs : regno @ cb : regno@ rt : regno @ offset : bits(8) @ 0b0 @ 0b11) = Some(CStore(rs, cb, rt, 0b00000, offset, D, false)) /* CSD */ + +function clause decode (0b010010 @ 0b10000 @ rs : regno @ cb : regno @ rd : regno @ 0b0000 @ 0b00) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, B, true)) /* CSCB */ +function clause decode (0b010010 @ 0b10000 @ rs : regno @ cb : regno @ rd : regno @ 0b0000 @ 0b01) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, H, true)) /* CSCH */ +function clause decode (0b010010 @ 0b10000 @ rs : regno @ cb : regno @ rd : regno @ 0b0000 @ 0b10) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, W, true)) /* CSCW */ +function clause decode (0b010010 @ 0b10000 @ rs : regno @ cb : regno @ rd : regno @ 0b0000 @ 0b11) = Some(CStore(rs, cb, 0b00000, rd, 0b00000000, D, true)) /* CSCD */ + +function clause decode (0b111110 @ cs : regno @ cb : regno@ rt : regno @ offset : bits(11)) = Some(CSC(cs, cb, rt, 0b00000, offset, false)) +function clause decode (0b010010 @ 0b10000 @ cs : regno @ cb : regno@ rd : regno @ 0b00 @ 0b0111) = Some(CSC(cs, cb, 0b00000, rd, 0b00000000000, true)) + +function clause decode (0b110110 @ cd : regno @ cb : regno@ rt : regno @ offset : bits(11)) = Some(CLC(cd, cb, rt, offset, false)) +function clause decode (0b010010 @ 0b10000 @ cd : regno @ cb : regno@ 0b0000000 @ 0b1111) = Some(CLC(cd, cb, 0b00000, 0b00000000000, true)) + +function clause decode (0b010010 @ 0b00100 @ rt : regno @ 0x0006) = Some(C2Dump(rt)) + +/* Operations that extract parts of a capability into GPR */ + +union clause ast = CGetPerm : (regno, regno) +union clause ast = CGetType : (regno, regno) +union clause ast = CGetBase : (regno, regno) +union clause ast = CGetLen : (regno, regno) +union clause ast = CGetTag : (regno, regno) +union clause ast = CGetSealed : (regno, regno) +union clause ast = CGetOffset : (regno, regno) function clause execute (CGetPerm(rd, cb)) = { - (* START_CGetPerms *) + /* START_CGetPerms */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in - wGPR(rd) := EXTZ(getCapPerms(capVal)); - (* END_CGetPerms *) + wGPR(rd) = EXTZ(getCapPerms(capVal)); + /* END_CGetPerms */ } function clause execute (CGetType(rd, cb)) = { - (* START_CGetType *) + /* START_CGetType */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in - wGPR(rd) := if (capVal.sealed) + wGPR(rd) = if (capVal.sealed) then EXTZ(capVal.otype) else (bitone ^^ 64) - (* END_CGetType *) + /* END_CGetType */ } function clause execute (CGetBase(rd, cb)) = { - (* START_CGetBase *) + /* START_CGetBase */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in - wGPR(rd) := (bit[64]) (getCapBase(capVal)); - (* END_CGetBase *) + wGPR(rd) = to_bits(64, getCapBase(capVal)); + /* END_CGetBase */ } function clause execute (CGetOffset(rd, cb)) = { - (* START_CGetOffset *) + /* START_CGetOffset */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in - wGPR(rd) := (bit[64]) (getCapOffset(capVal)); - (* END_CGetOffset *) + wGPR(rd) = to_bits(64, getCapOffset(capVal)); + /* END_CGetOffset */ } function clause execute (CGetLen(rd, cb)) = { - (* START_CGetLen *) + /* START_CGetLen */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in let len65 = getCapLength(capVal) in - wGPR(rd) := (if len65 > MAX_U64 then MAX_U64 else len65); - (*let (uint64) len64 = (if len65 > MAX_U64 then MAX_U64 else len65) in - wGPR(rd) := (bit[64]) len64;*) - (* END_CGetLen *) + wGPR(rd) = to_bits(64, if len65 > MAX_U64 then MAX_U64 else len65); + /* END_CGetLen */ } function clause execute (CGetTag(rd, cb)) = { - (* START_CGetTag *) + /* START_CGetTag */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in - wGPR(rd) := EXTZ([capVal.tag]); - (* END_CGetTag *) + wGPR(rd) = EXTZ(capVal.tag); + /* END_CGetTag */ } function clause execute (CGetSealed(rd, cb)) = { - (* START_CGetSealed *) + /* START_CGetSealed */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else let capVal = readCapReg(cb) in - wGPR(rd) := EXTZ([capVal.sealed]); - (* END_CGetSealed *) + wGPR(rd) = EXTZ(capVal.sealed); + /* END_CGetSealed */ } -union ast member regno CGetPCC +union clause ast = CGetPCC : regno function clause execute (CGetPCC(cd)) = { - (* START_CGetPCC *) + /* START_CGetPCC */ checkCP2usable(); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else let pcc = (capRegToCapStruct(PCC)) in let (success, pcc2) = setCapOffset(pcc, PC) in - {assert (success, ""); (* guaranteed to be in-bounds *) + {assert (success, ""); /* guaranteed to be in-bounds */ writeCapReg(cd, pcc2)}; - (* END_CGetPCC *) + /* END_CGetPCC */ } -union ast member (regno, regno) CGetPCCSetOffset +union clause ast = CGetPCCSetOffset : (regno, regno) function clause execute (CGetPCCSetOffset(cd, rs)) = { - (* START_CGetPCCSetOffset *) + /* START_CGetPCCSetOffset */ checkCP2usable(); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) @@ -315,45 +313,45 @@ function clause execute (CGetPCCSetOffset(cd, rs)) = writeCapReg(cd, newPCC) else writeCapReg(cd, int_to_cap(rs_val)); - (* END_CGetPCCSetOffset *) + /* END_CGetPCCSetOffset */ } -(* Get and Set CP2 cause register *) +/* Get and Set CP2 cause register */ -union ast member regno CGetCause +union clause ast = CGetCause : regno function clause execute (CGetCause(rd)) = { - (* START_CGetCause *) + /* START_CGetCause */ checkCP2usable(); if not (pcc_access_system_regs ()) then raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) else - wGPR(rd) := EXTZ(CapCause) - (* END_CGetCause *) + wGPR(rd) = EXTZ(CapCause.bits()) + /* END_CGetCause */ } -union ast member (regno) CSetCause -function clause execute (CSetCause((regno) rt)) = +union clause ast = CSetCause : regno +function clause execute (CSetCause(rt)) = { - (* START_CSetCause *) + /* START_CSetCause */ checkCP2usable(); if not (pcc_access_system_regs ()) then raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation) else { - (bit[64]) rt_val := rGPR(rt); - CapCause.ExcCode := rt_val[15..8]; - CapCause.RegNum := rt_val[7..0]; + let rt_val = rGPR(rt); + CapCause->ExcCode() = rt_val[15..8]; + CapCause->RegNum() = rt_val[7..0]; } - (* END_CSetCause *) + /* END_CSetCause */ } -union ast member regregreg CAndPerm +union clause ast = CAndPerm : (regno, regno, regno) function clause execute(CAndPerm(cd, cb, rt)) = { - (* START_CAndPerm *) + /* START_CAndPerm */ checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := rGPR(rt); + let cb_val = readCapReg(cb); + let rt_val = rGPR(rt); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -366,18 +364,18 @@ function clause execute(CAndPerm(cd, cb, rt)) = let perms = getCapPerms(cb_val) in let newCap = setCapPerms(cb_val, (perms & rt_val[30..0])) in writeCapReg(cd, newCap); - (* END_CAndPerm *) + /* END_CAndPerm */ } -union ast member regregreg CToPtr +union clause ast = CToPtr : (regno, regno, regno) function clause execute(CToPtr(rd, cb, ct)) = { - (* START_CToPtr *) + /* START_CToPtr */ checkCP2usable(); - ct_val := readCapReg(ct); - cb_val := readCapReg(cb); + let ct_val = readCapReg(ct); + let cb_val = readCapReg(cb); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else if (register_inaccessible(ct)) then @@ -392,40 +390,40 @@ function clause execute(CToPtr(rd, cb, ct)) = let cbTop = getCapTop(cb_val) in let ctBase = getCapBase(ct_val) in let ctTop = getCapTop(ct_val) in - wGPR(rd) := if (not (cb_val.tag)) | + wGPR(rd) = if (not (cb_val.tag)) | (cbBase < ctBase) | (cbTop > ctTop) then - ((bit[64]) 0) + zeros() else - (bit[64])(getCapCursor(cb_val) - ctBase) + to_bits(64, getCapCursor(cb_val) - ctBase) } - (* END_CToPtr *) + /* END_CToPtr */ } -union ast member regregreg CSub +union clause ast = CSub : (regno, regno, regno) function clause execute(CSub(rd, cb, ct)) = { - (* START_CSub *) + /* START_CSub */ checkCP2usable(); - ct_val := readCapReg(ct); - cb_val := readCapReg(cb); + let ct_val = readCapReg(ct); + let cb_val = readCapReg(cb); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else if (register_inaccessible(ct)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) else { - wGPR(rd) := (bit[64])(to_svec(getCapCursor(cb_val) - getCapCursor(ct_val))) + wGPR(rd) = to_bits(64, getCapCursor(cb_val) - getCapCursor(ct_val)) } - (* END_CSub *) + /* END_CSub */ } -union ast member (regno, regno, regno, CPtrCmpOp) CPtrCmp +union clause ast = CPtrCmp : (regno, regno, regno, CPtrCmpOp) function clause execute(CPtrCmp(rd, cb, ct, op)) = { - (* START_CPtrCmp *) + /* START_CPtrCmp */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) @@ -433,48 +431,49 @@ function clause execute(CPtrCmp(rd, cb, ct, op)) = raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) else { - cb_val := readCapReg(cb); - ct_val := readCapReg(ct); - equal := false; - ltu := false; - lts := false; + let cb_val = readCapReg(cb); + let ct_val = readCapReg(ct); + equal = false; + ltu = false; + lts = false; if (cb_val.tag != ct_val.tag) then { if not (cb_val.tag) then { - ltu := true; - lts := true; + ltu = true; + lts = true; } } else { - cursor1 := getCapCursor(cb_val); - cursor2 := getCapCursor(ct_val); - equal := (cursor1 == cursor2); - ltu := (cursor1 < cursor2); - lts := (((bit[64])cursor1) <_s ((bit[64])cursor2)); + cursor1 = getCapCursor(cb_val); + cursor2 = getCapCursor(ct_val); + equal = (cursor1 == cursor2); + ltu = (cursor1 < cursor2); + lts = to_bits(64, cursor1) <_s to_bits(64, cursor2); }; - wGPR(rd) := EXTZ ((bool[1]) (switch (op) { - case CEQ -> [equal] - case CNE -> [not (equal)] - case CLT -> [lts] - case CLE -> [lts | equal] - case CLTU -> [ltu] - case CLEU -> [ltu | equal] - case CEXEQ -> [cb_val == ct_val] - case CNEXEQ -> [cb_val != ct_val] - })) + let cmp : bool = match op { + CEQ => equal, + CNE => not (equal), + CLT => lts, + CLE => lts | equal, + CLTU => ltu, + CLEU => ltu | equal, + CEXEQ => cb_val == ct_val, + CNEXEQ => cb_val != ct_val + }; + wGPR(rd) = EXTZ (cmp) } - (* END_CPtrCmp *) + /* END_CPtrCmp */ } -union ast member regregreg CIncOffset +union clause ast = CIncOffset : (regno, regno, regno) function clause execute (CIncOffset(cd, cb, rt)) = { - (* START_CIncOffset *) + /* START_CIncOffset */ checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := rGPR(rt); + cb_val = readCapReg(cb); + rt_val = rGPR(rt); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -486,17 +485,17 @@ function clause execute (CIncOffset(cd, cb, rt)) = if (success) then writeCapReg(cd, newCap) else - writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) - (* END_CIncOffset *) + writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val)) + /* END_CIncOffset */ } -union ast member (regno, regno, bit[11]) CIncOffsetImmediate +union clause ast = CIncOffsetImmediate : (regno, regno, bits(11)) function clause execute (CIncOffsetImmediate(cd, cb, imm)) = { - (* START_CIncOffsetImmediate *) + /* START_CIncOffsetImmediate */ checkCP2usable(); - cb_val := readCapReg(cb); - let (bit[64]) imm64 = EXTS(imm) in + let cb_val = readCapReg(cb); + let imm64 : bits(64) = EXTS(imm) in if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -508,17 +507,17 @@ function clause execute (CIncOffsetImmediate(cd, cb, imm)) = if (success) then writeCapReg(cd, newCap) else - writeCapReg(cd, int_to_cap(getCapBase(cb_val) + imm64)) - (* END_CIncOffsetImmediate *) + writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + imm64)) + /* END_CIncOffsetImmediate */ } -union ast member regregreg CSetOffset +union clause ast = CSetOffset : (regno, regno, regno) function clause execute (CSetOffset(cd, cb, rt)) = { - (* START_CSetOffset *) + /* START_CSetOffset */ checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := rGPR(rt); + let cb_val = readCapReg(cb); + let rt_val = rGPR(rt); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -530,21 +529,21 @@ function clause execute (CSetOffset(cd, cb, rt)) = if (success) then writeCapReg(cd, newCap) else - writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) - (* END_CSetOffset *) + writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val)) + /* END_CSetOffset */ } -union ast member regregreg CSetBounds +union clause ast = CSetBounds : (regno, regno, regno) function clause execute (CSetBounds(cd, cb, rt)) = { - (* START_CSetBounds *) + /* START_CSetBounds */ checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := unsigned(rGPR(rt)); - cursor := getCapCursor(cb_val); - base := getCapBase(cb_val); - top := getCapTop(cb_val); - newTop := cursor + rt_val; + let cb_val = readCapReg(cb); + let rt_val = unsigned(rGPR(rt)); + cursor = getCapCursor(cb_val); + base = getCapBase(cb_val); + top = getCapTop(cb_val); + newTop = cursor + rt_val; if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -558,22 +557,22 @@ function clause execute (CSetBounds(cd, cb, rt)) = else if (newTop > top) then raise_c2_exception(CapEx_LengthViolation, cb) else - let (_, newCap) = setCapBounds(cb_val, (bit[64]) cursor, (bit[65]) newTop) in - writeCapReg(cd, newCap) (* ignore exact *) - (* END_CSetBounds *) + let (_, newCap) = setCapBounds(cb_val, to_bits(64, cursor), to_bits(65, newTop)) in + writeCapReg(cd, newCap) /* ignore exact */ + /* END_CSetBounds */ } -union ast member (regno, regno, bit[11]) CSetBoundsImmediate +union clause ast = CSetBoundsImmediate : (regno, regno, bits(11)) function clause execute (CSetBoundsImmediate(cd, cb, imm)) = { - (* START_CSetBoundsImmedate *) + /* START_CSetBoundsImmedate */ checkCP2usable(); - cb_val := readCapReg(cb); - immU := unsigned(imm); - cursor := getCapCursor(cb_val); - base := getCapBase(cb_val); - top := getCapTop(cb_val); - newTop := cursor + immU; + cb_val = readCapReg(cb); + immU = unsigned(imm); + cursor = getCapCursor(cb_val); + base = getCapBase(cb_val); + top = getCapTop(cb_val); + newTop = cursor + immU; if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -587,22 +586,22 @@ function clause execute (CSetBoundsImmediate(cd, cb, imm)) = else if (newTop > top) then raise_c2_exception(CapEx_LengthViolation, cb) else - let (_, newCap) = setCapBounds(cb_val, (bit[64]) cursor, (bit[65]) newTop) in - writeCapReg(cd, newCap) (* ignore exact *) - (* END_CSetBoundsImmediate *) + let (_, newCap) = setCapBounds(cb_val, to_bits(64, cursor), to_bits(65, newTop)) in + writeCapReg(cd, newCap) /* ignore exact */ + /* END_CSetBoundsImmediate */ } -union ast member regregreg CSetBoundsExact +union clause ast = CSetBoundsExact : (regno, regno, regno) function clause execute (CSetBoundsExact(cd, cb, rt)) = { - (* START_CSetBoundsExact *) + /* START_CSetBoundsExact */ checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := unsigned(rGPR(rt)); - cursor := getCapCursor(cb_val); - base := getCapBase(cb_val); - top := getCapTop(cb_val); - newTop := cursor + rt_val; + cb_val = readCapReg(cb); + rt_val = unsigned(rGPR(rt)); + cursor = getCapCursor(cb_val); + base = getCapBase(cb_val); + top = getCapTop(cb_val); + newTop = cursor + rt_val; if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -616,18 +615,18 @@ function clause execute (CSetBoundsExact(cd, cb, rt)) = else if (newTop > top) then raise_c2_exception(CapEx_LengthViolation, cb) else - let (exact, newCap) = setCapBounds(cb_val, (bit[64]) cursor, (bit[65]) newTop) in + let (exact, newCap) = setCapBounds(cb_val, to_bits(64, cursor), to_bits(65, newTop)) in if not (exact) then raise_c2_exception(CapEx_InexactBounds, cb) else writeCapReg(cd, newCap) - (* END_CSetBoundsExact *) + /* END_CSetBoundsExact */ } -union ast member (regno, regno) CClearTag +union clause ast = CClearTag : (regno, regno) function clause execute (CClearTag(cd, cb)) = { - (* START_CClearTag *) + /* START_CClearTag */ checkCP2usable(); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) @@ -635,60 +634,60 @@ function clause execute (CClearTag(cd, cb)) = raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else { - cb_val := readCapReg(cb); - writeCapReg(cd, {cb_val with tag = false}); + cb_val = readCapReg(cb); + writeCapReg(cd, {cb_val with tag=false}); } - (* END_CClearTag *) + /* END_CClearTag */ } -union ast member (regno,regno,regno,bool) CMOVX +union clause ast = CMOVX : (regno,regno,regno,bool) function clause execute (CMOVX(cd, cb, rt, ismovn)) = { - (* START_CMOVX *) + /* START_CMOVX */ checkCP2usable(); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if ((rGPR(rt) == 0) ^ ismovn) then - writeCapReg(cd) := readCapReg(cb); - (* END_CMOVX *) + else if ((rGPR(rt) == zeros()) ^ ismovn) then + writeCapReg(cd) = readCapReg(cb); + /* END_CMOVX */ } -union ast member (ClearRegSet, bit[16]) ClearRegs -function clause execute (ClearRegs(regset, mask)) = +union clause ast = ClearRegs : (ClearRegSet, bits(16)) +function clause execute (ClearRegs(regset, m)) = { - (* START_ClearRegs *) + /* START_ClearRegs */ if ((regset == CLo) | (regset == CHi)) then checkCP2usable(); if (regset == CHi) then foreach (i from 0 to 15) - let r = ((bit[5]) (i+16)) in - if (mask[i] & register_inaccessible(r)) then + let r = to_bits(5, i+16) in + if (m[i] & register_inaccessible(r)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, r); foreach (i from 0 to 15) - if (mask[i]) then - switch (regset) { - case GPLo -> wGPR((bit[5])i) := 0 - case GPHi -> wGPR((bit[5])(i+16)) := 0 - case CLo -> writeCapReg((bit[5]) i) := null_cap - case CHi -> writeCapReg((bit[5]) (i+16)) := null_cap + if (m[i]) then + match regset { + GPLo => wGPR(to_bits(5, i)) = zeros(), + GPHi => wGPR(to_bits(5, i+16)) = zeros(), + CLo => writeCapReg(to_bits(5, i)) = null_cap, + CHi => writeCapReg(to_bits(5, i+16)) = null_cap } - (* END_ClearRegs *) + /* END_ClearRegs */ } -union ast member regregreg CFromPtr +union clause ast = CFromPtr : (regno, regno, regno) function clause execute (CFromPtr(cd, cb, rt)) = { - (* START_CFromPtr *) + /* START_CFromPtr */ checkCP2usable(); - cb_val := readCapReg(cb); - rt_val := rGPR(rt); + cb_val = readCapReg(cb); + rt_val = rGPR(rt); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) - else if (rt == 0) then + else if (rt == 0b00000) then writeCapReg(cd, null_cap) else if not (cb_val.tag) then raise_c2_exception(CapEx_TagViolation, cb) @@ -699,24 +698,24 @@ function clause execute (CFromPtr(cd, cb, rt)) = if (success) then writeCapReg(cd, newCap) else - writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val)) - (* END_CFromPtr *) + writeCapReg(cd, int_to_cap(to_bits(64, getCapBase(cb_val)) + rt_val)) + /* END_CFromPtr */ } -union ast member regregreg CBuildCap +union clause ast = CBuildCap : (regno, regno, regno) function clause execute (CBuildCap(cd, cb, ct)) = { - (* START_CBuildCap *) + /* START_CBuildCap */ checkCP2usable(); - cb_val := readCapReg(cb); - ct_val := readCapReg(ct); - cb_base := getCapBase(cb_val); - ct_base := getCapBase(ct_val); - cb_top := getCapTop(cb_val); - ct_top := getCapTop(ct_val); - cb_perms := getCapPerms(cb_val); - ct_perms := getCapPerms(ct_val); - ct_offset := getCapOffset(ct_val); + cb_val = readCapReg(cb); + ct_val = readCapReg(ct); + cb_base = getCapBase(cb_val); + ct_base = getCapBase(ct_val); + cb_top = getCapTop(cb_val); + ct_top = getCapTop(ct_val); + cb_perms = getCapPerms(cb_val); + ct_perms = getCapPerms(ct_val); + ct_offset = getCapOffset(ct_val); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -731,32 +730,32 @@ function clause execute (CBuildCap(cd, cb, ct)) = raise_c2_exception(CapEx_LengthViolation, cb) else if ct_top > cb_top then raise_c2_exception(CapEx_LengthViolation, cb) - else if ct_base > ct_top then (* check for length < 0 - possible because ct might be untagged *) + else if ct_base > ct_top then /* check for length < 0 - possible because ct might be untagged */ raise_c2_exception(CapEx_LengthViolation, ct) else if (ct_perms & cb_perms) != ct_perms then raise_c2_exception(CapEx_UserDefViolation, ct) else - let (exact, cd1) = setCapBounds(cb_val, (bit[64]) ct_base, (bit[65]) ct_top) in - let (representable, cd2) = setCapOffset(cd1, (bit[64]) ct_offset) in + let (exact, cd1) = setCapBounds(cb_val, to_bits(64, ct_base), to_bits(65, ct_top)) in + let (representable, cd2) = setCapOffset(cd1, to_bits(64, ct_offset)) in let cd3 = setCapPerms(cd2, ct_perms) in { - assert(exact, ""); (* base and top came from ct originally so will be exact *) - assert(representable, ""); (* similarly offset should be representable XXX except for fastRepCheck *) + assert(exact, ""); /* base and top came from ct originally so will be exact */ + assert(representable, ""); /* similarly offset should be representable XXX except for fastRepCheck */ writeCapReg(cd, cd3); } - (* END_CBuildCap *) + /* END_CBuildCap */ } -union ast member regregreg CCopyType +union clause ast = CCopyType : (regno, regno, regno) function clause execute (CCopyType(cd, cb, ct)) = { - (* START_CCopyType *) + /* START_CCopyType */ checkCP2usable(); - cb_val := readCapReg(cb); - ct_val := readCapReg(ct); - cb_base := getCapBase(cb_val); - cb_top := getCapTop(cb_val); - ct_otype := unsigned(ct_val.otype); + cb_val = readCapReg(cb); + ct_val = readCapReg(ct); + cb_base = getCapBase(cb_val); + cb_top = getCapTop(cb_val); + ct_otype = unsigned(ct_val.otype); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -773,23 +772,23 @@ function clause execute (CCopyType(cd, cb, ct)) = else if ct_otype >= cb_top then raise_c2_exception(CapEx_LengthViolation, cb) else - let (success, cap) = setCapOffset(cb_val, (bit[64]) (ct_otype - cb_base)) in { - assert(success, ""); (* offset is in bounds so must succeed *) + let (success, cap) = setCapOffset(cb_val, to_bits(64, ct_otype - cb_base)) in { + assert(success, ""); /* offset is in bounds so must succeed */ writeCapReg(cd, cap); } } else writeCapReg(cd, int_to_cap(bitone ^^ 64)) - (* END_CCopyType *) + /* END_CCopyType */ } -union ast member (regno, regno) CCheckPerm +union clause ast = CCheckPerm : (regno, regno) function clause execute (CCheckPerm(cs, rt)) = { - (* START_CCheckPerm *) + /* START_CCheckPerm */ checkCP2usable(); - cs_val := readCapReg(cs); - cs_perms := (bit[64]) (EXTZ(getCapPerms(cs_val))); - rt_perms := rGPR(rt); + cs_val = readCapReg(cs); + cs_perms : bits(64) = EXTZ(getCapPerms(cs_val)); + rt_perms = rGPR(rt); if (register_inaccessible(cs)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) else if not (cs_val.tag) then @@ -798,16 +797,16 @@ function clause execute (CCheckPerm(cs, rt)) = raise_c2_exception(CapEx_UserDefViolation, cs) else () - (* END_CCheckPerm *) + /* END_CCheckPerm */ } -union ast member (regno, regno) CCheckType +union clause ast = CCheckType : (regno, regno) function clause execute (CCheckType(cs, cb)) = { - (* START_CCheckType *) + /* START_CCheckType */ checkCP2usable(); - cs_val := readCapReg(cs); - cb_val := readCapReg(cb); + cs_val = readCapReg(cs); + cb_val = readCapReg(cb); if (register_inaccessible(cs)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) else if (register_inaccessible(cb)) then @@ -824,54 +823,54 @@ function clause execute (CCheckType(cs, cb)) = raise_c2_exception(CapEx_TypeViolation, cs) else () - (* END_CCheckType *) + /* END_CCheckType */ } -union ast member regregreg CTestSubset +union clause ast = CTestSubset : (regno, regno, regno) function clause execute (CTestSubset(rd, cb, ct)) = { - (* START_CTestSubset *) + /* START_CTestSubset */ checkCP2usable(); - cb_val := readCapReg(cb); - ct_val := readCapReg(ct); - ct_top := getCapTop(ct_val); - ct_base := getCapBase(ct_val); - ct_perms := getCapPerms(ct_val); - cb_top := getCapTop(cb_val); - cb_base := getCapBase(cb_val); - cb_perms := getCapPerms(cb_val); + cb_val = readCapReg(cb); + ct_val = readCapReg(ct); + ct_top = getCapTop(ct_val); + ct_base = getCapBase(ct_val); + ct_perms = getCapPerms(ct_val); + cb_top = getCapTop(cb_val); + cb_base = getCapBase(cb_val); + cb_perms = getCapPerms(cb_val); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else if (register_inaccessible(ct)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, ct) else { - (bit[64]) result := EXTZ(if (cb_val.tag != ct_val.tag) then - 0x0 + result : bits(1) = if (cb_val.tag != ct_val.tag) then + 0b0 else if (cb_val.sealed != ct_val.sealed) then - 0x0 + 0b0 else if (ct_base < cb_base) then - 0x0 + 0b0 else if (ct_top > cb_top) then - 0x0 + 0b0 else if ((ct_perms & cb_perms) != cb_perms) then - 0x0 + 0b0 else - 0x1); - wGPR(rd) := result; + 0b1; + wGPR(rd) = EXTZ(result); } - (* END_CTestSubset *) + /* END_CTestSubset */ } -union ast member regregreg CSeal +union clause ast = CSeal : (regno, regno, regno) function clause execute (CSeal(cd, cs, ct)) = { - (* START_CSeal *) + /* START_CSeal */ checkCP2usable(); - cs_val := readCapReg(cs); - ct_val := readCapReg(ct); - ct_cursor := getCapCursor(ct_val); - ct_top := getCapTop(ct_val); - ct_base := getCapBase(ct_val); + cs_val = readCapReg(cs); + ct_val = readCapReg(ct); + ct_cursor = getCapCursor(ct_val); + ct_top = getCapTop(ct_val); + ct_base = getCapBase(ct_val); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cs)) then @@ -895,24 +894,24 @@ function clause execute (CSeal(cd, cs, ct)) = else if (ct_cursor > max_otype) then raise_c2_exception(CapEx_LengthViolation, ct) else - let (success, newCap) = sealCap(cs_val, (bit[24]) ct_cursor) in + let (success, newCap) = sealCap(cs_val, to_bits(24, ct_cursor)) in if not (success) then raise_c2_exception(CapEx_InexactBounds, cs) else writeCapReg(cd, newCap) - (* END_CSeal *) + /* END_CSeal */ } -union ast member regregreg CCSeal +union clause ast = CCSeal : (regno, regno, regno) function clause execute (CCSeal(cd, cs, ct)) = { - (* START_CCSeal *) + /* START_CCSeal */ checkCP2usable(); - cs_val := readCapReg(cs); - ct_val := readCapReg(ct); - ct_cursor := getCapCursor(ct_val); - ct_top := getCapTop(ct_val); - ct_base := getCapBase(ct_val); + cs_val = readCapReg(cs); + ct_val = readCapReg(ct); + ct_cursor = getCapCursor(ct_val); + ct_top = getCapTop(ct_val); + ct_base = getCapBase(ct_val); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cs)) then @@ -936,22 +935,22 @@ function clause execute (CCSeal(cd, cs, ct)) = else if (ct_cursor > max_otype) then raise_c2_exception(CapEx_LengthViolation, ct) else - let (success, newCap) = sealCap(cs_val, (bit[24]) ct_cursor) in + let (success, newCap) = sealCap(cs_val, to_bits(24, ct_cursor)) in if not (success) then raise_c2_exception(CapEx_InexactBounds, cs) else writeCapReg(cd, newCap) - (* END_CCSeal *) + /* END_CCSeal */ } -union ast member regregreg CUnseal +union clause ast = CUnseal : (regno, regno, regno) function clause execute (CUnseal(cd, cs, ct)) = { - (* START_CUnseal *) + /* START_CUnseal */ checkCP2usable(); - cs_val := readCapReg(cs); - ct_val := readCapReg(ct); - ct_cursor := getCapCursor(ct_val); + cs_val = readCapReg(cs); + ct_val = readCapReg(ct); + ct_cursor = getCapCursor(ct_val); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cs)) then @@ -976,22 +975,22 @@ function clause execute (CUnseal(cd, cs, ct)) = raise_c2_exception(CapEx_LengthViolation, ct) else writeCapReg(cd, {cs_val with - sealed=false; - otype=0; + sealed=false, + otype=zeros(), global=(cs_val.global & ct_val.global) }) - (* END_CUnseal *) + /* END_CUnseal */ } -union ast member (regno, regno, bit[11]) CCall -function clause execute (CCall(cs, cb, 0b00000000000)) = (* selector=0 *) +union clause ast = CCall : (regno, regno, bits(11)) +function clause execute (CCall(cs, cb, 0b00000000000)) = /* selector=0 */ { - (* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation *) - (* START_CCall *) + /* Partial implementation of CCall with checks in hardware, but raising a trap to perform trusted stack manipulation */ + /* START_CCall */ checkCP2usable(); - cs_val := readCapReg(cs); - cb_val := readCapReg(cb); - cs_cursor := getCapCursor(cs_val); + cs_val = readCapReg(cs); + cb_val = readCapReg(cb); + cs_cursor = getCapCursor(cs_val); if (register_inaccessible(cs)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) else if (register_inaccessible(cb)) then @@ -1016,17 +1015,17 @@ function clause execute (CCall(cs, cb, 0b00000000000)) = (* selector=0 *) raise_c2_exception(CapEx_LengthViolation, cs) else raise_c2_exception(CapEx_CallTrap, cs); - (* END_CCall *) + /* END_CCall */ } -function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *) +function clause execute (CCall(cs, cb, 0b00000000001)) = /* selector=1 */ { - (* Jump-like implementation of CCall that unseals arguments *) - (* START_CCall2 *) + /* Jump-like implementation of CCall that unseals arguments */ + /* START_CCall2 */ checkCP2usable(); - cs_val := readCapReg(cs); - cb_val := readCapReg(cb); - cs_cursor := getCapCursor(cs_val); + cs_val = readCapReg(cs); + cb_val = readCapReg(cb); + cs_cursor = getCapCursor(cs_val); if (register_inaccessible(cs)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) else if (register_inaccessible(cb)) then @@ -1055,71 +1054,71 @@ function clause execute (CCall(cs, cb, 0b00000000001)) = (* selector=1 *) raise_c2_exception(CapEx_LengthViolation, cs) else let csUnsealed = capStructToCapReg({cs_val with - sealed=false; - otype=0; + sealed=false, + otype=zeros() }) in { - delayedPC := (bit[64]) (getCapOffset(cs_val)); - delayedPCC := csUnsealed; - branchPending := 0b1; - inCCallDelay := 0b1; - C26 := capStructToCapReg({cb_val with - sealed=false; - otype=0; + delayedPC = to_bits(64, getCapOffset(cs_val)); + delayedPCC = csUnsealed; + branchPending = 0b1; + inCCallDelay = 0b1; + C26 = capStructToCapReg({cb_val with + sealed=false, + otype=zeros() }); } - (* END_CCall2 *) + /* END_CCall2 */ } -union ast member unit CReturn +union clause ast = CReturn : unit function clause execute (CReturn) = { - (* START_CReturn *) + /* START_CReturn */ checkCP2usable(); raise_c2_exception_noreg(CapEx_ReturnTrap) - (* END_CReturn *) + /* END_CReturn */ } -union ast member (regno, bit[16], bool) CBX +union clause ast = CBX : (regno, bits(16), bool) function clause execute (CBX(cb, imm, invert)) = { - (* START_CBx *) + /* START_CBx */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else if (((readCapReg(cb)).tag) ^ invert) then { - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - delayedPC := PC + offset; - branchPending := 1; + let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in + delayedPC = PC + offset; + branchPending = 0b1; } - (* END_CBx *) + /* END_CBx */ } -union ast member (regno, bit[16], bool) CBZ +union clause ast = CBZ : (regno, bits(16), bool) function clause execute (CBZ(cb, imm, invert)) = { - (* START_CBz *) + /* START_CBz */ checkCP2usable(); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else if (((readCapReg(cb)) == null_cap) ^ invert) then { - let (bit[64]) offset = (EXTS(imm : 0b00) + 4) in - delayedPC := PC + offset; - branchPending := 1; + let offset : bits(64) = (EXTS(imm @ 0b00) + 4) in + delayedPC = PC + offset; + branchPending = 0b1; } - (* END_CBz *) + /* END_CBz */ } -union ast member (regno, regno, bool) CJALR +union clause ast = CJALR : (regno, regno, bool) function clause execute(CJALR(cd, cb, link)) = { - (* START_CJALR *) + /* START_CJALR */ checkCP2usable(); - cb_val := readCapReg(cb); - cb_ptr := getCapCursor(cb_val); - cb_top := getCapTop(cb_val); - cb_base:= getCapBase(cb_val); + cb_val = readCapReg(cb); + cb_ptr = getCapCursor(cb_val); + cb_top = getCapTop(cb_val); + cb_base= getCapBase(cb_val); if (link & register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -1134,7 +1133,7 @@ function clause execute(CJALR(cd, cb, link)) = raise_c2_exception(CapEx_LengthViolation, cb) else if ((cb_ptr + 4) > cb_top) then raise_c2_exception(CapEx_LengthViolation, cb) - else if ((cb_ptr mod 4) != 0) then + else if ((cb_ptr % 4) != 0) then SignalException(AdEL) else { @@ -1145,19 +1144,19 @@ function clause execute(CJALR(cd, cb, link)) = writeCapReg(cd, linkCap) else assert(false, ""); - delayedPC := (bit[64]) (getCapOffset(cb_val)); - delayedPCC := capStructToCapReg(cb_val); - branchPending := 1; + delayedPC = to_bits(64, getCapOffset(cb_val)); + delayedPCC = capStructToCapReg(cb_val); + branchPending = 0b1; } - (* END_CJALR *) + /* END_CJALR */ } -union ast member (regno, regno, regno, bit[8], bool, WordType, bool) CLoad +union clause ast = CLoad : (regno, regno, regno, bits(8), bool, WordType, bool) function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = { - (* START_CLoad *) + /* START_CLoad */ checkCP2usable(); - cb_val := readCapReg(cb); + cb_val = readCapReg(cb); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else if not (cb_val.tag) then @@ -1168,10 +1167,10 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = raise_c2_exception(CapEx_PermitLoadViolation, cb) else { - size := wordWidthBytes(width); - cursor := getCapCursor(cb_val); - vAddr := cursor + unsigned(rGPR(rt)) + (size*signed(offset)); - vAddr64:= (bit[64]) (to_svec(vAddr)); + size = wordWidthBytes(width); + cursor = getCapCursor(cb_val); + vAddr = cursor + unsigned(rGPR(rt)) + (size*signed(offset)); + vAddr64= to_bits(64, vAddr); if ((vAddr + size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr < getCapBase(cb_val)) then @@ -1180,12 +1179,12 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = SignalExceptionBadAddr(AdEL, vAddr64) else { - pAddr := (TLBTranslate(vAddr64, LoadData)); - widthBytes := wordWidthBytes(width); - (bit[64]) memResult := if (linked) then + pAddr = (TLBTranslate(vAddr64, LoadData)); + widthBytes = wordWidthBytes(width); + memResult : bits(64) = if (linked) then { - CP0LLBit := 0b1; - CP0LLAddr := pAddr; + CP0LLBit = 0b1; + CP0LLAddr = pAddr; if widthBytes == 1 then extendLoad(MEMr_reserve_wrapper(pAddr, 1), signext) else if widthBytes == 2 then extendLoad(MEMr_reserve_wrapper(pAddr, 2), signext) else if widthBytes == 4 then extendLoad(MEMr_reserve_wrapper(pAddr, 4), signext) @@ -1198,19 +1197,19 @@ function clause execute (CLoad(rd, cb, rt, offset, signext, width, linked)) = else if widthBytes == 4 then extendLoad(MEMr_wrapper(pAddr, 4), signext) else extendLoad(MEMr_wrapper(pAddr, 8), signext) }; - wGPR(rd) := memResult; + wGPR(rd) = memResult; } } - (* END_CLoad *) + /* END_CLoad */ } -union ast member (regno, regno, regno, regno, bit[8], WordType, bool) CStore +union clause ast = CStore : (regno, regno, regno, regno, bits(8), WordType, bool) function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = { - (* START_CStore *) + /* START_CStore */ checkCP2usable(); - cb_val := readCapReg(cb); + cb_val = readCapReg(cb); if (register_inaccessible(cb)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cb) else if not (cb_val.tag) then @@ -1221,10 +1220,10 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = raise_c2_exception(CapEx_PermitStoreViolation, cb) else { - size := wordWidthBytes(width); - cursor := getCapCursor(cb_val); - vAddr := cursor + unsigned(rGPR(rt)) + (size * signed(offset)); - vAddr64:= (bit[64]) (to_svec(vAddr)); + size = wordWidthBytes(width); + cursor = getCapCursor(cb_val); + vAddr = cursor + unsigned(rGPR(rt)) + (size * signed(offset)); + vAddr64= to_bits(64, vAddr); if ((vAddr + size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr < getCapBase(cb_val)) then @@ -1233,42 +1232,42 @@ function clause execute (CStore(rs, cb, rt, rd, offset, width, conditional)) = SignalExceptionBadAddr(AdES, vAddr64) else { - pAddr := (TLBTranslate(vAddr64, StoreData)); - rs_val := rGPR(rs); + pAddr = (TLBTranslate(vAddr64, StoreData)); + rs_val = rGPR(rs); if (conditional) then { - (bool) success := if (CP0LLBit[0]) then - switch(width) + success : bool = if (CP0LLBit[0]) then + match width { - case B -> MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0]) - case H -> MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0]) - case W -> MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0]) - case D -> MEMw_conditional_wrapper(pAddr, 8, rs_val) + B => MEMw_conditional_wrapper(pAddr, 1, rs_val[7..0]), + H => MEMw_conditional_wrapper(pAddr, 2, rs_val[15..0]), + W => MEMw_conditional_wrapper(pAddr, 4, rs_val[31..0]), + D => MEMw_conditional_wrapper(pAddr, 8, rs_val) } else false; - wGPR(rd) := EXTZ([success]); + wGPR(rd) = EXTZ(success); } else - switch(width) + match width { - case B -> MEMw_wrapper(pAddr, 1) := rs_val[7..0] - case H -> MEMw_wrapper(pAddr, 2) := rs_val[15..0] - case W -> MEMw_wrapper(pAddr, 4) := rs_val[31..0] - case D -> MEMw_wrapper(pAddr, 8) := rs_val + B => MEMw_wrapper(pAddr, 1) = rs_val[7..0], + H => MEMw_wrapper(pAddr, 2) = rs_val[15..0], + W => MEMw_wrapper(pAddr, 4) = rs_val[31..0], + D => MEMw_wrapper(pAddr, 8) = rs_val } } } - (* END_CStore *) + /* END_CStore */ } -union ast member (regno, regno, regno, regno, bit[11], bool) CSC +union clause ast = CSC : (regno, regno, regno, regno, bits(11), bool) function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = { - (* START_CSC *) + /* START_CSC */ checkCP2usable(); - cs_val := readCapReg(cs); - cb_val := readCapReg(cb); + cs_val = readCapReg(cs); + cb_val = readCapReg(cb); if (register_inaccessible(cs)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cs) else if (register_inaccessible(cb)) then @@ -1283,41 +1282,41 @@ function clause execute (CSC(cs, cb, rt, rd, offset, conditional)) = raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb) else { - cursor := getCapCursor(cb_val); - vAddr := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset)); - vAddr64:= (bit[64]) (to_svec(vAddr)); + cursor = getCapCursor(cb_val); + vAddr = cursor + unsigned(rGPR(rt)) + (16 * signed(offset)); + vAddr64= to_bits(64, vAddr); if ((vAddr + cap_size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr < getCapBase(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) - else if ((vAddr mod cap_size) != 0) then + else if ((vAddr % cap_size) != 0) then SignalExceptionBadAddr(AdES, vAddr64) else { - let (pAddr, noStoreCap) = (TLBTranslateC(vAddr64, StoreData)) in + let (pAddr, noStoreCap) = TLBTranslateC(vAddr64, StoreData) in if (cs_val.tag & noStoreCap) then raise_c2_exception(CapEx_TLBNoStoreCap, cs) else if (conditional) then { - success := if (CP0LLBit[0]) then + success = if (CP0LLBit[0]) then MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val)) else false; - wGPR(rd) := EXTZ([success]); + wGPR(rd) = EXTZ(success); } else MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val)); } } - (* END_CSC *) + /* END_CSC */ } -union ast member (regno, regno, regno, bit[11], bool) CLC +union clause ast = CLC : (regno, regno, regno, bits(11), bool) function clause execute (CLC(cd, cb, rt, offset, linked)) = { - (* START_CLC *) + /* START_CLC */ checkCP2usable(); - cb_val := readCapReg(cb); + cb_val = readCapReg(cb); if (register_inaccessible(cd)) then raise_c2_exception(CapEx_AccessSystemRegsViolation, cd) else if (register_inaccessible(cb)) then @@ -1328,35 +1327,36 @@ function clause execute (CLC(cd, cb, rt, offset, linked)) = raise_c2_exception(CapEx_SealViolation, cb) else { - cursor := getCapCursor(cb_val); - vAddr := cursor + unsigned(rGPR(rt)) + (((int) 16) * signed(offset)); - vAddr64:= (bit[64]) (to_svec(vAddr)); + cursor = getCapCursor(cb_val); + vAddr = cursor + unsigned(rGPR(rt)) + (16 * signed(offset)); + vAddr64= to_bits(64, vAddr); if ((vAddr + cap_size) > getCapTop(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) else if (vAddr < getCapBase(cb_val)) then raise_c2_exception(CapEx_LengthViolation, cb) - else if ((vAddr mod cap_size) != 0) then + else if ((vAddr % cap_size) != 0) then SignalExceptionBadAddr(AdEL, vAddr64) else { - let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in + let (pAddr, suppressTag) = TLBTranslateC(vAddr64, LoadData) in + let 'cd = unsigned(cd) in if (linked) then { - CP0LLBit := 0b1; - CP0LLAddr := pAddr; + CP0LLBit = 0b1; + CP0LLAddr = pAddr; let (tag, mem) = MEMr_tagged_reserve(pAddr) in - (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem); + (*CapRegs[cd]) = memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem); } else { let (tag, mem) = MEMr_tagged(pAddr) in - (CapRegs[cd]) := memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem); + (*CapRegs[cd]) = memBitsToCapBits(tag & (cb_val.permit_load_cap) & (not (suppressTag)), mem); } } } - (* END_CLC *) + /* END_CLC */ } -union ast member (regno) C2Dump +union clause ast = C2Dump : regno function clause execute (C2Dump (rt)) = - () (* Currently a NOP *) + () /* Currently a NOP */ diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index cc939f59..23881f03 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -1,51 +1,51 @@ -(*========================================================================*) -(* *) -(* 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 *) -typedef CapReg = bit[129] - -val cast extern bool -> bit effect pure cast_bool_bit -val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec -val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec +/*========================================================================*/ +/* */ +/* 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) + +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 extern bool -> bool effect pure not +val not : extern bool -> bool effect pure -typedef uint64 = range<0, (2** 64) - 1> +type uint64 = range<0, (2** 64) - 1> -typedef CapStruct = const struct { +type CapStruct = const struct { bool tag; - bit[4] uperms; + bits(4) uperms; bool access_system_regs; bool perm_reserved9; bool permit_ccall; @@ -57,16 +57,16 @@ typedef CapStruct = const struct { bool permit_load; bool permit_execute; bool global; - bit[2] reserved; - bit[6] E; + bits(2) reserved; + bits(6) E; bool sealed; - bit[20] B; - bit[20] T; - bit[24] otype; - bit[64] address; + bits(20) B; + bits(20) T; + bits(24) otype; + bits(64) address; } -let (CapStruct) null_cap = { +let null_cap : CapStruct = { tag = false; uperms = 0; access_system_regs = false; @@ -81,7 +81,7 @@ let (CapStruct) null_cap = { permit_execute = false; global = false; reserved = 0; - E = 48; (* encoded as 0 in memory due to xor *) + E = 48; /* encoded as 0 in memory due to xor */ sealed = false; B = 0; T = 0x10000; @@ -89,14 +89,14 @@ let (CapStruct) null_cap = { address = 0; } -def Nat cap_size_t = 16 (* cap size in bytes *) -let ([:cap_size_t:]) cap_size = 16 +def Nat cap_size_t = 16 /* cap size in bytes */ +let cap_size : [:cap_size_t:] = 16 function CapStruct capRegToCapStruct((CapReg) c) = - let (bool) s = c[104] in - let (bit[20]) Bc = if s then c[103..96] : 0x000 else c[103..84] in - let (bit[20]) Tc = if s then c[83..76] : 0x000 else c[83..64] in - let (bit[24]) otype = if s then c[95..84] : c[75..64] else 0 in + 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]; @@ -120,7 +120,7 @@ function CapStruct capRegToCapStruct((CapReg) c) = address = c[63..0]; } -function (bit[11]) getCapHardPerms((CapStruct) cap) = +function (bits(11)) getCapHardPerms((CapStruct) cap) = ([cap.access_system_regs] : [cap.perm_reserved9] : [cap.permit_ccall] @@ -133,13 +133,13 @@ function (bit[11]) getCapHardPerms((CapStruct) cap) = : [cap.permit_execute] : [cap.global]) -function (bit[128]) capStructToMemBits128((CapStruct) cap) = - let (bit[20]) b = if cap.sealed then (cap.B)[19..12] : (cap.otype)[23..12] else cap.B in - let (bit[20]) t = if cap.sealed then (cap.T)[19..12] : (cap.otype)[11..0] else cap.T in +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 ( cap.uperms : getCapHardPerms(cap) : cap.reserved - : (cap.E ^ 0b110000) (* XXX brackets required otherwise sail interpreter error *) + : (cap.E ^ 0b110000) /* XXX brackets required otherwise sail interpreter error */ : [cap.sealed] : b : t @@ -149,32 +149,32 @@ function (bit[128]) capStructToMemBits128((CapStruct) cap) = function (CapReg) capStructToCapReg((CapStruct) cap) = ([cap.tag] : capStructToMemBits128(cap)) -(* Reverse of above used when reading from memory *) -function (CapReg) memBitsToCapBits128((bool) tag, (bit[128]) b) = +/* Reverse of above used when reading from memory */ +function (CapReg) memBitsToCapBits128((bool) tag, (bits(128)) b) = ([tag] : b) -(* When saving/restoring capabilities xor them with bits of null_cap -- +/* 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 *) + even though it may have bits set logically (e.g. length or exponent */ -let (bit[128]) null_cap_bits = capStructToMemBits128(null_cap) +let null_cap_bits : bits(128) = capStructToMemBits128(null_cap) -function (bit[128]) capStructToMemBits((CapStruct) cap) = +function (bits(128)) capStructToMemBits((CapStruct) cap) = capStructToMemBits128(cap) ^ null_cap_bits -function (bit[129]) memBitsToCapBits((bool) tag, (bit[128]) b) = +function (bits(129)) memBitsToCapBits((bool) tag, (bits(128)) b) = memBitsToCapBits128(tag, b ^ null_cap_bits) -function (bit[31]) getCapPerms((CapStruct) cap) = - let (bit[15]) perms = EXTS(getCapHardPerms(cap)) in (* NB access_system copied into 14-11 *) - (0x000 (* uperms 30-19 *) +function (bits(31)) getCapPerms((CapStruct) cap) = + let perms : bits(15) = EXTS(getCapHardPerms(cap)) in /* NB access_system copied into 14-11 */ + (0x000 /* uperms 30-19 */ : cap.uperms : perms) -function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) = +function CapStruct setCapPerms((CapStruct) cap, (bits(31)) perms) = { cap with uperms = perms[18..15]; - (* 14..11 reserved -- ignore *) + /* 14..11 reserved -- ignore */ access_system_regs = perms[10]; perm_reserved9 = perms[9]; permit_ccall = perms[8]; @@ -188,41 +188,41 @@ function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) = global = perms[0]; } -function (bool, CapStruct) sealCap((CapStruct) cap, (bit[24]) otype) = +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}) else - (false, cap (* was undefined but ocaml shallow embedding can't handle it *) ) - -function [|-1:1|] a_top_correction((bit[20]) a_mid, (bit[20]) R, (bit[20]) bound) = - switch (a_mid < R, bound < R) { - case (false, false) -> 0 - case (false, true) -> 1 - case (true, false) -> -1 - case (true, true) -> 0 + (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 } function uint64 getCapBase((CapStruct) c) = - let ([|48|]) E = min(unsigned(c.E), 48) in - let (bit[20]) Bc = c.B in - let (bit[65]) a = EXTZ(c.address) in - let (bit[20]) R = Bc - 0x01000 in (* wraps *) - let (bit[20]) a_mid = mask(a >> E) in + let E : [|48|] = 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 correction = a_top_correction(a_mid, R, Bc) in let a_top = a >> (E+20) in - let (bit[64]) base = EXTZ((a_top + correction) : Bc) << E in + let base : bits(64) = EXTZ((a_top + correction) : Bc) << E in unsigned(base) function CapLen getCapTop ((CapStruct) c) = - let ([|45|]) E = min(unsigned(c.E), 48) in - let (bit[20]) Bc = c.B in - let (bit[20]) T = c.T in - let (bit[65]) a = EXTZ(c.address) in - let (bit[20]) R = Bc - 0x01000 in (* wraps *) - let (bit[20]) a_mid = mask(a >> E) in + let E : [|45|] = 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 correction = a_top_correction(a_mid, R, T) in let a_top = a >> (E+20) in - let (bit[65]) top1 = EXTZ((a_top + correction) : T) in + let top1 : bits(65) = EXTZ((a_top + correction) : T) in (CapLen) (top1 << E) function uint64 getCapOffset((CapStruct) c) = @@ -233,58 +233,58 @@ function CapLen getCapLength((CapStruct) c) = getCapTop(c) - getCapBase(c) function uint64 getCapCursor((CapStruct) cap) = unsigned(cap.address) -function bool fastRepCheck((CapStruct) c, (bit[64]) i) = +function bool fastRepCheck((CapStruct) c, (bits(64)) i) = if ((c.E) >= 44) then - true (* in this case representable region is whole address space *) + true /* in this case representable region is whole address space */ else let E = min(unsigned(c.E), 43) in let i_top = signed(i[63..E+20]) in - let (bit[20]) i_mid = i[E+19..E] in - let (bit[20]) a_mid = (c.address)[E+19..E] in - let (bit[20]) R = (c.B) - 0x01000 in - let (bit[20]) diff = R - a_mid in - let (bit[20]) diff1 = diff - 1 in - (* i_top determines 1. whether the increment is inRange + 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 *) + 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 - unsigned(i_mid) >= unsigned(diff) & (R != a_mid) (* XXX sail missing unsigned >= *) + unsigned(i_mid) >= unsigned(diff) & (R != a_mid) /* XXX sail missing unsigned >= */ else false -function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = - let (bit[64]) base = (bit[64]) (getCapBase(c)) in - let (bit[64]) newAddress = base + offset in +function (bool, CapStruct) setCapOffset((CapStruct) c, (bits(64)) offset) = + let base : bits(64) = (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, (bit[64]) delta) = - let (bit[64]) newAddress = c.address + delta in +function (bool, CapStruct) incCapOffset((CapStruct) c, (bits(64)) delta) = + 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) *) +/** FUNCTION:integer HighestSetBit(bits(N) x) */ -function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['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; + ([|('N + -1)|]) result = 0; + (bool) break = false; foreach (i from (N - 1) downto 0) if ~(break) & x[i] == 1 then { - result := i; - break := true; + result = i; + break = true; }; if break then Some(result) else None; }} -(* hw rounds up E to multiple of 4 *) +/* hw rounds up E to multiple of 4 */ function [|48|] roundUp(([|45|]) e) = let r = e mod 4 in if (r == 0) @@ -292,25 +292,25 @@ function [|48|] roundUp(([|45|]) e) = else (e - r + 4) -function [|48|] computeE ((bit[65]) rlength) = +function [|48|] computeE ((bits(65)) rlength) = let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in - switch (msb) { - (* above will always return <= 45 because 19 bits of zero are shifted in from right *) - case (Some(b)) -> {assert(b <= 45, None); roundUp (min(b,45)) } - case None -> 0 + match msb { + /* 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 } -function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) = - (* {cap with base=base; length=(bit[64]) length; offset=0} *) - let ([|48|]) e = computeE(top - (0b0 : base)) in - let (bit[20]) Bc = base[19+e..e] in - let (bit[20]) T = top[19+e..e] in - let (bit[20]) T2 = T + if (top[(e - 1)..0] == 0) then 0 else 1 in - let newCap = {cap with E=(bit[6]) e; B=Bc; T=T2} in +function (bool, CapStruct) setCapBounds((CapStruct) cap, (bits(64)) base, (bits(65)) top) = + /* {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 newBase = getCapBase(newCap) in let newTop = getCapTop(newCap) in let exact = (base == newBase) & (top == newTop) in (exact, newCap) -function CapStruct int_to_cap ((bit[64]) offset) = +function CapStruct int_to_cap ((bits(64)) offset) = {null_cap with address = offset} diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index 988cfe49..9e3a0cd9 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -1,226 +1,224 @@ -(*========================================================================*) -(* *) -(* 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. *) -(*========================================================================*) - -(* 256 bit cap + tag *) -typedef CapReg = bit[257] - -val cast extern bool -> bit effect pure cast_bool_bit -val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec -val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec +/*========================================================================*/ +/* */ +/* 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. */ +/*========================================================================*/ + +/* 256 bit cap + tag */ +type CapReg = bits(257) + +/* +val cast_bool_bit : bool -> bit effect pure +val cast_boolvec_bitvec : 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure +val cast_range_bitvec : 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 extern bool -> bool effect pure not - -typedef uint64 = range<0, (2** 64) - 1> - -typedef CapStruct = const struct { - bool tag; - bit[8] padding; - bit[24] otype; - bit[16] uperms; - bit[4] perm_reserved11_14; - 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; - bool sealed; - bit[64] offset; - bit[64] base; - bit[64] length; +val not : extern bool -> bool effect pure */ + +type uint64 = range(0, (2 ^ 64) - 1) + +struct CapStruct = { + tag : bool , + padding : bits(8) , + otype : bits(24), + uperms : bits(16), + perm_reserved11_14 : 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 , + sealed : bool , + offset : bits(64), + base : bits(64), + length : bits(64), } -let (CapStruct) null_cap = { - tag = false; - padding = 0; - otype = 0; - uperms = 0; - perm_reserved11_14 = 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; - sealed = false; - offset = 0; - base = 0; - length = 0xffffffffffffffff; +let null_cap : CapStruct = struct { + tag = false, + padding = zeros(), + otype = zeros(), + uperms = zeros(), + perm_reserved11_14 = 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, + sealed = false, + offset = zeros(), + base = zeros(), + length = 0xffffffffffffffff } -def Nat cap_size_t = 32 (* cap size in bytes *) -let ([:cap_size_t:]) cap_size = 32 - -function CapStruct capRegToCapStruct((CapReg) capReg) = - { - tag = capReg[256]; - padding = capReg[255..248]; - otype = capReg[247..224]; - uperms = capReg[223..208]; - perm_reserved11_14 = capReg[207..204]; - access_system_regs = capReg[203]; - perm_reserved9 = capReg[202]; - permit_ccall = capReg[201]; - permit_seal = capReg[200]; - permit_store_local_cap = capReg[199]; - permit_store_cap = capReg[198]; - permit_load_cap = capReg[197]; - permit_store = capReg[196]; - permit_load = capReg[195]; - permit_execute = capReg[194]; - global = capReg[193]; - sealed = capReg[192]; - offset = capReg[191..128]; - base = capReg[127..64]; - length = capReg[63..0]; +let 'cap_size = 32 + +function capRegToCapStruct(capReg) : CapReg -> CapStruct = + struct { + tag = capReg[256], + padding = capReg[255..248], + otype = capReg[247..224], + uperms = capReg[223..208], + perm_reserved11_14 = capReg[207..204], + access_system_regs = capReg[203], + perm_reserved9 = capReg[202], + permit_ccall = capReg[201], + permit_seal = capReg[200], + permit_store_local_cap = capReg[199], + permit_store_cap = capReg[198], + permit_load_cap = capReg[197], + permit_store = capReg[196], + permit_load = capReg[195], + permit_execute = capReg[194], + global = capReg[193], + sealed = capReg[192], + offset = capReg[191..128], + base = capReg[127..64], + length = capReg[63..0] } -function (bit[31]) getCapPerms((CapStruct) cap) = +function getCapPerms(cap) : CapStruct -> bits(31) = ( cap.uperms - : cap.perm_reserved11_14 - : [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] + @ cap.perm_reserved11_14 + @ 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 used to convert capabilities to in-memory format +/* Function used to convert capabilities to in-memory format - this is the same as register format except for the offset, field which is stored as an absolute cursor on CHERI - due to uarch optimisation *) -function (bit[256]) capStructToMemBits256((CapStruct) cap) = + due to uarch optimisation */ +function capStructToMemBits256(cap) : CapStruct -> bits(256) = ( cap.padding - : cap.otype - : getCapPerms(cap) - : [cap.sealed] - (* NB in memory format stores cursor, not offset *) - : (cap.base + cap.offset) - : cap.base - : cap.length + @ cap.otype + @ getCapPerms(cap) + @ cap.sealed + /* NB in memory format stores cursor, not offset */ + @ (cap.base + cap.offset) + @ cap.base + @ cap.length ) -(* Reverse of above used when reading from memory *) -function (bit[257]) memBitsToCapBits256((bool) tag, (bit[256]) b) = - ([tag] - : b[255..192] - : ((bit[64])(b[191..128] - b[127..64])) - : b[127..0] +/* Reverse of above used when reading from memory */ +function memBitsToCapBits256(tag, b) : (bool, bits(256)) -> bits(257)= + (tag + @ b[255..192] + @ (b[191..128] - b[127..64]) + @ b[127..0] ) -(* When saving/restoring capabilities xor them with bits of null_cap -- +/* 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 *) + even though it may have bits set logically (e.g. length or exponent) */ -function (bit[256]) capStructToMemBits((CapStruct) cap) = - let (bit[256]) null_cap_bits = capStructToMemBits256(null_cap) in +function capStructToMemBits(cap) : CapStruct -> bits(256)= + let null_cap_bits : bits(256) = capStructToMemBits256(null_cap) in capStructToMemBits256(cap) ^ null_cap_bits -function (bit[257]) memBitsToCapBits((bool) tag, (bit[256]) b) = - let (bit[256]) null_cap_bits = capStructToMemBits256(null_cap) in +function memBitsToCapBits(tag, b) : (bool, bits(256)) -> bits(257) = + let null_cap_bits : bits(256) = capStructToMemBits256(null_cap) in memBitsToCapBits256(tag, b ^ null_cap_bits) -function (CapReg) capStructToCapReg((CapStruct) cap) = - ( - [cap.tag] - : cap.padding - : cap.otype - : getCapPerms(cap) - : [cap.sealed] - : cap.offset - : cap.base - : cap.length - ) - -function CapStruct setCapPerms((CapStruct) cap, (bit[31]) perms) = +function capStructToCapReg(cap) : CapStruct -> CapReg = + cap.tag + @ cap.padding + @ cap.otype + @ getCapPerms(cap) + @ cap.sealed + @ cap.offset + @ cap.base + @ cap.length + +function setCapPerms(cap, perms) : (CapStruct, bits(31)) -> CapStruct = { cap with - uperms = perms[30..15]; - perm_reserved11_14 = perms[14..11]; - 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, (bit[24]) otype) = - (true, {cap with sealed=true; otype=otype}) - -function bit[64] getCapBase((CapStruct) c) = c.base -function [|0:2**65 - 2|] getCapTop((CapStruct) c) = unsigned(c.base) + unsigned(c.length) -function bit[64] getCapOffset((CapStruct) c) = c.offset -function CapLen getCapLength((CapStruct) c) = unsigned(c.length) - -function uint64 getCapCursor((CapStruct) cap) = - (unsigned(cap.base) + unsigned(cap.offset)) mod (pow2(64)) - -function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) = + uperms = perms[30..15], + perm_reserved11_14 = perms[14..11], + 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 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 getCapOffset(c) : CapStruct -> uint64 = unsigned(c.offset) +function getCapLength(c) : CapStruct -> CapLen = unsigned(c.length) + +function getCapCursor(cap) : CapStruct -> uint64 = + (unsigned(cap.base) + unsigned(cap.offset)) % (pow2(64)) + +function setCapOffset(c, offset) : (CapStruct, bits(64)) -> (bool, CapStruct) = (true, {c with offset=offset}) -function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) = - let (bit[64]) newOffset = c.offset + delta in +function incCapOffset(c, delta) : (CapStruct, bits(64)) -> (bool, CapStruct) = + let newOffset : bits(64) = c.offset + delta in (true, {c with offset = newOffset}) -function (bool, CapStruct) setCapBounds((CapStruct) cap, (bit[64]) base, (bit[65]) top) = - let (bit[65]) length = top - (0b0 : base) in - (true, {cap with base = base; length = length[63..0]; offset = 0}) +function setCapBounds(cap, base, top) : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) = + let length : bits(65) = top - (0b0 @ base) in + (true, {cap with base = base, length = length[63..0], offset = zeros()}) -function CapStruct int_to_cap ((bit[64]) offset) = +function int_to_cap (offset) : bits(64) -> CapStruct = {null_cap with offset = offset} diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail index a2d3b441..6b29ffce 100644 --- a/cheri/cheri_prelude_common.sail +++ b/cheri/cheri_prelude_common.sail @@ -1,338 +1,363 @@ -(*========================================================================*) -(* *) -(* 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. *) -(*========================================================================*) - - -scattered typedef ast = const union - -val ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmvt, wreg} execute -scattered function unit execute - -val bit[32] -> option<ast> effect pure decode -scattered function option<ast> decode - - -register CapReg PCC -register CapReg nextPCC -register CapReg delayedPCC -register (bit[1]) inCCallDelay -register CapReg C00 (* aka default data capability, DDC *) -register CapReg C01 -register CapReg C02 -register CapReg C03 -register CapReg C04 -register CapReg C05 -register CapReg C06 -register CapReg C07 -register CapReg C08 -register CapReg C09 -register CapReg C10 -register CapReg C11 -register CapReg C12 -register CapReg C13 -register CapReg C14 -register CapReg C15 -register CapReg C16 -register CapReg C17 -register CapReg C18 -register CapReg C19 -register CapReg C20 -register CapReg C21 -register CapReg C22 -register CapReg C23 -register CapReg C24 (* aka return code capability, RCC *) -register CapReg C25 -register CapReg C26 (* aka invoked data capability, IDC *) -register CapReg C27 (* aka kernel reserved capability 1, KR1C *) -register CapReg C28 (* aka kernel reserved capability 2, KR2C *) -register CapReg C29 (* aka kernel code capability, KCC *) -register CapReg C30 (* aka kernel data capability, KDC *) -register CapReg C31 (* aka exception program counter capability, EPCC *) - -let (vector <0, 32, inc, (register<CapReg>)>) CapRegs = - [ C00, C01, C02, C03, C04, C05, C06, C07, C08, C09, C10, - C11, C12, C13, C14, C15, C16, C17, C18, C19, C20, - C21, C22, C23, C24, C25, C26, C27, C28, C29, C30, C31 +/*========================================================================*/ +/* */ +/* 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. */ +/*========================================================================*/ + + +scattered union ast + +val execute : ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmvt, wreg} +scattered function execute + +val decode : bits(32) -> option(ast) effect pure +scattered function decode + + +register PCC : CapReg +register nextPCC : CapReg +register delayedPCC : CapReg +register inCCallDelay : bits(1) +register C00 : CapReg /* aka default data capability, DDC */ +register C01 : CapReg +register C02 : CapReg +register C03 : CapReg +register C04 : CapReg +register C05 : CapReg +register C06 : CapReg +register C07 : CapReg +register C08 : CapReg +register C09 : CapReg +register C10 : CapReg +register C11 : CapReg +register C12 : CapReg +register C13 : CapReg +register C14 : CapReg +register C15 : CapReg +register C16 : CapReg +register C17 : CapReg +register C18 : CapReg +register C19 : CapReg +register C20 : CapReg +register C21 : CapReg +register C22 : CapReg +register C23 : CapReg +register C24 : CapReg /* aka return code capability, RCC */ +register C25 : CapReg +register C26 : CapReg /* aka invoked data capability, IDC */ +register C27 : CapReg /* aka kernel reserved capability 1, KR1C */ +register C28 : CapReg /* aka kernel reserved capability 2, KR2C */ +register C29 : CapReg /* aka kernel code capability, KCC */ +register C30 : CapReg /* aka kernel data capability, KDC */ +register C31 : CapReg /* aka exception program counter capability, EPCC */ + +let IDC : regno = 0b11010 /* 26 */ + +let CapRegs : vector(32, dec, register(CapReg)) = + [ + ref C31, + ref C30, + ref C29, + ref C28, + ref C27, + ref C26, + ref C25, + ref C24, + ref C23, + ref C22, + ref C21, + ref C20, + ref C19, + ref C18, + ref C17, + ref C16, + ref C15, + ref C14, + ref C13, + ref C12, + ref C11, + ref C10, + ref C09, + ref C08, + ref C07, + ref C06, + ref C05, + ref C04, + ref C03, + ref C02, + ref C01, + ref C00 ] -let max_otype = MAX(24) (*0xffffff*) +let max_otype = MAX(24) /*0xffffff*/ let have_cp2 = true -function (CapStruct) readCapReg((regno) n) = - capRegToCapStruct(CapRegs[n]) - -function unit writeCapReg((regno) n, (CapStruct) cap) = - CapRegs[n] := capStructToCapReg(cap) - -typedef CapEx = enumerate { - CapEx_None; - CapEx_LengthViolation; - CapEx_TagViolation; - CapEx_SealViolation; - CapEx_TypeViolation; - CapEx_CallTrap; - CapEx_ReturnTrap; - CapEx_TSSUnderFlow; - CapEx_UserDefViolation; - CapEx_TLBNoStoreCap; - CapEx_InexactBounds; - CapEx_GlobalViolation; - CapEx_PermitExecuteViolation; - CapEx_PermitLoadViolation; - CapEx_PermitStoreViolation; - CapEx_PermitLoadCapViolation; - CapEx_PermitStoreCapViolation; - CapEx_PermitStoreLocalCapViolation; - CapEx_PermitSealViolation; - CapEx_AccessSystemRegsViolation; - CapEx_PermitCCallViolation; - CapEx_AccessCCallIDCViolation; +function readCapReg(n) : regno -> CapStruct = + let 'i = unsigned(n) in + capRegToCapStruct(reg_deref(CapRegs[i])) + +function writeCapReg(n, cap) : (regno, CapStruct) -> unit = + let 'i = unsigned(n) in + (*CapRegs[i]) = capStructToCapReg(cap) + +enum CapEx = { + CapEx_None, + CapEx_LengthViolation, + CapEx_TagViolation, + CapEx_SealViolation, + CapEx_TypeViolation, + CapEx_CallTrap, + CapEx_ReturnTrap, + CapEx_TSSUnderFlow, + CapEx_UserDefViolation, + CapEx_TLBNoStoreCap, + CapEx_InexactBounds, + CapEx_GlobalViolation, + CapEx_PermitExecuteViolation, + CapEx_PermitLoadViolation, + CapEx_PermitStoreViolation, + CapEx_PermitLoadCapViolation, + CapEx_PermitStoreCapViolation, + CapEx_PermitStoreLocalCapViolation, + CapEx_PermitSealViolation, + CapEx_AccessSystemRegsViolation, + CapEx_PermitCCallViolation, + CapEx_AccessCCallIDCViolation } -typedef CPtrCmpOp = enumerate { - CEQ; - CNE; - CLT; - CLE; - CLTU; - CLEU; - CEXEQ; - CNEXEQ; -} - -typedef ClearRegSet = enumerate { -GPLo; -GPHi; -CLo; -CHi; -} - -function (bit[8]) CapExCode((CapEx) ex) = - switch(ex) { - case CapEx_None -> 0x00 - case CapEx_LengthViolation -> 0x01 - case CapEx_TagViolation -> 0x02 - case CapEx_SealViolation -> 0x03 - case CapEx_TypeViolation -> 0x04 - case CapEx_CallTrap -> 0x05 - case CapEx_ReturnTrap -> 0x06 - case CapEx_TSSUnderFlow -> 0x07 - case CapEx_UserDefViolation -> 0x08 - case CapEx_TLBNoStoreCap -> 0x09 - case CapEx_InexactBounds -> 0x0a - case CapEx_GlobalViolation -> 0x10 - case CapEx_PermitExecuteViolation -> 0x11 - case CapEx_PermitLoadViolation -> 0x12 - case CapEx_PermitStoreViolation -> 0x13 - case CapEx_PermitLoadCapViolation -> 0x14 - case CapEx_PermitStoreCapViolation -> 0x15 - case CapEx_PermitStoreLocalCapViolation -> 0x16 - case CapEx_PermitSealViolation -> 0x17 - case CapEx_AccessSystemRegsViolation -> 0x18 - case CapEx_PermitCCallViolation -> 0x19 - case CapEx_AccessCCallIDCViolation -> 0x1a +function CapExCode(ex) : CapEx -> bits(8)= + match ex { + CapEx_None => 0x00, + CapEx_LengthViolation => 0x01, + CapEx_TagViolation => 0x02, + CapEx_SealViolation => 0x03, + CapEx_TypeViolation => 0x04, + CapEx_CallTrap => 0x05, + CapEx_ReturnTrap => 0x06, + CapEx_TSSUnderFlow => 0x07, + CapEx_UserDefViolation => 0x08, + CapEx_TLBNoStoreCap => 0x09, + CapEx_InexactBounds => 0x0a, + CapEx_GlobalViolation => 0x10, + CapEx_PermitExecuteViolation => 0x11, + CapEx_PermitLoadViolation => 0x12, + CapEx_PermitStoreViolation => 0x13, + CapEx_PermitLoadCapViolation => 0x14, + CapEx_PermitStoreCapViolation => 0x15, + CapEx_PermitStoreLocalCapViolation => 0x16, + CapEx_PermitSealViolation => 0x17, + CapEx_AccessSystemRegsViolation => 0x18, + CapEx_PermitCCallViolation => 0x19, + CapEx_AccessCCallIDCViolation => 0x1a } -typedef CapCauseReg = register bits [15:0] { - 15..8: ExcCode; - 7..0: RegNum; +bitfield CapCauseReg : bits(16) = { + ExcCode : 15..8, + RegNum : 7..0, } -register CapCauseReg CapCause +register CapCause : CapCauseReg -function forall Type 'o . 'o SignalException ((Exception) ex) = +function SignalException (ex) = { - if (~ (CP0Status.EXL)) then { - let pc = (bit[64]) PC in (* Cast forces read of register. *) + if (not (CP0Status.EXL())) then { + let pc = PC in let pcc = capRegToCapStruct(PCC) in let (success, epcc) = setCapOffset(pcc, pc) in if (success) then - C31 := capStructToCapReg(epcc) + C31 = capStructToCapReg(epcc) else - C31 := capStructToCapReg(int_to_cap(getCapBase(pcc) + pc)); + C31 = capStructToCapReg(int_to_cap(to_bits(64, getCapBase(pcc)) + unsigned(pc))); }; - nextPCC := C29; (* KCC *) - delayedPCC := C29; (* always write delayedPCC together with nextPCC so - that non-capability branches don't override PCC *) - let base = (bit[64]) (getCapBase(capRegToCapStruct(C29))) in - SignalExceptionMIPS(ex, base); + nextPCC = C29; /* KCC */ + delayedPCC = C29; /* always write delayedPCC together with nextPCC so + that non-capability branches don't override PCC */ + let base = getCapBase(capRegToCapStruct(C29)) in + SignalExceptionMIPS(ex, to_bits(64, base)); } -function unit ERETHook() = +function ERETHook() : unit -> unit = { - nextPCC := C31; - delayedPCC := C31; (* always write delayedPCC together with nextPCC so - that non-capability branches don't override PCC *) + nextPCC = C31; + delayedPCC = C31; /* always write delayedPCC together with nextPCC so + that non-capability branches don't override PCC */ } -function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) regnum) = +val raise_c2_exception8 : forall ('o : Type) . (CapEx, bits(8)) -> 'o effect {escape, rreg, wreg} +function raise_c2_exception8(capEx, regnum) = { - (CapCause.ExcCode) := CapExCode(capEx); - (CapCause.RegNum) := regnum; + CapCause->ExcCode() = CapExCode(capEx); + CapCause->RegNum() = regnum; let mipsEx = if ((capEx == CapEx_CallTrap) | (capEx == CapEx_ReturnTrap)) then C2Trap else C2E in SignalException(mipsEx); } -function forall Type 'o . 'o raise_c2_exception((CapEx) capEx, (regno) regnum) = - let reg8 = 0b000 : regnum in - if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == 26 (* IDC *))) then +val raise_c2_exception : forall ('o : Type) . (CapEx, regno) -> 'o effect {escape, rreg, wreg} +function raise_c2_exception(capEx, regnum) = + let reg8 = 0b000 @ regnum in + if ((capEx == CapEx_AccessSystemRegsViolation) & (regnum == IDC)) then raise_c2_exception8(CapEx_AccessCCallIDCViolation, reg8) else raise_c2_exception8(capEx, reg8) -function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) = +val raise_c2_exception_noreg : forall ('o : Type) . (CapEx) -> 'o effect {escape, rreg, wreg} +function raise_c2_exception_noreg(capEx) = raise_c2_exception8(capEx, 0xff) -function bool pcc_access_system_regs () = +val pcc_access_system_regs : unit -> bool effect {rreg} +function pcc_access_system_regs () = let pcc = capRegToCapStruct(PCC) in (pcc.access_system_regs) -function bool register_inaccessible((regno) r) = - if ((r == 26 (* IDC *)) & ((bool)inCCallDelay)) then true else (* XXX interpreter crash without cast *) - let (bool) is_sys_reg = switch(r) { - case 0b11011 -> true - case 0b11100 -> true - case 0b11101 -> true - case 0b11110 -> true - case 0b11111 -> true - case _ -> false +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 -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag -val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bool, bit[8 * 'n]) effect { rmemt } MEMr_tag_reserve +val MEMr_tag : forall 'n. ( bits(64) , atom('n) ) -> (bool, bits(8 * 'n)) effect { rmemt } +val MEMr_tag_reserve : forall 'n. ( bits(64) , atom('n) ) -> (bool, bits(8 * 'n)) effect { rmemt } -val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> unit effect { wmvt } MEMval_tag -val extern forall Nat 'n. ( bit[64] , [|'n|] , bool, bit[8 * 'n]) -> bool effect { wmvt } MEMval_tag_conditional +val MEMval_tag : forall 'n. ( bits(64) , atom('n), bool, bits(8*'n)) -> unit effect { wmvt } +val MEMval_tag_conditional : forall 'n. ( bits(64) , atom('n), bool, bits(8*'n)) -> bool effect { wmvt } - -function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) = - (* assumes addr is cap. aligned *) - let (tag, data) = MEMr_tag (addr, cap_size) in +val MEMr_tagged : bits(64) -> (bool, bits('cap_size * 8)) effect { rmemt } +function MEMr_tagged (addr) = + /* assumes addr is cap. aligned */ + let (tag, data) = MEMr_tag (addr, cap_size) in (tag, reverse_endianness(data)) - -function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) = - (* assumes addr is cap. aligned *) +val MEMr_tagged_reserve : bits(64) -> (bool, bits('cap_size * 8)) effect { rmemt } +function MEMr_tagged_reserve (addr) = + /* assumes addr is cap. aligned */ let (tag, data) = MEMr_tag_reserve(addr, cap_size) in (tag, reverse_endianness(data)) -function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = +val MEMw_tagged : (bits(64), bool, bits('cap_size * 8)) -> unit effect { eamem, wmvt } +function MEMw_tagged(addr, tag, data) = { - (* assumes addr is cap. aligned *) + /* assumes addr is cap. aligned */ MEMea(addr, cap_size); MEMval_tag(addr, cap_size, tag, reverse_endianness(data)); } -function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) = +val MEMw_tagged_conditional : (bits(64), bool, bits('cap_size * 8)) -> bool effect { eamem, wmvt } +function MEMw_tagged_conditional(addr, tag, data) = { - (* assumes addr is cap. aligned *) + /* assumes addr is cap. aligned */ MEMea_conditional(addr, cap_size); MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data)); } -val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> unit effect {wmvt, wreg, eamem} MEMw_wrapper -function unit effect {wmvt, wreg, eamem} MEMw_wrapper(addr, size, data) = +val MEMw_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmvt, wreg, eamem} +function MEMw_wrapper(addr, size, data) = let ledata = reverse_endianness(data) in if (addr == 0x000000007f000000) then { - UART_WDATA := ledata[7..0]; - UART_WRITTEN := 1; + UART_WDATA = ledata[7..0]; + UART_WRITTEN = 0b1; } else { - (* On cheri non-capability writes must clear the corresponding tag *) + /* On cheri non-capability writes must clear the corresponding tag */ MEMea(addr, size); MEMval_tag(addr, size, false, ledata); } -val forall Nat 'n, 'n >= 1. (bit[64], [:'n:], bit[8 * 'n]) -> bool effect {wmvt, eamem} MEMw_conditional_wrapper -function bool effect {wmvt, eamem} MEMw_conditional_wrapper(addr, size, data) = +val MEMw_conditional_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmvt, eamem} +function MEMw_conditional_wrapper(addr, size, data) = { - (* On cheri non-capability writes must clear the corresponding tag*) + /* On cheri non-capability writes must clear the corresponding tag*/ MEMea_conditional(addr, size); MEMval_tag_conditional(addr,size,false,reverse_endianness(data)); } -function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) = +val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg, wreg, escape} +function addrWrapper(addr, accessType, width) = { - capno := 0b00000; - cap := readCapReg(capno); - if (~(cap.tag)) then + capno = 0b00000; + cap = readCapReg(capno); + if (not (cap.tag)) then (raise_c2_exception(CapEx_TagViolation, capno)) else if (cap.sealed) then (raise_c2_exception(CapEx_SealViolation, capno)); - switch (accessType) { - case Instruction -> if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno)) - case LoadData -> if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno)) - case StoreData -> if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno)) + match accessType { + Instruction => if (~(cap.permit_execute)) then (raise_c2_exception(CapEx_PermitExecuteViolation, capno)), + LoadData => if (~(cap.permit_load)) then (raise_c2_exception(CapEx_PermitLoadViolation, capno)), + StoreData => if (~(cap.permit_store)) then (raise_c2_exception(CapEx_PermitStoreViolation, capno)) }; - cursor := getCapCursor(cap); - vAddr := cursor + unsigned(addr); - size := wordWidthBytes(width); - base := getCapBase(cap); - top := getCapTop(cap); + cursor = getCapCursor(cap); + vAddr = cursor + unsigned(addr); + size = wordWidthBytes(width); + base = getCapBase(cap); + top = getCapTop(cap); if ((vAddr + size) > top) then (raise_c2_exception(CapEx_LengthViolation, capno)) - else if (vAddr < (base)) then + else if (vAddr < base) then (raise_c2_exception(CapEx_LengthViolation, capno)) else - (bit[64]) (to_vec(vAddr)); (* XXX vAddr not truncated because top <= 2^64 and size > 0 *) + to_bits(64, vAddr); /* XXX vAddr not truncated because top <= 2^64 and size > 0 */ } -function (bit[64]) TranslatePC ((bit[64]) vAddr) = { +val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, undef, escape} +function TranslatePC (vAddr) = { incrementCP0Count(); let pcc = capRegToCapStruct(PCC) in let base = getCapBase(pcc) in let top = getCapTop(pcc) in let absPC = base + unsigned(vAddr) in - if ((absPC mod 4) != 0) then (* bad PC alignment *) - (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *) + if ((absPC % 4) != 0) then /* bad PC alignment */ + (SignalExceptionBadAddr(AdEL, to_bits(64, absPC))) /* XXX absPC may be truncated */ else if ((absPC + 4) > top) then (raise_c2_exception_noreg(CapEx_LengthViolation)) else - TLBTranslate((bit[64]) absPC, Instruction) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *) + TLBTranslate(to_bits(64, absPC), Instruction) /* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps */ } - -function unit checkCP2usable () = - if not ((norm_dec (CP0Status.CU))[2]) then +val checkCP2usable : unit -> unit effect {rreg, wreg, escape} +function checkCP2usable () = + if not ((CP0Status.CU())[2]) then { - (CP0Cause.CE) := 0b10; + (CP0Cause->CE()) = 0b10; (SignalException(CpU)); } diff --git a/cheri/cheri_types.sail b/cheri/cheri_types.sail index 031848f2..18043fa0 100644 --- a/cheri/cheri_types.sail +++ b/cheri/cheri_types.sail @@ -1,35 +1,54 @@ -(*========================================================================*) -(* *) -(* 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. *) -(*========================================================================*) +/*========================================================================*/ +/* */ +/* 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. */ +/*========================================================================*/ + +type CapLen = range(0, 2 ^ 65) + +enum CPtrCmpOp = { + CEQ, + CNE, + CLT, + CLE, + CLTU, + CLEU, + CEXEQ, + CNEXEQ +} + +enum ClearRegSet = { +GPLo, +GPHi, +CLo, +CHi +} -typedef CapLen = [|0 : 2**65|] diff --git a/mips_new_tc/mips_insts.sail b/mips_new_tc/mips_insts.sail index 6820aa8b..39f8c82b 100644 --- a/mips_new_tc/mips_insts.sail +++ b/mips_new_tc/mips_insts.sail @@ -577,7 +577,6 @@ function clause execute (SLTIU(rs, rt, imm)) = { let rs_val = rGPR(rs) in let immext : bits(64) = EXTS(imm) in /* NB defined to sign extend here even though comparison is unsigned! */ - let imm_val = unsigned(immext) in wGPR(rt) = EXTZ(if (rs_val <_u immext) then 0b1 else 0b0) } diff --git a/mips_new_tc/prelude.sail b/mips_new_tc/prelude.sail index 1add5bf8..abf13188 100644 --- a/mips_new_tc/prelude.sail +++ b/mips_new_tc/prelude.sail @@ -60,6 +60,9 @@ val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n) overload ~ = {not_bool, not_vec} +val not : bool -> bool +function not (b) = not_bool(b) + val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool function neq_vec (x, y) = not_bool(eq_vec(x, y)) @@ -225,7 +228,7 @@ overload operator / = {quotient_nat, quotient, quotient_real} val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot"} : (int, int) -> int val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod"} : (int, int) -> int -val modulus = {ocaml: "modulus", lem: "hardware_mod"} : (int, int) -> int +val modulus = {ocaml: "modulus", lem: "hardware_mod"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) overload operator % = {modulus} @@ -317,6 +320,9 @@ val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) function EXTS v = sign_extend(v, sizeof('m)) function EXTZ v = zero_extend(v, sizeof('m)) +val zeros : forall 'n, 'n >= 0 . unit -> bits('n) +function zeros() = replicate_bits (0b0,'n) + infix 4 <_s infix 4 >=_s infix 4 <_u |