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

Add disjunctive completion of Apron domains #1339

Closed
wants to merge 15 commits into from

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Jan 26, 2024

This is on top of #1216 as an attempt to make it handle disjunctive relational invariants.

It "works" except there are some very odd fixpoint errors that I'll have to debug further. Last I looked at them it seemed so odd that they might've something to do with the mutable aspects of Apron domains.

@sim642 sim642 added feature precision pr-dependency Depends or builds on another PR, which should be merged before labels Jan 26, 2024
@sim642 sim642 self-assigned this Jan 26, 2024
@michael-schwarz michael-schwarz added the relational Relational analyses (Apron, affeq, lin2var) label Jan 26, 2024
@sim642
Copy link
Member Author

sim642 commented Jan 26, 2024

Something completely mysterious is happening with the fixpoint errors. Printing out the solver solution indicates the unknown being there, yet not being found. Printing hashes shows they match, so that's not the problem. Tracing equal somehow makes the fixpoint error disappear...

Even more mysteriously, at one point duplicating an --enable argument caused the fixpoint error to disappear.

@sim642
Copy link
Member Author

sim642 commented Jan 29, 2024

I've hunted the issue down to Apron's compare implementations not being suitable for Set and Make: antoinemine/apron#99. I'm surprised that this hasn't shown up before. Or maybe it has and that's the source of some of the sporadic ERROR (verify) results on sv-benchmarks.

Base automatically changed from priv-atomic to master February 15, 2024 14:14
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Feb 19, 2024
@sim642 sim642 mentioned this pull request May 6, 2024
3 tasks
@sim642
Copy link
Member Author

sim642 commented Jul 30, 2024

This was for an attempt to validate some witnesses with ghosts. Since we no longer plan to do this and because this didn't scale (or be precise enough, depending on widen), we decided to close this at a GobCon.

I cherry-picked e5f097c and bc85d30 to master.

@sim642 sim642 closed this Jul 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature precision relational Relational analyses (Apron, affeq, lin2var)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants