Skip to content

Commit b187d06

Browse files
author
Leo
authored
Merge pull request #14534 from pgebal/pgebal/operators
Support user-defined operators in SMTChecker
2 parents ddb0d89 + da7c00e commit b187d06

13 files changed

+275
-246
lines changed

‎Changelog.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ Compiler Features:
88
* Commandline Interface: Add ``--no-import-callback`` option that prevents the compiler from loading source files not given explicitly on the CLI or in Standard JSON input.
99
* Commandline Interface: Use proper severity and coloring also for error messages produced outside of the compilation pipeline.
1010
* Parser: Remove the experimental error recovery mode (``--error-recovery`` / ``settings.parserErrorRecovery``).
11+
* SMTChecker: Support user-defined operators.
1112
* Yul Optimizer: If ``PUSH0`` is supported, favor zero literals over storing zero values in variables.
1213
* Yul Optimizer: Run the ``Rematerializer`` and ``UnusedPruner`` steps at the end of the default clean-up sequence.
1314

‎libsolidity/formal/BMC.cpp

Lines changed: 60 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -551,6 +551,17 @@ void BMC::endVisit(UnaryOperation const& _op)
551551
{
552552
SMTEncoder::endVisit(_op);
553553

554+
// User-defined operators are essentially function calls.
555+
if (auto funDef = *_op.annotation().userDefinedFunction)
556+
{
557+
std::vector<Expression const*> arguments;
558+
arguments.push_back(&_op.subExpression());
559+
// pushCallStack and defineExpr inside createReturnedExpression should be called on the expression
560+
// in case of a user-defined operator call
561+
inlineFunctionCall(funDef, _op, std::nullopt, arguments);
562+
return;
563+
}
564+
554565
if (
555566
_op.annotation().type->category() == Type::Category::RationalNumber ||
556567
_op.annotation().type->category() == Type::Category::FixedPoint
@@ -565,6 +576,22 @@ void BMC::endVisit(UnaryOperation const& _op)
565576
);
566577
}
567578

579+
void BMC::endVisit(BinaryOperation const& _op)
580+
{
581+
SMTEncoder::endVisit(_op);
582+
583+
if (auto funDef = *_op.annotation().userDefinedFunction)
584+
{
585+
std::vector<Expression const*> arguments;
586+
arguments.push_back(&_op.leftExpression());
587+
arguments.push_back(&_op.rightExpression());
588+
589+
// pushCallStack and defineExpr inside createReturnedExpression should be called on the expression
590+
// in case of a user-defined operator call
591+
inlineFunctionCall(funDef, _op, std::nullopt, arguments);
592+
}
593+
}
594+
568595
void BMC::endVisit(FunctionCall const& _funCall)
569596
{
570597
auto functionCallKind = *_funCall.annotation().kind;
@@ -674,15 +701,18 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
674701
SMTEncoder::visitAddMulMod(_funCall);
675702
}
676703

677-
void BMC::inlineFunctionCall(FunctionCall const& _funCall)
704+
void BMC::inlineFunctionCall(
705+
FunctionDefinition const* _funDef,
706+
Expression const& _callStackExpr,
707+
std::optional<Expression const*> _boundArgumentCall,
708+
std::vector<Expression const*> const& _arguments
709+
)
678710
{
679-
solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
680-
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
681-
solAssert(funDef, "");
711+
solAssert(_funDef, "");
682712

683-
if (visitedFunction(funDef))
713+
if (visitedFunction(_funDef))
684714
{
685-
auto const& returnParams = funDef->returnParameters();
715+
auto const& returnParams = _funDef->returnParameters();
686716
for (auto param: returnParams)
687717
{
688718
m_context.newValue(*param);
@@ -691,19 +721,38 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
691721
}
692722
else
693723
{
694-
initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall, m_currentContract));
724+
initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall));
695725

696726
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
697-
// is that there we don't have `_funCall`.
698-
pushCallStack({funDef, &_funCall});
727+
// is that there we don't have `_callStackExpr`.
728+
pushCallStack({_funDef, &_callStackExpr});
699729
pushPathCondition(currentPathConditions());
700730
auto oldChecked = std::exchange(m_checked, true);
701-
funDef->accept(*this);
731+
_funDef->accept(*this);
702732
m_checked = oldChecked;
703733
popPathCondition();
704734
}
705735

706-
createReturnedExpressions(_funCall, m_currentContract);
736+
createReturnedExpressions(_funDef, _callStackExpr);
737+
}
738+
739+
void BMC::inlineFunctionCall(FunctionCall const& _funCall)
740+
{
741+
solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
742+
743+
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
744+
Expression const* expr = &_funCall.expression();
745+
auto funType = dynamic_cast<FunctionType const*>(expr->annotation().type);
746+
std::optional<Expression const*> boundArgumentCall =
747+
funType->hasBoundFirstArgument() ? std::make_optional(expr) : std::nullopt;
748+
749+
std::vector<Expression const*> arguments;
750+
for (auto& arg: _funCall.sortedArguments())
751+
arguments.push_back(&(*arg));
752+
753+
// pushCallStack and defineExpr inside createReturnedExpression should be called
754+
// on the FunctionCall object for the normal function call case
755+
inlineFunctionCall(funDef, _funCall, boundArgumentCall, arguments);
707756
}
708757

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

‎libsolidity/formal/BMC.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,7 @@ class BMC: public SMTEncoder
9797
bool visit(WhileStatement const& _node) override;
9898
bool visit(ForStatement const& _node) override;
9999
void endVisit(UnaryOperation const& _node) override;
100+
void endVisit(BinaryOperation const& _node) override;
100101
void endVisit(FunctionCall const& _node) override;
101102
void endVisit(Return const& _node) override;
102103
bool visit(TryStatement const& _node) override;
@@ -113,6 +114,12 @@ class BMC: public SMTEncoder
113114
/// Visits the FunctionDefinition of the called function
114115
/// if available and inlines the return value.
115116
void inlineFunctionCall(FunctionCall const& _funCall);
117+
void inlineFunctionCall(
118+
FunctionDefinition const* _funDef,
119+
Expression const& _callStackExpr,
120+
std::optional<Expression const*> _calledExpr,
121+
std::vector<Expression const*> const& _arguments
122+
);
116123
/// Inlines if the function call is internal or external to `this`.
117124
/// Erases knowledge about state variables if external.
118125
void internalOrExternalFunctionCall(FunctionCall const& _funCall);

‎libsolidity/formal/CHC.cpp

Lines changed: 108 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -543,6 +543,35 @@ void CHC::endVisit(ForStatement const& _for)
543543
m_scopes.pop_back();
544544
}
545545

546+
void CHC::endVisit(UnaryOperation const& _op)
547+
{
548+
SMTEncoder::endVisit(_op);
549+
550+
if (auto funDef = *_op.annotation().userDefinedFunction)
551+
{
552+
std::vector<Expression const*> arguments;
553+
arguments.push_back(&_op.subExpression());
554+
internalFunctionCall(funDef, std::nullopt, _op.userDefinedFunctionType(), arguments, state().thisAddress());
555+
556+
createReturnedExpressions(funDef, _op);
557+
}
558+
}
559+
560+
void CHC::endVisit(BinaryOperation const& _op)
561+
{
562+
SMTEncoder::endVisit(_op);
563+
564+
if (auto funDef = *_op.annotation().userDefinedFunction)
565+
{
566+
std::vector<Expression const*> arguments;
567+
arguments.push_back(&_op.leftExpression());
568+
arguments.push_back(&_op.rightExpression());
569+
internalFunctionCall(funDef, std::nullopt, _op.userDefinedFunctionType(), arguments, state().thisAddress());
570+
571+
createReturnedExpressions(funDef, _op);
572+
}
573+
}
574+
546575
void CHC::endVisit(FunctionCall const& _funCall)
547576
{
548577
auto functionCallKind = *_funCall.annotation().kind;
@@ -593,8 +622,8 @@ void CHC::endVisit(FunctionCall const& _funCall)
593622
break;
594623
}
595624

596-
597-
createReturnedExpressions(_funCall, m_currentContract);
625+
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
626+
createReturnedExpressions(funDef, _funCall);
598627
}
599628

600629
void CHC::endVisit(Break const& _break)
@@ -820,20 +849,26 @@ void CHC::visitDeployment(FunctionCall const& _funCall)
820849
defineExpr(_funCall, newAddr);
821850
}
822851

823-
void CHC::internalFunctionCall(FunctionCall const& _funCall)
852+
void CHC::internalFunctionCall(
853+
FunctionDefinition const* _funDef,
854+
std::optional<Expression const*> _boundArgumentCall,
855+
FunctionType const* _funType,
856+
std::vector<Expression const*> const& _arguments,
857+
smtutil::Expression _contractAddressValue
858+
)
824859
{
825860
solAssert(m_currentContract, "");
861+
solAssert(_funType, "");
826862

827-
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
828-
if (function)
863+
if (_funDef)
829864
{
830865
if (m_currentFunction && !m_currentFunction->isConstructor())
831-
m_callGraph[m_currentFunction].insert(function);
866+
m_callGraph[m_currentFunction].insert(_funDef);
832867
else
833-
m_callGraph[m_currentContract].insert(function);
868+
m_callGraph[m_currentContract].insert(_funDef);
834869
}
835870

836-
m_context.addAssertion(predicate(_funCall));
871+
m_context.addAssertion(predicate(_funDef, _boundArgumentCall, _funType, _arguments, _contractAddressValue));
837872

838873
solAssert(m_errorDest, "");
839874
connectBlocks(
@@ -845,6 +880,42 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
845880
m_context.addAssertion(errorFlag().increaseIndex() == 0);
846881
}
847882

883+
void CHC::internalFunctionCall(FunctionCall const& _funCall)
884+
{
885+
solAssert(m_currentContract, "");
886+
887+
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
888+
if (funDef)
889+
{
890+
if (m_currentFunction && !m_currentFunction->isConstructor())
891+
m_callGraph[m_currentFunction].insert(funDef);
892+
else
893+
m_callGraph[m_currentContract].insert(funDef);
894+
}
895+
896+
Expression const* calledExpr = &_funCall.expression();
897+
auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
898+
899+
auto contractAddressValue = [this](FunctionCall const& _f) {
900+
auto [callExpr, callOptions] = functionCallExpression(_f);
901+
902+
FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
903+
if (funType.kind() == FunctionType::Kind::Internal)
904+
return state().thisAddress();
905+
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
906+
return expr(callBase->expression());
907+
solAssert(false, "Unreachable!");
908+
};
909+
910+
std::vector<Expression const*> arguments;
911+
for (auto& arg: _funCall.sortedArguments())
912+
arguments.push_back(&(*arg));
913+
914+
std::optional<Expression const*> boundArgumentCall =
915+
funType->hasBoundFirstArgument() ? std::make_optional(calledExpr) : std::nullopt;
916+
internalFunctionCall(funDef, boundArgumentCall, funType, arguments, contractAddressValue(_funCall));
917+
}
918+
848919
void CHC::addNondetCalls(ContractDefinition const& _contract)
849920
{
850921
for (auto var: _contract.stateVariables())
@@ -1028,7 +1099,10 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
10281099
state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall));
10291100
}
10301101

1031-
smtutil::Expression pred = predicate(_funCall);
1102+
std::vector<Expression const*> arguments;
1103+
for (auto& arg: _funCall.sortedArguments())
1104+
arguments.push_back(&(*arg));
1105+
smtutil::Expression pred = predicate(function, std::nullopt, &funType, arguments, calledAddress);
10321106

10331107
auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function);
10341108
m_context.addAssertion(pred && txConstraints);
@@ -1264,6 +1338,12 @@ std::set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot
12641338
return verificationTargetsIds;
12651339
}
12661340

1341+
bool CHC::usesStaticCall(FunctionDefinition const* _funDef, FunctionType const* _funType)
1342+
{
1343+
auto kind = _funType->kind();
1344+
return (_funDef && (_funDef->stateMutability() == StateMutability::Pure || _funDef->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall;
1345+
}
1346+
12671347
bool CHC::usesStaticCall(FunctionCall const& _funCall)
12681348
{
12691349
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
@@ -1733,40 +1813,34 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
17331813
solAssert(false, "");
17341814
}
17351815

1736-
smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
1816+
smtutil::Expression CHC::predicate(
1817+
FunctionDefinition const* _funDef,
1818+
std::optional<Expression const*> _boundArgumentCall,
1819+
FunctionType const* _funType,
1820+
std::vector<Expression const*> _arguments,
1821+
smtutil::Expression _contractAddressValue
1822+
)
17371823
{
1738-
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
1739-
auto kind = funType.kind();
1824+
solAssert(_funType, "");
1825+
auto kind = _funType->kind();
17401826
solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
1741-
1742-
solAssert(m_currentContract, "");
1743-
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
1744-
if (!function)
1827+
if (!_funDef)
17451828
return smtutil::Expression(true);
17461829

1747-
auto contractAddressValue = [this](FunctionCall const& _f) {
1748-
auto [callExpr, callOptions] = functionCallExpression(_f);
1749-
1750-
FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
1751-
if (funType.kind() == FunctionType::Kind::Internal)
1752-
return state().thisAddress();
1753-
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
1754-
return expr(callBase->expression());
1755-
solAssert(false, "Unreachable!");
1756-
};
17571830
errorFlag().increaseIndex();
1758-
std::vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
17591831

1760-
auto const* contract = function->annotation().contract;
1832+
std::vector<smtutil::Expression> args{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().crypto(), state().tx(), state().state()};
1833+
1834+
auto const* contract = _funDef->annotation().contract;
17611835
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
1762-
solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
1836+
solAssert(kind != FunctionType::Kind::Internal || _funDef->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
17631837

17641838
if (kind == FunctionType::Kind::Internal)
17651839
contract = m_currentContract;
17661840

17671841
args += currentStateVariables(*contract);
1768-
args += symbolicArguments(_funCall, contract);
1769-
if (!usesStaticCall(_funCall))
1842+
args += symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall);
1843+
if (!usesStaticCall(_funDef, _funType))
17701844
{
17711845
state().newState();
17721846
for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract))
@@ -1775,7 +1849,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
17751849
args += std::vector<smtutil::Expression>{state().state()};
17761850
args += currentStateVariables(*contract);
17771851

1778-
for (auto var: function->parameters() + function->returnParameters())
1852+
for (auto var: _funDef->parameters() + _funDef->returnParameters())
17791853
{
17801854
if (m_context.knownVariable(*var))
17811855
m_context.variable(*var)->increaseIndex();
@@ -1784,10 +1858,10 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
17841858
args.push_back(currentValue(*var));
17851859
}
17861860

1787-
Predicate const& summary = *m_summaries.at(contract).at(function);
1861+
Predicate const& summary = *m_summaries.at(contract).at(_funDef);
17881862
auto from = smt::function(summary, contract, m_context);
17891863
Predicate const& callPredicate = *createSummaryBlock(
1790-
*function,
1864+
*_funDef,
17911865
*contract,
17921866
kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
17931867
);

0 commit comments

Comments
 (0)