[SMTChecker] Integration with CVC4 by leonardoalt · Pull Request #3840 · argotorg/solidity

leonardoalt · 2018-04-06T16:12:32Z

Added CVC4 as an option for the SMT backend.
Z3 is still the default solver. CVC4 is only used when Z3 is not available.
The next step is writing the double solver that uses both and solves everything.

axic

Since the interface selection is done as if (z3) use_z3 elseif (cvc4) use_cvc4 else use_file the cmake should be updated to reflect that.

e.g. no point displaying the warning if z3 is not found and no point checking for cvc4 if z3 is found.

leonardoalt · 2018-04-06T16:29:08Z

This was done in preparation for the next step when we use both, in which case it makes sense to check for CVC4 even if Z3 is found.

leonardoalt · 2018-04-07T10:50:02Z

@axic Committed a fix. Will squash after review is finished

axic · 2018-04-09T10:14:36Z

The makefile changes look good.

axic · 2018-04-09T10:15:33Z

libsolidity/formal/CVC4Interface.cpp

+	return arguments[0];
+}
+
+CVC4::Type CVC4Interface::cvc4Sort(Sort _sort)


I'd name this toCVC4Sort.

Ok, noticed this follows the naming convention from Z3. I may just do a name refactoring as a separate step on all three (z3, smt, cvc4).

What's the smt case?

(*)SMTLibInterface

Ok now I remember ;)

axic · 2018-04-09T10:19:50Z

libsolidity/formal/CVC4Interface.cpp

+	return make_pair(result, values);
+}
+
+CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)


This seems to be a lot of copy paste from Z3, not sure how this could be shared between the two, but probably at least the arity map could be?

Perhaps we should have a validate() function on Expression which does the arity validation.

True, that could be shared. But same case with the rest, I mean, the goal of the function is exactly to translate from Solidity's internal SMT representation to Z3/CVC4

I was mostly wondering how could we improve this, but as part of this PR I would say the only thing to do is pull out the arity validation to the Expression class (and also check it in SMTLibInterface, which currently ignores it due to the flexible nature of S-expressions), that is a low hanging fruit.

Probably bool valid() const is a good idea, which then can be part of an assertion (solAssert(_expr.isValid(), "") in the interfaces.

Yep. I would also give as parameter the size of the arguments vector that the interface computed

axic · 2018-04-09T10:20:57Z

libsolidity/formal/CVC4Interface.cpp

+	}
+}
+
+pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const& _expressionsToEvaluate)


This seems to be a copy of Z3's too, but not sure how it can be refactored.

Also not sure how this could be refactored. The structure is the same, and the changes are exactly what are actually different between Z3 and CVC4: results enums, methods to get models, etc

axic · 2018-04-09T12:48:35Z

libsolidity/formal/SolverInterface.h


+	/// Checks whether this operator has a valid arity based on its name.
+	/// _arity is the arity of the operator in the solver.
+	bool isValid(unsigned _arity) const


Shouldn't this be only dependant on the internal state (m_arguments.size())?

It is indirectly. Z3 and CVC4 interfaces use the _expr.arguments to build the correspondent vector of arguments. It should be the same in the end, it just checks one more thing this way

I'm not sure if it is better this way or to have two different assertions. I think this isValid would need to be local to the Expression class.

Makes sense. I'll make it two assertions then, to keep it safe

Actually I don't think we need the second assertion.

axic · 2018-04-09T13:11:01Z

Also needs a changelog entry.

chriseth · 2018-04-09T13:27:21Z

libsolidity/formal/CVC4Interface.cpp

+CVC4Interface::CVC4Interface():
+	m_solver(&m_context)
+{
+	m_solver.setOption("produce-models", true);


Better to just call reset here?

chriseth · 2018-04-09T13:28:22Z

libsolidity/formal/CVC4Interface.cpp

+	{
+		m_solver.assertFormula(toCVC4Expr(_expr));
+	}
+	catch (CVC4::TypeCheckingException &)


No space in front of &. Also should use const&.

leonardoalt · 2018-04-10T08:17:30Z

Added Changelog entry and fixed review suggestions

axic · 2018-04-11T19:32:19Z

isValid had to be removed from smtlib, since its current version only checks for the "native operators". Both z3/cvc4 will try to replace constants and user functions before hitting isValid.

We may want to change that to only validate if the name is a native operator.

chriseth · 2018-04-11T20:12:56Z

libsolidity/formal/SolverInterface.h

+	/// Checks whether this operator has a valid arity based on its name.
+	bool isValid() const
+	{
+		static std::map<std::string, unsigned> operatorsArity{


Could be const.

chriseth · 2018-04-11T20:13:36Z

libsolidity/formal/SolverInterface.h

 	Expression& operator=(Expression const&) = default;
 	Expression& operator=(Expression&&) = default;

+	/// Checks whether this operator has a valid arity based on its name.


The comments suggests that the name of the function is not the best ;)

hasCorrectArity?

chriseth · 2018-04-11T20:15:32Z

libsolidity/formal/CVC4Interface.cpp

+	else if (n == "*")
+		return m_context.mkExpr(CVC4::kind::MULT, arguments[0], arguments[1]);
+	else if (n == "/")
+		return m_context.mkExpr(CVC4::kind::INTS_DIVISION_TOTAL, arguments[0], arguments[1]);


I remember the rounding was weird for negative integers in z3, so I think we added a higher-level workaround for signed integers.

What happens at division by zero?

The workaround was added in SMTChecker, right?

INTS_DIVISION_TOTAL returns 0 for division by 0.

Yes, perfect!

leonardoalt · 2018-04-12T08:45:51Z

@axic Good catch, SMTLib will return for constants before, but not for new functions.
We could have two functions in the SolverInterface, the one that was just introduced, and another one that does the same but is also fine with new functions. This way, Z3 and CVC4 can use the restricted version, since they know that at that point the expression should be a native operator.

axic · 2018-04-17T08:44:29Z

@chriseth OK to merge now?

@leonardoalt can you rebase to ensure the changelog entry is in the right spot?

chriseth · 2018-04-17T09:41:58Z

Ok to merge. We are basically still in the same mode, since we need to create the bugfix release, but let's try anyway.

axic · 2018-04-17T11:27:52Z

@chriseth rebased and applied changes, please review

chriseth · 2018-04-17T12:04:03Z

libsolidity/formal/CVC4Interface.h

+	void pop() override;
+
+	Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
+	Expression newInteger(std::string _name) override;


These should all use const& - don't they in the base class?

They're also just string in the base class, where they're moved to the Expression

Ah sorry, I didn't see the move.

axic suggested changes Apr 6, 2018

View reviewed changes

leonardoalt force-pushed the smt_cvc4 branch from d3a1a6d to f17f1dc Compare April 7, 2018 10:49

axic reviewed Apr 9, 2018

View reviewed changes

leonardoalt force-pushed the smt_cvc4 branch 2 times, most recently from 5e573f0 to 970af2b Compare April 9, 2018 11:28

axic reviewed Apr 9, 2018

View reviewed changes

chriseth suggested changes Apr 9, 2018

View reviewed changes

leonardoalt force-pushed the smt_cvc4 branch from 970af2b to 507f325 Compare April 10, 2018 06:49

leonardoalt force-pushed the smt_cvc4 branch 2 times, most recently from 2aeec85 to f3ef945 Compare April 11, 2018 16:26

axic force-pushed the smt_cvc4 branch from f3ef945 to 2f721af Compare April 11, 2018 18:34

axic previously approved these changes Apr 11, 2018

View reviewed changes

axic dismissed their stale review via c72158d April 11, 2018 19:30

axic force-pushed the smt_cvc4 branch from 2f721af to c72158d Compare April 11, 2018 19:30

axic previously approved these changes Apr 11, 2018

View reviewed changes

chriseth suggested changes Apr 11, 2018

View reviewed changes

axic self-assigned this Apr 17, 2018

[SMTChecker] Integration with CVC4

ae3350a

axic dismissed their stale review via ae3350a April 17, 2018 11:27

axic force-pushed the smt_cvc4 branch from c72158d to ae3350a Compare April 17, 2018 11:27

chriseth reviewed Apr 17, 2018

View reviewed changes

chriseth approved these changes Apr 17, 2018

View reviewed changes

axic merged commit f925747 into develop Apr 17, 2018

axic deleted the smt_cvc4 branch April 17, 2018 13:35

Conversation

leonardoalt commented Apr 6, 2018

Uh oh!

axic left a comment

Choose a reason for hiding this comment

Uh oh!

leonardoalt commented Apr 6, 2018

Uh oh!

leonardoalt commented Apr 7, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

axic commented Apr 9, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

axic Apr 9, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

axic Apr 9, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

leonardoalt Apr 9, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

axic commented Apr 9, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

leonardoalt commented Apr 10, 2018

Uh oh!

axic commented Apr 11, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

leonardoalt commented Apr 12, 2018

Uh oh!

axic commented Apr 17, 2018

leonardoalt commented Apr 7, 2018 •

edited

Loading

axic Apr 9, 2018 •

edited

Loading

axic Apr 9, 2018 •

edited

Loading

leonardoalt Apr 9, 2018 •

edited

Loading