Merge pull request #9159 from ethereum/smt_nondet_mod

[SMTChecker] Replace explicit mod by slack variables

libsolidity/formal/EncodingContext.cpp

@@ -32,12 +32,23 @@ EncodingContext::EncodingContext():
 void EncodingContext::reset()
 {
 	resetAllVariables();
+	resetSlackId();
 	m_expressions.clear();
 	m_globalContext.clear();
 	m_state.reset();
 	m_assertions.clear();
 }
 
+void EncodingContext::resetSlackId()
+{
+	m_nextSlackId = 0;
+}
+
+unsigned EncodingContext::newSlackId()
+{
+	return m_nextSlackId++;
+}
+
 void EncodingContext::clear()
 {
 	m_variables.clear();

libsolidity/formal/EncodingContext.h

@@ -40,6 +40,10 @@ public:
 	/// alive because of state variables and inlined function calls.
 	/// To be used in the beginning of a root function visit.
 	void reset();
+	/// Resets the fresh id for slack variables.
+	void resetSlackId();
+	/// Returns the current fresh slack id and increments it.
+	unsigned newSlackId();
 	/// Clears the entire context, erasing everything.
 	/// To be used before a model checking engine starts.
 	void clear();
@@ -168,6 +172,9 @@ private:
 	/// Whether to conjoin assertions in the assertion stack.
 	bool m_accumulateAssertions = true;
 	//@}
+
+	/// Fresh ids for slack variables to be created deterministically.
+	unsigned m_nextSlackId = 0;
 };
 
 }

libsolidity/formal/SMTEncoder.cpp

@@ -1204,7 +1204,7 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	smtutil::Expression const& _left,
 	smtutil::Expression const& _right,
 	TypePointer const& _commonType,
-	Expression const&
+	Expression const& _operation
 )
 {
 	static set<Token> validOperators{
@@ -1227,39 +1227,66 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 	else
 		intType = TypeProvider::uint256();
 
-	smtutil::Expression valueNoMod(
-		_op == Token::Add ? _left + _right :
-		_op == Token::Sub ? _left - _right :
-		_op == Token::Div ? division(_left, _right, *intType) :
-		_op == Token::Mul ? _left * _right :
-		/*_op == Token::Mod*/ _left % _right
-	);
+	auto valueUnbounded = [&]() -> smtutil::Expression {
+		switch (_op)
+		{
+		case Token::Add: return _left + _right;
+		case Token::Sub: return _left - _right;
+		case Token::Mul: return _left * _right;
+		case Token::Div: return division(_left, _right, *intType);
+		case Token::Mod: return _left % _right;
+		default: solAssert(false, "");
+		}
+	}();
 
 	if (_op == Token::Div || _op == Token::Mod)
+	{
 		m_context.addAssertion(_right != 0);
 
+		// mod and unsigned division never underflow/overflow
+		if (_op == Token::Mod || !intType->isSigned())
+			return {valueUnbounded, valueUnbounded};
+
+		// The only case where division overflows is
+		// - type is signed
+		// - LHS is type.min
+		// - RHS is -1
+		// the result is then -(type.min), which wraps back to type.min
+		smtutil::Expression maxLeft = _left == smt::minValue(*intType);
+		smtutil::Expression minusOneRight = _right == -1;
+		smtutil::Expression wrap = smtutil::Expression::ite(maxLeft && minusOneRight, smt::minValue(*intType), valueUnbounded);
+		return {wrap, valueUnbounded};
+	}
+
 	auto symbMin = smt::minValue(*intType);
 	auto symbMax = smt::maxValue(*intType);
 
 	smtutil::Expression intValueRange = (0 - symbMin) + symbMax + 1;
+	string suffix = to_string(_operation.id()) + "_" + to_string(m_context.newSlackId());
+	smt::SymbolicIntVariable k(intType, intType, "k_" + suffix, m_context);
+	smt::SymbolicIntVariable m(intType, intType, "m_" + suffix, m_context);
+
+	// To wrap around valueUnbounded in case of overflow or underflow, we replace it with a k, given:
+	// 1. k + m * intValueRange = valueUnbounded
+	// 2. k is in range of the desired integer type
+	auto wrap = k.currentValue();
+	m_context.addAssertion(valueUnbounded == (k.currentValue() + intValueRange * m.currentValue()));
+	m_context.addAssertion(k.currentValue() >= symbMin);
+	m_context.addAssertion(k.currentValue() <= symbMax);
+
+	// TODO this could be refined:
+	// for unsigned types it's enough to check only the upper bound.
 	auto value = smtutil::Expression::ite(
-		valueNoMod > symbMax,
-		valueNoMod % intValueRange,
+		valueUnbounded > symbMax,
+		wrap,
 		smtutil::Expression::ite(
-			valueNoMod < symbMin,
-			valueNoMod % intValueRange,
-			valueNoMod
+			valueUnbounded < symbMin,
+			wrap,
+			valueUnbounded
 		)
 	);
 
-	if (intType->isSigned())
-		value = smtutil::Expression::ite(
-			value > symbMax,
-			value - intValueRange,
-			value
-		);
-
-	return {value, valueNoMod};
+	return {value, valueUnbounded};
 }
 
 void SMTEncoder::compareOperation(BinaryOperation const& _op)

test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol

@@ -22,4 +22,3 @@ contract C
 	}
 }
 // ----
-// Warning: (130-144): Error trying to invoke SMT solver.

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -14,6 +14,4 @@ contract C
 	}
 }
 // ----
-// Warning: (296-309): Error trying to invoke SMT solver.
 // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
-// Warning: (296-309): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -19,7 +19,5 @@ contract LoopFor2 {
 	}
 }
 // ----
-// Warning: (317-337): Error trying to invoke SMT solver.
-// Warning: (317-337): Assertion violation happens here
 // Warning: (341-360): Assertion violation happens here
 // Warning: (364-383): Assertion violation happens here