cerc-io/solidity
16
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 #9424 from ethereum/smt_fix_bitwise_fixed_bytes

Browse Source 
[SMTChecker] Fix ICE when bitwise operator on fixed bytes
This commit is contained in:
chriseth 2020-07-16 13:27:37 +02:00 committed by GitHub
commit 13e19529c3
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 40 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -9,6 +9,7 @@ Compiler Features:
* Yul EVM Code Transform: Free stack slots directly after visiting the right-hand-side of variable declarations instead of at the end of the statement only.
Bugfixes:
* SMTChecker: Fix internal error when using bitwise operators on fixed bytes type.
* Type Checker: Fix overload resolution in combination with ``{value: ...}``.
* Type Checker: Fix internal compiler error related to oversized types.

23
libsmtutil/SolverInterface.h
View File

@ -59,10 +59,10 @@ class Expression
public:
explicit Expression(bool _v): Expression(_v ? "true" : "false", Kind::Bool) {}
explicit Expression(std::shared_ptr<SortSort> _sort, std::string _name = ""): Expression(std::move(_name), {}, _sort) {}
Expression(size_t _number): Expression(std::to_string(_number), Kind::Int) {}
Expression(u256 const& _number): Expression(_number.str(), Kind::Int) {}
Expression(s256 const& _number): Expression(_number.str(), Kind::Int) {}
Expression(bigint const& _number): Expression(_number.str(), Kind::Int) {}
Expression(size_t _number): Expression(std::to_string(_number), {}, SortProvider::sintSort) {}
Expression(u256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
Expression(s256 const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
Expression(bigint const& _number): Expression(_number.str(), {}, SortProvider::sintSort) {}
Expression(Expression const&) = default;
Expression(Expression&&) = default;
@ -262,23 +262,28 @@ public:
}
friend Expression operator+(Expression _a, Expression _b)
{
return Expression("+", std::move(_a), std::move(_b), Kind::Int);
auto intSort = _a.sort;
return Expression("+", {std::move(_a), std::move(_b)}, intSort);
}
friend Expression operator-(Expression _a, Expression _b)
{
return Expression("-", std::move(_a), std::move(_b), Kind::Int);
auto intSort = _a.sort;
return Expression("-", {std::move(_a), std::move(_b)}, intSort);
}
friend Expression operator*(Expression _a, Expression _b)
{
return Expression("*", std::move(_a), std::move(_b), Kind::Int);
auto intSort = _a.sort;
return Expression("*", {std::move(_a), std::move(_b)}, intSort);
}
friend Expression operator/(Expression _a, Expression _b)
{
return Expression("/", std::move(_a), std::move(_b), Kind::Int);
auto intSort = _a.sort;
return Expression("/", {std::move(_a), std::move(_b)}, intSort);
}
friend Expression operator%(Expression _a, Expression _b)
{
return Expression("mod", std::move(_a), std::move(_b), Kind::Int);
auto intSort = _a.sort;
return Expression("mod", {std::move(_a), std::move(_b)}, intSort);
}
friend Expression operator&(Expression _a, Expression _b)
{

6
libsolidity/formal/SMTEncoder.cpp
View File

@ -1376,9 +1376,11 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
bvSize = fixedType->numBits();
isSigned = fixedType->isSigned();
}
else if (auto const* fixedBytesType = dynamic_cast<FixedBytesType const*>(commonType))
bvSize = fixedBytesType->numBytes() * 8;
auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression()), bvSize);
auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression()), bvSize);
auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression(), commonType), bvSize);
auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize);
optional<smtutil::Expression> result;
if (_op.getOperator() == Token::BitAnd)

4
libsolidity/formal/SymbolicTypes.cpp
View File

@ -441,7 +441,11 @@ optional<smtutil::Expression> symbolicTypeConversion(TypePointer _from, TypePoin
// case they'd need to be encoded as numbers.
if (auto strType = dynamic_cast<StringLiteralType const*>(_from))
if (_to->category() == frontend::Type::Category::FixedBytes)
{
if (strType->value().empty())
return smtutil::Expression(size_t(0));
return smtutil::Expression(u256(toHex(util::asBytes(strType->value()), util::HexPrefix::Add)));
}
return std::nullopt;
}

8
test/libsolidity/smtCheckerTests/operators/bitwise_and_fixed_bytes.sol Normal file
View File

@ -0,0 +1,8 @@
pragma experimental SMTChecker;
contract C {
function f() public pure returns (byte) {
return (byte("") & (""));
}
}
// ----
// Warning 5084: (101-109): Type conversion is not yet fully supported and might yield false positives.

9
test/libsolidity/smtCheckerTests/operators/bitwise_xor_fixed_bytes.sol Normal file
View File

@ -0,0 +1,9 @@
pragma experimental SMTChecker;
contract Simp {
function f3() public pure returns (byte) {
bytes memory y = "def";
return y[0] ^ "e";
}
}
// ----
// Warning 1093: (142-152): Assertion checker does not yet implement this bitwise operator.