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.

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

iface methods with generic ret types that get bound to unit ret to undef memory #1910

Closed
nikomatsakis opened this issue Feb 29, 2012 · 3 comments

Comments

@nikomatsakis
Copy link
Contributor

In this test case:

enum deser = uint;

iface reader {
    fn read_vec_elt<T:copy>(f: fn() -> T) -> T;
}

impl of reader for deser {
    fn read_vec_elt<T:copy>(f: fn() -> T) -> T {
        f()
    }
}

fn read_to_vec<D:reader, T:copy>(self: D, f: fn() -> T) -> [T] {
    let v = [];
    self.read_vec_elt() {|| v += [f()] }
    v
}

fn main() {
    let x = deser(1u);
    assert [22u] == read_to_vec(x) {|| 22u };
}

The call to self.read_vec_elt() which occurs in read_to_vec() gets compiled down to some LLVM code like:

  invoke void %40([1 x i8*]* %3, i1* undef, { i64, %tydesc*, i8*, i8*, i8 }* %41, %tydesc* @tydesc1, { void (i1*, { i64, %tydesc*, i8*, i8*, i8 }*)*, { i64, %tydesc*, i8*, i8*, i8 }* }* %8)
          to label %54 unwind label %55

In particular, the second argument to this call (in this case, that is the destination ptr) is i1* undef. As a result, the return value of () gets written into random memory. This leads to crashes on some systems, in particular Ubuntu. This same bug is causing block-arg.rs to fail under testing (though not on the bots nor on macs etc).

This problem only seems to occur if the call is to an iface method. If you change the type of self to be deser or some other concrete type, the problem goes away. I presume this is some sort of interaction between the typing of iface methods vs those of other callees, because right now the code tries to get smart and avoid allocating space for the return value if the return type is unit... but in this case, that logic is not working.

@marijnh
Copy link
Contributor

marijnh commented Feb 29, 2012

I'll take this.

@ghost ghost assigned marijnh Feb 29, 2012
@marijnh
Copy link
Contributor

marijnh commented Mar 1, 2012

So is this fixed now?

@nikomatsakis
Copy link
Contributor Author

Sorry, yes it is. Fixed in ed952ec

celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
A bunch of the harnesses from the smack testsuite were missing kani::proof annotation. They have the kani-verify-fail tag on them, and because of rust-lang#1910, they would fail but with a different error than expected.

Add #[kani::proof] to them.
celinval added a commit to celinval/rust-dev that referenced this issue Jun 4, 2024
…ler (rust-lang#1956)

This PR is a pre-req for getting a per-harness reachability algorithm. First we need to stop treating all goto generated by the compiler as the same model which is what this PR does.

For that, I introduce the concept of a project, which is basically a container of artifacts produced by the build system. The goal is to abstracts the verification code from the build system we pick. It also provide methods to get artifacts relevant to a harness. Today this method will return the artifact related to the crate where it is contained, but in the future it can be easily modified to be the harness specific goto model.

The only behavioral change in this PR is that we disabled `--gen-c` for `--function` and `--legacy-linker` to simplify the code since all these options are for internal usage or on track to be deleted.

This change also fixes inconsistent / incorrect behaviors. They are the following:

1. Kani is now sound when two or more targets contains harnesses or no mangled functions that have the same name (rust-lang#1974). Note that this is not the case for `--legacy-linker` and `--function` options.
2. `kani` now respects the `--target-dir` argument provided by the customer.
3. `kani` no longer crash when the crate has no harness (rust-lang#1910).

Co-authored-by: Zyad Hassan <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants