Make use of extensionEnabled() instead of have*()

* Utilize extensionEnabled() instead of `haveZmmul()`, `haveUsrMode()`,
  `haveSupMode()`, `haveNExt()`, etc..
* Delete all unused  `have*` definitions of various extensions

model/riscv_fdext_control.sail

@@ -21,11 +21,14 @@ function clause extensionEnabled(Ext_F) = (misa[F] == 0b1) & (mstatus[FS] != 0b0
 enum clause extensions = Ext_D
 function clause extensionEnabled(Ext_D) = (misa[D] == 0b1) & (mstatus[FS] != 0b00) & sizeof(flen) >= 64
 
+enum clause extensions = Ext_Zfinx
+function clause extensionEnabled(Ext_Zfinx) = sys_enable_zfinx()
+
 /* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */
 
-function clause ext_is_CSR_defined (0x001, _) = extensionEnabled(Ext_F) | haveZfinx()
-function clause ext_is_CSR_defined (0x002, _) = extensionEnabled(Ext_F) | haveZfinx()
-function clause ext_is_CSR_defined (0x003, _) = extensionEnabled(Ext_F) | haveZfinx()
+function clause ext_is_CSR_defined (0x001, _) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
+function clause ext_is_CSR_defined (0x002, _) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
+function clause ext_is_CSR_defined (0x003, _) = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
 
 function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS]))
 function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM]))

model/riscv_insts_base.sail

@@ -664,8 +664,8 @@ mapping clause encdec = SRET()
 function clause execute SRET() = {
   let sret_illegal : bool = match cur_privilege {
     User       => true,
-    Supervisor => not(haveSupMode ()) | mstatus[TSR] == 0b1,
-    Machine    => not(haveSupMode ())
+    Supervisor => not(extensionEnabled(Ext_S)) | mstatus[TSR] == 0b1,
+    Machine    => not(extensionEnabled(Ext_S))
   };
   if   sret_illegal
   then { handle_illegal(); RETIRE_FAIL }

model/riscv_insts_dext.sail

@@ -224,13 +224,16 @@ function fle_D   (v1,       v2,        is_quiet) = {
 /* **************************************************************** */
 /* Helper functions for 'encdec()'                                  */
 
-function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | haveZdinx()
+enum clause extensions = Ext_Zdinx
+function clause extensionEnabled(Ext_Zdinx) = sys_enable_zfinx() & sizeof(flen) >= 64
+
+function haveDoubleFPU() -> bool = extensionEnabled(Ext_D) | extensionEnabled(Ext_Zdinx)
 
 /* RV32Zdinx requires even register pairs; can be omitted for code  */
 /* not used for RV32Zdinx (i.e. RV64-only or D-only).               */
 val validDoubleRegs : forall 'n, 'n > 0. (implicit('n), vector('n, dec, regidx)) -> bool
 function validDoubleRegs(n, regs) = {
-  if haveZdinx() & sizeof(xlen) == 32 then
+  if extensionEnabled(Ext_Zdinx) & sizeof(xlen) == 32 then
     foreach (i from 0 to (n - 1))
       if (regs[i][0] == bitone) then return false;
   true

model/riscv_insts_fext.sail

@@ -262,7 +262,7 @@ function fle_S   (v1,       v2,        is_quiet) = {
 /* **************************************************************** */
 /* Helper functions for 'encdec()'                                  */
 
-function haveSingleFPU() -> bool = extensionEnabled(Ext_F) | haveZfinx()
+function haveSingleFPU() -> bool = extensionEnabled(Ext_F) | extensionEnabled(Ext_Zfinx)
 
 /* ****************************************************************** */
 /* Floating-point loads                                               */

model/riscv_insts_next.sail

@@ -15,7 +15,7 @@ mapping clause encdec = URET()
   <-> 0b0000000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
 
 function clause execute URET() = {
-  if   not(haveUsrMode()) | not(sys_enable_next())
+  if   not(extensionEnabled(Ext_U)) | not(sys_enable_next())
   then handle_illegal()
   else if not(ext_check_xret_priv(User))
   then ext_fail_xret_priv()

model/riscv_insts_svinval.sail

@@ -6,11 +6,14 @@
 /*  SPDX-License-Identifier: BSD-2-Clause                                                */
 /*=======================================================================================*/
 
+enum clause extensions = Ext_Svinval
+function clause extensionEnabled(Ext_Svinval) = sys_enable_svinval()
+
 union clause ast = SINVAL_VMA : (regidx, regidx)
 
 mapping clause encdec =
-      SINVAL_VMA(rs1, rs2)                                                  if haveSvinval()
-  <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+      SINVAL_VMA(rs1, rs2)                                                  if extensionEnabled(Ext_Svinval)
+  <-> 0b0001011 @ rs2 : regidx @ rs1 : regidx @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)
 
 function clause execute SINVAL_VMA(rs1, rs2) = {
   execute(SFENCE_VMA(rs1, rs2))
@@ -24,8 +27,8 @@ mapping clause assembly = SINVAL_VMA(rs1, rs2)
 union clause ast = SFENCE_W_INVAL : unit
 
 mapping clause encdec =
-      SFENCE_W_INVAL()                                            if haveSvinval()
-  <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+      SFENCE_W_INVAL()                                            if extensionEnabled(Ext_Svinval)
+  <-> 0b0001100 @ 0b00000 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)
 
 function clause execute SFENCE_W_INVAL() = {
   if cur_privilege == User
@@ -40,8 +43,8 @@ mapping clause assembly = SFENCE_W_INVAL() <-> "sfence.w.inval"
 union clause ast = SFENCE_INVAL_IR : unit
 
 mapping clause encdec =
-      SFENCE_INVAL_IR()                                           if haveSvinval()
-  <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if haveSvinval()
+      SFENCE_INVAL_IR()                                           if extensionEnabled(Ext_Svinval)
+  <-> 0b0001100 @ 0b00001 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011 if extensionEnabled(Ext_Svinval)
 
 function clause execute SFENCE_INVAL_IR() = {
   if cur_privilege == User