C++: Fix join orders in 'exprIsSubLeftOrLess'.

Before:

Tuple counts for UnsignedDifferenceExpressionComparedZero::exprIsSubLeftOrLess#ff/2@i3#a5071w3a after 24s:
  304220    ~2%      {2} r1 = JOIN UnsignedDifferenceExpressionComparedZero::exprIsSubLeftOrLess#ff#prev_delta WITH Expr::BinaryOperation#class#f#join_rhs ON FIRST 1 OUTPUT Lhs.1, Rhs.0 'sub'

  190061335 ~24%     {2} r2 = JOIN r1 WITH DataFlowUtil::localFlowStep#ff ON FIRST 1 OUTPUT Lhs.1 'sub', Rhs.1 'n'

  3956      ~0%      {2} r3 = JOIN r1 WITH DataFlowUtil::localFlowStep#ff_10#join_rhs ON FIRST 1 OUTPUT Lhs.1 'sub', Rhs.1 'n'

  407983    ~1%      {2} r4 = JOIN Expr::BinaryOperation#class#f#join_rhs WITH UnsignedDifferenceExpressionComparedZero::exprIsSubLeftOrLess#ff#prev ON FIRST 1 OUTPUT Rhs.1 'n', Lhs.0 'sub'
  380823    ~0%      {2} r5 = JOIN r4 WITH DataFlowUtil::TExprNode#ff_10#join_rhs ON FIRST 1 OUTPUT Lhs.1 'sub', Rhs.1
  0         ~0%      {2} r6 = JOIN r5 WITH UnsignedDifferenceExpressionComparedZero::isGuarded#fff#prev_delta ON FIRST 2 OUTPUT Rhs.2, Lhs.0 'sub'
  0         ~0%      {2} r7 = JOIN r6 WITH DataFlowUtil::TExprNode#ff ON FIRST 1 OUTPUT Lhs.1 'sub', Rhs.1 'n'

  3956      ~0%      {2} r8 = r3 UNION r7
  190065291 ~24%     {2} r9 = r2 UNION r8
  ...

After:

Tuple counts for UnsignedDifferenceExpressionComparedZero::interestingSubExpr#f/1@654e29g3 after 228ms:
  370 ~2%     {2} r1 = ComparisonOperation::RelationalOperation::getGreaterOperand_dispred#fb AND NOT Exclusions::isFromMacroDefinition#b(Lhs.1 'sub')
  370 ~0%     {2} r2 = SCAN r1 OUTPUT In.1 'sub', In.0
  370 ~3%     {3} r3 = JOIN r2 WITH Expr::Expr::getFullyConverted_dispred#ff ON FIRST 1 OUTPUT Rhs.1, Lhs.1, Lhs.0 'sub'
  210 ~1%     {2} r4 = JOIN r3 WITH SimpleRangeAnalysis::SimpleRangeAnalysisCached::exprMightOverflowNegatively#f ON FIRST 1 OUTPUT Lhs.2 'sub', Lhs.1
  210 ~0%     {3} r5 = JOIN r4 WITH Expr::Expr::getFullyConverted_dispred#ff ON FIRST 1 OUTPUT Lhs.1, Lhs.0 'sub', Rhs.1
  210 ~1%     {3} r6 = JOIN r5 WITH ComparisonOperation::RelationalOperation::getLesserOperand_dispred#ff ON FIRST 1 OUTPUT Rhs.1, Lhs.1 'sub', Lhs.2
  59  ~2%     {4} r7 = JOIN r6 WITH Expr::Expr::getValue_dispred#ff ON FIRST 1 OUTPUT Lhs.1 'sub', Lhs.2, Rhs.1, toInt(Rhs.1)
  17  ~0%     {4} r8 = SELECT r7 ON In.3 = 0
  17  ~0%     {2} r9 = SCAN r8 OUTPUT In.1, In.0 'sub'
  8   ~0%     {2} r10 = JOIN r9 WITH Expr::Expr::getUnspecifiedType_dispred#bb ON FIRST 1 OUTPUT Rhs.1, Lhs.1 'sub'
  8   ~0%     {1} r11 = JOIN r10 WITH Type::IntegralType::isUnsigned_dispred#f ON FIRST 1 OUTPUT Lhs.1 'sub'
              return r11

Tuple counts for UnsignedDifferenceExpressionComparedZero::exprIsSubLeftOrLess#ff/2@i2#61800weu after 1ms:
  8  ~0%      {2} r1 = JOIN UnsignedDifferenceExpressionComparedZero::exprIsSubLeftOrLess#ff#prev_delta WITH UnsignedDifferenceExpressionComparedZero::interestingSubExpr#f ON FIRST 1 OUTPUT Lhs.1, Lhs.0 'sub'

  0  ~0%      {2} r2 = JOIN r1 WITH DataFlowUtil::localFlowStep#ff ON FIRST 1 OUTPUT Lhs.1 'sub', Rhs.1 'n'

  1  ~0%      {2} r3 = JOIN r1 WITH DataFlowUtil::localFlowStep#ff_10#join_rhs ON FIRST 1 OUTPUT Lhs.1 'sub', Rhs.1 'n'

  0  ~0%      {3} r4 = JOIN UnsignedDifferenceExpressionComparedZero::isGuarded#fff#prev_delta WITH UnsignedDifferenceExpressionComparedZero::interestingSubExpr#f ON FIRST 1 OUTPUT Lhs.1, Lhs.0 'sub', Lhs.2
  0  ~0%      {3} r5 = JOIN r4 WITH DataFlowUtil::TExprNode#ff ON FIRST 1 OUTPUT Lhs.1 'sub', Rhs.1 'n', Lhs.2
  0  ~0%      {2} r6 = JOIN r5 WITH UnsignedDifferenceExpressionComparedZero::exprIsSubLeftOrLess#ff#prev ON FIRST 2 OUTPUT Lhs.2, Lhs.0 'sub'
  0  ~0%      {2} r7 = JOIN r6 WITH DataFlowUtil::TExprNode#ff ON FIRST 1 OUTPUT Lhs.1 'sub', Rhs.1 'n'

  1  ~0%      {2} r8 = r3 UNION r7
  1  ~0%      {2} r9 = r2 UNION r8
  ...
This commit is contained in:
Mathias Vorreiter Pedersen
2022-01-10 17:28:14 +00:00
parent f2d6bcd767
commit 2a02ce137a

View File

@@ -38,47 +38,56 @@ predicate isGuarded(SubExpr sub, Expr left, Expr right) {
* `sub.getLeftOperand()`.
*/
predicate exprIsSubLeftOrLess(SubExpr sub, DataFlow::Node n) {
n.asExpr() = sub.getLeftOperand()
or
exists(DataFlow::Node other |
// dataflow
exprIsSubLeftOrLess(sub, other) and
(
DataFlow::localFlowStep(n, other) or
DataFlow::localFlowStep(other, n)
interestingSubExpr(sub, _) and // Manual magic
(
n.asExpr() = sub.getLeftOperand()
or
exists(DataFlow::Node other |
// dataflow
exprIsSubLeftOrLess(sub, other) and
(
DataFlow::localFlowStep(n, other) or
DataFlow::localFlowStep(other, n)
)
)
or
exists(DataFlow::Node other |
// guard constraining `sub`
exprIsSubLeftOrLess(sub, other) and
isGuarded(sub, other.asExpr(), n.asExpr()) // other >= n
)
or
exists(DataFlow::Node other, float p, float q |
// linear access of `other`
exprIsSubLeftOrLess(sub, other) and
linearAccess(n.asExpr(), other.asExpr(), p, q) and // n = p * other + q
p <= 1 and
q <= 0
)
or
exists(DataFlow::Node other, float p, float q |
// linear access of `n`
exprIsSubLeftOrLess(sub, other) and
linearAccess(other.asExpr(), n.asExpr(), p, q) and // other = p * n + q
p >= 1 and
q >= 0
)
)
or
exists(DataFlow::Node other |
// guard constraining `sub`
exprIsSubLeftOrLess(sub, other) and
isGuarded(sub, other.asExpr(), n.asExpr()) // other >= n
)
or
exists(DataFlow::Node other, float p, float q |
// linear access of `other`
exprIsSubLeftOrLess(sub, other) and
linearAccess(n.asExpr(), other.asExpr(), p, q) and // n = p * other + q
p <= 1 and
q <= 0
)
or
exists(DataFlow::Node other, float p, float q |
// linear access of `n`
exprIsSubLeftOrLess(sub, other) and
linearAccess(other.asExpr(), n.asExpr(), p, q) and // other = p * n + q
p >= 1 and
q >= 0
)
}
from RelationalOperation ro, SubExpr sub
where
not isFromMacroDefinition(ro) and
predicate interestingSubExpr(SubExpr sub, RelationalOperation ro) {
not isFromMacroDefinition(sub) and
ro.getLesserOperand().getValue().toInt() = 0 and
ro.getGreaterOperand() = sub and
sub.getFullyConverted().getUnspecifiedType().(IntegralType).isUnsigned() and
exprMightOverflowNegatively(sub.getFullyConverted()) and // generally catches false positives involving constants
not exprIsSubLeftOrLess(sub, DataFlow::exprNode(sub.getRightOperand())) // generally catches false positives where there's a relation between the left and right operands
// generally catches false positives involving constants
exprMightOverflowNegatively(sub.getFullyConverted())
}
from RelationalOperation ro, SubExpr sub
where
interestingSubExpr(sub, ro) and
not isFromMacroDefinition(ro) and
// generally catches false positives where there's a relation between the left and right operands
not exprIsSubLeftOrLess(sub, DataFlow::exprNode(sub.getRightOperand()))
select ro, "Unsigned subtraction can never be negative."