Kani Implementation#210
Conversation
dbittman
left a comment
dbittman
left a comment
There was a problem hiding this comment.
I still need to go through the docs and try it out, but I wanted to get back comments on the PR sooner than I'd be able to get to that. Just some cleanup things.
Can the new directories that are being created in the root be moved somewhere? Trying to keep the root of the repo as minimal as possible. Under tools/kani, perhaps? And any generated files should be under (idk) target//kani or something.
| async-io = { git = "https://github.com/twizzler-operating-system/async-io.git", branch = "twizzler" } | ||
| async-executor = { git = "https://github.com/twizzler-operating-system/async-executor.git", branch = "twizzler" } | ||
| twizzler-futures = { path = "src/lib/twizzler-futures" } | ||
| #twizzler-futures = { path = "src/lib/twizzler-futures" } |
There was a problem hiding this comment.
It'd be nice if we could figure this out before we merge this, since we'll need that crate for async code pretty soon.
There was a problem hiding this comment.
So I think its related to some config that is in a Cargo.toml everyone else depends on but this one, since its new with few dependencies, doesn't and that is messing it up. I can spend the time to try and isolate it.
| # syscall_encode = { version = "0.1.2" } | ||
| volatile = "0.5" | ||
| uart_16550 = "0.3.0" | ||
| x86 = "0.52.0" |
There was a problem hiding this comment.
Some of these are target dependent -- do they have to be moved back up here?
There was a problem hiding this comment.
It does create an error just removing them:
use of undeclared crate or module x86
I can try and find out if there is a way to either
A) Make Kani recognize target-dependent dependencies or
B) Have a seperate category for Kani complication
| // }; | ||
| // p | c | f | u | ||
| // } | ||
| // } |
There was a problem hiding this comment.
What's going on here? Should this be left in, uncommented, or removed?
There was a problem hiding this comment.
I don't know to be honest. I'll ask Esteban and Allen since its in the AMD. I don't remember touching this so I'll find out.
|
|
||
| } | ||
|
|
||
|
|
There was a problem hiding this comment.
Is this a partial example of a kani test? Or one that's not working? If it's the former, what do we still need to do to get it to work? If it's the latter, we should not include it in the main branch, I think.
| //! Low-level object APIs, mostly around IDs and basic things like protection definitions and metadata. | ||
|
|
||
| /* | ||
| KANI_TODO |
There was a problem hiding this comment.
Please include some more detail for these KANI_TODO comments.
| #[cfg(kani)] | ||
| #[kani::proof] | ||
| pub fn it_locks(){ | ||
| // let var:bool = kani::any(); |
There was a problem hiding this comment.
Remove the commented out code
| impl_unit_conversion!(Seconds, FemtoSeconds, FEMTOS_PER_SEC); | ||
| impl_unit_conversion!(NanoSeconds, FemtoSeconds, FEMTOS_PER_NANO); | ||
|
|
||
| #[cfg(kani)] |
There was a problem hiding this comment.
Why is this all commented out?
There was a problem hiding this comment.
Ya these tests fail so its to make to github actions pass, we can
A) Disable them elsewhere
B) Make them passing
C) Remove them entirely
I'll probably do B long term and A short term if possible.
| assert!(tr.get_state() == state); | ||
|
|
||
| } | ||
|
|
There was a problem hiding this comment.
Can't we derive kani::Arbitrary (https://model-checking.github.io/kani/tutorial-nondeterministic-variables.html#custom-nondeterministic-types) for some of these types? I recall doing that, but I'm not the kani expert here :)
| } | ||
|
|
||
| fn wake(_x: &AtomicU64) { | ||
| // println!("wake"); |
There was a problem hiding this comment.
can these be moved into the mod below?
|
I got to some of the comments but I'll go into more depth later this week to fix some of the core issues. |
3 participants
This is a first attempt at integrating Kani into main. There are a few things to note:
In theory, should be good to start adding harnesses.