SMT checker for various things

[chriseth]

This can now handle conditions and while loops. It checks for conditions being constant and correctly erases knowledge about local variables at control flow join paths.

[chriseth]

This can be merged in the current state.

[axic]

Consider merging #3030 and rebase this after.

[chriseth]

Is #3030 in conflict with this?

[axic]

It doesn't seem to be used in this PR, but it was missing anyway.

[axic]

Should this be reviewed/merged or #3032?

[chriseth]

#3032 is an extension of this. Please review this one.

[axic]

This is failing tests though:

/home/travis/build/ethereum/solidity/libsolidity/formal/SMTChecker.cpp(674): fatal error in "void dev::solidity::SMTChecker::setZeroValue(const dev::solidity::Declaration &)": std::exception: 
/home/travis/build/ethereum/solidity/test/libsolidity/SMTChecker.cpp(91): last checkpoint

[chriseth]

Cherry-picked a commit from #3032 that should fix the tests.

[chriseth]

The remaining failure seems to be a travis issue.

[axic]

Any reasonable way to split this? It seems to do a lot of different improvements.

[chriseth]

Can you review the individual commits? "track variables" is probably the largest. I can try to split it up, but I fear it will be a lot of work.

[axic]

I think I can pull out the renaming and the exceptions easily, the rest is mushy to me at the moment at least.

Based on the tests it seems it supports at least more variables, branching, bools.

[axic]

Ah, >= was duplicated.

[axic]

Rebased on #3091.

[axic]

@chriseth you've pushed an old version over the rebased one. Any reason for it? In any case, please rebase.

[chriseth]

You mean I rebased on top of an old version? Sorry, I don't know why that happened. I hope I did not lose any commits. Fixing...

[axic]

I've rebased it on top of the cleanup branch, but hasn't changed anything. It should be safe as long as you had the last version before that :)

[axic]

Are there are any asserts which should be solUnimplementedAssert?

[chriseth]

I will take a look at the next iteration.

[chriseth]

@axic can this be merged? We already have two other finished pull requests waiting on top of this one.

[axic]

Rebased before merging as it was fairly old (had circleci too).