Added ecall/mret and exception support.

4 files changed, 316 insertions, 2 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index fabaaafc..00451f6f 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -1,4 +1,4 @@
-SAIL_SRCS = prelude.sail riscv_types.sail riscv.sail
+SAIL_SRCS = prelude.sail riscv_types.sail riscv_sys.sail riscv.sail
 SAIL_DIR ?= $(realpath ..)
 
 export SAIL_DIR
diff --git a/riscv/prelude.sail b/riscv/prelude.sail
index 427da759..69fc1017 100644
--- a/riscv/prelude.sail
+++ b/riscv/prelude.sail
@@ -331,6 +331,7 @@ union exception = {
   Error_not_implemented : string,
   Error_misaligned_access,
   Error_EBREAK,
+  Error_internal_error
 }
 
 val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
@@ -373,3 +374,12 @@ val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits
 val vector64 : int -> bits(64)
 
 function vector64 n = __raw_GetSlice_int(64, n, 0)
+
+val vector_update_subrange_dec = "update_subrange" : forall 'n 'm 'o.
+  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
+
+val vector_update_subrange_inc = "update_subrange" : forall 'n 'm 'o.
+  (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
+
+overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
+
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index beb29327..76d98dcf 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -275,7 +275,22 @@ union clause ast = ECALL
 
 function clause decode 0b000000000000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(ECALL)
 
-function clause execute ECALL = not_implemented("ECALL is not implemented")
+function clause execute ECALL =
+  let t : sync_exception =
+    struct { trap = match (cur_privilege) {
+                      USER => User_ECall,
+		      MACHINE => Machine_ECall
+		    },
+             badaddr = (None : option(regval)) } in
+  nextPC = handle_exception_ctl(cur_privilege, CTL_TRAP(t), PC)
+
+/* ****************************************************************** */
+union clause ast = MRET
+
+function clause decode 0b0011000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 = Some(MRET)
+
+function clause execute MRET =
+  nextPC = handle_exception_ctl(cur_privilege, CTL_MRET, PC)
 
 /* ****************************************************************** */
 union clause ast = EBREAK
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
new file mode 100644
index 00000000..84002ed7
--- /dev/null
+++ b/riscv/riscv_sys.sail
@@ -0,0 +1,289 @@
+/* exception codes */
+
+enum Interrupts = {
+  UserSWIntr,
+  SupervisorSWIntr,
+  ReservedIntr0,
+  MachineSWIntr,
+
+  UserTimerIntr,
+  SupervisorTimerIntr,
+  ReservedIntr1,
+  MachineTimerIntr,
+
+  UserExternalIntr,
+  SupervisorExternalIntr,
+  ReservedIntr2,
+  MachineExternalIntr
+}
+
+enum ExceptionCode = {
+  Misaligned_Fetch,
+  Fetch_Access,
+  Illegal_Instr,
+  Breakpoint,
+  Misaligned_Load,
+
+  Load_Access,
+  Misaligned_Store,
+  Store_Access,
+
+  User_ECall,
+  Supervisor_ECall,
+  ReservedExc0,
+  Machine_ECall,
+
+  Fetch_PageFault,
+  Load_PageFault,
+  ReservedExc1,
+  Store_PageFault
+}
+
+/* machine mode registers */
+
+/* FIXME: currently we have only those used by riscv-tests. */
+
+bitfield Mstatus : bits(64) = {
+  SD   : 63,
+
+  SXL  : 35 .. 34,
+  UXL  : 33 .. 32,
+
+  TSR  : 22,
+  TW   : 21,
+  TVM  : 20,
+  MXR  : 19,
+  SUM  : 18,
+  MPRV : 17,
+
+  XS   : 16 .. 15,
+  FS   : 14 .. 13,
+
+  MPP  : 12 .. 11,
+  SPP  : 8,
+
+  MPIE : 7,
+  SPIE : 5,
+  UPIE : 4,
+
+  MIE  : 3,
+  SIE  : 1,
+  UIE  : 0
+}
+register mstatus : Mstatus
+
+bitfield Mip : bits(64) = {
+  MEIP : 11,
+  SEIP : 9,
+  UEIP : 8,
+
+  MTIP : 7,
+  STIP : 5,
+  UTIP : 4,
+
+  MSIP : 3,
+  SSIP : 1,
+  USIP : 0,
+
+}
+register mip : Mip
+
+bitfield Mie : bits(64) = {
+  MEIE : 11,
+  SEIE : 9,
+  UEIE : 8,
+
+  MTIE : 7,
+  STIE : 5,
+  UTIE : 4,
+
+  MSIE : 3,
+  SSIE : 1,
+  USIE : 0,
+
+}
+register mie : Mie
+
+bitfield Mideleg : bits(64) = {
+  MEID : 6,
+  SEID : 5,
+  UEID : 4,
+
+  MTID : 6,
+  STID : 5,
+  UTID : 4,
+
+  MSID : 3,
+  SSID : 1,
+  USID : 0
+}
+register mideleg : Mideleg
+
+bitfield Medeleg : bits(64) = {
+  STORE_PAGE_FAULT  : 15,
+  LOAD_PAGE_FAULT   : 13,
+  FETCH_PAGE_FAULT  : 12,
+  MACHINE_ECALL     : 10,
+  SUPERVISOR_ECALL  : 9,
+  USER_ECALL        : 8,
+  STORE_ACCESS      : 7,
+  MISALIGNED_STORE  : 6,
+  LOAD_ACCESS       : 5,
+  MISALIGNED_LOAD   : 4,
+  BREAKPOINT        : 3,
+  ILLEGAL_INSTR     : 2,
+  FETCH_ACCESS      : 1,
+  MISALIGNED_FETCH  : 0
+}
+register medeleg : Medeleg
+
+/* exception registers */
+register mepc : regval
+register mtval : regval
+register mtvec : regval
+register mscratch : regval
+
+/* other registers */
+
+register pmpaddr0 : regval
+register pmpcfg0 : regval
+/* TODO: this should be readonly, and always 0 for now */
+register mhartid : regval
+
+/* instruction control flow */
+
+struct sync_exception = {
+  trap : ExceptionCode,
+  badaddr : option(regval)
+}
+
+union ctl_result = {
+  CTL_TRAP : sync_exception,
+/* TODO:
+  CTL_URET,
+  CTL_SRET,
+*/
+  CTL_MRET
+}
+
+/* privilege level */
+
+union privilege = {
+  MACHINE,
+  USER
+}
+register cur_privilege : privilege
+
+function priv_to_bits(p : privilege) -> bits(2) =
+  match (p) {
+    USER    => 0b00,
+    MACHINE => 0b11
+  }
+function bits_to_priv(b : bits(2)) -> privilege =
+  match (b) {
+    0b00    => USER,
+    0b11    => MACHINE
+  }
+
+/* handle exceptional ctl flow by updating nextPC */
+
+function handle_exception_ctl(cur_priv : privilege, ctl : ctl_result,
+                              pc: regval) -> regval =
+  /* TODO: check delegation */
+  match (cur_priv, ctl) {
+    (_, CTL_TRAP(e)) => {
+      mepc            = pc;
+      mcause          = e.trap;
+
+      mstatus->MPIE() = mstatus.MIE();
+      mstatus->MIE()  = false;
+      mstatus->MPP()  = priv_to_bits(cur_priv);
+      cur_privilege   = MACHINE;
+
+      match (e.trap) {
+        Misaligned_Fetch => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+        Fetch_Access => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+        Illegal_Instr => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+
+        Breakpoint => not_implemented("breakpoint"),
+
+        Misaligned_Load => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+        Load_Access => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+        Misaligned_Store => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+        Store_Access => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+
+        User_ECall => {
+          mtval  = EXTZ(0b0)
+        },
+        Supervisor_ECall => {
+          mtval  = EXTZ(0b0)
+        },
+        Machine_ECall => {
+          mtval  = EXTZ(0b0)
+        },
+
+        Fetch_PageFault => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+        Load_PageFault => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        },
+        Store_PageFault => {
+          match (e.badaddr) {
+            Some(a) => mtval = a,
+            None    => throw(Error_internal_error)
+          }
+        }
+      };
+      /* TODO: make register read explicit */
+      mtvec
+    },
+    (_, CTL_MRET) => {
+      mstatus->MIE()  = mstatus.MPIE();
+      mstatus->MPIE() = true;
+      cur_privilege   = bits_to_priv(mstatus.MPP());
+      mstatus->MPP()  = priv_to_bits(USER);
+      mepc
+    }
+  }