-
Notifications
You must be signed in to change notification settings - Fork 105
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
Memory blows up on a simple two-dimensional vector example #1226
Comments
An immutable version of the above program doesn't run out of memory, but it doesn't terminate in 1 hour with an #[cfg_attr(kani, kani::proof, kani::unwind(6))]
fn main() {
let v1: Vec<Vec<i32>> = vec![vec![1, 2], vec![3]];
let v2: Vec<i32> = v1.into_iter().flatten().collect();
assert_eq!(v2, vec![1, 2, 3]);
} If I reduce the EDIT: It terminated in 65 minutes with an unwinding of 6 and used 12.6 GB of memory, but an unwinding assertion still failed. |
The probable cause of this is that:
edited to clarify things a bit Possible experiments:
|
Documenting a couple more results:
|
For the record, a smaller version of the above program: #[cfg_attr(kani, kani::proof, kani::unwind(5))]
fn main() {
let v1: Vec<Vec<i32>> = vec![vec![1], vec![]];
let v2: Vec<i32> = v1.into_iter().flatten().collect();
assert_eq!(v2, vec![1]);
} completes in 34 minutes with a minimum unwind of 5 and uses 6.3GB of memory. |
With diffblue/cbmc#7230 on top of diffblue/cbmc@70b7cf7baf735f I get "Verification Time: 74.53128s" when it takes 86.885506s using diffblue/cbmc@70b7cf7baf735f and Kani revision 057926b. These are numbers referring to #1226 (comment). It seems further investigation is necessary here. |
Changes to CBMC to be PR'ed, but I have now gotten this down to 2 seconds. |
Awesome! Is the PR also related to unions? |
My further changes are all extensions to expression simplification, but it's probably necessary to have union field-sensitivity in place as well for otherwise there might just not be anything to propagate (and then simplify). |
I tried this code:
using the following command line invocation:
with Kani version:
I expected to see this happen: Verification successful
Instead, this happened: Memory usage went up to ~25 GB in about 90 seconds.
The text was updated successfully, but these errors were encountered: