Merge branch 'sail2' into cheri-mono

In order to use up-to-date sequential CHERI model for test suite

8 files changed, 66 insertions, 34 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index 7173f24d..9d3a2196 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -43,6 +43,10 @@ riscv_sequentialScript.sml : riscv_sequential.lem riscv_extras_sequential.lem
 		riscv_sequential_types.lem \
 		riscv_sequential.lem
 
+# we exclude prelude.sail here, most code there should move to sail lib
+LOC_FILES:=$(SAIL_SRCS) main.sail
+include ../etc/loc.mk
+
 clean:
 	-rm -rf riscv _sbuild
 	-rm -f riscv.lem riscv_types.lem
diff --git a/riscv/main.sail b/riscv/main.sail
index 5d7b1108..28afe5ac 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -43,7 +43,6 @@ function main () = {
     loop ()
   } catch {
     Error_not_implemented(s) => print_string("Error: Not implemented: ", s),
-    Error_misaligned_access() => print("Error: misaligned_access"),
     Error_EBREAK() => print("EBREAK"),
     Error_internal_error() => print("Error: internal error")
   }
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index d667573e..c92497c1 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -350,11 +350,11 @@ infix 4 <_u
 infix 4 >=_u
 infix 4 <=_u
 
-val operator <_s  = {lem: "slt_vec"}   : forall 'n. (bits('n), bits('n)) -> bool
-val operator >=_s = {lem: "sgteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-val operator <_u  = {lem: "ult_vec"}   : forall 'n. (bits('n), bits('n)) -> bool
-val operator >=_u = {lem: "ugteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
-val operator <=_u = {lem: "ulteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
+val operator <_s  : forall 'n. (bits('n), bits('n)) -> bool
+val operator >=_s : forall 'n. (bits('n), bits('n)) -> bool
+val operator <_u  : forall 'n. (bits('n), bits('n)) -> bool
+val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
+val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool
 
 function operator <_s  (x, y) = signed(x) < signed(y)
 function operator >=_s (x, y) = signed(x) >= signed(y)
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index d93c7dae..374ea4a9 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -254,7 +254,8 @@ function clause print_insn (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
       (HALF,   true)  => "lhu   ",
       (WORD,   false) => "lw    ",
       (WORD,   true)  => "lwu   ",
-      (_,      _)     => "ld.bad "
+      (DOUBLE, false) => "ld    ",
+      (DOUBLE, true)  => "ldu   "
     } in
   insn ^ rd ^ ", " ^ rs1 ^ ", " ^ BitStr(imm)
 
@@ -822,6 +823,7 @@ function readCSR csr : csreg -> xlenbits =
     0xF13 => mimpid,
     0xF14 => mhartid,
     0x300 => mstatus.bits(),
+    0x301 => misa.bits(),
     0x302 => medeleg.bits(),
     0x303 => mideleg.bits(),
     0x304 => mie.bits(),
@@ -850,6 +852,9 @@ function readCSR csr : csreg -> xlenbits =
     0xC01 => mtime,
     0xC02 => minstret,
 
+    /* trigger/debug */
+    0x7a0 => ~(tselect),    /* this indicates we don't have any trigger support */
+
     _     => { print_bits("unhandled read to CSR ", csr);
                0x0000_0000_0000_0000 }
   }
@@ -882,6 +887,9 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit =
     0x144 => { mip = legalize_sip(mip, mideleg, value); Some(mip.bits()) },
     0x180 => { satp = legalize_satp(cur_Architecture(), satp, value); Some(satp) },
 
+    /* trigger/debug */
+    0x7a0 => { tselect = value; Some(tselect) },
+
     _     => None()
   } in
   match res {
@@ -889,9 +897,6 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit =
     None()  => print_bits("unhandled write to CSR ", csr)
   }
 
-val signalIllegalInstruction : unit -> unit effect {escape}
-function signalIllegalInstruction () = not_implemented ("illegal instruction")
-
 function clause execute CSR(csr, rs1, rd, is_imm, op) =
   let rs1_val : xlenbits = if is_imm then EXTZ(rs1) else X(rs1) in
   let isWrite : bool = match op {
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 7783317a..7ddd8a44 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -51,7 +51,6 @@ function step() = {
       false
     },
     None() => {
-      print_bits("PC: ", PC);
       match fetch() {
         F_Error(e, addr) => {
           handle_mem_exception(addr, e);
@@ -60,12 +59,12 @@ function step() = {
         F_RVC(h) => {
           match decodeCompressed(h) {
             None() => {
-              print(BitStr(h) ^ " :  <no-decode>");
+              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(h) ^ " :  <no-decode>");
               handle_decode_exception(EXTZ(h));
               false
             },
             Some(ast) => {
-              print(BitStr(h) ^ " :  " ^ ast);
+              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(h) ^ " :  " ^ ast);
               nextPC = PC + 2;
               execute(ast);
               true
@@ -75,12 +74,12 @@ function step() = {
         F_Base(w) => {
           match decode(w) {
             None() => {
-              print(BitStr(w) ^ " :  <no-decode>");
+              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(w) ^ " :  <no-decode>");
               handle_decode_exception(EXTZ(w));
               false
             },
             Some(ast) => {
-              print(BitStr(w) ^ " :  " ^ ast);
+              print("PC: " ^ BitStr(PC) ^ " instr: " ^ BitStr(w) ^ " :  " ^ ast);
               nextPC = PC + 4;
               execute(ast);
               true
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index ce5ef321..803531bd 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -404,6 +404,9 @@ register sepc : xlenbits
 register scause : Mcause
 register stval : xlenbits
 
+/* disabled trigger/debug module */
+register tselect : xlenbits
+
 /* csr name printer */
 
 val cast csr_name : csreg -> string
@@ -466,6 +469,8 @@ function csr_name(csr) = {
     0xB80  => "mcycleh",
     0xB82  => "minstreth",
     /* TODO: other hpm counters and events */
+    /* trigger/debug */
+    0x7a0  => "tselect",
     _      => "UNKNOWN"
   }
 }
@@ -515,6 +520,9 @@ function is_CSR_defined (csr : bits(12), p : Privilege) -> bool =
     /* supervisor mode: address translation */
     0x180 => p == Machine | p == Supervisor, // satp
 
+    /* disabled trigger/debug module */
+    0x7a0 => p == Machine,
+
     _     => false
   }
 
@@ -619,7 +627,7 @@ union ctl_result = {
 
 function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits))
                     -> xlenbits = {
-  print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv);
+  print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info)));
   match (del_priv) {
     Machine => {
        mcause->IsInterrupt() = intr;
diff --git a/riscv/riscv_types.sail b/riscv/riscv_types.sail
index 2a5a03ec..ee0eb94d 100644
--- a/riscv/riscv_types.sail
+++ b/riscv/riscv_types.sail
@@ -259,7 +259,6 @@ function trapVectorMode_of_bits (m) = {
 
 union exception = {
   Error_not_implemented : string,
-  Error_misaligned_access : unit,
   Error_EBREAK : unit,
   Error_internal_error : unit
 }
diff --git a/riscv/riscv_vmem.sail b/riscv/riscv_vmem.sail
index 0c1b9949..7fddb047 100644
--- a/riscv/riscv_vmem.sail
+++ b/riscv/riscv_vmem.sail
@@ -128,7 +128,7 @@ union PTW_Result = {
 val walk39 : (vaddr39, AccessType, Privilege, bool, bool, paddr39, nat, bool) -> PTW_Result effect {rmem, escape}
 function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = {
   let va = Mk_SV39_Vaddr(vaddr);
-  let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[SV39_LEVEL_BITS .. 0]),
+  let pt_ofs : paddr39 = shiftl(EXTZ(shiftr(va.VPNi(), (level * SV39_LEVEL_BITS))[(SV39_LEVEL_BITS - 1) .. 0]),
                                 PTE39_LOG_SIZE);
   let pte_addr = ptb + pt_ofs;
   match (checked_mem_read(Data, EXTZ(pte_addr), 8)) {
@@ -142,22 +142,32 @@ function walk39(vaddr, ac, priv, mxr, sum, ptb, level, global) -> PTW_Result = {
         PTW_Failure(PTW_Invalid_PTE)
       } else {
         if isPTEPtr(pbits) then {
-          if level == 0 then PTW_Failure(PTW_Invalid_PTE)
-          else walk39(vaddr, ac, priv, mxr, sum, EXTZ(pte.PPNi()), level - 1, is_global)
+          if level == 0 then {
+            /* last-level PTE contains a pointer instead of a leaf */
+            PTW_Failure(PTW_Invalid_PTE)
+          } else {
+            /* walk down the pointer to the next level */
+            walk39(vaddr, ac, priv, mxr, sum, EXTZ(shiftl(pte.PPNi(), PAGESIZE_BITS)), level - 1, is_global)
+          }
         } else { /* leaf PTE */
-          if ~ (checkPTEPermission(ac, priv, mxr, sum, pattr)) then
+          if ~ (checkPTEPermission(ac, priv, mxr, sum, pattr)) then {
             PTW_Failure(PTW_No_Permission)
-          else {
+          } else {
             if level > 0 then { /* superpage */
-              let masked = pte.PPNi() & EXTZ(shiftl(0b1, level * SV39_LEVEL_BITS) - 1);
-              if masked != EXTZ(0b0) then
+              /* fixme hack: to get a mask of appropriate size */
+              let mask = shiftl(pte.PPNi() ^ pte.PPNi() ^ EXTZ(0b1), level * SV39_LEVEL_BITS) - 1;
+              if (pte.PPNi() & mask) != EXTZ(0b0) then {
+                /* misaligned superpage mapping */
                 PTW_Failure(PTW_Misaligned)
-              else {
-                let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & EXTZ(shiftl(0b1, level * SV39_LEVEL_BITS) - 1));
+              } else {
+                /* add the appropriate bits of the VPN to the superpage PPN */
+                let ppn = pte.PPNi() | (EXTZ(va.VPNi()) & mask);
                 PTW_Success(append(ppn, va.PgOfs()), pte, pte_addr, level, is_global)
               }
-            } else
+            } else {
+              /* normal leaf PTE */
               PTW_Success(append(pte.PPNi(), va.PgOfs()), pte, pte_addr, level, is_global)
+            }
           }
         }
       }
@@ -184,7 +194,8 @@ val make_TLB39_Entry : (asid64, bool, vaddr39, paddr39, SV39_PTE, nat, paddr39)
 
 function make_TLB39_Entry(asid, global, vAddr, pAddr, pte, level, pteAddr) = {
   let shift : nat = PAGESIZE_BITS + (level * SV39_LEVEL_BITS);
-  let vAddrMask : vaddr39 = shiftl(EXTZ(0b1), shift) - 1;
+  /* fixme hack: use a better idiom for masks */
+  let vAddrMask : vaddr39 = shiftl(vAddr ^ vAddr ^ EXTZ(0b1), shift) - 1;
   let vMatchMask : vaddr39 = ~ (vAddrMask);
   struct {
     asid = asid,
@@ -245,7 +256,7 @@ union TR39_Result = {
   TR39_Failure : PTW_Error
 }
 
-let enable_dirty_update = true
+let enable_dirty_update = false
 
 val translate39 : (vaddr39, AccessType, Privilege, bool, bool, nat) -> TR39_Result effect {rreg, wreg, wmv, escape, rmem}
 function translate39(vAddr, ac, priv, mxr, sum, level) = {
@@ -260,8 +271,10 @@ function translate39(vAddr, ac, priv, mxr, sum, level) = {
           None() => TR39_Address(ent.pAddr | EXTZ(vAddr & ent.vAddrMask)),
           Some(pbits) => {
             if ~ (enable_dirty_update)
-            then TR39_Failure(PTW_PTE_Update)
-            else {
+            then {
+              /* pte needs dirty/accessed update but that is not enabled */
+              TR39_Failure(PTW_PTE_Update)
+            } else {
               /* update PTE entry and TLB */
               n_ent : TLB39_Entry = ent;
               n_ent.pte = update_BITS(ent.pte, pbits.bits());
@@ -288,15 +301,20 @@ function translate39(vAddr, ac, priv, mxr, sum, level) = {
             },
             Some(pbits) =>
               if ~ (enable_dirty_update)
-              then TR39_Failure(PTW_PTE_Update)
-              else {
+              then {
+                /* pte needs dirty/accessed update but that is not enabled */
+                TR39_Failure(PTW_PTE_Update)
+              } else {
                 w_pte : SV39_PTE = update_BITS(pte, pbits.bits());
                 match checked_mem_write(EXTZ(pteAddr), 8, w_pte.bits()) {
                   MemValue(_) => {
                     addToTLB39(asid, vAddr, pAddr, w_pte, pteAddr, level, global);
                     TR39_Address(pAddr)
                   },
-                  MemException(e) => TR39_Failure(PTW_Access)
+                  MemException(e) => {
+                    /* pte is not in valid memory */
+                    TR39_Failure(PTW_Access)
+                  }
                 }
               }
           }