Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Multiple failures in overlapping traits example #564

Closed
adpaco-aws opened this issue Oct 18, 2021 · 3 comments · Fixed by #1801
Closed

Multiple failures in overlapping traits example #564

adpaco-aws opened this issue Oct 18, 2021 · 3 comments · Fixed by #1801
Assignees
@celinval
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Milestone
Fix linking issue...

Comments

@adpaco-aws
Copy link
Contributor

In the example from Rust by Example/Traits/Disambiguating overlapping traits/11.rs shown here:

// compile-flags: --edition 2018
// rmc-flags: --cbmc-args --unwind 10
#![allow(unused)]
trait UsernameWidget {
    // Get the selected username out of this widget
    fn get(&self) -> String;
}

trait AgeWidget {
    // Get the selected age out of this widget
    fn get(&self) -> u8;
}

// A form with both a UsernameWidget and an AgeWidget
struct Form {
    username: String,
    age: u8,
}

impl UsernameWidget for Form {
    fn get(&self) -> String {
        self.username.clone()
    }
}

impl AgeWidget for Form {
    fn get(&self) -> u8 {
        self.age
    }
}

pub fn main() {
    let form = Form{
        username: "rustacean".to_owned(),
        age: 28,
    };

    // If you uncomment this line, you'll get an error saying 
    // "multiple `get` found". Because, after all, there are multiple methods
    // named `get`.
    // println!("{}", form.get());

    let username = <Form as UsernameWidget>::get(&form);
    assert_eq!("rustacean".to_owned(), username);
    let age = <Form as AgeWidget>::get(&form);
    assert_eq!(28, age);
}

we get many multiple failures:

[std::alloc::dealloc.precondition_instance.1] line 104 free argument must be NULL or valid pointer: FAILURE
[std::alloc::dealloc.precondition_instance.2] line 104 free argument must be dynamic object: FAILURE
[std::alloc::dealloc.precondition_instance.3] line 104 free argument has offset zero: FAILURE
[std::alloc::dealloc.precondition_instance.4] line 104 double free: FAILURE
[alloc::raw_vec::RawVec::<T, A>::current_memory.pointer_dereference.3] line 260 dereference failure: deallocated dynamic object in self->cap: FAILURE
[alloc::raw_vec::RawVec::<T, A>::current_memory.pointer_dereference.10] line 267 dereference failure: deallocated dynamic object in self->cap: FAILURE
[alloc::raw_vec::RawVec::<T, A>::current_memory.pointer_dereference.16] line 269 dereference failure: deallocated dynamic object in self->ptr: FAILURE
[alloc::raw_vec::RawVec::<T, A>::ptr.pointer_dereference.3] line 243 dereference failure: deallocated dynamic object in self->ptr: FAILURE
[<std::vec::Vec<T, A> as std::ops::Drop>::drop.pointer_dereference.3] line 2784 dereference failure: deallocated dynamic object in self->len: FAILURE
[std::vec::Vec::<T, A>::as_mut_ptr.assertion.1] line 1172 assumption failed: FAILURE
[std::vec::Vec::<T, A>::as_ptr.assertion.1] line 1136 assumption failed: FAILURE
[std::alloc::Layout::align.pointer_dereference.3] line 119 dereference failure: deallocated dynamic object in self->align_: FAILURE
[std::alloc::Layout::size.pointer_dereference.3] line 109 dereference failure: deallocated dynamic object in self->size_: FAILURE
[main.assertion.1] line 44 a panicking function core::panicking::assert_failed is invoked: FAILURE
[memcmp.precondition.2] line 21 memcpy region 2 readable: FAILURE
[memcmp.pointer_arithmetic.7] line 27 pointer arithmetic: pointer NULL in sc2 + 1l: FAILURE
[memcmp.pointer_arithmetic.8] line 27 pointer arithmetic: pointer invalid in sc2 + 1l: FAILURE
[memcmp.pointer_arithmetic.9] line 27 pointer arithmetic: deallocated dynamic object in sc2 + 1l: FAILURE
[memcmp.pointer_arithmetic.10] line 27 pointer arithmetic: dead object in sc2 + 1l: FAILURE
[memcmp.pointer_arithmetic.11] line 27 pointer arithmetic: pointer outside object bounds in sc2 + 1l: FAILURE
[memcmp.pointer_arithmetic.12] line 27 pointer arithmetic: invalid integer address in sc2 + 1l: FAILURE
[memcmp.pointer_dereference.7] line 27 dereference failure: pointer NULL in *tmp_post$0: FAILURE
[memcmp.pointer_dereference.8] line 27 dereference failure: pointer invalid in *tmp_post$0: FAILURE
[memcmp.pointer_dereference.9] line 27 dereference failure: deallocated dynamic object in *tmp_post$0: FAILURE
[memcmp.pointer_dereference.10] line 27 dereference failure: dead object in *tmp_post$0: FAILURE
[memcmp.pointer_dereference.11] line 27 dereference failure: pointer outside object bounds in *tmp_post$0: FAILURE
[memcmp.pointer_dereference.12] line 27 dereference failure: invalid integer address in *tmp_post$0: FAILURE

Moreover, the unwind value seems to be higher than I would expect (currently 10).
@adpaco-aws adpaco-aws mentioned this issue Oct 18, 2021
Closed
98 tasks
@zhassan-aws zhassan-aws added [C] Bug This is a bug. Something isn't working. MLP - Must Have labels Mar 16, 2022
@celinval
Copy link
Contributor

Some of these failures are related to #763. Once we fix it, we should see what tests are still failing here.

@zhassan-aws
Copy link
Contributor

zhassan-aws commented Mar 24, 2022 •
edited
Loading

With the switch to replacing unknown functions with assert false followed by assume false (done in #964), this test now produces a single failure due to the missing std library function:

Check 10: _ZN60_$LT$alloc..string..String$u20$as$u20$core..clone..Clone$GT$5clone17h2f973f87e464a75bE.assertion.1
	 - Status: FAILURE
	 - Description: "assertion false"
	 - Location: Unknown File in function _ZN60_$LT$alloc..string..String$u20$as$u20$core..clone..Clone$GT$5clone17h2f973f87e464a75bE

SUMMARY: 
 ** 1 of 231 failed (2 unreachable)
Failed Checks: assertion false

VERIFICATION:- FAILED

If this is something that cannot be easily supported, we should add a warning/error message in the short term and remove the "MLP - Must Have" label.

@zhassan-aws
Copy link
Contributor

Here's a minimized example that produces the missing function failure:

fn main() {
    let x = String::from("foo");
    let y = x.clone();
    assert_eq!("foo", y);
}

@jaisnan jaisnan mentioned this issue Apr 28, 2022
Merged
4 tasks
@tedinski tedinski mentioned this issue May 23, 2022
Closed
@celinval celinval self-assigned this Oct 24, 2022
@celinval celinval mentioned this issue Oct 26, 2022
Merged
4 tasks
celinval added a commit that referenced this issue Oct 26, 2022
@celinval
Add tests for issues related to std linking (#1801)
f306a44 
Add tests for #564, #208 and #87.

Unfortunately, it looks like there are still issues with with how we are
encoding panic threads and dynamic objects which are causing two of the
test cases to fail.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@celinval celinval

Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Projects
None yet
Milestone
Fix linking issues against std librar...
Development

Successfully merging a pull request may close this issue.

Add tests for issues related to std linking celinval/kani-dev
4 participants
@celinval @adpaco-aws @zhassan-aws @jaisnan