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

[SMTChecker] Ensure that push to a string casted to bytes is registered in the original string

Browse Source
This commit is contained in:
Martin Blicha 2021-03-02 18:29:52 +01:00
parent 41a01de664
commit 41fc59f00f
2 changed files with 34 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
libsolidity/formal/SMTEncoder.cpp
View File

@ -1635,7 +1635,7 @@ void SMTEncoder::arrayPop(FunctionCall const& _funCall)
void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression const& _array)
{
Expression const* expr = innermostTuple(_expr);
Expression const* expr = cleanExpression(_expr);
if (auto const* id = dynamic_cast<Identifier const*>(expr))
{
@ -2610,6 +2610,33 @@ Expression const* SMTEncoder::innermostTuple(Expression const& _expr)
return expr;
}
Expression const* SMTEncoder::cleanExpression(Expression const& _expr)
{
auto const* expr = &_expr;
if (auto const* tuple = dynamic_cast<TupleExpression const*>(expr))
return cleanExpression(*innermostTuple(*tuple));
if (auto const* functionCall = dynamic_cast<FunctionCall const*>(expr))
if (*functionCall->annotation().kind == FunctionCallKind::TypeConversion)
{
auto typeType = dynamic_cast<TypeType const*>(functionCall->expression().annotation().type);
solAssert(typeType, "");
if (auto const* arrayType = dynamic_cast<ArrayType const*>(typeType->actualType()))
if (arrayType->isByteArray())
{
// this is a cast to `bytes`
solAssert(functionCall->arguments().size() == 1, "");
Expression const& arg = *functionCall->arguments()[0];
if (
auto const* argArrayType = dynamic_cast<ArrayType const*>(arg.annotation().type);
argArrayType && argArrayType->isByteArray()
)
return cleanExpression(arg);
}
}
solAssert(expr, "");
return expr;
}
set<VariableDeclaration const*> SMTEncoder::touchedVariables(ASTNode const& _node)
{
vector<CallableDeclaration const*> callStack;

6
libsolidity/formal/SMTEncoder.h
View File

@ -68,6 +68,12 @@ public:
/// otherwise _expr.
static Expression const* innermostTuple(Expression const& _expr);
/// @returns the expression after stripping redundant syntactic sugar.
/// Currently supports stripping:
/// 1. 1-tuple; i.e. ((x)) -> x
/// 2. Explicit cast from string to bytes; i.e. bytes(s) -> s; for s of type string
static Expression const* cleanExpression(Expression const& _expr);
/// @returns the FunctionDefinition of a FunctionCall
/// if possible or nullptr.
/// @param _scopeContract is the contract that contains the function currently being