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

Move stateVariablesIncludingInheritedAndPrivate from CHC to SMTEncoder

Browse Source
This commit is contained in:
Leonardo Alt 2020-08-19 13:51:58 +02:00
parent 016b9b83a8
commit 5bbb20d3cb
4 changed files with 23 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
libsolidity/formal/CHC.cpp
View File

@ -114,7 +114,7 @@ bool CHC::visit(ContractDefinition const& _contract)
initContract(_contract); initContract(_contract);
m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
m_stateSorts = stateSorts(_contract); m_stateSorts = stateSorts(_contract);
clearIndices(&_contract); clearIndices(&_contract);
@ -738,24 +738,10 @@ set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTN
return assertions; return assertions;
} }
vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
{
return fold(
_contract.annotation().linearizedBaseContracts,
vector<VariableDeclaration const*>{},
[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
);
}
vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
{
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
}
vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract) vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
{ {
return applyMap( return applyMap(
stateVariablesIncludingInheritedAndPrivate(_contract), SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
[](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); } [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
); );
} }
@ -848,7 +834,7 @@ smtutil::SortPointer CHC::sort(ASTNode const* _node)
smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract) smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
{ {
auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract); auto stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
auto sorts = stateSorts(_contract); auto sorts = stateSorts(_contract);
auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }; auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
@ -878,7 +864,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get())) if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
for (auto const* base: contract->annotation().linearizedBaseContracts) for (auto const* base: contract->annotation().linearizedBaseContracts)
{ {
for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base)) for (auto const* var: SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*base))
if (!m_context.knownVariable(*var)) if (!m_context.knownVariable(*var))
createVariable(*var); createVariable(*var);
@ -1048,7 +1034,7 @@ vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract) vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
{ {
return applyMap( return applyMap(
stateVariablesIncludingInheritedAndPrivate(_contract), SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
[&](auto _var) { return valueAtIndex(*_var, _index); } [&](auto _var) { return valueAtIndex(*_var, _index); }
); );
} }
@ -1061,7 +1047,7 @@ vector<smtutil::Expression> CHC::currentStateVariables()
vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract) vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
{ {
return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
} }
vector<smtutil::Expression> CHC::currentFunctionVariables() vector<smtutil::Expression> CHC::currentFunctionVariables()

2
libsolidity/formal/CHC.h
View File

@ -111,8 +111,6 @@ private:
void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
void setCurrentBlock(Predicate const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr); void setCurrentBlock(Predicate const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot); std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
//@} //@}
/// Sort helpers. /// Sort helpers.

14
libsolidity/formal/SMTEncoder.cpp
View File

@ -1982,6 +1982,20 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons
return funDef; return funDef;
} }
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
{
return fold(
_contract.annotation().linearizedBaseContracts,
vector<VariableDeclaration const*>{},
[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
);
}
vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
{
return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
}
void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
{ {
FunctionDefinition const* funDef = functionCallToDefinition(_funCall); FunctionDefinition const* funDef = functionCallToDefinition(_funCall);

3
libsolidity/formal/SMTEncoder.h
View File

@ -62,6 +62,9 @@ public:
/// if possible or nullptr. /// if possible or nullptr.
static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall); static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
protected: protected:
// TODO: Check that we do not have concurrent reads and writes to a variable, // TODO: Check that we do not have concurrent reads and writes to a variable,
// because the order of expression evaluation is undefined // because the order of expression evaluation is undefined