Initial support for faults of reads to physical addresses.

5 files changed, 144 insertions, 100 deletions

diff --git a/riscv/main.sail b/riscv/main.sail
index 66ac89bd..b6484755 100644
--- a/riscv/main.sail
+++ b/riscv/main.sail
@@ -13,32 +13,43 @@ function fetch_and_execute () =
     /* for now, always fetch a 32-bit value.  this would need to
        change with privileged mode, since we could cross a page
        boundary with PC only 16-bit aligned in C mode.  */
-    let instr = __RISCV_read(PC, 4);
-
-    let (instr_ast, instr_sz) : (option(ast), int)=
-       match (instr[1 .. 0]) {
-         0b11 => (decode(instr), 4),
-	 _    => (decodeCompressed(instr[15 .. 0]), 2)
-       };
-    match (instr_ast, instr_sz) {
-      (Some(ast), 4) => print(BitStr(instr)          ^ ":  " ^ ast),
-      (Some(ast), 2) => print(BitStr(instr[15 .. 0]) ^ ":  " ^ ast),
-      (_,         _) => print(BitStr(instr)          ^ ":  no-decode")
-    };
-    /* check whether a compressed instruction is legal. */
-    if (misa.C() == 0b0 & (instr_sz == 2)) then {
-      let t : sync_exception =
-      struct { trap = E_Illegal_Instr,
-               excinfo = Some (EXTZ(instr)) } in
-      nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
-    } else {
-      nextPC = PC + instr_sz;
-      match instr_ast {
-        Some(ast) => execute(ast),
-	None()    => {print("Decode failed"); exit()}
+    let irdval = checked_mem_read(Instruction, PC, 4);
+    match (irdval) {
+      MemValue(instr) => {
+        let (instr_ast, instr_sz) : (option(ast), int) =
+          match (instr[1 .. 0]) {
+             0b11 => { cur_inst = EXTZ(instr);
+                       (decode(instr), 4)
+                     },
+             _    => { cur_inst = EXTZ(instr[15 .. 0]);
+                       (decodeCompressed(instr[15 .. 0]), 2)
+                     }
+          };
+        match (instr_ast, instr_sz) {
+          (Some(ast), 4) => print(BitStr(instr)          ^ ":  " ^ ast),
+          (Some(ast), 2) => print(BitStr(instr[15 .. 0]) ^ ":  " ^ ast),
+          (_,         _) => print(BitStr(instr)          ^ ":  no-decode")
+        };
+        /* check whether a compressed instruction is legal. */
+        if (misa.C() == 0b0 & (instr_sz == 2)) then {
+          let t : sync_exception = struct { trap = E_Illegal_Instr,
+                                            excinfo = Some(cur_inst) } in
+          nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+        } else {
+          nextPC = PC + instr_sz;
+          match instr_ast {
+            Some(ast) => execute(ast),
+            None()    => {print("Decode failed"); exit()}
+          }
+        }
+      },
+      MemException(e) => {
+        let t : sync_exception = struct { trap = e,
+                                          excinfo = Some(PC) } in
+        nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
       }
     };
-    let tohost_val = __RISCV_read(tohost, 4);
+    let tohost_val = __ReadRAM(64, 4, 0x0000_0000_0000_0000, tohost);
     if unsigned(tohost_val) != 0 then {
       let exit_val = unsigned(tohost_val >> 0b1) in
       if exit_val == 0 then
@@ -57,13 +68,6 @@ val elf_entry = {
 
 val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg}
 
-function dump_state () : unit -> unit = {
-  print("Dumping state");
-  print_bits(" PC: ", PC);
-  let instr = __RISCV_read(PC, 4);
-  print_bits(" instr: ", instr)
-}
-
 function main () = {
   PC = __GetSlice_int(64, elf_entry(), 0);
   try {
@@ -74,6 +78,5 @@ function main () = {
     Error_misaligned_access() => print("Error: misaligned_access"),
     Error_EBREAK() => print("EBREAK"),
     Error_internal_error() => print("Error: internal error")
-  };
-  dump_state ()
+  }
 }
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 2051c7fa..24e856e7 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -295,8 +295,8 @@ val __TraceMemoryWrite : forall 'n 'm.
 val __ReadRAM = "read_ram" : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem}
 
-val __RISCV_read : forall 'n. (bits(64), atom('n)) -> bits(8 * 'n) effect {rmem}
-function __RISCV_read (addr, width) = __ReadRAM(64, width, 0x0000_0000_0000_0000, addr)
+val __RISCV_read : forall 'n. (bits(64), atom('n)) -> option(bits(8 * 'n)) effect {rmem}
+function __RISCV_read (addr, width) = Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr))
 
 val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit
 
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 839d604d..550ccfee 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -218,23 +218,34 @@ function clause decode imm : bits(12) @ rs1 : regbits @ 0b100 @ rd : regbits @ 0
 function clause decode imm : bits(12) @ rs1 : regbits @ 0b101 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  HALF,   false, false))
 function clause decode imm : bits(12) @ rs1 : regbits @ 0b110 @ rd : regbits @ 0b0000011 = Some(LOAD(imm, rs1, rd, true,  WORD,   false, false))
 
-function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
-    let addr : xlenbits = X(rs1) + EXTS(imm) in
-    let result : xlenbits = if is_unsigned then
-        match width {
-	  BYTE   => EXTZ(mem_read(addr, 1, aq, rl, false)),
-	  HALF   => EXTZ(mem_read(addr, 2, aq, rl, false)),
-	  WORD   => EXTZ(mem_read(addr, 4, aq, rl, false)),
-	  DOUBLE => mem_read(addr, 8, aq, rl, false)
+val extend_value : forall 'n, 0 < 'n <= 8. (bool, MemoryOpResult(bits(8 * 'n))) -> MemoryOpResult(xlenbits)
+function extend_value(is_unsigned, value) = match (value) {
+  MemValue(v)     => MemValue(if is_unsigned then EXTZ(v) else EXTS(v) : xlenbits),
+  MemException(e) => MemException(e)
+}
+
+val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> option(xlenbits) effect {escape, rreg, wreg}
+function process_load(rd, addr, value, is_unsigned) =
+  match (extend_value(is_unsigned, value)) {
+    MemValue(result) => { X(rd) = result;
+                          Some(result) },
+    MemException(e)  =>
+        { let t : sync_exception = struct { trap    = e,
+                                            excinfo = Some(addr) } in
+          nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC);
+          None()
         }
-      else
-        match width {
-	  BYTE   => EXTS(mem_read(addr, 1, aq, rl, false)),
-	  HALF   => EXTS(mem_read(addr, 2, aq, rl, false)),
-	  WORD   => EXTS(mem_read(addr, 4, aq, rl, false)),
-	  DOUBLE => mem_read(addr, 8, aq, rl, false)
-        } in
-    X(rd) = result
+  }
+
+function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
+    let addr  : xlenbits = X(rs1) + EXTS(imm) in
+    let _ : option(xlenbits) = match width {
+      BYTE   => process_load(rd, addr, mem_read(addr, 1, aq, rl, false), is_unsigned),
+      HALF   => process_load(rd, addr, mem_read(addr, 2, aq, rl, false), is_unsigned),
+      WORD   => process_load(rd, addr, mem_read(addr, 4, aq, rl, false), is_unsigned),
+      DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, false), is_unsigned)
+    } in
+    ()
 
 /* FIXME: aq/rl are getting dropped */
 function clause print_insn (LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) =
@@ -551,15 +562,16 @@ union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits)
 function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b010 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, WORD, rd))
 function clause decode 0b00010 @ [aq] @ [rl] @ 0b00000 @ rs1 : regbits @ 0b011 @ rd : regbits @ 0b0101111 = Some(LOADRES(aq, rl, rs1, DOUBLE, rd))
 
+val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit
+
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
   let addr : xlenbits = X(rs1) in
-  let result : xlenbits =
-      match width {
-	WORD   => EXTS(mem_read(addr, 4, aq, rl, true)),
-	DOUBLE => mem_read(addr, 8, aq, rl, true),
-	_      => internal_error("LOADRES expected WORD or DOUBLE")
-      } in
-  X(rd) = result
+  let _ : option(xlenbits) = match width {
+    WORD   => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false),
+    DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, true), false),
+    _      => internal_error("LOADRES expected WORD or DOUBLE")
+  } in
+  ()
 
 /* FIXME */
 function clause print_insn (LOADRES(aq, rl, rs1, width, rd)) =
@@ -638,35 +650,44 @@ function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
     _      => internal_error ("AMO expected WORD or DOUBLE")
   };
 
-  loaded : xlenbits =
+  /* FIXME: this is incorrect! It could update rd even if the
+     mem_write below fails.  This will be fixed once we support
+     mem_write actually failing, and then do the write before the
+     register update.
+   */
+  value : option(xlenbits) =
     match width {
-      WORD   => EXTS(mem_read(addr, 4, aq, aq & rl, true)),
-      DOUBLE => mem_read(addr, 8, aq, aq & rl, true),
+      WORD   => process_load(rd, addr, mem_read(addr, 4, aq, aq & rl, true), false),
+      DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, aq & rl, true), false),
       _      => internal_error ("AMO expected WORD or DOUBLE")
     };
-  X(rd) = loaded;
-
-  rs2_val : xlenbits = X(rs2);
-  result : xlenbits =
-    match op {
-      AMOSWAP => rs2_val,
-      AMOADD  => rs2_val + loaded,
-      AMOXOR  => rs2_val ^ loaded,
-      AMOAND  => rs2_val & loaded,
-      AMOOR   => rs2_val | loaded,
-
-      /* Have to convert number to vector here. Check this */
-      AMOMIN  => vector64(min(signed(rs2_val),   signed(loaded))),
-      AMOMAX  => vector64(max(signed(rs2_val),   signed(loaded))),
-      AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))),
-      AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded)))
-    };
 
-  match width {
-    WORD   => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
-    DOUBLE => mem_write_value(addr, 8, result,        aq & rl, rl, true),
-    _      => internal_error("AMO expected WORD or DOUBLE")
-  };
+  match (value) {
+    None() => (),
+    Some(loaded) => {
+      rs2_val : xlenbits = X(rs2);
+      result : xlenbits =
+        match op {
+          AMOSWAP => rs2_val,
+          AMOADD  => rs2_val + loaded,
+          AMOXOR  => rs2_val ^ loaded,
+          AMOAND  => rs2_val & loaded,
+          AMOOR   => rs2_val | loaded,
+
+          /* Have to convert number to vector here. Check this */
+          AMOMIN  => vector64(min(signed(rs2_val),   signed(loaded))),
+          AMOMAX  => vector64(max(signed(rs2_val),   signed(loaded))),
+          AMOMINU => vector64(min(unsigned(rs2_val), unsigned(loaded))),
+          AMOMAXU => vector64(max(unsigned(rs2_val), unsigned(loaded)))
+        };
+
+        match width {
+          WORD   => mem_write_value(addr, 4, result[31..0], aq & rl, rl, true),
+          DOUBLE => mem_write_value(addr, 8, result,        aq & rl, rl, true),
+          _      => internal_error("AMO expected WORD or DOUBLE")
+        }
+    }
+  }
 }
 
 function clause print_insn (AMO(op, aq, rl, rs2, rs1, width, rd)) =
@@ -788,7 +809,7 @@ function clause execute CSR(csr, rs1, rd, is_imm, op) =
     _      => if is_imm then unsigned(rs1_val) != 0 else unsigned(rs1) != 0
   } in
   if ~ (check_CSR(csr, cur_privilege, isWrite)) then {
-    let instr : xlenbits = EXTZ(__RISCV_read(PC, 4));
+    let instr : xlenbits = cur_inst;
     let t : sync_exception =
     struct { trap = E_Illegal_Instr,
              excinfo = Some (instr) } in
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 5ec665e8..87d7e41a 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -1,28 +1,44 @@
 /* memory */
 
+/* TODO: remove this when unused */
 function check_alignment (addr : xlenbits, width : atom('n)) -> forall 'n. unit =
   if unsigned(addr) % width != 0 then throw Error_misaligned_access() else ()
 
-val MEMr                         : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_acquire                 : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_strong_acquire          : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_reserved                : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_reserved_acquire        : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
-val MEMr_reserved_strong_acquire : forall 'n. (xlenbits, atom('n)) -> bits(8 * 'n) effect {rmem}
+union MemoryOpResult ('a : Type) = {
+  MemValue : 'a,
+  MemException: ExceptionType
+}
 
-function MEMr                         (addr, width) = __RISCV_read(addr, width)
-function MEMr_acquire                 (addr, width) = __RISCV_read(addr, width)
-function MEMr_strong_acquire          (addr, width) = __RISCV_read(addr, width)
-function MEMr_reserved                (addr, width) = __RISCV_read(addr, width)
-function MEMr_reserved_acquire        (addr, width) = __RISCV_read(addr, width)
-function MEMr_reserved_strong_acquire (addr, width) = __RISCV_read(addr, width)
+function is_aligned_addr (addr : xlenbits, width : atom('n)) -> forall 'n. bool =
+  unsigned(addr) % width != 0
 
-val mem_read : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> bits(8 * 'n) effect {rmem, escape}
+function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n. MemoryOpResult(bits(8 * 'n)) =
+  match (t, __RISCV_read(addr, width)) {
+    (Instruction, None()) => MemException(E_Fetch_Access_Fault),
+    (Data, None())        => MemException(E_Load_Access_Fault),
+    (_, Some(v))          => MemValue(v)
+  }
 
-function mem_read (addr, width, aq, rl, res) = {
-  if aq | res then check_alignment(addr, width);
+val MEMr                         : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
+val MEMr_acquire                 : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
+val MEMr_strong_acquire          : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
+val MEMr_reserved                : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
+val MEMr_reserved_acquire        : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
+val MEMr_reserved_strong_acquire : forall 'n. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem}
 
-  match (aq, rl, res) {
+function MEMr                         (addr, width) = checked_mem_read(Data, addr, width)
+function MEMr_acquire                 (addr, width) = checked_mem_read(Data, addr, width)
+function MEMr_strong_acquire          (addr, width) = checked_mem_read(Data, addr, width)
+function MEMr_reserved                (addr, width) = checked_mem_read(Data, addr, width)
+function MEMr_reserved_acquire        (addr, width) = checked_mem_read(Data, addr, width)
+function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width)
+
+val mem_read : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, escape}
+
+function mem_read (addr, width, aq, rl, res) = {
+  if (aq | res) & (~ (is_aligned_addr(addr, width)))
+  then MemException(E_Load_Addr_Align)
+  else match (aq, rl, res) {
     (false, false, false) => MEMr(addr, width),
     (true,  false, false) => MEMr_acquire(addr, width),
     (false, false, true)  => MEMr_reserved(addr, width),
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index ea80d640..fbba53af 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -2,6 +2,10 @@
 
 register cur_privilege : Privilege
 
+/* current instruction bits, used for illegal instruction exceptions */
+
+register cur_inst : xlenbits
+
 /* M-mode registers */
 
 bitfield Misa : bits(64) = {