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

SMTChecker: computation of loop iterations and unrolling while and do-while #3274

Closed
wants to merge 1 commit into
base: develop
from

Conversation

Projects
None yet
3 participants
@leonardoalt
Member

leonardoalt commented Dec 3, 2017

New code:

  • Detects automatically the amount of times a loop runs, supports <=, <, > and >=. This is done by asking z3 to maximize and minimize the equation, and checking whether the resulting value is the same. If yes, that is the constant difference between the left and right sides at that code point. Assuming (Assumption [1]) the difference decreases once every loop iteration, that is the loop bound.
  • The loop is then unrolled that amount of times, and the touched variables merged after each iteration.
  • If the loop runs less times than the computed bound the code is sound. If the loop runs more times, there are no guarantees.
  • If a constant difference isn't found, the loop body is run once, as it was before.
  • Added tests for while and do-while.

Main changes to existing code:

  • Added the maximize and minimize functions to the solver interface.
  • Since the loop condition and body may be visited several times, an Expression may now have many smt::Expression. Method expr now points to the latest one.

Questions:

  • Do we want to keep the check of whether a do-while condition is always true/false? I wonder how much help that would actually be to the user.
  • In the while case, I kept the warning message only when the condition is false at the moment of the first condition check, that is, will never go in.
  • Do we want a warning message stating that automatic loop bound detection does not support == and !=?
  • I've added a note stating assumption [1] as a warning message. Do we want to keep it?

This PR depends on (or subsumes) #3217.

@chriseth chriseth added the in progress label Dec 3, 2017

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 3, 2017

Member

@leonardoalt is there a way you could split these changes into smaller PRs?

Member

axic commented Dec 3, 2017

@leonardoalt is there a way you could split these changes into smaller PRs?

@leonardoalt leonardoalt closed this Dec 3, 2017

@chriseth chriseth removed the in progress label Dec 3, 2017

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Dec 3, 2017

Member

@axic I actually just noticed that the older commits from the other PR were indeed merged into division. I'll rebase and check how the new PR would look like.

Member

leonardoalt commented Dec 3, 2017

@axic I actually just noticed that the older commits from the other PR were indeed merged into division. I'll rebase and check how the new PR would look like.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 3, 2017

Member

@leonardoalt you don't need to close the PR you can just force push over it.

Also I hope we can merge #3032 tomorrow just need an answer from @chriseth on the question there.

Member

axic commented Dec 3, 2017

@leonardoalt you don't need to close the PR you can just force push over it.

Also I hope we can merge #3032 tomorrow just need an answer from @chriseth on the question there.

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Dec 3, 2017

Member

Yeah but I wanted to get rid of the old commits...

Member

leonardoalt commented Dec 3, 2017

Yeah but I wanted to get rid of the old commits...

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Dec 3, 2017

Member

Actually, I don't quite get why GitHub is placing all those commits from @chriseth under this PR, since they are already in the division branch. Going to reopen.

Member

leonardoalt commented Dec 3, 2017

Actually, I don't quite get why GitHub is placing all those commits from @chriseth under this PR, since they are already in the division branch. Going to reopen.

@leonardoalt leonardoalt reopened this Dec 3, 2017

@chriseth chriseth added the in progress label Dec 3, 2017

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Dec 3, 2017

Member

Ok, I see now.
Commits 12f31d8 to acaaccf were from branch trackVariables, and were already merged into develop.
Commits 8a5f940 to 74814bd were from branch division, and are the ones about to be merged by PR #3032.
GH shows the commits from trackVariables because division doesn't know about them.
Since this PR depends on all of them, I guess it's better to wait for division to be merged into develop, and then create a PR directly to develop.
What do you think?

Member

leonardoalt commented Dec 3, 2017

Ok, I see now.
Commits 12f31d8 to acaaccf were from branch trackVariables, and were already merged into develop.
Commits 8a5f940 to 74814bd were from branch division, and are the ones about to be merged by PR #3032.
GH shows the commits from trackVariables because division doesn't know about them.
Since this PR depends on all of them, I guess it's better to wait for division to be merged into develop, and then create a PR directly to develop.
What do you think?

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 5, 2017

Member

@leonardoalt it should be possible to rebase now since both PRs have been merged

Member

axic commented Dec 5, 2017

@leonardoalt it should be possible to rebase now since both PRs have been merged

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Dec 5, 2017

Member

@axic Cool. I guess it doesn't really make sense anymore to create a PR into division, since develop is the branch with the code from trackVariables and division. So I'd say it's better to create two new PRs into develop, one for the ite variables and one for loops (this). This way each PR gets less confusing and easier to review.

Member

leonardoalt commented Dec 5, 2017

@axic Cool. I guess it doesn't really make sense anymore to create a PR into division, since develop is the branch with the code from trackVariables and division. So I'd say it's better to create two new PRs into develop, one for the ite variables and one for loops (this). This way each PR gets less confusing and easier to review.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 5, 2017

Member

@leonardoalt you can change the merge destination in the Github UI. There should be a dropdown next to the merge destination or an edit button.

Member

axic commented Dec 5, 2017

@leonardoalt you can change the merge destination in the Github UI. There should be a dropdown next to the merge destination or an edit button.

@axic axic changed the base branch from division to develop Dec 5, 2017

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 5, 2017

Member

@leonardoalt just did it myself. Also please always use develop as the destination and not other PRs. That is our current process.

Member

axic commented Dec 5, 2017

@leonardoalt just did it myself. Also please always use develop as the destination and not other PRs. That is our current process.

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Dec 5, 2017

Member

@axic ah ok, didn't know that, thanks. Rebased. I'll fix the other PR as well.

Member

leonardoalt commented Dec 5, 2017

@axic ah ok, didn't know that, thanks. Rebased. I'll fix the other PR as well.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 11, 2017

Member

@leonardoalt so in what order are these two PRs laid out? Can we split these PRs into smaller bite size chunks?

Member

axic commented Dec 11, 2017

@leonardoalt so in what order are these two PRs laid out? Can we split these PRs into smaller bite size chunks?

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Dec 11, 2017

Member

@axic PR #3217 comes first. I can make them smaller, starting with keeping track of the path conditions I think (before the ite vars). Should I modify #3217 so that it starts with simpler code, or create a new one for that?

Member

leonardoalt commented Dec 11, 2017

@axic PR #3217 comes first. I can make them smaller, starting with keeping track of the path conditions I think (before the ite vars). Should I modify #3217 so that it starts with simpler code, or create a new one for that?

);
m_interface->push();
m_interface->addAssertion(expr(_op));
m_maximizationResult = m_interface->maximize(toMinMax);

This comment has been minimized.

@chriseth

chriseth Dec 11, 2017

Contributor

What happens if this is used in something like while (f(a < b)) { ... }, where the f ignores its argument and just depends on side-effects?

@chriseth

chriseth Dec 11, 2017

Contributor

What happens if this is used in something like while (f(a < b)) { ... }, where the f ignores its argument and just depends on side-effects?

This comment has been minimized.

@leonardoalt

leonardoalt Dec 11, 2017

Member

That's one of the things I wanted to discuss. For the beginning I wanted to support only binary comparison operations (except = and !=) as the condition. I followed from m_currentFunction the usage of class members to keep track of the current state with the new m_currentLoopCondition, but it indeed doesn't work in the case you mentioned. So in order to support exactly what I wanted at first, the check would have to be "is the condition one of the supported operators?" in the scope of the loop, which looks like a hack in the pattern. So I'm still not sure about the best way to handle that...

@leonardoalt

leonardoalt Dec 11, 2017

Member

That's one of the things I wanted to discuss. For the beginning I wanted to support only binary comparison operations (except = and !=) as the condition. I followed from m_currentFunction the usage of class members to keep track of the current state with the new m_currentLoopCondition, but it indeed doesn't work in the case you mentioned. So in order to support exactly what I wanted at first, the check would have to be "is the condition one of the supported operators?" in the scope of the loop, which looks like a hack in the pattern. So I'm still not sure about the best way to handle that...

This comment has been minimized.

@chriseth

chriseth Dec 12, 2017

Contributor

Yeah, I think you should check in the loop whether it conforms to the pattern. lots of dynamic_castss involved, but I don't have a better solution for now.

@chriseth

chriseth Dec 12, 2017

Contributor

Yeah, I think you should check in the loop whether it conforms to the pattern. lots of dynamic_castss involved, but I don't have a better solution for now.

This comment has been minimized.

@leonardoalt

leonardoalt Dec 15, 2017

Member

Gonna go with that then, thanks.

@leonardoalt

leonardoalt Dec 15, 2017

Member

Gonna go with that then, thanks.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Dec 11, 2017

Member

@leonardoalt:

I can make them smaller, starting with keeping track of the path conditions I think (before the ite vars). Should I modify #3217

Cool, having them smaller eases review and speeds up the merging process. You can create a new one for that simple change and then rebase the one which depends on it. I'd like to merge at least two of your bite-size PRs this week.

Member

axic commented Dec 11, 2017

@leonardoalt:

I can make them smaller, starting with keeping track of the path conditions I think (before the ite vars). Should I modify #3217

Cool, having them smaller eases review and speeds up the merging process. You can create a new one for that simple change and then rebase the one which depends on it. I'd like to merge at least two of your bite-size PRs this week.

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Dec 11, 2017

Member

@axic Ok, will do.

Member

leonardoalt commented Dec 11, 2017

@axic Ok, will do.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Jan 5, 2018

Member

@leonardoalt is this the next PR in the series?

Member

axic commented Jan 5, 2018

@leonardoalt is this the next PR in the series?

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Jan 5, 2018

Member

@axic Yep, still requires some discussion though. If this is supported, I would suggest that the user should have a way to give a general upper bound. @chriseth This could be related to what we talked about some time ago (pre and post conditions).

Member

leonardoalt commented Jan 5, 2018

@axic Yep, still requires some discussion though. If this is supported, I would suggest that the user should have a way to give a general upper bound. @chriseth This could be related to what we talked about some time ago (pre and post conditions).

}
void Z3Interface::reset()
{
m_constants.clear();
m_functions.clear();
m_solver.reset();
if (m_optimizer != nullptr)
delete m_optimizer;
m_optimizer = new z3::optimize(m_context);

This comment has been minimized.

@axic

axic Apr 11, 2018

Member

Doesn't z3::optimize has a reset function instead?

@axic

axic Apr 11, 2018

Member

Doesn't z3::optimize has a reset function instead?

This comment has been minimized.

@chriseth

chriseth Apr 11, 2018

Contributor

Oh wow, please just wrap that inside a smart pointer.

@chriseth

chriseth Apr 11, 2018

Contributor

Oh wow, please just wrap that inside a smart pointer.

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Apr 12, 2018

Member

I need to rebase this PR and work on it a bit, there were multiple changes in the SMTChecker that will affect this.

Member

leonardoalt commented Apr 12, 2018

I need to rebase this PR and work on it a bit, there were multiple changes in the SMTChecker that will affect this.

@axic

This comment has been minimized.

Show comment
Hide comment
@axic

axic Jun 12, 2018

Member

@leonardoalt is this still a PR to be finished? Is it worth working off this or due to the changes better to start form scratch?

Member

axic commented Jun 12, 2018

@leonardoalt is this still a PR to be finished? Is it worth working off this or due to the changes better to start form scratch?

@leonardoalt

This comment has been minimized.

Show comment
Hide comment
@leonardoalt

leonardoalt Jun 13, 2018

Member

The SMTChecker has been changing a lot, so it's probably better to close this one and I'll start from scratch reusing some code.

Member

leonardoalt commented Jun 13, 2018

The SMTChecker has been changing a lot, so it's probably better to close this one and I'll start from scratch reusing some code.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment