solidity/libsolidity/formal/SymbolicState.h

177 lines
5.7 KiB
C
Raw Normal View History

2020-03-24 19:15:15 +00:00
/*
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/>.
*/
// SPDX-License-Identifier: GPL-3.0
2020-03-24 19:15:15 +00:00
#pragma once
2020-09-29 08:36:20 +00:00
#include <libsolidity/formal/SymbolicTypes.h>
2020-03-24 19:15:15 +00:00
#include <libsolidity/formal/SymbolicVariables.h>
2020-05-18 15:42:24 +00:00
#include <libsmtutil/Sorts.h>
#include <libsmtutil/SolverInterface.h>
2020-03-24 19:15:15 +00:00
namespace solidity::frontend::smt
{
class EncodingContext;
2020-09-07 14:45:14 +00:00
class SymbolicAddressVariable;
class SymbolicArrayVariable;
2020-03-24 19:15:15 +00:00
2020-09-29 08:36:20 +00:00
class BlockchainVariable
{
public:
BlockchainVariable(std::string _name, std::map<std::string, smtutil::SortPointer> _members, EncodingContext& _context);
/// @returns the variable data as a tuple.
smtutil::Expression value() const { return m_tuple->currentValue(); }
smtutil::Expression value(unsigned _idx) const { return m_tuple->valueAtIndex(_idx); }
smtutil::SortPointer const& sort() const { return m_tuple->sort(); }
unsigned index() const { return m_tuple->index(); }
void newVar() { m_tuple->increaseIndex(); }
void reset() { m_tuple->resetIndex(); }
/// @returns the symbolic _member.
smtutil::Expression member(std::string const& _member) const;
/// Generates a new tuple where _member is assigned _value.
smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _value);
private:
std::string const m_name;
std::map<std::string, smtutil::SortPointer> const m_members;
EncodingContext& m_context;
std::map<std::string, unsigned> m_componentIndices;
std::unique_ptr<SymbolicTupleVariable> m_tuple;
};
2020-03-24 19:15:15 +00:00
/**
2020-09-07 14:45:14 +00:00
* 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
2020-09-29 08:36:20 +00:00
* - block and transaction properties, represented as a tuple of:
* - blockhash
* - block coinbase
* - block difficulty
* - block gaslimit
* - block number
* - block timestamp
* - TODO gasleft
* - msg data
* - msg sender
* - msg sig
* - msg value
* - tx gasprice
* - tx origin
2020-03-24 19:15:15 +00:00
*/
class SymbolicState
{
public:
2020-09-29 08:36:20 +00:00
SymbolicState(EncodingContext& _context): m_context(_context) {}
2020-03-24 19:15:15 +00:00
void reset();
2020-09-29 08:36:20 +00:00
/// Error flag.
2020-03-24 19:15:15 +00:00
//@{
2020-09-29 08:36:20 +00:00
SymbolicIntVariable& errorFlag() { return m_error; }
smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); }
//@}
2020-09-18 16:55:23 +00:00
2020-09-29 08:36:20 +00:00
/// This.
//@{
2020-09-18 16:55:23 +00:00
/// @returns the symbolic value of the currently executing contract's address.
2020-09-29 08:36:20 +00:00
smtutil::Expression thisAddress() const { return m_thisAddress.currentValue(); }
smtutil::Expression thisAddress(unsigned _idx) const { return m_thisAddress.valueAtIndex(_idx); }
smtutil::SortPointer const& thisAddressSort() const { return m_thisAddress.sort(); }
//@}
2020-09-18 16:55:23 +00:00
2020-09-29 08:36:20 +00:00
/// 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(); }
2020-09-07 14:45:14 +00:00
/// @returns the symbolic balances.
2020-09-29 08:36:20 +00:00
smtutil::Expression balances() const;
2020-03-24 19:15:15 +00:00
/// @returns the symbolic balance of address `this`.
2020-09-29 08:36:20 +00:00
smtutil::Expression balance() const;
2020-03-24 19:15:15 +00:00
/// @returns the symbolic balance of an address.
2020-09-29 08:36:20 +00:00
smtutil::Expression balance(smtutil::Expression _address) const;
2020-03-24 19:15:15 +00:00
/// Transfer _value from _from to _to.
2020-05-19 12:14:46 +00:00
void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
2020-03-24 19:15:15 +00:00
//@}
2020-09-29 08:36:20 +00:00
/// Transaction data.
//@{
/// @returns the tx data as a tuple.
smtutil::Expression tx() const { return m_tx.value(); }
smtutil::Expression tx(unsigned _idx) const { return m_tx.value(_idx); }
smtutil::SortPointer const& txSort() const { return m_tx.sort(); }
void newTx() { m_tx.newVar(); }
smtutil::Expression txMember(std::string const& _member) const;
smtutil::Expression txConstraints(FunctionDefinition const& _function) const;
smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
//@}
2020-03-24 19:15:15 +00:00
private:
/// Adds _value to _account's balance.
2020-05-19 12:14:46 +00:00
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
2020-03-24 19:15:15 +00:00
EncodingContext& m_context;
2020-09-07 14:45:14 +00:00
SymbolicIntVariable m_error{
TypeProvider::uint256(),
TypeProvider::uint256(),
"error",
2020-03-24 19:15:15 +00:00
m_context
};
2020-09-07 14:45:14 +00:00
SymbolicAddressVariable m_thisAddress{
"this",
2020-03-24 19:15:15 +00:00
m_context
};
2020-09-29 08:36:20 +00:00
BlockchainVariable m_state{
"state",
{{"balances", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)}},
m_context
};
BlockchainVariable m_tx{
"tx",
{
{"blockhash", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)},
{"block.coinbase", smt::smtSort(*TypeProvider::address())},
{"block.difficulty", smtutil::SortProvider::uintSort},
{"block.gaslimit", smtutil::SortProvider::uintSort},
{"block.number", smtutil::SortProvider::uintSort},
{"block.timestamp", smtutil::SortProvider::uintSort},
// TODO gasleft
{"msg.data", smt::smtSort(*TypeProvider::bytesMemory())},
{"msg.sender", smt::smtSort(*TypeProvider::address())},
{"msg.sig", smtutil::SortProvider::uintSort},
{"msg.value", smtutil::SortProvider::uintSort},
{"tx.gasprice", smtutil::SortProvider::uintSort},
{"tx.origin", smt::smtSort(*TypeProvider::address())}
},
m_context
};
2020-03-24 19:15:15 +00:00
};
}