mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
[SMTChecker] Fix ICE compound bitwise op inside branch
This commit is contained in:
parent
967ee944a5
commit
d5fb8cf58a
@ -20,6 +20,7 @@ Compiler Features:
|
|||||||
Bugfixes:
|
Bugfixes:
|
||||||
* SMTChecker: Fix internal error when inlining functions that contain tuple expressions.
|
* SMTChecker: Fix internal error when inlining functions that contain tuple expressions.
|
||||||
* SMTChecker: Fix pointer knowledge erasing in loops.
|
* 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.
|
* View/Pure Checker: Properly detect state variable access through base class.
|
||||||
* Yul analyzer: Check availability of data objects already in analysis phase.
|
* 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.
|
* Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program.
|
||||||
|
@ -214,10 +214,16 @@ void SMTEncoder::endVisit(Assignment const& _assignment)
|
|||||||
};
|
};
|
||||||
Token op = _assignment.assignmentOperator();
|
Token op = _assignment.assignmentOperator();
|
||||||
if (op != Token::Assign && !compoundOps.count(op))
|
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(
|
m_errorReporter.warning(
|
||||||
_assignment.location(),
|
_assignment.location(),
|
||||||
"Assertion checker does not yet implement this assignment operator."
|
"Assertion checker does not yet implement this assignment operator."
|
||||||
);
|
);
|
||||||
|
}
|
||||||
else if (!smt::isSupportedType(_assignment.annotation().type->category()))
|
else if (!smt::isSupportedType(_assignment.annotation().type->category()))
|
||||||
{
|
{
|
||||||
// Give it a new index anyway to keep the SSA scheme sound.
|
// Give it a new index anyway to keep the SSA scheme sound.
|
||||||
@ -1026,10 +1032,16 @@ void SMTEncoder::assignment(
|
|||||||
)
|
)
|
||||||
{
|
{
|
||||||
if (!smt::isSupportedType(_type->category()))
|
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(
|
m_errorReporter.warning(
|
||||||
_location,
|
_location,
|
||||||
"Assertion checker does not yet implement type " + _type->toString()
|
"Assertion checker does not yet implement type " + _type->toString()
|
||||||
);
|
);
|
||||||
|
}
|
||||||
else if (auto varDecl = identifierToVariable(_left))
|
else if (auto varDecl = identifierToVariable(_left))
|
||||||
{
|
{
|
||||||
solAssert(_right.size() == 1, "");
|
solAssert(_right.size() == 1, "");
|
||||||
|
@ -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
|
@ -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
|
@ -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
|
@ -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
|
@ -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
|
Loading…
Reference in New Issue
Block a user