From 773e000227db1cdd9164d6d58a9f5c4c01c672fc Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Mon, 21 Sep 2020 16:54:58 +0200 Subject: [PATCH 01/19] [SMTChecker] Implementing compound bitwise And/Or/Xor operators --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 114 +++++++++++++++++++++--------- libsolidity/formal/SMTEncoder.h | 8 +++ 3 files changed, 88 insertions(+), 35 deletions(-) diff --git a/Changelog.md b/Changelog.md index fb05610a5..c994a90f6 100644 --- a/Changelog.md +++ b/Changelog.md @@ -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``. * Yul Optimizer: Prune unused parameters in functions. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 90df7a908..f9c7cce50 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -357,7 +357,10 @@ void SMTEncoder::endVisit(Assignment const& _assignment) Token::AssignSub, Token::AssignMul, Token::AssignDiv, - Token::AssignMod + Token::AssignMod, + Token::AssignBitAnd, + Token::AssignBitOr, + Token::AssignBitXor }; Token op = _assignment.assignmentOperator(); if (op != Token::Assign && !compoundOps.count(op)) @@ -1381,6 +1384,59 @@ pair SMTEncoder::arithmeticOperation( return {value, valueUnbounded}; } +smtutil::Expression SMTEncoder::bitwiseOperation( + Token _op, + smtutil::Expression const& _left, + smtutil::Expression const& _right, + TypePointer const& _commonType +) +{ + static set 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 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; @@ -1457,39 +1513,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 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) @@ -1597,9 +1626,24 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment {Token::AssignDiv, Token::Div}, {Token::AssignMod, Token::Mod} }; + static map const compoundToBitwise{ + {Token::AssignBitAnd, Token::BitAnd}, + {Token::AssignBitOr, Token::BitOr}, + {Token::AssignBitXor, Token::BitXor} + }; 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()), diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 9bb7b81ce..454f8777c 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -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); From 69df163dcb3c25acfa2a8bb4642bfa1b335bf9ec Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Mon, 21 Sep 2020 16:55:32 +0200 Subject: [PATCH 02/19] [SMTChecker] Updating old and adding new tests for compound bitwise and operator. --- .../operators/compound_bitwise_and_1.sol | 13 -------- .../compound_bitwise_and_fixed_bytes.sol | 14 ++++++++ .../operators/compound_bitwise_and_int.sol | 21 ++++++++++++ .../operators/compound_bitwise_and_uint.sol | 33 +++++++++++++++++++ 4 files changed, 68 insertions(+), 13 deletions(-) delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol deleted file mode 100644 index d80dbb90a..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol +++ /dev/null @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol new file mode 100644 index 000000000..1f733c429 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_fixed_bytes.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol new file mode 100644 index 000000000..309fa64c0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_int.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol new file mode 100644 index 000000000..33da9936f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_uint.sol @@ -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. From e2e0b33ee7a204c316c72e1562e89e5347285281 Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Tue, 22 Sep 2020 10:14:31 +0200 Subject: [PATCH 03/19] [SMTChecker] Updating old and adding new tests for compound bitwise or operator. --- .../operators/compound_bitwise_or_1.sol | 10 ------- .../operators/compound_bitwise_or_2.sol | 10 ------- .../operators/compound_bitwise_or_3.sol | 13 --------- .../operators/compound_bitwise_or_4.sol | 13 --------- .../compound_bitwise_or_fixed_bytes.sol | 14 +++++++++ .../operators/compound_bitwise_or_int.sol | 21 ++++++++++++++ .../operators/compound_bitwise_or_int_1.sol | 11 +++++++ .../operators/compound_bitwise_or_uint.sol | 29 +++++++++++++++++++ .../operators/compound_bitwise_or_uint_1.sol | 11 +++++++ .../operators/compound_bitwise_or_uint_2.sol | 14 +++++++++ .../operators/compound_bitwise_or_uint_3.sol | 12 ++++++++ 11 files changed, 112 insertions(+), 46 deletions(-) delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol deleted file mode 100644 index 24e61cf58..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol +++ /dev/null @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol deleted file mode 100644 index 4569afa88..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_2.sol +++ /dev/null @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol deleted file mode 100644 index fdcfa3e14..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_3.sol +++ /dev/null @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol deleted file mode 100644 index 00e32d0d1..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_4.sol +++ /dev/null @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol new file mode 100644 index 000000000..8be3855b0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_fixed_bytes.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol new file mode 100644 index 000000000..b6fd90ce7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol new file mode 100644 index 000000000..e25ae354d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol @@ -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); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol new file mode 100644 index 000000000..ddc0c4376 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol new file mode 100644 index 000000000..790d30a76 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol @@ -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); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol new file mode 100644 index 000000000..04d907cf4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol new file mode 100644 index 000000000..8132ae773 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol @@ -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); + } +} +// ---- From 01939521067f77e51f8be019cdd2b6242ac005a5 Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Tue, 22 Sep 2020 10:14:06 +0200 Subject: [PATCH 04/19] [SMTChecker] Updating old and adding new tests for compound bitwise xor operator. --- .../operators/compound_bitwise_xor_1.sol | 13 --------- .../compound_bitwise_xor_fixed_bytes.sol | 14 +++++++++ .../operators/compound_bitwise_xor_int.sol | 18 ++++++++++++ .../operators/compound_bitwise_xor_uint.sol | 29 +++++++++++++++++++ 4 files changed, 61 insertions(+), 13 deletions(-) delete mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol deleted file mode 100644 index 22d3a5836..000000000 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol +++ /dev/null @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol new file mode 100644 index 000000000..fe60d8621 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_fixed_bytes.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol new file mode 100644 index 000000000..fc7dc19f7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_int.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol new file mode 100644 index 000000000..684e9fc01 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_uint.sol @@ -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. From 79f550dba94d5831be264745012cf0433556d8fb Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Tue, 22 Sep 2020 11:15:56 +0200 Subject: [PATCH 05/19] [SMTChecker] Supporting compound shift operators. --- libsolidity/formal/SMTEncoder.cpp | 39 +++++++------------------------ 1 file changed, 9 insertions(+), 30 deletions(-) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index f9c7cce50..b9eb3caac 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -352,34 +352,10 @@ void SMTEncoder::endVisit(Assignment const& _assignment) { createExpr(_assignment); - static set const compoundOps{ - Token::AssignAdd, - Token::AssignSub, - Token::AssignMul, - Token::AssignDiv, - Token::AssignMod, - Token::AssignBitAnd, - Token::AssignBitOr, - Token::AssignBitXor - }; Token op = _assignment.assignmentOperator(); - if (op != Token::Assign && !compoundOps.count(op)) - { - Expression const* identifier = &_assignment.leftHandSide(); - if (auto const* indexAccess = dynamic_cast(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. @@ -397,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(), @@ -1629,7 +1605,10 @@ smtutil::Expression SMTEncoder::compoundAssignment(Assignment const& _assignment static map const compoundToBitwise{ {Token::AssignBitAnd, Token::BitAnd}, {Token::AssignBitOr, Token::BitOr}, - {Token::AssignBitXor, Token::BitXor} + {Token::AssignBitXor, Token::BitXor}, + {Token::AssignShl, Token::SHL}, + {Token::AssignShr, Token::SHR}, + {Token::AssignSar, Token::SAR} }; Token op = _assignment.assignmentOperator(); solAssert(compoundToArithmetic.count(op) || compoundToBitwise.count(op), ""); From 96bafb9ba38af2e1e9b1300176b982881c040fe8 Mon Sep 17 00:00:00 2001 From: Djordje Mijovic Date: Tue, 22 Sep 2020 11:16:34 +0200 Subject: [PATCH 06/19] [SMTChecker] Updating old and adding new tests for compound shift operators. --- .../smtCheckerTests/operators/compound_shl_1.sol | 2 -- .../smtCheckerTests/operators/compound_shr_1.sol | 1 - .../operators/shifts/compound_shift_left.sol | 15 +++++++++++++++ .../operators/shifts/compound_shift_right.sol | 15 +++++++++++++++ 4 files changed, 30 insertions(+), 3 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol diff --git a/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol index 9b7a264d6..8ccc8a800 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol index 3887f3e5e..e54344d2d 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol @@ -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. diff --git a/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol b/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol new file mode 100644 index 000000000..442bd3a77 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_left.sol @@ -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); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol b/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol new file mode 100644 index 000000000..75dc0fe0d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/shifts/compound_shift_right.sol @@ -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); + } +} +// ---- From 91f7c6644f4590d25ed10b78f87ba9d8ddf6b086 Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 16 Sep 2020 16:49:43 +0200 Subject: [PATCH 07/19] Only expect more failure data params if they are there. --- test/libsolidity/util/ContractABIUtils.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/test/libsolidity/util/ContractABIUtils.cpp b/test/libsolidity/util/ContractABIUtils.cpp index a3a19e6e5..e3ab01128 100644 --- a/test/libsolidity/util/ContractABIUtils.cpp +++ b/test/libsolidity/util/ContractABIUtils.cpp @@ -319,8 +319,11 @@ solidity::frontend::test::ParameterList ContractABIUtils::failureParameters(byte ParameterList parameters; parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::HexString, ABIType::AlignNone, 4}, FormatInfo{}}); - parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::Hex}, FormatInfo{}}); - parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::UnsignedDec}, FormatInfo{}}); + if (_bytes.size() > 4) + { + parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::Hex}, FormatInfo{}}); + parameters.push_back(Parameter{bytes(), "", ABIType{ABIType::UnsignedDec}, FormatInfo{}}); + } /// If _bytes contains at least a 1 byte message (function selector + tail pointer + message length + message) /// append an additional string parameter to represent that message. From 55e6a926926d197c49a102b4208cd3ba68fec507 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 15 Sep 2020 14:25:07 +0200 Subject: [PATCH 08/19] Add specialization for small numbers. --- libsolidity/codegen/YulUtilFunctions.cpp | 31 ++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/libsolidity/codegen/YulUtilFunctions.cpp b/libsolidity/codegen/YulUtilFunctions.cpp index 13ad3644c..0669b3f45 100644 --- a/libsolidity/codegen/YulUtilFunctions.cpp +++ b/libsolidity/codegen/YulUtilFunctions.cpp @@ -632,6 +632,16 @@ string YulUtilFunctions::overflowCheckedIntExpFunction( string YulUtilFunctions::overflowCheckedUnsignedExpFunction() { + // Checks for the "small number specialization" below. + using namespace boost::multiprecision; + solAssert(pow(bigint(10), 77) < pow(bigint(2), 256), ""); + solAssert(pow(bigint(11), 77) >= pow(bigint(2), 256), ""); + solAssert(pow(bigint(10), 78) >= pow(bigint(2), 256), ""); + + solAssert(pow(bigint(306), 31) < pow(bigint(2), 256), ""); + solAssert(pow(bigint(307), 31) >= pow(bigint(2), 256), ""); + solAssert(pow(bigint(306), 32) >= pow(bigint(2), 256), ""); + string functionName = "checked_exp_unsigned"; return m_functionCollector.createFunction(functionName, [&]() { return @@ -644,6 +654,27 @@ string YulUtilFunctions::overflowCheckedUnsignedExpFunction() if iszero(exponent) { power := 1 leave } if iszero(base) { power := 0 leave } + // Specializations for small bases + switch base + // 0 is handled above + case 1 { power := 1 leave } + case 2 + { + if gt(exponent, 255) { revert(0, 0) } + power := exp(2, exponent) + if gt(power, max) { revert(0, 0) } + leave + } + if or( + and(lt(base, 11), lt(exponent, 78)), + and(lt(base, 307), lt(exponent, 32)) + ) + { + power := exp(base, exponent) + if gt(power, max) { revert(0, 0) } + leave + } + power := 1 for { } gt(exponent, 1) {} From e696c4eafd6351507b85a077ab95d9b56f7a4b92 Mon Sep 17 00:00:00 2001 From: chriseth Date: Tue, 15 Sep 2020 14:33:36 +0200 Subject: [PATCH 09/19] Extract common loop. --- libsolidity/codegen/YulUtilFunctions.cpp | 51 +++++++++++++++--------- libsolidity/codegen/YulUtilFunctions.h | 4 ++ 2 files changed, 37 insertions(+), 18 deletions(-) diff --git a/libsolidity/codegen/YulUtilFunctions.cpp b/libsolidity/codegen/YulUtilFunctions.cpp index 0669b3f45..f622ae812 100644 --- a/libsolidity/codegen/YulUtilFunctions.cpp +++ b/libsolidity/codegen/YulUtilFunctions.cpp @@ -675,25 +675,14 @@ string YulUtilFunctions::overflowCheckedUnsignedExpFunction() leave } - power := 1 + power, base := (1, base, exponent, max) - for { } gt(exponent, 1) {} - { - // overflow check for base * base - if gt(base, div(max, base)) { revert(0, 0) } - if and(exponent, 1) - { - // no check needed here because base >= power - power := mul(power, base) - } - base := mul(base, base) - exponent := (exponent) - } if gt(power, div(max, base)) { revert(0, 0) } power := mul(power, base) } )") ("functionName", functionName) + ("expLoop", overflowCheckedExpLoopFunction()) ("shr_1", shiftRightFunction(1)) .render(); }); @@ -734,6 +723,35 @@ string YulUtilFunctions::overflowCheckedSignedExpFunction() // Below this point, base is always positive. + power, base := (power, base, exponent, max) + + if and(sgt(power, 0), gt(power, div(max, base))) { revert(0, 0) } + if and(slt(power, 0), slt(power, sdiv(min, base))) { revert(0, 0) } + power := mul(power, base) + } + )") + ("functionName", functionName) + ("expLoop", overflowCheckedExpLoopFunction()) + ("shr_1", shiftRightFunction(1)) + .render(); + }); +} + +string YulUtilFunctions::overflowCheckedExpLoopFunction() +{ + // We use this loop for both signed and unsigned exponentiation + // because we pull out the first iteration in the signed case which + // results in the base always being positive. + + // This function does not include the final multiplication. + + string functionName = "checked_exp_helper"; + return m_functionCollector.createFunction(functionName, [&]() { + return + Whiskers(R"( + function (_power, _base, exponent, max) -> power, base { + power := _power + base := _base for { } gt(exponent, 1) {} { // overflow check for base * base @@ -743,16 +761,13 @@ string YulUtilFunctions::overflowCheckedSignedExpFunction() // No checks for power := mul(power, base) needed, because the check // for base * base above is sufficient, since: // |power| <= base (proof by induction) and thus: - // |power * base| <= base * base <= max <= |min| + // |power * base| <= base * base <= max <= |min| (for signed) + // (this is equally true for signed and unsigned exp) power := mul(power, base) } base := mul(base, base) exponent := (exponent) } - - if and(sgt(power, 0), gt(power, div(max, base))) { revert(0, 0) } - if and(slt(power, 0), slt(power, sdiv(min, base))) { revert(0, 0) } - power := mul(power, base) } )") ("functionName", functionName) diff --git a/libsolidity/codegen/YulUtilFunctions.h b/libsolidity/codegen/YulUtilFunctions.h index 8394c33af..0e6fd5147 100644 --- a/libsolidity/codegen/YulUtilFunctions.h +++ b/libsolidity/codegen/YulUtilFunctions.h @@ -140,6 +140,10 @@ public: /// signature: (base, exponent, min, max) -> power std::string overflowCheckedSignedExpFunction(); + /// Helper function for the two checked exponentiation functions. + /// signature: (power, base, exponent, max) -> power + std::string overflowCheckedExpLoopFunction(); + /// @returns the name of a function that fetches the length of the given /// array /// signature: (array) -> length From c314ca3cf2b2977db352ef62b60a3953d65a485a Mon Sep 17 00:00:00 2001 From: Harikrishnan Mulackal Date: Wed, 23 Sep 2020 11:50:05 +0200 Subject: [PATCH 10/19] Tests for signed exponentiation --- test/libsolidity/semanticTests/viaYul/exp_neg.sol | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/test/libsolidity/semanticTests/viaYul/exp_neg.sol b/test/libsolidity/semanticTests/viaYul/exp_neg.sol index aa2f5eb18..149e9159a 100644 --- a/test/libsolidity/semanticTests/viaYul/exp_neg.sol +++ b/test/libsolidity/semanticTests/viaYul/exp_neg.sol @@ -25,4 +25,9 @@ contract C { // f(int256,uint256): -2, 2 -> 4 // f(int256,uint256): -7, 63 -> -174251498233690814305510551794710260107945042018748343 // f(int256,uint256): -128, 2 -> 0x4000 -// f(int256,uint256): -1, 115792089237316195423570985008687907853269984665640564039457584007913129639935 -> -1 \ No newline at end of file +// f(int256,uint256): -1, 115792089237316195423570985008687907853269984665640564039457584007913129639935 -> -1 +// f(int256,uint256): -2, 255 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968 +// f(int256,uint256): -8, 85 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968 +// f(int256,uint256): -131072, 15 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968 +// f(int256,uint256): -32, 51 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968 +// f(int256,uint256): -57896044618658097711785492504343953926634992332820282019728792003956564819968, 1 -> -57896044618658097711785492504343953926634992332820282019728792003956564819968 From af8d78010efcaaebe08e9c2146ec2b8538203b64 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Wed, 23 Sep 2020 15:08:55 +0100 Subject: [PATCH 11/19] Display BoolResult from implicit/explicit conversions for more clarity in error messages --- Changelog.md | 1 + libsolidity/analysis/TypeChecker.cpp | 23 +++++++++++++------ .../indexing/array_multidim_rational.sol | 4 ++-- .../indexing/array_multim_overflow_index.sol | 6 ++--- .../indexing/array_negative_index.sol | 2 +- .../indexing/array_noninteger_index.sol | 2 +- .../indexing/fixedbytes_negative_index.sol | 2 +- .../indexing/fixedbytes_noninteger_index.sol | 2 +- .../struct_array_noninteger_index.sol | 2 +- .../111_overflow_caused_by_ether_units.sol | 2 +- ...initialization_with_incorrect_type_int.sol | 2 +- ...gative_integers_to_signed_out_of_bound.sol | 2 +- ...sitive_integers_to_signed_out_of_bound.sol | 2 +- .../194_negative_integers_to_unsigned.sol | 2 +- ...tive_integers_to_unsigned_out_of_bound.sol | 2 +- .../types/array_index_too_large.sol | 2 +- .../types/rational_number_bitshift_limit.sol | 4 ++-- .../types/rational_number_exp_limit_fail.sol | 20 ++++++++-------- .../types/rational_number_huge_fail.sol | 2 +- .../types/rational_number_mul_limit.sol | 2 +- 20 files changed, 48 insertions(+), 38 deletions(-) diff --git a/Changelog.md b/Changelog.md index 865e3320a..758600cb5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -12,6 +12,7 @@ Compiler Features: * 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)``. + * Type Checker: More detailed error messages why implicit conversions fail. * Yul Optimizer: Prune unused parameters in functions. * Yul Optimizer: Inline into functions further down in the call graph first. * Yul Optimizer: Try to simplify function names. diff --git a/libsolidity/analysis/TypeChecker.cpp b/libsolidity/analysis/TypeChecker.cpp index 6f351faba..98c79427d 100644 --- a/libsolidity/analysis/TypeChecker.cpp +++ b/libsolidity/analysis/TypeChecker.cpp @@ -1645,7 +1645,8 @@ TypePointer TypeChecker::typeCheckTypeConversionAndRetrieveReturnType( dataLoc = argRefType->location(); if (auto type = dynamic_cast(resultType)) resultType = TypeProvider::withLocation(type, dataLoc, type->isPointer()); - if (argType->isExplicitlyConvertibleTo(*resultType)) + BoolResult result = argType->isExplicitlyConvertibleTo(*resultType); + if (result) { if (auto argArrayType = dynamic_cast(argType)) { @@ -1716,14 +1717,15 @@ TypePointer TypeChecker::typeCheckTypeConversionAndRetrieveReturnType( "you can use the .address member of the function." ); else - m_errorReporter.typeError( + m_errorReporter.typeErrorConcatenateDescriptions( 9640_error, _functionCall.location(), "Explicit type conversion not allowed from \"" + argType->toString() + "\" to \"" + resultType->toString() + - "\"." + "\".", + result.message() ); } if (auto addressType = dynamic_cast(resultType)) @@ -3217,7 +3219,8 @@ Declaration const& TypeChecker::dereference(UserDefinedTypeName const& _typeName bool TypeChecker::expectType(Expression const& _expression, Type const& _expectedType) { _expression.accept(*this); - if (!type(_expression)->isImplicitlyConvertibleTo(_expectedType)) + BoolResult result = type(_expression)->isImplicitlyConvertibleTo(_expectedType); + if (!result) { auto errorMsg = "Type " + type(_expression)->toString() + @@ -3236,17 +3239,23 @@ bool TypeChecker::expectType(Expression const& _expression, Type const& _expecte errorMsg + ", but it can be explicitly converted." ); else - m_errorReporter.typeError( + m_errorReporter.typeErrorConcatenateDescriptions( 2326_error, _expression.location(), errorMsg + ". Try converting to type " + type(_expression)->mobileType()->toString() + - " or use an explicit conversion." + " or use an explicit conversion.", + result.message() ); } else - m_errorReporter.typeError(7407_error, _expression.location(), errorMsg + "."); + m_errorReporter.typeErrorConcatenateDescriptions( + 7407_error, + _expression.location(), + errorMsg + ".", + result.message() + ); return false; } return true; diff --git a/test/libsolidity/syntaxTests/indexing/array_multidim_rational.sol b/test/libsolidity/syntaxTests/indexing/array_multidim_rational.sol index ace6dbdda..b0d4dbb10 100644 --- a/test/libsolidity/syntaxTests/indexing/array_multidim_rational.sol +++ b/test/libsolidity/syntaxTests/indexing/array_multidim_rational.sol @@ -5,7 +5,7 @@ contract C { } } // ---- -// TypeError 7407: (67-72): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. -// TypeError 7407: (74-79): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. +// TypeError 7407: (67-72): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. +// TypeError 7407: (74-79): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. // TypeError 7407: (81-90): Type rational_const 9485...(73 digits omitted)...5712 / 5 is not implicitly convertible to expected type uint256. // TypeError 6318: (65-91): Index expression cannot be represented as an unsigned integer. diff --git a/test/libsolidity/syntaxTests/indexing/array_multim_overflow_index.sol b/test/libsolidity/syntaxTests/indexing/array_multim_overflow_index.sol index e7701e7ab..0f18ec4d2 100644 --- a/test/libsolidity/syntaxTests/indexing/array_multim_overflow_index.sol +++ b/test/libsolidity/syntaxTests/indexing/array_multim_overflow_index.sol @@ -5,7 +5,7 @@ contract C { } } // ---- -// TypeError 7407: (67-72): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. -// TypeError 7407: (74-79): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. -// TypeError 7407: (81-90): Type int_const -189...(75 digits omitted)...1423 is not implicitly convertible to expected type uint256. +// TypeError 7407: (67-72): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. +// TypeError 7407: (74-79): Type int_const 1897...(74 digits omitted)...1424 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. +// TypeError 7407: (81-90): Type int_const -189...(75 digits omitted)...1423 is not implicitly convertible to expected type uint256. Cannot implicitly convert signed literal to unsigned type. // TypeError 6318: (65-91): Index expression cannot be represented as an unsigned integer. diff --git a/test/libsolidity/syntaxTests/indexing/array_negative_index.sol b/test/libsolidity/syntaxTests/indexing/array_negative_index.sol index 17ea84088..810ad3b73 100644 --- a/test/libsolidity/syntaxTests/indexing/array_negative_index.sol +++ b/test/libsolidity/syntaxTests/indexing/array_negative_index.sol @@ -5,4 +5,4 @@ contract C { } } // ---- -// TypeError 7407: (67-69): Type int_const -1 is not implicitly convertible to expected type uint256. +// TypeError 7407: (67-69): Type int_const -1 is not implicitly convertible to expected type uint256. Cannot implicitly convert signed literal to unsigned type. diff --git a/test/libsolidity/syntaxTests/indexing/array_noninteger_index.sol b/test/libsolidity/syntaxTests/indexing/array_noninteger_index.sol index 086cd42a4..c1a62ffb4 100644 --- a/test/libsolidity/syntaxTests/indexing/array_noninteger_index.sol +++ b/test/libsolidity/syntaxTests/indexing/array_noninteger_index.sol @@ -5,4 +5,4 @@ contract C { } } // ---- -// TypeError 7407: (67-178): Type int_const 8888...(103 digits omitted)...8888 is not implicitly convertible to expected type uint256. +// TypeError 7407: (67-178): Type int_const 8888...(103 digits omitted)...8888 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. diff --git a/test/libsolidity/syntaxTests/indexing/fixedbytes_negative_index.sol b/test/libsolidity/syntaxTests/indexing/fixedbytes_negative_index.sol index aeb5fc873..4d6e8545e 100644 --- a/test/libsolidity/syntaxTests/indexing/fixedbytes_negative_index.sol +++ b/test/libsolidity/syntaxTests/indexing/fixedbytes_negative_index.sol @@ -5,5 +5,5 @@ contract C { } } // ---- -// TypeError 7407: (58-60): Type int_const -1 is not implicitly convertible to expected type uint256. +// TypeError 7407: (58-60): Type int_const -1 is not implicitly convertible to expected type uint256. Cannot implicitly convert signed literal to unsigned type. // TypeError 6318: (56-61): Index expression cannot be represented as an unsigned integer. diff --git a/test/libsolidity/syntaxTests/indexing/fixedbytes_noninteger_index.sol b/test/libsolidity/syntaxTests/indexing/fixedbytes_noninteger_index.sol index 2b874eab2..c73064245 100644 --- a/test/libsolidity/syntaxTests/indexing/fixedbytes_noninteger_index.sol +++ b/test/libsolidity/syntaxTests/indexing/fixedbytes_noninteger_index.sol @@ -5,5 +5,5 @@ contract C { } } // ---- -// TypeError 7407: (58-169): Type int_const 8888...(103 digits omitted)...8888 is not implicitly convertible to expected type uint256. +// TypeError 7407: (58-169): Type int_const 8888...(103 digits omitted)...8888 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. // TypeError 6318: (56-170): Index expression cannot be represented as an unsigned integer. diff --git a/test/libsolidity/syntaxTests/indexing/struct_array_noninteger_index.sol b/test/libsolidity/syntaxTests/indexing/struct_array_noninteger_index.sol index 93f81abbd..024c58940 100644 --- a/test/libsolidity/syntaxTests/indexing/struct_array_noninteger_index.sol +++ b/test/libsolidity/syntaxTests/indexing/struct_array_noninteger_index.sol @@ -7,4 +7,4 @@ contract test { } // ---- -// TypeError 7407: (101-241): Type int_const 7555...(132 digits omitted)...5555 is not implicitly convertible to expected type uint256. +// TypeError 7407: (101-241): Type int_const 7555...(132 digits omitted)...5555 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. diff --git a/test/libsolidity/syntaxTests/nameAndTypeResolution/111_overflow_caused_by_ether_units.sol b/test/libsolidity/syntaxTests/nameAndTypeResolution/111_overflow_caused_by_ether_units.sol index e0ac9fa5d..6cdda2514 100644 --- a/test/libsolidity/syntaxTests/nameAndTypeResolution/111_overflow_caused_by_ether_units.sol +++ b/test/libsolidity/syntaxTests/nameAndTypeResolution/111_overflow_caused_by_ether_units.sol @@ -5,4 +5,4 @@ contract c { uint256 a; } // ---- -// TypeError 7407: (45-111): Type int_const 1157...(70 digits omitted)...0000 is not implicitly convertible to expected type uint256. +// TypeError 7407: (45-111): Type int_const 1157...(70 digits omitted)...0000 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. diff --git a/test/libsolidity/syntaxTests/nameAndTypeResolution/158_storage_variable_initialization_with_incorrect_type_int.sol b/test/libsolidity/syntaxTests/nameAndTypeResolution/158_storage_variable_initialization_with_incorrect_type_int.sol index f2c36a00a..0d0baf400 100644 --- a/test/libsolidity/syntaxTests/nameAndTypeResolution/158_storage_variable_initialization_with_incorrect_type_int.sol +++ b/test/libsolidity/syntaxTests/nameAndTypeResolution/158_storage_variable_initialization_with_incorrect_type_int.sol @@ -2,4 +2,4 @@ contract c { uint8 a = 1000; } // ---- -// TypeError 7407: (27-31): Type int_const 1000 is not implicitly convertible to expected type uint8. +// TypeError 7407: (27-31): Type int_const 1000 is not implicitly convertible to expected type uint8. Literal is too large to fit in uint8. diff --git a/test/libsolidity/syntaxTests/nameAndTypeResolution/190_negative_integers_to_signed_out_of_bound.sol b/test/libsolidity/syntaxTests/nameAndTypeResolution/190_negative_integers_to_signed_out_of_bound.sol index f56a4fcd4..a4d84f2da 100644 --- a/test/libsolidity/syntaxTests/nameAndTypeResolution/190_negative_integers_to_signed_out_of_bound.sol +++ b/test/libsolidity/syntaxTests/nameAndTypeResolution/190_negative_integers_to_signed_out_of_bound.sol @@ -2,4 +2,4 @@ contract test { int8 public i = -129; } // ---- -// TypeError 7407: (36-40): Type int_const -129 is not implicitly convertible to expected type int8. +// TypeError 7407: (36-40): Type int_const -129 is not implicitly convertible to expected type int8. Literal is too large to fit in int8. diff --git a/test/libsolidity/syntaxTests/nameAndTypeResolution/192_positive_integers_to_signed_out_of_bound.sol b/test/libsolidity/syntaxTests/nameAndTypeResolution/192_positive_integers_to_signed_out_of_bound.sol index f62c51cdf..0bc4699b3 100644 --- a/test/libsolidity/syntaxTests/nameAndTypeResolution/192_positive_integers_to_signed_out_of_bound.sol +++ b/test/libsolidity/syntaxTests/nameAndTypeResolution/192_positive_integers_to_signed_out_of_bound.sol @@ -2,4 +2,4 @@ contract test { int8 public j = 128; } // ---- -// TypeError 7407: (36-39): Type int_const 128 is not implicitly convertible to expected type int8. +// TypeError 7407: (36-39): Type int_const 128 is not implicitly convertible to expected type int8. Literal is too large to fit in int8. diff --git a/test/libsolidity/syntaxTests/nameAndTypeResolution/194_negative_integers_to_unsigned.sol b/test/libsolidity/syntaxTests/nameAndTypeResolution/194_negative_integers_to_unsigned.sol index 0d04e87ea..0dac77a73 100644 --- a/test/libsolidity/syntaxTests/nameAndTypeResolution/194_negative_integers_to_unsigned.sol +++ b/test/libsolidity/syntaxTests/nameAndTypeResolution/194_negative_integers_to_unsigned.sol @@ -2,4 +2,4 @@ contract test { uint8 public x = -1; } // ---- -// TypeError 7407: (37-39): Type int_const -1 is not implicitly convertible to expected type uint8. +// TypeError 7407: (37-39): Type int_const -1 is not implicitly convertible to expected type uint8. Cannot implicitly convert signed literal to unsigned type. diff --git a/test/libsolidity/syntaxTests/nameAndTypeResolution/195_positive_integers_to_unsigned_out_of_bound.sol b/test/libsolidity/syntaxTests/nameAndTypeResolution/195_positive_integers_to_unsigned_out_of_bound.sol index 0b5942cfb..dbc43d7dd 100644 --- a/test/libsolidity/syntaxTests/nameAndTypeResolution/195_positive_integers_to_unsigned_out_of_bound.sol +++ b/test/libsolidity/syntaxTests/nameAndTypeResolution/195_positive_integers_to_unsigned_out_of_bound.sol @@ -2,4 +2,4 @@ contract test { uint8 public x = 700; } // ---- -// TypeError 7407: (37-40): Type int_const 700 is not implicitly convertible to expected type uint8. +// TypeError 7407: (37-40): Type int_const 700 is not implicitly convertible to expected type uint8. Literal is too large to fit in uint8. diff --git a/test/libsolidity/syntaxTests/types/array_index_too_large.sol b/test/libsolidity/syntaxTests/types/array_index_too_large.sol index 646004800..e9a57df3f 100644 --- a/test/libsolidity/syntaxTests/types/array_index_too_large.sol +++ b/test/libsolidity/syntaxTests/types/array_index_too_large.sol @@ -5,4 +5,4 @@ contract C { } } // ---- -// TypeError 7407: (140-218): Type int_const 1234...(70 digits omitted)...5678 is not implicitly convertible to expected type uint256. +// TypeError 7407: (140-218): Type int_const 1234...(70 digits omitted)...5678 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. diff --git a/test/libsolidity/syntaxTests/types/rational_number_bitshift_limit.sol b/test/libsolidity/syntaxTests/types/rational_number_bitshift_limit.sol index a397993b9..9c59b015c 100644 --- a/test/libsolidity/syntaxTests/types/rational_number_bitshift_limit.sol +++ b/test/libsolidity/syntaxTests/types/rational_number_bitshift_limit.sol @@ -7,7 +7,7 @@ contract c { } } // ---- -// TypeError 7407: (71-80): Type int_const 5221...(1225 digits omitted)...5168 is not implicitly convertible to expected type int256. +// TypeError 7407: (71-80): Type int_const 5221...(1225 digits omitted)...5168 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (133-142): Operator << not compatible with types int_const 1 and int_const 4096 // TypeError 2271: (169-182): Operator << not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const 2 -// TypeError 7407: (169-182): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (169-182): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. diff --git a/test/libsolidity/syntaxTests/types/rational_number_exp_limit_fail.sol b/test/libsolidity/syntaxTests/types/rational_number_exp_limit_fail.sol index a989c4583..39be18a28 100644 --- a/test/libsolidity/syntaxTests/types/rational_number_exp_limit_fail.sol +++ b/test/libsolidity/syntaxTests/types/rational_number_exp_limit_fail.sol @@ -20,28 +20,28 @@ contract c { } // ---- // TypeError 2271: (71-102): Operator ** not compatible with types int_const 1797...(301 digits omitted)...7216 and int_const 4. Precision of rational constants is limited to 4096 bits. -// TypeError 7407: (71-102): Type int_const 1797...(301 digits omitted)...7216 is not implicitly convertible to expected type int256. +// TypeError 7407: (71-102): Type int_const 1797...(301 digits omitted)...7216 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (116-148): Operator ** not compatible with types int_const 1797...(301 digits omitted)...7216 and int_const 4. Precision of rational constants is limited to 4096 bits. // TypeError 2271: (116-153): Operator ** not compatible with types int_const 1797...(301 digits omitted)...7216 and int_const 4. Precision of rational constants is limited to 4096 bits. -// TypeError 7407: (116-153): Type int_const 1797...(301 digits omitted)...7216 is not implicitly convertible to expected type int256. +// TypeError 7407: (116-153): Type int_const 1797...(301 digits omitted)...7216 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (167-203): Operator ** not compatible with types int_const 4 and int_const -179...(302 digits omitted)...7216 // TypeError 2271: (217-228): Operator ** not compatible with types int_const 2 and int_const 1000...(1226 digits omitted)...0000 // TypeError 2271: (242-254): Operator ** not compatible with types int_const -2 and int_const 1000...(1226 digits omitted)...0000 // TypeError 2271: (268-280): Operator ** not compatible with types int_const 2 and int_const -100...(1227 digits omitted)...0000 // TypeError 2271: (294-307): Operator ** not compatible with types int_const -2 and int_const -100...(1227 digits omitted)...0000 // TypeError 2271: (321-332): Operator ** not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const 2. Precision of rational constants is limited to 4096 bits. -// TypeError 7407: (321-332): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (321-332): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (346-358): Operator ** not compatible with types int_const -100...(1227 digits omitted)...0000 and int_const 2. Precision of rational constants is limited to 4096 bits. -// TypeError 7407: (346-358): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (346-358): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (372-384): Operator ** not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const -2. Precision of rational constants is limited to 4096 bits. -// TypeError 7407: (372-384): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (372-384): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (398-411): Operator ** not compatible with types int_const -100...(1227 digits omitted)...0000 and int_const -2. Precision of rational constants is limited to 4096 bits. -// TypeError 7407: (398-411): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (398-411): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (425-441): Operator ** not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const 1000...(1226 digits omitted)...0000 -// TypeError 7407: (425-441): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (425-441): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (455-472): Operator ** not compatible with types int_const 1000...(1226 digits omitted)...0000 and int_const -100...(1227 digits omitted)...0000 -// TypeError 7407: (455-472): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (455-472): Type int_const 1000...(1226 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (486-503): Operator ** not compatible with types int_const -100...(1227 digits omitted)...0000 and int_const 1000...(1226 digits omitted)...0000 -// TypeError 7407: (486-503): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (486-503): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. // TypeError 2271: (517-535): Operator ** not compatible with types int_const -100...(1227 digits omitted)...0000 and int_const -100...(1227 digits omitted)...0000 -// TypeError 7407: (517-535): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. +// TypeError 7407: (517-535): Type int_const -100...(1227 digits omitted)...0000 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. diff --git a/test/libsolidity/syntaxTests/types/rational_number_huge_fail.sol b/test/libsolidity/syntaxTests/types/rational_number_huge_fail.sol index 1e3239ddf..cec814ef3 100644 --- a/test/libsolidity/syntaxTests/types/rational_number_huge_fail.sol +++ b/test/libsolidity/syntaxTests/types/rational_number_huge_fail.sol @@ -5,4 +5,4 @@ contract C { } } // ---- -// TypeError 7407: (142-209): Type int_const 1852...(71 digits omitted)...7281 is not implicitly convertible to expected type uint256. +// TypeError 7407: (142-209): Type int_const 1852...(71 digits omitted)...7281 is not implicitly convertible to expected type uint256. Literal is too large to fit in uint256. diff --git a/test/libsolidity/syntaxTests/types/rational_number_mul_limit.sol b/test/libsolidity/syntaxTests/types/rational_number_mul_limit.sol index c2d94da36..a02578453 100644 --- a/test/libsolidity/syntaxTests/types/rational_number_mul_limit.sol +++ b/test/libsolidity/syntaxTests/types/rational_number_mul_limit.sol @@ -6,4 +6,4 @@ contract c { } // ---- // TypeError 2271: (71-90): Operator * not compatible with types int_const 5221...(1225 digits omitted)...5168 and int_const 5221...(1225 digits omitted)...5168. Precision of rational constants is limited to 4096 bits. -// TypeError 7407: (71-90): Type int_const 5221...(1225 digits omitted)...5168 is not implicitly convertible to expected type int256. +// TypeError 7407: (71-90): Type int_const 5221...(1225 digits omitted)...5168 is not implicitly convertible to expected type int256. Literal is too large to fit in int256. From ca743191b7e9c157520b4245b126dc36b9941a14 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Wed, 23 Sep 2020 16:31:17 +0100 Subject: [PATCH 12/19] Report why assigning oversized hex strings to bytes fail --- Changelog.md | 1 + libsolidity/ast/Types.cpp | 6 +++++- ...ex_assign.sol => bytesNN_index_assign.sol} | 0 ...o_contract.sol => bytesNN_to_contract.sol} | 0 ...size.sol => bytesNN_to_uint_same_size.sol} | 0 .../{bytesm.sol => bytesNN_upcasting.sol} | 0 .../bytesNN_with_oversized_hex_string.sol | 7 +++++++ ...> decimal_literal_to_bytesNN_explicit.sol} | 0 ...> decimal_literal_to_bytesNN_implicit.sol} | 0 ...al_to_bytesNN_different_size_explicit.sol} | 0 ...al_to_bytesNN_different_size_implicit.sol} | 0 ...literal_to_bytesNN_same_size_explicit.sol} | 0 ...literal_to_bytesNN_same_size_implicit.sol} | 0 ...ing_to_bytesNN_different_size_explicit.sol | 20 +++++++++++++++++++ ...x_string_to_bytesNN_same_size_explicit.sol | 13 ++++++++++++ ...x_string_to_bytesNN_same_size_implicit.sol | 13 ++++++++++++ ...l => zero_literal_to_bytesNN_explicit.sol} | 0 ...l => zero_literal_to_bytesNN_implicit.sol} | 0 18 files changed, 59 insertions(+), 1 deletion(-) rename test/libsolidity/syntaxTests/types/{bytesXX_index_assign.sol => bytesNN_index_assign.sol} (100%) rename test/libsolidity/syntaxTests/types/{bytes_to_contract.sol => bytesNN_to_contract.sol} (100%) rename test/libsolidity/syntaxTests/types/{bytes_to_uint_same_size.sol => bytesNN_to_uint_same_size.sol} (100%) rename test/libsolidity/syntaxTests/types/{bytesm.sol => bytesNN_upcasting.sol} (100%) create mode 100644 test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol rename test/libsolidity/syntaxTests/types/{decimal_literal_to_bytesXX_explicit.sol => decimal_literal_to_bytesNN_explicit.sol} (100%) rename test/libsolidity/syntaxTests/types/{decimal_literal_to_bytesXX_implicit.sol => decimal_literal_to_bytesNN_implicit.sol} (100%) rename test/libsolidity/syntaxTests/types/{hex_literal_to_bytesXX_different_size_explicit.sol => hex_literal_to_bytesNN_different_size_explicit.sol} (100%) rename test/libsolidity/syntaxTests/types/{hex_literal_to_bytesXX_different_size_implicit.sol => hex_literal_to_bytesNN_different_size_implicit.sol} (100%) rename test/libsolidity/syntaxTests/types/{hex_literal_to_bytesXX_same_size_explicit.sol => hex_literal_to_bytesNN_same_size_explicit.sol} (100%) rename test/libsolidity/syntaxTests/types/{hex_literal_to_bytesXX_same_size_implicit.sol => hex_literal_to_bytesNN_same_size_implicit.sol} (100%) create mode 100644 test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol create mode 100644 test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_explicit.sol create mode 100644 test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_implicit.sol rename test/libsolidity/syntaxTests/types/{zero_literal_to_bytesXX_explicit.sol => zero_literal_to_bytesNN_explicit.sol} (100%) rename test/libsolidity/syntaxTests/types/{zero_literal_to_bytesXX_implicit.sol => zero_literal_to_bytesNN_implicit.sol} (100%) diff --git a/Changelog.md b/Changelog.md index 758600cb5..be82d098b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -13,6 +13,7 @@ Compiler Features: * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``. * SMTChecker: Support ``address`` type conversion with literals, e.g. ``address(0)``. * Type Checker: More detailed error messages why implicit conversions fail. + * Type Checker: Explain why oversized hex string literals can not be explicitly converted to a shorter ``bytesNN`` type. * Yul Optimizer: Prune unused parameters in functions. * Yul Optimizer: Inline into functions further down in the call graph first. * Yul Optimizer: Try to simplify function names. diff --git a/libsolidity/ast/Types.cpp b/libsolidity/ast/Types.cpp index 322f5c7b7..7335ba548 100644 --- a/libsolidity/ast/Types.cpp +++ b/libsolidity/ast/Types.cpp @@ -1351,7 +1351,11 @@ StringLiteralType::StringLiteralType(string _value): BoolResult StringLiteralType::isImplicitlyConvertibleTo(Type const& _convertTo) const { if (auto fixedBytes = dynamic_cast(&_convertTo)) - return static_cast(fixedBytes->numBytes()) >= m_value.size(); + { + if (static_cast(fixedBytes->numBytes()) < m_value.size()) + return BoolResult::err("Literal is larger than the type."); + return true; + } else if (auto arrayType = dynamic_cast(&_convertTo)) return arrayType->location() != DataLocation::CallData && diff --git a/test/libsolidity/syntaxTests/types/bytesXX_index_assign.sol b/test/libsolidity/syntaxTests/types/bytesNN_index_assign.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/bytesXX_index_assign.sol rename to test/libsolidity/syntaxTests/types/bytesNN_index_assign.sol diff --git a/test/libsolidity/syntaxTests/types/bytes_to_contract.sol b/test/libsolidity/syntaxTests/types/bytesNN_to_contract.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/bytes_to_contract.sol rename to test/libsolidity/syntaxTests/types/bytesNN_to_contract.sol diff --git a/test/libsolidity/syntaxTests/types/bytes_to_uint_same_size.sol b/test/libsolidity/syntaxTests/types/bytesNN_to_uint_same_size.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/bytes_to_uint_same_size.sol rename to test/libsolidity/syntaxTests/types/bytesNN_to_uint_same_size.sol diff --git a/test/libsolidity/syntaxTests/types/bytesm.sol b/test/libsolidity/syntaxTests/types/bytesNN_upcasting.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/bytesm.sol rename to test/libsolidity/syntaxTests/types/bytesNN_upcasting.sol diff --git a/test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol b/test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol new file mode 100644 index 000000000..a76c4ec53 --- /dev/null +++ b/test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol @@ -0,0 +1,7 @@ +contract C { + function f() public pure returns (bytes2) { + return bytes2(hex"123456"); + } +} +// ---- +// TypeError 9640: (76-95): Explicit type conversion not allowed from "literal_string "4V"" to "bytes2". Literal is larger than the type. diff --git a/test/libsolidity/syntaxTests/types/decimal_literal_to_bytesXX_explicit.sol b/test/libsolidity/syntaxTests/types/decimal_literal_to_bytesNN_explicit.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/decimal_literal_to_bytesXX_explicit.sol rename to test/libsolidity/syntaxTests/types/decimal_literal_to_bytesNN_explicit.sol diff --git a/test/libsolidity/syntaxTests/types/decimal_literal_to_bytesXX_implicit.sol b/test/libsolidity/syntaxTests/types/decimal_literal_to_bytesNN_implicit.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/decimal_literal_to_bytesXX_implicit.sol rename to test/libsolidity/syntaxTests/types/decimal_literal_to_bytesNN_implicit.sol diff --git a/test/libsolidity/syntaxTests/types/hex_literal_to_bytesXX_different_size_explicit.sol b/test/libsolidity/syntaxTests/types/hex_literal_to_bytesNN_different_size_explicit.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/hex_literal_to_bytesXX_different_size_explicit.sol rename to test/libsolidity/syntaxTests/types/hex_literal_to_bytesNN_different_size_explicit.sol diff --git a/test/libsolidity/syntaxTests/types/hex_literal_to_bytesXX_different_size_implicit.sol b/test/libsolidity/syntaxTests/types/hex_literal_to_bytesNN_different_size_implicit.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/hex_literal_to_bytesXX_different_size_implicit.sol rename to test/libsolidity/syntaxTests/types/hex_literal_to_bytesNN_different_size_implicit.sol diff --git a/test/libsolidity/syntaxTests/types/hex_literal_to_bytesXX_same_size_explicit.sol b/test/libsolidity/syntaxTests/types/hex_literal_to_bytesNN_same_size_explicit.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/hex_literal_to_bytesXX_same_size_explicit.sol rename to test/libsolidity/syntaxTests/types/hex_literal_to_bytesNN_same_size_explicit.sol diff --git a/test/libsolidity/syntaxTests/types/hex_literal_to_bytesXX_same_size_implicit.sol b/test/libsolidity/syntaxTests/types/hex_literal_to_bytesNN_same_size_implicit.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/hex_literal_to_bytesXX_same_size_implicit.sol rename to test/libsolidity/syntaxTests/types/hex_literal_to_bytesNN_same_size_implicit.sol diff --git a/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol new file mode 100644 index 000000000..829199bf2 --- /dev/null +++ b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol @@ -0,0 +1,20 @@ +contract C { + function f() public pure { + bytes1 b1 = bytes1(hex""); + bytes1 b2 = bytes1(hex"1234"); + bytes2 b3 = bytes2(hex"12"); + bytes2 b4 = bytes2(hex"1234"); + bytes2 b5 = bytes2(hex"123456"); + bytes3 b6 = bytes3(hex"1234"); + bytes3 b7 = bytes3(hex"123456"); + bytes3 b8 = bytes3(hex"12345678"); + bytes4 b9 = bytes4(hex"123456"); + bytes4 b10 = bytes4(hex"12345678"); + bytes4 b11 = bytes4(hex"1234567890"); + } +} +// ---- +// TypeError 9640: (92-109): Explicit type conversion not allowed from "literal_string "4"" to "bytes1". Literal is larger than the type. +// TypeError 9640: (198-217): Explicit type conversion not allowed from "literal_string "4V"" to "bytes2". Literal is larger than the type. +// TypeError 9640: (310-331): Explicit type conversion not allowed from "literal_string "4Vx"" to "bytes3". Literal is larger than the type. +// TypeError 9640: (430-453): Explicit type conversion not allowed from "literal_string (contains invalid UTF-8 sequence at position 4)" to "bytes4". Literal is larger than the type. diff --git a/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_explicit.sol b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_explicit.sol new file mode 100644 index 000000000..e121abbd6 --- /dev/null +++ b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_explicit.sol @@ -0,0 +1,13 @@ +contract C { + function f() public pure { + bytes1 b1 = bytes1(hex"01"); + bytes1 b2 = bytes1(hex"FF"); + bytes2 b3 = bytes2(hex"0100"); + bytes2 b4 = bytes2(hex"FFFF"); + bytes3 b5 = bytes3(hex"010000"); + bytes3 b6 = bytes3(hex"FFFFFF"); + bytes4 b7 = bytes4(hex"01000000"); + bytes4 b8 = bytes4(hex"FFFFFFFF"); + b1; b2; b3; b4; b5; b6; b7; b8; + } +} diff --git a/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_implicit.sol b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_implicit.sol new file mode 100644 index 000000000..dbf4a4cf0 --- /dev/null +++ b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_same_size_implicit.sol @@ -0,0 +1,13 @@ +contract C { + function f() public pure { + bytes1 b1 = hex"01"; + bytes1 b2 = hex"FF"; + bytes2 b3 = hex"0100"; + bytes2 b4 = hex"FFFF"; + bytes3 b5 = hex"010000"; + bytes3 b6 = hex"FFFFFF"; + bytes4 b7 = hex"01000000"; + bytes4 b8 = hex"FFFFFFFF"; + b1; b2; b3; b4; b5; b6; b7; b8; + } +} diff --git a/test/libsolidity/syntaxTests/types/zero_literal_to_bytesXX_explicit.sol b/test/libsolidity/syntaxTests/types/zero_literal_to_bytesNN_explicit.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/zero_literal_to_bytesXX_explicit.sol rename to test/libsolidity/syntaxTests/types/zero_literal_to_bytesNN_explicit.sol diff --git a/test/libsolidity/syntaxTests/types/zero_literal_to_bytesXX_implicit.sol b/test/libsolidity/syntaxTests/types/zero_literal_to_bytesNN_implicit.sol similarity index 100% rename from test/libsolidity/syntaxTests/types/zero_literal_to_bytesXX_implicit.sol rename to test/libsolidity/syntaxTests/types/zero_literal_to_bytesNN_implicit.sol From 8eba66daf9cd9e50d52d838a3ec0dc32ce95fa65 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 23 Sep 2020 17:55:55 +0200 Subject: [PATCH 13/19] Extract boost smt and remove unused tests --- test/CMakeLists.txt | 3 - test/InteractiveTests.h | 1 - test/boostTest.cpp | 3 - test/libsolidity/SMTChecker.cpp | 143 -------------- test/libsolidity/SMTCheckerJSONTest.cpp | 176 ------------------ test/libsolidity/SMTCheckerJSONTest.h | 48 ----- .../smtCheckerTests/imports/import_base.sol | 25 +++ .../imports/import_library.sol | 19 ++ test/tools/CMakeLists.txt | 1 - 9 files changed, 44 insertions(+), 375 deletions(-) delete mode 100644 test/libsolidity/SMTChecker.cpp delete mode 100644 test/libsolidity/SMTCheckerJSONTest.cpp delete mode 100644 test/libsolidity/SMTCheckerJSONTest.h create mode 100644 test/libsolidity/smtCheckerTests/imports/import_base.sol create mode 100644 test/libsolidity/smtCheckerTests/imports/import_library.sol diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 3567f20ce..052929c09 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -79,9 +79,6 @@ set(libsolidity_sources libsolidity/SemanticTest.cpp libsolidity/SemanticTest.h libsolidity/SemVerMatcher.cpp - libsolidity/SMTChecker.cpp - libsolidity/SMTCheckerJSONTest.cpp - libsolidity/SMTCheckerJSONTest.h libsolidity/SMTCheckerTest.cpp libsolidity/SMTCheckerTest.h libsolidity/SolidityCompiler.cpp diff --git a/test/InteractiveTests.h b/test/InteractiveTests.h index 7ecc8de5e..2daf716aa 100644 --- a/test/InteractiveTests.h +++ b/test/InteractiveTests.h @@ -25,7 +25,6 @@ #include #include #include -#include #include #include #include diff --git a/test/boostTest.cpp b/test/boostTest.cpp index 18a5a2ea8..81aae19ab 100644 --- a/test/boostTest.cpp +++ b/test/boostTest.cpp @@ -205,9 +205,6 @@ test_suite* init_unit_test_suite( int /*argc*/, char* /*argv*/[] ) removeTestSuite(suite); } - if (solidity::test::CommonOptions::get().disableSMT) - removeTestSuite("SMTChecker"); - return nullptr; } diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp deleted file mode 100644 index a7347a21a..000000000 --- a/test/libsolidity/SMTChecker.cpp +++ /dev/null @@ -1,143 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see . -*/ -/** - * Unit tests for the SMT checker. - */ - -#include -#include - -#include - -#include - -using namespace std; -using namespace solidity::langutil; - -namespace solidity::frontend::test -{ - -class SMTCheckerFramework: public AnalysisFramework -{ -protected: - std::pair - parseAnalyseAndReturnError( - std::string const& _source, - bool _reportWarnings = false, - bool _insertLicenseAndVersionPragma = true, - bool _allowMultipleErrors = false, - bool _allowRecoveryErrors = false - ) override - { - return AnalysisFramework::parseAnalyseAndReturnError( - "pragma experimental SMTChecker;\n" + _source, - _reportWarnings, - _insertLicenseAndVersionPragma, - _allowMultipleErrors, - _allowRecoveryErrors - ); - } -}; - -BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) - -BOOST_AUTO_TEST_CASE(import_base, *boost::unit_test::label("no_options")) -{ - CompilerStack c; - c.setSources({ - {"base", R"( - pragma solidity >=0.0; - contract Base { - uint x; - address a; - function f() internal returns (uint) { - a = address(this); - ++x; - return 2; - } - } - )"}, - {"der", R"( - pragma solidity >=0.0; - pragma experimental SMTChecker; - import "base"; - contract Der is Base { - function g(uint y) public { - x += f(); - assert(y > x); - } - } - )"} - }); - c.setEVMVersion(solidity::test::CommonOptions::get().evmVersion()); - BOOST_CHECK(c.compile()); - - unsigned asserts = 0; - for (auto const& e: c.errors()) - { - string const* msg = e->comment(); - BOOST_REQUIRE(msg); - if (msg->find("Assertion violation") != string::npos) - ++asserts; - } - BOOST_CHECK_EQUAL(asserts, 1); -} - -BOOST_AUTO_TEST_CASE(import_library, *boost::unit_test::label("no_options")) -{ - CompilerStack c; - c.setSources({ - {"lib", R"( - pragma solidity >=0.0; - library L { - uint constant one = 1; - function f() internal pure returns (uint) { - return one; - } - } - )"}, - {"c", R"( - pragma solidity >=0.0; - pragma experimental SMTChecker; - import "lib"; - contract C { - function g(uint x) public pure { - uint y = L.f(); - assert(x > y); - } - } - )"} - }); - c.setEVMVersion(solidity::test::CommonOptions::get().evmVersion()); - BOOST_CHECK(c.compile()); - - unsigned asserts = 0; - for (auto const& e: c.errors()) - { - string const* msg = e->comment(); - BOOST_REQUIRE(msg); - if (msg->find("Assertion violation") != string::npos) - ++asserts; - } - BOOST_CHECK_EQUAL(asserts, 1); - -} - - -BOOST_AUTO_TEST_SUITE_END() - -} diff --git a/test/libsolidity/SMTCheckerJSONTest.cpp b/test/libsolidity/SMTCheckerJSONTest.cpp deleted file mode 100644 index ca6608905..000000000 --- a/test/libsolidity/SMTCheckerJSONTest.cpp +++ /dev/null @@ -1,176 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#include -#include - -#include -#include -#include -#include - -#include -#include -#include -#include -#include - -#include -#include -#include -#include - -using namespace std; -using namespace solidity; -using namespace solidity::frontend; -using namespace solidity::frontend::test; -using namespace solidity::util; -using namespace solidity::util::formatting; -using namespace boost::unit_test; - -SMTCheckerJSONTest::SMTCheckerJSONTest(string const& _filename, langutil::EVMVersion _evmVersion) -: SyntaxTest(_filename, _evmVersion) -{ - if (!boost::algorithm::ends_with(_filename, ".sol")) - BOOST_THROW_EXCEPTION(runtime_error("Invalid test contract file name: \"" + _filename + "\".")); - - string jsonFilename = _filename.substr(0, _filename.size() - 4) + ".json"; - if ( - !jsonParseStrict(readFileAsString(jsonFilename), m_smtResponses) || - !m_smtResponses.isObject() - ) - BOOST_THROW_EXCEPTION(runtime_error("Invalid JSON file.")); - - if (ModelChecker::availableSolvers().none()) - m_shouldRun = false; -} - -TestCase::TestResult SMTCheckerJSONTest::run(ostream& _stream, string const& _linePrefix, bool _formatted) -{ - StandardCompiler compiler; - - // Run the compiler and retrieve the smtlib2queries (1st run) - string preamble = "pragma solidity >=0.0;\n// SPDX-License-Identifier: GPL-3.0\n"; - Json::Value input = buildJson(preamble); - Json::Value result = compiler.compile(input); - - // This is the list of query hashes requested by the 1st run - vector outHashes = hashesFromJson(result, "auxiliaryInputRequested", "smtlib2queries"); - - // This is the list of responses provided in the test - string auxInput("auxiliaryInput"); - if (!m_smtResponses.isMember(auxInput)) - BOOST_THROW_EXCEPTION(runtime_error("JSON file does not contain field \"auxiliaryInput\".")); - - vector inHashes = hashesFromJson(m_smtResponses, auxInput, "smtlib2responses"); - - // Ensure that the provided list matches the requested one - if (outHashes != inHashes) - BOOST_THROW_EXCEPTION(runtime_error( - "SMT query hashes differ: " + - boost::algorithm::join(outHashes, ", ") + - " x " + - boost::algorithm::join(inHashes, ", ") - )); - - // Rerun the compiler with the provided hashed (2nd run) - input[auxInput] = m_smtResponses[auxInput]; - Json::Value endResult = compiler.compile(input); - - if (endResult.isMember("errors") && endResult["errors"].isArray()) - { - Json::Value const& errors = endResult["errors"]; - for (auto const& error: errors) - { - if ( - !error.isMember("type") || - !error["type"].isString() - ) - BOOST_THROW_EXCEPTION(runtime_error("Error must have a type.")); - if ( - !error.isMember("message") || - !error["message"].isString() - ) - BOOST_THROW_EXCEPTION(runtime_error("Error must have a message.")); - if (!error.isMember("sourceLocation")) - continue; - Json::Value const& location = error["sourceLocation"]; - if ( - !location.isMember("start") || - !location["start"].isInt() || - !location.isMember("end") || - !location["end"].isInt() - ) - BOOST_THROW_EXCEPTION(runtime_error("Error must have a SourceLocation with start and end.")); - size_t start = location["start"].asUInt(); - size_t end = location["end"].asUInt(); - std::string sourceName; - if (location.isMember("source") && location["source"].isString()) - sourceName = location["source"].asString(); - if (start >= preamble.size()) - start -= preamble.size(); - if (end >= preamble.size()) - end -= preamble.size(); - m_errorList.emplace_back(SyntaxTestError{ - error["type"].asString(), - error["errorId"].isNull() ? nullopt : optional(langutil::ErrorId{error["errorId"].asUInt()}), - error["message"].asString(), - sourceName, - static_cast(start), - static_cast(end) - }); - } - } - - return conclude(_stream, _linePrefix, _formatted); -} - -vector SMTCheckerJSONTest::hashesFromJson(Json::Value const& _jsonObj, string const& _auxInput, string const& _smtlib) -{ - vector hashes; - Json::Value const& auxInputs = _jsonObj[_auxInput]; - if (!!auxInputs) - { - Json::Value const& smtlib = auxInputs[_smtlib]; - if (!!smtlib) - for (auto const& hashString: smtlib.getMemberNames()) - hashes.push_back(hashString); - } - return hashes; -} - -Json::Value SMTCheckerJSONTest::buildJson(string const& _extra) -{ - string language = "\"language\": \"Solidity\""; - string sources = " \"sources\": { "; - bool first = true; - for (auto [sourceName, sourceContent]: m_sources) - { - string sourceObj = "{ \"content\": \"" + _extra + sourceContent + "\"}"; - if (!first) - sources += ", "; - sources += "\"" + sourceName + "\": " + sourceObj; - first = false; - } - sources += "}"; - string input = "{" + language + ", " + sources + "}"; - Json::Value source; - if (!jsonParseStrict(input, source)) - BOOST_THROW_EXCEPTION(runtime_error("Could not build JSON from string: " + input)); - return source; -} diff --git a/test/libsolidity/SMTCheckerJSONTest.h b/test/libsolidity/SMTCheckerJSONTest.h deleted file mode 100644 index 6de7f36c9..000000000 --- a/test/libsolidity/SMTCheckerJSONTest.h +++ /dev/null @@ -1,48 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see . -*/ -// SPDX-License-Identifier: GPL-3.0 - -#pragma once - -#include - -#include - -#include - -namespace solidity::frontend::test -{ - -class SMTCheckerJSONTest: public SyntaxTest -{ -public: - static std::unique_ptr create(Config const& _config) - { - return std::make_unique(_config.filename, _config.evmVersion); - } - SMTCheckerJSONTest(std::string const& _filename, langutil::EVMVersion _evmVersion); - - TestResult run(std::ostream& _stream, std::string const& _linePrefix = "", bool _formatted = false) override; - -private: - std::vector hashesFromJson(Json::Value const& _jsonObj, std::string const& _auxInput, std::string const& _smtlib); - Json::Value buildJson(std::string const& _extra); - - Json::Value m_smtResponses; -}; - -} diff --git a/test/libsolidity/smtCheckerTests/imports/import_base.sol b/test/libsolidity/smtCheckerTests/imports/import_base.sol new file mode 100644 index 000000000..a65f8b3f5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/import_base.sol @@ -0,0 +1,25 @@ +==== Source: base ==== +contract Base { + uint x; + address a; + function f() internal returns (uint) { + a = address(this); + ++x; + return 2; + } +} +==== Source: der ==== +pragma experimental SMTChecker; +import "base"; +contract Der is Base { + function g(uint y) public { + x += f(); + assert(y > x); + } +} +// ---- +// Warning 1218: (der:101-109): Error trying to invoke SMT solver. +// Warning 6328: (der:113-126): Assertion violation happens here. +// Warning 2661: (base:100-103): Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 2661: (der:101-109): Overflow (resulting value larger than 2**256 - 1) happens here. +// Warning 2661: (base:100-103): Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/import_library.sol b/test/libsolidity/smtCheckerTests/imports/import_library.sol new file mode 100644 index 000000000..b6c6702bc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/imports/import_library.sol @@ -0,0 +1,19 @@ +==== Source: c ==== +pragma experimental SMTChecker; +import "lib"; +contract C { + function g(uint x) public pure { + uint y = L.f(); + assert(x > y); + } +} +==== Source: lib ==== +library L { + uint constant one = 1; + function f() internal pure returns (uint) { + return one; + } +} +// ---- +// Warning 6328: (c:113-126): Assertion violation happens here. +// Warning 8364: (c:104-105): Assertion checker does not yet implement type type(library L) diff --git a/test/tools/CMakeLists.txt b/test/tools/CMakeLists.txt index c8add4ce7..dc0d58bce 100644 --- a/test/tools/CMakeLists.txt +++ b/test/tools/CMakeLists.txt @@ -31,7 +31,6 @@ add_executable(isoltest ../libsolidity/ABIJsonTest.cpp ../libsolidity/ASTJSONTest.cpp ../libsolidity/SMTCheckerTest.cpp - ../libsolidity/SMTCheckerJSONTest.cpp ../libyul/Common.cpp ../libyul/EwasmTranslationTest.cpp ../libyul/FunctionSideEffects.cpp From 0e5abbd4a9ae5dd2a5daf175fe078f9faa533583 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Wed, 23 Sep 2020 13:21:30 +0100 Subject: [PATCH 14/19] Display location of invalid UTF-8 sequence in unicode literals in SyntaxChecker --- Changelog.md | 1 + libsolidity/analysis/SyntaxChecker.cpp | 5 +++-- .../libsolidity/syntaxTests/string/invalid_utf8_sequence.sol | 2 +- 3 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Changelog.md b/Changelog.md index be82d098b..579613841 100644 --- a/Changelog.md +++ b/Changelog.md @@ -12,6 +12,7 @@ Compiler Features: * 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)``. + * Type Checker: Report position of first invalid UTF-8 sequence in ``unicode""`` literals. * Type Checker: More detailed error messages why implicit conversions fail. * Type Checker: Explain why oversized hex string literals can not be explicitly converted to a shorter ``bytesNN`` type. * Yul Optimizer: Prune unused parameters in functions. diff --git a/libsolidity/analysis/SyntaxChecker.cpp b/libsolidity/analysis/SyntaxChecker.cpp index 670939321..076592053 100644 --- a/libsolidity/analysis/SyntaxChecker.cpp +++ b/libsolidity/analysis/SyntaxChecker.cpp @@ -219,11 +219,12 @@ bool SyntaxChecker::visit(Throw const& _throwStatement) bool SyntaxChecker::visit(Literal const& _literal) { - if ((_literal.token() == Token::UnicodeStringLiteral) && !validateUTF8(_literal.value())) + size_t invalidSequence; + if ((_literal.token() == Token::UnicodeStringLiteral) && !validateUTF8(_literal.value(), invalidSequence)) m_errorReporter.syntaxError( 8452_error, _literal.location(), - "Invalid UTF-8 sequence found" + "Contains invalid UTF-8 sequence at position " + toString(invalidSequence) + "." ); if (_literal.token() != Token::Number) diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol index f5d5077f2..7655757a7 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol @@ -2,5 +2,5 @@ contract C { string s = unicode"À"; } // ---- -// SyntaxError 8452: (28-38): Invalid UTF-8 sequence found +// SyntaxError 8452: (28-38): Contains invalid UTF-8 sequence at position 0. // TypeError 7407: (28-38): Type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. From a154594de6b6b3b0fb5e80f1603e5783aeb820f9 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Wed, 23 Sep 2020 13:53:56 +0100 Subject: [PATCH 15/19] Display string literal as hex in error messages if it is not printable ASCII --- libsolidity/ast/Types.cpp | 19 ++++++++++++++++--- test/libsolidity/ASTJSON/non_utf8.json | 2 +- test/libsolidity/ASTJSON/non_utf8_legacy.json | 2 +- test/libsolidity/ASTJSON/unicode.json | 2 +- test/libsolidity/ASTJSON/unicode_legacy.json | 2 +- .../string/invalid_utf8_explicit_string.sol | 2 +- .../string/invalid_utf8_hex_string.sol | 2 +- .../string/invalid_utf8_implicit_string.sol | 2 +- .../string/invalid_utf8_sequence.sol | 2 +- ...code_escape_literals_invalid_codepoint.sol | 2 +- .../bytesNN_with_oversized_hex_string.sol | 2 +- ...ing_to_bytesNN_different_size_explicit.sol | 8 ++++---- 12 files changed, 30 insertions(+), 17 deletions(-) diff --git a/libsolidity/ast/Types.cpp b/libsolidity/ast/Types.cpp index 7335ba548..42ff01213 100644 --- a/libsolidity/ast/Types.cpp +++ b/libsolidity/ast/Types.cpp @@ -1382,12 +1382,25 @@ bool StringLiteralType::operator==(Type const& _other) const std::string StringLiteralType::toString(bool) const { + auto isPrintableASCII = [](string const& s) + { + for (auto c: s) + { + if (static_cast(c) <= 0x1f || static_cast(c) >= 0x7f) + return false; + } + return true; + }; + + string ret = isPrintableASCII(m_value) ? + ("literal_string \"" + m_value + "\"") : + ("literal_string hex\"" + util::toHex(util::asBytes(m_value)) + "\""); + size_t invalidSequence; - if (!util::validateUTF8(m_value, invalidSequence)) - return "literal_string (contains invalid UTF-8 sequence at position " + util::toString(invalidSequence) + ")"; + ret += " (contains invalid UTF-8 sequence at position " + util::toString(invalidSequence) + ")"; - return "literal_string \"" + m_value + "\""; + return ret; } TypePointer StringLiteralType::mobileType() const diff --git a/test/libsolidity/ASTJSON/non_utf8.json b/test/libsolidity/ASTJSON/non_utf8.json index 98db4273f..eab03546d 100644 --- a/test/libsolidity/ASTJSON/non_utf8.json +++ b/test/libsolidity/ASTJSON/non_utf8.json @@ -86,7 +86,7 @@ "typeDescriptions": { "typeIdentifier": "t_stringliteral_8b1a944cf13a9a1c08facb2c9e98623ef3254d2ddb48113885c3e8e97fec8db9", - "typeString": "literal_string (contains invalid UTF-8 sequence at position 0)" + "typeString": "literal_string hex\"ff\" (contains invalid UTF-8 sequence at position 0)" } }, "nodeType": "VariableDeclarationStatement", diff --git a/test/libsolidity/ASTJSON/non_utf8_legacy.json b/test/libsolidity/ASTJSON/non_utf8_legacy.json index d9430c82d..566d29c4b 100644 --- a/test/libsolidity/ASTJSON/non_utf8_legacy.json +++ b/test/libsolidity/ASTJSON/non_utf8_legacy.json @@ -131,7 +131,7 @@ "isPure": true, "lValueRequested": false, "token": "hexString", - "type": "literal_string (contains invalid UTF-8 sequence at position 0)" + "type": "literal_string hex\"ff\" (contains invalid UTF-8 sequence at position 0)" }, "id": 5, "name": "Literal", diff --git a/test/libsolidity/ASTJSON/unicode.json b/test/libsolidity/ASTJSON/unicode.json index 81c8ad0da..219d89500 100644 --- a/test/libsolidity/ASTJSON/unicode.json +++ b/test/libsolidity/ASTJSON/unicode.json @@ -86,7 +86,7 @@ "typeDescriptions": { "typeIdentifier": "t_stringliteral_cd7a99177cebb3d14b8cc54e313dbf76867c71cd6fbb9a33ce3870dc80e9992b", - "typeString": "literal_string \"Hello \ud83d\ude03\"" + "typeString": "literal_string hex\"48656c6c6f20f09f9883\"" }, "value": "Hello \ud83d\ude03" }, diff --git a/test/libsolidity/ASTJSON/unicode_legacy.json b/test/libsolidity/ASTJSON/unicode_legacy.json index 22976f6f9..f3e4ad321 100644 --- a/test/libsolidity/ASTJSON/unicode_legacy.json +++ b/test/libsolidity/ASTJSON/unicode_legacy.json @@ -131,7 +131,7 @@ "isPure": true, "lValueRequested": false, "token": "unicodeString", - "type": "literal_string \"Hello \ud83d\ude03\"", + "type": "literal_string hex\"48656c6c6f20f09f9883\"", "value": "Hello \ud83d\ude03" }, "id": 5, diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol index b9a8c5279..4084c99e9 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol @@ -2,4 +2,4 @@ contract C { string s = string("\xa0\x00"); } // ---- -// TypeError 9640: (28-46): Explicit type conversion not allowed from "literal_string (contains invalid UTF-8 sequence at position 0)" to "string memory". +// TypeError 9640: (28-46): Explicit type conversion not allowed from "literal_string hex"a000" (contains invalid UTF-8 sequence at position 0)" to "string memory". diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol index d72ee5af0..d25886c91 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol @@ -2,4 +2,4 @@ contract C { string s = hex"a000"; } // ---- -// TypeError 7407: (28-37): Type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. +// TypeError 7407: (28-37): Type literal_string hex"a000" (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol index 3cf3361f3..6b630249e 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol @@ -2,4 +2,4 @@ contract C { string s = "\xa0\x00"; } // ---- -// TypeError 7407: (28-38): Type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. +// TypeError 7407: (28-38): Type literal_string hex"a000" (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol index 7655757a7..05b0f223c 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol @@ -3,4 +3,4 @@ contract C { } // ---- // SyntaxError 8452: (28-38): Contains invalid UTF-8 sequence at position 0. -// TypeError 7407: (28-38): Type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. +// TypeError 7407: (28-38): Type literal_string hex"c0" (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. diff --git a/test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol b/test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol index 46a0de5f4..f30f26fe4 100644 --- a/test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol +++ b/test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol @@ -4,4 +4,4 @@ contract test { } } // ---- -// TypeError 6359: (86-92): Return argument type literal_string (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type (type of first return variable) string memory. +// TypeError 6359: (86-92): Return argument type literal_string hex"c1" (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type (type of first return variable) string memory. diff --git a/test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol b/test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol index a76c4ec53..9412a7882 100644 --- a/test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol +++ b/test/libsolidity/syntaxTests/types/bytesNN_with_oversized_hex_string.sol @@ -4,4 +4,4 @@ contract C { } } // ---- -// TypeError 9640: (76-95): Explicit type conversion not allowed from "literal_string "4V"" to "bytes2". Literal is larger than the type. +// TypeError 9640: (76-95): Explicit type conversion not allowed from "literal_string hex"123456"" to "bytes2". Literal is larger than the type. diff --git a/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol index 829199bf2..3fa37ddf1 100644 --- a/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol +++ b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol @@ -14,7 +14,7 @@ contract C { } } // ---- -// TypeError 9640: (92-109): Explicit type conversion not allowed from "literal_string "4"" to "bytes1". Literal is larger than the type. -// TypeError 9640: (198-217): Explicit type conversion not allowed from "literal_string "4V"" to "bytes2". Literal is larger than the type. -// TypeError 9640: (310-331): Explicit type conversion not allowed from "literal_string "4Vx"" to "bytes3". Literal is larger than the type. -// TypeError 9640: (430-453): Explicit type conversion not allowed from "literal_string (contains invalid UTF-8 sequence at position 4)" to "bytes4". Literal is larger than the type. +// TypeError 9640: (92-109): Explicit type conversion not allowed from "literal_string hex"1234"" to "bytes1". Literal is larger than the type. +// TypeError 9640: (198-217): Explicit type conversion not allowed from "literal_string hex"123456"" to "bytes2". Literal is larger than the type. +// TypeError 9640: (310-331): Explicit type conversion not allowed from "literal_string hex"12345678"" to "bytes3". Literal is larger than the type. +// TypeError 9640: (430-453): Explicit type conversion not allowed from "literal_string hex"1234567890" (contains invalid UTF-8 sequence at position 4)" to "bytes4". Literal is larger than the type. From e54110ff173f8903acc098f25a416085d9e507ae Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Wed, 23 Sep 2020 15:04:22 +0100 Subject: [PATCH 16/19] Return UTF-8 error in BoolResult and remove it from string type --- libsolidity/ast/Types.cpp | 20 ++++++++++--------- test/libsolidity/ASTJSON/non_utf8.json | 2 +- test/libsolidity/ASTJSON/non_utf8_legacy.json | 2 +- .../string/invalid_utf8_explicit_string.sol | 2 +- .../string/invalid_utf8_hex_string.sol | 2 +- .../string/invalid_utf8_implicit_string.sol | 2 +- .../string/invalid_utf8_sequence.sol | 2 +- ...code_escape_literals_invalid_codepoint.sol | 2 +- ...ing_to_bytesNN_different_size_explicit.sol | 2 +- 9 files changed, 19 insertions(+), 17 deletions(-) diff --git a/libsolidity/ast/Types.cpp b/libsolidity/ast/Types.cpp index 42ff01213..a874bab9c 100644 --- a/libsolidity/ast/Types.cpp +++ b/libsolidity/ast/Types.cpp @@ -1357,11 +1357,19 @@ BoolResult StringLiteralType::isImplicitlyConvertibleTo(Type const& _convertTo) return true; } else if (auto arrayType = dynamic_cast(&_convertTo)) + { + size_t invalidSequence; + if (arrayType->isString() && !util::validateUTF8(value(), invalidSequence)) + return BoolResult::err( + "Contains invalid UTF-8 sequence at position " + + util::toString(invalidSequence) + + "." + ); return arrayType->location() != DataLocation::CallData && arrayType->isByteArray() && - !(arrayType->dataStoredIn(DataLocation::Storage) && arrayType->isPointer()) && - !(arrayType->isString() && !util::validateUTF8(value())); + !(arrayType->dataStoredIn(DataLocation::Storage) && arrayType->isPointer()); + } else return false; } @@ -1392,15 +1400,9 @@ std::string StringLiteralType::toString(bool) const return true; }; - string ret = isPrintableASCII(m_value) ? + return isPrintableASCII(m_value) ? ("literal_string \"" + m_value + "\"") : ("literal_string hex\"" + util::toHex(util::asBytes(m_value)) + "\""); - - size_t invalidSequence; - if (!util::validateUTF8(m_value, invalidSequence)) - ret += " (contains invalid UTF-8 sequence at position " + util::toString(invalidSequence) + ")"; - - return ret; } TypePointer StringLiteralType::mobileType() const diff --git a/test/libsolidity/ASTJSON/non_utf8.json b/test/libsolidity/ASTJSON/non_utf8.json index eab03546d..1a1ea5b96 100644 --- a/test/libsolidity/ASTJSON/non_utf8.json +++ b/test/libsolidity/ASTJSON/non_utf8.json @@ -86,7 +86,7 @@ "typeDescriptions": { "typeIdentifier": "t_stringliteral_8b1a944cf13a9a1c08facb2c9e98623ef3254d2ddb48113885c3e8e97fec8db9", - "typeString": "literal_string hex\"ff\" (contains invalid UTF-8 sequence at position 0)" + "typeString": "literal_string hex\"ff\"" } }, "nodeType": "VariableDeclarationStatement", diff --git a/test/libsolidity/ASTJSON/non_utf8_legacy.json b/test/libsolidity/ASTJSON/non_utf8_legacy.json index 566d29c4b..72b514fda 100644 --- a/test/libsolidity/ASTJSON/non_utf8_legacy.json +++ b/test/libsolidity/ASTJSON/non_utf8_legacy.json @@ -131,7 +131,7 @@ "isPure": true, "lValueRequested": false, "token": "hexString", - "type": "literal_string hex\"ff\" (contains invalid UTF-8 sequence at position 0)" + "type": "literal_string hex\"ff\"" }, "id": 5, "name": "Literal", diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol index 4084c99e9..3ad1c4b56 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_explicit_string.sol @@ -2,4 +2,4 @@ contract C { string s = string("\xa0\x00"); } // ---- -// TypeError 9640: (28-46): Explicit type conversion not allowed from "literal_string hex"a000" (contains invalid UTF-8 sequence at position 0)" to "string memory". +// TypeError 9640: (28-46): Explicit type conversion not allowed from "literal_string hex"a000"" to "string memory". Contains invalid UTF-8 sequence at position 0. diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol index d25886c91..a089137dc 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_hex_string.sol @@ -2,4 +2,4 @@ contract C { string s = hex"a000"; } // ---- -// TypeError 7407: (28-37): Type literal_string hex"a000" (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. +// TypeError 7407: (28-37): Type literal_string hex"a000" is not implicitly convertible to expected type string storage ref. Contains invalid UTF-8 sequence at position 0. diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol index 6b630249e..98d83e1d4 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_implicit_string.sol @@ -2,4 +2,4 @@ contract C { string s = "\xa0\x00"; } // ---- -// TypeError 7407: (28-38): Type literal_string hex"a000" (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. +// TypeError 7407: (28-38): Type literal_string hex"a000" is not implicitly convertible to expected type string storage ref. Contains invalid UTF-8 sequence at position 0. diff --git a/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol b/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol index 05b0f223c..f8df14ca5 100644 --- a/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol +++ b/test/libsolidity/syntaxTests/string/invalid_utf8_sequence.sol @@ -3,4 +3,4 @@ contract C { } // ---- // SyntaxError 8452: (28-38): Contains invalid UTF-8 sequence at position 0. -// TypeError 7407: (28-38): Type literal_string hex"c0" (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type string storage ref. +// TypeError 7407: (28-38): Type literal_string hex"c0" is not implicitly convertible to expected type string storage ref. Contains invalid UTF-8 sequence at position 0. diff --git a/test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol b/test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol index f30f26fe4..975c5ac39 100644 --- a/test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol +++ b/test/libsolidity/syntaxTests/string/unicode_escape_literals_invalid_codepoint.sol @@ -4,4 +4,4 @@ contract test { } } // ---- -// TypeError 6359: (86-92): Return argument type literal_string hex"c1" (contains invalid UTF-8 sequence at position 0) is not implicitly convertible to expected type (type of first return variable) string memory. +// TypeError 6359: (86-92): Return argument type literal_string hex"c1" is not implicitly convertible to expected type (type of first return variable) string memory. Contains invalid UTF-8 sequence at position 0. diff --git a/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol index 3fa37ddf1..18b628cb6 100644 --- a/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol +++ b/test/libsolidity/syntaxTests/types/hex_string_to_bytesNN_different_size_explicit.sol @@ -17,4 +17,4 @@ contract C { // TypeError 9640: (92-109): Explicit type conversion not allowed from "literal_string hex"1234"" to "bytes1". Literal is larger than the type. // TypeError 9640: (198-217): Explicit type conversion not allowed from "literal_string hex"123456"" to "bytes2". Literal is larger than the type. // TypeError 9640: (310-331): Explicit type conversion not allowed from "literal_string hex"12345678"" to "bytes3". Literal is larger than the type. -// TypeError 9640: (430-453): Explicit type conversion not allowed from "literal_string hex"1234567890" (contains invalid UTF-8 sequence at position 4)" to "bytes4". Literal is larger than the type. +// TypeError 9640: (430-453): Explicit type conversion not allowed from "literal_string hex"1234567890"" to "bytes4". Literal is larger than the type. From 5917fd82b3ca4cab5f817f78b8da8ebe409dd02e Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 23 Sep 2020 16:51:52 +0200 Subject: [PATCH 17/19] [SMTChecker] Do not throw when counterexample is not available (older z3 versions) --- libsmtutil/Z3CHCInterface.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/libsmtutil/Z3CHCInterface.cpp b/libsmtutil/Z3CHCInterface.cpp index 9ea155621..2e11c7d0a 100644 --- a/libsmtutil/Z3CHCInterface.cpp +++ b/libsmtutil/Z3CHCInterface.cpp @@ -142,14 +142,17 @@ instead of a path. */ CHCSolverInterface::CexGraph Z3CHCInterface::cexGraph(z3::expr const& _proof) { - CexGraph graph; - /// The root fact of the refutation proof is `false`. /// The node itself is not a hyper resolution, so we need to /// extract the `query` hyper resolution node from the /// `false` node (the first child). - smtAssert(_proof.is_app(), ""); - smtAssert(fact(_proof).decl().decl_kind() == Z3_OP_FALSE, ""); + /// The proof has the shape above for z3 >=4.8.8. + /// If an older version is used, this check will fail and no + /// counterexample will be generated. + if (!_proof.is_app() || fact(_proof).decl().decl_kind() != Z3_OP_FALSE) + return {}; + + CexGraph graph; stack proofStack; proofStack.push(_proof.arg(0)); From ebb6f61506c1ad25d75baf45aaeebffac291e3ed Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 23 Sep 2020 19:28:47 +0200 Subject: [PATCH 18/19] [SMTChecker] Decrease rlimit --- libsmtutil/Z3Interface.h | 2 +- .../loops/while_loop_array_assignment_storage_storage.sol | 2 ++ .../smtCheckerTests/operators/compound_bitwise_or_int_1.sol | 1 + .../smtCheckerTests/operators/compound_bitwise_or_uint_1.sol | 1 + .../smtCheckerTests/operators/compound_bitwise_or_uint_2.sol | 3 ++- .../smtCheckerTests/operators/compound_bitwise_or_uint_3.sol | 2 ++ 6 files changed, 9 insertions(+), 2 deletions(-) diff --git a/libsmtutil/Z3Interface.h b/libsmtutil/Z3Interface.h index 23534fd75..a44bfafcd 100644 --- a/libsmtutil/Z3Interface.h +++ b/libsmtutil/Z3Interface.h @@ -49,7 +49,7 @@ public: // Z3 "basic resources" limit. // This is used to make the runs more deterministic and platform/machine independent. - static int const resourceLimit = 12500000; + static int const resourceLimit = 1000000; private: void declareFunction(std::string const& _name, Sort const& _sort); diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol index 1eceace61..5d2bb0f0d 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol @@ -22,5 +22,7 @@ contract LoopFor2 { } // ---- // Warning 1218: (229-234): Error trying to invoke SMT solver. +// Warning 1218: (296-316): Error trying to invoke SMT solver. // Warning 6328: (320-339): Assertion violation happens here. // Warning 6328: (343-362): Assertion violation happens here. +// Warning 4661: (296-316): Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol index e25ae354d..aaeb0d10a 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_int_1.sol @@ -9,3 +9,4 @@ contract C { } } // ---- +// Warning 1218: (174-212): Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol index 790d30a76..b332e5bb4 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_1.sol @@ -9,3 +9,4 @@ contract C { } } // ---- +// Warning 1218: (166-183): Error trying to invoke SMT solver. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol index 04d907cf4..de45cd2ac 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol @@ -11,4 +11,5 @@ contract C { } } // ---- -// Warning 6328: (173-192): Assertion violation happens here. +// Warning 1218: (173-192): Error trying to invoke SMT solver. +// Warning 7812: (173-192): Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol index 8132ae773..71a6cbac7 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_3.sol @@ -10,3 +10,5 @@ contract C { } } // ---- +// Warning 1218: (157-172): Error trying to invoke SMT solver. +// Warning 7812: (157-172): Assertion violation might happen here. From 11fc924d231a3d9d70e0a192c55b6567c81fa053 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 23 Sep 2020 17:33:56 +0200 Subject: [PATCH 19/19] Split SMTCheckerTests in CI --- .circleci/soltest_all.sh | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/.circleci/soltest_all.sh b/.circleci/soltest_all.sh index 7b1fb053b..78cc1137d 100755 --- a/.circleci/soltest_all.sh +++ b/.circleci/soltest_all.sh @@ -30,7 +30,7 @@ REPODIR="$(realpath $(dirname $0)/..)" EVM_VALUES=(homestead byzantium constantinople petersburg istanbul) OPTIMIZE_VALUES=(0 1) -STEPS=$(( 1 + ${#EVM_VALUES[@]} * ${#OPTIMIZE_VALUES[@]} )) +STEPS=$(( 2 + ${#EVM_VALUES[@]} * ${#OPTIMIZE_VALUES[@]} )) if (( $CIRCLE_NODE_TOTAL )) && (( $CIRCLE_NODE_TOTAL > 1 )) then @@ -57,7 +57,12 @@ echo "Running steps $RUN_STEPS..." STEP=1 -[[ " $RUN_STEPS " =~ " $STEP " ]] && EVM=istanbul OPTIMIZE=1 ABI_ENCODER_V2=1 "${REPODIR}/.circleci/soltest.sh" +# Run SMTChecker tests separately, as the heaviest expected run. +[[ " $RUN_STEPS " =~ " $STEP " ]] && EVM=istanbul OPTIMIZE=1 ABI_ENCODER_V2=1 BOOST_TEST_ARGS="-t smtCheckerTests/*" "${REPODIR}/.circleci/soltest.sh" +STEP=$(($STEP + 1)) + +# Run without SMTChecker tests. +[[ " $RUN_STEPS " =~ " $STEP " ]] && EVM=istanbul OPTIMIZE=1 ABI_ENCODER_V2=1 BOOST_TEST_ARGS="-t !smtCheckerTests" "${REPODIR}/.circleci/soltest.sh" STEP=$(($STEP + 1)) for OPTIMIZE in ${OPTIMIZE_VALUES[@]}