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 #9854 from ethereum/bitwiseSmt

Browse Source 
[SMTChecker] Support compound shifts and bitwise and, or, and xor
This commit is contained in:
Đorđe Mijović 2020-09-23 12:35:48 +02:00 committed by GitHub
commit 858b4507e2
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
26 changed files with 363 additions and 135 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -8,6 +8,7 @@ Compiler Features:
* SMTChecker: Support events and low-level logs.
* SMTChecker: Support ``revert()``.
* SMTChecker: Support shifts.
* SMTChecker: Support compound and, or, and xor operators.
* SMTChecker: Support structs.
* SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
* SMTChecker: Support ``address`` type conversion with literals, e.g. ``address(0)``.

143
libsolidity/formal/SMTEncoder.cpp
View File

@ -352,31 +352,10 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
{
createExpr(_assignment);
static set<Token> const compoundOps{
Token::AssignAdd,
Token::AssignSub,
Token::AssignMul,
Token::AssignDiv,
Token::AssignMod
};
Token op = _assignment.assignmentOperator();
if (op != Token::Assign && !compoundOps.count(op))
{
Expression const* identifier = &_assignment.leftHandSide();
if (auto const* indexAccess = dynamic_cast<IndexAccess const*>(identifier))
identifier = leftmostBase(*indexAccess);
// Give it a new index anyway to keep the SSA scheme sound.
solAssert(identifier, "");
if (auto varDecl = identifierToVariable(*identifier))
m_context.newValue(*varDecl);
solAssert(TokenTraits::isAssignmentOp(op), "");
m_errorReporter.warning(
9149_error,
_assignment.location(),
"Assertion checker does not yet implement this assignment operator."
);
}
else if (!smt::isSupportedType(*_assignment.annotation().type))
if (!smt::isSupportedType(*_assignment.annotation().type))
{
// Give it a new index anyway to keep the SSA scheme sound.
@ -394,9 +373,9 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
else
{
auto const& type = _assignment.annotation().type;
auto rightHandSide = compoundOps.count(op) ?
compoundAssignment(_assignment) :
expr(_assignment.rightHandSide(), type);
auto rightHandSide = op == Token::Assign ?
expr(_assignment.rightHandSide(), type) :
compoundAssignment(_assignment);
defineExpr(_assignment, rightHandSide);
assignment(
_assignment.leftHandSide(),
@ -1388,6 +1367,59 @@ pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
return {value, valueUnbounded};
}
smtutil::Expression SMTEncoder::bitwiseOperation(
Token _op,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
TypePointer const& _commonType
)
{
static set<Token> validOperators{
Token::BitAnd,
Token::BitOr,
Token::BitXor,
Token::SHL,
Token::SHR,
Token::SAR
};
solAssert(validOperators.count(_op), "");
solAssert(_commonType, "");
auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(_commonType);
auto bvLeft = smtutil::Expression::int2bv(_left, bvSize);
auto bvRight = smtutil::Expression::int2bv(_right, bvSize);
optional<smtutil::Expression> result;
switch (_op)
{
case Token::BitAnd:
result = bvLeft & bvRight;
break;
case Token::BitOr:
result = bvLeft | bvRight;
break;
case Token::BitXor:
result = bvLeft ^ bvRight;
break;
case Token::SHL:
result = bvLeft << bvRight;
break;
case Token::SHR:
solAssert(false, "");
case Token::SAR:
result = isSigned ?
smtutil::Expression::ashr(bvLeft, bvRight) :
bvLeft >> bvRight;
break;
default:
solAssert(false, "");
}
solAssert(result.has_value(), "");
return smtutil::Expression::bv2int(*result, isSigned);
}
void SMTEncoder::compareOperation(BinaryOperation const& _op)
{
auto const& commonType = _op.annotation().commonType;
@ -1464,39 +1496,12 @@ void SMTEncoder::bitwiseOperation(BinaryOperation const& _op)
auto commonType = _op.annotation().commonType;
solAssert(commonType, "");
auto [bvSize, isSigned] = smt::typeBvSizeAndSignedness(commonType);
auto bvLeft = smtutil::Expression::int2bv(expr(_op.leftExpression(), commonType), bvSize);
auto bvRight = smtutil::Expression::int2bv(expr(_op.rightExpression(), commonType), bvSize);
optional<smtutil::Expression> result;
switch (op)
{
case Token::BitAnd:
result = bvLeft & bvRight;
break;
case Token::BitOr:
result = bvLeft | bvRight;
break;
case Token::BitXor:
result = bvLeft ^ bvRight;
break;
case Token::SHL:
result = bvLeft << bvRight;
break;
case Token::SHR:
solAssert(false, "");
case Token::SAR:
result = isSigned ?
smtutil::Expression::ashr(bvLeft, bvRight) :
bvLeft >> bvRight;
break;
default:
solAssert(false, "");
}
solAssert(result, "");
defineExpr(_op, smtutil::Expression::bv2int(*result, isSigned));
defineExpr(_op, bitwiseOperation(
_op.getOperator(),
expr(_op.leftExpression(), commonType),
expr(_op.rightExpression(), commonType),
commonType
));
}
void SMTEncoder::bitwiseNotOperation(UnaryOperation const& _op)
@ -1604,9 +1609,27 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment
{Token::AssignDiv, Token::Div},
{Token::AssignMod, Token::Mod}
};
static map<Token, Token> const compoundToBitwise{
{Token::AssignBitAnd, Token::BitAnd},
{Token::AssignBitOr, Token::BitOr},
{Token::AssignBitXor, Token::BitXor},
{Token::AssignShl, Token::SHL},
{Token::AssignShr, Token::SHR},
{Token::AssignSar, Token::SAR}
};
Token op = _assignment.assignmentOperator();
solAssert(compoundToArithmetic.count(op), "");
solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), "");
auto decl = identifierToVariable(_assignment.leftHandSide());
if (compoundToBitwise.count(op))
return bitwiseOperation(
compoundToBitwise.at(op),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),
expr(_assignment.rightHandSide()),
_assignment.annotation().type
);
auto values = arithmeticOperation(
compoundToArithmetic.at(op),
decl ? currentValue(*decl) : expr(_assignment.leftHandSide()),

8
libsolidity/formal/SMTEncoder.h
View File

@ -119,6 +119,14 @@ protected:
TypePointer const& _commonType,
Expression const& _expression
);
smtutil::Expression bitwiseOperation(
Token _op,
smtutil::Expression const& _left,
smtutil::Expression const& _right,
TypePointer const& _commonType
);
void compareOperation(BinaryOperation const& _op);
void booleanOperation(BinaryOperation const& _op);
void bitwiseOperation(BinaryOperation const& _op);

13
test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol
View File

@ -1,13 +0,0 @@
pragma experimental SMTChecker;
contract C {
function f(bool b) public pure {
uint v = 1;
if (b)
v &= 1;
assert(v == 1);
}
}
// ----
// Warning 6328: (116-130): Assertion violation happens here.
// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator.

14
test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
function f() public pure returns (byte) {
byte a = 0xff;
byte b = 0xf0;
a &= b;
assert(a == b);
a &= ~b;
assert(a != 0); // fails
}
}
// ----
// Warning 6328: (203-217): Assertion violation happens here.

21
test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol Normal file
View File

@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
int8 x = 1;
int8 y = 0;
x &= y;
assert(x != 0); // fails
x = -1; y = 3;
y &= x;
assert(y == 3);
y = -1;
y &= x;
assert(y == -1);
y = 127;
x &= y;
assert(x == 127);
}
}
// ----
// Warning 6328: (114-128): Assertion violation happens here.

33
test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol Normal file
View File

@ -0,0 +1,33 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
uint v = 1;
v &= 1;
assert(v == 1);
v = 7;
v &= 3;
assert(v != 3); // fails, as 7 & 3 = 3
uint c = 0;
c &= v;
assert(c == 0);
uint8 x = 0xff;
uint16 y = 0xffff;
y &= x;
assert(y == 0xff);
assert(y == 0xffff); // fails
y = 0xffff;
x = 0xff;
y &= y | x;
assert(y == 0xffff);
assert(y == 0xff); // fails
}
}
// ----
// Warning 6328: (177-191): Assertion violation happens here.
// Warning 6328: (380-399): Assertion violation happens here.
// Warning 6328: (506-523): Assertion violation happens here.

10
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol
View File

@ -1,10 +0,0 @@
pragma experimental SMTChecker;
contract C {
int[1] c;
function f(bool b) public {
if (b)
c[0] |= 1;
}
}
// ----
// Warning 9149: (97-106): Assertion checker does not yet implement this assignment operator.

10
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol
View File

@ -1,10 +0,0 @@
pragma experimental SMTChecker;
contract C {
int[1][20] c;
function f(bool b) public {
if (b)
c[10][0] |= 1;
}
}
// ----
// Warning 9149: (101-114): Assertion checker does not yet implement this assignment operator.

13
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol
View File

@ -1,13 +0,0 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint x;
}
S s;
function f(bool b) public {
if (b)
s.x |= 1;
}
}
// ----
// Warning 9149: (117-125): Assertion checker does not yet implement this assignment operator.

13
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol
View File

@ -1,13 +0,0 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint[] x;
}
S s;
function f(bool b) public {
if (b)
s.x[2] |= 1;
}
}
// ----
// Warning 9149: (119-130): Assertion checker does not yet implement this assignment operator.

14
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
function f() public pure returns (byte) {
byte a = 0xff;
byte b = 0xf0;
b |= a;
assert(a == b);
a |= ~b;
assert(a == 0); // fails
}
}
// ----
// Warning 6328: (203-217): Assertion violation happens here.

21
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol Normal file
View File

@ -0,0 +1,21 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
int8 x = 1;
int8 y = 0;
x |= y;
assert(x == 0); // fails
x = -1; y = 3;
x |= y;
assert(x == -1);
x = 4;
y |= x;
assert(y == 7);
y = 127;
x |= y;
assert(x == 127);
}
}
// ----
// Warning 6328: (114-128): Assertion violation happens here.

11
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
int[1][20] c;
function f(bool b) public {
require(c[10][0] == 0);
if (b)
c[10][0] |= 1;
assert(c[10][0] == 0 || c[10][0] == 1);
}
}
// ----

29
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol Normal file
View File

@ -0,0 +1,29 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
uint v = 7;
v |= 3;
assert(v != 7); // fails, as 7 | 3 = 7
uint c = 0;
c |= v;
assert(c == 7);
uint16 x = 0xff;
uint16 y = 0xffff;
y |= x;
assert(y == 0xff); // fails
assert(y == 0xffff);
y = 0xf1ff;
x = 0xff00;
x |= y & x;
assert(y == 0xffff); // fails
assert(x == 0xff00);
}
}
// ----
// Warning 6328: (121-135): Assertion violation happens here.
// Warning 6328: (298-315): Assertion violation happens here.
// Warning 6328: (424-443): Assertion violation happens here.

11
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol Normal file
View File

@ -0,0 +1,11 @@
pragma experimental SMTChecker;
contract C {
uint[1] c;
function f(bool b) public {
require(c[0] == 0);
if (b)
c[0] |= 1;
assert(c[0] <= 1);
}
}
// ----

14
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint[] x;
}
S s;
function f(bool b) public {
if (b)
s.x[2] |= 1;
assert(s.x[2] != 1);
}
}
// ----
// Warning 6328: (173-192): Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C {
struct S {
uint x;
}
S s;
function f(bool b) public {
s.x |= b ? 1 : 2;
assert(s.x > 0);
}
}
// ----

13
test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol
View File

@ -1,13 +0,0 @@
pragma experimental SMTChecker;
contract C {
function f(bool b) public pure {
uint v = 0;
if (b)
v ^= 1;
assert(v == 1);
}
}
// ----
// Warning 6328: (116-130): Assertion violation happens here.
// Warning 9149: (106-112): Assertion checker does not yet implement this assignment operator.

14
test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
function f() public pure returns (byte) {
byte a = 0xff;
byte b = 0xf0;
a ^= ~b;
assert(a == b);
a ^= ~b;
assert(a != 0xff); // fails
}
}
// ----
// Warning 6328: (204-221): Assertion violation happens here.

18
test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol Normal file
View File

@ -0,0 +1,18 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
int8 x = 1;
int8 y = 0;
x ^= y;
assert(x != 1); // fails
x = -1; y = 1;
x ^= y;
assert(x == -2);
x = 4;
y ^= x;
assert(y == 5);
}
}
// ----
// Warning 6328: (114-128): Assertion violation happens here.

29
test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol Normal file
View File

@ -0,0 +1,29 @@
pragma experimental SMTChecker;
contract C {
function f() public pure {
uint v = 7;
v ^= 3;
assert(v != 4); // fails, as 7 ^ 3 = 4
uint c = 0;
c ^= v;
assert(c == 4);
uint16 x = 0xff;
uint16 y = 0xffff;
y ^= x;
assert(y == 0xff); // fails
assert(y == 0xff00);
y = 0xf1;
x = 0xff00;
y ^= x | y;
assert(y == 0xffff); // fails
assert(x == 0xff00);
}
}
// ----
// Warning 6328: (121-135): Assertion violation happens here.
// Warning 6328: (298-315): Assertion violation happens here.
// Warning 6328: (422-441): Assertion violation happens here.

2
test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol
View File

@ -9,5 +9,3 @@ contract C {
}
}
// ----
// Warning 6328: (123-136): Assertion violation happens here.
// Warning 9149: (112-119): Assertion checker does not yet implement this assignment operator.

1
test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol
View File

@ -10,4 +10,3 @@ contract C {
}
// ----
// Warning 6328: (117-130): Assertion violation happens here.
// Warning 9149: (106-113): Assertion checker does not yet implement this assignment operator.

15
test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
function f(uint256 a, uint256 b) internal pure returns (uint256) {
a <<= b;
return a;
}
function t() public pure {
assert(f(0x4266, 0x0) == 0x4266);
assert(f(0x4266, 0x8) == 0x426600);
assert(f(0x4266, 0xf0) == 0x4266000000000000000000000000000000000000000000000000000000000000);
assert(f(0x4266, 0x4266) == 0);
}
}
// ----

15
test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol Normal file
View File

@ -0,0 +1,15 @@
pragma experimental SMTChecker;
contract C {
function f(uint256 a, uint256 b) internal pure returns (uint256) {
a >>= b;
return a;
}
function t() public pure {
assert(f(0x4266, 0) == 0x4266);
assert(f(0x4266, 0x8) == 0x42);
assert(f(0x4266, 0x11) == 0);
assert(f(57896044618658097711785492504343953926634992332820282019728792003956564819968, 5) == 1809251394333065553493296640760748560207343510400633813116524750123642650624);
}
}
// ----