Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support user-defined operators in SMTChecker #14534

Merged
merged 4 commits into from
Oct 22, 2023
Merged

Support user-defined operators in SMTChecker #14534

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
78eb37d
Support user defined operators in SMT
pgebal Aug 8, 2023
13c2d62
apply CR changes
pgebal Oct 6, 2023
353dbdd
refactor: rename calledExpr to boundArgumentCall
pgebal Oct 19, 2023
da7c00e
fix test error
pgebal Oct 20, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ Compiler Features:
* 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.
* Commandline Interface: Use proper severity and coloring also for error messages produced outside of the compilation pipeline.
* Parser: Remove the experimental error recovery mode (``--error-recovery`` / ``settings.parserErrorRecovery``).
* SMTChecker: Support user-defined operators.
* Yul Optimizer: If ``PUSH0`` is supported, favor zero literals over storing zero values in variables.
* Yul Optimizer: Run the ``Rematerializer`` and ``UnusedPruner`` steps at the end of the default clean-up sequence.

Expand Down
71 changes: 60 additions & 11 deletions libsolidity/formal/BMC.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -551,6 +551,17 @@ void BMC::endVisit(UnaryOperation const& _op)
{
SMTEncoder::endVisit(_op);

// User-defined operators are essentially function calls.
if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<Expression const*> arguments;
arguments.push_back(&_op.subExpression());
// pushCallStack and defineExpr inside createReturnedExpression should be called on the expression
// in case of a user-defined operator call
inlineFunctionCall(funDef, _op, std::nullopt, arguments);
return;
}

if (
_op.annotation().type->category() == Type::Category::RationalNumber ||
_op.annotation().type->category() == Type::Category::FixedPoint
Expand All @@ -565,6 +576,22 @@ void BMC::endVisit(UnaryOperation const& _op)
);
}

void BMC::endVisit(BinaryOperation const& _op)
{
SMTEncoder::endVisit(_op);

if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<Expression const*> arguments;
arguments.push_back(&_op.leftExpression());
arguments.push_back(&_op.rightExpression());

// pushCallStack and defineExpr inside createReturnedExpression should be called on the expression
// in case of a user-defined operator call
inlineFunctionCall(funDef, _op, std::nullopt, arguments);
}
}

void BMC::endVisit(FunctionCall const& _funCall)
{
auto functionCallKind = *_funCall.annotation().kind;
Expand Down Expand Up @@ -674,15 +701,18 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
SMTEncoder::visitAddMulMod(_funCall);
}

void BMC::inlineFunctionCall(FunctionCall const& _funCall)
void BMC::inlineFunctionCall(
FunctionDefinition const* _funDef,
Expression const& _callStackExpr,
std::optional<Expression const*> _boundArgumentCall,
std::vector<Expression const*> const& _arguments
)
{
solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
solAssert(funDef, "");
solAssert(_funDef, "");

if (visitedFunction(funDef))
if (visitedFunction(_funDef))
{
auto const& returnParams = funDef->returnParameters();
auto const& returnParams = _funDef->returnParameters();
for (auto param: returnParams)
{
m_context.newValue(*param);
Expand All @@ -691,19 +721,38 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
}
else
{
initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall, m_currentContract));
initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall));

// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
// is that there we don't have `_funCall`.
pushCallStack({funDef, &_funCall});
// is that there we don't have `_callStackExpr`.
pushCallStack({_funDef, &_callStackExpr});
pushPathCondition(currentPathConditions());
auto oldChecked = std::exchange(m_checked, true);
funDef->accept(*this);
_funDef->accept(*this);
m_checked = oldChecked;
popPathCondition();
}

createReturnedExpressions(_funCall, m_currentContract);
createReturnedExpressions(_funDef, _callStackExpr);
}

void BMC::inlineFunctionCall(FunctionCall const& _funCall)
{
solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");

auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
Expression const* expr = &_funCall.expression();
auto funType = dynamic_cast<FunctionType const*>(expr->annotation().type);
std::optional<Expression const*> boundArgumentCall =
funType->hasBoundFirstArgument() ? std::make_optional(expr) : std::nullopt;

std::vector<Expression const*> arguments;
for (auto& arg: _funCall.sortedArguments())
arguments.push_back(&(*arg));

// pushCallStack and defineExpr inside createReturnedExpression should be called
// on the FunctionCall object for the normal function call case
inlineFunctionCall(funDef, _funCall, boundArgumentCall, arguments);
}

void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
Expand Down
7 changes: 7 additions & 0 deletions libsolidity/formal/BMC.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ class BMC: public SMTEncoder
bool visit(WhileStatement const& _node) override;
bool visit(ForStatement const& _node) override;
void endVisit(UnaryOperation const& _node) override;
void endVisit(BinaryOperation const& _node) override;
void endVisit(FunctionCall const& _node) override;
void endVisit(Return const& _node) override;
bool visit(TryStatement const& _node) override;
Expand All @@ -113,6 +114,12 @@ class BMC: public SMTEncoder
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
void inlineFunctionCall(FunctionCall const& _funCall);
void inlineFunctionCall(
FunctionDefinition const* _funDef,
Expression const& _callStackExpr,
std::optional<Expression const*> _calledExpr,
std::vector<Expression const*> const& _arguments
);
/// Inlines if the function call is internal or external to `this`.
/// Erases knowledge about state variables if external.
void internalOrExternalFunctionCall(FunctionCall const& _funCall);
Expand Down
142 changes: 108 additions & 34 deletions libsolidity/formal/CHC.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -543,6 +543,35 @@ void CHC::endVisit(ForStatement const& _for)
m_scopes.pop_back();
}

void CHC::endVisit(UnaryOperation const& _op)
{
SMTEncoder::endVisit(_op);

if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<Expression const*> arguments;
arguments.push_back(&_op.subExpression());
internalFunctionCall(funDef, std::nullopt, _op.userDefinedFunctionType(), arguments, state().thisAddress());

createReturnedExpressions(funDef, _op);
}
}

void CHC::endVisit(BinaryOperation const& _op)
{
SMTEncoder::endVisit(_op);

if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<Expression const*> arguments;
arguments.push_back(&_op.leftExpression());
arguments.push_back(&_op.rightExpression());
internalFunctionCall(funDef, std::nullopt, _op.userDefinedFunctionType(), arguments, state().thisAddress());

createReturnedExpressions(funDef, _op);
}
}

void CHC::endVisit(FunctionCall const& _funCall)
{
auto functionCallKind = *_funCall.annotation().kind;
Expand Down Expand Up @@ -593,8 +622,8 @@ void CHC::endVisit(FunctionCall const& _funCall)
break;
}


createReturnedExpressions(_funCall, m_currentContract);
auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
createReturnedExpressions(funDef, _funCall);
}

void CHC::endVisit(Break const& _break)
Expand Down Expand Up @@ -820,20 +849,26 @@ void CHC::visitDeployment(FunctionCall const& _funCall)
defineExpr(_funCall, newAddr);
}

void CHC::internalFunctionCall(FunctionCall const& _funCall)
void CHC::internalFunctionCall(
FunctionDefinition const* _funDef,
std::optional<Expression const*> _boundArgumentCall,
FunctionType const* _funType,
std::vector<Expression const*> const& _arguments,
smtutil::Expression _contractAddressValue
)
{
solAssert(m_currentContract, "");
solAssert(_funType, "");

auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
if (function)
if (_funDef)
{
if (m_currentFunction && !m_currentFunction->isConstructor())
m_callGraph[m_currentFunction].insert(function);
m_callGraph[m_currentFunction].insert(_funDef);
else
m_callGraph[m_currentContract].insert(function);
m_callGraph[m_currentContract].insert(_funDef);
}

m_context.addAssertion(predicate(_funCall));
m_context.addAssertion(predicate(_funDef, _boundArgumentCall, _funType, _arguments, _contractAddressValue));

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

void CHC::internalFunctionCall(FunctionCall const& _funCall)
{
solAssert(m_currentContract, "");

auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
if (funDef)
{
if (m_currentFunction && !m_currentFunction->isConstructor())
m_callGraph[m_currentFunction].insert(funDef);
else
m_callGraph[m_currentContract].insert(funDef);
}

Expression const* calledExpr = &_funCall.expression();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The calledExpr here has the meaning that I imagined at first during the previous review, but in BMC it means bound functions. We should clarify this

auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);

auto contractAddressValue = [this](FunctionCall const& _f) {
auto [callExpr, callOptions] = functionCallExpression(_f);

FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
if (funType.kind() == FunctionType::Kind::Internal)
return state().thisAddress();
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
return expr(callBase->expression());
solAssert(false, "Unreachable!");
};

std::vector<Expression const*> arguments;
for (auto& arg: _funCall.sortedArguments())
arguments.push_back(&(*arg));

std::optional<Expression const*> boundArgumentCall =
funType->hasBoundFirstArgument() ? std::make_optional(calledExpr) : std::nullopt;
internalFunctionCall(funDef, boundArgumentCall, funType, arguments, contractAddressValue(_funCall));
}

void CHC::addNondetCalls(ContractDefinition const& _contract)
{
for (auto var: _contract.stateVariables())
Expand Down Expand Up @@ -1028,7 +1099,10 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall));
}

smtutil::Expression pred = predicate(_funCall);
std::vector<Expression const*> arguments;
for (auto& arg: _funCall.sortedArguments())
arguments.push_back(&(*arg));
smtutil::Expression pred = predicate(function, std::nullopt, &funType, arguments, calledAddress);

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

bool CHC::usesStaticCall(FunctionDefinition const* _funDef, FunctionType const* _funType)
{
auto kind = _funType->kind();
return (_funDef && (_funDef->stateMutability() == StateMutability::Pure || _funDef->stateMutability() == StateMutability::View)) || kind == FunctionType::Kind::BareStaticCall;
}

bool CHC::usesStaticCall(FunctionCall const& _funCall)
{
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
Expand Down Expand Up @@ -1733,40 +1813,34 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
solAssert(false, "");
}

smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
smtutil::Expression CHC::predicate(
FunctionDefinition const* _funDef,
std::optional<Expression const*> _boundArgumentCall,
FunctionType const* _funType,
std::vector<Expression const*> _arguments,
smtutil::Expression _contractAddressValue
)
{
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind();
solAssert(_funType, "");
auto kind = _funType->kind();
solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");

solAssert(m_currentContract, "");
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
if (!function)
if (!_funDef)
return smtutil::Expression(true);

auto contractAddressValue = [this](FunctionCall const& _f) {
auto [callExpr, callOptions] = functionCallExpression(_f);

FunctionType const& funType = dynamic_cast<FunctionType const&>(*callExpr->annotation().type);
if (funType.kind() == FunctionType::Kind::Internal)
return state().thisAddress();
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(callExpr))
return expr(callBase->expression());
solAssert(false, "Unreachable!");
};
errorFlag().increaseIndex();
std::vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};

auto const* contract = function->annotation().contract;
std::vector<smtutil::Expression> args{errorFlag().currentValue(), _contractAddressValue, state().abi(), state().crypto(), state().tx(), state().state()};

auto const* contract = _funDef->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
solAssert(kind != FunctionType::Kind::Internal || function->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");
solAssert(kind != FunctionType::Kind::Internal || _funDef->isFree() || (contract && contract->isLibrary()) || util::contains(hierarchy, contract), "");

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

args += currentStateVariables(*contract);
args += symbolicArguments(_funCall, contract);
if (!usesStaticCall(_funCall))
args += symbolicArguments(_funDef->parameters(), _arguments, _boundArgumentCall);
if (!usesStaticCall(_funDef, _funType))
{
state().newState();
for (auto const& var: stateVariablesIncludingInheritedAndPrivate(*contract))
Expand All @@ -1775,7 +1849,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
args += std::vector<smtutil::Expression>{state().state()};
args += currentStateVariables(*contract);

for (auto var: function->parameters() + function->returnParameters())
for (auto var: _funDef->parameters() + _funDef->returnParameters())
{
if (m_context.knownVariable(*var))
m_context.variable(*var)->increaseIndex();
Expand All @@ -1784,10 +1858,10 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
args.push_back(currentValue(*var));
}

Predicate const& summary = *m_summaries.at(contract).at(function);
Predicate const& summary = *m_summaries.at(contract).at(_funDef);
auto from = smt::function(summary, contract, m_context);
Predicate const& callPredicate = *createSummaryBlock(
*function,
*_funDef,
*contract,
kind == FunctionType::Kind::Internal ? PredicateType::InternalCall : PredicateType::ExternalCallTrusted
);
Expand Down
Loading