Add storage to state

libsolidity/formal/BMC.cpp

@@ -82,7 +82,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 	m_context.setAssertionAccumulation(true);
 	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 	createFreeConstants(sourceDependencies(_source));
-	state().prepareForSourceUnit(_source);
+	state().prepareForSourceUnit(_source, false);
 	m_unprovedAmt = 0;
 
 	_source.accept(*this);

libsolidity/formal/SMTEncoder.cpp

@@ -3063,7 +3063,7 @@ RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
 	return nullptr;
 }
 
-set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
+set<FunctionCall const*, ASTCompareByID<FunctionCall>> SMTEncoder::collectABICalls(ASTNode const* _node)
 {
 	struct ABIFunctions: public ASTConstVisitor
 	{
@@ -3085,7 +3085,7 @@ set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
 				}
 		}
 
-		set<FunctionCall const*> abiCalls;
+		set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
 	};
 
 	return ABIFunctions(_node).abiCalls;

libsolidity/formal/SMTEncoder.h

@@ -123,7 +123,7 @@ 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);
+	static std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> collectABICalls(ASTNode const* _node);
 
 	/// @returns all the sources that @param _source depends on,
 	/// including itself.

libsolidity/formal/SymbolicState.cpp

@@ -22,6 +22,10 @@
 #include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SMTEncoder.h>
 
+#include <libsmtutil/Sorts.h>
+
+#include <range/v3/view.hpp>
+
 using namespace std;
 using namespace solidity;
 using namespace solidity::smtutil;
@@ -58,16 +62,8 @@ smtutil::Expression BlockchainVariable::member(string const& _member) const
 
 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));
+	smtutil::Expression newTuple = smt::assignMember(m_tuple->currentValue(), {{_member, _value}});
+	m_context.addAssertion(m_tuple->increaseIndex() == newTuple);
 	return m_tuple->currentValue();
 }
 
@@ -75,16 +71,19 @@ void SymbolicState::reset()
 {
 	m_error.resetIndex();
 	m_thisAddress.resetIndex();
-	m_state.reset();
 	m_tx.reset();
 	m_crypto.reset();
 	if (m_abi)
 		m_abi->reset();
+	/// We don't reset nor clear these pointers on purpose,
+	/// since it only helps to keep the already generated types.
+	if (m_state)
+		m_state->reset();
 }
 
 smtutil::Expression SymbolicState::balances() const
 {
-	return m_state.member("balances");
+	return m_state->member("balances");
 }
 
 smtutil::Expression SymbolicState::balance() const
@@ -107,24 +106,84 @@ void SymbolicState::newBalances()
 	auto tupleSort = dynamic_pointer_cast<TupleSort>(stateSort());
 	auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances"));
 	SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context);
-	m_state.assignMember("balances", newBalances.currentValue());
+	m_state->assignMember("balances", newBalances.currentValue());
 }
 
 void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
 {
-	unsigned indexBefore = m_state.index();
+	unsigned indexBefore = m_state->index();
 	addBalance(_from, 0 - _value);
 	addBalance(_to, move(_value));
-	unsigned indexAfter = m_state.index();
+	unsigned indexAfter = m_state->index();
 	solAssert(indexAfter > indexBefore, "");
-	m_state.newVar();
+	m_state->newVar();
 	/// Do not apply the transfer operation if _from == _to.
 	auto newState = smtutil::Expression::ite(
 		move(_from) == move(_to),
-		m_state.value(indexBefore),
-		m_state.value(indexAfter)
+		m_state->value(indexBefore),
+		m_state->value(indexAfter)
 	);
-	m_context.addAssertion(m_state.value() == newState);
+	m_context.addAssertion(m_state->value() == newState);
+}
+
+smtutil::Expression SymbolicState::storage(ContractDefinition const& _contract) const
+{
+	return smt::member(m_state->member("storage"), contractStorageKey(_contract));
+}
+
+smtutil::Expression SymbolicState::storage(ContractDefinition const& _contract, smtutil::Expression _address) const
+{
+	return smtutil::Expression::select(storage(_contract), move(_address));
+}
+
+smtutil::Expression SymbolicState::addressActive(smtutil::Expression _address) const
+{
+	return smtutil::Expression::select(m_state->member("isActive"), move(_address));
+}
+
+void SymbolicState::setAddressActive(
+	smtutil::Expression _address,
+	bool _active
+)
+{
+	m_state->assignMember("isActive", smtutil::Expression::store(
+		m_state->member("isActive"),
+		move(_address),
+		smtutil::Expression(_active))
+	);
+}
+
+void SymbolicState::writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address)
+{
+	auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
+	if (stateVars.empty())
+		return;
+
+	map<string, smtutil::Expression> values;
+	for (auto var: stateVars)
+		values.emplace(stateVarStorageKey(*var, _contract), m_context.variable(*var)->currentValue());
+
+	smtutil::Expression thisStorage = storage(_contract, _address);
+	smtutil::Expression newStorage = smt::assignMember(thisStorage, values);
+	auto newContractStorage = smtutil::Expression::store(
+		storage(_contract), move(_address), newStorage
+	);
+	smtutil::Expression newAllStorage = smt::assignMember(m_state->member("storage"), {{contractStorageKey(_contract), newContractStorage}});
+	m_state->assignMember("storage", newAllStorage);
+}
+
+void SymbolicState::readStateVars(ContractDefinition const& _contract, smtutil::Expression _address)
+{
+	auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
+	if (stateVars.empty())
+		return;
+
+	auto contractStorage = storage(_contract, move(_address));
+	for (auto var: stateVars)
+		m_context.addAssertion(
+			m_context.variable(*var)->increaseIndex() ==
+			smt::member(contractStorage, stateVarStorageKey(*var, _contract))
+		);
 }
 
 void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
@@ -134,7 +193,7 @@ void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression
 		_address,
 		balance(_address) + move(_value)
 	);
-	m_state.assignMember("balances", newBalances);
+	m_state->assignMember("balances", newBalances);
 }
 
 smtutil::Expression SymbolicState::txMember(string const& _member) const
@@ -187,17 +246,99 @@ smtutil::Expression SymbolicState::txFunctionConstraints(FunctionDefinition cons
 	return conj;
 }
 
-void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
+void SymbolicState::prepareForSourceUnit(SourceUnit const& _source, bool _storage)
 {
-	set<FunctionCall const*> abiCalls = SMTEncoder::collectABICalls(&_source);
-	for (auto const& source: _source.referencedSourceUnits(true))
+	auto allSources = _source.referencedSourceUnits(true);
+	allSources.insert(&_source);
+	set<FunctionCall const*, ASTCompareByID<FunctionCall>> abiCalls;
+	set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> contracts;
+	for (auto const& source: allSources)
+	{
 		abiCalls += SMTEncoder::collectABICalls(source);
+		for (auto node: source->nodes())
+			if (auto contract = dynamic_cast<ContractDefinition const*>(node.get()))
+				contracts.insert(contract);
+	}
+	buildState(contracts, _storage);
 	buildABIFunctions(abiCalls);
 }
 
 /// Private helpers.
 
-void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
+string SymbolicState::contractSuffix(ContractDefinition const& _contract) const
+{
+	return "_" + _contract.name() + "_" + to_string(_contract.id());
+}
+
+string SymbolicState::contractStorageKey(ContractDefinition const& _contract) const
+{
+	return "storage" + contractSuffix(_contract);
+}
+
+string SymbolicState::stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const
+{
+	return _var.name() + "_" + to_string(_var.id()) + contractSuffix(_contract);
+}
+
+void SymbolicState::buildState(set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> const& _contracts, bool _allStorages)
+{
+	map<string, SortPointer> stateMembers{
+		{"balances", make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}
+	};
+
+	if (_allStorages)
+	{
+		vector<string> memberNames;
+		vector<SortPointer> memberSorts;
+		for (auto contract: _contracts)
+		{
+			string suffix = contractSuffix(*contract);
+
+			// z3 doesn't like empty tuples, so if the contract has 0
+			// state vars we can't put it there.
+			auto stateVars = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract);
+			if (stateVars.empty())
+				continue;
+
+			auto names = applyMap(stateVars, [&](auto var) {
+				return var->name() + "_" + to_string(var->id()) + suffix;
+			});
+			auto sorts = applyMap(stateVars, [](auto var) { return smtSortAbstractFunction(*var->type()); });
+
+			string name = "storage" + suffix;
+			auto storageTuple = make_shared<smtutil::TupleSort>(
+				name + "_type", names, sorts
+			);
+
+			auto storageSort = make_shared<smtutil::ArraySort>(
+				smtSort(*TypeProvider::address()),
+				storageTuple
+			);
+
+			memberNames.emplace_back(name);
+			memberSorts.emplace_back(storageSort);
+		}
+
+		stateMembers.emplace(
+			"isActive",
+			make_shared<smtutil::ArraySort>(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort)
+		);
+		stateMembers.emplace(
+			"storage",
+			make_shared<smtutil::TupleSort>(
+				"storage_type", memberNames, memberSorts
+			)
+		);
+	}
+
+	m_state = make_unique<BlockchainVariable>(
+		"state",
+		move(stateMembers),
+		m_context
+	);
+}
+
+void SymbolicState::buildABIFunctions(set<FunctionCall const*, ASTCompareByID<FunctionCall>> const& _abiFunctions)
 {
 	map<string, SortPointer> functions;
 

libsolidity/formal/SymbolicState.h

@@ -62,7 +62,8 @@ private:
  * - this (the address of the currently executing contract)
  * - state, represented as a tuple of:
  *   - balances
- *   - TODO: potentially storage of contracts
+ *   - array of address => bool representing whether an address is used by a contract
+ *   - storage of contracts
  * - block and transaction properties, represented as a tuple of:
  *   - blockhash
  *   - block basefee
@@ -99,29 +100,40 @@ public:
 	/// @returns the symbolic value of the currently executing contract's address.
 	smtutil::Expression thisAddress() const { return m_thisAddress.currentValue(); }
 	smtutil::Expression thisAddress(unsigned _idx) const { return m_thisAddress.valueAtIndex(_idx); }
+	smtutil::Expression newThisAddress() { return m_thisAddress.increaseIndex(); }
 	smtutil::SortPointer const& thisAddressSort() const { return m_thisAddress.sort(); }
 	//@}
 
 	/// 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(); }
+	smtutil::Expression state() const { solAssert(m_state, ""); return m_state->value(); }
+	smtutil::Expression state(unsigned _idx) const { solAssert(m_state, ""); return m_state->value(_idx); }
+	smtutil::SortPointer const& stateSort() const { solAssert(m_state, ""); return m_state->sort(); }
+	void newState() { solAssert(m_state, ""); m_state->newVar(); }
 
 	void newBalances();
+
+	/// Balance.
 	/// @returns the symbolic balances.
 	smtutil::Expression balances() const;
 	/// @returns the symbolic balance of address `this`.
 	smtutil::Expression balance() const;
 	/// @returns the symbolic balance of an 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);
 
 	/// Adds _value to _account's balance.
 	void addBalance(smtutil::Expression _account, smtutil::Expression _value);
+
+	/// Storage.
+	smtutil::Expression storage(ContractDefinition const& _contract) const;
+	smtutil::Expression storage(ContractDefinition const& _contract, smtutil::Expression _address) const;
+	smtutil::Expression addressActive(smtutil::Expression _address) const;
+	void setAddressActive(smtutil::Expression _address, bool _active);
+
+	void writeStateVars(ContractDefinition const& _contract, smtutil::Expression _address);
+	void readStateVars(ContractDefinition const& _contract, smtutil::Expression _address);
 	//@}
 
 	/// Transaction data.
@@ -148,11 +160,15 @@ public:
 	smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); }
 	//@}
 
+	/// Calls the internal methods that build
+	/// - the symbolic ABI functions based on the abi.* calls
+	///   in _source and referenced sources.
+	/// - the symbolic storages for all contracts in _source and
+	///   referenced sources.
+	void prepareForSourceUnit(SourceUnit const& _source, bool _storage);
+
 	/// 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,
@@ -168,8 +184,15 @@ public:
 	//@}
 
 private:
+	std::string contractSuffix(ContractDefinition const& _contract) const;
+	std::string contractStorageKey(ContractDefinition const& _contract) const;
+	std::string stateVarStorageKey(VariableDeclaration const& _var, ContractDefinition const& _contract) const;
+
+	/// Builds state.storage based on _contracts.
+	void buildState(std::set<ContractDefinition const*, ASTCompareByID<ContractDefinition>> const& _contracts, bool _allStorages);
+
 	/// Builds m_abi based on the abi.* calls _abiFunctions.
-	void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);
+	void buildABIFunctions(std::set<FunctionCall const*, ASTCompareByID<FunctionCall>> const& _abiFunctions);
 
 	EncodingContext& m_context;
 
@@ -185,11 +208,14 @@ private:
 		m_context
 	};
 
-	BlockchainVariable m_state{
-		"state",
-		{{"balances", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}},
-		m_context
-	};
+	/// m_state is a tuple of
+	/// - balances: array of address to balance of address.
+	/// - isActive: array of address to Boolean, where element is true iff address is used.
+	/// - storage: tuple containing the storage of every contract, where
+	/// each element of the tuple represents a contract,
+	/// and is defined by an array where the index is the contract's address
+	/// and the element is a tuple containing the state variables of that contract.
+	std::unique_ptr<BlockchainVariable> m_state;
 
 	BlockchainVariable m_tx{
 		"tx",

libsolidity/formal/SymbolicTypes.cpp

@@ -586,4 +586,26 @@ optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from
 	return std::nullopt;
 }
 
+smtutil::Expression member(smtutil::Expression const& _tuple, string const& _member)
+{
+	TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort);
+	return smtutil::Expression::tuple_get(
+		_tuple,
+		_sort.memberToIndex.at(_member)
+	);
+}
+
+smtutil::Expression assignMember(smtutil::Expression const _tuple, map<string, smtutil::Expression> const& _values)
+{
+	TupleSort const& _sort = dynamic_cast<TupleSort const&>(*_tuple.sort);
+	vector<smtutil::Expression> args;
+	for (auto const& m: _sort.members)
+		if (auto* value = util::valueOrNullptr(_values, m))
+			args.emplace_back(*value);
+		else
+			args.emplace_back(member(_tuple, m));
+	auto sortExpr = smtutil::Expression(make_shared<smtutil::SortSort>(_tuple.sort), _tuple.name);
+	return smtutil::Expression::tuple_constructor(sortExpr, args);
+}
+
 }

libsolidity/formal/SymbolicTypes.h

@@ -82,4 +82,8 @@ void setSymbolicUnknownValue(smtutil::Expression _expr, frontend::Type const* _t
 smtutil::Expression symbolicUnknownConstraints(smtutil::Expression _expr, frontend::Type const* _type);
 
 std::optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const* _from, frontend::Type const* _to);
+
+smtutil::Expression member(smtutil::Expression const& _tuple, std::string const& _member);
+smtutil::Expression assignMember(smtutil::Expression const _tuple, std::map<std::string, smtutil::Expression> const& _values);
+
 }