Add tx data to symbolic state

libsolidity/formal/BMC.cpp

@@ -389,7 +389,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
-	case FunctionType::Kind::BlockHash:
 		SMTEncoder::endVisit(_funCall);
 		abstractFunctionCall(_funCall);
 		break;
@@ -409,6 +408,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		SMTEncoder::endVisit(_funCall);
 		break;
 	}
+	case FunctionType::Kind::BlockHash:
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
 		[[fallthrough]];

libsolidity/formal/SMTEncoder.cpp

@@ -633,7 +633,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
+		break;
 	case FunctionType::Kind::BlockHash:
+		defineExpr(_funCall, m_context.state().blockhash(expr(*_funCall.arguments().at(0))));
 		break;
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
@@ -1032,7 +1034,11 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 	if (exprType->category() == Type::Category::Magic)
 	{
 		if (identifier)
-			defineGlobalVariable(identifier->name() + "." + _memberAccess.memberName(), _memberAccess);
+		{
+			auto const& name = identifier->name();
+			solAssert(name == "block" || name == "msg" || name == "tx", "");
+			defineExpr(_memberAccess, m_context.state().txMember(name + "." + _memberAccess.memberName()));
+		}
 		else if (auto magicType = dynamic_cast<MagicType const*>(exprType); magicType->kind() == MagicType::Kind::MetaType)
 		{
 			auto const& memberName = _memberAccess.memberName();

libsolidity/formal/SymbolicState.cpp

@@ -26,110 +26,126 @@ using namespace solidity;
 using namespace solidity::smtutil;
 using namespace solidity::frontend::smt;
 
-SymbolicState::SymbolicState(EncodingContext& _context):
+BlockchainVariable::BlockchainVariable(
+	string _name,
+	map<string, smtutil::SortPointer> _members,
+	EncodingContext& _context
+):
+	m_name(move(_name)),
+	m_members(move(_members)),
 	m_context(_context)
 {
-	m_stateMembers.emplace("balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort));
-
 	vector<string> members;
 	vector<SortPointer> sorts;
-	for (auto const& [component, sort]: m_stateMembers)
+	for (auto const& [component, sort]: m_members)
 	{
 		members.emplace_back(component);
 		sorts.emplace_back(sort);
 		m_componentIndices[component] = members.size() - 1;
 	}
-	m_stateTuple = make_unique<SymbolicTupleVariable>(
+	m_tuple = make_unique<SymbolicTupleVariable>(
-		make_shared<smtutil::TupleSort>("state_type", members, sorts),
+		make_shared<smtutil::TupleSort>(m_name + "_type", members, sorts),
-		"state",
+		m_name,
 		m_context
 	);
 }
 
+smtutil::Expression BlockchainVariable::member(string const& _member) const
+{
+	return m_tuple->component(m_componentIndices.at(_member));
+}
+
+smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtutil::Expression const& _value)
+{
+	vector<smtutil::Expression> args;
+	for (auto const& m: m_members)
+		if (m.first == _member)
+			args.emplace_back(_value);
+		else
+			args.emplace_back(member(m.first));
+	m_tuple->increaseIndex();
+	auto tuple = m_tuple->currentValue();
+	auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
+	m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
+	return m_tuple->currentValue();
+}
+
 void SymbolicState::reset()
 {
 	m_error.resetIndex();
 	m_thisAddress.resetIndex();
-	m_stateTuple->resetIndex();
+	m_state.reset();
+	m_tx.reset();
 }
 
-// Blockchain
+smtutil::Expression SymbolicState::balances() const
-
-SymbolicIntVariable& SymbolicState::errorFlag()
 {
-	return m_error;
+	return m_state.member("balances");
 }
 
-SortPointer SymbolicState::errorFlagSort()
+smtutil::Expression SymbolicState::balance() const
-{
-	return m_error.sort();
-}
-
-smtutil::Expression SymbolicState::thisAddress()
-{
-	return m_thisAddress.currentValue();
-}
-
-smtutil::Expression SymbolicState::thisAddress(unsigned _idx)
-{
-	return m_thisAddress.valueAtIndex(_idx);
-}
-
-SortPointer SymbolicState::thisAddressSort()
-{
-	return m_thisAddress.sort();
-}
-
-smtutil::Expression SymbolicState::state()
-{
-	return m_stateTuple->currentValue();
-}
-
-smtutil::Expression SymbolicState::state(unsigned _idx)
-{
-	return m_stateTuple->valueAtIndex(_idx);
-}
-
-SortPointer SymbolicState::stateSort()
-{
-	return m_stateTuple->sort();
-}
-
-void SymbolicState::newState()
-{
-	m_stateTuple->increaseIndex();
-}
-
-smtutil::Expression SymbolicState::balances()
-{
-	return m_stateTuple->component(m_componentIndices.at("balances"));
-}
-
-smtutil::Expression SymbolicState::balance()
 {
 	return balance(thisAddress());
 }
 
-smtutil::Expression SymbolicState::balance(smtutil::Expression _address)
+smtutil::Expression SymbolicState::balance(smtutil::Expression _address) const
 {
 	return smtutil::Expression::select(balances(), move(_address));
 }
 
+smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) const
+{
+	return smtutil::Expression::select(m_tx.member("blockhash"), move(_blockNumber));
+}
+
 void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
 {
-	unsigned indexBefore = m_stateTuple->index();
+	unsigned indexBefore = m_state.index();
 	addBalance(_from, 0 - _value);
 	addBalance(_to, move(_value));
-	unsigned indexAfter = m_stateTuple->index();
+	unsigned indexAfter = m_state.index();
 	solAssert(indexAfter > indexBefore, "");
-	m_stateTuple->increaseIndex();
+	m_state.newVar();
 	/// Do not apply the transfer operation if _from == _to.
 	auto newState = smtutil::Expression::ite(
 		move(_from) == move(_to),
-		m_stateTuple->valueAtIndex(indexBefore),
+		m_state.value(indexBefore),
-		m_stateTuple->valueAtIndex(indexAfter)
+		m_state.value(indexAfter)
 	);
-	m_context.addAssertion(m_stateTuple->currentValue() == newState);
+	m_context.addAssertion(m_state.value() == newState);
+}
+
+smtutil::Expression SymbolicState::txMember(string const& _member) const
+{
+	return m_tx.member(_member);
+}
+
+smtutil::Expression SymbolicState::txConstraints(FunctionDefinition const& _function) const
+{
+	smtutil::Expression conj = smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::uint(160)) &&
+		smt::symbolicUnknownConstraints(m_tx.member("msg.sender"), TypeProvider::uint(160)) &&
+		smt::symbolicUnknownConstraints(m_tx.member("tx.origin"), TypeProvider::uint(160));
+
+	if (_function.isPartOfExternalInterface())
+	{
+		auto sig = TypeProvider::function(_function)->externalIdentifier();
+		conj = conj && m_tx.member("msg.sig") == sig;
+
+		auto b0 = sig >> (3 * 8);
+		auto b1 = (sig & 0x00ff0000) >> (2 * 8);
+		auto b2 = (sig & 0x0000ff00) >> (1 * 8);
+		auto b3 = (sig & 0x000000ff);
+		auto data = smtutil::Expression::tuple_get(m_tx.member("msg.data"), 0);
+		conj = conj && smtutil::Expression::select(data, 0) == b0;
+		conj = conj && smtutil::Expression::select(data, 1) == b1;
+		conj = conj && smtutil::Expression::select(data, 2) == b2;
+		conj = conj && smtutil::Expression::select(data, 3) == b3;
+		auto length = smtutil::Expression::tuple_get(m_tx.member("msg.data"), 1);
+		// TODO add ABI size of function input parameters here \/
+		conj = conj && length >= 4;
+	}
+
+	return conj;
 }
 
 /// Private helpers.
@@ -141,20 +157,5 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression
 		_address,
 		balance(_address) + move(_value)
 	);
-	assignStateMember("balances", newBalances);
+	m_state.assignMember("balances", newBalances);
-}
-
-smtutil::Expression SymbolicState::assignStateMember(string const& _member, smtutil::Expression const& _value)
-{
-	vector<smtutil::Expression> args;
-	for (auto const& member: m_stateMembers)
-		if (member.first == _member)
-			args.emplace_back(_value);
-		else
-			args.emplace_back(m_stateTuple->component(m_componentIndices.at(member.first)));
-	m_stateTuple->increaseIndex();
-	auto tuple = m_stateTuple->currentValue();
-	auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(tuple.sort), tuple.name);
-	m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args));
-	return m_stateTuple->currentValue();
 }

libsolidity/formal/SymbolicState.h

@@ -18,6 +18,7 @@
 
 #pragma once
 
+#include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 
 #include <libsmtutil/Sorts.h>
@@ -30,6 +31,31 @@ class EncodingContext;
 class SymbolicAddressVariable;
 class SymbolicArrayVariable;
 
+class BlockchainVariable
+{
+public:
+	BlockchainVariable(std::string _name, std::map<std::string, smtutil::SortPointer> _members, EncodingContext& _context);
+	/// @returns the variable data as a tuple.
+	smtutil::Expression value() const { return m_tuple->currentValue(); }
+	smtutil::Expression value(unsigned _idx) const { return m_tuple->valueAtIndex(_idx); }
+	smtutil::SortPointer const& sort() const { return m_tuple->sort(); }
+	unsigned index() const { return m_tuple->index(); }
+	void newVar() { m_tuple->increaseIndex(); }
+	void reset() { m_tuple->resetIndex(); }
+
+	/// @returns the symbolic _member.
+	smtutil::Expression member(std::string const& _member) const;
+	/// Generates a new tuple where _member is assigned _value.
+	smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _value);
+
+private:
+	std::string const m_name;
+	std::map<std::string, smtutil::SortPointer> const m_members;
+	EncodingContext& m_context;
+	std::map<std::string, unsigned> m_componentIndices;
+	std::unique_ptr<SymbolicTupleVariable> m_tuple;
+};
+
 /**
  * Symbolic representation of the blockchain context:
  * - error flag
@@ -37,49 +63,75 @@ class SymbolicArrayVariable;
  * - state, represented as a tuple of:
  *   - balances
  *   - TODO: potentially storage of contracts
- * - TODO transaction variables
+ * - block and transaction properties, represented as a tuple of:
+ *   - blockhash
+ *   - block coinbase
+ *   - block difficulty
+ *   - block gaslimit
+ *   - block number
+ *   - block timestamp
+ *   - TODO gasleft
+ *   - msg data
+ *   - msg sender
+ *   - msg sig
+ *   - msg value
+ *   - tx gasprice
+ *   - tx origin
  */
 class SymbolicState
 {
 public:
-	SymbolicState(EncodingContext& _context);
+	SymbolicState(EncodingContext& _context): m_context(_context) {}
 
 	void reset();
 
-	/// Blockchain.
+	/// Error flag.
 	//@{
-	SymbolicIntVariable& errorFlag();
+	SymbolicIntVariable& errorFlag() { return m_error; }
-	smtutil::SortPointer errorFlagSort();
+	smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); }
+	//@}
 
+	/// This.
+	//@{
 	/// @returns the symbolic value of the currently executing contract's address.
-	smtutil::Expression thisAddress();
+	smtutil::Expression thisAddress() const { return m_thisAddress.currentValue(); }
-	smtutil::Expression thisAddress(unsigned _idx);
+	smtutil::Expression thisAddress(unsigned _idx) const { return m_thisAddress.valueAtIndex(_idx); }
-	smtutil::SortPointer thisAddressSort();
+	smtutil::SortPointer const& thisAddressSort() const { return m_thisAddress.sort(); }
-
+	//@}
-	/// @returns the state as a tuple.
-	smtutil::Expression state();
-	smtutil::Expression state(unsigned _idx);
-	smtutil::SortPointer stateSort();
-	void newState();
 
+	/// Blockchain state.
+	//@{
+	smtutil::Expression state() const { return m_state.value(); }
+	smtutil::Expression state(unsigned _idx) const { return m_state.value(_idx); }
+	smtutil::SortPointer const& stateSort() const { return m_state.sort(); }
+	void newState() { m_state.newVar(); }
 	/// @returns the symbolic balances.
-	smtutil::Expression balances();
+	smtutil::Expression balances() const;
 	/// @returns the symbolic balance of address `this`.
-	smtutil::Expression balance();
+	smtutil::Expression balance() const;
 	/// @returns the symbolic balance of an address.
-	smtutil::Expression balance(smtutil::Expression _address);
+	smtutil::Expression balance(smtutil::Expression _address) const;
 
 	/// Transfer _value from _from to _to.
 	void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
 	//@}
 
+	/// Transaction data.
+	//@{
+	/// @returns the tx data as a tuple.
+	smtutil::Expression tx() const { return m_tx.value(); }
+	smtutil::Expression tx(unsigned _idx) const { return m_tx.value(_idx); }
+	smtutil::SortPointer const& txSort() const { return m_tx.sort(); }
+	void newTx() { m_tx.newVar(); }
+	smtutil::Expression txMember(std::string const& _member) const;
+	smtutil::Expression txConstraints(FunctionDefinition const& _function) const;
+	smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
+	//@}
+
 private:
 	/// Adds _value to _account's balance.
 	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
 
-	/// Generates a new tuple where _member is assigned _value.
-	smtutil::Expression assignStateMember(std::string const& _member, smtutil::Expression const& _value);
-
 	EncodingContext& m_context;
 
 	SymbolicIntVariable m_error{
@@ -94,10 +146,31 @@ private:
 		m_context
 	};
 
-	std::map<std::string, unsigned> m_componentIndices;
+	BlockchainVariable m_state{
-	/// balances, TODO storage of other contracts
+		"state",
-	std::map<std::string, smtutil::SortPointer> m_stateMembers;
+		{{"balances", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}},
-	std::unique_ptr<SymbolicTupleVariable> m_stateTuple;
+		m_context
+	};
+
+	BlockchainVariable m_tx{
+		"tx",
+		{
+			{"blockhash", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)},
+			{"block.coinbase", smt::smtSort(*TypeProvider::address())},
+			{"block.difficulty", smtutil::SortProvider::uintSort},
+			{"block.gaslimit", smtutil::SortProvider::uintSort},
+			{"block.number", smtutil::SortProvider::uintSort},
+			{"block.timestamp", smtutil::SortProvider::uintSort},
+			// TODO gasleft
+			{"msg.data", smt::smtSort(*TypeProvider::bytesMemory())},
+			{"msg.sender", smt::smtSort(*TypeProvider::address())},
+			{"msg.sig", smtutil::SortProvider::uintSort},
+			{"msg.value", smtutil::SortProvider::uintSort},
+			{"tx.gasprice", smtutil::SortProvider::uintSort},
+			{"tx.origin", smt::smtSort(*TypeProvider::address())}
+		},
+		m_context
+	};
 };
 
 }

libsolidity/formal/SymbolicTypes.cpp

@@ -18,6 +18,8 @@
 
 #include <libsolidity/formal/SymbolicTypes.h>
 
+#include <libsolidity/formal/EncodingContext.h>
+
 #include <libsolidity/ast/TypeProvider.h>
 #include <libsolidity/ast/Types.h>
 #include <libsolutil/CommonData.h>
@@ -535,22 +537,26 @@ void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext&
 }
 
 void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context)
+{
+	_context.addAssertion(symbolicUnknownConstraints(_expr, _type));
+}
+
+smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type)
 {
 	solAssert(_type, "");
 	if (isEnum(*_type))
 	{
 		auto enumType = dynamic_cast<frontend::EnumType const*>(_type);
 		solAssert(enumType, "");
-		_context.addAssertion(_expr >= 0);
+		return _expr >= 0 && _expr < enumType->numberOfMembers();
-		_context.addAssertion(_expr < enumType->numberOfMembers());
 	}
 	else if (isInteger(*_type))
 	{
 		auto intType = dynamic_cast<frontend::IntegerType const*>(_type);
 		solAssert(intType, "");
-		_context.addAssertion(_expr >= minValue(*intType));
+		return _expr >= minValue(*intType) && _expr <= maxValue(*intType);
-		_context.addAssertion(_expr <= maxValue(*intType));
 	}
+	return smtutil::Expression(true);
 }
 
 optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to)

libsolidity/formal/SymbolicTypes.h

@@ -18,7 +18,6 @@
 
 #pragma once
 
-#include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 #include <libsolidity/ast/AST.h>
 #include <libsolidity/ast/Types.h>
@@ -26,6 +25,8 @@
 namespace solidity::frontend::smt
 {
 
+class EncodingContext;
+
 /// Returns the SMT sort that models the Solidity type _type.
 smtutil::SortPointer smtSort(frontend::Type const& _type);
 std::vector<smtutil::SortPointer> smtSort(std::vector<frontend::TypePointer> const& _types);
@@ -77,6 +78,7 @@ void setSymbolicZeroValue(SymbolicVariable const& _variable, EncodingContext& _c
 void setSymbolicZeroValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
 void setSymbolicUnknownValue(SymbolicVariable const& _variable, EncodingContext& _context);
 void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::TypePointer const& _type, EncodingContext& _context);
+smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::TypePointer const& _type);
 
 std::optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePointer _to);
 }

libsolidity/formal/SymbolicVariables.cpp

@@ -18,6 +18,7 @@
 
 #include <libsolidity/formal/SymbolicVariables.h>
 
+#include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 #include <libsolidity/ast/AST.h>