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

Add constraints correlating address(this).balance and msg.value

Browse Source
This commit is contained in:
Leo Alt 2021-08-20 15:49:36 +02:00
parent c69f91917d
commit 61160aa0e7
7 changed files with 123 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -6,6 +6,7 @@ Language Features:
Compiler Features:
* Immutable variables can be read at construction time once they are initialized.
* SMTChecker: Support low level ``call`` as external calls to unknown code.
* SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``.
Bugfixes:

12
libsmtutil/Sorts.h
View File

@ -159,7 +159,15 @@ struct TupleSort: public Sort
name(std::move(_name)),
members(std::move(_members)),
components(std::move(_components))
{}
{
for (size_t i = 0; i < members.size(); ++i)
memberToIndex[members.at(i)] = i;
}
SortPointer memberSort(std::string const& _member)
{
return components.at(memberToIndex.at(_member));
}
bool operator==(Sort const& _other) const override
{
@ -186,8 +194,10 @@ struct TupleSort: public Sort
std::string const name;
std::vector<std::string> const members;
std::vector<SortPointer> const components;
std::map<std::string, size_t> memberToIndex;
};
/** Frequently used sorts.*/
struct SortProvider
{

77
libsolidity/formal/CHC.cpp
View File

@ -169,7 +169,13 @@ void CHC::endVisit(ContractDefinition const& _contract)
smtutil::Expression zeroes(true);
for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
addRule(smtutil::Expression::implies(initialConstraints(_contract) && zeroes, predicate(entry)), entry.functor().name);
// The contract's address might already have funds before deployment,
// so the balance must be at least `msg.value`, but not equals.
auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value");
addRule(smtutil::Expression::implies(
initialConstraints(_contract) && zeroes && initialBalanceConstraint,
predicate(entry)
), entry.functor().name);
setCurrentBlock(entry);
solAssert(!m_errorDest, "");
@ -315,11 +321,16 @@ void CHC::endVisit(FunctionDefinition const& _function)
shouldAnalyze(*m_currentContract)
)
{
auto sum = summary(_function);
defineExternalFunctionInterface(_function, *m_currentContract);
setCurrentBlock(*m_interfaces.at(m_currentContract));
// Create the rule
// interface \land externalFunctionEntry => interface'
auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(_function);
m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre});
connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0);
auto sum = externalSummary(_function);
m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre});
connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0);
}
m_currentFunction = nullptr;
@ -949,6 +960,7 @@ void CHC::resetSourceAnalysis()
m_queryPlaceholders.clear();
m_callGraph.clear();
m_summaries.clear();
m_externalSummaries.clear();
m_interfaces.clear();
m_nondetInterfaces.clear();
m_constructorSummaries.clear();
@ -1128,6 +1140,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
if (!function->isConstructor() && function->isPublic() && resolved.count(function))
{
m_externalSummaries[contract].emplace(function, createSummaryBlock(*function, *contract));
auto state1 = stateVariablesAtIndex(1, *contract);
auto state2 = stateVariablesAtIndex(2, *contract);
@ -1144,12 +1158,41 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_summaries.at(contract).at(function))(args));
connectBlocks(nondetPre, nondetPost, errorPre == 0 && (*m_externalSummaries.at(contract).at(function))(args));
}
}
}
}
void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
// Create a rule that represents an external call to this function.
// This contains more things than the function body itself,
// such as balance updates because of ``msg.value``.
auto functionEntryBlock = createBlock(&_function, PredicateType::FunctionBlock);
auto functionPred = predicate(*functionEntryBlock);
addRule(functionPred, functionPred.name);
setCurrentBlock(*functionEntryBlock);
m_context.addAssertion(initialConstraints(_contract, &_function));
m_context.addAssertion(state().txTypeConstraints() && state().txFunctionConstraints(_function));
// The contract may have received funds through a selfdestruct or
// block.coinbase, which do not trigger calls into the contract.
// So the only constraint we can add here is that the balance of
// the contract grows by at least `msg.value`.
SymbolicIntVariable k{TypeProvider::uint256(), TypeProvider::uint256(), "funds_" + to_string(m_context.newUniqueId()), m_context};
m_context.addAssertion(k.currentValue() >= state().txMember("msg.value"));
// Assume that address(this).balance cannot overflow.
m_context.addAssertion(smt::symbolicUnknownConstraints(state().balance(state().thisAddress()) + k.currentValue(), TypeProvider::uint256()));
state().addBalance(state().thisAddress(), k.currentValue());
errorFlag().increaseIndex();
m_context.addAssertion(summaryCall(_function));
connectBlocks(functionPred, externalSummary(_function));
}
void CHC::defineContractInitializer(ContractDefinition const& _contract, ContractDefinition const& _contextContract)
{
m_contractInitializers[&_contextContract][&_contract] = createConstructorBlock(_contract, "contract_initializer");
@ -1220,12 +1263,34 @@ smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDe
return smt::function(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
}
smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
return smt::functionCall(*m_summaries.at(&_contract).at(&_function), &_contract, m_context);
}
smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract)
{
return smt::function(*m_externalSummaries.at(&_contract).at(&_function), &_contract, m_context);
}
smtutil::Expression CHC::summary(FunctionDefinition const& _function)
{
solAssert(m_currentContract, "");
return summary(_function, *m_currentContract);
}
smtutil::Expression CHC::summaryCall(FunctionDefinition const& _function)
{
solAssert(m_currentContract, "");
return summaryCall(_function, *m_currentContract);
}
smtutil::Expression CHC::externalSummary(FunctionDefinition const& _function)
{
solAssert(m_currentContract, "");
return externalSummary(_function, *m_currentContract);
}
Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, string const& _prefix)
{
auto block = createSymbolicBlock(

16
libsolidity/formal/CHC.h
View File

@ -164,6 +164,12 @@ private:
/// in a given _source.
void defineInterfacesAndSummaries(SourceUnit const& _source);
/// Creates the rule
/// summary_function \land transaction_entry_constraints => external_summary_function
/// This is needed to add these transaction entry constraints which include
/// potential balance increase by external means, for example.
void defineExternalFunctionInterface(FunctionDefinition const& _function, ContractDefinition const& _contract);
/// Creates a CHC system that, for a given contract,
/// - initializes its state variables (as 0 or given value, if any).
/// - "calls" the explicit constructor function of the contract, if any.
@ -225,6 +231,13 @@ private:
/// @returns a predicate that defines a function summary.
smtutil::Expression summary(FunctionDefinition const& _function);
smtutil::Expression summary(FunctionDefinition const& _function, ContractDefinition const& _contract);
/// @returns a predicate that applies a function summary
/// over the constrained variables.
smtutil::Expression summaryCall(FunctionDefinition const& _function);
smtutil::Expression summaryCall(FunctionDefinition const& _function, ContractDefinition const& _contract);
/// @returns a predicate that defines an external function summary.
smtutil::Expression externalSummary(FunctionDefinition const& _function);
smtutil::Expression externalSummary(FunctionDefinition const& _function, ContractDefinition const& _contract);
//@}
/// Solver related.
@ -317,6 +330,9 @@ private:
/// Function predicates.
std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_summaries;
/// External function predicates.
std::map<ContractDefinition const*, std::map<FunctionDefinition const*, Predicate const*>> m_externalSummaries;
//@}
/// Variables.

4
libsolidity/formal/SMTEncoder.cpp
View File

@ -2283,9 +2283,7 @@ void SMTEncoder::resetStorageVariables()
void SMTEncoder::resetBalances()
{
// TODO this should be changed to `balances` only
// when `state` gets more members.
state().newState();
state().newBalances();
}
void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)

28
libsolidity/formal/SymbolicState.cpp
View File

@ -104,6 +104,14 @@ smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) c
return smtutil::Expression::select(m_tx.member("blockhash"), move(_blockNumber));
}
void SymbolicState::newBalances()
{
auto tupleSort = dynamic_pointer_cast<TupleSort>(stateSort());
auto balanceSort = tupleSort->components.at(tupleSort->memberToIndex.at("balances"));
SymbolicVariable newBalances(balanceSort, "fresh_balances_" + to_string(m_context.newUniqueId()), m_context);
m_state.assignMember("balances", newBalances.currentValue());
}
void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value)
{
unsigned indexBefore = m_state.index();
@ -121,6 +129,16 @@ void SymbolicState::transfer(smtutil::Expression _from, smtutil::Expression _to,
m_context.addAssertion(m_state.value() == newState);
}
void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
{
auto newBalances = smtutil::Expression::store(
balances(),
_address,
balance(_address) + move(_value)
);
m_state.assignMember("balances", newBalances);
}
smtutil::Expression SymbolicState::txMember(string const& _member) const
{
return m_tx.member(_member);
@ -181,16 +199,6 @@ void SymbolicState::prepareForSourceUnit(SourceUnit const& _source)
/// Private helpers.
void SymbolicState::addBalance(smtutil::Expression _address, smtutil::Expression _value)
{
auto newBalances = smtutil::Expression::store(
balances(),
_address,
balance(_address) + move(_value)
);
m_state.assignMember("balances", newBalances);
}
void SymbolicState::buildABIFunctions(set<FunctionCall const*> const& _abiFunctions)
{
map<string, SortPointer> functions;

8
libsolidity/formal/SymbolicState.h
View File

@ -108,6 +108,8 @@ public:
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(); }
void newBalances();
/// @returns the symbolic balances.
smtutil::Expression balances() const;
/// @returns the symbolic balance of address `this`.
@ -117,6 +119,9 @@ public:
/// Transfer _value from _from to _to.
void transfer(smtutil::Expression _from, smtutil::Expression _to, smtutil::Expression _value);
/// Adds _value to _account's balance.
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
//@}
/// Transaction data.
@ -163,9 +168,6 @@ public:
//@}
private:
/// Adds _value to _account's balance.
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
/// Builds m_abi based on the abi.* calls _abiFunctions.
void buildABIFunctions(std::set<FunctionCall const*> const& _abiFunctions);