[DRAFT] Support MMIO regions #1328

danielsn · 2022-07-01T01:41:28Z

Description of changes:

Adds support for MMIO regions to kani proof harnesses.

Resolved issues:

Resolves #1304

Call-outs:

This is dependent on New option --mmio-regions to specify memory regions diffblue/cbmc#6747. It will not work until that is released. I tested against a locally built copy.
We need documentation for this feature
Should probably add some negative tests too
Should test that it behaves like MMIO: writes don't need to be the same as is read back, two reads can get different values

Testing:

How is this change tested? New regression tests.
Is this a refactor change? No

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

kroening · 2022-07-01T12:08:38Z

Why not simply have --mmio_region enabled by default?

kroening · 2022-07-01T12:11:19Z

Why not simply have --mmio_region enabled by default?

(Ignore, it is already)

zpzigi754 · 2022-07-03T08:30:20Z

tests/kani/MMIO/semantics.rs

+        assert_eq!(*p2, val1);
+        assert_eq!(*p1, val2);


I guess that these should be changed like

assert_ne!(*p2, val1); assert_ne!(*p1, val2);

fzaiser · 2022-07-12T19:40:24Z

library/kani_macros/src/lib.rs

+pub fn mmio_region(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let mut result = TokenStream::new();
+
+    // Translate #[kani::unwind(arg)] to #[kanitool::unwind(arg)]


Update comment

fzaiser · 2022-07-12T19:40:31Z

library/kani_macros/src/lib.rs

+
+/// 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.


Update comment

celinval

The semantics here aren't clear to me. Your test_read_is_stable contradicts the item in the callout:

Should test that it behaves like MMIO: writes don't need to be the same as is read back, two reads can get different values.

celinval · 2022-07-12T23:03:53Z

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

+        // 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'");


Can you print or at least log which values we got?

celinval · 2022-07-12T23:06:55Z

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)>,


Should we use usize instead?

celinval · 2022-07-12T23:10:49Z

tests/expected/mmio/expected

@@ -0,0 +1,26 @@
+Status: SUCCESS\
+Description: "offset: attempt to compute number in bytes which would overflow"


This seems irrelevant for your test. I would just remove it.

celinval · 2022-07-12T23:14:26Z

tests/expected/mmio/main.rs

+        //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;


You are not really checking that both fail though. This test will succeed if only one of these fail. You can either add the line in the file to the expected file or break this into two harness and add the function name. I prefer the second since it is always painful to maintain LoC up to date.

celinval · 2022-07-12T23:15:06Z

tests/expected/mmio/main.rs

+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 8)]
+fn test_write() {


can you rename this to check_invalid_write() or something like that?

celinval · 2022-07-12T23:15:50Z

tests/kani/MMIO/semantics.rs

+    }
+}
+
+//TODO Weirdly, these fail even tho the other tests pass???


This looks like a blocker to me. Maybe we should investigate this behavior a bit better.

celinval · 2022-07-12T23:20:05Z

tests/kani/MMIO/semantics.rs

+#[kani::proof]
+#[kani::mmio_region(0x8000, 4)]
+fn test_read_after_write_doesnt_havoc() {
+    let val = 12;


Can you use any instead?

celinval · 2022-07-12T23:21:13Z

tests/kani/MMIO/semantics.rs

@@ -0,0 +1,63 @@
+// Copyright Kani Contributors


Can you please document what these tests are testing?

celinval · 2022-07-12T23:24:14Z

tests/kani/MMIO/test.rs

@@ -0,0 +1,39 @@
+// Copyright Kani Contributors


Can you cover 0 sized operations?

celinval · 2022-07-12T23:29:16Z

tests/kani/MMIO/semantics.rs

+#[cfg(kani)]
+#[kani::proof]
+#[kani::mmio_region(0x8000, 4)]
+fn test_read_is_stable() {


But should it be stable?

celinval · 2023-01-19T20:51:50Z

@danielsn any news here?

danielsn force-pushed the mmio branch from 8173a48 to 5cdaf2f Compare July 1, 2022 01:45

danielsn added 2 commits July 1, 2022 15:55

initial support for mmio

669b56a

turns out only the comma seperated way works

c74fdf5

danielsn force-pushed the mmio branch from 5cdaf2f to 2d3e6c8 Compare July 1, 2022 19:55

better tests

68148ac

danielsn force-pushed the mmio branch from 2d3e6c8 to 68148ac Compare July 1, 2022 19:56

semantics of mmio tests

baee127

zpzigi754 reviewed Jul 3, 2022

View reviewed changes

fzaiser reviewed Jul 12, 2022

View reviewed changes

celinval requested changes Jul 12, 2022

View reviewed changes

adpaco-aws mentioned this pull request Nov 9, 2022

How to verify mmio access? #1304

Open

danielsn closed this Jan 23, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[DRAFT] Support MMIO regions #1328

[DRAFT] Support MMIO regions #1328

danielsn commented Jul 1, 2022 •

edited

Loading

kroening commented Jul 1, 2022

kroening commented Jul 1, 2022

zpzigi754 Jul 3, 2022 •

edited

Loading

fzaiser Jul 12, 2022

fzaiser Jul 12, 2022

celinval left a comment

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval Jul 12, 2022

celinval commented Jan 19, 2023

		@@ -0,0 +1,26 @@
		Status: SUCCESS\
		Description: "offset: attempt to compute number in bytes which would overflow"

[DRAFT] Support MMIO regions #1328

[DRAFT] Support MMIO regions #1328

Conversation

danielsn commented Jul 1, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

kroening commented Jul 1, 2022

kroening commented Jul 1, 2022

zpzigi754 Jul 3, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval commented Jan 19, 2023

danielsn commented Jul 1, 2022 •

edited

Loading

zpzigi754 Jul 3, 2022 •

edited

Loading