Skip to content

Commit 353dbdd

Browse files
pgebalpgebal
committed
refactor: rename calledExpr to boundArgumentCall
1 parent 13c2d62 commit 353dbdd

File tree

5 files changed

+23
-24
lines changed

5 files changed

+23
-24
lines changed

‎libsolidity/formal/BMC.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -704,7 +704,7 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
704704
void BMC::inlineFunctionCall(
705705
FunctionDefinition const* _funDef,
706706
Expression const& _callStackExpr,
707-
std::optional<Expression const*> _calledExpr,
707+
std::optional<Expression const*> _boundArgumentCall,
708708
std::vector<Expression const*> const& _arguments
709709
)
710710
{
@@ -721,7 +721,7 @@ void BMC::inlineFunctionCall(
721721
}
722722
else
723723
{
724-
initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _calledExpr, _arguments));
724+
initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall));
725725

726726
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
727727
// is that there we don't have `_callStackExpr`.
@@ -743,7 +743,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
743743
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
744744
Expression const* expr = &_funCall.expression();
745745
auto funType = dynamic_cast<FunctionType const*>(expr->annotation().type);
746-
std::optional<Expression const*> calledExpr =
746+
std::optional<Expression const*> boundArgumentCall =
747747
funType->hasBoundFirstArgument() ? std::make_optional(expr) : std::nullopt;
748748

749749
std::vector<Expression const*> arguments;
@@ -752,7 +752,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
752752

753753
// pushCallStack and defineExpr inside createReturnedExpression should be called
754754
// on the FunctionCall object for the normal function call case
755-
inlineFunctionCall(funDef, _funCall, calledExpr, arguments);
755+
inlineFunctionCall(funDef, _funCall, boundArgumentCall, arguments);
756756
}
757757

758758
void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)

‎libsolidity/formal/CHC.cpp

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -551,7 +551,7 @@ void CHC::endVisit(UnaryOperation const& _op)
551551
{
552552
std::vector<Expression const*> arguments;
553553
arguments.push_back(&_op.subExpression());
554-
internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress());
554+
internalFunctionCall(funDef, std::nullopt, _op.userDefinedFunctionType(), arguments, state().thisAddress());
555555

556556
createReturnedExpressions(funDef, _op);
557557
}
@@ -566,7 +566,7 @@ void CHC::endVisit(BinaryOperation const& _op)
566566
std::vector<Expression const*> arguments;
567567
arguments.push_back(&_op.leftExpression());
568568
arguments.push_back(&_op.rightExpression());
569-
internalFunctionCall(funDef, &_op, _op.userDefinedFunctionType(), arguments, state().thisAddress());
569+
internalFunctionCall(funDef, std::nullopt, _op.userDefinedFunctionType(), arguments, state().thisAddress());
570570

571571
createReturnedExpressions(funDef, _op);
572572
}
@@ -851,14 +851,13 @@ void CHC::visitDeployment(FunctionCall const& _funCall)
851851

852852
void CHC::internalFunctionCall(
853853
FunctionDefinition const* _funDef,
854-
Expression const* _calledExpr,
854+
std::optional<Expression const*> _boundArgumentCall,
855855
FunctionType const* _funType,
856856
std::vector<Expression const*> const& _arguments,
857857
smtutil::Expression _contractAddressValue
858858
)
859859
{
860860
solAssert(m_currentContract, "");
861-
solAssert(_calledExpr, "");
862861
solAssert(_funType, "");
863862

864863
if (_funDef)
@@ -869,7 +868,7 @@ void CHC::internalFunctionCall(
869868
m_callGraph[m_currentContract].insert(_funDef);
870869
}
871870

872-
m_context.addAssertion(predicate(_funDef, _calledExpr, _funType, _arguments, _contractAddressValue));
871+
m_context.addAssertion(predicate(_funDef, _boundArgumentCall, _funType, _arguments, _contractAddressValue));
873872

874873
solAssert(m_errorDest, "");
875874
connectBlocks(
@@ -911,7 +910,10 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
911910
std::vector<Expression const*> arguments;
912911
for (auto& arg: _funCall.sortedArguments())
913912
arguments.push_back(&(*arg));
914-
internalFunctionCall(funDef, calledExpr, funType, arguments, contractAddressValue(_funCall));
913+
914+
std::optional<Expression const*> boundArgumentCall =
915+
funType->hasBoundFirstArgument() ? std::make_optional(calledExpr) : std::nullopt;
916+
internalFunctionCall(funDef, boundArgumentCall, funType, arguments, contractAddressValue(_funCall));
915917
}
916918

917919
void CHC::addNondetCalls(ContractDefinition const& _contract)
@@ -1813,13 +1815,12 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
18131815

18141816
smtutil::Expression CHC::predicate(
18151817
FunctionDefinition const* _funDef,
1816-
Expression const* _calledExpr,
1818+
std::optional<Expression const*> _boundArgumentCall,
18171819
FunctionType const* _funType,
18181820
std::vector<Expression const*> _arguments,
18191821
smtutil::Expression _contractAddressValue
18201822
)
18211823
{
1822-
solAssert(_calledExpr, "");
18231824
solAssert(_funType, "");
18241825
auto kind = _funType->kind();
18251826
solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
@@ -1838,10 +1839,7 @@ smtutil::Expression CHC::predicate(
18381839
contract = m_currentContract;
18391840

18401841
args += currentStateVariables(*contract);
1841-
1842-
std::optional<Expression const*> calledExpr =
1843-
_funType->hasBoundFirstArgument() ? std::make_optional(_calledExpr) : std::nullopt;
1844-
args += symbolicArguments(_funDef->parameters(), calledExpr, _arguments);
1842+
args += symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall);
18451843
if (!usesStaticCall(_funDef, _funType))
18461844
{
18471845
state().newState();

‎libsolidity/formal/CHC.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ class CHC: public SMTEncoder
131131
void internalFunctionCall(FunctionCall const& _funCall);
132132
void internalFunctionCall(
133133
FunctionDefinition const* _funDef,
134-
Expression const* _calledExpr,
134+
std::optional<Expression const*> _boundArgumentCall,
135135
FunctionType const* _funType,
136136
std::vector<Expression const*> const& _arguments,
137137
smtutil::Expression _contractAddressValue
@@ -258,7 +258,7 @@ class CHC: public SMTEncoder
258258
/// @returns the summary predicate for the called function.
259259
smtutil::Expression predicate(
260260
FunctionDefinition const* _funDef,
261-
Expression const* _calledExpr,
261+
std::optional<Expression const*> _boundArgumentCall,
262262
FunctionType const* _funType,
263263
std::vector<Expression const*> _arguments,
264264
smtutil::Expression _contractAddressValue

‎libsolidity/formal/SMTEncoder.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3138,14 +3138,15 @@ void SMTEncoder::createReturnedExpressions(FunctionDefinition const* _funDef, Ex
31383138

31393139
std::vector<smtutil::Expression> SMTEncoder::symbolicArguments(
31403140
std::vector<ASTPointer<VariableDeclaration>> const& _funParameters,
3141-
std::optional<Expression const*> _calledExpr,
3142-
std::vector<Expression const*> const& _arguments)
3141+
std::vector<Expression const*> const& _arguments,
3142+
std::optional<Expression const*> _boundArgumentCall
3143+
)
31433144
{
31443145
std::vector<smtutil::Expression> args;
31453146
unsigned firstParam = 0;
3146-
if (_calledExpr)
3147+
if (_boundArgumentCall)
31473148
{
3148-
Expression const* calledExpr = innermostTuple(*_calledExpr.value());
3149+
Expression const* calledExpr = innermostTuple(*_boundArgumentCall.value());
31493150
auto const& attachedFunction = dynamic_cast<MemberAccess const*>(calledExpr);
31503151
solAssert(attachedFunction, "");
31513152
args.push_back(expr(attachedFunction->expression(), _funParameters.front()->type()));

‎libsolidity/formal/SMTEncoder.h

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -410,8 +410,8 @@ class SMTEncoder: public ASTConstVisitor
410410
/// type conversion.
411411
std::vector<smtutil::Expression> symbolicArguments(
412412
std::vector<ASTPointer<VariableDeclaration>> const& _funParameters,
413-
std::optional<Expression const*> _calledExpr,
414-
std::vector<Expression const*> const& _arguments
413+
std::vector<Expression const*> const& _arguments,
414+
std::optional<Expression const*> _calledExpr
415415
);
416416

417417
smtutil::Expression constantExpr(Expression const& _expr, VariableDeclaration const& _var);

0 commit comments

Comments
 (0)