cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Symbolic state

Browse Source
This commit is contained in:
Leonardo Alt 2020-03-24 20:15:15 +01:00
parent 0a72a3b8af
commit 05a85461fe
7 changed files with 169 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libsolidity/CMakeLists.txt
View File

@ -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

3
libsolidity/formal/BMC.cpp
View File

@ -18,6 +18,7 @@
#include <libsolidity/formal/BMC.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <boost/algorithm/string/replace.hpp>
@ -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,

57
libsolidity/formal/EncodingContext.cpp
View File

@ -25,13 +25,8 @@ using namespace solidity::util;
using namespace solidity::frontend::smt;
EncodingContext::EncodingContext():
m_thisAddress(make_unique<SymbolicAddressVariable>("this", *this))
m_state(*this)
{
auto sort = make_shared<ArraySort>(
SortProvider::intSort,
SortProvider::intSort
);
m_balances = make_unique<SymbolicVariable>(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());
}

25
libsolidity/formal/EncodingContext.h
View File

@ -18,6 +18,7 @@
#pragma once
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicVariables.h>
#include <unordered_map>
@ -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<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
/// Symbolic `this` address.
std::unique_ptr<SymbolicAddressVariable> m_thisAddress;
/// Symbolic balances.
std::unique_ptr<SymbolicVariable> m_balances;
/// Symbolic representation of the blockchain state.
SymbolicState m_state;
//@}
/// Solver related.

9
libsolidity/formal/SMTEncoder.cpp
View File

@ -19,6 +19,7 @@
#include <libsolidity/ast/TypeProvider.h>
#include <libsolidity/formal/SMTPortfolio.h>
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/SymbolicTypes.h>
#include <boost/range/adaptors.hpp>
@ -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;

82
libsolidity/formal/SymbolicState.cpp Normal file
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
#include <libsolidity/formal/SymbolicState.h>
#include <libsolidity/formal/EncodingContext.h>
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());
}

71
libsolidity/formal/SymbolicState.h Normal file
View File

@ -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 <http://www.gnu.org/licenses/>.
*/
#pragma once
#include <libsolidity/formal/Sorts.h>
#include <libsolidity/formal/SolverInterface.h>
#include <libsolidity/formal/SymbolicVariables.h>
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<ArraySort>(SortProvider::intSort, SortProvider::intSort),
"balances",
m_context
};
};
}