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

Boolector failures for functions that return 0 length slices #9

Closed
hudson-ayers opened this issue Aug 28, 2020 · 5 comments
Closed

Comments

@hudson-ayers
Copy link
Contributor

If Haybale encounters a function that returns a 0 length slice (e.g. &mut []) when symbolically exectuing rust code, it aborts with the following boolector failure:

[boolector] boolector_bitvec_sort: 'width' must be > 0

I can't see any reason why this case should be impossible for haybale to analyze, so I am assuming this is a bug. My apologies if this is the intended behavior.

An example of a test that triggers this can be found here: hudson-ayers@1150cbd . Feel free to incorporate this test into your repo if you like. Notably, if you replace &mut [] with self.a in ez2(), the test passes.

@cdisselkoen
Copy link
Collaborator

This is an interesting one. It's not intended behavior - at the minimum, we always want problems to be reported as Haybale errors rather than just having a Boolector crash; but more importantly, it's intended that Haybale can interpret all valid LLVM code.

Both Boolector and LLVM disallow zero-width values in general (e.g. LLVM doesn't allow the i0 type), but it looks like there is a loophole here in that LLVM allows arrays with 0 elements.

I'm not sure the best way to handle this within Haybale. The most general solution would probably be for Haybale's BV object to internally be an enum with two variants, ZeroWidth or a real Boolector BV. I don't have a good sense for whether this would be detrimental to performance or not. Ideally if we could hide all the implementation behind the backend::BV trait facade, we wouldn't have to put match statements all over to specially handle the zero-width case.

But that said, most of the time LLVM doesn't allow zero-width values, so I'm not sure if there might be an easier way to handle this special case without fully building support for zero-width values into Haybale. In particular, LLVM arrays are not first-class values, so we'll never be directly doing operations on zero-width arrays. In this case, probably in most cases, we're only manipulating pointers to zero-width values. The particular error here happens because the Rust expression &mut [] gets translated into an LLVM global variable representing a 0-element array, and when we try to return a pointer to that array, Haybale tries to "initialize" the global variable (which is marked zeroinitializer in LLVM) and tries to create a 0-width BV representing the global variable's value.

I wonder if it's possible to have zero-width arrays that aren't global variables. If not, then we could just add a check when initializing global variables to skip initializing if the variable's width would be 0.

@hudson-ayers
Copy link
Contributor Author

So one rust issue that shed a little information on this for me is this one: rust-lang/rust#74154 . Perhaps that will be helpful to you.

One quote: "references to ZSTs are basically pulled out of thin air and are valid as long as they are non-null".

Even if it is also possible to have zero-width arrays that LLVM does not treat as global variables, it does seem that fixing the case where they are global variables is low cost and an improvement. I struggled to find info on whether LLVM will create zero width arrays that are not global variables.

@cdisselkoen
Copy link
Collaborator

I agree that fixing the global variables case is the best way to go for now - should fix the immediate issue here, and possibly fixes the issue in general. Unfortunately the naive fix I described above fails immediately because it doesn't handle the case of a global variable which is a struct where one element is a zero-width array (which also happens in this example). But handling the struct case as well shouldn't be a big problem. Working on it now.

@cdisselkoen
Copy link
Collaborator

Should be fixed now. Also, thanks for the test case!

@hudson-ayers
Copy link
Contributor Author

Thanks!

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