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

Simplify internal function calls

Browse Source
This commit is contained in:
Leonardo Alt 2020-09-26 12:12:39 +02:00
parent 3519b38055
commit fa7c9a0dc6
2 changed files with 26 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
libsolidity/formal/CHC.cpp
View File

@ -532,6 +532,10 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
void CHC::externalFunctionCall(FunctionCall const& _funCall) void CHC::externalFunctionCall(FunctionCall const& _funCall)
{ {
/// In external function calls we do not add a "predicate call"
/// because we do not trust their function body anyway,
/// so we just add the nondet_interface predicate.
solAssert(m_currentContract, ""); solAssert(m_currentContract, "");
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type); FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
@ -978,24 +982,35 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
smtutil::Expression CHC::predicate(FunctionCall const& _funCall) smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
{ {
/// Used only for internal calls.
auto const* function = functionCallToDefinition(_funCall); auto const* function = functionCallToDefinition(_funCall);
if (!function) if (!function)
return smtutil::Expression(true); return smtutil::Expression(true);
errorFlag().increaseIndex(); errorFlag().increaseIndex();
vector<smtutil::Expression> args{errorFlag().currentValue()}; vector<smtutil::Expression> args{errorFlag().currentValue()};
auto const* contract = function->annotation().contract;
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
bool otherContract = contract->isLibrary() ||
funType.kind() == FunctionType::Kind::External ||
funType.kind() == FunctionType::Kind::BareStaticCall;
args += otherContract ? stateVariablesAtIndex(0, *contract) : currentStateVariables(); FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
solAssert(funType.kind() == FunctionType::Kind::Internal, "");
/// Internal calls can be made to the contract itself or a library.
auto const* contract = function->annotation().contract;
auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
solAssert(contract->isLibrary() || find(hierarchy.begin(), hierarchy.end(), contract) != hierarchy.end(), "");
/// If the call is to a library, we use that library as the called contract.
/// If it is not, we use the current contract even if it is a call to a contract
/// up in the inheritance hierarchy, since the interfaces/predicates are different.
auto const* calledContract = contract->isLibrary() ? contract : m_currentContract;
solAssert(calledContract, "");
args += currentStateVariables(*calledContract);
args += symbolicArguments(_funCall); args += symbolicArguments(_funCall);
if (!otherContract) if (!calledContract->isLibrary())
for (auto const& var: m_stateVariables) for (auto const& var: m_stateVariables)
m_context.variable(*var)->increaseIndex(); m_context.variable(*var)->increaseIndex();
args += otherContract ? stateVariablesAtIndex(1, *contract) : currentStateVariables(); args += currentStateVariables(*calledContract);
for (auto var: function->parameters() + function->returnParameters()) for (auto var: function->parameters() + function->returnParameters())
{ {
@ -1006,11 +1021,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
args.push_back(currentValue(*var)); args.push_back(currentValue(*var));
} }
if (otherContract) return (*m_summaries.at(calledContract).at(function))(args);
return (*m_summaries.at(contract).at(function))(args);
solAssert(m_currentContract, "");
return (*m_summaries.at(m_currentContract).at(function))(args);
} }
void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName) void CHC::addRule(smtutil::Expression const& _rule, string const& _ruleName)

6
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -14,13 +14,11 @@ contract LoopFor2 {
c[i] = b[i]; c[i] = b[i];
++i; ++i;
} }
// Fails as false positive.
assert(b[0] == c[0]); assert(b[0] == c[0]);
assert(a[0] == 900); assert(a[0] == 900);
assert(b[0] == 900); assert(b[0] == 900);
} }
} }
// ---- // ----
// Warning 6328: (320-339): CHC: Assertion violation happens here. // Warning 6328: (290-309): CHC: Assertion violation happens here.
// Warning 6328: (343-362): CHC: Assertion violation happens here. // Warning 6328: (313-332): CHC: Assertion violation happens here.
// Warning 4661: (296-316): BMC: Assertion violation happens here.