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

Extract symbolicArguments function

Browse Source
This commit is contained in:
Leonardo Alt 2020-02-11 22:11:28 -03:00
parent 6451a4d2a0
commit 34d64761d9
3 changed files with 34 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
libsolidity/formal/BMC.cpp
View File

@ -441,26 +441,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
} }
else else
{ {
vector<smt::Expression> funArgs; initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall));
Expression const* calledExpr = &_funCall.expression();
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, "");
auto const& functionParams = funDef->parameters();
auto const& arguments = _funCall.arguments();
unsigned firstParam = 0;
if (funType->bound())
{
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
solAssert(boundFunction, "");
funArgs.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
firstParam = 1;
}
solAssert((arguments.size() + firstParam) == functionParams.size(), "");
for (unsigned i = 0; i < arguments.size(); ++i)
funArgs.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
initializeFunctionCallParameters(*funDef, funArgs);
// The reason why we need to pushCallStack here instead of visit(FunctionDefinition) // The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
// is that there we don't have `_funCall`. // is that there we don't have `_funCall`.

28
libsolidity/formal/SMTEncoder.cpp
View File

@ -1682,3 +1682,31 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
else if (returnParams.size() == 1) else if (returnParams.size() == 1)
defineExpr(_funCall, currentValue(*returnParams.front())); defineExpr(_funCall, currentValue(*returnParams.front()));
} }
vector<smt::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall)
{
auto const* function = functionCallToDefinition(_funCall);
solAssert(function, "");
vector<smt::Expression> args;
Expression const* calledExpr = &_funCall.expression();
auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
solAssert(funType, "");
auto const& functionParams = function->parameters();
auto const& arguments = _funCall.arguments();
unsigned firstParam = 0;
if (funType->bound())
{
auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
solAssert(boundFunction, "");
args.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
firstParam = 1;
}
solAssert((arguments.size() + firstParam) == functionParams.size(), "");
for (unsigned i = 0; i < arguments.size(); ++i)
args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
return args;
}

5
libsolidity/formal/SMTEncoder.h
View File

@ -230,6 +230,11 @@ protected:
/// and set them as the components of the symbolic tuple. /// and set them as the components of the symbolic tuple.
void createReturnedExpressions(FunctionCall const& _funCall); void createReturnedExpressions(FunctionCall const& _funCall);
/// @returns the symbolic arguments for a function call,
/// taking into account bound functions and
/// type conversion.
std::vector<smt::Expression> symbolicArguments(FunctionCall const& _funCall);
/// @returns a note to be added to warnings. /// @returns a note to be added to warnings.
std::string extraComment(); std::string extraComment();