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 pull request #10489 from ethereum/develop

Browse Source 
Merge develop into breaking.
This commit is contained in:
chriseth
2020-12-03 18:11:12 +01:00
committed by GitHub
parent 9bb83ef82d e04cc80438
commit d56a7bb89e
68 changed files with 943 additions and 238 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+5
View File
@@ -506,6 +506,11 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
if (shouldInlineFunctionCall(_funCall))
inlineFunctionCall(_funCall);
else if (isPublicGetter(_funCall.expression()))
{
// Do nothing here.
// The processing happens in SMT Encoder, but we need to prevent the resetting of the state variables.
}
else if (funType.kind() == FunctionType::Kind::Internal)
m_errorReporter.warning(
5729_error,
libsolidity/formal/SMTEncoder.cpp
+149 -90
View File
@@ -318,18 +318,12 @@ void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
assignment(*declarations.at(i), symbTuple->component(i, components.at(i), declarations.at(i)->type()));
}
}
else if (m_context.knownVariable(*_varDecl.declarations().front()))
else
{
solAssert(m_context.knownVariable(*_varDecl.declarations().front()), "");
if (_varDecl.initialValue())
assignment(*_varDecl.declarations().front(), *_varDecl.initialValue());
}
else
m_errorReporter.warning(
7186_error,
_varDecl.location(),
"Assertion checker does not yet implement such variable declarations."
);
}
bool SMTEncoder::visit(Assignment const& _assignment)
@@ -492,11 +486,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
indexOrMemberAssignment(*subExpr, newValue);
}
else
m_errorReporter.warning(
1950_error,
_op.location(),
"Assertion checker does not yet implement such increments / decrements."
);
solAssert(false, "");
break;
}
@@ -530,11 +520,7 @@ void SMTEncoder::endVisit(UnaryOperation const& _op)
break;
}
default:
m_errorReporter.warning(
3682_error,
_op.location(),
"Assertion checker does not yet implement this operator."
);
solAssert(false, "");
}
}
@@ -571,11 +557,7 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
else if (TokenTraits::isBitOp(_op.getOperator()) || TokenTraits::isShiftOp(_op.getOperator()))
bitwiseOperation(_op);
else
m_errorReporter.warning(
3876_error,
_op.location(),
"Assertion checker does not yet implement this operator."
);
solAssert(false, "");
}
bool SMTEncoder::visit(Conditional const& _op)
@@ -634,8 +616,11 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::GasLeft:
visitGasLeft(_funCall);
break;
case FunctionType::Kind::Internal:
case FunctionType::Kind::External:
if (isPublicGetter(_funCall.expression()))
visitPublicGetter(_funCall);
break;
case FunctionType::Kind::Internal:
case FunctionType::Kind::DelegateCall:
case FunctionType::Kind::BareCall:
case FunctionType::Kind::BareCallCode:
@@ -862,6 +847,98 @@ void SMTEncoder::endVisit(ElementaryTypeNameExpression const& _typeName)
m_context.createExpression(_typeName, result.second);
}
namespace // helpers for SMTEncoder::visitPublicGetter
{
bool isReturnedFromStructGetter(TypePointer _type)
{
// So far it seems that only Mappings and ordinary Arrays are not returned.
auto category = _type->category();
if (category == Type::Category::Mapping)
return false;
if (category == Type::Category::Array)
return dynamic_cast<ArrayType const&>(*_type).isByteArray();
// default
return true;
}
vector<string> structGetterReturnedMembers(StructType const& _structType)
{
vector<string> returnedMembers;
for (auto const& member: _structType.nativeMembers(nullptr))
if (isReturnedFromStructGetter(member.type))
returnedMembers.push_back(member.name);
return returnedMembers;
}
}
void SMTEncoder::visitPublicGetter(FunctionCall const& _funCall)
{
MemberAccess const& access = dynamic_cast<MemberAccess const&>(_funCall.expression());
auto var = dynamic_cast<VariableDeclaration const*>(access.annotation().referencedDeclaration);
solAssert(var, "");
solAssert(m_context.knownExpression(_funCall), "");
auto paramExpectedTypes = FunctionType(*var).parameterTypes();
auto actualArguments = _funCall.arguments();
solAssert(actualArguments.size() == paramExpectedTypes.size(), "");
vector<smtutil::Expression> symbArguments;
for (unsigned i = 0; i < paramExpectedTypes.size(); ++i)
symbArguments.push_back(expr(*actualArguments[i], paramExpectedTypes[i]));
TypePointer type = var->type();
if (
type->isValueType() ||
(type->category() == Type::Category::Array && dynamic_cast<ArrayType const&>(*type).isByteArray())
)
{
solAssert(symbArguments.empty(), "");
defineExpr(_funCall, currentValue(*var));
return;
}
switch (type->category())
{
case Type::Category::Array:
case Type::Category::Mapping:
{
// For nested arrays/mappings, each argument in the call is an index to the next layer.
// We mirror this with `select` after unpacking the SMT-LIB array expression.
smtutil::Expression exprVal = currentValue(*var);
for (auto const& arg: symbArguments)
{
exprVal = smtutil::Expression::select(
smtutil::Expression::tuple_get(exprVal, 0),
arg
);
}
defineExpr(_funCall, exprVal);
break;
}
case Type::Category::Struct:
{
auto returnedMembers = structGetterReturnedMembers(dynamic_cast<StructType const&>(*type));
solAssert(!returnedMembers.empty(), "");
auto structVar = dynamic_pointer_cast<smt::SymbolicStructVariable>(m_context.variable(*var));
solAssert(structVar, "");
auto returnedValues = applyMap(returnedMembers, [&](string const& memberName) { return structVar->member(memberName); });
if (returnedValues.size() == 1)
defineExpr(_funCall, returnedValues.front());
else
{
auto symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_funCall));
solAssert(symbTuple, "");
symbTuple->increaseIndex(); // Increasing the index explicitly since we cannot use defineExpr in this case.
auto const& symbComponents = symbTuple->components();
solAssert(symbComponents.size() == returnedValues.size(), "");
for (unsigned i = 0; i < symbComponents.size(); ++i)
m_context.addAssertion(symbTuple->component(i) == returnedValues.at(i));
}
break;
}
default: {} // Unsupported cases, do nothing and the getter will be abstracted.
}
}
void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
{
solAssert(*_funCall.annotation().kind == FunctionCallKind::TypeConversion, "");
@@ -1025,15 +1102,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
);
}
else
{
m_errorReporter.warning(
7885_error,
_literal.location(),
"Assertion checker does not yet support the type of this literal (" +
_literal.annotation().type->toString() +
")."
);
}
solAssert(false, "");
}
void SMTEncoder::addArrayLiteralAssertions(
@@ -1111,11 +1180,8 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
);
}
else
m_errorReporter.warning(
9551_error,
_memberAccess.location(),
"Assertion checker does not yet support this expression."
);
solUnimplementedAssert(false, "");
return false;
}
else if (smt::isNonRecursiveStruct(*exprType))
@@ -1505,40 +1571,32 @@ void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
{
auto type = _op.annotation().commonType;
solAssert(type, "");
if (type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint)
solAssert(type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint, "");
switch (_op.getOperator())
{
switch (_op.getOperator())
{
case Token::Add:
case Token::Sub:
case Token::Mul:
case Token::Div:
case Token::Mod:
{
auto values = arithmeticOperation(
_op.getOperator(),
expr(_op.leftExpression()),
expr(_op.rightExpression()),
_op.annotation().commonType,
_op
);
defineExpr(_op, values.first);
break;
}
default:
m_errorReporter.warning(
5188_error,
_op.location(),
"Assertion checker does not yet implement this operator."
);
}
}
else
m_errorReporter.warning(
9011_error,
_op.location(),
"Assertion checker does not yet implement this operator for type " + type->richIdentifier() + "."
case Token::Add:
case Token::Sub:
case Token::Mul:
case Token::Div:
case Token::Mod:
{
auto values = arithmeticOperation(
_op.getOperator(),
expr(_op.leftExpression()),
expr(_op.rightExpression()),
_op.annotation().commonType,
_op
);
defineExpr(_op, values.first);
break;
}
default:
m_errorReporter.warning(
5188_error,
_op.location(),
"Assertion checker does not yet implement this operator."
);
}
}
pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
@@ -1727,29 +1785,21 @@ void SMTEncoder::booleanOperation(BinaryOperation const& _op)
{
solAssert(_op.getOperator() == Token::And || _op.getOperator() == Token::Or, "");
solAssert(_op.annotation().commonType, "");
if (_op.annotation().commonType->category() == Type::Category::Bool)
solAssert(_op.annotation().commonType->category() == Type::Category::Bool, "");
// @TODO check that both of them are not constant
_op.leftExpression().accept(*this);
if (_op.getOperator() == Token::And)
{
// @TODO check that both of them are not constant
_op.leftExpression().accept(*this);
if (_op.getOperator() == Token::And)
{
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
}
else
{
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
}
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), expr(_op.leftExpression())).first;
mergeVariables(touchedVariables(_op.rightExpression()), !expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
defineExpr(_op, expr(_op.leftExpression()) && expr(_op.rightExpression()));
}
else
m_errorReporter.warning(
3263_error,
_op.location(),
"Assertion checker does not yet implement the type " + _op.annotation().commonType->toString() + " for boolean operations"
);
{
auto indicesAfterSecond = visitBranch(&_op.rightExpression(), !expr(_op.leftExpression())).first;
mergeVariables(touchedVariables(_op.rightExpression()), expr(_op.leftExpression()), copyVariableIndices(), indicesAfterSecond);
defineExpr(_op, expr(_op.leftExpression()) || expr(_op.rightExpression()));
}
}
void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
@@ -2398,6 +2448,15 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
return nullptr;
}
bool SMTEncoder::isPublicGetter(Expression const& _expr) {
if (!isTrustedExternalCall(&_expr))
return false;
auto varDecl = dynamic_cast<VariableDeclaration const*>(
dynamic_cast<MemberAccess const&>(_expr).annotation().referencedDeclaration
);
return varDecl != nullptr;
}
bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
if (!memberAccess)
libsolidity/formal/SMTEncoder.h
+3
View File
@@ -153,6 +153,9 @@ protected:
void visitTypeConversion(FunctionCall const& _funCall);
void visitStructConstructorCall(FunctionCall const& _funCall);
void visitFunctionIdentifier(Identifier const& _identifier);
void visitPublicGetter(FunctionCall const& _funCall);
bool isPublicGetter(Expression const& _expr);
/// Encodes a modifier or function body according to the modifier
/// visit depth.
libsolidity/interface/OptimiserSettings.h
+2 -2
View File
@@ -32,7 +32,7 @@ namespace solidity::frontend
struct OptimiserSettings
{
static char constexpr DefaultYulOptimiserSteps[] =
"NdhfoDgvulfnTUtnIf" // None of these can make stack problems worse
"dhfoDgvulfnTUtnIf" // None of these can make stack problems worse
"["
"xarrscLM" // Turn into SSA and simplify
"cCTUtTOntnfDIul" // Perform structural simplification
@@ -47,7 +47,7 @@ struct OptimiserSettings
"gvif" // Run full inliner
"CTUcarrLsTOtfDncarrIulc" // SSA plus simplify
"]"
"jmuljuljul VcTOcul jmulN"; // Make source short and pretty
"jmuljuljul VcTOcul jmul"; // Make source short and pretty
/// No optimisations at all - not recommended.
static OptimiserSettings none()