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

Merge pull request #11032 from blishko/smt_string_to_bytes

Browse Source 
[SMTChecker] Fix analysis of push to a string casted to bytes
This commit is contained in:
Leonardo 2021-03-03 20:29:51 +01:00 committed by GitHub
commit be5647735e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 67 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Changelog.md
View File

@ -7,7 +7,7 @@ Compiler Features:
Bugfixes:
* SMTChecker: Fix internal error on pushing to ``string`` casted to ``bytes``.
AST Changes:

35
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))
{
@ -1654,8 +1654,10 @@ void SMTEncoder::arrayPushPopAssign(Expression const& _expr, smtutil::Expression
indexOrMemberAssignment(_expr, _array);
else if (auto const* funCall = dynamic_cast<FunctionCall const*>(expr))
{
FunctionType const& funType = dynamic_cast<FunctionType const&>(*funCall->expression().annotation().type);
if (funType.kind() == FunctionType::Kind::ArrayPush)
if (
auto funType = dynamic_cast<FunctionType const*>(funCall->expression().annotation().type);
funType && funType->kind() == FunctionType::Kind::ArrayPush
)
{
auto memberAccess = dynamic_cast<MemberAccess const*>(&funCall->expression());
solAssert(memberAccess, "");
@ -2608,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

14
test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_1.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
string x;
function s() public {
x = "abc";
bytes(x).push("a");
assert(bytes(x).length == 4); // should hold
assert(bytes(x).length == 3); // should fail
}
}
// ----
// Warning 6328: (165-193): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()

14
test/libsolidity/smtCheckerTests/typecast/string_to_bytes_push_2.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
string x;
function s() public {
x = "abc";
((bytes(((x))))).push("a");
assert(bytes(x).length == 4); // should hold
assert(bytes(x).length == 3); // should fail
}
}
// ----
// Warning 6328: (173-201): CHC: Assertion violation happens here.\nCounterexample:\nx = [97, 98, 99, 97]\n\nTransaction trace:\nC.constructor()\nState: x = []\nC.s()