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

Witness generation crashes in combine_env with abortUnless analysis #1453

Closed
sim642 opened this issue May 10, 2024 · 0 comments · Fixed by #1462 or #1464
Closed

Witness generation crashes in combine_env with abortUnless analysis #1453

sim642 opened this issue May 10, 2024 · 0 comments · Fixed by #1462 or #1464
Assignees
@sim642
Labels
bug precision sv-comp
Milestone
SV-COMP 2025

Comments

@sim642
Copy link
Member

sim642 commented May 10, 2024

Together with #1450, @karoliineh found SV-COMP no-overflow tasks where the abortUnless analysis from #875 does help us. Without it, we learn nothing from assume_abort_if_not conditions which are often used to assume bounds on variables that are key to proving overflow-freedom.

We did some quick benchmarks and it could be worth adding abortUnless to our svcomp conf, however it causes a lot of Not_found crashes from witness generation.
Specifically during combine_env:

analyzer/src/analyses/abortUnless.ml

Lines 51 to 59 in 5cd8650

let combine_env ctx lval fexp f args fc au f_ask =
if au then (
(* Assert before combine_assign, so if variables in `arg` are assigned to, asserting doesn't unsoundly yield bot *)
(* See test 62/03 *)
match args with
| [arg] -> ctx.emit (Events.Assert arg)
| _ -> ()
);
false

There's probably some issue with emitting events from combine_env, but before combine_assign.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@sim642 sim642

Labels
bug precision sv-comp
Projects
None yet
Milestone
SV-COMP 2025
1 participant
@sim642