cerc-io/solidity
11
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

[SMTChecker] Inline external function calls to this.

Browse Source
This commit is contained in:
Leonardo Alt
2019-05-09 16:53:30 +02:00
parent c3a1c168d0
commit ef32bf185f
8 changed files with 108 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTChecker.cpp
+35 -6
View File
@@ -666,8 +666,6 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
visitGasLeft(_funCall);
break;
case FunctionType::Kind::Internal:
inlineFunctionCall(_funCall);
break;
case FunctionType::Kind::External:
case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCall:
@@ -675,9 +673,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::BareDelegateCall:
case FunctionType::Kind::BareStaticCall:
case FunctionType::Kind::Creation:
m_externalFunctionCallHappened = true;
resetStateVariables();
resetStorageReferences();
internalOrExternalFunctionCall(_funCall);
break;
case FunctionType::Kind::KECCAK256:
case FunctionType::Kind::ECRecover:
@@ -805,6 +801,25 @@ void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall)
}
}
void SMTChecker::internalOrExternalFunctionCall(FunctionCall const& _funCall)
{
auto funDef = inlinedFunctionCallToDefinition(_funCall);
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
if (funDef)
inlineFunctionCall(_funCall);
else if (funType.kind() == FunctionType::Kind::Internal)
m_errorReporter.warning(
_funCall.location(),
"Assertion checker does not yet implement this type of function call."
);
else
{
m_externalFunctionCallHappened = true;
resetStateVariables();
resetStorageReferences();
}
}
void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall)
{
vector<smt::Expression> smtArguments;
@@ -1931,7 +1946,21 @@ FunctionDefinition const* SMTChecker::inlinedFunctionCallToDefinition(FunctionCa
return nullptr;
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
if (funType.kind() != FunctionType::Kind::Internal)
if (funType.kind() == FunctionType::Kind::External)
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
auto identifier = memberAccess ?
dynamic_cast<Identifier const*>(&memberAccess->expression()) :
nullptr;
if (!(
identifier &&
identifier->name() == "this" &&
identifier->annotation().referencedDeclaration &&
dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
))
return nullptr;
}
else if (funType.kind() != FunctionType::Kind::Internal)
return nullptr;
FunctionDefinition const* funDef = nullptr;
libsolidity/formal/SMTChecker.h
+3
View File
@@ -115,6 +115,9 @@ private:
void inlineFunctionCall(FunctionCall const& _funCall);
/// Creates an uninterpreted function call.
void abstractFunctionCall(FunctionCall const& _funCall);
/// Inlines if the function call is internal or external to `this`.
/// Erases knowledge about state variables if external.
void internalOrExternalFunctionCall(FunctionCall const& _funCall);
void visitFunctionIdentifier(Identifier const& _identifier);
/// Encodes a modifier or function body according to the modifier