Make store-local violations non-trapping.

It's difficult to write defensive code if stores may trap depending on
the copied value.  Allowing store-local to trap makes it easy to force
anything that copies on behalf of a caller able to trap by inserting a
local capability into the source that it's copying from.

This change is already made in CHERIoT Ibex, the spec is catching up.

This also removes the associated exception codes.  We may wish to
reserve them for a debugging mode for finding places where the tag
clearing occurs.

Fixes #20.

.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:

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"),

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"