Skip to content

Commit

Permalink
apply CR changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@pgebal
pgebal committed Oct 13, 2023
1 parent de49459 commit 00bf98e
Show file tree
Hide file tree
Showing 7 changed files with 62 additions and 54 deletions.
3 changes: 0 additions & 3 deletions libsolidity/ast/AST.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2111,7 +2111,6 @@ class UnaryOperation: public Expression
Token getOperator() const { return m_operator; }
bool isPrefixOperation() const { return m_isPrefix; }
Expression const& subExpression() const { return *m_subExpression; }
ASTPointer<Expression> const& argument() const { return m_subExpression; }

FunctionType const* userDefinedFunctionType() const;

Expand Down Expand Up @@ -2146,8 +2145,6 @@ class BinaryOperation: public Expression

Expression const& leftExpression() const { return *m_left; }
Expression const& rightExpression() const { return *m_right; }
ASTPointer<Expression> leftArgument() const { return m_left; }
ASTPointer<Expression> rightArgument() const { return m_right; }
Token getOperator() const { return m_operator; }

FunctionType const* userDefinedFunctionType() const;
Expand Down
45 changes: 27 additions & 18 deletions libsolidity/formal/BMC.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -554,9 +554,11 @@ void BMC::endVisit(UnaryOperation const& _op)
// User-defined operators are essentially function calls.
if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<ASTPointer<Expression const>> arguments;
arguments.push_back(_op.argument());
inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments);
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;
}

Expand All @@ -580,10 +582,13 @@ void BMC::endVisit(BinaryOperation const& _op)

if (auto funDef = *_op.annotation().userDefinedFunction)
{
std::vector<ASTPointer<Expression const>> arguments;
arguments.push_back(_op.leftArgument());
arguments.push_back(_op.rightArgument());
inlineFunctionCall(funDef, _op, &_op, _op.userDefinedFunctionType(), arguments);
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);
}
}

Expand Down Expand Up @@ -699,14 +704,11 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
void BMC::inlineFunctionCall(
FunctionDefinition const* _funDef,
Expression const& _callStackExpr,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments
std::optional<Expression const*> _calledExpr,
std::vector<Expression const*> const& _arguments
)
{
solAssert(_funDef, "");
solAssert(_funType, "");
solAssert(_calledExpr, "");

if (visitedFunction(_funDef))
{
Expand All @@ -719,7 +721,7 @@ void BMC::inlineFunctionCall(
}
else
{
initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef, _calledExpr, _funType, _arguments));
initializeFunctionCallParameters(*_funDef, symbolicArguments(_funDef->parameters(), _calledExpr, _arguments));

// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
// is that there we don't have `_callStackExpr`.
Expand All @@ -739,11 +741,18 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");

auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
Expression const* calledExpr = &_funCall.expression();
auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();

inlineFunctionCall(funDef, _funCall, calledExpr, funType, arguments);
Expression const* expr = &_funCall.expression();
auto funType = dynamic_cast<FunctionType const*>(expr->annotation().type);
std::optional<Expression const*> calledExpr =
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, calledExpr, arguments);
}

void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
Expand Down
5 changes: 2 additions & 3 deletions libsolidity/formal/BMC.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,9 +117,8 @@ class BMC: public SMTEncoder
void inlineFunctionCall(
FunctionDefinition const* _funDef,
Expression const& _callStackExpr,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments
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.
Expand Down
28 changes: 18 additions & 10 deletions libsolidity/formal/CHC.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -549,8 +549,8 @@ void CHC::endVisit(UnaryOperation const& _op)

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

createReturnedExpressions(funDef, _op);
Expand All @@ -563,9 +563,9 @@ void CHC::endVisit(BinaryOperation const& _op)

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

createReturnedExpressions(funDef, _op);
Expand Down Expand Up @@ -853,7 +853,7 @@ void CHC::internalFunctionCall(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments,
std::vector<Expression const*> const& _arguments,
smtutil::Expression _contractAddressValue
)
{
Expand Down Expand Up @@ -896,7 +896,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)

Expression const* calledExpr = &_funCall.expression();
auto funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
std::vector<ASTPointer<Expression const>> arguments = _funCall.sortedArguments();

auto contractAddressValue = [this](FunctionCall const& _f) {
auto [callExpr, callOptions] = functionCallExpression(_f);
Expand All @@ -909,6 +908,9 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
solAssert(false, "Unreachable!");
};

std::vector<Expression const*> arguments;
for (auto& arg: _funCall.sortedArguments())
arguments.push_back(&(*arg));
internalFunctionCall(funDef, calledExpr, funType, arguments, contractAddressValue(_funCall));
}

Expand Down Expand Up @@ -1095,7 +1097,10 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
state().readStateVars(*function->annotation().contract, contractAddressValue(_funCall));
}

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

auto txConstraints = state().txTypeConstraints() && state().txFunctionConstraints(*function);
m_context.addAssertion(pred && txConstraints);
Expand Down Expand Up @@ -1810,7 +1815,7 @@ smtutil::Expression CHC::predicate(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> _arguments,
std::vector<Expression const*> _arguments,
smtutil::Expression _contractAddressValue
)
{
Expand All @@ -1833,7 +1838,10 @@ smtutil::Expression CHC::predicate(
contract = m_currentContract;

args += currentStateVariables(*contract);
args += symbolicArguments(_funDef, _calledExpr, _funType, _arguments);

std::optional<Expression const*> calledExpr =
_funType->hasBoundFirstArgument() ? std::make_optional(_calledExpr) : std::nullopt;
args += symbolicArguments(_funDef->parameters(), calledExpr, _arguments);
if (!usesStaticCall(_funDef, _funType))
{
state().newState();
Expand Down
4 changes: 2 additions & 2 deletions libsolidity/formal/CHC.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ class CHC: public SMTEncoder
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments,
std::vector<Expression const*> const& _arguments,
smtutil::Expression _contractAddressValue
);
void externalFunctionCall(FunctionCall const& _funCall);
Expand Down Expand Up @@ -260,7 +260,7 @@ class CHC: public SMTEncoder
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> _arguments,
std::vector<Expression const*> _arguments,
smtutil::Expression _contractAddressValue
);
/// @returns a predicate that defines a contract initializer for _contract in the context of _contractContext.
Expand Down
24 changes: 10 additions & 14 deletions libsolidity/formal/SMTEncoder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3137,29 +3137,25 @@ void SMTEncoder::createReturnedExpressions(FunctionDefinition const* _funDef, Ex
}

std::vector<smtutil::Expression> SMTEncoder::symbolicArguments(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments)
std::vector<ASTPointer<VariableDeclaration>> const& _funParameters,
std::optional<Expression const*> _calledExpr,
std::vector<Expression const*> const& _arguments)
{
solAssert(_funDef, "");
solAssert(_funType, "");

std::vector<smtutil::Expression> args;
auto functionParams = _funDef->parameters();
unsigned firstParam = 0;
if (_funType->hasBoundFirstArgument())
if (_calledExpr)
{
_calledExpr = innermostTuple(*_calledExpr);
auto const& attachedFunction = dynamic_cast<MemberAccess const*>(_calledExpr);
Expression const* calledExpr = innermostTuple(*_calledExpr.value());
auto const& attachedFunction = dynamic_cast<MemberAccess const*>(calledExpr);
solAssert(attachedFunction, "");
args.push_back(expr(attachedFunction->expression(), functionParams.front()->type()));
args.push_back(expr(attachedFunction->expression(), _funParameters.front()->type()));
firstParam = 1;
}

solAssert((_arguments.size() + firstParam) == functionParams.size(), "");
solAssert((_arguments.size() + firstParam) == _funParameters.size(), "");

for (unsigned i = 0; i < _arguments.size(); ++i)
args.push_back(expr(*_arguments.at(i), functionParams.at(i + firstParam)->type()));
args.push_back(expr(*_arguments.at(i), _funParameters.at(i + firstParam)->type()));

return args;
}
Expand Down
7 changes: 3 additions & 4 deletions libsolidity/formal/SMTEncoder.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -409,10 +409,9 @@ class SMTEncoder: public ASTConstVisitor
/// taking into account attached functions and
/// type conversion.
std::vector<smtutil::Expression> symbolicArguments(
FunctionDefinition const* _funDef,
Expression const* _calledExpr,
FunctionType const* _funType,
std::vector<ASTPointer<Expression const>> const& _arguments
std::vector<ASTPointer<VariableDeclaration>> const& _funParameters,
std::optional<Expression const*> _calledExpr,
std::vector<Expression const*> const& _arguments
);

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

0 comments on commit 00bf98e

Please sign in to comment.