Initial support for faults of writes to physical addresses.

4 files changed, 127 insertions, 105 deletions

diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 24e856e7..d667573e 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -286,8 +286,11 @@ overload max = {max_nat, max_int}
 val __WriteRAM = "write_ram" : forall 'n 'm.
   (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> unit effect {wmv}
 
-val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> unit effect {wmv}
-function __RISCV_write (addr, width, data) = __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data)
+val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmv}
+function __RISCV_write (addr, width, data) = {
+  __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data);
+  true
+}
 
 val __TraceMemoryWrite : forall 'n 'm.
   (atom('n), bits('m), bits(8 * 'n)) -> unit
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 550ccfee..9c61e65f 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -224,28 +224,21 @@ function extend_value(is_unsigned, value) = match (value) {
   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}
+val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit 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()
-        }
+    MemValue(result) => X(rd) = result,
+    MemException(e)  => handle_mem_exception(addr, e)
   }
 
 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 {
+    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)) =
@@ -270,19 +263,27 @@ function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b010 @
 function clause decode imm7 : bits(7) @ rs2 : regbits @ rs1 : regbits @ 0b011 @ imm5 : bits(5) @ 0b0100011 = Some(STORE(imm7 @ imm5, rs2, rs1, DOUBLE, false, false))
 
 function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) =
-    let addr : xlenbits = X(rs1) + EXTS(imm) in {
-      match width {
-	BYTE   => mem_write_ea(addr, 1, aq, rl, false),
-	HALF   => mem_write_ea(addr, 2, aq, rl, false),
-	WORD   => mem_write_ea(addr, 4, aq, rl, false),
-	DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
-      };
-      let rs2_val = X(rs2) in
-      match width {
-	BYTE   => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
-	HALF   => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
-	WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
-	DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
+    let addr : xlenbits = X(rs1) + EXTS(imm) in
+    let eares : MemoryOpResult(unit) = match width {
+      BYTE   => mem_write_ea(addr, 1, aq, rl, false),
+      HALF   => mem_write_ea(addr, 2, aq, rl, false),
+      WORD   => mem_write_ea(addr, 4, aq, rl, false),
+      DOUBLE => mem_write_ea(addr, 8, aq, rl, false)
+    } in
+    match (eares) {
+      MemException(e) => handle_mem_exception(addr, e),
+      MemValue(_) => {
+        let rs2_val = X(rs2) in
+        let res : MemoryOpResult(unit) = match width {
+          BYTE   => mem_write_value(addr, 1, rs2_val[7..0],  aq, rl, false),
+          HALF   => mem_write_value(addr, 2, rs2_val[15..0], aq, rl, false),
+          WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, false),
+          DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, false)
+        } in
+        match (res) {
+          MemValue(_)     => (),
+          MemException(e) => handle_mem_exception(addr, e)
+        }
       }
     }
 
@@ -566,12 +567,11 @@ val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult
 
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
   let addr : xlenbits = X(rs1) in
-  let _ : option(xlenbits) = match width {
+  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)) =
@@ -595,18 +595,27 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
 
   if status == 0b1 then () else {
     addr : xlenbits = X(rs1);
-    match width {
+    let eares : MemoryOpResult(unit) = match width {
       WORD   => mem_write_ea(addr, 4, aq, rl, true),
       DOUBLE => mem_write_ea(addr, 8, aq, rl, true),
       _      => internal_error("STORECON expected word or double")
     };
-    rs2_val = X(rs2);
-    match width {
-      WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
-      DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
-      _      => internal_error("STORECON expected word or double")
-    };
-  };
+    match (eares) {
+      MemException(e)  => handle_mem_exception(addr, e),
+      MemValue(_) => {
+        rs2_val = X(rs2);
+        let res : MemoryOpResult(unit) = match width {
+          WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
+          DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
+          _      => internal_error("STORECON expected word or double")
+        } in
+        match (res) {
+          MemValue(_)     => (),
+          MemException(e) => handle_mem_exception(addr, e)
+        }
+      }
+    }
+  }
 }
 
 /* FIXME */
@@ -644,48 +653,49 @@ function clause decode 0b11100 @ [aq] @ [rl] @ rs2 : regbits @ rs1 : regbits @ 0
 function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
   addr : xlenbits = X(rs1);
 
-  match width {
+  let eares : MemoryOpResult(unit) = match width {
     WORD   => mem_write_ea(addr, 4, aq & rl, rl, true),
     DOUBLE => mem_write_ea(addr, 8, aq & rl, rl, true),
     _      => internal_error ("AMO expected WORD or DOUBLE")
   };
-
-  /* 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   => 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")
-    };
-
-  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")
+  match (eares) {
+    MemException(e) => handle_mem_exception(addr, e),
+    MemValue(_) => {
+      let rval : MemoryOpResult(xlenbits) = match width {
+        WORD   => extend_value(false, mem_read(addr, 4, aq, aq & rl, true)),
+        DOUBLE => extend_value(false, mem_read(addr, 8, aq, aq & rl, true)),
+      _        => internal_error ("AMO expected WORD or DOUBLE")
+      };
+      match (rval) {
+        MemException(e) => handle_mem_exception(addr, e),
+        MemValue(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)))
+            };
+
+          let wval : MemoryOpResult(unit) = 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 (wval) {
+            MemValue(_) => X(rd) = loaded,
+            MemException(e) => handle_mem_exception(addr, e)
+          }
         }
+      }
     }
   }
 }
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 87d7e41a..67c35bce 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -1,9 +1,5 @@
 /* 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 ()
-
 union MemoryOpResult ('a : Type) = {
   MemValue : 'a,
   MemException: ExceptionType
@@ -63,43 +59,49 @@ val MEMea_conditional_release = {ocaml: "memea", lem: "MEMea_conditional_release
 val MEMea_conditional_strong_release = {ocaml: "memea", lem: "MEMea_conditional_strong_release"} : forall 'n.
   (xlenbits, atom('n)) -> unit effect {eamem}
 
-val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> unit effect {eamem, escape}
+val mem_write_ea : forall 'n. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(unit) effect {eamem, escape}
 
 function mem_write_ea (addr, width, aq, rl, con) = {
-  if rl | con then check_alignment(addr, width);
-
-  match (aq, rl, con) {
-    (false, false, false) => MEMea(addr, width),
-    (false, true,  false) => MEMea_release(addr, width),
-    (false, false, true)  => MEMea_conditional(addr, width),
-    (false, true , true)  => MEMea_conditional_release(addr, width),
+  if (rl | con) & (~ (is_aligned_addr(addr, width)))
+  then MemException(E_SAMO_Addr_Align)
+  else match (aq, rl, con) {
+    (false, false, false) => MemValue(MEMea(addr, width)),
+    (false, true,  false) => MemValue(MEMea_release(addr, width)),
+    (false, false, true)  => MemValue(MEMea_conditional(addr, width)),
+    (false, true , true)  => MemValue(MEMea_conditional_release(addr, width)),
     (true,  false, false) => throw(Error_not_implemented("store.aq")),
-    (true,  true,  false) => MEMea_strong_release(addr, width),
+    (true,  true,  false) => MemValue(MEMea_strong_release(addr, width)),
     (true,  false, true)  => throw(Error_not_implemented("sc.aq")),
-    (true,  true , true)  => MEMea_conditional_strong_release(addr, width)
+    (true,  true , true)  => MemValue(MEMea_conditional_strong_release(addr, width))
   }
 }
 
-val MEMval                            : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_release                    : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_strong_release             : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_conditional                : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_conditional_release        : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
-val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> unit effect {wmv}
+function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n. MemoryOpResult(unit) =
+  if (__RISCV_write(addr, width, data))
+  then MemValue(())
+  else MemException(E_SAMO_Access_Fault)
 
-function MEMval                            (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_release                    (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_strong_release             (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_conditional                (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_conditional_release        (addr, width, data) = __RISCV_write(addr, width, data)
-function MEMval_conditional_strong_release (addr, width, data) = __RISCV_write(addr, width, data)
+val MEMval                            : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
+val MEMval_release                    : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
+val MEMval_strong_release             : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
+val MEMval_conditional                : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
+val MEMval_conditional_release        : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
+val MEMval_conditional_strong_release : forall 'n. (xlenbits, atom('n), bits(8 * 'n)) -> MemoryOpResult(unit) effect {wmv}
 
-val mem_write_value : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> unit effect {wmv, escape}
+function MEMval                            (addr, width, data) = checked_mem_write(addr, width, data)
+function MEMval_release                    (addr, width, data) = checked_mem_write(addr, width, data)
+function MEMval_strong_release             (addr, width, data) = checked_mem_write(addr, width, data)
+function MEMval_conditional                (addr, width, data) = checked_mem_write(addr, width, data)
+function MEMval_conditional_release        (addr, width, data) = checked_mem_write(addr, width, data)
+function MEMval_conditional_strong_release (addr, width, data) = checked_mem_write(addr, width, data)
 
-function mem_write_value (addr, width, value, aq, rl, con) = {
-  if rl | con then check_alignment(addr, width);
 
-  match (aq, rl, con) {
+val mem_write_value : forall 'n. (xlenbits, atom('n), bits(8 * 'n), bool, bool, bool) -> MemoryOpResult(unit) effect {wmv, escape}
+
+function mem_write_value (addr, width, value, aq, rl, con) = {
+  if (rl | con) & (~ (is_aligned_addr(addr, width)))
+  then MemException(E_SAMO_Addr_Align)
+  else match (aq, rl, con) {
     (false, false, false) => MEMval(addr, width, value),
     (false, true,  false) => MEMval_release(addr, width, value),
     (false, false, true)  => MEMval_conditional(addr, width, value),
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index fbba53af..ab15604b 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -675,6 +675,13 @@ function handle_exception_ctl(cur_priv : Privilege, ctl : ctl_result,
     }
   }
 
+function handle_mem_exception(addr : xlenbits, e : ExceptionType) -> unit = {
+  let t : sync_exception = struct { trap    = e,
+                                    excinfo = Some(addr) } in
+  nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+}
+
+
 function init_sys() -> unit = {
   cur_privilege = Machine;