SMTChecker support ABI functions as UFs

libsolidity/formal/CHC.cpp

@@ -916,7 +916,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().crypto(), state().tx(), state().state(1)};
+						vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().abi(), 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)} +
@@ -1160,7 +1160,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		solAssert(false, "Unreachable!");
 	};
 	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().crypto(), state().tx(), state().state()};
+	vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
 
 	auto const* contract = function->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;

libsolidity/formal/Predicate.cpp

@@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
 	auto const* fun = programFunction();
 	solAssert(fun, "");
 
-	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in preInputVars.
-	auto first = _args.begin() + 5 + static_cast<int>(stateVars->size());
+	auto first = _args.begin() + 6 + static_cast<int>(stateVars->size());
 	auto last = first + static_cast<int>(fun->parameters().size());
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 	solAssert(last >= _args.begin() && last <= _args.end(), "");
@@ -189,8 +189,8 @@ string Predicate::formatSummaryCall(vector<smtutil::Expression> const& _args) co
 
 vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expression> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
-	/// The signature of the summary predicate of a contract without constructor is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
+	/// The signature of the summary predicate of a contract without constructor is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, postBlockchainState, preStateVars, postStateVars).
 	/// Here we are interested in postStateVars.
 	auto stateVars = stateVariables();
 	solAssert(stateVars.has_value(), "");
@@ -199,12 +199,12 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
 	vector<smtutil::Expression>::const_iterator stateLast;
 	if (auto const* function = programFunction())
 	{
-		stateFirst = _args.begin() + 5 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
+		stateFirst = _args.begin() + 6 + 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() + 6 + static_cast<int>(stateVars->size());
+		stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size());
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else
@@ -221,7 +221,7 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
 
 vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expression> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in postInputVars.
 	auto const* function = programFunction();
 	solAssert(function, "");
@@ -231,7 +231,7 @@ vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expre
 
 	auto const& inParams = function->parameters();
 
-	auto first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
+	auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
 	auto last = first + static_cast<int>(inParams.size());
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
@@ -245,7 +245,7 @@ vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expre
 
 vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expression> const& _args) const
 {
-	/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
+	/// The signature of a function summary predicate is: summary(error, this, abiFunctions, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
 	/// Here we are interested in outputVars.
 	auto const* function = programFunction();
 	solAssert(function, "");
@@ -255,7 +255,7 @@ vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expr
 
 	auto const& inParams = function->parameters();
 
-	auto first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
+	auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 
@@ -311,6 +311,11 @@ optional<string> Predicate::expressionToString(smtutil::Expression const& _expr,
 		{
 			return {};
 		}
+		catch(invalid_argument const&)
+		{
+			return {};
+		}
+
 		// Limit this counterexample size to 1k.
 		// Some OSs give you "unlimited" memory through swap and other virtual memory,
 		// so purely relying on bad_alloc being thrown is not a good idea.
@@ -382,6 +387,10 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
 		{
 			return true;
 		}
+		catch (invalid_argument const&)
+		{
+			return true;
+		}
 		optional<string> elemStr = expressionToString(_expr.arguments.at(2), _type.baseType());
 		if (!elemStr)
 			return false;

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.crypto(0), state.state(0)};
+	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(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.crypto(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
 	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
@@ -58,7 +58,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
 		return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
 	return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
 }
 
@@ -69,7 +69,7 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co
 		return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
 	state.newState();
 	stateExprs += vector<smtutil::Expression>{state.state()};
 	stateExprs += currentStateVariables(contract, _context);
@@ -145,7 +145,7 @@ vector<smtutil::Expression> currentFunctionVariablesForDefinition(
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(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()};
@@ -162,7 +162,7 @@ vector<smtutil::Expression> currentFunctionVariablesForCall(
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state()};
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
 	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
 

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.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
+		vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }
@@ -54,7 +54,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
 	auto varSorts = stateSorts(_contract);
 	vector<SortPointer> stateSort{_state.stateSort()};
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
 		SortProvider::boolSort
 	);
 }
@@ -66,7 +66,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.cryptoSort(), _state.txSort(), _state.stateSort()} +
+		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _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, cryptoFunctions, blockchainState, stateVariables).
+ * interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
  *
  * 2. Nondet interface
  * The nondeterminism behavior of a contract. Signature:
@@ -43,15 +43,15 @@ namespace solidity::frontend::smt
  * The summary of a contract's deployment procedure.
  * Signature:
  * If the contract has a constructor function, this is the same as the summary of that function. Otherwise:
- * constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
+ * constructor_summary(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
  *
  * 4. Function entry/summary
  * The entry point of a function definition. Signature:
- * function_entry(error, this, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
+ * function_entry(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
  *
  * 5. 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, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
  */
 
 /// @returns the interface predicate sort for _contract.

libsolidity/formal/SMTEncoder.cpp

@@ -71,7 +71,12 @@ bool SMTEncoder::analyze(SourceUnit const& _source)
 				analysis = false;
 			}
 
-	return analysis;
+	if (!analysis)
+		return false;
+
+	m_context.state().prepareForSourceUnit(_source);
+
+	return true;
 }
 
 bool SMTEncoder::visit(ContractDefinition const& _contract)
@@ -680,13 +685,15 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		if (isPublicGetter(_funCall.expression()))
 			visitPublicGetter(_funCall);
 		break;
+	case FunctionType::Kind::ABIDecode:
+	case FunctionType::Kind::ABIEncode:
+	case FunctionType::Kind::ABIEncodePacked:
+	case FunctionType::Kind::ABIEncodeWithSelector:
+	case FunctionType::Kind::ABIEncodeWithSignature:
+		visitABIFunction(_funCall);
+		break;
 	case FunctionType::Kind::Internal:
-	case FunctionType::Kind::DelegateCall:
-	case FunctionType::Kind::BareCall:
-	case FunctionType::Kind::BareCallCode:
-	case FunctionType::Kind::BareDelegateCall:
 	case FunctionType::Kind::BareStaticCall:
-	case FunctionType::Kind::Creation:
 		break;
 	case FunctionType::Kind::KECCAK256:
 	case FunctionType::Kind::ECRecover:
@@ -728,6 +735,11 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ObjectCreation:
 		visitObjectCreation(_funCall);
 		return;
+	case FunctionType::Kind::DelegateCall:
+	case FunctionType::Kind::BareCall:
+	case FunctionType::Kind::BareCallCode:
+	case FunctionType::Kind::BareDelegateCall:
+	case FunctionType::Kind::Creation:
 	default:
 		m_errorReporter.warning(
 			4588_error,
@@ -786,6 +798,50 @@ void SMTEncoder::visitRequire(FunctionCall const& _funCall)
 	addPathImpliedExpression(expr(*args.front()));
 }
 
+void SMTEncoder::visitABIFunction(FunctionCall const& _funCall)
+{
+	auto symbFunction = m_context.state().abiFunction(&_funCall);
+	auto const& [name, inTypes, outTypes] = m_context.state().abiFunctionTypes(&_funCall);
+
+	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	auto const& args = _funCall.sortedArguments();
+	auto argsActualLength = kind == FunctionType::Kind::ABIDecode ? 1 : args.size();
+
+	vector<smtutil::Expression> symbArgs;
+	solAssert(inTypes.size() == argsActualLength, "");
+	for (unsigned i = 0; i < argsActualLength; ++i)
+		if (args.at(i))
+			symbArgs.emplace_back(expr(*args.at(i), inTypes.at(i)));
+
+	optional<smtutil::Expression> arg;
+	if (inTypes.size() == 1)
+		arg = expr(*args.at(0));
+	else
+	{
+		auto inputSort = dynamic_cast<smtutil::ArraySort&>(*symbFunction.sort).domain;
+		arg = smtutil::Expression::tuple_constructor(
+			smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""),
+			symbArgs
+		);
+	}
+
+	auto out = smtutil::Expression::select(symbFunction, *arg);
+	if (outTypes.size() == 1)
+		defineExpr(_funCall, out);
+	else
+	{
+		auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
+		solAssert(symbTuple, "");
+		solAssert(symbTuple->components().size() == outTypes.size(), "");
+		solAssert(out.sort->kind == smtutil::Kind::Tuple, "");
+
+		symbTuple->increaseIndex();
+		for (unsigned i = 0; i < symbTuple->components().size(); ++i)
+			m_context.addAssertion(symbTuple->component(i) == smtutil::Expression::tuple_get(out, i));
+	}
+}
+
 void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
 {
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
@@ -2672,6 +2728,33 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
 	return nullptr;
 }
 
+set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
+{
+	struct ABIFunctions: public ASTConstVisitor
+	{
+		ABIFunctions(ASTNode const* _node) { _node->accept(*this); }
+		void endVisit(FunctionCall const& _funCall)
+		{
+			if (*_funCall.annotation().kind == FunctionCallKind::FunctionCall)
+				switch (dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type).kind())
+				{
+				case FunctionType::Kind::ABIEncode:
+				case FunctionType::Kind::ABIEncodePacked:
+				case FunctionType::Kind::ABIEncodeWithSelector:
+				case FunctionType::Kind::ABIEncodeWithSignature:
+				case FunctionType::Kind::ABIDecode:
+					abiCalls.insert(&_funCall);
+					break;
+				default: {}
+				}
+		}
+
+		set<FunctionCall const*> abiCalls;
+	};
+
+	return ABIFunctions(_node).abiCalls;
+}
+
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);

libsolidity/formal/SMTEncoder.h

@@ -87,6 +87,8 @@ public:
 	/// RationalNumberType or can be const evaluated, and nullptr otherwise.
 	static RationalNumberType const* isConstant(Expression const& _expr);
 
+	static std::set<FunctionCall const*> collectABICalls(ASTNode const* _node);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined
@@ -159,6 +161,7 @@ protected:
 	void initFunction(FunctionDefinition const& _function);
 	void visitAssert(FunctionCall const& _funCall);
 	void visitRequire(FunctionCall const& _funCall);
+	void visitABIFunction(FunctionCall const& _funCall);
 	void visitCryptoFunction(FunctionCall const& _funCall);
 	void visitGasLeft(FunctionCall const& _funCall);
 	virtual void visitAddMulMod(FunctionCall const& _funCall);

libsolidity/formal/SymbolicState.cpp

@@ -20,6 +20,7 @@
 
 #include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/formal/EncodingContext.h>
+#include <libsolidity/formal/SMTEncoder.h>
 
 using namespace std;
 using namespace solidity;
@@ -77,6 +78,10 @@ void SymbolicState::reset()
 	m_state.reset();
 	m_tx.reset();
 	m_crypto.reset();
+	/// We don't reset m_abi's pointer nor clear m_abiMembers on purpose,
+	/// since it only helps to keep the already generated types.
+	solAssert(m_abi, "");
+	m_abi->reset();
 }
 
 smtutil::Expression SymbolicState::balances() const
@@ -149,6 +154,14 @@ smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _func
 	return conj;
 }
 
+void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
+{
+	set<FunctionCall const*> abiCalls = SMTEncoder::collectABICalls(&_source);
+	for (auto const& source: _source.referencedSourceUnits(true))
+		abiCalls += SMTEncoder::collectABICalls(source);
+	buildABIFunctions(abiCalls);
+}
+
 /// Private helpers.
 
 void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
@@ -160,3 +173,126 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression
 	);
 	m_state.assignMember("balances", newBalances);
 }
+
+void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
+{
+	map<string, SortPointer> functions;
+
+	for (auto const* funCall: _abiFunctions)
+	{
+		auto t = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
+
+		auto const& args = funCall->sortedArguments();
+		auto const& paramTypes = t->parameterTypes();
+		auto const& returnTypes = t->returnParameterTypes();
+
+
+		auto argTypes = [](auto const& _args) {
+			return applyMap(_args, [](auto arg) { return arg->annotation().type; });
+		};
+
+		/// Since each abi.* function may have a different number of input/output parameters,
+		/// we generically compute those types.
+		vector<TypePointer> inTypes;
+		vector<TypePointer> outTypes;
+		if (t->kind() == FunctionType::Kind::ABIDecode)
+		{
+			/// abi.decode : (bytes, tuple_of_types(return_types)) -> (return_types)
+			inTypes.emplace_back(TypeProvider::bytesMemory());
+			auto const* tupleType = dynamic_cast<TupleType const*>(args.at(1)->annotation().type);
+			solAssert(tupleType, "");
+			for (auto t: tupleType->components())
+			{
+				auto typeType = dynamic_cast<TypeType const*>(t);
+				solAssert(typeType, "");
+				outTypes.emplace_back(typeType->actualType());
+			}
+		}
+		else
+		{
+			outTypes = returnTypes;
+			if (
+				t->kind() == FunctionType::Kind::ABIEncodeWithSelector ||
+				t->kind() == FunctionType::Kind::ABIEncodeWithSignature
+			)
+			{
+				/// abi.encodeWithSelector : (bytes4, one_or_more_types) -> bytes
+				/// abi.encodeWithSignature : (string, one_or_more_types) -> bytes
+				inTypes.emplace_back(paramTypes.front());
+				inTypes += argTypes(vector<ASTPointer<Expression const>>(args.begin() + 1, args.end()));
+			}
+			else
+			{
+				/// abi.encode/abi.encodePacked : one_or_more_types -> bytes
+				solAssert(
+					t->kind() == FunctionType::Kind::ABIEncode ||
+					t->kind() == FunctionType::Kind::ABIEncodePacked,
+					""
+				);
+				inTypes = argTypes(args);
+			}
+		}
+
+		/// Rational numbers and string literals add the concrete values to the type name,
+		/// so we replace them by uint256 and bytes since those are the same as their SMT types.
+		/// TODO we could also replace all types by their ABI type.
+		auto replaceTypes = [](auto& _types) {
+			for (auto& t: _types)
+				if (t->category() == frontend::Type::Category::RationalNumber)
+					t = TypeProvider::uint256();
+				else if (t->category() == frontend::Type::Category::StringLiteral)
+					t = TypeProvider::bytesMemory();
+		};
+		replaceTypes(inTypes);
+		replaceTypes(outTypes);
+
+		auto name = t->richIdentifier();
+		for (auto paramType: inTypes + outTypes)
+			name += "_" + paramType->richIdentifier();
+
+		m_abiMembers[funCall] = {name, inTypes, outTypes};
+
+		if (functions.count(name))
+			continue;
+
+		/// If there is only one input or output parameter, we use that type directly.
+		/// Otherwise we create a tuple wrapping the necessary input or output types.
+		auto typesToSort = [](auto const& _types, string const& _name) -> shared_ptr<Sort> {
+			if (_types.size() == 1)
+				return smtSort(*_types.front());
+
+			vector<string> inNames;
+			vector<SortPointer> sorts;
+			for (unsigned i = 0; i < _types.size(); ++i)
+			{
+				inNames.emplace_back(_name + "_input_" + to_string(i));
+				sorts.emplace_back(smtSort(*_types.at(i)));
+			}
+			return make_shared<smtutil::TupleSort>(
+				_name + "_input",
+				inNames,
+				sorts
+			);
+		};
+
+		auto functionSort = make_shared<smtutil::ArraySort>(
+			typesToSort(inTypes, name),
+			typesToSort(outTypes, name)
+		);
+
+		functions[name] = functionSort;
+	}
+
+	m_abi = make_unique<BlockchainVariable>("abi", move(functions), m_context);
+}
+
+smtutil::Expression SymbolicState::abiFunction(frontend::FunctionCall const* _funCall)
+{
+	solAssert(m_abi, "");
+	return m_abi->member(get<0>(m_abiMembers.at(_funCall)));
+}
+
+SymbolicState::SymbolicABIFunction const& SymbolicState::abiFunctionTypes(FunctionCall const* _funCall) const
+{
+	return m_abiMembers.at(_funCall);
+}

libsolidity/formal/SymbolicState.h

@@ -138,10 +138,32 @@ public:
 	smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); }
 	//@}
 
+	/// ABI functions.
+	//@{
+	/// Calls the internal methods that build the symbolic ABI functions
+	/// based on the abi.* calls in _source and referenced sources.
+	void prepareForSourceUnit(SourceUnit const& _source);
+	smtutil::Expression abiFunction(FunctionCall const* _funCall);
+	using SymbolicABIFunction = std::tuple<
+		std::string,
+		std::vector<TypePointer>,
+		std::vector<TypePointer>
+	>;
+	SymbolicABIFunction const& abiFunctionTypes(FunctionCall const* _funCall) const;
+
+	smtutil::Expression abi() const { solAssert(m_abi, ""); return m_abi->value(); }
+	smtutil::Expression abi(unsigned _idx) const { solAssert(m_abi, ""); return m_abi->value(_idx); }
+	smtutil::SortPointer const& abiSort() const { solAssert(m_abi, ""); return m_abi->sort(); }
+	void newABI() { solAssert(m_abi, ""); m_abi->newVar(); }
+	//@}
+
 private:
 	/// Adds _value to _account's balance.
 	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
 
+	/// Builds m_abi based on the abi.* calls _abiFunctions.
+	void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);
+
 	EncodingContext& m_context;
 
 	SymbolicIntVariable m_error{
@@ -213,6 +235,12 @@ private:
 		},
 		m_context
 	};
+
+	/// Tuple containing all used ABI functions.
+	std::unique_ptr<BlockchainVariable> m_abi;
+	/// Maps ABI functions calls to their tuple names generated by
+	/// `buildABIFunctions`.
+	std::map<FunctionCall const*, SymbolicABIFunction> m_abiMembers;
 };
 
 }

libsolidity/formal/SymbolicTypes.cpp

@@ -556,6 +556,10 @@ smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, fronte
 		solAssert(intType, "");
 		return _expr >= minValue(*intType) && _expr <= maxValue(*intType);
 	}
+	else if (isArray(*_type) || isMapping(*_type))
+		/// Length cannot be negative.
+		return smtutil::Expression::tuple_get(_expr, 1) >= 0;
+
 	return smtutil::Expression(true);
 }