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

Merge pull request #9518 from ethereum/smt_fix_bmc_function_inlining

Browse Source 
[SMTChecker] Fix ICE in BMC function inlining
This commit is contained in:
chriseth 2020-08-06 00:50:04 +02:00 committed by GitHub
commit 3a409c39e4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 38 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -8,6 +8,7 @@ Compiler Features:
Bugfixes:
* Optimizer: Keep side-effects of ``x`` in ``byte(a, shr(b, x))`` even if the constants ``a`` and ``b`` would make the expression zero unconditionally. This optimizer rule is very hard if not impossible to trigger in a way that it can result in invalid code, though.
* SMTChecker: Fix internal error in BMC function inlining.
* SMTChecker: Fix internal error on fixed bytes index access.
* References Resolver: Fix internal bug when using constructor for library.

2
libsolidity/formal/BMC.cpp
View File

@ -61,7 +61,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
m_context.setSolver(m_interface.get());
m_context.clear();
m_context.setAssertionAccumulation(true);
m_variableUsage.setFunctionInlining(true);
m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
_source.accept(*this);

1
libsolidity/formal/CHC.cpp
View File

@ -82,7 +82,6 @@ void CHC::analyze(SourceUnit const& _source)
}
m_context.clear();
m_context.setAssertionAccumulation(false);
m_variableUsage.setFunctionInlining(false);
resetSourceAnalysis();

4
libsolidity/formal/VariableUsage.cpp
View File

@ -60,8 +60,8 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
void VariableUsage::endVisit(FunctionCall const& _funCall)
{
if (m_inlineFunctionCalls)
if (auto const& funDef = SMTEncoder::functionCallToDefinition(_funCall))
if (m_inlineFunctionCalls(_funCall))
if (auto funDef = SMTEncoder::functionCallToDefinition(_funCall))
{
solAssert(funDef, "");
if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())

4
libsolidity/formal/VariableUsage.h
View File

@ -36,7 +36,7 @@ public:
std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<CallableDeclaration const*> const& _outerCallstack);
/// Sets whether to inline function calls.
void setFunctionInlining(bool _inlineFunction) { m_inlineFunctionCalls = _inlineFunction; }
void setFunctionInlining(std::function<bool(FunctionCall const&)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
private:
void endVisit(Identifier const& _node) override;
@ -54,7 +54,7 @@ private:
std::vector<CallableDeclaration const*> m_callStack;
CallableDeclaration const* m_lastCall = nullptr;
bool m_inlineFunctionCalls = false;
std::function<bool(FunctionCall const&)> m_inlineFunctionCalls = [](FunctionCall const&) { return false; };
};
}

16
test/libsolidity/smtCheckerTests/functions/function_external_call_should_not_inline_1.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract State {
C c;
function f() public returns (uint) {
while(true)
c.setOwner();
}
}
contract C {
address owner;
function setOwner() public {
owner = address(0);
}
}
// ----
// Warning 5084: (198-208): Type conversion is not yet fully supported and might yield false positives.

16
test/libsolidity/smtCheckerTests/functions/function_external_call_should_not_inline_2.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract Other {
C c;
function h(bool b) public {
if (b)
c.setOwner(address(0));
}
}
contract C {
address owner;
function setOwner(address _owner) public {
owner = _owner;
}
}
// ----
// Warning 5084: (107-117): Type conversion is not yet fully supported and might yield false positives.