From 05a85461fe43f61e972f564d481188e51746022a Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 24 Mar 2020 20:15:15 +0100 Subject: [PATCH] Symbolic state --- libsolidity/CMakeLists.txt | 2 + libsolidity/formal/BMC.cpp | 3 +- libsolidity/formal/EncodingContext.cpp | 57 +----------------- libsolidity/formal/EncodingContext.h | 25 ++------ libsolidity/formal/SMTEncoder.cpp | 9 +-- libsolidity/formal/SymbolicState.cpp | 82 ++++++++++++++++++++++++++ libsolidity/formal/SymbolicState.h | 71 ++++++++++++++++++++++ 7 files changed, 169 insertions(+), 80 deletions(-) create mode 100644 libsolidity/formal/SymbolicState.cpp create mode 100644 libsolidity/formal/SymbolicState.h diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index c7a517a0b..efb553e1a 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -106,6 +106,8 @@ set(sources formal/Sorts.h formal/SSAVariable.cpp formal/SSAVariable.h + formal/SymbolicState.cpp + formal/SymbolicState.h formal/SymbolicTypes.cpp formal/SymbolicTypes.h formal/SymbolicVariables.cpp diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 141a3eb32..1b4e8174a 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -18,6 +18,7 @@ #include #include +#include #include #include @@ -376,7 +377,7 @@ void BMC::endVisit(FunctionCall const& _funCall) SMTEncoder::endVisit(_funCall); auto value = _funCall.arguments().front(); solAssert(value, ""); - smt::Expression thisBalance = m_context.balance(); + smt::Expression thisBalance = m_context.state().balance(); addVerificationTarget( VerificationTarget::Type::Balance, diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 1f7b7a5e0..7ba51d657 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -25,13 +25,8 @@ using namespace solidity::util; using namespace solidity::frontend::smt; EncodingContext::EncodingContext(): - m_thisAddress(make_unique("this", *this)) + m_state(*this) { - auto sort = make_shared( - SortProvider::intSort, - SortProvider::intSort - ); - m_balances = make_unique(sort, "balances", *this); } void EncodingContext::reset() @@ -39,8 +34,7 @@ void EncodingContext::reset() resetAllVariables(); m_expressions.clear(); m_globalContext.clear(); - m_thisAddress->resetIndex(); - m_balances->resetIndex(); + m_state.reset(); m_assertions.clear(); } @@ -183,40 +177,6 @@ bool EncodingContext::knownGlobalSymbol(string const& _var) const return m_globalContext.count(_var); } -// Blockchain - -Expression EncodingContext::thisAddress() -{ - return m_thisAddress->currentValue(); -} - -Expression EncodingContext::balance() -{ - return balance(m_thisAddress->currentValue()); -} - -Expression EncodingContext::balance(Expression _address) -{ - return Expression::select(m_balances->currentValue(), move(_address)); -} - -void EncodingContext::transfer(Expression _from, Expression _to, Expression _value) -{ - unsigned indexBefore = m_balances->index(); - addBalance(_from, 0 - _value); - addBalance(_to, move(_value)); - unsigned indexAfter = m_balances->index(); - solAssert(indexAfter > indexBefore, ""); - m_balances->increaseIndex(); - /// Do not apply the transfer operation if _from == _to. - auto newBalances = Expression::ite( - move(_from) == move(_to), - m_balances->valueAtIndex(indexBefore), - m_balances->valueAtIndex(indexAfter) - ); - addAssertion(m_balances->currentValue() == newBalances); -} - /// Solver. Expression EncodingContext::assertions() @@ -248,16 +208,3 @@ void EncodingContext::addAssertion(Expression const& _expr) else m_assertions.back() = _expr && move(m_assertions.back()); } - -/// Private helpers. - -void EncodingContext::addBalance(Expression _address, Expression _value) -{ - auto newBalances = Expression::store( - m_balances->currentValue(), - _address, - balance(_address) + move(_value) - ); - m_balances->increaseIndex(); - addAssertion(newBalances == m_balances->currentValue()); -} diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index 648f7dc33..d62de055d 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -18,6 +18,7 @@ #pragma once #include +#include #include #include @@ -121,18 +122,6 @@ public: bool knownGlobalSymbol(std::string const& _var) const; //@} - /// Blockchain. - //@{ - /// Value of `this` address. - Expression thisAddress(); - /// @returns the symbolic balance of address `this`. - Expression balance(); - /// @returns the symbolic balance of an address. - Expression balance(Expression _address); - /// Transfer _value from _from to _to. - void transfer(Expression _from, Expression _to, Expression _value); - //@} - /// Solver. //@{ /// @returns conjunction of all added assertions. @@ -148,10 +137,9 @@ public: } //@} -private: - /// Adds _value to _account's balance. - void addBalance(Expression _account, Expression _value); + SymbolicState& state() { return m_state; } +private: /// Symbolic expressions. //{@ /// Symbolic variables. @@ -164,11 +152,8 @@ private: /// variables and functions. std::unordered_map> m_globalContext; - /// Symbolic `this` address. - std::unique_ptr m_thisAddress; - - /// Symbolic balances. - std::unique_ptr m_balances; + /// Symbolic representation of the blockchain state. + SymbolicState m_state; //@} /// Solver related. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 0efaf90a9..f02d32aae 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -19,6 +19,7 @@ #include #include +#include #include #include @@ -619,10 +620,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) auto const& value = args.front(); solAssert(value, ""); - smt::Expression thisBalance = m_context.balance(); + smt::Expression thisBalance = m_context.state().balance(); setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context); - m_context.transfer(m_context.thisAddress(), expr(address), expr(*value)); + m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value)); break; } default: @@ -711,7 +712,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier) defineGlobalVariable(_identifier.name(), _identifier); else if (_identifier.name() == "this") { - defineExpr(_identifier, m_context.thisAddress()); + defineExpr(_identifier, m_context.state().thisAddress()); m_uninterpretedTerms.insert(&_identifier); } else @@ -858,7 +859,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess) _memberAccess.expression().accept(*this); if (_memberAccess.memberName() == "balance") { - defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression()))); + defineExpr(_memberAccess, m_context.state().balance(expr(_memberAccess.expression()))); setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context); m_uninterpretedTerms.insert(&_memberAccess); return false; diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp new file mode 100644 index 000000000..d38e79c54 --- /dev/null +++ b/libsolidity/formal/SymbolicState.cpp @@ -0,0 +1,82 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#include + +#include + +using namespace std; +using namespace solidity::frontend::smt; + +SymbolicState::SymbolicState(EncodingContext& _context): + m_context(_context) +{ +} + +void SymbolicState::reset() +{ + m_thisAddress.resetIndex(); + m_balances.resetIndex(); +} + +// Blockchain + +Expression SymbolicState::thisAddress() +{ + return m_thisAddress.currentValue(); +} + +Expression SymbolicState::balance() +{ + return balance(m_thisAddress.currentValue()); +} + +Expression SymbolicState::balance(Expression _address) +{ + return Expression::select(m_balances.currentValue(), move(_address)); +} + +void SymbolicState::transfer(Expression _from, Expression _to, Expression _value) +{ + unsigned indexBefore = m_balances.index(); + addBalance(_from, 0 - _value); + addBalance(_to, move(_value)); + unsigned indexAfter = m_balances.index(); + solAssert(indexAfter > indexBefore, ""); + m_balances.increaseIndex(); + /// Do not apply the transfer operation if _from == _to. + auto newBalances = Expression::ite( + move(_from) == move(_to), + m_balances.valueAtIndex(indexBefore), + m_balances.valueAtIndex(indexAfter) + ); + m_context.addAssertion(m_balances.currentValue() == newBalances); +} + +/// Private helpers. + +void SymbolicState::addBalance(Expression _address, Expression _value) +{ + auto newBalances = Expression::store( + m_balances.currentValue(), + _address, + balance(_address) + move(_value) + ); + m_balances.increaseIndex(); + m_context.addAssertion(newBalances == m_balances.currentValue()); +} + diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h new file mode 100644 index 000000000..380bfda51 --- /dev/null +++ b/libsolidity/formal/SymbolicState.h @@ -0,0 +1,71 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#pragma once + +#include +#include +#include + +namespace solidity::frontend::smt +{ + +class EncodingContext; + +/** + * Symbolic representation of the blockchain state. + */ +class SymbolicState +{ +public: + SymbolicState(EncodingContext& _context); + + void reset(); + + /// Blockchain. + //@{ + /// Value of `this` address. + Expression thisAddress(); + /// @returns the symbolic balance of address `this`. + Expression balance(); + /// @returns the symbolic balance of an address. + Expression balance(Expression _address); + /// Transfer _value from _from to _to. + void transfer(Expression _from, Expression _to, Expression _value); + //@} + +private: + /// Adds _value to _account's balance. + void addBalance(Expression _account, Expression _value); + + EncodingContext& m_context; + + /// Symbolic `this` address. + SymbolicAddressVariable m_thisAddress{ + "this", + m_context + }; + + /// Symbolic balances. + SymbolicArrayVariable m_balances{ + std::make_shared(SortProvider::intSort, SortProvider::intSort), + "balances", + m_context + }; +}; + +}