diff --git a/.github/workflows/compile.yml b/.github/workflows/compile.yml index dee846b..398277a 100644 --- a/.github/workflows/compile.yml +++ b/.github/workflows/compile.yml @@ -13,7 +13,7 @@ jobs: - name: Init opam run: opam init -y - name: Install sail - run: opam install -y sail + run: opam pin sail 0.15 && opam install -y sail - name: Check out repository code uses: actions/checkout@HEAD with: diff --git a/sail-riscv b/sail-riscv index 6d0cc0f..e7f4b31 160000 --- a/sail-riscv +++ b/sail-riscv @@ -1 +1 @@ -Subproject commit 6d0cc0fac7ad743651e295594c274e9b89ca23f7 +Subproject commit e7f4b31f4fa558342f77378a1dd94aa39e29600d diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index b2b4dea..80b30e2 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -835,9 +835,6 @@ function clause execute StoreCapImm(cs2, cs1, imm) = { } else if not (auth_val.permit_load_store_cap) & cs2_val.tag then { handle_cheri_reg_exception(CapEx_PermitStoreCapViolation, cs1); RETIRE_FAIL - } else if not (auth_val.permit_store_local_cap) & cs2_val.tag & not(cs2_val.global) then { - handle_cheri_reg_exception(CapEx_PermitStoreLocalCapViolation, cs1); - RETIRE_FAIL } else if not(inCapBounds(auth_val, vaddrBits, cap_size)) then { handle_cheri_reg_exception(CapEx_BoundsViolation, cs1); RETIRE_FAIL @@ -851,7 +848,8 @@ function clause execute StoreCapImm(cs2, cs1, imm) = { match (eares) { MemException(e) => { handle_mem_exception(vaddrBits, e); RETIRE_FAIL }, MemValue(_) => { - let res : MemoryOpResult(bool) = mem_write_cap(addr, cs2_val, false, false, false); + let stored_val = clearTagIf(cs2_val, not (auth_val.permit_store_local_cap) & not(cs2_val.global)); + let res : MemoryOpResult(bool) = mem_write_cap(addr, stored_val, false, false, false); match (res) { MemValue(true) => RETIRE_SUCCESS, MemValue(false) => internal_error("store got false from mem_write_value"), diff --git a/src/cheri_types.sail b/src/cheri_types.sail index b115c3e..ef7aca9 100644 --- a/src/cheri_types.sail +++ b/src/cheri_types.sail @@ -96,7 +96,6 @@ enum CapEx = { CapEx_PermitStoreViolation, CapEx_PermitLoadCapViolation, CapEx_PermitStoreCapViolation, - CapEx_PermitStoreLocalCapViolation, CapEx_AccessSystemRegsViolation, CapEx_PermitCInvokeViolation, CapEx_PermitSetCIDViolation @@ -117,7 +116,6 @@ function CapExCode(ex) : CapEx -> bits(5) = CapEx_PermitStoreViolation => 0b10011, CapEx_PermitLoadCapViolation => 0b10100, CapEx_PermitStoreCapViolation => 0b10101, - CapEx_PermitStoreLocalCapViolation => 0b10110, CapEx_AccessSystemRegsViolation => 0b11000, CapEx_PermitCInvokeViolation => 0b11001, CapEx_PermitSetCIDViolation => 0b11100 @@ -138,7 +136,6 @@ function string_of_capex (ex) : CapEx -> string = CapEx_PermitStoreViolation => "PermitStoreViolation" , CapEx_PermitLoadCapViolation => "PermitLoadCapViolation" , CapEx_PermitStoreCapViolation => "PermitStoreCapViolation" , - CapEx_PermitStoreLocalCapViolation => "PermitStoreLocalCapViolation", CapEx_AccessSystemRegsViolation => "AccessSystemRegsViolation" , CapEx_PermitCInvokeViolation => "PermitCInvokeViolation" , CapEx_PermitSetCIDViolation => "PermitSetCIDViolation"