[DRAFT] Support MMIO regions

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -13,7 +13,6 @@ use rustc_ast::{Attribute, LitKind};
 use rustc_middle::mir::{HasLocalDecls, Local};
 use rustc_middle::ty::{self, Instance};
 use std::collections::BTreeMap;
-use std::convert::TryInto;
 use std::iter::FromIterator;
 use tracing::{debug, info_span};
 
@@ -272,6 +271,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let mut harness = self.default_kanitool_proof();
         for attr in other_attributes.iter() {
             match attr.0.as_str() {
+                "mmio_region" => self.handle_kanitool_mmio_region(attr.1, &mut harness),
                 "unwind" => self.handle_kanitool_unwind(attr.1, &mut harness),
                 _ => {
                     self.tcx.sess.span_err(
@@ -297,16 +297,39 @@ impl<'tcx> GotocCtx<'tcx> {
             original_file: loc.filename().unwrap(),
             original_line: loc.line().unwrap().to_string(),
             unwind_value: None,
+            mmio_regions: vec![],
         }
     }
 
+    fn handle_kanitool_mmio_region(&mut self, attr: &Attribute, harness: &mut HarnessMetadata) {
+        let attr_args = attr.meta_item_list();
+        if let Some(attr_args) = attr_args {
+            if attr_args.len() == 2 {
+                if let (Some(start), Some(len)) = (attr_args[0].literal(), attr_args[1].literal()) {
+                    if let (LitKind::Int(start, ..), LitKind::Int(len, ..)) =
+                        (&start.kind, &len.kind)
+                    {
+                        harness.mmio_regions.push((*start, *len));
+                        return;
+                    }
+                }
+            }
+        }
+
+        // If we didn't successfully process, give an error message
+        self.tcx
+            .sess
+            .span_err(attr.span, "Expected exactly two integers are the argument to 'mmio_region'");
+    }
+
     /// Updates the proof harness with new unwind value
     fn handle_kanitool_unwind(&mut self, attr: &Attribute, harness: &mut HarnessMetadata) {
         // If some unwind value already exists, then the current unwind being handled is a duplicate
         if harness.unwind_value.is_some() {
             self.tcx.sess.span_err(attr.span, "Only one '#[kani::unwind]' allowed");
             return;
         }
+
         // Get Attribute value and if it's not none, assign it to the metadata
         match extract_integer_argument(attr) {
             None => {

kani-driver/src/call_cbmc.rs

@@ -95,12 +95,22 @@ impl KaniSession {
             args.push(unwind_value.to_string().into());
         }
 
+        if !harness_metadata.mmio_regions.is_empty() {
+            args.push("--mmio-regions".into());
+            let mmio_string = harness_metadata
+                .mmio_regions
+                .iter()
+                .map(|(s, l)| format!("{}:{}", s, l))
+                .collect::<Vec<String>>()
+                .join(",");
+            args.push(mmio_string.into());
+        }
+
         args.push("--slice-formula".into());
 
         args.extend(self.args.cbmc_args.iter().cloned());
 
         args.push(file.to_owned().into_os_string());
-
         Ok(args)
     }
 

kani-driver/src/metadata.rs

@@ -147,6 +147,7 @@ pub fn mock_proof_harness(name: &str, unwind_value: Option<u32>) -> HarnessMetad
         original_file: "<unknown>".into(),
         original_line: "<unknown>".into(),
         unwind_value,
+        mmio_regions: vec![],
     }
 }
 

kani_metadata/src/harness.rs

@@ -16,4 +16,6 @@ pub struct HarnessMetadata {
     pub original_line: String,
     /// Optional data to store unwind value
     pub unwind_value: Option<u32>,
+    /// Optional MMIO regions
+    pub mmio_regions: Vec<(u128, u128)>,
 }

library/kani_macros/src/lib.rs

@@ -73,3 +73,26 @@ pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
     result.extend(item);
     result
 }
+
+#[cfg(not(kani))]
+#[proc_macro_attribute]
+pub fn mmio_region(_attr: TokenStream, item: TokenStream) -> TokenStream {
+    // When the config is not kani, we should leave the function alone
+    item
+}
+
+/// Set Loop unwind limit for proof harnesses
+/// The attribute '#[kani::unwind(arg)]' can only be called alongside '#[kani::proof]'.
+/// arg - Takes in a integer value (u32) that represents the unwind value for the harness.
+#[cfg(kani)]
+#[proc_macro_attribute]
+pub fn mmio_region(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let mut result = TokenStream::new();
+
+    // Translate #[kani::unwind(arg)] to #[kanitool::unwind(arg)]
+    let insert_string = "#[kanitool::mmio_region(".to_owned() + &attr.clone().to_string() + ")]";
+    result.extend(insert_string.parse::<TokenStream>().unwrap());
+
+    result.extend(item);
+    result
+}

tests/expected/mmio/expected

@@ -0,0 +1,26 @@
+Status: SUCCESS\
+Description: "offset: attempt to compute number in bytes which would overflow"
+
+Status: SUCCESS\
+Description: "attempt to compute offset which would overflow"
+
+Status: FAILURE\
+Description: "dereference failure: pointer NULL"
+
+Status: SUCCESS
+Description: "dereference failure: pointer invalid"
+
+Status: FAILURE\
+Description: "dereference failure: deallocated dynamic object"
+
+Status: FAILURE\
+Description: "dereference failure: dead object"
+
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"
+
+Status: FAILURE\
+Description: "dereference failure: invalid integer address"
+
+Status: FAILURE\
+Description: "dereference failure: invalid integer address"

tests/expected/mmio/main.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+const BUFFER: *mut u32 = 0x8000 as *mut u32;
+const BUFFER2: *mut u32 = 0x1000 as *mut u32;
+
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 8)]
+fn test_write() {
+    let val = 12;
+    unsafe {
+        //BUFFER+2 is not in the MMIO region. Expect pointer check failures.
+        *(BUFFER.offset(2)) = val;
+        //BUFFER2 is not in the MMIO region. Expect pointer check failures.
+        *BUFFER2 = val;
+    }
+}

tests/kani/MMIO/semantics.rs

@@ -0,0 +1,63 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+const BUFFER: *mut u32 = 0x8000 as *mut u32;
+
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 4)]
+fn test_read_after_write_doesnt_havoc() {
+    let val = 12;
+    unsafe {
+        core::ptr::write_volatile(BUFFER, val);
+        let new_val = core::ptr::read_volatile(BUFFER);
+        assert_eq!(new_val, val);
+    }
+}
+
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 4)]
+fn test_read_is_stable() {
+    unsafe {
+        let val1 = core::ptr::read_volatile(BUFFER);
+        let val2 = core::ptr::read_volatile(BUFFER);
+        assert_eq!(val1, val2);
+    }
+}
+
+//TODO Weirdly, these fail even tho the other tests pass???
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 16)]
+fn test_writes_dont_alias() {
+    let val1 = 42;
+    let val2 = 314;
+    unsafe {
+        let p1 = BUFFER;
+        let p2 = BUFFER.offset(2);
+        core::ptr::write_volatile(p1, val1);
+        core::ptr::write_volatile(p2, val2);
+        assert_eq!(core::ptr::read_volatile(p1), val1);
+        assert_eq!(core::ptr::read_volatile(p2), val2);
+    }
+}
+
+//TODO Weirdly, these fail even tho the other tests pass???
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 16)]
+fn test_writes_dont_alias2() {
+    let val1 = 42;
+    let val2 = 314;
+    unsafe {
+        let p1 = BUFFER;
+        let p2 = BUFFER.offset(2);
+        *p1 = val1;
+        *p2 = val2;
+        assert_eq!(*p1, val1);
+        assert_eq!(*p2, val2);
+        assert_eq!(*p2, val1);
+        assert_eq!(*p1, val2);
+    }
+}

tests/kani/MMIO/test.rs

@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+const BUFFER: *mut u32 = 0x8000 as *mut u32;
+const BUFFER2: *mut u32 = 0x1000 as *mut u32;
+
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 4)]
+fn test_write() {
+    let val = 12;
+    unsafe {
+        core::ptr::write_volatile(BUFFER, val);
+    }
+}
+
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 4)]
+#[kani::mmio_region(0x1000, 4)]
+fn test_write2() {
+    let val = 12;
+    unsafe {
+        core::ptr::write_volatile(BUFFER, val);
+        core::ptr::write_volatile(BUFFER2, val);
+    }
+}
+
+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 8)]
+/// Check that larger MMIO regions also work
+fn test_write3() {
+    let val = 12;
+    unsafe {
+        *BUFFER = val;
+        *(BUFFER.offset(1)) = val;
+    }
+}