Open nokunish opened 1 year ago
Verifying the properties of a vector after cloning its elements cause unsoundness.
For instance, given an element,
struct Elem<T> where T: Copy { val: T, next: usize }
Verifying the field next, in which we don't clone, will cause the error,
next
fn push<T>(init: T) where T: Copy { let mut vec:Vec<Elem<T>> = Vec::new(); let mut i = 0; prusti_assert!( i < vec.len() ==> (*SliceIndex::index(i, &vec)).next == 0 ); vec.push(Elem {val: init.clone(), next: 0}); }
Error message:
Details: consistency error in prusti_test::test_v1::code::debug::debug::push: Consistency error: DomainType references non-existent domain Snap$__TYPARAM__$_T$0$__. (<no position>)
However, all four of the below will get verified successfully:
Verifying the cloned val field instead
val
fn push<T>(init: T) where T: Copy { let mut vec:Vec<Elem<T>> = Vec::new(); let mut i = 0; prusti_assert!( i < vec.len() ==> (*SliceIndex::index(i, &vec)).val === init ); vec.push(Elem {val: init.clone(), next: 0}); }
Verifying the cloned val field before / after verifying the next field
fn push<T>(init: T) where T: Copy { let mut vec:Vec<Elem<T>> = Vec::new(); let mut i = 0; prusti_assert!( i < vec.len() ==> (*SliceIndex::index(i, &vec)).val === init ); prusti_assert!( i < vec.len() ==> (*SliceIndex::index(i, &vec)).next == 0 ); vec.push(Elem {val: init.clone(), next: 0}); }
clone the value first, before calling push
push
fn push<T>(init: T) where T: Copy { let mut vec:Vec<Elem<T>> = Vec::new(); let mut i = 0; let val = init.clone(); prusti_assert!( i < vec.len() ==> (*SliceIndex::index(i, &vec)).next == 0 ); vec.push(Elem {val, next: 0}); }
if we don't clone (which is possible in this case since we implemented Copy)
fn push<T>(init: T) where T: Copy { let mut vec:Vec<Elem<T>> = Vec::new(); let mut i = 0; prusti_assert!( i < vec.len() ==> (*SliceIndex::index(i, &vec)).next == 0 ); vec.push(Elem {val: init, next: 0}); }
Also, providing the post-condition,
#[ensures( *SliceIndex::index(&self, self.len() - 1) === value )] pub fn push(&mut self, value: T);
in the external specification seems to fix the issue (but providing post-conditions that does not reference value has no effect), which I'm not sure why?
value
Thanks for the report. Could you provide a full example with the specification of SliceIndex?
SliceIndex
Verifying the properties of a vector after cloning its elements cause unsoundness.
For instance, given an element,
Verifying the field
next
, in which we don't clone, will cause the error,Error message:
However, all four of the below will get verified successfully:
Verifying the cloned
val
field insteadVerifying the cloned
val
field before / after verifying thenext
fieldclone the value first, before calling
push
if we don't clone (which is possible in this case since we implemented Copy)
Also, providing the post-condition,
in the external specification seems to fix the issue (but providing post-conditions that does not reference
value
has no effect), which I'm not sure why?