From d5fb8cf58a482b1f4dd4710be86f60a597a67f5f Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 2 Aug 2019 19:46:06 +0200 Subject: [PATCH] [SMTChecker] Fix ICE compound bitwise op inside branch --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 12 ++++++++++++ .../operators/compound_bitwise_and_1.sol | 13 +++++++++++++ .../operators/compound_bitwise_or_1.sol | 13 +++++++++++++ .../operators/compound_bitwise_xor_1.sol | 13 +++++++++++++ .../smtCheckerTests/operators/compound_shl_1.sol | 13 +++++++++++++ .../smtCheckerTests/operators/compound_shr_1.sol | 13 +++++++++++++ 7 files changed, 78 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol diff --git a/Changelog.md b/Changelog.md index 197baad7e..ad7f4b6a0 100644 --- a/Changelog.md +++ b/Changelog.md @@ -20,6 +20,7 @@ Compiler Features: Bugfixes: * SMTChecker: Fix internal error when inlining functions that contain tuple expressions. * SMTChecker: Fix pointer knowledge erasing in loops. + * SMTChecker: Fix internal error when using compound bitwise assignment operators inside branches. * View/Pure Checker: Properly detect state variable access through base class. * Yul analyzer: Check availability of data objects already in analysis phase. * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b7d827a05..51904d660 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -214,10 +214,16 @@ void SMTEncoder::endVisit(Assignment const& _assignment) }; Token op = _assignment.assignmentOperator(); if (op != Token::Assign && !compoundOps.count(op)) + { + // Give it a new index anyway to keep the SSA scheme sound. + if (auto varDecl = identifierToVariable(_assignment.leftHandSide())) + m_context.newValue(*varDecl); + m_errorReporter.warning( _assignment.location(), "Assertion checker does not yet implement this assignment operator." ); + } else if (!smt::isSupportedType(_assignment.annotation().type->category())) { // Give it a new index anyway to keep the SSA scheme sound. @@ -1026,10 +1032,16 @@ void SMTEncoder::assignment( ) { if (!smt::isSupportedType(_type->category())) + { + // Give it a new index anyway to keep the SSA scheme sound. + if (auto varDecl = identifierToVariable(_left)) + m_context.newValue(*varDecl); + m_errorReporter.warning( _location, "Assertion checker does not yet implement type " + _type->toString() ); + } else if (auto varDecl = identifierToVariable(_left)) { solAssert(_right.size() == 1, ""); diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol new file mode 100644 index 000000000..2e35014e6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_and_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bool b) public pure { + uint v = 1; + if (b) + v &= 1; + assert(v == 1); + } +} +// ---- +// Warning: (106-112): Assertion checker does not yet implement this assignment operator. +// Warning: (116-130): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol new file mode 100644 index 000000000..e9d654088 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bool b) public pure { + uint v = 0; + if (b) + v |= 1; + assert(v == 1); + } +} +// ---- +// Warning: (106-112): Assertion checker does not yet implement this assignment operator. +// Warning: (116-130): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol new file mode 100644 index 000000000..a96e2efe8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_xor_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bool b) public pure { + uint v = 0; + if (b) + v ^= 1; + assert(v == 1); + } +} +// ---- +// Warning: (106-112): Assertion checker does not yet implement this assignment operator. +// Warning: (116-130): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol new file mode 100644 index 000000000..8f84e5127 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_shl_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bool b) public pure { + uint v = 1000000; + if (b) + v <<= 2; + assert(v > 0); + } +} +// ---- +// Warning: (112-119): Assertion checker does not yet implement this assignment operator. +// Warning: (123-136): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol b/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol new file mode 100644 index 000000000..8b58b79a0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/compound_shr_1.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C { + function f(bool b) public pure { + uint v = 1; + if (b) + v >>= 2; + assert(v > 0); + } +} +// ---- +// Warning: (106-113): Assertion checker does not yet implement this assignment operator. +// Warning: (117-130): Assertion violation happens here