[SMTChecker] Support addmod and mulmod.

libsolidity/formal/BMC.cpp

@@ -390,8 +390,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
 	case FunctionType::Kind::BlockHash:
-	case FunctionType::Kind::AddMod:
-	case FunctionType::Kind::MulMod:
 		SMTEncoder::endVisit(_funCall);
 		abstractFunctionCall(_funCall);
 		break;
@@ -410,6 +408,9 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		);
 		break;
 	}
+	case FunctionType::Kind::AddMod:
+	case FunctionType::Kind::MulMod:
+		[[fallthrough]];
 	default:
 		SMTEncoder::endVisit(_funCall);
 		break;
@@ -443,6 +444,18 @@ void BMC::visitRequire(FunctionCall const& _funCall)
 		);
 }
 
+void BMC::visitAddMulMod(FunctionCall const& _funCall)
+{
+	solAssert(_funCall.arguments().at(2), "");
+	addVerificationTarget(
+		VerificationTarget::Type::DivByZero,
+		expr(*_funCall.arguments().at(2)),
+		&_funCall
+	);
+
+	SMTEncoder::visitAddMulMod(_funCall);
+}
+
 void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(shouldInlineFunctionCall(_funCall), "");

libsolidity/formal/BMC.h

@@ -95,6 +95,7 @@ private:
 	//@{
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
+	void visitAddMulMod(FunctionCall const& _funCall) override;
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);

libsolidity/formal/CHC.cpp

@@ -497,6 +497,24 @@ void CHC::visitAssert(FunctionCall const& _funCall)
 	m_context.addAssertion(errorFlag().currentValue() == previousError);
 }
 
+void CHC::visitAddMulMod(FunctionCall const& _funCall)
+{
+	auto previousError = errorFlag().currentValue();
+	errorFlag().increaseIndex();
+
+	addVerificationTarget(
+		&_funCall,
+		VerificationTarget::Type::DivByZero,
+		errorFlag().currentValue()
+	);
+
+	solAssert(_funCall.arguments().at(2), "");
+	smtutil::Expression target = expr(*_funCall.arguments().at(2)) == 0 && errorFlag().currentValue() == newErrorId(_funCall);
+	m_context.addAssertion((errorFlag().currentValue() == previousError) || target);
+
+	SMTEncoder::visitAddMulMod(_funCall);
+}
+
 void CHC::internalFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(m_currentContract, "");
@@ -1158,6 +1176,11 @@ void CHC::checkVerificationTargets()
 					errorReporterId = overflowErrorId;
 				}
 			}
+			else if (target.type == VerificationTarget::Type::DivByZero)
+			{
+				satMsg = "Division by zero happens here.";
+				errorReporterId = 4281_error;
+			}
 			else
 				solAssert(false, "");
 

libsolidity/formal/CHC.h

@@ -83,6 +83,7 @@ private:
 	void endVisit(Continue const& _node) override;
 
 	void visitAssert(FunctionCall const& _funCall);
+	void visitAddMulMod(FunctionCall const& _funCall) override;
 	void internalFunctionCall(FunctionCall const& _funCall);
 	void externalFunctionCall(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);

libsolidity/formal/SMTEncoder.cpp

@@ -632,8 +632,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
 	case FunctionType::Kind::BlockHash:
+		break;
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
+		visitAddMulMod(_funCall);
 		break;
 	case FunctionType::Kind::Send:
 	case FunctionType::Kind::Transfer:
@@ -738,6 +740,24 @@ void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
 		m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
+void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
+{
+	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	solAssert(kind == FunctionType::Kind::AddMod || kind == FunctionType::Kind::MulMod, "");
+	auto const& args = _funCall.arguments();
+	solAssert(args.at(0) && args.at(1) && args.at(2), "");
+	auto x = expr(*args.at(0));
+	auto y = expr(*args.at(1));
+	auto k = expr(*args.at(2));
+	m_context.addAssertion(k != 0);
+
+	if (kind == FunctionType::Kind::AddMod)
+		defineExpr(_funCall, (x + y) % k);
+	else
+		defineExpr(_funCall, (x * y) % k);
+}
+
 void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();

libsolidity/formal/SMTEncoder.h

@@ -137,6 +137,7 @@ protected:
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
 	void visitGasLeft(FunctionCall const& _funCall);
+	virtual void visitAddMulMod(FunctionCall const& _funCall);
 	void visitObjectCreation(FunctionCall const& _funCall);
 	void visitTypeConversion(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);