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

Merge remote-tracking branch 'origin/develop' into breaking

Browse Source
This commit is contained in:
chriseth
2020-11-17 18:51:57 +01:00
parent 6e3f817aac e1292380bd
commit e8a278eefa
141 changed files with 2354 additions and 1203 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+22 -36
View File
@@ -96,20 +96,7 @@ bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall)
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
if (funType.kind() == FunctionType::Kind::External)
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
if (!memberAccess)
return false;
auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
if (!(
identifier &&
identifier->name() == "this" &&
identifier->annotation().referencedDeclaration &&
dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
))
return false;
}
return isTrustedExternalCall(&_funCall.expression());
else if (funType.kind() != FunctionType::Kind::Internal)
return false;
@@ -133,7 +120,10 @@ void BMC::endVisit(ContractDefinition const& _contract)
constructor->accept(*this);
else
{
/// Visiting implicit constructor - we need a dummy callstack frame
pushCallStack({nullptr, nullptr});
inlineConstructorHierarchy(_contract);
popCallStack();
/// Check targets created by state variable initialization.
smtutil::Expression constraints = m_context.assertions();
checkVerificationTargets(constraints);
@@ -844,32 +834,28 @@ void BMC::checkCondition(
{
case smtutil::CheckResult::SATISFIABLE:
{
solAssert(!_callStack.empty(), "");
std::ostringstream message;
message << "BMC: " << _description << " happens here.";
if (_callStack.size())
{
std::ostringstream modelMessage;
modelMessage << "Counterexample:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);
std::ostringstream modelMessage;
modelMessage << "Counterexample:\n";
solAssert(values.size() == expressionNames.size(), "");
map<string, string> sortedModel;
for (size_t i = 0; i < values.size(); ++i)
if (expressionsToEvaluate.at(i).name != values.at(i))
sortedModel[expressionNames.at(i)] = values.at(i);
for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
for (auto const& eval: sortedModel)
modelMessage << " " << eval.first << " = " << eval.second << "\n";
m_errorReporter.warning(
_errorHappens,
_location,
message.str(),
SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
.append(SMTEncoder::callStackMessage(_callStack))
.append(move(secondaryLocation))
);
}
else
m_errorReporter.warning(6084_error, _location, message.str(), secondaryLocation);
m_errorReporter.warning(
_errorHappens,
_location,
message.str(),
SecondarySourceLocation().append(modelMessage.str(), SourceLocation{})
.append(SMTEncoder::callStackMessage(_callStack))
.append(move(secondaryLocation))
);
break;
}
case smtutil::CheckResult::UNSATISFIABLE:
libsolidity/formal/CHC.cpp
+58 -14
View File
@@ -562,8 +562,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
m_context.addAssertion(interface(*contract));
}
auto previousError = errorFlag().currentValue();
m_context.addAssertion(predicate(_funCall));
connectBlocks(
@@ -572,8 +570,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
(errorFlag().currentValue() > 0)
);
m_context.addAssertion(errorFlag().currentValue() == 0);
errorFlag().increaseIndex();
m_context.addAssertion(errorFlag().currentValue() == previousError);
}
void CHC::externalFunctionCall(FunctionCall const& _funCall)
@@ -583,6 +579,11 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
/// so we just add the nondet_interface predicate.
solAssert(m_currentContract, "");
if (isTrustedExternalCall(&_funCall.expression()))
{
externalFunctionCallToTrustedCode(_funCall);
return;
}
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind();
@@ -615,6 +616,42 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
m_context.addAssertion(errorFlag().currentValue() == 0);
}
void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
{
solAssert(m_currentContract, "");
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind();
solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
auto const* function = functionCallToDefinition(_funCall);
if (!function)
return;
// External call creates a new transaction.
auto originalTx = state().tx();
auto txOrigin = state().txMember("tx.origin");
state().newTx();
// set the transaction sender as this contract
m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
// set the origin to be the current transaction origin
m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
smtutil::Expression pred = predicate(_funCall);
auto txConstraints = m_context.state().txConstraints(*function);
m_context.addAssertion(pred && txConstraints);
// restore the original transaction data
state().newTx();
m_context.addAssertion(originalTx == state().tx());
connectBlocks(
m_currentBlock,
(m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract),
(errorFlag().currentValue() > 0)
);
m_context.addAssertion(errorFlag().currentValue() == 0);
}
void CHC::unknownFunctionCall(FunctionCall const&)
{
/// Function calls are not handled at the moment,
@@ -1011,27 +1048,34 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
{
/// Used only for internal calls.
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind();
solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
auto const* function = functionCallToDefinition(_funCall);
if (!function)
return smtutil::Expression(true);
auto contractAddressValue = [this](FunctionCall const& _f) {
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_f.expression().annotation().type);
if (funType.kind() == FunctionType::Kind::Internal)
return state().thisAddress();
if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(&_f.expression()))
return expr(callBase->expression());
solAssert(false, "Unreachable!");
};
errorFlag().increaseIndex();
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state()};
vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().crypto(), state().tx(), state().state()};
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(), "");
solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), "");
/// 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;
/// If the call is to a contract not in the inheritance hierarchy, we also use that as the called contract.
/// Otherwise, the call is to some contract in the inheritance hierarchy of the current contract.
/// In this case we use current contract as the called one since the interfaces/predicates are different.
auto const* calledContract = contains(hierarchy, contract) ? m_currentContract : contract;
solAssert(calledContract, "");
bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
libsolidity/formal/CHC.h
+1
View File
@@ -88,6 +88,7 @@ private:
void visitAddMulMod(FunctionCall const& _funCall) override;
void internalFunctionCall(FunctionCall const& _funCall);
void externalFunctionCall(FunctionCall const& _funCall);
void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
void unknownFunctionCall(FunctionCall const& _funCall);
void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
/// Creates underflow/overflow verification targets.
libsolidity/formal/SMTEncoder.cpp
+13
View File
@@ -2386,6 +2386,19 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
return nullptr;
}
bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
if (!memberAccess)
return false;
auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
return identifier &&
identifier->name() == "this" &&
identifier->annotation().referencedDeclaration &&
dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
;
}
string SMTEncoder::extraComment()
{
string extra;
libsolidity/formal/SMTEncoder.h
+4
View File
@@ -295,6 +295,10 @@ protected:
/// otherwise nullptr.
MemberAccess const* isEmptyPush(Expression const& _expr) const;
/// @returns true if the given identifier is a contract which is known and trusted.
/// This means we don't have to abstract away effects of external function calls to this contract.
static bool isTrustedExternalCall(Expression const* _expr);
/// Creates symbolic expressions for the returned values
/// and set them as the components of the symbolic tuple.
void createReturnedExpressions(FunctionCall const& _funCall);