From a86f6567046d1a5781208b52d41ca5dbbd9b9ff3 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 7 Sep 2020 16:45:14 +0200 Subject: [PATCH] Refactor state as tuple --- libsolidity/formal/SymbolicState.cpp | 76 ++++++++++++++++++++++------ libsolidity/formal/SymbolicState.h | 46 +++++++++++------ 2 files changed, 91 insertions(+), 31 deletions(-) diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp index 40fac322d..d51d68162 100644 --- a/libsolidity/formal/SymbolicState.cpp +++ b/libsolidity/formal/SymbolicState.cpp @@ -16,24 +16,42 @@ */ // SPDX-License-Identifier: GPL-3.0 +#include "libsmtutil/SolverInterface.h" #include +#include #include using namespace std; using namespace solidity; +using namespace solidity::smtutil; using namespace solidity::frontend::smt; SymbolicState::SymbolicState(EncodingContext& _context): m_context(_context) { + m_stateMembers.emplace("balances", make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)); + + vector members; + vector sorts; + for (auto const& [component, sort]: m_stateMembers) + { + members.emplace_back(component); + sorts.emplace_back(sort); + m_componentIndices[component] = members.size() - 1; + } + m_stateTuple = make_unique( + make_shared("state_type", members, sorts), + "state", + m_context + ); } void SymbolicState::reset() { - m_thisAddress.resetIndex(); - m_balances.resetIndex(); m_error.resetIndex(); + m_thisAddress.resetIndex(); + m_stateTuple->resetIndex(); } // Blockchain @@ -43,14 +61,19 @@ smtutil::Expression SymbolicState::thisAddress() return m_thisAddress.currentValue(); } +smtutil::Expression SymbolicState::balances() +{ + return m_stateTuple->component(m_componentIndices.at("balances")); +} + smtutil::Expression SymbolicState::balance() { - return balance(m_thisAddress.currentValue()); + return balance(thisAddress()); } smtutil::Expression SymbolicState::balance(smtutil::Expression _address) { - return smtutil::Expression::select(m_balances.elements(), move(_address)); + return smtutil::Expression::select(balances(), move(_address)); } SymbolicIntVariable& SymbolicState::errorFlag() @@ -58,21 +81,31 @@ SymbolicIntVariable& SymbolicState::errorFlag() return m_error; } +smtutil::Expression SymbolicState::state() +{ + return m_stateTuple->currentValue(); +} + +SortPointer SymbolicState::stateSort() +{ + return m_stateTuple->sort(); +} + void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value) { - unsigned indexBefore = m_balances.index(); + unsigned indexBefore = m_stateTuple->index(); addBalance(_from, 0 - _value); addBalance(_to, move(_value)); - unsigned indexAfter = m_balances.index(); + unsigned indexAfter = m_stateTuple->index(); solAssert(indexAfter > indexBefore, ""); - m_balances.increaseIndex(); + m_stateTuple->increaseIndex(); /// Do not apply the transfer operation if _from == _to. - auto newBalances = smtutil::Expression::ite( + auto newState = smtutil::Expression::ite( move(_from) == move(_to), - m_balances.valueAtIndex(indexBefore), - m_balances.valueAtIndex(indexAfter) + m_stateTuple->valueAtIndex(indexBefore), + m_stateTuple->valueAtIndex(indexAfter) ); - m_context.addAssertion(m_balances.currentValue() == newBalances); + m_context.addAssertion(m_stateTuple->currentValue() == newState); } /// Private helpers. @@ -80,13 +113,24 @@ void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value) { auto newBalances = smtutil::Expression::store( - m_balances.elements(), + balances(), _address, balance(_address) + move(_value) ); - auto oldLength = m_balances.length(); - m_balances.increaseIndex(); - m_context.addAssertion(m_balances.elements() == newBalances); - m_context.addAssertion(m_balances.length() == oldLength); + assignStateMember("balances", newBalances); } +smtutil::Expression SymbolicState::assignStateMember(string const& _member, smtutil::Expression const& _value) +{ + vector 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(tuple.sort), tuple.name); + m_context.addAssertion(tuple == smtutil::Expression::tuple_constructor(sortExpr, args)); + return m_stateTuple->currentValue(); +} diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h index e11dc3840..9878e1926 100644 --- a/libsolidity/formal/SymbolicState.h +++ b/libsolidity/formal/SymbolicState.h @@ -27,9 +27,17 @@ namespace solidity::frontend::smt { class EncodingContext; +class SymbolicAddressVariable; +class SymbolicArrayVariable; /** - * Symbolic representation of the blockchain state. + * Symbolic representation of the blockchain context: + * - error flag + * - this (the address of the currently executing contract) + * - state, represented as a tuple of: + * - balances + * - TODO: potentially storage of contracts + * - TODO transaction variables */ class SymbolicState { @@ -42,6 +50,8 @@ public: //@{ /// Value of `this` address. smtutil::Expression thisAddress(); + /// @returns the symbolic balances. + smtutil::Expression balances(); /// @returns the symbolic balance of address `this`. smtutil::Expression balance(); /// @returns the symbolic balance of an address. @@ -49,6 +59,12 @@ public: SymbolicIntVariable& errorFlag(); + /// @returns the state as a tuple. + smtutil::Expression state(); + + /// @returns the state sort. + smtutil::SortPointer stateSort(); + /// Transfer _value from _from to _to. void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value); //@} @@ -57,27 +73,27 @@ 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; - /// Symbolic `this` address. - SymbolicAddressVariable m_thisAddress{ - "this", - m_context - }; - - /// Symbolic balances. - SymbolicArrayVariable m_balances{ - std::make_shared(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort), - "balances", - m_context - }; - - smt::SymbolicIntVariable m_error{ + SymbolicIntVariable m_error{ TypeProvider::uint256(), TypeProvider::uint256(), "error", m_context }; + + SymbolicAddressVariable m_thisAddress{ + "this", + m_context + }; + + std::map m_componentIndices; + /// balances, TODO storage of other contracts + std::map m_stateMembers; + std::unique_ptr m_stateTuple; }; }