mc: Verify rmi version

This harness verifies RMI_VERSION's behaviors using model checking. Usage) (in islet/model-checking) $ RMI_TARGET=rmi_version make verify Signed-off-by: Changho Choi <ch754.choi@samsung.com>
islet-project · Oct 8, 2024 · 9fc89c0 · 9fc89c0
1 parent 1900464
commit 9fc89c0
Show file tree

Hide file tree

Showing 8 changed files with 44 additions and 1 deletion.
diff --git a/doc/getting-started/verification.md b/doc/getting-started/verification.md
@@ -15,6 +15,7 @@ the conformance of the two systems written in different languages.
 rmi_features
 rmi_granule_delegate
 rmi_granule_undelegate
+rmi_version
 ```
 
 ## Verifying Islet

diff --git a/model-checking/Cargo.toml b/model-checking/Cargo.toml
@@ -9,6 +9,7 @@ edition = "2021"
 mc_rmi_features = ["islet_rmm/mc_rmi_features"]
 mc_rmi_granule_delegate = ["islet_rmm/mc_rmi_granule_delegate"]
 mc_rmi_granule_undelegate = ["islet_rmm/mc_rmi_granule_undelegate"]
+mc_rmi_version = ["islet_rmm/mc_rmi_version"]
 
 [dependencies]
 islet_rmm = { path = "../rmm" }
diff --git a/model-checking/Makefile b/model-checking/Makefile
@@ -11,7 +11,8 @@ RMI_TARGET ?= rmi_features
 ALLOWED_RMI_TARGET = \
 	rmi_features \
 	rmi_granule_delegate \
-	rmi_granule_undelegate
+	rmi_granule_undelegate \
+	rmi_version
 
 ifeq ("$(filter $(RMI_TARGET), $(ALLOWED_RMI_TARGET))", "")
     $(error Invalid RMI_TARGET. Choose one of the following: $(ALLOWED_RMI_TARGET))

diff --git a/model-checking/src/lib.rs b/model-checking/src/lib.rs
@@ -5,3 +5,5 @@ mod rmi_features;
 mod rmi_granule_delegate;
 #[cfg(feature = "mc_rmi_granule_undelegate")]
 mod rmi_granule_undelegate;
+#[cfg(feature = "mc_rmi_version")]
+mod rmi_version;
diff --git a/model-checking/src/rmi_version.rs b/model-checking/src/rmi_version.rs
@@ -0,0 +1,33 @@
+use islet_rmm::monitor::Monitor;
+use islet_rmm::rmi;
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn verify_version() {
+    // Initialize registers (symbolic input)
+    let regs: [usize; 8] = kani::any();
+    kani::assume(regs[0] == rmi::VERSION);
+
+    // Pre-conditions
+    let no_failures_pre = true;
+
+    // Execute command and read the result.
+    let out = Monitor::new().run(regs);
+    let result = out[0];
+    let lower = out[1];
+    let higher = out[2];
+
+    // Result assertion
+    let prop_result_ante = no_failures_pre;
+
+    kani::cover!();
+    if prop_result_ante {
+        let prop_result_cons = (lower == (rmi::ABI_MAJOR_VERSION << 16) | rmi::ABI_MINOR_VERSION)
+            && (higher == (rmi::ABI_MAJOR_VERSION << 16) | rmi::ABI_MINOR_VERSION);
+
+        kani::cover!();
+        assert!(prop_result_cons);
+    }
+
+    kani::cover!();
+}
diff --git a/rmm/Cargo.toml b/rmm/Cargo.toml
@@ -42,3 +42,4 @@ gst_page_table = []
 mc_rmi_features = []
 mc_rmi_granule_delegate = []
 mc_rmi_granule_undelegate = []
+mc_rmi_version = []
diff --git a/rmm/src/event/mainloop.rs b/rmm/src/event/mainloop.rs
@@ -44,6 +44,8 @@ impl Mainloop {
             feature = "mc_rmi_granule_undelegate"
         ))]
         rmi::gpt::set_event_handler(self);
+        #[cfg(feature = "mc_rmi_version")]
+        rmi::version::set_event_handler(self);
     }
 
     #[cfg(not(kani))]

diff --git a/rmm/src/event/mod.rs b/rmm/src/event/mod.rs
@@ -108,6 +108,8 @@ impl Context {
                 feature = "mc_rmi_granule_undelegate"
             ))]
             assert!(ret_len == 1);
+            #[cfg(feature = "mc_rmi_version")]
+            assert!(ret_len == 3);
         }
         result[..ret_len].copy_from_slice(&self.ret[..]);
         result