Merge remote-tracking branch 'origin/develop' into HEAD

libsolidity/formal/BMC.cpp

@@ -385,13 +385,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		SMTEncoder::endVisit(_funCall);
 		internalOrExternalFunctionCall(_funCall);
 		break;
-	case FunctionType::Kind::KECCAK256:
-	case FunctionType::Kind::ECRecover:
-	case FunctionType::Kind::SHA256:
-	case FunctionType::Kind::RIPEMD160:
-		SMTEncoder::endVisit(_funCall);
-		abstractFunctionCall(_funCall);
-		break;
 	case FunctionType::Kind::Send:
 	case FunctionType::Kind::Transfer:
 	{
@@ -408,6 +401,10 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		SMTEncoder::endVisit(_funCall);
 		break;
 	}
+	case FunctionType::Kind::KECCAK256:
+	case FunctionType::Kind::ECRecover:
+	case FunctionType::Kind::SHA256:
+	case FunctionType::Kind::RIPEMD160:
 	case FunctionType::Kind::BlockHash:
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
@@ -485,16 +482,6 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 	createReturnedExpressions(_funCall);
 }
 
-void BMC::abstractFunctionCall(FunctionCall const& _funCall)
-{
-	vector<smtutil::Expression> smtArguments;
-	for (auto const& arg: _funCall.arguments())
-		smtArguments.push_back(expr(*arg));
-	defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
-	m_uninterpretedTerms.insert(&_funCall);
-	setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_context);
-}
-
 void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 {
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
@@ -836,7 +823,7 @@ void BMC::checkCondition(
 			"\nNote that some information is erased after the execution of loops.\n"
 			"You can re-introduce information using require().";
 	if (m_externalFunctionCallHappened)
-		extraComment+=
+		extraComment +=
 			"\nNote that external function calls are not inlined,"
 			" even if the source code of the function is available."
 			" This is due to the possibility that the actual called contract"
@@ -854,7 +841,7 @@ void BMC::checkCondition(
 		if (_callStack.size())
 		{
 			std::ostringstream modelMessage;
-			modelMessage << "\nCounterexample:\n";
+			modelMessage << "Counterexample:\n";
 			solAssert(values.size() == expressionNames.size(), "");
 			map<string, string> sortedModel;
 			for (size_t i = 0; i < values.size(); ++i)
@@ -863,6 +850,7 @@ void BMC::checkCondition(
 
 			for (auto const& eval: sortedModel)
 				modelMessage << "  " << eval.first << " = " << eval.second << "\n";
+
 			m_errorReporter.warning(
 				_errorHappens,
 				_location,

libsolidity/formal/BMC.h

@@ -99,8 +99,6 @@ private:
 	/// Visits the FunctionDefinition of the called function
 	/// if available and inlines the return value.
 	void inlineFunctionCall(FunctionCall const& _funCall);
-	/// Creates an uninterpreted function call.
-	void abstractFunctionCall(FunctionCall const& _funCall);
 	/// Inlines if the function call is internal or external to `this`.
 	/// Erases knowledge about state variables if external.
 	void internalOrExternalFunctionCall(FunctionCall const& _funCall);

libsolidity/formal/CHC.cpp

@@ -120,7 +120,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 		&_contract
 	);
 	addRule(
-		(*implicitConstructorPredicate)({0, state().thisAddress(), state().tx(), state().state()}),
+		(*implicitConstructorPredicate)({0, state().thisAddress(), state().crypto(), state().tx(), state().state()}),
 		implicitConstructorPredicate->functor().name
 	);
 	setCurrentBlock(*implicitConstructorPredicate);
@@ -874,7 +874,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 						auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
 						auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
 
-						vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state(1)};
+						vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state(1)};
 						args += state1 +
 							applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
 							vector<smtutil::Expression>{state().state(2)} +
@@ -1053,7 +1053,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		return smtutil::Expression(true);
 
 	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state()};
+	vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state()};
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	solAssert(funType.kind() == FunctionType::Kind::Internal, "");
@@ -1298,7 +1298,7 @@ void CHC::checkAndReportTarget(
 				_errorReporterId,
 				_scope->location(),
 				"CHC: " + _satMsg,
-				SecondarySourceLocation().append("\nCounterexample:\n" + *cex, SourceLocation{})
+				SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{})
 			);
 		else
 			m_outerErrorReporter.warning(
@@ -1402,9 +1402,13 @@ optional<string> CHC::generateCounterexample(CHCSolverInterface::CexGraph const&
 			}
 		}
 		else
+		{
+			auto modelMsg = formatVariableModel(*stateVars, stateValues, ", ");
 			/// We report the state after every tx in the trace except for the last, which is reported
 			/// first in the code above.
-			path.emplace_back("State: " + formatVariableModel(*stateVars, stateValues, ", "));
+			if (!modelMsg.empty())
+				path.emplace_back("State: " + modelMsg);
+		}
 
 		string txCex = summaryPredicate->formatSummaryCall(summaryArgs);
 		path.emplace_back(txCex);

libsolidity/formal/ModelChecker.cpp

@@ -27,9 +27,11 @@ using namespace solidity::frontend;
 ModelChecker::ModelChecker(
 	ErrorReporter& _errorReporter,
 	map<h256, string> const& _smtlib2Responses,
+	ModelCheckerEngine _engine,
 	ReadCallback::Callback const& _smtCallback,
 	smtutil::SMTSolverChoice _enabledSolvers
 ):
+	m_engine(_engine),
 	m_context(),
 	m_bmc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers),
 	m_chc(m_context, _errorReporter, _smtlib2Responses, _smtCallback, _enabledSolvers)
@@ -41,13 +43,15 @@ void ModelChecker::analyze(SourceUnit const& _source)
 	if (!_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker))
 		return;
 
-	m_chc.analyze(_source);
+	if (m_engine.chc)
+		m_chc.analyze(_source);
 
 	auto solvedTargets = m_chc.safeTargets();
 	for (auto const& target: m_chc.unsafeTargets())
 		solvedTargets[target.first] += target.second;
 
-	m_bmc.analyze(_source, solvedTargets);
+	if (m_engine.bmc)
+		m_bmc.analyze(_source, solvedTargets);
 }
 
 vector<string> ModelChecker::unhandledQueries()

libsolidity/formal/ModelChecker.h

@@ -32,6 +32,8 @@
 #include <libsmtutil/SolverInterface.h>
 #include <liblangutil/ErrorReporter.h>
 
+#include <optional>
+
 namespace solidity::langutil
 {
 class ErrorReporter;
@@ -41,6 +43,34 @@ struct SourceLocation;
 namespace solidity::frontend
 {
 
+struct ModelCheckerEngine
+{
+	bool bmc = false;
+	bool chc = false;
+
+	static constexpr ModelCheckerEngine All() { return {true, true}; }
+	static constexpr ModelCheckerEngine BMC() { return {true, false}; }
+	static constexpr ModelCheckerEngine CHC() { return {false, true}; }
+	static constexpr ModelCheckerEngine None() { return {false, false}; }
+
+	bool none() const { return !any(); }
+	bool any() const { return bmc || chc; }
+	bool all() const { return bmc && chc; }
+
+	static std::optional<ModelCheckerEngine> fromString(std::string const& _engine)
+	{
+		static std::map<std::string, ModelCheckerEngine> engineMap{
+			{"all", All()},
+			{"bmc", BMC()},
+			{"chc", CHC()},
+			{"none", None()}
+		};
+		if (engineMap.count(_engine))
+			return engineMap.at(_engine);
+		return {};
+	}
+};
+
 class ModelChecker
 {
 public:
@@ -49,6 +79,7 @@ public:
 	ModelChecker(
 		langutil::ErrorReporter& _errorReporter,
 		std::map<solidity::util::h256, std::string> const& _smtlib2Responses,
+		ModelCheckerEngine _engine = ModelCheckerEngine::All(),
 		ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(),
 		smtutil::SMTSolverChoice _enabledSolvers = smtutil::SMTSolverChoice::All()
 	);
@@ -64,6 +95,8 @@ public:
 	static smtutil::SMTSolverChoice availableSolvers();
 
 private:
+	ModelCheckerEngine m_engine;
+
 	/// Stores the context of the encoding.
 	smt::EncodingContext m_context;
 

libsolidity/formal/Predicate.cpp

@@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
 	auto const* fun = programFunction();
 	solAssert(fun, "");
 
-	/// The signature of a function summary predicate is: summary(error, this, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in preInputVars.
-	vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size());
+	vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size());
 	vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 	solAssert(last >= _args.begin() && last <= _args.end(), "");
@@ -188,10 +188,9 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
 
 vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
-	/// The signature of an implicit constructor summary predicate is: summary(error, this, txData, preBlockSchainState, postBlockchainState, postStateVars).
+	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of an implicit constructor summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, postStateVars).
 	/// Here we are interested in postStateVars.
-
 	auto stateVars = stateVariables();
 	solAssert(stateVars.has_value(), "");
 
@@ -199,12 +198,12 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 	vector<string>::const_iterator stateLast;
 	if (auto const* function = programFunction())
 	{
-		stateFirst = _args.begin() + 4 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
+		stateFirst = _args.begin() + 5 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else if (programContract())
 	{
-		stateFirst = _args.begin() + 5;
+		stateFirst = _args.begin() + 6;
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else
@@ -220,7 +219,7 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
 
 vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in postInputVars.
 	auto const* function = programFunction();
 	solAssert(function, "");
@@ -230,7 +229,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
 
 	auto const& inParams = function->parameters();
 
-	vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
+	vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
 	vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
@@ -243,7 +242,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
 
 vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in outputVars.
 	auto const* function = programFunction();
 	solAssert(function, "");
@@ -253,7 +252,7 @@ vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) c
 
 	auto const& inParams = function->parameters();
 
-	vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
+	vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 

libsolidity/formal/PredicateInstance.cpp

@@ -30,14 +30,14 @@ namespace solidity::frontend::smt
 smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.state(0)};
+	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.crypto(0), state.state(0)};
 	return _pred(stateExprs + initialStateVariables(_contract, _context));
 }
 
 smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.crypto(0), state.state()};
 	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
@@ -54,7 +54,7 @@ smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition c
 smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context)
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
 	return _pred(stateExprs);
 }
 
@@ -64,7 +64,7 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const
 		return _pred(currentFunctionVariables(*constructor, &_contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
 	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
@@ -118,7 +118,7 @@ vector<smtutil::Expression> currentFunctionVariables(
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)};
+	vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
 	exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
 	exprs += vector<smtutil::Expression>{state.state()};

libsolidity/formal/PredicateSort.cpp

@@ -31,7 +31,7 @@ namespace solidity::frontend::smt
 SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
 {
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract),
+		vector<SortPointer>{_state.thisAddressSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }
@@ -49,7 +49,7 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
 SortPointer implicitConstructorSort(SymbolicState& _state)
 {
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()},
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()},
 		SortProvider::boolSort
 	);
 }
@@ -60,7 +60,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
 		return functionSort(*constructor, &_contract, _state);
 
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }
@@ -72,7 +72,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()} +
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
 			varSorts +
 			inputSorts +
 			vector<SortPointer>{_state.stateSort()} +

libsolidity/formal/PredicateSort.h

@@ -33,7 +33,7 @@ namespace solidity::frontend::smt
  *
  * 1. Interface
  * The idle state of a contract. Signature:
- * interface(this, blockchainState, stateVariables).
+ * interface(this, cryptoFunctions, blockchainState, stateVariables).
  *
  * 2. Nondet interface
  * The nondeterminism behavior of a contract. Signature:
@@ -41,19 +41,19 @@ namespace solidity::frontend::smt
  *
  * 3. Implicit constructor
  * The implicit constructor of a contract, that is, without input parameters. Signature:
- * implicit_constructor(error, this, txData, blockchainState).
+ * implicit_constructor(error, this, cryptoFunctions, txData, blockchainState).
  *
  * 4. Constructor entry/summary
  * The summary of an implicit constructor. Signature:
- * constructor_summary(error, this, txData, blockchainState, blockchainState', stateVariables').
+ * constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables').
  *
  * 5. Function entry/summary
  * The entry point of a function definition. Signature:
- * function_entry(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
+ * function_entry(error, this, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
  *
  * 6. Function body
  * Use for any predicate within a function. Signature:
- * function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables).
+ * function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
  */
 
 /// @returns the interface predicate sort for _contract.

libsolidity/formal/SMTEncoder.cpp

@@ -633,6 +633,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
+		visitCryptoFunction(_funCall);
 		break;
 	case FunctionType::Kind::BlockHash:
 		defineExpr(_funCall, m_context.state().blockhash(expr(*_funCall.arguments().at(0))));
@@ -730,6 +731,38 @@ void SMTEncoder::visitRequire(FunctionCall const& _funCall)
 	addPathImpliedExpression(expr(*args.front()));
 }
 
+void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
+{
+	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	auto arg0 = expr(*_funCall.arguments().at(0));
+	optional<smtutil::Expression> result;
+	if (kind == FunctionType::Kind::KECCAK256)
+		result = smtutil::Expression::select(m_context.state().cryptoFunction("keccak256"), arg0);
+	else if (kind == FunctionType::Kind::SHA256)
+		result = smtutil::Expression::select(m_context.state().cryptoFunction("sha256"), arg0);
+	else if (kind == FunctionType::Kind::RIPEMD160)
+		result = smtutil::Expression::select(m_context.state().cryptoFunction("ripemd160"), arg0);
+	else if (kind == FunctionType::Kind::ECRecover)
+	{
+		auto e = m_context.state().cryptoFunction("ecrecover");
+		auto arg0 = expr(*_funCall.arguments().at(0));
+		auto arg1 = expr(*_funCall.arguments().at(1));
+		auto arg2 = expr(*_funCall.arguments().at(2));
+		auto arg3 = expr(*_funCall.arguments().at(3));
+		auto inputSort = dynamic_cast<smtutil::ArraySort&>(*e.sort).domain;
+		auto ecrecoverInput = smtutil::Expression::tuple_constructor(
+			smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""),
+			{arg0, arg1, arg2, arg3}
+		);
+		result = smtutil::Expression::select(e, ecrecoverInput);
+	}
+	else
+		solAssert(false, "");
+
+	defineExpr(_funCall, *result);
+}
+
 void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
 {
 	string gasLeft = "gasleft()";
@@ -755,11 +788,12 @@ void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
 	auto y = expr(*args.at(1));
 	auto k = expr(*args.at(2));
 	m_context.addAssertion(k != 0);
+	auto const& intType = dynamic_cast<IntegerType const&>(*_funCall.annotation().type);
 
 	if (kind == FunctionType::Kind::AddMod)
-		defineExpr(_funCall, (x + y) % k);
+		defineExpr(_funCall, divModWithSlacks(x + y, k, intType).second);
 	else
-		defineExpr(_funCall, (x * y) % k);
+		defineExpr(_funCall, divModWithSlacks(x * y, k, intType).second);
 }
 
 void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
@@ -1490,8 +1524,8 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
 		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;
+		case Token::Div: return divModWithSlacks(_left, _right, *intType).first;
+		case Token::Mod: return divModWithSlacks(_left, _right, *intType).second;
 		default: solAssert(false, "");
 		}
 	}();
@@ -1693,13 +1727,30 @@ void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
 	defineExpr(_op, smtutil::Expression::bv2int(~bvOperand, isSigned));
 }
 
-smtutil::Expression SMTEncoder::division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type)
+pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
+	smtutil::Expression _left,
+	smtutil::Expression _right,
+	IntegerType const& _type
+)
 {
-	// Signed division in SMTLIB2 rounds differently for negative division.
+	IntegerType const* intType = &_type;
+	string suffix = "div_mod_" + to_string(m_context.newUniqueId());
+	smt::SymbolicIntVariable d(intType, intType, "d_" + suffix, m_context);
+	smt::SymbolicIntVariable r(intType, intType, "r_" + suffix, m_context);
+
+	// x / y = d and x % y = r iff d * y + r = x and
+	// either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned)
+	// or     x < 0 and -abs(y) < r <= 0
+	m_context.addAssertion(((d.currentValue() * _right) + r.currentValue()) == _left);
 	if (_type.isSigned())
-		return signedDivisionEVM(_left, _right);
-	else
-		return _left / _right;
+		m_context.addAssertion(
+			(_left >= 0 && 0 <= r.currentValue() && r.currentValue() < smtutil::abs(_right)) ||
+			(_left < 0 && (0 - smtutil::abs(_right)) < r.currentValue() && r.currentValue() <= 0)
+		);
+	else // unsigned version
+		m_context.addAssertion(0 <= r.currentValue() && r.currentValue() < _right);
+
+	return {d.currentValue(), r.currentValue()};
 }
 
 void SMTEncoder::assignment(
@@ -2114,7 +2165,7 @@ SecondarySourceLocation SMTEncoder::callStackMessage(vector<CallStackEntry> cons
 {
 	SecondarySourceLocation callStackLocation;
 	solAssert(!_callStack.empty(), "");
-	callStackLocation.append("Callstack: ", SourceLocation());
+	callStackLocation.append("Callstack:", SourceLocation());
 	for (auto const& call: _callStack | boost::adaptors::reversed)
 		if (call.second)
 			callStackLocation.append("", call.second->location());

libsolidity/formal/SMTEncoder.h

@@ -36,6 +36,7 @@
 #include <string>
 #include <unordered_map>
 #include <vector>
+#include <utility>
 
 namespace solidity::langutil
 {
@@ -136,6 +137,7 @@ protected:
 	void initFunction(FunctionDefinition const& _function);
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
+	void visitCryptoFunction(FunctionCall const& _funCall);
 	void visitGasLeft(FunctionCall const& _funCall);
 	virtual void visitAddMulMod(FunctionCall const& _funCall);
 	void visitObjectCreation(FunctionCall const& _funCall);
@@ -174,9 +176,14 @@ protected:
 		std::vector<smtutil::Expression> const& _elementValues
 	);
 
-	/// Division expression in the given type. Requires special treatment because
-	/// of rounding for signed division.
-	smtutil::Expression division(smtutil::Expression _left, smtutil::Expression _right, IntegerType const& _type);
+	/// @returns a pair of expressions representing _left / _right and _left mod _right, respectively.
+	/// Uses slack variables and additional constraints to express the results using only operations
+	/// more friendly to the SMT solver (multiplication, addition, subtraction and comparison).
+	std::pair<smtutil::Expression, smtutil::Expression>	divModWithSlacks(
+		smtutil::Expression _left,
+		smtutil::Expression _right,
+		IntegerType const& _type
+	);
 
 	void assignment(VariableDeclaration const& _variable, Expression const& _value);
 	/// Handles assignments to variables of different types.

libsolidity/formal/SymbolicState.cpp

@@ -76,6 +76,7 @@ void SymbolicState::reset()
 	m_thisAddress.resetIndex();
 	m_state.reset();
 	m_tx.reset();
+	m_crypto.reset();
 }
 
 smtutil::Expression SymbolicState::balances() const

libsolidity/formal/SymbolicState.h

@@ -128,6 +128,16 @@ public:
 	smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
 	//@}
 
+	/// Crypto functions.
+	//@{
+	/// @returns the crypto functions represented as a tuple of arrays.
+	smtutil::Expression crypto() const { return m_crypto.value(); }
+	smtutil::Expression crypto(unsigned _idx) const { return m_crypto.value(_idx); }
+	smtutil::SortPointer const& cryptoSort() const { return m_crypto.sort(); }
+	void newCrypto() { m_crypto.newVar(); }
+	smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); }
+	//@}
+
 private:
 	/// Adds _value to _account's balance.
 	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
@@ -171,6 +181,38 @@ private:
 		},
 		m_context
 	};
+
+	BlockchainVariable m_crypto{
+		"crypto",
+		{
+			{"keccak256", std::make_shared<smtutil::ArraySort>(
+				smt::smtSort(*TypeProvider::bytesStorage()),
+				smtSort(*TypeProvider::fixedBytes(32))
+			)},
+			{"sha256", std::make_shared<smtutil::ArraySort>(
+				smt::smtSort(*TypeProvider::bytesStorage()),
+				smtSort(*TypeProvider::fixedBytes(32))
+			)},
+			{"ripemd160", std::make_shared<smtutil::ArraySort>(
+				smt::smtSort(*TypeProvider::bytesStorage()),
+				smtSort(*TypeProvider::fixedBytes(20))
+			)},
+			{"ecrecover", std::make_shared<smtutil::ArraySort>(
+				std::make_shared<smtutil::TupleSort>(
+					"ecrecover_input_type",
+					std::vector<std::string>{"hash", "v", "r", "s"},
+					std::vector<smtutil::SortPointer>{
+						smt::smtSort(*TypeProvider::fixedBytes(32)),
+						smt::smtSort(*TypeProvider::uint(8)),
+						smt::smtSort(*TypeProvider::fixedBytes(32)),
+						smt::smtSort(*TypeProvider::fixedBytes(32))
+					}
+				),
+				smtSort(*TypeProvider::address())
+			)}
+		},
+		m_context
+	};
 };
 
 }