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

Flux (ultimately z3) hangs on trivial constraint. #949

Open
vrindisbacher opened this issue Dec 17, 2024 · 20 comments
Open

Flux (ultimately z3) hangs on trivial constraint. #949

vrindisbacher opened this issue Dec 17, 2024 · 20 comments

Comments

@vrindisbacher
Copy link
Collaborator

@ranjitjhala, here's the constraint from exception_entry that hangs in z3.

l.smt2.txt
@ranjitjhala
Copy link
Contributor

@nilehmann the issue here is this: there is a flux constraint of the form

(forall ... 
  (=> ( = (foo x y z)  (bar x y z)) 
         ( = (foo x y z) (bar x y z)))

The trouble is foo and bar are complicated functions with various bitvectory things going on.

Now, flux expands out the definitions of foo and bar and then fixpoint does some further shenanigans, so then z3 has to do a lot of work to figure out that its just the above, and z3 seems to hang in the process, even though just treating foo and bar as uninterpreted should let it trivially prove the VC.

So, I think its worth exploring leaving all the unfolding just to z3?

i.e. pass the definitions of the functions into fixpoint, which will then pass it into z3, which can chose to unfold or not. Does that make sense?

@nilehmann
Copy link
Member

How are functions definitions translated into z3? My understanding is that define-fun is treated as a macro and eagerly expanded but define-fun-rec is not.

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 17, 2024 via email

@ranjitjhala
Copy link
Contributor

Actually, it occurs to me that one relatively simple thing that could be done either in (a) flux, (b) fixpoint or (c) the SMT solver, is our "refinement reflection" trick which is, given a formula P with "applications" inside it, you can
just add all the equalities for the applications, so if your VC is forall x.... p you strengthen it to forall x... eqs &&p where eqs are conjunctions of the form f1(x1..) = e1 && f2(x2..) = e2 && ...

This way you have your cake and eat it too.

If you can trivially prove the formula with just uninterpreted functions, then great.

If instead you need the definitions, then those are also available via the equalities.

What I don't know is whether Z3 and friends do something like this already (in which case we should just pass the folded-up function applications directly) or whether they aggressively inline).

At any rate, maybe the easiest option is to implement this equality-based method in flux to see if it works?

@nilehmann
Copy link
Member

My understanding from z3's docs is that define-fun-rec works similar to that trick by incrementally doing more unfolding

https://microsoft.github.io/z3guide/docs/logic/Recursive%20Functions/

I know this is standard smtlib, but I don't know how other solvers handle it.

Ultimately, it's a matter of who is in better position to do the unfolding.

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 17, 2024 via email

@vrindisbacher
Copy link
Collaborator Author

@ranjitjhala @nilehmann I have two other annotations that cause z3 to hang. The constraints are not trivial unfortunately. Would it be helpful to add the smt2 files here? Or maybe the liquid fixpoint smt2 file?

@ranjitjhala
Copy link
Contributor

Lets just keep them here to track them for now?

@vrindisbacher
Copy link
Collaborator Author

Ok i'll edit the issue with their description.

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 17, 2024 via email

@vrindisbacher
Copy link
Collaborator Author

vrindisbacher commented Dec 17, 2024 •
edited
Loading

ahh interesting... I ran cvc5 on the smt2 file outputted by fixpoint for one of the hanging constraints and it solves everything no problem. I'm going to try this with my other hanging constraints. I did see this issue which seems to indicate z3 is not the best at solving bitvectory things.

@vrindisbacher
Copy link
Collaborator Author

Ya, CVC5 seems to be able to check all assertions that z3 hangs on very quickly.

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 17, 2024 via email

@vrindisbacher
Copy link
Collaborator Author

Ya - it smashes the whole smt2 file in less than a second...

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 17, 2024 via email

@ranjitjhala
Copy link
Contributor

ranjitjhala commented Dec 17, 2024 via email

@nilehmann
Copy link
Member

I'll work on adding a flag for cvc5

@vrindisbacher vrindisbacher mentioned this issue Dec 17, 2024
Merged
@vrindisbacher
Copy link
Collaborator Author

@ranjitjhala, I patched up liquid fixpoint so that I could run it like so fixpoint --solver=cvc5. I created a pr for that here.

@vrindisbacher
Copy link
Collaborator Author

I also manually patched flux to run fixpoint --solver=cvc5 on my machine. It checks the trivial constraint in 1 second :)
Screenshot 2024-12-17 at 10 26 03 AM

@ranjitjhala
Copy link
Contributor

Have posted an issue here Z3Prover/z3#7484

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@ranjitjhala @nilehmann @vrindisbacher