Add support to shadow memory #3184
Description
Requested feature: Add support to shadow memory
Use case: Allow users to extend their code for verification without impacting runtime
Test case:
union Data {
word: usize,
byte: u8,
}
impl Data {
unsafe fn assume_word(&self) -> usize {
self.word
}
unsafe fn assume_byte(&self) -> u8 {
self.byte
}
}
struct Memory {
data: [Data; 1024],
word: bool,
}
impl Memory {
unsafe fn read_word(&self, index: usize) -> usize {
assert!(self.word);
unsafe { self.data[index].assume_word() }
}
unsafe fn read_byte(&self, index: usize) -> u8 {
assert!(!self.word);
unsafe { self.data[index].assume_byte() }
}
fn new(word: bool) { /* */}
}
#[kani::proof]
fn check_memory() {
// info
}Dummy example where users may want to use shadow memory to track how this code is being used. E.g.: Shadow memory could be used to track if the union has been initialized and which type has been used.