finish scattering the termination module and update references to it

Author: Ptival

doc/ReadingGuide.md

@@ -236,10 +236,7 @@ Vector (`V`) and cryptography (`Zk*`) extensions.
 
 ### Other modules
 
-The `termination` module specifies
-[functions](../model/termination/termination.sail) that are used to prove
-loop termination for theorem prover backends of Sail. The
-`unit_tests` module collects Sail unit tests for the specification.
+The `unit_tests` module collects Sail unit tests for the specification.
 The `main` module provides a [`main()`](../model/main/main.sail)
 function that is used in other Sail backends.
 

model/CMakeLists.txt

@@ -32,8 +32,6 @@ execute_process(
         ${SAIL_BIN}
         ${project_file}
         --require-version ${SAIL_REQUIRED_VER}
-        # include termination.sail in the list of dependencies
-        --variable "TERMINATION_FILE = true"
         --all-modules
         --list-files
     OUTPUT_VARIABLE sail_list_files
@@ -372,7 +370,6 @@ foreach (xlen IN ITEMS 32 64)
             --config ${config_file}
             # Input files.
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
     add_custom_command(
@@ -438,7 +435,6 @@ foreach (xlen IN ITEMS 32 64)
             ${lean_sail_common}
             ${lean_sail_default}
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
     add_custom_command(
@@ -457,7 +453,6 @@ foreach (xlen IN ITEMS 32 64)
             ${lean_sail_common}
             ${lean_sail_executable}
             ${SAIL_MODULES}
-            --variable "TERMINATION_FILE = true"
             ${project_file}
     )
 

model/core/extensions.sail

@@ -19,14 +19,28 @@ scattered mapping extensionName
 val hartSupports : extension -> bool
 scattered function hartSupports
 
+function hartSupports_measure(ext : extension) -> int =
+  match ext {
+    Ext_D => 1,
+    Ext_V => 1,
+    Ext_Zvkn => 1,
+    Ext_Zvks => 1,
+    Ext_C => 2,
+    Ext_Zvknc => 2,
+    Ext_Zvkng => 2,
+    Ext_Zvksc => 2,
+    Ext_Zvksg => 2,
+    _ => 0,
+  }
+
+termination_measure hartSupports(ext) = hartSupports_measure(ext)
+
 // Function used to determine if an extension is currently enabled in the model.
 // This means an extension is supported, *and* any necessary bits are set in the
 // relevant CSRs (misa, mstatus, etc.) to enable its use. It is possible for some
 // extensions to be supported in hardware, but temporarily disabled via a CSR, in
 // which case this function should return false.
-// Note: when adding a new extension, adjust the associated termination measure
-// in the file termination.sail, as explained in the comment in
-// that file.
+// Note: when adding a new extension, adjust the `currentlyEnabled_measure` below.
 val currentlyEnabled : extension -> bool
 scattered function currentlyEnabled
 
@@ -473,9 +487,9 @@ function currentlyEnabled_measure(ext : extension) -> int =
     Ext_F => 1,
     Ext_M => 1,
     Ext_S => 1,
-    Ext_V => 1,
-    Ext_H => 4,
     Ext_Smcntrpmf => 3,
+    Ext_Sscofpmf => 3,
+    Ext_Sv39 => 3,
     Ext_Zabha => 3,
     Ext_Zacas => 3,
     Ext_Zcb => 3,
@@ -484,9 +498,20 @@ function currentlyEnabled_measure(ext : extension) -> int =
     Ext_Zcmop => 3,
     Ext_Zfhmin => 3,
     Ext_Zhinx => 3,
+    Ext_Zicfilp => 3,
+    Ext_Zve32x => 3,
     Ext_Zvkb => 3,
-    Ext_Sscofpmf => 3,
+    Ext_H => 4,
+    Ext_Svrsw60t59b => 4,
     Ext_Zhinxmin => 4,
+    Ext_Zve32f => 4,
+    Ext_Zve64x => 4,
+    Ext_Zve64f => 5,
+    Ext_Zvfh => 5,
+    Ext_Zve64d => 6,
+    Ext_Zvfhmin => 6,
+    Ext_Zvl128b => 6,
+    Ext_V => 7,
     _ => 2
   }
 

model/core/sys_regs.sail

@@ -144,6 +144,8 @@ function virtual_memory_supported() -> bool = {
   currentlyEnabled(Ext_Sv32) | currentlyEnabled(Ext_Sv39) | currentlyEnabled(Ext_Sv48) | currentlyEnabled(Ext_Sv57)
 }
 
+termination_measure virtual_memory_supported(_) = 3
+
 //
 // Illegal values legalized to least privileged mode supported.
 // Note: the only valid combinations of supported modes are M, M+U, M+S+U.

model/extensions/cfi/zicfilp_regs.sail

@@ -32,6 +32,8 @@ function get_xLPE(p : Privilege) -> bool =
     VirtualUser       => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"),
   }
 
+termination_measure get_xLPE(_) = 2
+
 function clause currentlyEnabled(Ext_Zicfilp) =
   currentlyEnabled(Ext_Zicsr) & hartSupports(Ext_Zicfilp) & get_xLPE(cur_privilege)
 

model/postlude/step.sail

@@ -288,3 +288,13 @@ function loop () : unit -> unit = {
     }
   }
 }
+
+// Termination measures for loops are not supported by the Lean backend, so they
+// should be guarded by this condition:
+$iftarget coq
+
+// The top-level loop isn't terminating, but we put a limit so that it can still
+// be included in the Coq output
+termination_measure loop while 100
+
+$endif

model/riscv.sail_project

@@ -1,4 +1,3 @@
-variable TERMINATION_FILE = false
 variable RMEM = false
 
 core {
@@ -466,18 +465,8 @@ postlude {
     postlude/model.sail
 }
 
-termination {
-  after postlude
-  requires core, sys, Zca, FD
-
-  files
-    if $TERMINATION_FILE then
-      termination/termination.sail
-    else []
-}
-
 unit_tests {
-  after termination
+  after postlude
   requires core, sys, exceptions, postlude
 
   files

model/sys/vmem_utils.sail

@@ -172,6 +172,8 @@ function vmem_read_addr(vaddr, offset, width, acc, aq, rl, res) = {
   Ok(data)
 }
 
+termination_measure vmem_read_addr repeat n
+
 val vmem_write_addr : forall 'width, is_mem_width('width).
   (virtaddr, int('width), bits(8 * 'width), AccessType(ext_access_type), bool, bool, bool)
   -> result(bool, ExecutionResult)
@@ -227,6 +229,8 @@ function vmem_write_addr(vaddr, width, data, acc, aq, rl, res) = {
   Ok(write_success)
 }
 
+termination_measure vmem_write_addr repeat n
+
 val vmem_read : forall 'width, is_mem_width('width).
   (regidx, xlenbits, int('width), AccessType(ext_access_type), bool, bool, bool)
   -> result(bits(8 * 'width), ExecutionResult)