From 534a5d562037a323575e3e7dca798952320899b2 Mon Sep 17 00:00:00 2001 From: Andrei Listochkin Date: Tue, 29 Oct 2024 18:36:42 +0100 Subject: [PATCH] exercise: validating data structures with kani --- exercise-book/src/SUMMARY.md | 4 + exercise-book/src/kani-linked-list.md | 446 ++++++++++++++++++ exercise-solutions/Cargo.toml | 1 + .../kani-linked-list/.vscode/settings.json | 5 + .../kani-linked-list/Cargo.toml | 13 + .../kani-linked-list/src/lib.rs | 349 ++++++++++++++ 6 files changed, 818 insertions(+) create mode 100644 exercise-book/src/kani-linked-list.md create mode 100644 exercise-solutions/kani-linked-list/.vscode/settings.json create mode 100644 exercise-solutions/kani-linked-list/Cargo.toml create mode 100644 exercise-solutions/kani-linked-list/src/lib.rs diff --git a/exercise-book/src/SUMMARY.md b/exercise-book/src/SUMMARY.md index c73fbf36..74655d59 100644 --- a/exercise-book/src/SUMMARY.md +++ b/exercise-book/src/SUMMARY.md @@ -134,4 +134,8 @@ - [Final Server Code](./async-chat/final_server_code.md) - [Implementing a Client](./async-chat/implementing_a_client.md) +# Kani Rust Verifier + +- [Verifying Data Structures with Kani](./kani-linked-list.md) + # Other Topics diff --git a/exercise-book/src/kani-linked-list.md b/exercise-book/src/kani-linked-list.md new file mode 100644 index 00000000..2e65242c --- /dev/null +++ b/exercise-book/src/kani-linked-list.md @@ -0,0 +1,446 @@ + +# Verifying Data Structures with Kani + +In this exercise we implement a `remove_at` method for a linked list data structure and will write a Kani harness to prove the correctness of the method. + +Custom data structures (trees, graphs, etc.) in Rust often require the use of `unsafe` code for efficient implementation. +Working with raw pointers means that Rust's borrow checker cannot guarantee the correctness of memory access, and Rust cannot reliably clean memory for us. +Getting a code like this right is difficult, and without Rust compiler helping us along the way we would have to rely on testing instead. + +Today we will look at a linked list - the simplest data structure that relies pointer manipulation. +The example below is very limited. +The unofficial Rust tutorial - [Learn Rust With Entirely Too Many Linked Lists](https://rust-unofficial.github.io/too-many-lists/index.html) - explores the production-ready design of a linked list from Rust Standard Library, while [Implementing Vec](https://doc.rust-lang.org/nomicon/vec/vec.html) section of The Rustonomicon explores aspects of `unsafe` Rust use for designing data structures in more detail. +The same principles apply to other, more complex data structures like trees, graphs, queues, etc. + +## After completing this exercise you will be able to + +- set up Kani support for a project +- write Kani harnesses +- produce Kani playback tests + +## Tasks + +1. Create a new library project `kani-linked-list`, copy the code from below +2. Set up Kani support for the project +3. Add Kani proof for `remove_at` method. +4. If Kani discovers bugs in the method generate playback tests. +5. Fix bugs in the code. + +### Starting code + +This is a doubly-linked list with a relatively limited API. +You can push and pop elements from both ends of the list (`push_front`, `pop_front`, and `push_back`, `pop_back` respectively), you can access the ends of the list (`front[_mut]` and `back[_mut]`), read list's length, and iterate over it. +The test at the bottom of a snippet demonstrates most of the methods available. + +```rust +use std::{fmt::Debug, ptr::NonNull, vec::IntoIter}; + +type Link = Option>>; + +pub struct DoublyLinkedList { + first: Link, + last: Link, + len: usize, +} + +struct Node { + prev: Link, + next: Link, + elem: T, +} + +impl Default for DoublyLinkedList { + fn default() -> Self { + Self::new() + } +} + +impl DoublyLinkedList { + pub fn new() -> Self { + Self { + first: None, + last: None, + len: 0, + } + } + + pub fn push_front(&mut self, elem: T) { + unsafe { + let mut new_first = NonNull::new_unchecked(Box::into_raw(Box::new(Node { + prev: None, + next: None, + elem, + }))); + match self.first { + Some(mut old_first) => { + // rewire pointers + old_first.as_mut().prev = Some(new_first); + new_first.as_mut().next = Some(old_first); + } + None => { + // make a list with a single element + self.last = Some(new_first) + } + } + self.first = Some(new_first); + self.len += 1; + } + } + + pub fn push_back(&mut self, elem: T) { + unsafe { + let mut new_last = NonNull::new_unchecked(Box::into_raw(Box::new(Node { + prev: None, + next: None, + elem, + }))); + match self.last { + Some(mut old_last) => { + // Put the new back before the old one + old_last.as_mut().next = Some(new_last); + new_last.as_mut().prev = Some(old_last); + } + None => { + // make a list with a single element + self.first = Some(new_last); + } + } + self.last = Some(new_last); + self.len += 1; + } + } + + pub fn pop_front(&mut self) -> Option { + let node = self.first?; + unsafe { + let node = Box::from_raw(node.as_ptr()); + let elem = node.elem; + + self.first = node.next; + match self.first { + Some(mut new_first) => { + new_first.as_mut().prev = None; + } + None => { + self.last = None; + } + } + + self.len -= 1; + Some(elem) + } + } + + pub fn pop_back(&mut self) -> Option { + let node = self.last?; + unsafe { + let node = Box::from_raw(node.as_ptr()); + let elem = node.elem; + + self.last = node.prev; + match self.last { + Some(mut new_last) => { + new_last.as_mut().prev = None; + } + None => { + self.last = None; + } + } + + self.len -= 1; + Some(elem) + } + } + + pub fn front(&self) -> Option<&T> { + Some(unsafe { &self.first?.as_ref().elem }) + } + + pub fn front_mut(&mut self) -> Option<&mut T> { + Some(unsafe { &mut self.first?.as_mut().elem }) + } + + pub fn back(&self) -> Option<&T> { + Some(unsafe { &self.last?.as_ref().elem }) + } + + pub fn back_mut(&mut self) -> Option<&mut T> { + Some(unsafe { &mut self.last?.as_mut().elem }) + } + + pub fn len(&self) -> usize { + self.len + } + + pub fn is_empty(&self) -> bool { + self.len == 0 + } + + pub fn iter(&self) -> IntoIter<&T> { + self.into_iter() + } + + pub fn remove_at(&mut self, index: usize) -> Option { + unsafe { + // find an element to remove. + // if `index` is too large this will return `None` early + let to_remove = { + let mut to_remove = self.first; + for _ in 0..index { + to_remove = to_remove?.as_mut().next; + } + Box::from_raw(to_remove?.as_ptr()) + }; + // connect previous and next elements together + let mut prev = to_remove.prev?; + let mut next = to_remove.next?; + prev.as_mut().next = Some(next); + next.as_mut().prev = Some(prev); + + Some(to_remove.elem) + } + } +} + +impl Drop for DoublyLinkedList { + fn drop(&mut self) { + while self.pop_front().is_some() {} + } +} + +impl IntoIterator for DoublyLinkedList { + type Item = T; + + type IntoIter = IntoIter; + + fn into_iter(mut self) -> Self::IntoIter { + // lazy implementation: we take all items from a linked list, put them + // into a vector, and return Vec's iterator. + let mut iter = vec![]; + while let Some(elem) = self.pop_front() { + iter.push(elem); + } + iter.into_iter() + } +} + +impl<'a, T> IntoIterator for &'a DoublyLinkedList { + type Item = &'a T; + + type IntoIter = IntoIter; + + fn into_iter(self) -> Self::IntoIter { + // lazy implementation: we take all items from a linked list, put them + // into a vector, and return Vec's iterator. + let mut iter: Vec<&'a T> = vec![]; + let mut current = self.first; + while let Some(node) = current.map(|n| unsafe { n.as_ref() }) { + current = node.next; + iter.push(&node.elem); + } + iter.into_iter() + } +} + +impl FromIterator for DoublyLinkedList { + fn from_iter>(iter: I) -> Self { + let mut list = Self::new(); + for item in iter { + list.push_back(item); + } + list + } +} + +// Needed for testing +impl Debug for DoublyLinkedList +where + T: Debug, +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_list().entries(self).finish() + } +} + +// Needed for testing +impl PartialEq for DoublyLinkedList +where + T: PartialEq, +{ + fn eq(&self, other: &Self) -> bool { + self.iter().eq(other.iter()) + } +} + +#[cfg(test)] +mod tests { + use crate::DoublyLinkedList; + + #[test] + fn test_list_apis() { + let mut list = DoublyLinkedList::new(); + list.push_back(2); + list.push_front(1); + list.push_back(3); + assert_eq!(format!("{list:?}"), "[1, 2, 3]"); + let front = list.front(); + assert_eq!(front, Some(&1)); + + let removed = list.remove_at(1); + assert_eq!(removed, Some(2)); + assert_eq!(format!("{list:?}"), "[1, 3]"); + + let non_existing = list.remove_at(100); + assert_eq!(non_existing, None); + assert_eq!(format!("{list:?}"), "[1, 3]"); + } +} + +mod proofs { + use super::*; + + // TODO: write a proof for `DoublyLinkedList::remove_at` +} +``` + +## Help + +### Setting up Kani + +

+

+ +Setting up Cargo + + +```toml +# put this into Cargo.toml +[dev-dependencies] +kani-verifier = "0.56.0" + +[dependencies] +# enables autocomplete and code inspections for `kani::*` api +kani = { version = "0.56", git = "https://github.com/model-checking/kani", tag = "kani-0.56.0", optional = true } + +# removes warnings about unknown `cfg` attributes +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(rust_analyzer)', 'cfg(kani)'] } +``` + +
+

+ +

+

+ +Rust Analyzer project settings + + +For VSCode this should be in `.vscode/settings.json` + +```json +{ + "rust-analyzer.cargo.features": ["kani"] +} +``` + +
+

+ +

+

+ +Optional: You may decide to use nightly Rust if Rust Analyzer doesn't work as expected. + + +Create `rust-toolchain.toml` in project's root + +```toml +[toolchain] +channel = "nightly" +``` + +
+

+ +### Writing Kani proofs + +

+

+ +Code snippet to keep Rust Analyzer from showing macro errors for Kani + + +```rust ignore +#[cfg_attr(not(rust_analyzer), cfg(kani))] +mod proofs { + use super::*; + + #[cfg_attr(not(rust_analyzer), kani::proof)] + fn kani_harness() { + todo!(); + } + + #[test] + fn kani_concrete_playback_xxx() { + // playback code here + } +} +``` + +
+

+ +### Other Kani help + +

+

+ +Generating a list of random elements. + + +You can make a list by making an array first using [`from_fn`](https://doc.rust-lang.org/std/array/fn.from_fn.html) function. +Then you can pass the array to a [`from_iter`](https://doc.rust-lang.org/std/iter/trait.FromIterator.html#tymethod.from_iter) method. + +```rust ignore +const TOTAL: usize = 10; +let items: [u32; TOTAL] = std::array::from_fn(|_| kani::any::()); + +let mut list = DoublyLinkedList::from_iter(items.iter().copied()); +assert_eq!(list.len(), TOTAL); +``` + +
+

+ +

+

+ +You can use kani::any_where() to generate a value within a specific range. + + +```rust ignore +let x: i32 = kani::any_where(|n| (1..=10).contains(n)); +``` + +
+

+ +

+

+ +If the proof takes a lot of time to run you can introduce the upper unwind limit for loops. + + +```rust ignore +#[cfg_attr(not(rust_analyzer), kani::proof)] +#[cfg_attr(not(rust_analyzer), kani::unwind(20))] +fn long_running_proof() { +} +``` + +The exact limit is not important. +But by making the list under test shorter you can in turn safely lower the limit while letting the solver observe *all* possible states of the program and complete the verification. + +
+

diff --git a/exercise-solutions/Cargo.toml b/exercise-solutions/Cargo.toml index 44b6dac8..d84b3a1a 100644 --- a/exercise-solutions/Cargo.toml +++ b/exercise-solutions/Cargo.toml @@ -11,4 +11,5 @@ members = [ "shapes-part-3", "tcp-server-exercises", "async-chat", + "kani-linked-list", ] diff --git a/exercise-solutions/kani-linked-list/.vscode/settings.json b/exercise-solutions/kani-linked-list/.vscode/settings.json new file mode 100644 index 00000000..6cf1acb5 --- /dev/null +++ b/exercise-solutions/kani-linked-list/.vscode/settings.json @@ -0,0 +1,5 @@ +{ + "rust-analyzer.cargo.features": [ + "kani" + ] +} diff --git a/exercise-solutions/kani-linked-list/Cargo.toml b/exercise-solutions/kani-linked-list/Cargo.toml new file mode 100644 index 00000000..451526a7 --- /dev/null +++ b/exercise-solutions/kani-linked-list/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "kani-linked-list" +version = "0.1.0" +edition = "2021" + +[dependencies] +kani = { version = "=0.56", git = "https://github.com/model-checking/kani", tag = "kani-0.56.0", optional = true } + +[dev-dependencies] +kani-verifier = "=0.56.0" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(rust_analyzer)', 'cfg(kani)'] } diff --git a/exercise-solutions/kani-linked-list/src/lib.rs b/exercise-solutions/kani-linked-list/src/lib.rs new file mode 100644 index 00000000..f40d1712 --- /dev/null +++ b/exercise-solutions/kani-linked-list/src/lib.rs @@ -0,0 +1,349 @@ +use std::{fmt::Debug, ptr::NonNull, vec::IntoIter}; + +type Link = Option>>; + +pub struct DoublyLinkedList { + first: Link, + last: Link, + len: usize, +} + +struct Node { + prev: Link, + next: Link, + elem: T, +} + +impl Default for DoublyLinkedList { + fn default() -> Self { + Self::new() + } +} + +impl DoublyLinkedList { + pub fn new() -> Self { + Self { + first: None, + last: None, + len: 0, + } + } + + pub fn push_front(&mut self, elem: T) { + unsafe { + let mut new_first = NonNull::new_unchecked(Box::into_raw(Box::new(Node { + prev: None, + next: None, + elem, + }))); + match self.first { + Some(mut old_first) => { + // rewire pointers + old_first.as_mut().prev = Some(new_first); + new_first.as_mut().next = Some(old_first); + } + None => { + // make a list with a single element + self.last = Some(new_first) + } + } + self.first = Some(new_first); + self.len += 1; + } + } + + pub fn push_back(&mut self, elem: T) { + unsafe { + let mut new_last = NonNull::new_unchecked(Box::into_raw(Box::new(Node { + prev: None, + next: None, + elem, + }))); + match self.last { + Some(mut old_last) => { + // Put the new back before the old one + old_last.as_mut().next = Some(new_last); + new_last.as_mut().prev = Some(old_last); + } + None => { + // make a list with a single element + self.first = Some(new_last); + } + } + self.last = Some(new_last); + self.len += 1; + } + } + + pub fn pop_front(&mut self) -> Option { + let node = self.first?; + unsafe { + let node = Box::from_raw(node.as_ptr()); + let elem = node.elem; + + self.first = node.next; + match self.first { + Some(mut new_first) => { + new_first.as_mut().prev = None; + } + None => { + self.last = None; + } + } + + self.len -= 1; + Some(elem) + } + } + + pub fn pop_back(&mut self) -> Option { + let node = self.last?; + unsafe { + let node = Box::from_raw(node.as_ptr()); + let elem = node.elem; + + self.last = node.prev; + match self.last { + Some(mut new_last) => { + new_last.as_mut().prev = None; + } + None => { + self.last = None; + } + } + + self.len -= 1; + Some(elem) + } + } + + pub fn front(&self) -> Option<&T> { + Some(unsafe { &self.first?.as_ref().elem }) + } + + pub fn front_mut(&mut self) -> Option<&mut T> { + Some(unsafe { &mut self.first?.as_mut().elem }) + } + + pub fn back(&self) -> Option<&T> { + Some(unsafe { &self.last?.as_ref().elem }) + } + + pub fn back_mut(&mut self) -> Option<&mut T> { + Some(unsafe { &mut self.last?.as_mut().elem }) + } + + pub fn len(&self) -> usize { + self.len + } + + pub fn is_empty(&self) -> bool { + self.len == 0 + } + + pub fn iter(&self) -> IntoIter<&T> { + self.into_iter() + } + + pub fn remove_at(&mut self, index: usize) -> Option { + unsafe { + // find an element to remove. + // if `index` is too large this will return `None` early + let to_remove = { + let mut to_remove = self.first; + for _ in 0..index { + to_remove = to_remove?.as_mut().next; + } + Box::from_raw(to_remove?.as_ptr()) + }; + // connect previous and next elements together + let prev = to_remove.prev; + let next = to_remove.next; + match (prev, next) { + (Some(mut prev), Some(mut next)) => { + prev.as_mut().next = Some(next); + next.as_mut().prev = Some(prev); + } + (Some(mut prev), None) => { + prev.as_mut().next = None; + self.last = Some(prev); + } + (None, Some(mut next)) => { + next.as_mut().prev = None; + self.first = Some(next); + } + (None, None) => { + self.first = None; + self.last = None; + } + } + Some(to_remove.elem) + } + } +} + +impl Drop for DoublyLinkedList { + fn drop(&mut self) { + while self.pop_front().is_some() {} + } +} + +impl IntoIterator for DoublyLinkedList { + type Item = T; + + type IntoIter = IntoIter; + + fn into_iter(mut self) -> Self::IntoIter { + // lazy implementation: we take all items from a linked list, put them + // into a vector, and return Vec's iterator. + let mut iter = vec![]; + while let Some(elem) = self.pop_front() { + iter.push(elem); + } + iter.into_iter() + } +} + +impl<'a, T> IntoIterator for &'a DoublyLinkedList { + type Item = &'a T; + + type IntoIter = IntoIter; + + fn into_iter(self) -> Self::IntoIter { + // lazy implementation: we take all items from a linked list, put them + // into a vector, and return Vec's iterator. + let mut iter: Vec<&'a T> = vec![]; + let mut current = self.first; + while let Some(node) = current.map(|n| unsafe { n.as_ref() }) { + current = node.next; + iter.push(&node.elem); + } + iter.into_iter() + } +} + +impl FromIterator for DoublyLinkedList { + fn from_iter>(iter: I) -> Self { + let mut list = Self::new(); + for item in iter { + list.push_back(item); + } + list + } +} + +// Needed for testing +impl Debug for DoublyLinkedList +where + T: Debug, +{ + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_list().entries(self).finish() + } +} + +// Needed for testing +impl PartialEq for DoublyLinkedList +where + T: PartialEq, +{ + fn eq(&self, other: &Self) -> bool { + self.iter().eq(other.iter()) + } +} + +#[cfg(test)] +mod tests { + use crate::DoublyLinkedList; + + #[test] + fn test_list_apis() { + let mut list = DoublyLinkedList::new(); + list.push_back(2); + list.push_front(1); + list.push_back(3); + assert_eq!(format!("{list:?}"), "[1, 2, 3]"); + let front = list.front(); + assert_eq!(front, Some(&1)); + + let removed = list.remove_at(1); + assert_eq!(removed, Some(2)); + assert_eq!(format!("{list:?}"), "[1, 3]"); + + let non_existing = list.remove_at(100); + assert_eq!(non_existing, None); + assert_eq!(format!("{list:?}"), "[1, 3]"); + } +} + +#[cfg_attr(not(rust_analyzer), cfg(kani))] +mod proofs { + use super::*; + + #[cfg_attr(not(rust_analyzer), kani::proof)] + #[cfg_attr(not(rust_analyzer), kani::unwind(20))] + fn remove_at() { + const TOTAL: usize = 10; + let items: [u32; TOTAL] = std::array::from_fn(|_| kani::any::()); + + let mut list = DoublyLinkedList::from_iter(items.iter().copied()); + assert_eq!(list.len(), TOTAL); + + // let position: usize = kani::any_where(|&n| n > 0 && n < TOTAL - 1); + let position: usize = kani::any_where(|n| (0..TOTAL).contains(n)); + let removed = list.remove_at(position); + assert_eq!(removed, Some(items[position])); + // Check pointer integrity + assert!(list.front().is_some()); + assert!(list.back().is_some()); + + let position: usize = kani::any_where(|&n| n >= TOTAL); + let removed = list.remove_at(position); + assert_eq!(removed, None); + } + + #[cfg_attr(not(rust_analyzer), kani::proof)] + fn remove_the_only_element_from_list() { + let item: u32 = kani::any(); + let mut list = DoublyLinkedList::new(); + list.push_back(item); + let removed = list.remove_at(0); + assert_eq!(removed, Some(item)); + assert_eq!(list.front(), None); + assert_eq!(list.back(), None); + } + + // The exact number of playback tests can vary. + // As you fix more bugs some older playback tests may become invalid, and + // may have to be removed + #[test] + fn kani_concrete_playback_remove_at_11026539725679402838() { + let concrete_vals: Vec> = vec![ + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 4294967292 + vec![252, 255, 255, 255], + // 0ul + vec![0, 0, 0, 0, 0, 0, 0, 0], + // 10ul + vec![10, 0, 0, 0, 0, 0, 0, 0], + ]; + kani::concrete_playback_run(concrete_vals, remove_at); + } +}