[SMTChecker] Apply const eval to arithmetic binary expressions

Author: Leonardo Alt

Diff for: Changelog.md

@@ -11,6 +11,7 @@ Language Features:
 Compiler Features:
  * Build System: Optionally support dynamic loading of Z3 and use that mechanism for Linux release builds.
  * Code Generator: Avoid memory allocation for default value if it is not used.
+ * SMTChecker: Apply constant evaluation on binary arithmetic expressions.
  * SMTChecker: Create underflow and overflow verification targets for increment/decrement in the CHC engine.
  * SMTChecker: Report struct values in counterexamples from CHC engine.
  * SMTChecker: Support early returns in the CHC engine.

Diff for: libsolidity/formal/SMTEncoder.cpp

@@ -22,6 +22,8 @@
 #include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsolidity/analysis/ConstantEvaluator.h>
+
 #include <libsmtutil/SMTPortfolio.h>
 #include <libsmtutil/Helpers.h>
 
@@ -600,7 +602,8 @@ bool SMTEncoder::visit(BinaryOperation const& _op)
 
 void SMTEncoder::endVisit(BinaryOperation const& _op)
 {
-	if (_op.annotation().type->category() == Type::Category::RationalNumber)
+	/// If _op is const evaluated the RationalNumber shortcut was taken.
+	if (isConstant(_op))
 		return;
 	if (TokenTraits::isBooleanOp(_op.getOperator()))
 		return;
@@ -1628,17 +1631,17 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
 
 bool SMTEncoder::shortcutRationalNumber(Expression const& _expr)
 {
-	if (_expr.annotation().type->category() == Type::Category::RationalNumber)
-	{
-		auto rationalType = dynamic_cast<RationalNumberType const*>(_expr.annotation().type);
-		solAssert(rationalType, "");
-		if (rationalType->isNegative())
-			defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
-		else
-			defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr)));
-		return true;
-	}
-	return false;
+	auto type = isConstant(_expr);
+	if (!type)
+		return false;
+
+	solAssert(type->category() == Type::Category::RationalNumber, "");
+	auto const& rationalType = dynamic_cast<RationalNumberType const&>(*type);
+	if (rationalType.isNegative())
+		defineExpr(_expr, smtutil::Expression(u2s(rationalType.literalValue(nullptr))));
+	else
+		defineExpr(_expr, smtutil::Expression(rationalType.literalValue(nullptr)));
+	return true;
 }
 
 void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
@@ -2660,6 +2663,22 @@ map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEnco
 	return baseArgs;
 }
 
+TypePointer SMTEncoder::isConstant(Expression const& _expr)
+{
+	if (
+		auto type = _expr.annotation().type;
+		type->category() == Type::Category::RationalNumber
+	)
+		return type;
+
+	// _expr may not be constant evaluable.
+	// In that case we ignore any warnings emitted by the constant evaluator,
+	// as it will return nullptr in case of failure.
+	ErrorList l;
+	ErrorReporter e(l);
+	return ConstantEvaluator(e).evaluate(_expr);
+}
+
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);

Diff for: libsolidity/formal/SMTEncoder.h

@@ -83,6 +83,10 @@ class SMTEncoder: public ASTConstVisitor
 	/// @returns the arguments for each base constructor call in the hierarchy of @a _contract.
 	std::map<ContractDefinition const*, std::vector<ASTPointer<frontend::Expression>>> baseArguments(ContractDefinition const& _contract);
 
+	/// @returns a valid RationalNumberType pointer if _expr has type
+	/// RationalNumberType or can be const evaluated, and nullptr otherwise.
+	static TypePointer isConstant(Expression const& _expr);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined

Diff for: test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol

@@ -50,7 +50,9 @@ contract MyConc{
     }
 
 }
+// ====
+// SMTIgnoreCex: yes
 // ----
 // Warning 2519: (773-792): This declaration shadows an existing declaration.
 // Warning 2018: (1009-1086): Function state mutability can be restricted to view
-// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nA = 1, should_be_constant = 0, should_be_constant_2 = 2, not_constant = 0, not_constant_2 = 115792089237316195423570985008687907853269984665640564039457584007913129639926, not_constant_3 = 0\n\nTransaction trace:\nconstructor()
+// Warning 4984: (985-1002): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.

Diff for: test/libsolidity/smtCheckerTests/operators/const_exp_1.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint constant x = 2;
+	uint constant y = x ** 10;
+
+	function f() public view {
+		assert(y == 2 ** 10);
+		assert(y == 1024);
+		assert(y == 14); // should fail
+	}
+}
+// ----
+// Warning 2018: (98-206): Function state mutability can be restricted to pure
+// Warning 6328: (172-187): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, y = 1024\n\n\n\nTransaction trace:\nconstructor()\nState: x = 2, y = 1024\nf()

Diff for: test/libsolidity/smtCheckerTests/operators/constant_propagation_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint constant DEPOSIT_CONTRACT_TREE_DEPTH = 32;
+	uint constant MAX_DEPOSIT_COUNT = 2**DEPOSIT_CONTRACT_TREE_DEPTH - 1;
+	function f() public pure {
+		assert(DEPOSIT_CONTRACT_TREE_DEPTH == 32);
+		assert(MAX_DEPOSIT_COUNT == 4294967295);
+		assert(MAX_DEPOSIT_COUNT == 2); // should fail
+	}
+}
+// ----
+// Warning 6328: (284-314): CHC: Assertion violation happens here.\nCounterexample:\nDEPOSIT_CONTRACT_TREE_DEPTH = 32, MAX_DEPOSIT_COUNT = 4294967295\n\n\n\nTransaction trace:\nconstructor()\nState: DEPOSIT_CONTRACT_TREE_DEPTH = 32, MAX_DEPOSIT_COUNT = 4294967295\nf()