Add support for read_tag and write_tag in sail_lib.ml. and support for intialising and dumping CHERI state. Somewhat working cheri sail2 model.

10 files changed, 146 insertions, 41 deletions

diff --git a/cheri/Makefile b/cheri/Makefile
index a443d123..26bc84ef 100644
--- a/cheri/Makefile
+++ b/cheri/Makefile
@@ -7,9 +7,7 @@ CHERI_SAIL_DIR:=$(SAIL_DIR)/cheri
 SAIL:=$(SAIL_DIR)/sail
 SAIL_LIB_HEADERS:=$(SAIL_LIB_DIR)/flow.sail
 
-MIPS_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(MIPS_SAIL_DIR)/mips_wrappers.sail $(MIPS_SAIL_DIR)/mips_ast_decl.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail
-
-CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+CHERI_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail $(MIPS_SAIL_DIR)/main.sail
 
 CHERI128_SAILS:=$(SAIL_LIB_HEADERS) $(MIPS_SAIL_DIR)/prelude.sail $(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail  $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
@@ -17,7 +15,7 @@ cheri: $(CHERI_SAILS)
 	$(SAIL) -ocaml -o cheri $(CHERI_SAILS)
 
 clean:
-	rm -rf _sbuild
+	rm -rf cheri _sbuild
 
 EXTRACT_INST=sed -n "/START_${1}\b/,/END_${1}\b/p" cheri_insts.sail | sed 's/^  //;1d;$$d' > inst_$1.sail
 extract: cheri_insts.sail
diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail
index 9e3a0cd9..c1afbdb2 100644
--- a/cheri/cheri_prelude_256.sail
+++ b/cheri/cheri_prelude_256.sail
@@ -90,7 +90,31 @@ let null_cap : CapStruct = struct {
   length = 0xffffffffffffffff
 }
 
+let default_cap : CapStruct = struct {
+  tag = true,
+  padding = zeros(),
+  otype = zeros(),
+  uperms = ones(),
+  perm_reserved11_14 = zeros(),
+  access_system_regs = true,
+  perm_reserved9 = false,
+  permit_ccall = true,
+  permit_seal = true,
+  permit_store_local_cap = true,
+  permit_store_cap = true,
+  permit_load_cap = true,
+  permit_store = true,
+  permit_load = true,
+  permit_execute = true,
+  global = true,
+  sealed = false,
+  offset = zeros(),
+  base = zeros(),
+  length = 0xffffffffffffffff
+}
+
 let 'cap_size = 32
+let cap_addr_mask = to_bits(64, pow2(64) - cap_size)
 
 function capRegToCapStruct(capReg) : CapReg -> CapStruct =
   struct {
diff --git a/cheri/cheri_prelude_common.sail b/cheri/cheri_prelude_common.sail
index 6b29ffce..ac9d4a89 100644
--- a/cheri/cheri_prelude_common.sail
+++ b/cheri/cheri_prelude_common.sail
@@ -35,13 +35,12 @@
 
 scattered union ast
 
-val execute : ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmvt, wreg}
+val execute : ast -> unit effect {barr, eamem, escape, rmem, rmemt, rreg, undef, wmv, wmvt, wreg}
 scattered function execute
 
 val decode : bits(32) -> option(ast) effect pure
 scattered function decode
 
-
 register PCC        : CapReg
 register nextPCC    : CapReg
 register delayedPCC : CapReg
@@ -256,41 +255,52 @@ function register_inaccessible(r) =
   else
     false
 
-val MEMr_tag         : forall 'n. ( bits(64) , atom('n) ) -> (bool, bits(8 * 'n)) effect { rmemt }
-val MEMr_tag_reserve : forall 'n. ( bits(64) , atom('n) ) -> (bool, bits(8 * 'n)) effect { rmemt }
-
-val MEMval_tag : forall 'n. ( bits(64) , atom('n), bool, bits(8*'n)) -> unit effect { wmvt }
-val MEMval_tag_conditional : forall 'n. ( bits(64) , atom('n), bool, bits(8*'n)) -> bool effect { wmvt }
+val MEMr_tag = "read_tag"  : bits(64) -> bool effect { rmemt }
+val MEMw_tag = "write_tag" : (bits(64) , bool) -> unit effect { wmvt }
 
-val MEMr_tagged : bits(64) -> (bool, bits('cap_size * 8)) effect { rmemt }
+val MEMr_tagged : bits(64) -> (bool, bits('cap_size * 8)) effect { escape, rmem, rmemt }
 function MEMr_tagged (addr) =
+{
   /* assumes addr is cap. aligned */
-  let (tag, data) =  MEMr_tag (addr, cap_size) in
+  assert(unsigned(addr) % cap_size == 0);
+  let tag  = MEMr_tag(addr) in
+  let data = MEMr(addr, cap_size) in
   (tag, reverse_endianness(data))
+}
 
-val MEMr_tagged_reserve : bits(64) -> (bool, bits('cap_size * 8)) effect { rmemt }
+val MEMr_tagged_reserve : bits(64) -> (bool, bits('cap_size * 8)) effect { escape, rmem, rmemt }
 function MEMr_tagged_reserve (addr) =
+{
   /* assumes addr is cap. aligned */
-  let (tag, data) = MEMr_tag_reserve(addr, cap_size) in
+  assert(unsigned(addr) % cap_size == 0);
+  let tag = MEMr_tag(addr) in
+  let data = MEMr_reserve(addr, cap_size) in
   (tag, reverse_endianness(data))
+}
 
-val MEMw_tagged : (bits(64), bool, bits('cap_size * 8)) -> unit effect { eamem, wmvt }
+val MEMw_tagged : (bits(64), bool, bits('cap_size * 8)) -> unit effect { escape, eamem, wmv, wmvt }
 function MEMw_tagged(addr, tag, data) =
 {
   /* assumes addr is cap. aligned */
+  assert(unsigned(addr) % cap_size == 0);
   MEMea(addr, cap_size);
-  MEMval_tag(addr, cap_size,  tag, reverse_endianness(data));
+  MEMval(addr, cap_size, reverse_endianness(data));
+  MEMw_tag(addr, tag);
 }
 
-val MEMw_tagged_conditional : (bits(64), bool, bits('cap_size * 8)) -> bool effect { eamem, wmvt }
+val MEMw_tagged_conditional : (bits(64), bool, bits('cap_size * 8)) -> bool effect { escape, eamem, wmv, wmvt }
 function MEMw_tagged_conditional(addr, tag, data) =
 {
   /* assumes addr is cap. aligned */
+  assert(unsigned(addr) % cap_size == 0);
   MEMea_conditional(addr, cap_size);
-  MEMval_tag_conditional(addr, cap_size, tag, reverse_endianness(data));
+  success = MEMval_conditional(addr, cap_size, reverse_endianness(data));
+  if success then
+     MEMw_tag(addr, tag);
+  success;
 }
 
-val MEMw_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmvt, wreg, eamem}
+val MEMw_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {escape, wmv, wmvt, wreg, eamem}
 function MEMw_wrapper(addr, size, data) =
   let ledata = reverse_endianness(data) in
   if (addr == 0x000000007f000000) then
@@ -300,17 +310,25 @@ function MEMw_wrapper(addr, size, data) =
   }
   else
   {
-    /* On cheri non-capability writes must clear the corresponding tag */
+    /* require that writes don't cross capability boundaries (should be true due to mips alignment requirements) */  
+    assert((addr & cap_addr_mask) == ((addr + to_bits(64, size - 1)) & cap_addr_mask));
     MEMea(addr, size);
-    MEMval_tag(addr, size, false, ledata);
+    MEMval(addr, size, ledata);
+    /* On cheri non-capability writes must clear the corresponding tag*/
+    MEMw_tag(addr & cap_addr_mask, false);
   }
 
-val MEMw_conditional_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmvt, eamem}
+val MEMw_conditional_wrapper : forall 'n, 'n >= 1. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {escape, wmv, wmvt, eamem}
 function MEMw_conditional_wrapper(addr, size, data) =
   {
-    /* On cheri non-capability writes must clear the corresponding tag*/
+    /* require that writes don't cross capability boundaries (should be true due to mips alignment requirements) */
+    assert((addr & cap_addr_mask) == ((addr + to_bits(64, size - 1)) & cap_addr_mask));
     MEMea_conditional(addr, size);
-    MEMval_tag_conditional(addr,size,false,reverse_endianness(data));
+    success = MEMval_conditional(addr,size,reverse_endianness(data));
+    if success then
+       /* On cheri non-capability writes must clear the corresponding tag */
+       MEMw_tag(addr & cap_addr_mask, false);
+    success;
   }
 
 val addrWrapper : (bits(64), MemAccessType, WordType) -> bits(64) effect {rreg, wreg, escape}
@@ -343,10 +361,10 @@ function addrWrapper(addr, accessType, width) =
 val TranslatePC : bits(64) -> bits(64) effect {rreg, wreg, undef, escape}
 function TranslatePC (vAddr) = {
   incrementCP0Count();
-  let pcc = capRegToCapStruct(PCC) in
-  let base  = getCapBase(pcc) in
-  let top   = getCapTop(pcc) in
-  let absPC = base + unsigned(vAddr) in
+  let pcc = capRegToCapStruct(PCC);
+  let base  = getCapBase(pcc);
+  let top   = getCapTop(pcc);
+  let absPC = base + unsigned(vAddr);
   if ((absPC % 4)  != 0) then /* bad PC alignment */
     (SignalExceptionBadAddr(AdEL, to_bits(64, absPC))) /* XXX absPC may be truncated */
   else if ((absPC + 4) > top) then
@@ -361,3 +379,37 @@ function checkCP2usable ()  =
       (CP0Cause->CE()) = 0b10;
       (SignalException(CpU));
     }
+
+function init_cp2_state () = {
+  let defaultBits = capStructToCapReg(default_cap);
+  PCC = defaultBits;
+  nextPCC = defaultBits;
+  delayedPCC = defaultBits;
+  foreach(i from 0 to 31) {
+    let idx = to_bits(5, i) in
+    writeCapReg(idx, default_cap);
+  }
+}
+
+val capToString : CapStruct -> string
+function capToString cap =
+         concat_str(" t:",
+         concat_str(if cap.tag then "1" else "0",
+         concat_str(" s:",
+         concat_str(if cap.sealed then "1" else "0",
+         concat_str(" perms:",
+         concat_str(BitStr(0b0 @ getCapPerms(cap)),
+         concat_str(" type:",
+         concat_str(BitStr(cap.otype),
+         concat_str(" offset:",
+         concat_str(BitStr(to_bits(64, getCapOffset(cap))),
+         concat_str(" base:",
+         concat_str(BitStr(to_bits(64, getCapBase(cap))),
+         concat_str(" length:", BitStr(to_bits(64, getCapLength(cap))))))))))))))))
+
+function dump_cp2_state () = {
+  print(concat_str("DEBUG CAP PCC", capToString(capRegToCapStruct(PCC))));
+  foreach(i from 0 to 31) {
+    print(concat_str("DEBUG CAP REG", concat_str(string_of_int(i), capToString(readCapReg(to_bits(5, i))))))
+  }
+}
\ No newline at end of file
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index 382e4d7f..c3197eda 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -556,6 +556,7 @@ function forall Nat 'r, 'r IN {1,2,4,8}.[:'r:] wordWidthBytes((WordType) w) =
     case D -> 8
   }
 
+
 (* This function checks that memory accesses are naturally aligned
    -- it is disabled in favour of BERI specific behaviour below.
 function bool isAddressAligned(addr, (WordType) wordType) =
diff --git a/mips_new_tc/Makefile b/mips_new_tc/Makefile
index d9ccba6b..fb926c6e 100644
--- a/mips_new_tc/Makefile
+++ b/mips_new_tc/Makefile
@@ -28,4 +28,4 @@ M%.thy: m%.lem m%_types.lem mips_extras.lem
 	lem -isa -outdir . -lib $(SAIL_DIR)/src/gen_lib -lib $(SAIL_DIR)/src/lem_interp $^
 
 clean:
-	rm -rf _sbuild
+	rm -rf mips Mips.thy mips.lem _sbuild
diff --git a/mips_new_tc/main.sail b/mips_new_tc/main.sail
index 0ccd7c71..71beb582 100644
--- a/mips_new_tc/main.sail
+++ b/mips_new_tc/main.sail
@@ -1,7 +1,7 @@
 
 
 
-val fetch_and_execute : unit -> unit effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef}
+val fetch_and_execute : unit -> unit effect {barr, eamem, escape, rmem, rreg, wmv, wreg, undef, wmvt, rmemt}
 function fetch_and_execute () = {
   while true do {
     PC = nextPC;
@@ -30,14 +30,16 @@ function fetch_and_execute () = {
          just continue from nextPC, which should have been set to the appropriate
          exception vector (along with clearing branchPending etc.) . */
     };
-  }
+  };
+  skip_rmemt();
+  skip_wmvt();
 }
 
 val elf_entry = "Elf_loader.elf_entry" : unit -> int
 
-val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg}
+val main : unit -> unit effect {barr, eamem, escape, rmem, rreg, undef, wmv, wreg, rmemt, wmvt}
 
-function dump_state () : unit -> unit = {
+function dump_mips_state () : unit -> unit = {
   print_bits("DEBUG MIPS PC ", PC);
   foreach (idx from 0 to 32) {
     print(concat_str("DEBUG MIPS REG ", concat_str(string_of_int(idx), concat_str(" ", BitStr(rGPR(to_bits(5,idx)))))));
@@ -45,8 +47,10 @@ function dump_state () : unit -> unit = {
 }
 
 function main () = {
+  init_cp0_state();
+  init_cp2_state();
   nextPC = to_bits(64, elf_entry());
-  CP0Status->BEV() = bitone;
   fetch_and_execute();
-  dump_state ()
+  dump_mips_state ();
+  dump_cp2_state ()
 }
diff --git a/mips_new_tc/mips_prelude.sail b/mips_new_tc/mips_prelude.sail
index d2e44092..d1302c52 100644
--- a/mips_new_tc/mips_prelude.sail
+++ b/mips_new_tc/mips_prelude.sail
@@ -343,6 +343,10 @@ val MEMval_conditional = {lem: "MEMval_conditional"} : forall 'n.
 /* Extern nops with effects, sometimes useful for faking effect */
 val skip_eamem = "skip" : unit -> unit effect {eamem}
 val skip_barr = "skip" : unit -> unit effect {barr}
+val skip_wreg = "skip" : unit -> unit effect {wreg}
+val skip_rreg = "skip" : unit -> unit effect {rreg}
+val skip_wmvt = "skip" : unit -> unit effect {wmvt}
+val skip_rmemt = "skip" : unit -> unit effect {rmemt}
 
 function MEMr (addr, size) = __MIPS_read(addr, size)
 function MEMr_reserve (addr, size) = __MIPS_read(addr, size)
@@ -426,8 +430,8 @@ function SignalExceptionMIPS (ex, kccBase) =
       throw (ISAException);
   }
 
+/* Defined either in mips_wrappers (directly calling SignalExceptionMIPS) or in cheri_prelude_common (cheri things plus above) */
 val SignalException : forall ('o : Type) . Exception -> 'o effect {escape, rreg, wreg}
-function SignalException (ex) = SignalExceptionMIPS(ex, 0x0000000000000000)
 
 val SignalExceptionBadAddr : forall ('o : Type) . (Exception, bits(64)) -> 'o effect {escape, rreg, wreg}
 function  SignalExceptionBadAddr(ex, badAddr) =
@@ -604,3 +608,11 @@ function MEMr_wrapper (addr, size) = reverse_endianness(MEMr (addr, size))
 val MEMr_reserve_wrapper : forall 'n, 1 <= 'n <= 8 . ( bits(64) , atom('n) ) -> (bits(8 * 'n)) effect { rmem }
 function MEMr_reserve_wrapper (addr , size) =
     reverse_endianness(MEMr_reserve(addr, size))
+
+
+function init_cp0_state () : unit -> unit = {
+  CP0Status->BEV() = bitone;
+}
+
+val init_cp2_state : unit -> unit effect {wreg}
+val dump_cp2_state : unit -> unit effect {rreg}
\ No newline at end of file
diff --git a/mips_new_tc/mips_wrappers.sail b/mips_new_tc/mips_wrappers.sail
index fd0619f4..bbb99e17 100644
--- a/mips_new_tc/mips_wrappers.sail
+++ b/mips_new_tc/mips_wrappers.sail
@@ -76,8 +76,10 @@ function TranslatePC (vAddr) = {
 
 let have_cp2 = false
 
-
-
+function SignalException (ex) = SignalExceptionMIPS(ex, 0x0000000000000000)
 
 val ERETHook : unit -> unit
 function ERETHook() = ()
+
+function init_cp2_state () = skip_wreg()
+function dump_cp2_state () = skip_rreg()
diff --git a/mips_new_tc/prelude.sail b/mips_new_tc/prelude.sail
index abf13188..3f1198f5 100644
--- a/mips_new_tc/prelude.sail
+++ b/mips_new_tc/prelude.sail
@@ -60,8 +60,7 @@ val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
 
 overload ~ = {not_bool, not_vec}
 
-val not : bool -> bool
-function not (b) = not_bool(b)
+val not = "not" : bool -> bool
 
 val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
 function neq_vec (x, y) = not_bool(eq_vec(x, y))
@@ -323,6 +322,9 @@ function EXTZ v = zero_extend(v, sizeof('m))
 val zeros : forall 'n, 'n >= 0 . unit -> bits('n)
 function zeros() = replicate_bits (0b0,'n)
 
+val ones : forall 'n, 'n >= 0 . unit -> bits('n)
+function ones() = replicate_bits (0b1,'n)
+
 infix 4 <_s
 infix 4 >=_s
 infix 4 <_u
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 44dd4ac5..4e78507f 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -433,6 +433,16 @@ let read_ram (addr_size, data_size, hex_ram, addr) =
   in
   read_byte data_size
 
+let tag_ram : bool RAM.t = RAM.create 256
+
+let write_tag (addr, tag) =
+  let addri = uint addr in
+  RAM.add tag_ram addri tag
+
+let read_tag addr =
+  let addri = uint addr in
+  try RAM.find tag_ram addri with Not_found -> false
+
 let rec reverse_endianness bits =
   if List.length bits <= 8 then bits else
   reverse_endianness (drop 8 bits) @ (take 8 bits)