summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKathy Gray2017-01-25 14:02:13 +0000
committerKathy Gray2017-01-25 14:02:13 +0000
commit2968c83f019b6945ac06a6faf8aaf518e92bdc29 (patch)
treea6f2bf7e5bbc7fa7420686db1ef2a69b71ff8c7b
parentf3426bab18961a59886e0100dcc93f7f8402f3a6 (diff)
parentf2c3c4d00d0004c73004b61b8e6c8096841e208b (diff)
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail
Diffstat
-rw-r--r--Makefile2
-rw-r--r--cheri/Makefile8
-rw-r--r--cheri/cheri_insts_128.sail973
-rw-r--r--cheri/cheri_prelude_128.sail569
-rw-r--r--mips/mips_prelude.sail5
-rw-r--r--src/Makefile14
-rw-r--r--src/lem_interp/interp_inter_imp.lem82
-rw-r--r--src/lem_interp/printing_functions.ml2
-rw-r--r--src/lem_interp/run_with_elf_cheri128.ml1364
-rw-r--r--src/lem_interp/sail_impl_base.lem41
10 files changed, 3055 insertions, 5 deletions
diff --git a/Makefile b/Makefile
index 51a51042..038249f6 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
.PHONY: all sail language clean archs
-all: sail
+all: sail interpreter
apply_header:
headache -c etc/headache_config -h etc/mips_header `ls mips/*.sail`
diff --git a/cheri/Makefile b/cheri/Makefile
index 200ddd5a..4e9a397a 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -1,7 +1,12 @@
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,CGetX)
+ $(call EXTRACT_INST,CGetPerms)
+ $(call EXTRACT_INST,CGetType)
+ $(call EXTRACT_INST,CGetBase)
+ $(call EXTRACT_INST,CGetOffset)
+ $(call EXTRACT_INST,CGetTag)
+ $(call EXTRACT_INST,CGetSealed)
$(call EXTRACT_INST,CGetPCC)
$(call EXTRACT_INST,CGetPCCSetOffset)
$(call EXTRACT_INST,CGetCause)
@@ -13,6 +18,7 @@ extract: cheri_insts.sail
$(call EXTRACT_INST,CIncOffset)
$(call EXTRACT_INST,CSetOffset)
$(call EXTRACT_INST,CSetBounds)
+ $(call EXTRACT_INST,CSetBoundsExact)
$(call EXTRACT_INST,CClearTag)
$(call EXTRACT_INST,ClearRegs)
$(call EXTRACT_INST,CFromPtr)
diff --git a/cheri/cheri_insts_128.sail b/cheri/cheri_insts_128.sail
new file mode 100644
index 00000000..1d2b37fb
--- /dev/null
+++ b/cheri/cheri_insts_128.sail
@@ -0,0 +1,973 @@
+(*========================================================================*)
+(* *)
+(* Copyright (c) 2015-2016 Robert M. Norton *)
+(* Copyright (c) 2015-2016 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. *)
+(*========================================================================*)
+
+(* 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
+
+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))
+(* NB CGetCause Handled separately *)
+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 : 0b01101 : (regno) rd : (regno) cb : 0b00000000 : 0b010) = Some(CGetOffset(rd, cb)) (* NB encoding does not follow pattern *)
+
+function clause execute (CGetPerm(rd, cb)) =
+{
+ (* 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 *)
+}
+
+function clause execute (CGetType(rd, cb)) =
+{
+ (* START_CGetType *)
+ checkCP2usable();
+ if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else
+ let capVal = readCapReg(cb) in
+ wGPR(rd) := EXTZ(capVal.otype);
+ (* END_CGetType *)
+}
+
+function clause execute (CGetBase(rd, cb)) =
+{
+ (* START_CGetBase *)
+ checkCP2usable();
+ if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else
+ let capVal = readCapReg(cb) in
+ wGPR(rd) := getCapBase(capVal);
+ (* END_CGetBase *)
+}
+
+function clause execute (CGetOffset(rd, cb)) =
+{
+ (* START_CGetOffset *)
+ checkCP2usable();
+ if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else
+ let capVal = readCapReg(cb) in
+ wGPR(rd) := getCapOffset(capVal);
+ (* END_CGetOffset *)
+}
+
+function clause execute (CGetLen(rd, cb)) =
+{
+ (* 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
+ let len64 = if unsigned(len65) > MAX_U64 then
+ (bit[64]) MAX_U64 else len65[63..0] in
+ wGPR(rd) := len64;
+ (* END_CGetLen *)
+}
+
+function clause execute (CGetTag(rd, cb)) =
+{
+ (* 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 *)
+}
+
+function clause execute (CGetSealed(rd, cb)) =
+{
+ (* 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 *)
+}
+
+union ast member regno CGetPCC
+function clause decode (0b010010 : 0b00000 : (regno) cd : 0b00000 : 0b11111 : 0b111111) = Some(CGetPCC(cd))
+function clause execute (CGetPCC(cd)) =
+{
+ (* 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, None); (* guaranteed to be in-bounds *)
+ writeCapReg(cd, pcc2)};
+ (* END_CGetPCC *)
+}
+
+
+union ast member (regno, regno) CGetPCCSetOffset
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) rs : 0b00111 : 0b111111) = Some(CGetPCCSetOffset(cd, rs))
+function clause execute (CGetPCCSetOffset(cd, rs)) =
+{
+ (* START_CGetPCCSetOffset *)
+ checkCP2usable();
+ if (register_inaccessible(cd)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+ else
+ let pcc = (capRegToCapStruct(PCC)) in
+ let rs_val = rGPR(rs) in
+ let (success, newPCC) = setCapOffset(pcc, rs_val) in
+ if (success) then
+ writeCapReg(cd, newPCC)
+ else
+ writeCapReg(cd, int_to_cap(rs_val));
+ (* END_CGetPCCSetOffset *)
+}
+(* Get and Set CP2 cause register *)
+
+union ast member regno CGetCause
+function clause decode (0b010010 : 0b00000 : (regno) rd : 0b00000 : 0b00000000 : 0b100) = Some(CGetCause(rd))
+function clause execute (CGetCause(rd)) =
+{
+ (* START_CGetCause *)
+ checkCP2usable();
+ if not (pcc_access_system_regs ()) then
+ raise_c2_exception_noreg(CapEx_AccessSystemRegsViolation)
+ else
+ wGPR(rd) := EXTZ(CapCause)
+ (* END_CGetCause *)
+}
+
+union ast member (regno) CSetCause
+function clause decode (0b010010 : 0b00100 : 0b00000 : 0b00000 : (regno) rt : 0b000 : 0b100) = Some(CSetCause(rt))
+function clause execute (CSetCause((regno) rt)) =
+{
+ (* 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];
+ }
+ (* END_CSetCause *)
+}
+
+union ast member regregreg CAndPerm
+function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CAndPerm(cd, cb, rt))
+function clause execute(CAndPerm(cd, cb, rt)) =
+{
+ (* START_CAndPerm *)
+ checkCP2usable();
+ 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 not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else
+ let perms = getCapPerms(cb_val) in
+ let newCap = setCapPerms(cb_val, (perms & rt_val[30..0])) in
+ writeCapReg(cd, newCap);
+ (* END_CAndPerm *)
+}
+
+
+
+union ast member regregreg CToPtr
+function clause decode (0b010010 : 0b01100 : (regno) rd : (regno) cb : (regno) ct : 0b000 : 0b000) = Some(CToPtr(rd, cb, ct))
+function clause execute(CToPtr(rd, cb, ct)) =
+{
+ (* START_CToPtr *)
+ checkCP2usable();
+ ct_val := readCapReg(ct);
+ 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 if not (ct_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, ct)
+ else
+ {
+ wGPR(rd) := if not (cb_val.tag) then
+ ((bit[64]) 0)
+ else
+ (bit[64])(getCapCursor(cb_val) - unsigned(getCapBase(ct_val)))
+ }
+ (* END_CToPtr *)
+}
+
+
+
+union ast member regregreg CSub
+function clause decode (0b010010 : 0b00000 : (regno) rd : (regno) cb : (regno) ct : 0b001010) = Some(CSub(rd, cb, ct))
+function clause execute(CSub(rd, cb, ct)) =
+{
+ (* START_CSub *)
+ checkCP2usable();
+ ct_val := readCapReg(ct);
+ 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])(getCapCursor(cb_val) - getCapCursor(ct_val))
+ }
+ (* END_CSub *)
+}
+
+union ast member (regno, regno, regno, CPtrCmpOp) CPtrCmp
+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 execute(CPtrCmp(rd, cb, ct, op)) =
+{
+ (* START_CPtrCmp *)
+ checkCP2usable();
+ if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if (register_inaccessible(ct)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+ else
+ {
+ cb_val := readCapReg(cb);
+ 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;
+ }
+ }
+ else
+ {
+ cursor1 := getCapCursor(cb_val);
+ cursor2 := getCapCursor(ct_val);
+ equal := (cursor1 == cursor2);
+ ltu := (cursor1 < cursor2);
+ lts := (((bit[64])cursor1) <_s ((bit[64])cursor2));
+ };
+ wGPR(rd) := EXTZ(switch (op) {
+ case CEQ -> [equal]
+ case CNE -> [not (equal)]
+ case CLT -> [lts]
+ case CLE -> [lts | equal]
+ case CLTU -> [ltu]
+ case CLEU -> [lts | equal]
+ case CEXEQ -> [cb_val == ct_val]
+ })
+ }
+ (* END_CPtrCmp *)
+}
+
+union ast member regregreg CIncOffset
+function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b000) = Some(CIncOffset(cd, cb, rt))
+function clause execute (CIncOffset(cd, cb, rt)) =
+{
+ (* START_CIncOffset *)
+ checkCP2usable();
+ 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 ((cb_val.tag) & (cb_val.sealed) & (rt_val != 0x0000000000000000)) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else
+ let (success, newCap) = incCapOffset(cb_val, rt_val) in
+ if (success) then
+ writeCapReg(cd, newCap)
+ else
+ writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val))
+ (* END_CIncOffset *)
+}
+
+union ast member regregreg CSetOffset
+function clause decode (0b010010 : 0b01101 : (regno) cd : (regno) cb : (regno) rt : 0b000 : 0b001) = Some(CSetOffset(cd, cb, rt))
+function clause execute (CSetOffset(cd, cb, rt)) =
+{
+ (* START_CSetOffset *)
+ checkCP2usable();
+ 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 ((cb_val.tag) & (cb_val.sealed)) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else
+ let (success, newCap) = setCapOffset(cb_val, rt_val) in
+ if (success) then
+ writeCapReg(cd, newCap)
+ else
+ writeCapReg(cd, int_to_cap(cb_val.address + rt_val))
+ (* END_CSetOffset *)
+}
+
+union ast member regregreg CSetBounds
+function clause decode (0b010010 : 0b00001 : (regno) cd : (regno) cb : (regno) rt : 0b000000) = Some(CSetBounds(cd, cb, rt))
+function clause execute (CSetBounds(cd, cb, rt)) =
+{
+ (* START_CSetBounds *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ rt_val := unsigned(rGPR(rt));
+ cursor := getCapCursor(cb_val);
+ base := unsigned(getCapBase(cb_val));
+ top := unsigned(getCapTop(cb_val));
+ newTop := cursor + rt_val;
+ 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 not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if (cursor < base) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ 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 *)
+}
+
+
+union ast member regregreg CSetBoundsExact
+function clause decode (0b010010 : 0b00000 : (regno) cd : (regno) cb : (regno) rt : 0b001001) = Some(CSetBoundsExact(cd, cb, rt))
+function clause execute (CSetBoundsExact(cd, cb, rt)) =
+{
+ (* START_CSetBoundsExact *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ rt_val := unsigned(rGPR(rt));
+ cursor := getCapCursor(cb_val);
+ base := unsigned(getCapBase(cb_val));
+ top := unsigned(getCapTop(cb_val));
+ 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 not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if (cursor < base) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if ((cursor + rt_val) > top) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else
+ let (exact, newCap) = setCapBounds(cb_val, (bit[64]) base, (bit[65]) top) in
+ if not (exact) then
+ raise_c2_exception(CapEx_InexactBounds, cb)
+ else
+ writeCapReg(cd, newCap)
+ (* END_CSetBoundsExact *)
+}
+
+union ast member (regno, regno) CClearTag
+function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : 0b00000 : 0b000: 0b101) = Some(CClearTag(cd, cb))
+function clause execute (CClearTag(cd, cb)) =
+{
+ (* START_CClearTag *)
+ 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
+ {
+ cb_val := readCapReg(cb);
+ writeCapReg(cd, {cb_val with tag = false});
+ }
+ (* END_CClearTag *)
+}
+
+union ast member (ClearRegSet, bit[16]) ClearRegs
+function clause decode (0b010010 : 0b01111 : 0b00000 : (bit[16]) imm) = Some(ClearRegs(GPLo, imm)) (* ClearLo *)
+function clause decode (0b010010 : 0b01111 : 0b00001 : (bit[16]) imm) = Some(ClearRegs(GPHi, imm)) (* ClearHi *)
+function clause decode (0b010010 : 0b01111 : 0b00010 : (bit[16]) imm) = Some(ClearRegs(CLo, imm)) (* CClearLo *)
+function clause decode (0b010010 : 0b01111 : 0b00011 : (bit[16]) imm) = Some(ClearRegs(CHi, imm)) (* CClearHi *)
+function clause execute (ClearRegs(regset, mask)) =
+{
+ (* 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
+ 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
+ }
+ (* END_ClearRegs *)
+}
+
+union ast member regregreg CFromPtr
+function clause decode (0b010010 : 0b00100 : (regno) cd : (regno) cb : (regno) rt : 0b000: 0b111) = Some(CFromPtr(cd, cb, rt))
+function clause execute (CFromPtr(cd, cb, rt)) =
+{
+ (* START_CFromPtr *)
+ checkCP2usable();
+ 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
+ writeCapReg(cd, null_cap)
+ else if not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else
+ let (success, newCap) = setCapOffset(cb_val, rt_val) in
+ if (success) then
+ writeCapReg(cd, newCap)
+ else
+ writeCapReg(cd, int_to_cap(getCapBase(cb_val) + rt_val))
+ (* END_CFromPtr *)
+}
+
+union ast member (regno, regno) CCheckPerm
+function clause decode (0b010010 : 0b01011 : (regno) cs : 0b00000 : (regno) rt : 0b000: 0b000) = Some(CCheckPerm(cs, rt))
+function clause execute (CCheckPerm(cs, rt)) =
+{
+ (* START_CCheckPerm *)
+ checkCP2usable();
+ cs_val := readCapReg(cs);
+ cs_perms := 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
+ raise_c2_exception(CapEx_TagViolation, cs)
+ else if ((cs_perms & rt_perms) != rt_perms) then
+ raise_c2_exception(CapEx_UserDefViolation, cs)
+ else
+ ()
+ (* END_CCheckPerm *)
+}
+
+union ast member (regno, regno) CCheckType
+function clause decode (0b010010 : 0b01011 : (regno) cs : (regno) cb : 0b00000 : 0b000: 0b001) = Some(CCheckType(cs, cb))
+function clause execute (CCheckType(cs, cb)) =
+{
+ (* START_CCheckType *)
+ checkCP2usable();
+ 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
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if not (cs_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cs)
+ else if not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if not (cs_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cs)
+ else if not (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if ((cs_val.otype) != (cb_val.otype)) then
+ raise_c2_exception(CapEx_TypeViolation, cs)
+ else
+ ()
+ (* END_CCheckType *)
+}
+
+union ast member regregreg CSeal
+function clause decode (0b010010 : 0b00010 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CSeal(cd, cs, ct))
+function clause execute (CSeal(cd, cs, ct)) =
+{
+ (* START_CSeal *)
+ checkCP2usable();
+ cs_val := readCapReg(cs);
+ ct_val := readCapReg(ct);
+ ct_cursor := getCapCursor(ct_val);
+ ct_top := unsigned(getCapTop(ct_val));
+ if (register_inaccessible(cd)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+ else if (register_inaccessible(cs)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+ else if (register_inaccessible(ct)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+ else if not (cs_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cs)
+ else if not (ct_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, ct)
+ else if (cs_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cs)
+ else if (ct_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, ct)
+ else if not (ct_val.permit_seal) then
+ raise_c2_exception(CapEx_PermitSealViolation, ct)
+ else if (ct_cursor >= ct_top) then
+ raise_c2_exception(CapEx_LengthViolation, 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
+ if not (success) then
+ raise_c2_exception(CapEx_InexactBounds, cs)
+ else
+ writeCapReg(cd, newCap)
+ (* END_CSeal *)
+}
+
+union ast member regregreg CUnseal
+function clause decode (0b010010 : 0b00011 : (regno) cd : (regno) cs : (regno) ct : 0b000: 0b000) = Some(CUnseal(cd, cs, ct))
+function clause execute (CUnseal(cd, cs, ct)) =
+{
+ (* START_CUnseal *)
+ checkCP2usable();
+ 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
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+ else if (register_inaccessible(ct)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, ct)
+ else if not (cs_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cs)
+ else if not (ct_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, ct)
+ else if not (cs_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cs)
+ else if (ct_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, ct)
+ else if (ct_cursor != unsigned(cs_val.otype)) then
+ raise_c2_exception(CapEx_TypeViolation, ct)
+ else if not (ct_val.permit_seal) then
+ raise_c2_exception(CapEx_PermitSealViolation, ct)
+ else if (ct_cursor >= unsigned(getCapTop(ct_val))) then
+ raise_c2_exception(CapEx_LengthViolation, ct)
+ else
+ writeCapReg(cd, {cs_val with
+ sealed=false;
+ otype=0;
+ global=(cs_val.global & ct_val.global)
+ })
+ (* END_CUnseal *)
+}
+
+union ast member (regno, regno) CCall
+function clause decode (0b010010 : 0b00101 : (regno) cs : (regno) cb : (bit[11]) selector) = Some(CCall(cs, cb))
+function clause execute (CCall(cs, cb)) =
+{
+ (* 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);
+ if (register_inaccessible(cs)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cs)
+ else if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if not (cs_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cs)
+ else if not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if not (cs_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cs)
+ else if not (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if ((cs_val.otype) != (cb_val.otype)) then
+ raise_c2_exception(CapEx_TypeViolation, cs)
+ else if not (cs_val.permit_execute) then
+ raise_c2_exception(CapEx_PermitExecuteViolation, cs)
+ else if (cb_val.permit_execute) then
+ raise_c2_exception(CapEx_PermitExecuteViolation, cb)
+ else if (getCapCursor(cs_val) >= unsigned(getCapTop(cs_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cs)
+ else
+ raise_c2_exception(CapEx_CallTrap, cs);
+ (* END_CCall *)
+}
+
+union ast member unit CReturn
+function clause decode (0b010010 : 0b00110 : 0b000000000000000000000) = Some(CReturn)
+function clause execute (CReturn) =
+{
+ (* START_CReturn *)
+ checkCP2usable();
+ raise_c2_exception_noreg(CapEx_ReturnTrap)
+ (* END_CReturn *)
+}
+
+union ast member (regno, bit[16], bool) CBX
+function clause decode (0b010010 : 0b01001 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, true)) (* CBTU *)
+function clause decode (0b010010 : 0b01010 : (regno) cb : (bit[16]) imm) = Some(CBX(cb, imm, false)) (* CBTS *)
+
+function clause execute (CBX(cb, imm, invert)) =
+{
+ (* 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;
+ }
+ (* END_CBx *)
+}
+
+union ast member (regno, regno, bool) CJALR
+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 *)
+function clause execute(CJALR(cd, cb, link)) =
+{
+ (* START_CJALR *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ cb_ptr := getCapCursor(cb_val);
+ cb_top := unsigned(getCapTop(cb_val));
+ if (link & register_inaccessible(cd)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cd)
+ else if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if not (cb_val.permit_execute) then
+ raise_c2_exception(CapEx_PermitExecuteViolation, cb)
+ else if not (cb_val.global) then
+ raise_c2_exception(CapEx_GlobalViolation, cb)
+ else if (cb_ptr + 4 > cb_top) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if ((cb_ptr mod 4) != 0) then
+ SignalException(AdEL)
+ else
+ {
+ if (link) then
+ let pcc = capRegToCapStruct(PCC) in
+ let (success, linkCap) = setCapOffset(pcc, PC+8) in
+ if (success) then
+ writeCapReg(cd, linkCap)
+ else
+ assert(false, None);
+ delayedPC := getCapOffset(cb_val);
+ delayedPCC := capStructToCapReg(cb_val);
+ branchPending := 1;
+ }
+ (* END_CJALR *)
+}
+
+union ast member (regno, regno, regno, bit[8], bool, WordType, bool) CLoad
+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 execute (CLoad(rd, cb, rt, offset, signext, width, linked)) =
+{
+ (* START_CLoad *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if not (cb_val.permit_load) then
+ 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]) vAddr;
+ if ((vAddr + size) > unsigned(getCapTop(cb_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if (vAddr < unsigned(getCapBase(cb_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if not (isAddressAligned(vAddr64, width)) then
+ SignalExceptionBadAddr(AdEL, vAddr64)
+ else
+ {
+ pAddr := (TLBTranslate(vAddr64, LoadData));
+ widthBytes := wordWidthBytes(width);
+ memResult := if (linked) then
+ {
+ CP0LLBit := 0b1;
+ CP0LLAddr := pAddr;
+ MEMr_reserve(pAddr, widthBytes);
+ }
+ else
+ MEMr(pAddr, widthBytes);
+ if (signext) then
+ wGPR(rd) := EXTS(memResult)
+ else
+ wGPR(rd) := EXTZ(memResult)
+ }
+ }
+ (* END_CLoad *)
+}
+
+union ast member (regno, regno, regno, regno, bit[8], WordType, bool) CStore
+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 execute (CStore(rs, cb, rt, rd, offset, width, conditional)) =
+{
+ (* START_CStore *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ if (register_inaccessible(cb)) then
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if not (cb_val.permit_store) then
+ 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]) vAddr;
+ if ((vAddr + size) > unsigned(getCapTop(cb_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if (vAddr < unsigned(getCapBase(cb_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if not (isAddressAligned(vAddr64, width)) then
+ SignalExceptionBadAddr(AdES, vAddr64)
+ else
+ {
+ pAddr := (TLBTranslate(vAddr64, StoreData));
+ rs_val := rGPR(rs);
+ if (conditional) then
+ {
+ success := if (CP0LLBit[0]) then
+ switch(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)
+ }
+ else
+ false;
+ wGPR(rd) := EXTZ([success]);
+ }
+ else
+ switch(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
+ }
+ }
+ }
+ (* END_CStore *)
+}
+
+union ast member (regno, regno, regno, regno, bit[11], bool) CSC
+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 execute (CSC(cs, cb, rt, rd, offset, conditional)) =
+{
+ (* START_CSC *)
+ checkCP2usable();
+ 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
+ raise_c2_exception(CapEx_AccessSystemRegsViolation, cb)
+ else if not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if not (cb_val.permit_store_cap) then
+ raise_c2_exception(CapEx_PermitStoreCapViolation, cb)
+ else if not (cb_val.permit_store_local_cap) & (cs_val.tag) & not (cs_val.global) then
+ raise_c2_exception(CapEx_PermitStoreLocalCapViolation, cb)
+ else
+ {
+ cursor := getCapCursor(cb_val);
+ vAddr := cursor + unsigned(rGPR(rt)) + (16 * signed(offset));
+ vAddr64:= (bit[64]) vAddr;
+ if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if (vAddr < unsigned(getCapBase(cb_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if ((vAddr mod cap_size) != 0) then
+ SignalExceptionBadAddr(AdES, vAddr64)
+ else
+ {
+ 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
+ MEMw_tagged_conditional(pAddr, cs_val.tag, capStructToMemBits(cs_val))
+ else
+ false;
+ wGPR(rd) := EXTZ([success]);
+ }
+ else
+ MEMw_tagged(pAddr, cs_val.tag, capStructToMemBits(cs_val));
+ }
+ }
+ (* END_CSC *)
+}
+
+union ast member (regno, regno, regno, bit[11], bool) CLC
+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 execute (CLC(cd, cb, rt, offset, linked)) =
+{
+ (* START_CLC *)
+ checkCP2usable();
+ cb_val := readCapReg(cb);
+ 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 not (cb_val.tag) then
+ raise_c2_exception(CapEx_TagViolation, cb)
+ else if (cb_val.sealed) then
+ raise_c2_exception(CapEx_SealViolation, cb)
+ else if not (cb_val.permit_load_cap) then
+ raise_c2_exception(CapEx_PermitLoadCapViolation, cb)
+ else
+ {
+ cursor := getCapCursor(cb_val);
+ vAddr := cursor + unsigned(rGPR(rt)) + (16*signed(offset));
+ vAddr64:= (bit[64]) vAddr;
+ if ((vAddr + cap_size) > unsigned(getCapTop(cb_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if (vAddr < unsigned(getCapBase(cb_val))) then
+ raise_c2_exception(CapEx_LengthViolation, cb)
+ else if ((vAddr mod cap_size) != 0) then
+ SignalExceptionBadAddr(AdEL, vAddr64)
+ else
+ {
+ let (pAddr, suppressTag) = (TLBTranslateC(vAddr64, LoadData)) in
+ let (tag, mem) = (if (linked)
+ then
+ {
+ CP0LLBit := 0b1;
+ CP0LLAddr := pAddr;
+ MEMr_tagged_reserve(pAddr);
+ }
+ else
+ (MEMr_tagged(pAddr)))
+ in
+ (CapRegs[cd]) := memBitsToCapBits(tag & not (suppressTag), mem);
+ }
+ }
+ (* END_CLC *)
+}
+
+union ast member (regno) C2Dump
+function clause decode (0b010010 : 0b00100 : (regno) rt : 0x0006) = Some(C2Dump(rt))
+function clause execute (C2Dump (rt)) =
+ () (* Currently a NOP *)
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail
new file mode 100644
index 00000000..323682b7
--- /dev/null
+++ b/cheri/cheri_prelude_128.sail
@@ -0,0 +1,569 @@
+(*========================================================================*)
+(* *)
+(* Copyright (c) 2015-2016 Robert M. Norton *)
+(* Copyright (c) 2015-2016 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. *)
+(*========================================================================*)
+
+(* 265-bit capability is really 257 bits including tag *)
+typedef CapReg = bit[129]
+
+register CapReg PCC
+register CapReg nextPCC
+register CapReg delayedPCC
+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
+ ]
+
+let num_uperms = 4
+
+
+typedef CapStruct = const struct {
+ bool tag;
+ bit[4] uperms;
+ bool access_system_regs;
+ bool perm_reserved9;
+ bool perm_reserved8;
+ 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;
+ bit[2] reserved;
+ bit[6] E;
+ bool sealed;
+ bit[20] B;
+ bit[20] T;
+ bit[24] otype;
+ bit[64] address;
+}
+
+let (CapStruct) null_cap = {
+ tag = false;
+ uperms = 0;
+ access_system_regs = false;
+ perm_reserved9 = false;
+ perm_reserved8 = false;
+ permit_seal = false;
+ permit_store_local_cap = false;
+ permit_store_cap = false;
+ permit_load_cap = false;
+ permit_store = false;
+ permit_load = false;
+ permit_execute = false;
+ global = false;
+ reserved = 0;
+ E = 48; (* encoded as 0 in memory due to xor *)
+ sealed = false;
+ B = 0;
+ T = 0;
+ otype = 0;
+ address = 0;
+}
+
+let (nat) max_otype = 0xffffff
+def Nat cap_size_t = 16 (* cap size in bytes *)
+let ([:cap_size_t:]) cap_size = 16
+let have_cp2 = true
+
+function CapStruct capRegToCapStruct((CapReg) c) =
+ let (bool) s = c[104] in
+ let (bit[20]) B = if s then c[103..96] : 0x000 else c[103..84] in
+ let (bit[20]) T = 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
+ {
+ tag = c[128];
+ uperms = c[127..124];
+ access_system_regs = c[123];
+ perm_reserved9 = c[122];
+ perm_reserved8 = c[121];
+ permit_seal = c[120];
+ permit_store_local_cap = c[119];
+ permit_store_cap = c[118];
+ permit_load_cap = c[117];
+ permit_store = c[116];
+ permit_load = c[115];
+ permit_execute = c[114];
+ global = c[113];
+ reserved = c[112..111];
+ E = c[110..105];
+ sealed = s;
+ B = B;
+ T = T;
+ otype = otype;
+ address = c[63..0];
+ }
+
+
+function (CapStruct) readCapReg((regno) n) =
+ capRegToCapStruct(CapRegs[n])
+
+function (bit[11]) getCapHardPerms((CapStruct) cap) =
+ ([cap.access_system_regs]
+ : [cap.perm_reserved9]
+ : [cap.perm_reserved8]
+ : [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 (bit[31]) getCapPerms((CapStruct) cap) =
+ let (bit[15]) perms = 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) =
+ { cap with
+ uperms = perms[18..15];
+(* perm_reserved11_14 = (cap.perm_reserved11_14 & (perms[14..11]));*)
+ access_system_regs = perms[10];
+ perm_reserved9 = perms[9];
+ perm_reserved8 = 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) =
+ if (((cap.T)[11..0] == 0) & ((cap.B)[11..0] == 0)) then
+ (true, {cap with sealed=true; otype=otype})
+ else
+ (false, undefined)
+
+function (bit[128]) capStructToMemBits((CapStruct) cap) =
+ let (bit[20]) b = if cap.sealed then (cap.B)[23..12] : (cap.otype)[23..12] else cap.B in
+ let (bit[20]) t = if cap.sealed then (cap.T)[23..12] : (cap.otype)[11..0] else cap.T in
+ ( cap.uperms
+ : getCapHardPerms(cap)
+ : cap.reserved
+ : cap.E
+ : [cap.sealed]
+ : b
+ : t
+ : cap.address
+ )
+
+function (CapReg) capStructToCapReg((CapStruct) cap) =
+ ([cap.tag] : capStructToMemBits(cap))
+
+(* Reverse of above used when reading from memory *)
+function (CapReg) memBitsToCapBits((bool) tag, (bit[128]) b) =
+ ([tag]
+ : b
+ )
+
+function unit writeCapReg((regno) n, (CapStruct) cap) =
+ {
+ CapRegs[n] := capStructToCapReg(cap)
+ }
+
+
+function int 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
+ }
+
+function bit[64] getCapBase((CapStruct) c) =
+ let ([|63|]) E = unsigned(c.E) in
+ let (bool) s = c.sealed in
+ let (bit[20]) B = c.B in
+ let (bit[64]) a = c.address in
+ let (bit[20]) R = B - 0x00100 in (* wraps *)
+ let (bit[20]) a_mid = a[(E + 19)..E] in
+ let (int) correction = a_top_correction(a_mid, R, B) in
+ let a_top = a[63..(E+20)] in
+ let (bit[64]) base = EXTZ((a_top + correction) : B) in
+ base << E
+
+function bit[65] getCapTop((CapStruct) c) =
+ let ([|63|]) E = unsigned(c.E) in
+ let (bool) s = c.sealed in
+ let (bit[20]) B = c.B in
+ let (bit[20]) T = c.T in
+ let (bit[64]) a = c.address in
+ let (bit[20]) R = B - 0x00100 in (* wraps *)
+ let (bit[20]) a_mid = a[(E + 19)..E] in
+ let (int) correction = a_top_correction(a_mid, R, T) in
+ let a_top = a[63..(E+20)] in
+ let (bit[65]) top1 = EXTZ((a_top + correction) : T) in
+ top1 << E
+
+function bit[64] getCapOffset((CapStruct) c) =
+ let base = getCapBase(c) in
+ c.address - base
+
+function bit[65] getCapLength((CapStruct) c) = getCapTop(c) - (0b0 : getCapBase(c))
+
+function nat getCapCursor((CapStruct) cap) = unsigned(cap.address)
+
+function (bool, CapStruct) setCapOffset((CapStruct) c, (bit[64]) offset) =
+ let oldBase = getCapBase(c) in
+ let oldTop = getCapTop(c) in
+ let (bit[64]) newAddress = oldBase + offset in
+ let newCap = { c with address = newAddress } in
+ let newBase = getCapBase(newCap) in
+ let newTop = getCapTop(newCap) in
+ let representable = (oldBase == newBase) & (oldTop == newTop) in
+ (representable, newCap)
+
+function (bool, CapStruct) incCapOffset((CapStruct) c, (bit[64]) delta) =
+ let oldBase = getCapBase(c) in
+ let oldTop = getCapTop(c) in
+ let (bit[64]) newAddress = c.address + delta in
+ let newCap = { c with address = newAddress } in
+ let newBase = getCapBase(newCap) in
+ let newTop = getCapTop(newCap) in
+ let representable = (oldBase == newBase) & (oldTop == newTop) in
+ (representable, newCap)
+
+(** FUNCTION:integer HighestSetBit(bits(N) x) *)
+
+function forall Nat 'N. option<[|0:('N + -1)|]> HighestSetBit((bit['N]) x) = {
+ let N = (length(x)) in {
+ ([|('N + -1)|]) result := 0;
+ (bool) break := false;
+ foreach (i from (N - 1) downto 0)
+ if ~(break) & x[i] == 1 then {
+ result := i;
+ break := true;
+ };
+
+ if break then Some(result) else None;
+}}
+
+function (bit[6]) computeE ((bit[65]) rlength) =
+ let msb = HighestSetBit((rlength + (rlength >> 6)) >> 19) in
+ switch (msb) {
+ case (Some(b)) -> (bit[6]) b (* hw rounds up to multiple of 4 *)
+ case 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 (bit[6]) e = computeE(top - (0b0 : base)) in
+ let (bit[20]) B = 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=e; B=B; 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) =
+ {null_cap with address = offset}
+
+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;
+}
+
+typedef CPtrCmpOp = enumerate {
+ CEQ;
+ CNE;
+ CLT;
+ CLE;
+ CLTU;
+ CLEU;
+ CEXEQ;
+}
+
+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
+ }
+
+typedef CapCauseReg = register bits [15:0] {
+ 15..8: ExcCode;
+ 7..0: RegNum;
+}
+
+register CapCauseReg CapCause
+
+function forall Type 'o . 'o SignalException ((Exception) ex) =
+ {
+ C31 := PCC;
+ (*C31.offset := PC; XXX fix this *)
+ nextPCC := C29; (* KCC *)
+ delayedPCC := C29; (* always write delayedPCC together whether PCC so
+ that non-capability branches don't override PCC *)
+ SignalExceptionMIPS(ex, getCapBase(capRegToCapStruct(C29)));
+ }
+
+function unit ERETHook() =
+ {
+ nextPCC := C31;
+ delayedPCC := C31; (* always write delayedPCC together whether PCC so
+ that non-capability branches don't override PCC *)
+ }
+
+function forall Type 'o . 'o raise_c2_exception8((CapEx) capEx, (bit[8]) 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) =
+ raise_c2_exception8(capEx, 0b000 : regnum)
+
+function forall Type 'o . 'o raise_c2_exception_noreg((CapEx) capEx) =
+ raise_c2_exception8(capEx, 0xff)
+
+function bool pcc_access_system_regs () =
+ let pcc = capRegToCapStruct(PCC) in
+ (pcc.access_system_regs)
+
+function bool register_inaccessible((regno) r) =
+ let is_sys_reg = switch(r) {
+ case 0b11011 -> true
+ case 0b11100 -> true
+ case 0b11101 -> true
+ case 0b11110 -> true
+ case 0b11111 -> true
+ case _ -> false
+ } in
+ if is_sys_reg then
+ not (pcc_access_system_regs ())
+ else
+ false
+
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * ('n + 1)]) effect { rmem } MEMr_tag_reserve
+
+val extern (bit[64] , bit[8]) -> unit effect { wmem } TAGw
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|]) -> unit effect { eamem } MEMea_tag_conditional
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> unit effect { wmv } MEMval_tag
+val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8 * ('n + 1)]) -> bool effect { wmv } MEMval_tag_conditional
+
+
+function (bool, bit[cap_size_t * 8]) MEMr_tagged ((bit[64]) addr) =
+{
+ (* assumes addr is cap. aligned *)
+ let ((bit[8]) tag : mem) = (MEMr_tag (addr, cap_size)) in
+ (tag[0], mem)
+}
+
+function (bool, bit[cap_size_t * 8]) MEMr_tagged_reserve ((bit[64]) addr) =
+{
+ (* assumes addr is cap. aligned *)
+ let ((bit[8]) tag : mem) = (MEMr_tag_reserve (addr, cap_size)) in
+ (tag[0], mem)
+}
+
+function unit MEMw_tagged((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
+{
+ (* assumes addr is cap. aligned *)
+ MEMea_tag(addr, cap_size);
+ MEMval_tag(addr, cap_size, 0b0000000 : [tag] : data);
+}
+
+function bool MEMw_tagged_conditional((bit[64]) addr, (bool) tag, (bit[cap_size_t * 8]) data) =
+{
+ (* assumes addr is cap. aligned *)
+ MEMea_tag_conditional(addr, cap_size);
+ MEMval_tag_conditional(addr, cap_size, 0b0000000 : [tag] : data);
+}
+
+function unit effect {wmem} MEMw_wrapper(addr, size, data) =
+ if (addr == 0x000000007f000000) then
+ {
+ UART_WDATA := data[31..24];
+ UART_WRITTEN := 1;
+ }
+ else
+ {
+ (* On cheri non-capability writes must clear the corresponding tag
+ XXX this is vestigal and only works on sequential modle -- tag clearing
+ should probably be done in memory model. *)
+ TAGw((addr[63..4] : 0b0000), 0x00);
+ MEMea(addr,size);
+ MEMval(addr, size, data);
+ }
+
+function bool effect {wmem} MEMw_conditional_wrapper(addr, size, data) =
+ {
+ (* On cheri non-capability writes must clear the corresponding tag*)
+ MEMea_conditional(addr, size);
+ success := MEMval_conditional(addr,size,data);
+ if (success) then
+ (* XXX as above TAGw is vestigal and must die *)
+ TAGw((addr[63..4] : 0b0000), 0x00);
+ success;
+ }
+
+function bit[64] addrWrapper((bit[64]) addr, (MemAccessType) accessType, (WordType) width) =
+ {
+ capno := 0b00000;
+ cap := readCapReg(capno);
+ if (~(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))
+ };
+ cursor := getCapCursor(cap);
+ vAddr := cursor + unsigned(addr);
+ size := wordWidthBytes(width);
+ base := unsigned(getCapBase(cap));
+ top := unsigned(getCapTop(cap));
+ if ((vAddr + size) > top) then
+ (raise_c2_exception(CapEx_LengthViolation, capno))
+ else if (vAddr < (base)) then
+ (raise_c2_exception(CapEx_LengthViolation, capno))
+ else
+ (bit[64]) vAddr; (* XXX vAddr not truncated because top <= 2^64 and size > 0 *)
+ }
+
+function (bit[64]) TranslateAddress ((bit[64]) vAddr, (MemAccessType) accessType) = {
+ incrementCP0Count();
+ let pcc = capRegToCapStruct(PCC) in
+ let base = unsigned(getCapBase(pcc)) in
+ let top = unsigned(getCapTop(pcc)) in
+ let absPC = (unsigned(vAddr)) in
+ if ((absPC mod 4) != 0) then (* bad PC alignment *)
+ (SignalExceptionBadAddr(AdEL, (bit[64]) absPC)) (* XXX absPC may be truncated *)
+ else if ((absPC + 4) > top) then
+ (raise_c2_exception_noreg(CapEx_LengthViolation))
+ else
+ TLBTranslate((bit[64]) absPC, accessType) (* XXX assert absPC never gets truncated due to above check and top <= 2^64 for valid caps *)
+}
+
+function unit checkCP2usable () =
+ {
+ if (~((CP0Status.CU)[2])) then
+ {
+ (CP0Cause.CE) := 0b10;
+ (SignalException(CpU));
+ }
+ }
+
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 80350af1..8975193c 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -89,8 +89,9 @@ let ([:64:]) TLBNumEntries = 64
typedef TLBIndexT = (bit[6])
let (TLBIndexT) TLBIndexMax = 0b111111
-let MAX_VA = unsigned(0xffffffffff)
-let MAX_PA = unsigned(0xfffffffff)
+let MAX_U64 = unsigned(0xffffffffffffffff)
+let MAX_VA = unsigned(0xffffffffff)
+let MAX_PA = unsigned(0xfffffffff)
typedef TLBEntry = register bits [116 : 0] {
116 .. 101: pagemask;
diff --git a/src/Makefile b/src/Makefile
index fb71396d..594f5c15 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -42,6 +42,8 @@ CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_prelude.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_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude.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:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts_128.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+
elf:
make -C $(ELFDIR)
@@ -56,6 +58,10 @@ _build/run_with_elf_cheri.ml: lem_interp/run_with_elf_cheri.ml
mkdir -p _build
cp $< $@
+_build/run_with_elf_cheri128.ml: lem_interp/run_with_elf_cheri128.ml
+ mkdir -p _build
+ cp $< $@
+
_build/mips.lem: $(MIPS_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
@@ -76,6 +82,11 @@ _build/cheri.lem: $(CHERI_SAILS) ./sail.native
cd _build ;\
../sail.native -lem_ast -o cheri $(CHERI_SAILS)
+_build/cheri128.lem: $(CHERI128_SAILS) ./sail.native
+ mkdir -p _build
+ cd _build ;\
+ ../sail.native -lem_ast -o cheri128 $(CHERI128_SAILS)
+
_build/cheri_notlb.lem: $(CHERI_NOTLB_SAILS) ./sail.native
mkdir -p _build
cd _build ;\
@@ -111,6 +122,9 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int
run_cheri.native: _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml -o run_cheri.native
+run_cheri128.native: _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml interpreter
+ env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri128.ml _build/mips_extras.ml _build/run_with_elf_cheri128.ml -o run_cheri128.native
+
mips_notlb: _build/mips_notlb.ml _build/mips_embed_types.lem _build/mips_extras.ml
true
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index cbd56240..75e695eb 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1215,3 +1215,85 @@ let interp_instruction_analysis
end in
(regs_in, regs_out, regs_feeding_address, nias, dia, inst_kind)
+
+let interp_handwritten_instruction_analysis context endianness instruction analysis_function reg_info environment =
+ fst (instruction_analysis context endianness analysis_function
+ reg_info (Just environment) instruction)
+
+
+
+val print_and_fail_of_inequal : forall 'a. Show 'a =>
+ (string -> unit) ->
+ (instruction -> string) ->
+ (string * 'a) -> (string * 'a) -> unit
+let print_and_fail_if_inequal
+ (print_endline,pp_instruction,instruction)
+ (name1,xs1) (name2,xs2) =
+ if xs1 = xs2 then ()
+ else
+ let () = print_endline (name1^": "^show xs1) in
+ let () = print_endline (name2^": "^show xs2) in
+ failwith (name1^" and "^ name2^" inequal for instruction " ^ pp_instruction instruction)
+
+let interp_compare_analyses
+ print_endline
+ pp_instruction
+ (non_pseudo_registers : set reg_name -> set reg_name)
+ context
+ endianness
+ interp_exhaustive
+ instruction
+ nia_reg
+ ism
+ environment
+ analysis_function
+ reg_info =
+ let (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1) =
+ interp_instruction_analysis interp_exhaustive instruction nia_reg ism
+ environment in
+ let (regs_in1S,regs_out1S,regs_feeding_address1S,nias1S) =
+ (Set.fromList regs_in1,
+ Set.fromList regs_out1,
+ Set.fromList regs_feeding_address1,
+ Set.fromList nias1) in
+ let (regs_in1S,regs_out1S,regs_feeding_addres1S) =
+ (non_pseudo_registers regs_in1S,
+ non_pseudo_registers regs_out1S,
+ non_pseudo_registers regs_feeding_address1S) in
+
+ let (regs_in2,regs_out2,regs_feeding_address2,nias2,dia2,inst_kind2) =
+ interp_handwritten_instruction_analysis
+ context endianness instruction analysis_function reg_info environment in
+ let (regs_in2S,regs_out2S,regs_feeding_address2S,nias2S) =
+ (Set.fromList regs_in2,
+ Set.fromList regs_out2,
+ Set.fromList regs_feeding_address2,
+ Set.fromList nias2) in
+ let (regs_in2S,regs_out2S,regs_feeding_addres2S) =
+ (non_pseudo_registers regs_in2S,
+ non_pseudo_registers regs_out2S,
+ non_pseudo_registers regs_feeding_address2S) in
+
+ let aux = (print_endline,pp_instruction,instruction) in
+ let () = (print_and_fail_if_inequal aux)
+ ("regs_in exhaustive",regs_in1S)
+ ("regs_in hand",regs_in2S) in
+ let () = (print_and_fail_if_inequal aux)
+ ("regs_out exhaustive",regs_out1S)
+ ("regs_out hand",regs_out2S) in
+ let () = (print_and_fail_if_inequal aux)
+ ("regs_feeding_address exhaustive",regs_feeding_address1S)
+ ("regs_feeding_address hand",regs_feeding_address2S) in
+ let () = (print_and_fail_if_inequal aux)
+ ("nias exhaustive",nias1S)
+ ("nias hand",nias2S) in
+ let () = (print_and_fail_if_inequal aux)
+ ("dia exhaustive",dia1)
+ ("dia hand",dia2) in
+ let () = (print_and_fail_if_inequal aux)
+ ("inst_kind exhaustive",inst_kind1)
+ ("inst_kind hand",inst_kind2) in
+
+ (regs_in1,regs_out1,regs_feeding_address1,nias1,dia1,inst_kind1)
+
+
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 760b0a35..202af6bb 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -150,7 +150,7 @@ let bit_lifteds_to_string ?(collapse=true) (bls: bit_lifted list) (show_length_a
else
"0x"^s
else
- simple_bit_lifteds_to_string bls show_length_and_start starto
+ simple_bit_lifteds_to_string ~collapse:collapse bls show_length_and_start starto
let register_value_to_string rv =
diff --git a/src/lem_interp/run_with_elf_cheri128.ml b/src/lem_interp/run_with_elf_cheri128.ml
new file mode 100644
index 00000000..99a6e681
--- /dev/null
+++ b/src/lem_interp/run_with_elf_cheri128.ml
@@ -0,0 +1,1364 @@
+open Printf ;;
+open Format ;;
+open Big_int ;;
+open Interp_ast ;;
+open Interp_interface ;;
+open Interp_inter_imp ;;
+open Run_interp_model ;;
+open Sail_impl_base ;;
+open Sail_interface ;;
+
+module StringMap = Map.Make(String)
+
+let file = ref "" ;;
+
+let rec foldli f acc ?(i=0) = function
+ | [] -> acc
+ | x::xs -> foldli f (f i acc x) ~i:(i+1) xs
+;;
+
+let endian = ref E_big_endian ;;
+
+let hex_to_big_int s = big_int_of_int64 (Int64.of_string s) ;;
+
+let data_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;;
+let prog_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref) ;;
+let tag_mem = (ref Mem.empty : (memory_byte Run_interp_model.Mem.t) ref);;
+let reg = ref Reg.empty ;;
+let input_buf = (ref [] : int list ref);;
+
+let add_mem byte addr mem =
+ assert(byte >= 0 && byte < 256);
+ (*Printf.printf "add_mem %s: 0x%02x\n" (Uint64.to_string_hex (Uint64.of_string (Nat_big_num.to_string addr))) byte;*)
+ let mem_byte = memory_byte_of_int byte in
+ let zero_byte = memory_byte_of_int 0 in
+ mem := Mem.add addr mem_byte !mem;
+ tag_mem := Mem.add addr zero_byte !tag_mem
+
+let get_reg reg name =
+ let reg_content = Reg.find name reg in reg_content
+
+let rec load_memory_segment' (bytes,addr) mem =
+ match bytes with
+ | [] -> ()
+ | byte::bytes' ->
+ let data_byte = Char.code byte in
+ let addr' = Nat_big_num.succ addr in
+ begin add_mem data_byte addr mem;
+ load_memory_segment' (bytes',addr') mem
+ end
+
+let rec load_memory_segment (segment: Elf_interpreted_segment.elf64_interpreted_segment) mem =
+ let (Byte_sequence.Sequence bytes) = segment.Elf_interpreted_segment.elf64_segment_body in
+ let addr = segment.Elf_interpreted_segment.elf64_segment_paddr in
+ load_memory_segment' (bytes,addr) mem
+
+
+let rec load_memory_segments segments =
+ begin match segments with
+ | [] -> ()
+ | segment::segments' ->
+ let (x,w,r) = segment.Elf_interpreted_segment.elf64_segment_flags in
+ begin
+ load_memory_segment segment prog_mem;
+ load_memory_segments segments'
+ end
+ end
+
+let rec read_mem mem address length =
+ if length = 0
+ then []
+ else
+ let byte =
+ try Mem.find address mem with
+ | Not_found -> failwith "start address not found"
+ in
+ byte :: (read_mem mem (Nat_big_num.succ address) (length - 1))
+
+let register_state_zero register_data rbn : register_value =
+ let (dir,width,start_index) =
+ try List.assoc rbn register_data with
+ | Not_found -> failwith ("register_state_zero lookup failed (" ^ rbn)
+ in register_value_zeros dir width start_index
+
+type model = PPC | AArch64 | MIPS
+(*
+let ppc_register_data_all = [
+ (*Pseudo registers*)
+ ("CIA", (D_increasing, 64, 0));
+ ("NIA", (D_increasing, 64, 0));
+ ("mode64bit", (D_increasing, 1, 0));
+ ("bigendianmode", (D_increasing, 1, 0));
+ (* special registers *)
+ ("CR", (D_increasing, 32, 32));
+ ("CTR", (D_increasing, 64, 0 ));
+ ("LR", (D_increasing, 64, 0 ));
+ ("XER", (D_increasing, 64, 0 ));
+ ("VRSAVE",(D_increasing, 32, 32));
+ ("FPSCR", (D_increasing, 64, 0 ));
+ ("VSCR", (D_increasing, 32, 96));
+
+ (* general purpose registers *)
+ ("GPR0", (D_increasing, 64, 0 ));
+ ("GPR1", (D_increasing, 64, 0 ));
+ ("GPR2", (D_increasing, 64, 0 ));
+ ("GPR3", (D_increasing, 64, 0 ));
+ ("GPR4", (D_increasing, 64, 0 ));
+ ("GPR5", (D_increasing, 64, 0 ));
+ ("GPR6", (D_increasing, 64, 0 ));
+ ("GPR7", (D_increasing, 64, 0 ));
+ ("GPR8", (D_increasing, 64, 0 ));
+ ("GPR9", (D_increasing, 64, 0 ));
+ ("GPR10", (D_increasing, 64, 0 ));
+ ("GPR11", (D_increasing, 64, 0 ));
+ ("GPR12", (D_increasing, 64, 0 ));
+ ("GPR13", (D_increasing, 64, 0 ));
+ ("GPR14", (D_increasing, 64, 0 ));
+ ("GPR15", (D_increasing, 64, 0 ));
+ ("GPR16", (D_increasing, 64, 0 ));
+ ("GPR17", (D_increasing, 64, 0 ));
+ ("GPR18", (D_increasing, 64, 0 ));
+ ("GPR19", (D_increasing, 64, 0 ));
+ ("GPR20", (D_increasing, 64, 0 ));
+ ("GPR21", (D_increasing, 64, 0 ));
+ ("GPR22", (D_increasing, 64, 0 ));
+ ("GPR23", (D_increasing, 64, 0 ));
+ ("GPR24", (D_increasing, 64, 0 ));
+ ("GPR25", (D_increasing, 64, 0 ));
+ ("GPR26", (D_increasing, 64, 0 ));
+ ("GPR27", (D_increasing, 64, 0 ));
+ ("GPR28", (D_increasing, 64, 0 ));
+ ("GPR29", (D_increasing, 64, 0 ));
+ ("GPR30", (D_increasing, 64, 0 ));
+ ("GPR31", (D_increasing, 64, 0 ));
+ (* vector registers *)
+ ("VR0", (D_increasing, 128, 0 ));
+ ("VR1", (D_increasing, 128, 0 ));
+ ("VR2", (D_increasing, 128, 0 ));
+ ("VR3", (D_increasing, 128, 0 ));
+ ("VR4", (D_increasing, 128, 0 ));
+ ("VR5", (D_increasing, 128, 0 ));
+ ("VR6", (D_increasing, 128, 0 ));
+ ("VR7", (D_increasing, 128, 0 ));
+ ("VR8", (D_increasing, 128, 0 ));
+ ("VR9", (D_increasing, 128, 0 ));
+ ("VR10", (D_increasing, 128, 0 ));
+ ("VR11", (D_increasing, 128, 0 ));
+ ("VR12", (D_increasing, 128, 0 ));
+ ("VR13", (D_increasing, 128, 0 ));
+ ("VR14", (D_increasing, 128, 0 ));
+ ("VR15", (D_increasing, 128, 0 ));
+ ("VR16", (D_increasing, 128, 0 ));
+ ("VR17", (D_increasing, 128, 0 ));
+ ("VR18", (D_increasing, 128, 0 ));
+ ("VR19", (D_increasing, 128, 0 ));
+ ("VR20", (D_increasing, 128, 0 ));
+ ("VR21", (D_increasing, 128, 0 ));
+ ("VR22", (D_increasing, 128, 0 ));
+ ("VR23", (D_increasing, 128, 0 ));
+ ("VR24", (D_increasing, 128, 0 ));
+ ("VR25", (D_increasing, 128, 0 ));
+ ("VR26", (D_increasing, 128, 0 ));
+ ("VR27", (D_increasing, 128, 0 ));
+ ("VR28", (D_increasing, 128, 0 ));
+ ("VR29", (D_increasing, 128, 0 ));
+ ("VR30", (D_increasing, 128, 0 ));
+ ("VR31", (D_increasing, 128, 0 ));
+ (* floating-point registers *)
+ ("FPR0", (D_increasing, 64, 0 ));
+ ("FPR1", (D_increasing, 64, 0 ));
+ ("FPR2", (D_increasing, 64, 0 ));
+ ("FPR3", (D_increasing, 64, 0 ));
+ ("FPR4", (D_increasing, 64, 0 ));
+ ("FPR5", (D_increasing, 64, 0 ));
+ ("FPR6", (D_increasing, 64, 0 ));
+ ("FPR7", (D_increasing, 64, 0 ));
+ ("FPR8", (D_increasing, 64, 0 ));
+ ("FPR9", (D_increasing, 64, 0 ));
+ ("FPR10", (D_increasing, 64, 0 ));
+ ("FPR11", (D_increasing, 64, 0 ));
+ ("FPR12", (D_increasing, 64, 0 ));
+ ("FPR13", (D_increasing, 64, 0 ));
+ ("FPR14", (D_increasing, 64, 0 ));
+ ("FPR15", (D_increasing, 64, 0 ));
+ ("FPR16", (D_increasing, 64, 0 ));
+ ("FPR17", (D_increasing, 64, 0 ));
+ ("FPR18", (D_increasing, 64, 0 ));
+ ("FPR19", (D_increasing, 64, 0 ));
+ ("FPR20", (D_increasing, 64, 0 ));
+ ("FPR21", (D_increasing, 64, 0 ));
+ ("FPR22", (D_increasing, 64, 0 ));
+ ("FPR23", (D_increasing, 64, 0 ));
+ ("FPR24", (D_increasing, 64, 0 ));
+ ("FPR25", (D_increasing, 64, 0 ));
+ ("FPR26", (D_increasing, 64, 0 ));
+ ("FPR27", (D_increasing, 64, 0 ));
+ ("FPR28", (D_increasing, 64, 0 ));
+ ("FPR29", (D_increasing, 64, 0 ));
+ ("FPR30", (D_increasing, 64, 0 ));
+ ("FPR31", (D_increasing, 64, 0 ));
+]
+
+let initial_stack_and_reg_data_of_PPC_elf_file e_entry all_data_memory =
+ (* set up initial registers, per 3.4.1 of 64-bit PowerPC ELF Application Binary Interface Supplement 1.9 *)
+
+ let auxiliary_vector_space = Nat_big_num.of_string "17592186042368" (*"0xffffffff800"*) in
+ (* notionally there should be at least an AT_NULL auxiliary vector entry there, but our examples will never read it *)
+
+ (* take start of stack roughly where running gdb on hello5 on bim says it is*)
+ let initial_GPR1_stack_pointer = Nat_big_num.of_string "17592186040320" (*"0xffffffff000"*) in
+ let initial_GPR1_stack_pointer_value =
+ Sail_impl_base.register_value_of_integer 64 0 Sail_impl_base.D_increasing initial_GPR1_stack_pointer in
+ (* ELF says we need an initial zero doubleword there *)
+ let initial_stack_data =
+ (* the code actually uses the stack, both above and below, so we map a bit more memory*)
+ (* this is a fairly big but arbitrary chunk *)
+ (* let initial_stack_data_address = Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128) in
+ [("initial_stack_data", initial_stack_data_address, Lem_list.replicate (128+32) 0 ))] in *)
+ (* this is the stack memory that test 1938 actually uses *)
+ [ ("initial_stack_data1", Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128),
+ Lem_list.replicate 8 0 );
+ ("initial_stack_data2", Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 8),
+ Lem_list.replicate 8 0 );
+ ("initial_stack_data3", Nat_big_num.add initial_GPR1_stack_pointer (Nat_big_num.of_int 16),
+ Lem_list.replicate 8 0 )] in
+
+ (* read TOC from the second field of the function descriptor pointed to by e_entry*)
+ let initial_GPR2_TOC =
+ Sail_impl_base.register_value_of_address
+ (Sail_impl_base.address_of_byte_list
+ (List.map (fun b -> match b with Some b -> b | None -> failwith "Address had undefined")
+ (List.map byte_of_byte_lifted
+ (read_mem all_data_memory
+ (Nat_big_num.add (Nat_big_num.of_int 8) e_entry) 8))))
+ Sail_impl_base.D_increasing in
+ (* these initial register values are all mandated to be zero, but that's handled by the generic zeroing below
+ let initial_GPR3_argc = (Nat_big_num.of_int 0) in
+ let initial_GPR4_argv = (Nat_big_num.of_int 0) in
+ let initial_GPR5_envp = (Nat_big_num.of_int 0) in
+ let initial_FPSCR = (Nat_big_num.of_int 0) in
+ *)
+ let initial_register_abi_data : (string * Sail_impl_base.register_value) list =
+ [ ("GPR1", initial_GPR1_stack_pointer_value);
+ ("GPR2", initial_GPR2_TOC);
+ (*
+ ("GPR3", initial_GPR3_argc);
+ ("GPR4", initial_GPR4_argv);
+ ("GPR5", initial_GPR5_envp);
+ ("FPSCR", initial_FPSCR);
+ *)
+ ] in
+
+ (initial_stack_data, initial_register_abi_data)
+
+
+let aarch64_reg bit_count name = (name, (D_decreasing, bit_count, bit_count - 1))
+
+let aarch64_PC_data = [aarch64_reg 64 "_PC"]
+
+(* most of the PSTATE fields are aliases to other registers so they
+ don't appear here *)
+let aarch64_PSTATE_data = [
+ aarch64_reg 1 "PSTATE_nRW";
+ aarch64_reg 1 "PSTATE_E";
+ aarch64_reg 5 "PSTATE_M";
+]
+
+let aarch64_general_purpose_registers_data = [
+ aarch64_reg 64 "R0";
+ aarch64_reg 64 "R1";
+ aarch64_reg 64 "R2";
+ aarch64_reg 64 "R3";
+ aarch64_reg 64 "R4";
+ aarch64_reg 64 "R5";
+ aarch64_reg 64 "R6";
+ aarch64_reg 64 "R7";
+ aarch64_reg 64 "R8";
+ aarch64_reg 64 "R9";
+ aarch64_reg 64 "R10";
+ aarch64_reg 64 "R11";
+ aarch64_reg 64 "R12";
+ aarch64_reg 64 "R13";
+ aarch64_reg 64 "R14";
+ aarch64_reg 64 "R15";
+ aarch64_reg 64 "R16";
+ aarch64_reg 64 "R17";
+ aarch64_reg 64 "R18";
+ aarch64_reg 64 "R19";
+ aarch64_reg 64 "R20";
+ aarch64_reg 64 "R21";
+ aarch64_reg 64 "R22";
+ aarch64_reg 64 "R23";
+ aarch64_reg 64 "R24";
+ aarch64_reg 64 "R25";
+ aarch64_reg 64 "R26";
+ aarch64_reg 64 "R27";
+ aarch64_reg 64 "R28";
+ aarch64_reg 64 "R29";
+ aarch64_reg 64 "R30";
+]
+
+let aarch64_SIMD_registers_data = [
+ aarch64_reg 128 "V0";
+ aarch64_reg 128 "V1";
+ aarch64_reg 128 "V2";
+ aarch64_reg 128 "V3";
+ aarch64_reg 128 "V4";
+ aarch64_reg 128 "V5";
+ aarch64_reg 128 "V6";
+ aarch64_reg 128 "V7";
+ aarch64_reg 128 "V8";
+ aarch64_reg 128 "V9";
+ aarch64_reg 128 "V10";
+ aarch64_reg 128 "V11";
+ aarch64_reg 128 "V12";
+ aarch64_reg 128 "V13";
+ aarch64_reg 128 "V14";
+ aarch64_reg 128 "V15";
+ aarch64_reg 128 "V16";
+ aarch64_reg 128 "V17";
+ aarch64_reg 128 "V18";
+ aarch64_reg 128 "V19";
+ aarch64_reg 128 "V20";
+ aarch64_reg 128 "V21";
+ aarch64_reg 128 "V22";
+ aarch64_reg 128 "V23";
+ aarch64_reg 128 "V24";
+ aarch64_reg 128 "V25";
+ aarch64_reg 128 "V26";
+ aarch64_reg 128 "V27";
+ aarch64_reg 128 "V28";
+ aarch64_reg 128 "V29";
+ aarch64_reg 128 "V30";
+ aarch64_reg 128 "V31";
+]
+
+let aarch64_special_purpose_registers_data = [
+ aarch64_reg 32 "CurrentEL";
+ aarch64_reg 32 "DAIF";
+ aarch64_reg 32 "NZCV";
+ aarch64_reg 64 "SP_EL0";
+ aarch64_reg 64 "SP_EL1";
+ aarch64_reg 64 "SP_EL2";
+ aarch64_reg 64 "SP_EL3";
+ aarch64_reg 32 "SPSel";
+ aarch64_reg 32 "SPSR_EL1";
+ aarch64_reg 32 "SPSR_EL2";
+ aarch64_reg 32 "SPSR_EL3";
+ aarch64_reg 64 "ELR_EL1";
+ aarch64_reg 64 "ELR_EL2";
+ aarch64_reg 64 "ELR_EL3";
+]
+
+let aarch64_general_system_control_registers_data = [
+ aarch64_reg 64 "HCR_EL2";
+ aarch64_reg 64 "ID_AA64MMFR0_EL1";
+ aarch64_reg 64 "RVBAR_EL1";
+ aarch64_reg 64 "RVBAR_EL2";
+ aarch64_reg 64 "RVBAR_EL3";
+ aarch64_reg 32 "SCR_EL3";
+ aarch64_reg 32 "SCTLR_EL1";
+ aarch64_reg 32 "SCTLR_EL2";
+ aarch64_reg 32 "SCTLR_EL3";
+ aarch64_reg 64 "TCR_EL1";
+ aarch64_reg 32 "TCR_EL2";
+ aarch64_reg 32 "TCR_EL3";
+]
+
+let aarch64_debug_registers_data = [
+ aarch64_reg 32 "DBGPRCR_EL1";
+ aarch64_reg 32 "OSDLR_EL1";
+]
+
+let aarch64_performance_monitors_registers_data = []
+let aarch64_generic_timer_registers_data = []
+let aarch64_generic_interrupt_controller_CPU_interface_registers_data = []
+
+let aarch64_external_debug_registers_data = [
+ aarch64_reg 32 "EDSCR";
+]
+
+let aarch32_general_system_control_registers_data = [
+ aarch64_reg 32 "SCR";
+]
+
+let aarch32_debug_registers_data = [
+ aarch64_reg 32 "DBGOSDLR";
+ aarch64_reg 32 "DBGPRCR";
+]
+
+let aarch64_register_data_all =
+ aarch64_PC_data @
+ aarch64_PSTATE_data @
+ aarch64_general_purpose_registers_data @
+ aarch64_SIMD_registers_data @
+ aarch64_special_purpose_registers_data @
+ aarch64_general_system_control_registers_data @
+ aarch64_debug_registers_data @
+ aarch64_performance_monitors_registers_data @
+ aarch64_generic_timer_registers_data @
+ aarch64_generic_interrupt_controller_CPU_interface_registers_data @
+ aarch64_external_debug_registers_data @
+ aarch32_general_system_control_registers_data @
+ aarch32_debug_registers_data
+
+let initial_stack_and_reg_data_of_AAarch64_elf_file e_entry all_data_memory =
+ let (reg_SP_EL0_direction, reg_SP_EL0_width, reg_SP_EL0_initial_index) =
+ List.assoc "SP_EL0" aarch64_register_data_all in
+
+ (* we compiled a small program that prints out SP and run it a few
+ times on the Nexus9, these are the results:
+ 0x0000007fe7f903e0
+ 0x0000007fdcdbf3f0
+ 0x0000007fcbe1ba90
+ 0x0000007fcf378280
+ 0x0000007fdd54b8d0
+ 0x0000007fd961bc10
+ 0x0000007ff3be6350
+ 0x0000007fd6bf6ef0
+ 0x0000007fff7676f0
+ 0x0000007ff2c34560 *)
+ let initial_SP_EL0 = Nat_big_num.of_string "549739036672" (*"0x0000007fff000000"*) in
+ let initial_SP_EL0_value =
+ Sail_impl_base.register_value_of_integer
+ reg_SP_EL0_width
+ reg_SP_EL0_initial_index
+ reg_SP_EL0_direction
+ initial_SP_EL0
+ in
+
+ (* ELF says we need an initial zero doubleword there *)
+ (* the code actually uses the stack, both above and below, so we map a bit more memory*)
+ let initial_stack_data =
+ (* this is a fairly big but arbitrary chunk: *)
+ (* let initial_stack_data_address = Nat_big_num.sub initial_GPR1_stack_pointer (Nat_big_num.of_int 128) in
+ [("initial_stack_data", initial_stack_data_address, Lem_list.replicate (128+32) 0 ))] in *)
+
+ [ ("initial_stack_data1", Nat_big_num.sub initial_SP_EL0 (Nat_big_num.of_int 16), Lem_list.replicate 8 0);
+ ("initial_stack_data2", Nat_big_num.sub initial_SP_EL0 (Nat_big_num.of_int 8), Lem_list.replicate 8 0)
+ ]
+ in
+
+ let initial_register_abi_data : (string * Sail_impl_base.register_value) list =
+ [("SP_EL0", initial_SP_EL0_value)]
+ in
+
+ (initial_stack_data, initial_register_abi_data)
+*)
+
+let mips_register_data_all = [
+ (*Pseudo registers*)
+ ("PC", (D_decreasing, 64, 63));
+ ("branchPending", (D_decreasing, 1, 0));
+ ("inBranchDelay", (D_decreasing, 1, 0));
+ ("delayedPC", (D_decreasing, 64, 63));
+ ("nextPC", (D_decreasing, 64, 63));
+ (* General purpose registers *)
+ ("GPR00", (D_decreasing, 64, 63));
+ ("GPR01", (D_decreasing, 64, 63));
+ ("GPR02", (D_decreasing, 64, 63));
+ ("GPR03", (D_decreasing, 64, 63));
+ ("GPR04", (D_decreasing, 64, 63));
+ ("GPR05", (D_decreasing, 64, 63));
+ ("GPR06", (D_decreasing, 64, 63));
+ ("GPR07", (D_decreasing, 64, 63));
+ ("GPR08", (D_decreasing, 64, 63));
+ ("GPR09", (D_decreasing, 64, 63));
+ ("GPR10", (D_decreasing, 64, 63));
+ ("GPR11", (D_decreasing, 64, 63));
+ ("GPR12", (D_decreasing, 64, 63));
+ ("GPR13", (D_decreasing, 64, 63));
+ ("GPR14", (D_decreasing, 64, 63));
+ ("GPR15", (D_decreasing, 64, 63));
+ ("GPR16", (D_decreasing, 64, 63));
+ ("GPR17", (D_decreasing, 64, 63));
+ ("GPR18", (D_decreasing, 64, 63));
+ ("GPR19", (D_decreasing, 64, 63));
+ ("GPR20", (D_decreasing, 64, 63));
+ ("GPR21", (D_decreasing, 64, 63));
+ ("GPR22", (D_decreasing, 64, 63));
+ ("GPR23", (D_decreasing, 64, 63));
+ ("GPR24", (D_decreasing, 64, 63));
+ ("GPR25", (D_decreasing, 64, 63));
+ ("GPR26", (D_decreasing, 64, 63));
+ ("GPR27", (D_decreasing, 64, 63));
+ ("GPR28", (D_decreasing, 64, 63));
+ ("GPR29", (D_decreasing, 64, 63));
+ ("GPR30", (D_decreasing, 64, 63));
+ ("GPR31", (D_decreasing, 64, 63));
+ (* special registers for mul/div *)
+ ("HI", (D_decreasing, 64, 63));
+ ("LO", (D_decreasing, 64, 63));
+ (* control registers *)
+ ("CP0Status", (D_decreasing, 32, 31));
+ ("CP0Cause", (D_decreasing, 32, 31));
+ ("CP0EPC", (D_decreasing, 64, 63));
+ ("CP0LLAddr", (D_decreasing, 64, 63));
+ ("CP0LLBit", (D_decreasing, 1, 0));
+ ("CP0Count", (D_decreasing, 32, 31));
+ ("CP0Compare", (D_decreasing, 32, 31));
+ ("CP0HWREna", (D_decreasing, 32, 31));
+ ("CP0UserLocal", (D_decreasing, 64, 63));
+ ("CP0BadVAddr", (D_decreasing, 64, 63));
+ ("TLBProbe" ,(D_decreasing, 1, 0));
+ ("TLBIndex" ,(D_decreasing, 6, 5));
+ ("TLBRandom" ,(D_decreasing, 6, 5));
+ ("TLBEntryLo0",(D_decreasing, 64, 63));
+ ("TLBEntryLo1",(D_decreasing, 64, 63));
+ ("TLBContext" ,(D_decreasing, 64, 63));
+ ("TLBPageMask",(D_decreasing, 16, 15));
+ ("TLBWired" ,(D_decreasing, 6, 5));
+ ("TLBEntryHi" ,(D_decreasing, 64, 63));
+ ("TLBXContext",(D_decreasing, 64, 63));
+
+ ("TLBEntry00" ,(D_decreasing, 117, 116));
+ ("TLBEntry01" ,(D_decreasing, 117, 116));
+ ("TLBEntry02" ,(D_decreasing, 117, 116));
+ ("TLBEntry03" ,(D_decreasing, 117, 116));
+ ("TLBEntry04" ,(D_decreasing, 117, 116));
+ ("TLBEntry05" ,(D_decreasing, 117, 116));
+ ("TLBEntry06" ,(D_decreasing, 117, 116));
+ ("TLBEntry07" ,(D_decreasing, 117, 116));
+ ("TLBEntry08" ,(D_decreasing, 117, 116));
+ ("TLBEntry09" ,(D_decreasing, 117, 116));
+ ("TLBEntry10" ,(D_decreasing, 117, 116));
+ ("TLBEntry11" ,(D_decreasing, 117, 116));
+ ("TLBEntry12" ,(D_decreasing, 117, 116));
+ ("TLBEntry13" ,(D_decreasing, 117, 116));
+ ("TLBEntry14" ,(D_decreasing, 117, 116));
+ ("TLBEntry15" ,(D_decreasing, 117, 116));
+ ("TLBEntry16" ,(D_decreasing, 117, 116));
+ ("TLBEntry17" ,(D_decreasing, 117, 116));
+ ("TLBEntry18" ,(D_decreasing, 117, 116));
+ ("TLBEntry19" ,(D_decreasing, 117, 116));
+ ("TLBEntry20" ,(D_decreasing, 117, 116));
+ ("TLBEntry21" ,(D_decreasing, 117, 116));
+ ("TLBEntry22" ,(D_decreasing, 117, 116));
+ ("TLBEntry23" ,(D_decreasing, 117, 116));
+ ("TLBEntry24" ,(D_decreasing, 117, 116));
+ ("TLBEntry25" ,(D_decreasing, 117, 116));
+ ("TLBEntry26" ,(D_decreasing, 117, 116));
+ ("TLBEntry27" ,(D_decreasing, 117, 116));
+ ("TLBEntry28" ,(D_decreasing, 117, 116));
+ ("TLBEntry29" ,(D_decreasing, 117, 116));
+ ("TLBEntry30" ,(D_decreasing, 117, 116));
+ ("TLBEntry31" ,(D_decreasing, 117, 116));
+ ("TLBEntry32" ,(D_decreasing, 117, 116));
+ ("TLBEntry33" ,(D_decreasing, 117, 116));
+ ("TLBEntry34" ,(D_decreasing, 117, 116));
+ ("TLBEntry35" ,(D_decreasing, 117, 116));
+ ("TLBEntry36" ,(D_decreasing, 117, 116));
+ ("TLBEntry37" ,(D_decreasing, 117, 116));
+ ("TLBEntry38" ,(D_decreasing, 117, 116));
+ ("TLBEntry39" ,(D_decreasing, 117, 116));
+ ("TLBEntry40" ,(D_decreasing, 117, 116));
+ ("TLBEntry41" ,(D_decreasing, 117, 116));
+ ("TLBEntry42" ,(D_decreasing, 117, 116));
+ ("TLBEntry43" ,(D_decreasing, 117, 116));
+ ("TLBEntry44" ,(D_decreasing, 117, 116));
+ ("TLBEntry45" ,(D_decreasing, 117, 116));
+ ("TLBEntry46" ,(D_decreasing, 117, 116));
+ ("TLBEntry47" ,(D_decreasing, 117, 116));
+ ("TLBEntry48" ,(D_decreasing, 117, 116));
+ ("TLBEntry49" ,(D_decreasing, 117, 116));
+ ("TLBEntry50" ,(D_decreasing, 117, 116));
+ ("TLBEntry51" ,(D_decreasing, 117, 116));
+ ("TLBEntry52" ,(D_decreasing, 117, 116));
+ ("TLBEntry53" ,(D_decreasing, 117, 116));
+ ("TLBEntry54" ,(D_decreasing, 117, 116));
+ ("TLBEntry55" ,(D_decreasing, 117, 116));
+ ("TLBEntry56" ,(D_decreasing, 117, 116));
+ ("TLBEntry57" ,(D_decreasing, 117, 116));
+ ("TLBEntry58" ,(D_decreasing, 117, 116));
+ ("TLBEntry59" ,(D_decreasing, 117, 116));
+ ("TLBEntry60" ,(D_decreasing, 117, 116));
+ ("TLBEntry61" ,(D_decreasing, 117, 116));
+ ("TLBEntry62" ,(D_decreasing, 117, 116));
+ ("TLBEntry63" ,(D_decreasing, 117, 116));
+
+ ("UART_WDATA" ,(D_decreasing, 8, 7));
+ ("UART_RDATA" ,(D_decreasing, 8, 7));
+ ("UART_WRITTEN" ,(D_decreasing, 1, 0));
+ ("UART_RVALID" ,(D_decreasing, 1, 0));
+]
+
+let cheri_register_data_all = mips_register_data_all @ [
+ ("CapCause", (D_decreasing, 16, 15));
+ ("PCC", (D_decreasing, 129, 128));
+ ("nextPCC", (D_decreasing, 129, 128));
+ ("delayedPCC", (D_decreasing, 129, 128));
+ ("C00", (D_decreasing, 129, 128));
+ ("C01", (D_decreasing, 129, 128));
+ ("C02", (D_decreasing, 129, 128));
+ ("C03", (D_decreasing, 129, 128));
+ ("C04", (D_decreasing, 129, 128));
+ ("C05", (D_decreasing, 129, 128));
+ ("C06", (D_decreasing, 129, 128));
+ ("C07", (D_decreasing, 129, 128));
+ ("C08", (D_decreasing, 129, 128));
+ ("C09", (D_decreasing, 129, 128));
+ ("C10", (D_decreasing, 129, 128));
+ ("C11", (D_decreasing, 129, 128));
+ ("C12", (D_decreasing, 129, 128));
+ ("C13", (D_decreasing, 129, 128));
+ ("C14", (D_decreasing, 129, 128));
+ ("C15", (D_decreasing, 129, 128));
+ ("C16", (D_decreasing, 129, 128));
+ ("C17", (D_decreasing, 129, 128));
+ ("C18", (D_decreasing, 129, 128));
+ ("C19", (D_decreasing, 129, 128));
+ ("C20", (D_decreasing, 129, 128));
+ ("C21", (D_decreasing, 129, 128));
+ ("C22", (D_decreasing, 129, 128));
+ ("C23", (D_decreasing, 129, 128));
+ ("C24", (D_decreasing, 129, 128));
+ ("C25", (D_decreasing, 129, 128));
+ ("C26", (D_decreasing, 129, 128));
+ ("C27", (D_decreasing, 129, 128));
+ ("C28", (D_decreasing, 129, 128));
+ ("C29", (D_decreasing, 129, 128));
+ ("C30", (D_decreasing, 129, 128));
+ ("C31", (D_decreasing, 129, 128));
+]
+
+let initial_stack_and_reg_data_of_MIPS_elf_file e_entry all_data_memory =
+ let initial_stack_data = [] in
+ let initial_cap_val_int = Nat_big_num.of_string "0x1fffe5a00000800000000000000000000" in (* hex((0x80000 << 64) + (45 << 105) + (0x7fff << 113) + (1 << 128)) *)
+ let initial_cap_val_reg = Sail_impl_base.register_value_of_integer 129 128 D_decreasing initial_cap_val_int in
+ let initial_register_abi_data : (string * Sail_impl_base.register_value) list = [
+ ("CP0Status", Sail_impl_base.register_value_of_integer 32 31 D_decreasing (Nat_big_num.of_string "0x00400000"));
+ ("PCC", initial_cap_val_reg);
+ ("nextPCC", initial_cap_val_reg);
+ ("delayedPCC", initial_cap_val_reg);
+ ("C00", initial_cap_val_reg);
+ ("C01", initial_cap_val_reg);
+ ("C02", initial_cap_val_reg);
+ ("C03", initial_cap_val_reg);
+ ("C04", initial_cap_val_reg);
+ ("C05", initial_cap_val_reg);
+ ("C06", initial_cap_val_reg);
+ ("C07", initial_cap_val_reg);
+ ("C08", initial_cap_val_reg);
+ ("C09", initial_cap_val_reg);
+ ("C10", initial_cap_val_reg);
+ ("C11", initial_cap_val_reg);
+ ("C12", initial_cap_val_reg);
+ ("C13", initial_cap_val_reg);
+ ("C14", initial_cap_val_reg);
+ ("C15", initial_cap_val_reg);
+ ("C16", initial_cap_val_reg);
+ ("C17", initial_cap_val_reg);
+ ("C18", initial_cap_val_reg);
+ ("C19", initial_cap_val_reg);
+ ("C20", initial_cap_val_reg);
+ ("C21", initial_cap_val_reg);
+ ("C22", initial_cap_val_reg);
+ ("C23", initial_cap_val_reg);
+ ("C24", initial_cap_val_reg);
+ ("C25", initial_cap_val_reg);
+ ("C26", initial_cap_val_reg);
+ ("C27", initial_cap_val_reg);
+ ("C28", initial_cap_val_reg);
+ ("C29", initial_cap_val_reg);
+ ("C30", initial_cap_val_reg);
+ ("C31", initial_cap_val_reg);
+ ] in
+ (initial_stack_data, initial_register_abi_data)
+
+let initial_reg_file reg_data init =
+ List.iter (fun (reg_name, _) -> reg := Reg.add reg_name (init reg_name) !reg) reg_data
+
+let initial_system_state_of_elf_file name =
+
+ (* call ELF analyser on file *)
+ match Sail_interface.populate_and_obtain_global_symbol_init_info name with
+ | Error.Fail s -> failwith ("populate_and_obtain_global_symbol_init_info: " ^ s)
+ | Error.Success
+ (_, (elf_epi: Sail_interface.executable_process_image),
+ (symbol_map: Elf_file.global_symbol_init_info))
+ ->
+ let (segments, e_entry, e_machine) =
+ begin match elf_epi with
+ | ELF_Class_32 _ -> failwith "cannot handle ELF_Class_32"
+ | ELF_Class_64 (segments,e_entry,e_machine) ->
+ (* remove all the auto generated segments (they contain only 0s) *)
+ let segments =
+ Lem_list.mapMaybe
+ (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None)
+ segments
+ in
+ (segments,e_entry,e_machine)
+ end
+ in
+
+ (* construct program memory and start address *)
+ begin
+ prog_mem := Mem.empty;
+ data_mem := Mem.empty;
+ tag_mem := Mem.empty;
+ load_memory_segments segments;
+ (*
+ debugf "prog_mem\n";
+ Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) !prog_mem;
+ debugf "data_mem\n";
+ Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) !data_mem;
+ *)
+ let (isa_defs, isa_memory_access, isa_externs, isa_model, model_reg_d, startaddr,
+ initial_stack_data, initial_register_abi_data, register_data_all) =
+ match Nat_big_num.to_int e_machine with
+(* | 21 (* EM_PPC64 *) ->
+ let startaddr =
+ let e_entry = Uint64.of_int64 (Nat_big_num.to_int64 e_entry) in
+ match Abi_power64.abi_power64_compute_program_entry_point segments e_entry with
+ | Error.Fail s -> failwith "Failed computing entry point"
+ | Error.Success s -> Nat_big_num.of_int64 (Uint64.to_int64 s)
+ in
+ let (initial_stack_data, initial_register_abi_data) =
+ initial_stack_and_reg_data_of_PPC_elf_file e_entry !data_mem in
+
+ (Power.defs,
+ (Power_extras.read_memory_functions,Power_extras.memory_writes,[],[],Power_extras.barrier_functions),
+ Power_extras.power_externs,
+ PPC,
+ D_increasing,
+ startaddr,
+ initial_stack_data,
+ initial_register_abi_data,
+ ppc_register_data_all)
+
+ | 183 (* EM_AARCH64 *) ->
+ let startaddr =
+ let e_entry = Uint64.of_int64 (Nat_big_num.to_int64 e_entry) in
+ match Abi_aarch64_le.abi_aarch64_le_compute_program_entry_point segments e_entry with
+ | Error.Fail s -> failwith "Failed computing entry point"
+ | Error.Success s -> Nat_big_num.of_int64 (Uint64.to_int64 s)
+ in
+
+ let (initial_stack_data, initial_register_abi_data) =
+ initial_stack_and_reg_data_of_AAarch64_elf_file e_entry !data_mem in
+
+ (ArmV8.defs,
+ (ArmV8_extras.aArch64_read_memory_functions,
+ ArmV8_extras.aArch64_memory_writes,
+ ArmV8_extras.aArch64_memory_eas,
+ ArmV8_extras.aArch64_memory_vals,
+ ArmV8_extras.aArch64_barrier_functions),
+ [],
+ AArch64,
+ D_decreasing,
+ startaddr,
+ initial_stack_data,
+ initial_register_abi_data,
+ aarch64_register_data_all) *)
+ | 8 (* EM_MIPS *) ->
+ let startaddr =
+ let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+ match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
+ | Error.Fail s -> failwith "Failed computing entry point"
+ | Error.Success s -> s
+ in
+ let (initial_stack_data, initial_register_abi_data) =
+ initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
+
+ (Cheri128.defs,
+ (Mips_extras.read_memory_functions,
+ Mips_extras.memory_writes,
+ Mips_extras.memory_eas,
+ Mips_extras.memory_vals,
+ Mips_extras.barrier_functions),
+ [],
+ MIPS,
+ D_decreasing,
+ startaddr,
+ initial_stack_data,
+ initial_register_abi_data,
+ cheri_register_data_all)
+
+ | _ -> failwith (Printf.sprintf "Sail sequential interpreter can't handle the e_machine value %s, only EM_PPC64, EM_AARCH64 and EM_MIPS are supported." (Nat_big_num.to_string e_machine))
+ in
+
+ (* pull the object symbols from the symbol table *)
+ let symbol_table : (string * Nat_big_num.num * int * word8 list (*their bytes*)) list =
+ let rec convert_symbol_table symbol_map =
+ begin match symbol_map with
+ | [] -> []
+ | ((name: string),
+ ((typ: Nat_big_num.num),
+ (size: Nat_big_num.num (*number of bytes*)),
+ (address: Nat_big_num.num),
+ (mb: Byte_sequence.byte_sequence option (*present iff type=stt_object*)),
+ (binding: Nat_big_num.num)))
+ (* (mb: Byte_sequence_wrapper.t option (*present iff type=stt_object*)) )) *)
+ ::symbol_map' ->
+ if Nat_big_num.equal typ Elf_symbol_table.stt_object && not (Nat_big_num.equal size (Nat_big_num.of_int 0))
+ then
+ (
+ (* an object symbol - map *)
+ (*Printf.printf "*** size %d ***\n" (Nat_big_num.to_int size);*)
+ let bytes =
+ (match mb with
+ | None -> raise (Failure "this cannot happen")
+ | Some (Sequence bytes) ->
+ List.map (fun (c:char) -> Char.code c) bytes) in
+ (name, address, List.length bytes, bytes):: convert_symbol_table symbol_map'
+ )
+ else
+ (* not an object symbol or of zero size - ignore *)
+ convert_symbol_table symbol_map'
+ end
+ in
+ (List.map (fun (n,a,bs) -> (n,a,List.length bs,bs)) initial_stack_data) @ convert_symbol_table symbol_map
+ in
+
+ (* invert the symbol table to use for pp *)
+ let symbol_table_pp : ((Sail_impl_base.address * int) * string) list =
+ (* map symbol to (bindings, footprint),
+ if a symbol appears more then onece keep the one with higher
+ precedence (stb_global > stb_weak > stb_local) *)
+ let map =
+ List.fold_left
+ (fun map (name, (typ, size, address, mb, binding)) ->
+ if String.length name <> 0 &&
+ (if String.length name = 1 then Char.code (String.get name 0) <> 0 else true) &&
+ not (Nat_big_num.equal address (Nat_big_num.of_int 0))
+ then
+ try
+ let (binding', _) = StringMap.find name map in
+ if Nat_big_num.equal binding' Elf_symbol_table.stb_local ||
+ Nat_big_num.equal binding Elf_symbol_table.stb_global
+ then
+ StringMap.add name (binding,
+ (Sail_impl_base.address_of_integer address, Nat_big_num.to_int size)) map
+ else map
+ with Not_found ->
+ StringMap.add name (binding,
+ (Sail_impl_base.address_of_integer address, Nat_big_num.to_int size)) map
+
+ else map
+ )
+ StringMap.empty
+ symbol_map
+ in
+
+ List.map (fun (name, (binding, fp)) -> (fp, name)) (StringMap.bindings map)
+ in
+
+
+ (* Now we examine the rest of the data memory,
+ removing the footprint of the symbols and chunking it into aligned chunks *)
+
+ let rec remove_symbols_from_data_memory data_mem symbols =
+ match symbols with
+ | [] -> data_mem
+ | (name,address,size,bs)::symbols' ->
+ let data_mem' =
+ Mem.filter
+ (fun a v ->
+ not (Nat_big_num.greater_equal a address &&
+ Nat_big_num.less a (Nat_big_num.add (Nat_big_num.of_int (List.length bs)) address)))
+ data_mem in
+ remove_symbols_from_data_memory data_mem' symbols' in
+
+ let trimmed_data_memory : (Nat_big_num.num * memory_byte) list =
+ Mem.bindings (remove_symbols_from_data_memory !data_mem symbol_table) in
+
+ (* make sure that's ordered increasingly.... *)
+ let trimmed_data_memory =
+ List.sort (fun (a,b) (a',b') -> Nat_big_num.compare a a') trimmed_data_memory in
+
+ let aligned a n = (* a mod n = 0 *)
+ let n_big = Nat_big_num.of_int n in
+ Nat_big_num.equal (Nat_big_num.modulus a n_big) ((Nat_big_num.of_int 0)) in
+
+ let isplus a' a n = (* a' = a+n *)
+ Nat_big_num.equal a' (Nat_big_num.add (Nat_big_num.of_int n) a) in
+
+ let rec chunk_data_memory dm =
+ match dm with
+ | (a0,b0)::(a1,b1)::(a2,b2)::(a3,b3)::(a4,b4)::(a5,b5)::(a6,b6)::(a7,b7)::dm' when
+ (aligned a0 8 && isplus a1 a0 1 && isplus a2 a0 2 && isplus a3 a0 3 &&
+ isplus a4 a0 4 && isplus a5 a0 5 && isplus a6 a0 6 && isplus a7 a0 7) ->
+ (a0,8,[b0;b1;b2;b3;b4;b5;b6;b7]) :: chunk_data_memory dm'
+ | (a0,b0)::(a1,b1)::(a2,b2)::(a3,b3)::dm' when
+ (aligned a0 4 && isplus a1 a0 1 && isplus a2 a0 2 && isplus a3 a0 3) ->
+ (a0,4,[b0;b1;b2;b3]) :: chunk_data_memory dm'
+ | (a0,b0)::(a1,b1)::dm' when
+ (aligned a0 2 && isplus a1 a0 1) ->
+ (a0,2,[b0;b1]) :: chunk_data_memory dm'
+ | (a0,b0)::dm' ->
+ (a0,1,[b0]):: chunk_data_memory dm'
+ | [] -> [] in
+
+ let initial_register_state =
+ fun rbn ->
+ try
+ List.assoc rbn initial_register_abi_data
+ with
+ Not_found ->
+ (register_state_zero register_data_all) rbn
+ in
+
+ begin
+ (initial_reg_file register_data_all initial_register_state);
+
+ (* construct initial system state *)
+ let initial_system_state =
+ (isa_defs,
+ isa_memory_access,
+ isa_externs,
+ isa_model,
+ model_reg_d,
+ startaddr,
+ (Sail_impl_base.address_of_integer startaddr))
+ in
+
+ (initial_system_state, symbol_table_pp)
+ end
+ end
+
+let eager_eval = ref true
+let break_point = ref false
+let break_instr = ref 0
+let max_cut_off = ref false
+let max_instr = ref 0
+let raw_file = ref ""
+let raw_at = ref 0
+
+let args = [
+ ("--file", Arg.Set_string file, "filename of elf binary to load in memory");
+ ("--quiet", Arg.Clear Run_interp_model.interact_print, "do not display per-instruction actions");
+ ("--silent", Arg.Tuple [Arg.Clear Run_interp_model.error_print;
+ Arg.Clear Run_interp_model.interact_print;
+ Arg.Clear Run_interp_model.result_print],
+ "do not dispaly error messages, per-instruction actions, or results");
+ ("--no_result", Arg.Clear Run_interp_model.result_print, "do not display final register values");
+ ("--interactive", Arg.Clear eager_eval , "interactive execution");
+ ("--breakpoint", Arg.Int (fun i -> break_point := true; break_instr:= i), "run to instruction number i, then run interactively");
+ ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop");
+ ("--raw", Arg.Set_string raw_file, "filename of raw file to load in memory");
+ ("--at", Arg.Set_int raw_at, "address to load raw file in memory");
+]
+
+let time_it action arg =
+ let start_time = Sys.time () in
+ ignore (action arg);
+ let finish_time = Sys.time () in
+ finish_time -. start_time
+
+(*TODO MIPS specific, should print final register values under all models*)
+let rec debug_print_gprs start stop =
+ resultf "DEBUG MIPS REG %.2d %s\n" start (Printing_functions.logfile_register_value_to_string (Reg.find (Format.sprintf "GPR%02d" start) !reg));
+ if start < stop
+ then debug_print_gprs (start + 1) stop
+ else ()
+
+let rec debug_print_capregs start stop =
+ resultf "DEBUG CAP REG %.2d %s\n" start (Printing_functions.logfile_register_value_to_string (Reg.find (Format.sprintf "C%02d" start) !reg));
+ if start < stop
+ then debug_print_capregs (start + 1) stop
+ else ()
+
+let stop_condition_met model instr =
+ match model with
+ | PPC ->
+ (match instr with
+ | ("Sc", [("Lev", _, arg)]) ->
+ Nat_big_num.equal (integer_of_bit_list arg) (Nat_big_num.of_int 32)
+ | _ -> false)
+ | AArch64 -> (match instr with
+ | ("ImplementationDefinedStopFetching", _) -> true
+ | _ -> false)
+ | MIPS -> (match instr with
+ | ("HCF", _) ->
+ resultf "DEBUG MIPS PC %s\n" (Printing_functions.logfile_register_value_to_string (Reg.find "PC" !reg));
+ debug_print_gprs 0 31;
+ resultf "DEBUG CAP PCC %s\n" (Printing_functions.logfile_register_value_to_string (Reg.find "PCC" !reg));
+ debug_print_capregs 0 31;
+ true
+ | _ -> false)
+
+let is_branch model instruction =
+ let (name,_,_) = instruction in
+ match (model , name) with
+ | (PPC, "B") -> true
+ | (PPC, "Bc") -> true
+ | (PPC, "Bclr") -> true
+ | (PPC, "Bcctr") -> true
+ | (PPC, _) -> false
+ | (AArch64, "BranchImmediate") -> true
+ | (AArch64, "BranchConditional") -> true
+ | (AArch64, "CompareAndBranch") -> true
+ | (AArch64, "TestBitAndBranch") -> true
+ | (AArch64, "BranchRegister") -> true
+ | (AArch64, _) -> false
+ | (MIPS, _) -> false (*todo,fill this in*)
+
+let option_int_of_option_integer i = match i with
+ | Some i -> Some (Nat_big_num.to_int i)
+ | None -> None
+
+let set_next_instruction_address model =
+ match model with
+ | PPC ->
+ let cia = Reg.find "CIA" !reg in
+ let cia_addr = address_of_register_value cia in
+ (match cia_addr with
+ | Some cia_addr ->
+ let nia_addr = add_address_nat cia_addr 4 in
+ let nia = register_value_of_address nia_addr Sail_impl_base.D_increasing in
+ reg := Reg.add "NIA" nia !reg
+ | _ -> failwith "CIA address contains unknown or undefined")
+ | AArch64 ->
+ let pc = Reg.find "_PC" !reg in
+ let pc_addr = address_of_register_value pc in
+ (match pc_addr with
+ | Some pc_addr ->
+ let n_addr = add_address_nat pc_addr 4 in
+ let n_pc = register_value_of_address n_addr D_decreasing in
+ reg := Reg.add "_PC" n_pc !reg
+ | _ -> failwith "_PC address contains unknown or undefined")
+ | MIPS ->
+ let pc_addr = address_of_register_value (Reg.find "PC" !reg) in
+ let branchPending = integer_of_register_value (Reg.find "branchPending" !reg) in
+ (match (pc_addr, option_int_of_option_integer branchPending) with
+ | (Some pc_val, Some 0) ->
+ (* normal -- increment PC *)
+ let n_addr = add_address_nat pc_val 4 in
+ let n_pc = register_value_of_address n_addr D_decreasing in
+ begin
+ reg := Reg.add "nextPC" n_pc !reg;
+ reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
+ end
+ | (Some pc_val, Some 1) ->
+ (* delay slot -- branch to delayed PC and clear branchPending *)
+ begin
+ reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg;
+ reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg;
+ reg := Reg.add "branchPending" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
+ reg := Reg.add "inBranchDelay" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg;
+ end
+ | (_, _) -> errorf "PC address contains unknown or undefined"; exit 1)
+
+let add1 = Nat_big_num.add (Nat_big_num.of_int 1)
+
+let get_addr_trans_regs _ =
+ (*resultf "PCC %s\n" (Printing_functions.logfile_register_value_to_string (Reg.find "PCC" !reg));*)
+ Some([
+ (Sail_impl_base.Reg("PC", 63, 64, Sail_impl_base.D_decreasing), Reg.find "PC" !reg);
+ (Sail_impl_base.Reg("PCC", 128, 129, Sail_impl_base.D_decreasing), Reg.find "PCC" !reg);
+ (Sail_impl_base.Reg("C29", 128, 129, Sail_impl_base.D_decreasing), Reg.find "C29" !reg);
+ (Sail_impl_base.Reg("CP0Status", 31, 32, Sail_impl_base.D_decreasing), Reg.find "CP0Status" !reg);
+ (Sail_impl_base.Reg("CP0Cause", 31, 32, Sail_impl_base.D_decreasing), Reg.find "CP0Cause" !reg);
+ (Sail_impl_base.Reg("CP0Count", 31, 32, Sail_impl_base.D_decreasing), Reg.find "CP0Count" !reg);
+ (Sail_impl_base.Reg("CP0Compare", 31, 32, Sail_impl_base.D_decreasing), Reg.find "CP0Compare" !reg);
+ (Sail_impl_base.Reg("inBranchDelay", 0, 1, Sail_impl_base.D_decreasing), Reg.find "inBranchDelay" !reg);
+ (Sail_impl_base.Reg("TLBRandom", 5, 6, Sail_impl_base.D_decreasing), Reg.find "TLBRandom" !reg);
+ (Sail_impl_base.Reg("TLBWired", 5, 6, Sail_impl_base.D_decreasing), Reg.find "TLBWired" !reg);
+ (Sail_impl_base.Reg("TLBEntryHi", 63, 64, Sail_impl_base.D_decreasing), Reg.find "TLBEntryHi" !reg);
+ (Sail_impl_base.Reg("TLBEntry00", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry00" !reg);
+ (Sail_impl_base.Reg("TLBEntry01", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry01" !reg);
+ (Sail_impl_base.Reg("TLBEntry02", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry02" !reg);
+ (Sail_impl_base.Reg("TLBEntry03", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry03" !reg);
+ (Sail_impl_base.Reg("TLBEntry04", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry04" !reg);
+ (Sail_impl_base.Reg("TLBEntry05", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry05" !reg);
+ (Sail_impl_base.Reg("TLBEntry06", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry06" !reg);
+ (Sail_impl_base.Reg("TLBEntry07", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry07" !reg);
+ (Sail_impl_base.Reg("TLBEntry08", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry08" !reg);
+ (Sail_impl_base.Reg("TLBEntry09", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry09" !reg);
+ (Sail_impl_base.Reg("TLBEntry10", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry10" !reg);
+ (Sail_impl_base.Reg("TLBEntry11", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry11" !reg);
+ (Sail_impl_base.Reg("TLBEntry12", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry12" !reg);
+ (Sail_impl_base.Reg("TLBEntry13", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry13" !reg);
+ (Sail_impl_base.Reg("TLBEntry14", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry14" !reg);
+ (Sail_impl_base.Reg("TLBEntry15", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry15" !reg);
+ (Sail_impl_base.Reg("TLBEntry16", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry16" !reg);
+ (Sail_impl_base.Reg("TLBEntry17", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry17" !reg);
+ (Sail_impl_base.Reg("TLBEntry18", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry18" !reg);
+ (Sail_impl_base.Reg("TLBEntry19", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry19" !reg);
+ (Sail_impl_base.Reg("TLBEntry20", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry20" !reg);
+ (Sail_impl_base.Reg("TLBEntry21", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry21" !reg);
+ (Sail_impl_base.Reg("TLBEntry22", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry22" !reg);
+ (Sail_impl_base.Reg("TLBEntry23", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry23" !reg);
+ (Sail_impl_base.Reg("TLBEntry24", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry24" !reg);
+ (Sail_impl_base.Reg("TLBEntry25", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry25" !reg);
+ (Sail_impl_base.Reg("TLBEntry26", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry26" !reg);
+ (Sail_impl_base.Reg("TLBEntry27", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry27" !reg);
+ (Sail_impl_base.Reg("TLBEntry28", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry28" !reg);
+ (Sail_impl_base.Reg("TLBEntry29", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry29" !reg);
+ (Sail_impl_base.Reg("TLBEntry30", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry30" !reg);
+ (Sail_impl_base.Reg("TLBEntry31", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry31" !reg);
+ (Sail_impl_base.Reg("TLBEntry32", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry32" !reg);
+ (Sail_impl_base.Reg("TLBEntry33", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry33" !reg);
+ (Sail_impl_base.Reg("TLBEntry34", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry34" !reg);
+ (Sail_impl_base.Reg("TLBEntry35", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry35" !reg);
+ (Sail_impl_base.Reg("TLBEntry36", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry36" !reg);
+ (Sail_impl_base.Reg("TLBEntry37", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry37" !reg);
+ (Sail_impl_base.Reg("TLBEntry38", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry38" !reg);
+ (Sail_impl_base.Reg("TLBEntry39", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry39" !reg);
+ (Sail_impl_base.Reg("TLBEntry40", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry40" !reg);
+ (Sail_impl_base.Reg("TLBEntry41", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry41" !reg);
+ (Sail_impl_base.Reg("TLBEntry42", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry42" !reg);
+ (Sail_impl_base.Reg("TLBEntry43", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry43" !reg);
+ (Sail_impl_base.Reg("TLBEntry44", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry44" !reg);
+ (Sail_impl_base.Reg("TLBEntry45", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry45" !reg);
+ (Sail_impl_base.Reg("TLBEntry46", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry46" !reg);
+ (Sail_impl_base.Reg("TLBEntry47", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry47" !reg);
+ (Sail_impl_base.Reg("TLBEntry48", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry48" !reg);
+ (Sail_impl_base.Reg("TLBEntry49", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry49" !reg);
+ (Sail_impl_base.Reg("TLBEntry50", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry50" !reg);
+ (Sail_impl_base.Reg("TLBEntry51", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry51" !reg);
+ (Sail_impl_base.Reg("TLBEntry52", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry52" !reg);
+ (Sail_impl_base.Reg("TLBEntry53", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry53" !reg);
+ (Sail_impl_base.Reg("TLBEntry54", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry54" !reg);
+ (Sail_impl_base.Reg("TLBEntry55", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry55" !reg);
+ (Sail_impl_base.Reg("TLBEntry56", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry56" !reg);
+ (Sail_impl_base.Reg("TLBEntry57", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry57" !reg);
+ (Sail_impl_base.Reg("TLBEntry58", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry58" !reg);
+ (Sail_impl_base.Reg("TLBEntry59", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry59" !reg);
+ (Sail_impl_base.Reg("TLBEntry60", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry60" !reg);
+ (Sail_impl_base.Reg("TLBEntry61", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry61" !reg);
+ (Sail_impl_base.Reg("TLBEntry62", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry62" !reg);
+ (Sail_impl_base.Reg("TLBEntry63", 116, 117, Sail_impl_base.D_decreasing), Reg.find "TLBEntry63" !reg);
+ ])
+
+let get_opcode pc_a =
+ List.map (fun b -> match b with
+ | Some b -> b
+ | None -> failwith "A byte in opcode contained unknown or undef")
+ (List.map byte_of_memory_byte
+ ([Mem.find pc_a !prog_mem;
+ Mem.find (add1 pc_a) !prog_mem;
+ Mem.find (add1 (add1 pc_a)) !prog_mem;
+ Mem.find (add1 (add1 (add1 pc_a))) !prog_mem]))
+
+let rec write_events = function
+ | [] -> ()
+ | e::events ->
+ (match e with
+ | E_write_reg (Reg(id,_,_,_), value) -> reg := Reg.add id value !reg
+ | E_write_reg ((Reg_slice(id,_,_,range) as reg_n),value)
+ | E_write_reg ((Reg_field(id,_,_,_,range) as reg_n),value)->
+ let old_val = Reg.find id !reg in
+ let new_val = fupdate_slice reg_n old_val value range in
+ reg := Reg.add id new_val !reg
+ | E_write_reg((Reg_f_slice(id,_,_,_,range,mini_range) as reg_n),value) ->
+ let old_val = Reg.find id !reg in
+ let new_val = fupdate_slice reg_n old_val value (combine_slices range mini_range) in
+ reg := Reg.add id new_val !reg
+ | _ -> failwith "Only register write events expected");
+ write_events events
+
+let fetch_instruction_opcode_and_update_ia model addr_trans =
+ match model with
+ | PPC ->
+ let cia = Reg.find "CIA" !reg in
+ let cia_addr = address_of_register_value cia in
+ (match cia_addr with
+ | Some cia_addr ->
+ let cia_a = integer_of_address cia_addr in
+ let opcode = (get_opcode cia_a) in
+ begin
+ reg := Reg.add "CIA" (Reg.find "NIA" !reg) !reg;
+ Opcode opcode
+ end
+ | None -> failwith "CIA address contains unknown or undefined")
+ | AArch64 ->
+ let pc = Reg.find "_PC" !reg in
+ let pc_addr = address_of_register_value pc in
+ (match pc_addr with
+ | Some pc_addr ->
+ let pc_a = integer_of_address pc_addr in
+ let opcode = (get_opcode pc_a) in
+ Opcode opcode
+ | None -> failwith "_PC address contains unknown or undefined")
+ | MIPS ->
+ begin
+ reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg;
+ let nextPC = Reg.find "nextPC" !reg in
+ let pc_addr = address_of_register_value nextPC in
+ (*let unused = interactf "PC: %s\n" (Printing_functions.register_value_to_string nextPC) in*)
+ (match pc_addr with
+ | Some pc_addr ->
+ let pc_a = match addr_trans (get_addr_trans_regs ()) pc_addr with
+ | Some a, Some events -> write_events (List.rev events); integer_of_address a
+ | Some a, None -> integer_of_address a
+ | None, Some events ->
+ write_events (List.rev events);
+ let nextPC = Reg.find "nextPC" !reg in
+ reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg;
+ let pc_addr = address_of_register_value nextPC in
+ (match pc_addr with
+ | Some pc_addr ->
+ (match addr_trans (get_addr_trans_regs ()) pc_addr with
+ | Some a, Some events -> write_events (List.rev events); integer_of_address a
+ | Some a, None -> integer_of_address a
+ | None, _ -> failwith "Address translation failed twice")
+ | None -> failwith "no nextPc address")
+ | _ -> failwith "No address and no events from translate address"
+ in
+ let opcode = (get_opcode pc_a) in
+ begin
+ reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
+ Opcode opcode
+ end
+ | None -> errorf "nextPC contains unknown or undefined"; exit 1)
+ end
+ | _ -> assert false
+
+let get_pc_address = function
+ | MIPS -> Reg.find "PC" !reg
+ | PPC -> Reg.find "CIA" !reg
+ | AArch64 -> Reg.find "_PC" !reg
+
+
+let option_int_of_reg str =
+ option_int_of_option_integer (integer_of_register_value (Reg.find str !reg))
+
+let rec fde_loop count context model mode track_dependencies addr_trans =
+ if !max_cut_off && count = !max_instr
+ then resultf "\nEnding evaluation due to reaching cut off point of %d instructions\n" count
+ else begin
+ if !break_point && count = !break_instr then begin break_point := false; eager_eval := false end;
+ let pc_regval = get_pc_address model in
+ interactf "\n**** instruction %d from address %s ****\n"
+ count (Printing_functions.register_value_to_string pc_regval);
+ let pc_addr = address_of_register_value pc_regval in
+ let pc_val = match pc_addr with
+ | Some v -> v
+ | None -> failwith "pc contains undef or unknown" in
+ let m_paddr_int = match addr_trans (get_addr_trans_regs ()) pc_val with
+ | Some a, Some events -> write_events (List.rev events); Some (integer_of_address a)
+ | Some a, None -> Some (integer_of_address a)
+ | None, Some events -> write_events (List.rev events); None
+ | None, None -> failwith "address translation failed and no writes" in
+ match m_paddr_int with
+ | Some pc ->
+ let inBranchDelay = option_int_of_reg "inBranchDelay" in
+ (match inBranchDelay with
+ | Some 0 ->
+ let npc_addr = add_address_nat pc_val 4 in
+ let npc_reg = register_value_of_address npc_addr Sail_impl_base.D_decreasing in
+ reg := Reg.add "nextPC" npc_reg !reg;
+ | Some 1 ->
+ reg := Reg.add "nextPC" (Reg.find "delayedPC" !reg) !reg;
+ reg := Reg.add "nextPCC" (Reg.find "delayedPCC" !reg) !reg;
+ | _ -> failwith "invalid value of inBranchDelay");
+ let opcode = Opcode (get_opcode pc) in
+ let (instruction,istate) = match Interp_inter_imp.decode_to_istate context None opcode with
+ | Instr(instruction,istate) ->
+ interactf "\n**** Running: %s ****\n" (Printing_functions.instruction_to_string instruction);
+ (instruction,istate)
+ | Decode_error d ->
+ (match d with
+ | Interp_interface.Unsupported_instruction_error instr ->
+ errorf "\n**** Encountered unsupported instruction %s ****\n" (Printing_functions.instruction_to_string instr)
+ | Interp_interface.Not_an_instruction_error op ->
+ (match op with
+ | Opcode bytes ->
+ errorf "\n**** Encountered non-decodeable opcode: %s ****\n" (Printing_functions.byte_list_to_string bytes))
+ | Internal_error s -> errorf "\n**** Internal error on decode: %s ****\n" s); exit 1
+ in
+ if stop_condition_met model instruction
+ then resultf "\nSUCCESS program terminated after %d instructions\n" count
+ else
+ begin
+ match Run_interp_model.run istate !reg !prog_mem !tag_mem !eager_eval track_dependencies mode "execute" with
+ | false, _,_, _ -> errorf "FAILURE\n"; exit 1
+ | true, mode, track_dependencies, (my_reg, my_mem, my_tags) ->
+ reg := my_reg;
+ prog_mem := my_mem;
+ tag_mem := my_tags;
+
+ (try
+ let (pending, _, _) = (Unix.select [(Unix.stdin)] [] [] 0.0) in
+ (if (pending != []) then
+ let char = (input_byte stdin) in (
+ errorf "Input %x\n" char;
+ input_buf := (!input_buf) @ [char]));
+ with
+ | _ -> ());
+
+ let uart_rvalid = option_int_of_reg "UART_RVALID" in
+ (match uart_rvalid with
+ | Some 0 ->
+ (match !input_buf with
+ | x :: xs -> (
+ reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Sail_impl_base.D_decreasing (Nat_big_num.of_int x)) !reg;
+ reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg;
+ input_buf := xs;
+ )
+ | [] -> ())
+ | _-> ());
+
+ let uart_written = option_int_of_reg "UART_WRITTEN" in
+ (match uart_written with
+ | Some 1 ->
+ (let uart_data = option_int_of_reg "UART_WDATA" in
+ match uart_data with
+ | Some b -> (printf "%c" (Char.chr b); printf "%!")
+ | None -> (errorf "UART_WDATA was undef" ; exit 1))
+ | _ -> ());
+ reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
+
+ reg := Reg.add "inBranchDelay" (Reg.find "branchPending" !reg) !reg;
+ reg := Reg.add "branchPending" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
+ reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
+ reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg;
+ fde_loop (count + 1) context model (Some mode) (ref track_dependencies) addr_trans
+ end
+ | None -> begin
+ reg := Reg.add "inBranchDelay" (Reg.find "branchPending" !reg) !reg;
+ reg := Reg.add "branchPending" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;
+ reg := Reg.add "PC" (Reg.find "nextPC" !reg) !reg;
+ reg := Reg.add "PCC" (Reg.find "nextPCC" !reg) !reg;
+ fde_loop (count + 1) context model mode track_dependencies addr_trans
+ end
+ end
+
+let rec load_raw_file' mem addr chan =
+ let byte = input_byte chan in
+ (add_mem byte addr mem;
+ load_raw_file' mem (Nat_big_num.succ addr) chan)
+
+let rec load_raw_file mem addr chan =
+ try
+ load_raw_file' mem addr chan
+ with
+ | End_of_file -> ()
+
+let run () =
+ Arg.parse args (fun _ -> raise (Arg.Bad "anonymous parameter")) "" ;
+ if !file = "" then begin
+ Arg.usage args "";
+ exit 1;
+ end;
+ if !break_point then eager_eval := true;
+
+ let ((isa_defs,
+ (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4),
+ isa_externs,
+ isa_model,
+ model_reg_d,
+ startaddr,
+ startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
+
+ let context = build_context isa_defs isa_m0 isa_m1 isa_m2 isa_m3 isa_m4 isa_externs in
+ (*NOTE: this is likely MIPS specific, so should probably pull from initial_system_state info on to translate or not,
+ endian mode, and translate function name
+ *)
+ let addr_trans = translate_address context E_big_endian "TranslateAddress" in
+ if String.length(!raw_file) != 0 then
+ load_raw_file prog_mem (Nat_big_num.of_int !raw_at) (open_in_bin !raw_file);
+ reg := Reg.add "PC" (register_value_of_address startaddr_internal model_reg_d ) !reg;
+ (* entry point: unit -> unit fde *)
+ let name = Filename.basename !file in
+ let t = time_it (fun () -> fde_loop 0 context isa_model (Some Run) (ref false) addr_trans) () in
+ resultf "Execution time for file %s: %f seconds\n" name t;;
+
+(* Turn off line-buffering of standard input to allow responsive console input *)
+if Unix.isatty (Unix.stdin) then begin
+ let tattrs = Unix.tcgetattr (Unix.stdin) in
+ Unix.tcsetattr (Unix.stdin) (Unix.TCSANOW) ({tattrs with c_icanon=false})
+end ;;
+
+run () ;;
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index 76ac1797..3f38f521 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -398,6 +398,18 @@ type write_kind =
(* AArch64 writes *)
| Write_release | Write_exclusive | Write_exclusive_release
+instance (Show write_kind)
+ let show = function
+ | Write_plain -> "Write_plain"
+ | Write_tag -> "Write_tag"
+ | Write_tag_conditional -> "Write_tag_conditional"
+ | Write_conditional -> "Write_conditional"
+ | Write_release -> "Write_release"
+ | Write_exclusive -> "Write_exclusive"
+ | Write_exclusive_release -> "Write_exclusive_release"
+ end
+end
+
type barrier_kind =
(* Power barriers *)
Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
@@ -407,6 +419,23 @@ type barrier_kind =
(* MIPS barriers *)
| Barrier_MIPS_SYNC
+instance (Show barrier_kind)
+ let show = function
+ | Barrier_Sync -> "Barrier_Sync"
+ | Barrier_LwSync -> "Barrier_LwSync"
+ | Barrier_Eieio -> "Barrier_Eieio"
+ | Barrier_Isync -> "Barrier_Isync"
+ | Barrier_DMB -> "Barrier_DMB"
+ | Barrier_DMB_ST -> "Barrier_DMB_ST"
+ | Barrier_DMB_LD -> "Barrier_DMB_LD"
+ | Barrier_DSB -> "Barrier_DSB"
+ | Barrier_DSB_ST -> "Barrier_DSB_ST"
+ | Barrier_DSB_LD -> "Barrier_DSB_LD"
+ | Barrier_ISB -> "Barrier_ISB"
+ | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC"
+ end
+end
+
type instruction_kind =
| IK_barrier of barrier_kind
| IK_mem_read of read_kind
@@ -419,6 +448,18 @@ they just have particular nias (and will be IK_simple *)
| IK_simple
+instance (Show instruction_kind)
+ let show = function
+ | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind)
+ | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind)
+ | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind)
+ | IK_cond_branch -> "IK_cond_branch"
+ | IK_simple -> "IK_simple"
+ end
+end
+
+
+
let ~{ocaml} read_kindCompare rk1 rk2 =
match (rk1, rk2) with
| (Read_plain, Read_plain) -> EQ
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 19:31:19 +0000