Merge pull request #6235 from ethereum/smt_large_rational

[SMTChecker] Shortcut RationalNumber expressions

Changelog.md

@@ -14,6 +14,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal compiler error when contract contains too large rational number.
  * Type system: Detect if a contract's base uses types that require the experimental abi encoder while the contract still uses the old encoder
  * Yul Optimizer: Fix visitation order bug for the structural simplifier.
 

libsolidity/formal/SMTChecker.cpp

@@ -374,6 +374,9 @@ void SMTChecker::checkOverflow(OverflowTarget& _target)
 
 void SMTChecker::endVisit(UnaryOperation const& _op)
 {
+	if (_op.annotation().type->category() == Type::Category::RationalNumber)
+		return;
+
 	switch (_op.getOperator())
 	{
 	case Token::Not: // !
@@ -431,8 +434,21 @@ void SMTChecker::endVisit(UnaryOperation const& _op)
 	}
 }
 
+bool SMTChecker::visit(UnaryOperation const& _op)
+{
+	return !shortcutRationalNumber(_op);
+}
+
+bool SMTChecker::visit(BinaryOperation const& _op)
+{
+	return !shortcutRationalNumber(_op);
+}
+
 void SMTChecker::endVisit(BinaryOperation const& _op)
 {
+	if (_op.annotation().type->category() == Type::Category::RationalNumber)
+		return;
+
 	if (TokenTraits::isArithmeticOp(_op.getOperator()))
 		arithmeticOperation(_op);
 	else if (TokenTraits::isCompareOp(_op.getOperator()))
@@ -908,6 +924,21 @@ void SMTChecker::defineGlobalFunction(string const& _name, Expression const& _ex
 	}
 }
 
+bool SMTChecker::shortcutRationalNumber(Expression const& _expr)
+{
+	if (_expr.annotation().type->category() == Type::Category::RationalNumber)
+	{
+		auto rationalType = dynamic_cast<RationalNumberType const*>(_expr.annotation().type.get());
+		solAssert(rationalType, "");
+		if (rationalType->isNegative())
+			defineExpr(_expr, smt::Expression(u2s(rationalType->literalValue(nullptr))));
+		else
+			defineExpr(_expr, smt::Expression(rationalType->literalValue(nullptr)));
+		return true;
+	}
+	return false;
+}
+
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 {
 	switch (_op.getOperator())

libsolidity/formal/SMTChecker.h

@@ -71,7 +71,9 @@ private:
 	void endVisit(VariableDeclarationStatement const& _node) override;
 	void endVisit(Assignment const& _node) override;
 	void endVisit(TupleExpression const& _node) override;
+	bool visit(UnaryOperation const& _node) override;
 	void endVisit(UnaryOperation const& _node) override;
+	bool visit(BinaryOperation const& _node) override;
 	void endVisit(BinaryOperation const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
 	void endVisit(Identifier const& _node) override;
@@ -80,6 +82,9 @@ private:
 	bool visit(MemberAccess const& _node) override;
 	void endVisit(IndexAccess const& _node) override;
 
+	/// Do not visit subtree if node is a RationalNumber.
+	/// Symbolic _expr is the rational literal.
+	bool shortcutRationalNumber(Expression const& _expr);
 	void arithmeticOperation(BinaryOperation const& _op);
 	void compareOperation(BinaryOperation const& _op);
 	void booleanOperation(BinaryOperation const& _op);

libsolidity/formal/SolverInterface.h

@@ -118,6 +118,7 @@ public:
 	explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
 	Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
 	Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
+	Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
 	Expression(bigint const& _number): Expression(_number.str(), Kind::Int) {}
 
 	Expression(Expression const&) = default;

test/libsolidity/smtCheckerTests/simple/static_array.sol

@@ -7,4 +7,3 @@ contract C
 	int[3*1] x;
 }
 // ----
-// Warning: (153-156): Assertion checker does not yet implement this operator on non-integer types.

test/libsolidity/smtCheckerTests/types/rational_large_1.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract c {
+	function f() public pure returns (uint) {
+		uint x = 8e130%9;
+		assert(x == 8);
+		assert(x != 8);
+	}
+}
+// ----
+// Warning: (128-142): Assertion violation happens here