Simplify condition.

This commit is contained in:
chriseth 2021-11-23 15:24:24 +01:00
parent 87e6e2f9ba
commit e15cac6f05
2 changed files with 14 additions and 25 deletions

View File

@ -352,30 +352,19 @@ bool UnusedStoreEliminator::knownUnrelated(
if (_op2.length && knowledge.knownToBeZero(*_op2.length)) if (_op2.length && knowledge.knownToBeZero(*_op2.length))
return true; return true;
// 1.start + 1.length <= 2.start // We use diff >= _op1.length && diff <= 2**256 - _op2.length
if (_op1.length && _op2.start && _op1.start) // This requires us to know both lengths as constants, but
{ // does not have any problems with overflows.
optional<u256> length1 = knowledge.valueIfKnownConstant(*_op1.length); // See test/formal/redundant_store_unrelated.py for a proof.
optional<u256> diff = knowledge.differenceIfKnownConstant(*_op2.start, *_op1.start);
// diff = 2.start - 1.start if (!(_op1.length && _op1.start && _op2.start && _op2.length))
if (length1 && diff) return false;
if ( optional<u256> diff = knowledge.differenceIfKnownConstant(*_op2.start, *_op1.start);
*length1 <= *diff && optional<u256> length1 = knowledge.valueIfKnownConstant(*_op1.length);
*length1 <= largestPositive && optional<u256> length2 = knowledge.valueIfKnownConstant(*_op2.length);
*diff <= largestPositive if (diff && length1 && length2)
) if (*diff >= *length1 && *diff <= u256(0) - *length2)
return true; return true;
}
// 2.start + 2.length <= 1.start
if (_op2.length && _op1.start && _op2.start)
{
optional<u256> length2 = knowledge.valueIfKnownConstant(*_op2.length);
optional<u256> diff = knowledge.differenceIfKnownConstant(*_op1.start, *_op2.start);
// diff = 1.start - 2.start
if (length2 && diff)
if (*length2 <= *diff && *length2 <= largestPositive && *diff <= largestPositive)
return true;
}
} }
return false; return false;

View File

@ -43,7 +43,7 @@ struct AssignedValue;
* The m_store member of UnusedStoreBase is only used with the empty yul string * The m_store member of UnusedStoreBase is only used with the empty yul string
* as key in the first dimension. * as key in the first dimension.
* *
* Best run in SSA form. * Best run in SSA form without inlined literals.
* *
* Prerequisite: Disambiguator, ForLoopInitRewriter. * Prerequisite: Disambiguator, ForLoopInitRewriter.
*/ */