Add load and store cap.

3 files changed, 176 insertions, 12 deletions

diff --git a/model/cheri_insts.sail b/model/cheri_insts.sail
index c4a6d60..2bec68c 100644
--- a/model/cheri_insts.sail
+++ b/model/cheri_insts.sail
@@ -231,7 +231,7 @@ function clause execute (CSpecialRW(cd, cs, idx)) =
   } else if (ro & cs != 0) |
      (cur_privilege <_u priv) |
      (needASR & not(pcc_access_system_regs())) then {
-    raise_c2_exception(CapEx_AccessSystemRegsViolation, idx)
+    raise_c2_exception6(CapEx_AccessSystemRegsViolation, 0b1 @ idx)
   } else {
     let cs_val = readCapReg(cs);
     if (cd != 0) then {
@@ -837,7 +837,7 @@ function clause execute (CCall(cs, cb, 0b00001)) = /* selector=1 */
 function clause execute (CCall(_, _, 0b11111)) = /* CReturn */
 {
   checkCP2usable();
-  raise_c2_exception(CapEx_ReturnTrap, 0b11111)
+  raise_c2_exception(CapEx_ReturnTrap, 0b11111) /* XXX what should correct reg number be? */
 }
 
 union clause ast = CJALR : (regbits, regbits)
@@ -870,7 +870,7 @@ function clause execute(CJALR(cd, cb)) =
   };
 }
 
-val handle_load_data_via_cap : (regbits, regbits, Capability, uint64, bool, word_width) -> bool effect {escape, rmem, rreg, wmv, wreg}
+val handle_load_data_via_cap : (regbits, bits(6), Capability, uint64, bool, word_width) -> bool effect {escape, rmem, rreg, wmv, wreg}
 function handle_load_data_via_cap(rd, cs, cap_val, vaddr, is_unsigned, width) = {
   let (base, top) = getCapBounds(cap_val);
   let vaddrBits = to_bits(xlen, vaddr);
@@ -878,15 +878,15 @@ function handle_load_data_via_cap(rd, cs, cap_val, vaddr, is_unsigned, width) =
   let aq : bool = false;
   let rl : bool = false;
   if not(cap_val.tag) then {
-    raise_c2_exception(CapEx_TagViolation, cs);
+    raise_c2_exception6(CapEx_TagViolation, cs);
   } else if cap_val.sealed then {
-    raise_c2_exception(CapEx_SealViolation, cs);
+    raise_c2_exception6(CapEx_SealViolation, cs);
   } else if not (cap_val.permit_load) then {
-    raise_c2_exception(CapEx_PermitLoadViolation, cs);
+    raise_c2_exception6(CapEx_PermitLoadViolation, cs);
   } else if (vaddr + size) > top then {
-    raise_c2_exception(CapEx_LengthViolation, cs);
+    raise_c2_exception6(CapEx_LengthViolation, cs);
   } else if vaddr < base then {
-    raise_c2_exception(CapEx_LengthViolation, cs);
+    raise_c2_exception6(CapEx_LengthViolation, cs);
   } else if check_misaligned(vaddrBits, width) then {
     handle_mem_exception(vaddrBits, E_Load_Addr_Align);
     false
@@ -902,7 +902,7 @@ function clause execute (CLoadDDC(rd, rs, is_unsigned, width)) =
   checkCP2usable();
   let ddc_val = DDC;
   let vaddr = (getCapBase(ddc_val) + unsigned(X(rs))) % pow2(xlen);
-  handle_load_data_via_cap(rd, 0b00000, ddc_val, vaddr, is_unsigned, width)
+  handle_load_data_via_cap(rd, 0b100001, ddc_val, vaddr, is_unsigned, width)
 }
 
 union clause ast = CLoadCap : (regbits, regbits, bool, word_width)
@@ -911,7 +911,56 @@ function clause execute (CLoadCap(rd, cs, is_unsigned, width)) =
   checkCP2usable();
   let cap_val = readCapReg(cs);
   let vaddr = getCapCursor(cap_val);
-  handle_load_data_via_cap(rd, cs, cap_val, vaddr, is_unsigned, width)
+  handle_load_data_via_cap(rd, 0b0 @ cs, cap_val, vaddr, is_unsigned, width)
+}
+
+val handle_load_cap_via_cap : (regbits, bits(6), Capability, uint64) -> bool effect {escape, rmem, rmemt, rreg, wmv, wreg}
+function handle_load_cap_via_cap(rd, cs, cap_val, vaddr) = {
+  let (base, top) = getCapBounds(cap_val);
+  let vaddrBits = to_bits(xlen, vaddr);
+  let aq : bool = false;
+  let rl : bool = false;
+  if not(cap_val.tag) then {
+    raise_c2_exception6(CapEx_TagViolation, cs);
+  } else if cap_val.sealed then {
+    raise_c2_exception6(CapEx_SealViolation, cs);
+  } else if not (cap_val.permit_load) then {
+    raise_c2_exception6(CapEx_PermitLoadViolation, cs);
+  } else if (vaddr + cap_size) > top then {
+    raise_c2_exception6(CapEx_LengthViolation, cs);
+  } else if vaddr < base then {
+    raise_c2_exception6(CapEx_LengthViolation, cs);
+  } else if not(is_aligned_addr(vaddrBits, cap_size)) then {
+    handle_mem_exception(vaddrBits, E_Load_Addr_Align);
+    false
+  } else match translateAddr(vaddrBits, Read, Data) {
+    TR_Failure(e) => { handle_mem_exception(vaddrBits, e); false },
+    TR_Address(addr) => {
+      let c = mem_read_cap(addr, aq, rl, false);
+      match c {
+        MemValue(v) => {writeCapReg(rd, v); true},
+        MemException(e) => {handle_mem_exception(vaddrBits, e); false }
+      }
+    }
+  }
+}
+
+union clause ast = CLoadCapDDC : (regbits, regbits)
+function clause execute (CLoadCapDDC(rd, rs)) =
+{
+  checkCP2usable();
+  let ddc_val = DDC;
+  let vaddr = (getCapBase(ddc_val) + unsigned(X(rs))) % pow2(xlen);
+  handle_load_cap_via_cap(rd, 0b100001, ddc_val, vaddr)
+}
+
+union clause ast = CLoadCapCap : (regbits, regbits)
+function clause execute (CLoadCapCap(rd, cs)) =
+{
+  checkCP2usable();
+  let cap_val = readCapReg(cs);
+  let vaddr = getCapCursor(cap_val);
+  handle_load_cap_via_cap(rd, 0b0 @ cs, cap_val, vaddr)
 }
 
 val handle_store_data_via_cap : (regbits, regbits, Capability, uint64, word_width) -> bool effect {eamem, escape, rmem, rreg, wmv, wreg}
@@ -960,7 +1009,7 @@ function handle_store_data_via_cap(rs, cs, cap_val, vaddr, width) = {
 }
 
 union clause ast = CStoreDDC : (regbits, regbits, word_width)
-function clause execute (CLoadDDC(rd, rs, is_unsigned, width)) =
+function clause execute (CStoreDDC(rd, rs, width)) =
 {
   checkCP2usable();
   let ddc_val = DDC;
@@ -969,7 +1018,7 @@ function clause execute (CLoadDDC(rd, rs, is_unsigned, width)) =
 }
 
 union clause ast = CStoreCap : (regbits, regbits, word_width)
-function clause execute (CLoadCap(rs, cs, is_unsigned, width)) =
+function clause execute (CStoreCap(rs, cs, width)) =
 {
   checkCP2usable();
   let cap_val = readCapReg(cs);
@@ -977,6 +1026,63 @@ function clause execute (CLoadCap(rs, cs, is_unsigned, width)) =
   handle_store_data_via_cap(rs, cs, cap_val, vaddr, width)
 }
 
+val handle_store_cap_via_cap : (regbits, regbits, Capability, uint64) -> bool effect {eamem, escape, rmem, rreg, wmv, wreg, wmvt}
+function handle_store_cap_via_cap(rs, cs, cap_val, vaddr) = {
+  let (base, top) = getCapBounds(cap_val);
+  let vaddrBits = to_bits(xlen, vaddr);
+  let aq : bool = false;
+  let rl : bool = false;
+  if not(cap_val.tag) then {
+    raise_c2_exception(CapEx_TagViolation, cs);
+  } else if cap_val.sealed then {
+    raise_c2_exception(CapEx_SealViolation, cs);
+  } else if not (cap_val.permit_store) then {
+    raise_c2_exception(CapEx_PermitStoreViolation, cs);
+  } else if (vaddr + cap_size) > top then {
+    raise_c2_exception(CapEx_LengthViolation, cs);
+  } else if vaddr < base then {
+    raise_c2_exception(CapEx_LengthViolation, cs);
+  } else if not(is_aligned_addr(vaddrBits, cap_size)) then {
+    handle_mem_exception(vaddrBits, E_SAMO_Addr_Align);
+    false
+  } else match translateAddr(vaddrBits, Write, Data) {
+    TR_Failure(e) => { handle_mem_exception(vaddrBits, e); false },
+    TR_Address(addr) => {
+      let eares : MemoryOpResult(unit) = mem_write_ea_cap(addr, aq, rl, false);
+      match (eares) {
+        MemException(e) => { handle_mem_exception(addr, e); false },
+        MemValue(_) => {
+          let rs_val = readCapReg(rs);
+          let res : MemoryOpResult(bool) = mem_write_cap(addr, rs_val, aq, rl, false);
+          match (res) {
+            MemValue(true)  => true,
+            MemValue(false) => internal_error("store got false from mem_write_value"),
+            MemException(e) => { handle_mem_exception(addr, e); false }
+          }
+        }
+      }
+    }
+  }
+}
+
+union clause ast = CStoreCapDDC : (regbits, regbits)
+function clause execute (CStoreCapDDC(rd, rs)) =
+{
+  checkCP2usable();
+  let ddc_val = DDC;
+  let vaddr = (getCapBase(ddc_val) + unsigned(X(rs))) % pow2(xlen);
+  handle_store_cap_via_cap(rd, 0b00000, ddc_val, vaddr)
+}
+
+union clause ast = CStoreCapCap : (regbits, regbits)
+function clause execute (CStoreCapCap(rs, cs)) =
+{
+  checkCP2usable();
+  let cap_val = readCapReg(cs);
+  let vaddr = getCapCursor(cap_val);
+  handle_store_cap_via_cap(rs, cs, cap_val, vaddr)
+}
+
 /*
 
 union clause ast = CLoadTags : (regbits, regbits)
@@ -1354,6 +1460,8 @@ mapping clause encdec = CStoreDDC(rd, rs, BYTE)         <-> 0b0000000 @ 0b01000
 mapping clause encdec = CStoreDDC(rd, rs, HALF)         <-> 0b0000000 @ 0b01001 @ rs @ 0b000 @ rd @ 0b1011011  /* shddc */
 mapping clause encdec = CStoreDDC(rd, rs, WORD)         <-> 0b0000000 @ 0b01010 @ rs @ 0b000 @ rd @ 0b1011011  /* swddc */
 mapping clause encdec = CStoreDDC(rd, rs, DOUBLE)       <-> 0b0000000 @ 0b01011 @ rs @ 0b000 @ rd @ 0b1011011  /* sdddc */
+mapping clause encdec = CStoreCapDDC(rd, rs)            <-> 0b0000000 @ 0b01100 @ rs @ 0b000 @ rd @ 0b1011011  /* sqddc */
+mapping clause encdec = CLoadCapDDC(rd, rs)             <-> 0b0000000 @ 0b01101 @ rs @ 0b000 @ rd @ 0b1011011  /* lqddc */
 
 /* Load / store data via cap, cs */
 mapping clause encdec = CLoadCap(rd, cs, false, BYTE)   <-> 0b0000000 @ 0b10000 @ cs @ 0b000 @ rd @ 0b1011011  /* lbcap */
@@ -1368,6 +1476,8 @@ mapping clause encdec = CStoreCap(rd, cs, BYTE)         <-> 0b0000000 @ 0b11000
 mapping clause encdec = CStoreCap(rd, cs, HALF)         <-> 0b0000000 @ 0b11001 @ cs @ 0b000 @ rd @ 0b1011011  /* shcap */
 mapping clause encdec = CStoreCap(rd, cs, WORD)         <-> 0b0000000 @ 0b11010 @ cs @ 0b000 @ rd @ 0b1011011  /* swcap */
 mapping clause encdec = CStoreCap(rd, cs, DOUBLE)       <-> 0b0000000 @ 0b11011 @ cs @ 0b000 @ rd @ 0b1011011  /* sdcap */
+mapping clause encdec = CStoreCapCap(rd, cs)            <-> 0b0000000 @ 0b11100 @ cs @ 0b000 @ rd @ 0b1011011  /* sqcap */
+mapping clause encdec = CLoadCapCap(rd, cs)             <-> 0b0000000 @ 0b11101 @ cs @ 0b000 @ rd @ 0b1011011  /* lqcap */
 
 /*
 
diff --git a/model/prelude.sail b/model/prelude.sail
index 03233b2..e26bf0b 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -1001,6 +1001,9 @@ function __RISCV_read (addr, width, aq, rl, res) =
     (false, true,  true)  => None()
   }
 
+val MEMr_tag = "read_tag_bool"  : bits(64) -> bool effect { rmemt }
+val MEMw_tag = "write_tag_bool" : (bits(64) , bool) -> unit effect { wmvt }
+
 val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
 
 val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm)
diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail
index 0b3e550..5029480 100644
--- a/model/riscv_mem.sail
+++ b/model/riscv_mem.sail
@@ -84,6 +84,28 @@ function mem_read (addr, width, aq, rl, res) = {
  result
 }
 
+val mem_read_cap : (xlenbits, bool, bool, bool) -> MemoryOpResult(Capability) effect {rmem, rmemt, rreg, escape}
+function mem_read_cap (addr, aq, rl, res) = {
+  let result : MemoryOpResult(bits(8 * 'cap_size)) =
+  if ~(is_aligned_addr(addr, cap_size))
+  then MemException(E_Load_Addr_Align)
+  else match (aq, rl, res) {
+    (false, false, false) => checked_mem_read(Data, addr, cap_size, false, false, false),
+    (true,  false, false) => MEMr_acquire(addr, cap_size),
+    (false, false, true)  => MEMr_reserved(addr, cap_size),
+    (true,  false, true)  => MEMr_reserved_acquire(addr, cap_size),
+    (false, true,  false) => throw(Error_not_implemented("load.rl")),
+    (true,  true,  false) => MEMr_strong_acquire(addr, cap_size),
+    (false, true,  true)  => throw(Error_not_implemented("lr.rl")),
+    (true,  true,  true)  => MEMr_reserved_strong_acquire(addr, cap_size)
+  };
+  let tag = MEMr_tag(addr);
+  match result {
+    MemValue(v) => MemValue(memBitsToCapability(tag, v)),
+    MemException(e) => MemException(e) : MemoryOpResult(Capability)
+  }
+}
+
 val MEMea = {lem: "MEMea", coq: "MEMea", _: "memea"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
 val MEMea_release = {lem: "MEMea_release", coq: "MEMea_release", _: "memea"} : forall 'n.
@@ -114,6 +136,14 @@ function mem_write_ea (addr, width, aq, rl, con) = {
   }
 }
 
+val mem_write_ea_cap : (xlenbits, bool, bool, bool) -> MemoryOpResult(unit) effect {eamem}
+function mem_write_ea_cap(addr, aq, rl, con) = {
+  if ~(is_aligned_addr(addr, cap_size)) then
+     MemException(E_SAMO_Addr_Align)
+  else
+     MemValue(MEMea(addr, cap_size))
+}
+
 // only used for actual memory regions, to avoid MMIO effects
 function phys_mem_write forall 'n. (addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> MemoryOpResult(bool) = {
   print_mem("mem[" ^ BitStr(addr) ^ "] <- " ^ BitStr(data));
@@ -178,6 +208,27 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
   }
 }
 
+/* NOTE: The wreg effect is due to MMIO, the rreg is due to checking mtime. */
+val mem_write_cap : (xlenbits, Capability, bool, bool, bool) -> MemoryOpResult(bool) effect {wmv, rreg, wreg, escape, wmvt}
+
+function mem_write_cap (addr, cap, aq, rl, con) = {
+  let cap_bits = capToMemBits(cap);
+  MEMw_tag(addr, cap.tag);
+  rvfi_write(addr, cap_size, cap_bits);
+  if ~ (is_aligned_addr(addr, cap_size))
+  then MemException(E_SAMO_Addr_Align)
+  else match (aq, rl, con) {
+    (false, false, false) => checked_mem_write(addr, cap_size, cap_bits),
+    (false, true,  false) => MEMval_release(addr, cap_size, cap_bits),
+    (false, false, true)  => MEMval_conditional(addr, cap_size, cap_bits),
+    (false, true,  true)  => MEMval_conditional_release(addr, cap_size, cap_bits),
+    (true,  false, false) => throw(Error_not_implemented("store.aq")),
+    (true,  true,  false) => MEMval_strong_release(addr, cap_size, cap_bits),
+    (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
+    (true,  true,  true)  => MEMval_conditional_strong_release(addr, cap_size, cap_bits)
+  }
+}
+
 val MEM_fence_rw_rw = {lem: "MEM_fence_rw_rw", coq: "MEM_fence_rw_rw", _: "skip"} : unit -> unit effect {barr}
 val MEM_fence_r_rw  = {lem: "MEM_fence_r_rw", coq: "MEM_fence_r_rw", _: "skip"}  : unit -> unit effect {barr}
 val MEM_fence_r_r   = {lem: "MEM_fence_r_r", coq: "MEM_fence_r_r", _: "skip"}   : unit -> unit effect {barr}