From 37f6dc1f8855e9162160a9462c546891475870c3 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 12 Oct 2021 11:14:52 +0200 Subject: [PATCH] Add storage to state --- libsolidity/formal/BMC.cpp | 2 +- libsolidity/formal/SMTEncoder.cpp | 4 +- libsolidity/formal/SMTEncoder.h | 2 +- libsolidity/formal/SymbolicState.cpp | 189 +++++++++++++++++++++++---- libsolidity/formal/SymbolicState.h | 56 +++++--- libsolidity/formal/SymbolicTypes.cpp | 22 ++++ libsolidity/formal/SymbolicTypes.h | 4 + 7 files changed, 236 insertions(+), 43 deletions(-) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index bf3618791..26cc35cb1 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -82,7 +82,7 @@ void BMC::analyze(SourceUnit const& _source, map SMTEncoder::collectABICalls(ASTNode const* _node) +set> SMTEncoder::collectABICalls(ASTNode const* _node) { struct ABIFunctions: public ASTConstVisitor { @@ -3085,7 +3085,7 @@ set SMTEncoder::collectABICalls(ASTNode const* _node) } } - set abiCalls; + set> abiCalls; }; return ABIFunctions(_node).abiCalls; diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 1c3196c8f..de70e7612 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/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 collectABICalls(ASTNode const* _node); + static std::set> collectABICalls(ASTNode const* _node); /// @returns all the sources that @param _source depends on, /// including itself. diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index b1fd7978f..3755cee64 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -22,6 +22,10 @@ #include #include +#include + +#include + 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 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(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(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 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 abiCalls = SMTEncoder::collectABICalls(&_source); - for (auto const& source: _source.referencedSourceUnits(true)) + auto allSources = _source.referencedSourceUnits(true); + allSources.insert(&_source); + set> abiCalls; + set> contracts; + for (auto const& source: allSources) + { abiCalls += SMTEncoder::collectABICalls(source); + for (auto node: source->nodes()) + if (auto contract = dynamic_cast(node.get())) + contracts.insert(contract); + } + buildState(contracts, _storage); buildABIFunctions(abiCalls); } /// Private helpers. -void SymbolicState::buildABIFunctions(set 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> const& _contracts, bool _allStorages) +{ + map stateMembers{ + {"balances", make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)} + }; + + if (_allStorages) + { + vector memberNames; + vector 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( + name + "_type", names, sorts + ); + + auto storageSort = make_shared( + smtSort(*TypeProvider::address()), + storageTuple + ); + + memberNames.emplace_back(name); + memberSorts.emplace_back(storageSort); + } + + stateMembers.emplace( + "isActive", + make_shared(smtSort(*TypeProvider::address()), smtutil::SortProvider::boolSort) + ); + stateMembers.emplace( + "storage", + make_shared( + "storage_type", memberNames, memberSorts + ) + ); + } + + m_state = make_unique( + "state", + move(stateMembers), + m_context + ); +} + +void SymbolicState::buildABIFunctions(set> const& _abiFunctions) { map functions; diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index 309d545b8..c4ac7382f 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/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> const& _contracts, bool _allStorages); + /// Builds m_abi based on the abi.* calls _abiFunctions. - void buildABIFunctions(std::set const& _abiFunctions); + void buildABIFunctions(std::set> const& _abiFunctions); EncodingContext& m_context; @@ -185,11 +208,14 @@ private: m_context }; - BlockchainVariable m_state{ - "state", - {{"balances", std::make_shared(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 m_state; BlockchainVariable m_tx{ "tx", diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index e40ff9245..b66ff9f40 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -586,4 +586,26 @@ optional symbolicTypeConversion(frontend::Type const* _from return std::nullopt; } +smtutil::Expression member(smtutil::Expression const& _tuple, string const& _member) +{ + TupleSort const& _sort = dynamic_cast(*_tuple.sort); + return smtutil::Expression::tuple_get( + _tuple, + _sort.memberToIndex.at(_member) + ); +} + +smtutil::Expression assignMember(smtutil::Expression const _tuple, map const& _values) +{ + TupleSort const& _sort = dynamic_cast(*_tuple.sort); + vector 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(_tuple.sort), _tuple.name); + return smtutil::Expression::tuple_constructor(sortExpr, args); +} + } diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h index 312e8581a..747e27b7e 100644 --- a/libsolidity/formal/SymbolicTypes.h +++ b/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 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 const& _values); + }