solidity/libsolidity/formal/SymbolicState.h

252 lines
8.5 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 chainid
2020-09-29 08:36:20 +00:00
* - 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; }
SymbolicIntVariable const& errorFlag() const { return m_error; }
2020-09-29 08:36:20 +00:00
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 txFunctionConstraints(FunctionDefinition const& _function) const;
smtutil::Expression txTypeConstraints() const;
smtutil::Expression txNonPayableConstraint() const;
2020-09-29 08:36:20 +00:00
smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
//@}
/// Crypto functions.
//@{
/// @returns the crypto functions represented as a tuple of arrays.
smtutil::Expression crypto() const { return m_crypto.value(); }
smtutil::Expression crypto(unsigned _idx) const { return m_crypto.value(_idx); }
smtutil::SortPointer const& cryptoSort() const { return m_crypto.sort(); }
void newCrypto() { m_crypto.newVar(); }
smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); }
//@}
/// 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,
std::vector<TypePointer>,
std::vector<TypePointer>
>;
SymbolicABIFunction const& abiFunctionTypes(FunctionCall const* _funCall) const;
smtutil::Expression abi() const { solAssert(m_abi, ""); return m_abi->value(); }
smtutil::Expression abi(unsigned _idx) const { solAssert(m_abi, ""); return m_abi->value(_idx); }
smtutil::SortPointer const& abiSort() const { solAssert(m_abi, ""); return m_abi->sort(); }
void newABI() { solAssert(m_abi, ""); m_abi->newVar(); }
//@}
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
/// Builds m_abi based on the abi.* calls _abiFunctions.
void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);
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",
{
{"block.chainid", smtutil::SortProvider::uintSort},
2020-09-29 08:36:20 +00:00
{"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},
2021-01-20 10:22:28 +00:00
{"blockhash", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)},
2020-09-29 08:36:20 +00:00
// 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
};
BlockchainVariable m_crypto{
"crypto",
{
{"keccak256", std::make_shared<smtutil::ArraySort>(
smt::smtSort(*TypeProvider::bytesStorage()),
smtSort(*TypeProvider::fixedBytes(32))
)},
{"sha256", std::make_shared<smtutil::ArraySort>(
smt::smtSort(*TypeProvider::bytesStorage()),
smtSort(*TypeProvider::fixedBytes(32))
)},
{"ripemd160", std::make_shared<smtutil::ArraySort>(
smt::smtSort(*TypeProvider::bytesStorage()),
smtSort(*TypeProvider::fixedBytes(20))
)},
{"ecrecover", std::make_shared<smtutil::ArraySort>(
std::make_shared<smtutil::TupleSort>(
"ecrecover_input_type",
std::vector<std::string>{"hash", "v", "r", "s"},
std::vector<smtutil::SortPointer>{
smt::smtSort(*TypeProvider::fixedBytes(32)),
smt::smtSort(*TypeProvider::uint(8)),
smt::smtSort(*TypeProvider::fixedBytes(32)),
smt::smtSort(*TypeProvider::fixedBytes(32))
}
),
smtSort(*TypeProvider::address())
)}
},
m_context
};
/// Tuple containing all used ABI functions.
std::unique_ptr<BlockchainVariable> m_abi;
/// Maps ABI functions calls to their tuple names generated by
/// `buildABIFunctions`.
std::map<FunctionCall const*, SymbolicABIFunction> m_abiMembers;
2020-03-24 19:15:15 +00:00
};
}