Fix more joins.

Before:
```
Tuple counts for valueFlowStepSsa#4#ffff/4@2cddce6j after 11.4s:
  11571217  ~3%     {3} r1 = SCAN semSsaUpdateStep#3#fff OUTPUT In.0 'v', In.1 'e', f2i(In.2)
  11992425  ~0%     {4} r2 = JOIN r1 WITH SemanticSSA#aa9d1d08::SemSsaReadPosition::hasReadOfVar#1#dispred#ff_10#join_rhs ON FIRST 1 OUTPUT Lhs.0 'v', Rhs.1 'pos', Lhs.1 'e', Lhs.2 'delta'

  869481225 ~2%     {4} r3 = JOIN SemanticGuard#7b46a302::semGuardDirectlyControlsSsaRead#3#fff_102#join_rhs WITH SemanticSSA#aa9d1d08::SemSsaReadPosition::hasReadOfVar#1#dispred#ff ON FIRST 1 OUTPUT Rhs.1 'v', Lhs.2, Lhs.1, Lhs.0 'pos'
  5749      ~0%     {4} r4 = JOIN r3 WITH semEqFlowCond#5#fffbff#cpe#12356_03412#join_rhs ON FIRST 3 OUTPUT Lhs.3 'pos', Lhs.0 'v', Rhs.3 'e', Rhs.4
  5749      ~1%     {4} r5 = SCAN r4 OUTPUT In.0 'pos', In.1 'v', In.2 'e', f2i(In.3)
  5749      ~0%     {4} r6 = SCAN r5 OUTPUT In.1 'v', In.0 'pos', In.2 'e', In.3 'delta'

  11998174  ~0%     {4} r7 = r2 UNION r6
                    return r7
```

After:
```
Tuple counts for valueFlowStepSsaEqFlowCond#4#ffff/4@f196e4ok after 37ms:
  59567  ~0%     {5} r1 = JOIN const_true WITH semEqFlowCond#5#ffffff_301245#join_rhs ON FIRST 1 OUTPUT Rhs.1 'v', Rhs.2 'e', Rhs.4, Rhs.5, Rhs.3
  59567  ~0%     {5} r2 = SCAN r1 OUTPUT In.0 'v', In.1 'e', In.2, In.3, f2i(In.4)
  59567  ~4%     {5} r3 = SCAN r2 OUTPUT In.3, In.2, In.0 'v', In.1 'e', In.4 'delta'
  176881 ~0%     {4} r4 = JOIN r3 WITH SemanticGuard#7b46a302::semGuardDirectlyControlsSsaRead#3#fff_021#join_rhs ON FIRST 2 OUTPUT Rhs.2 'pos', Lhs.2 'v', Lhs.3 'e', Lhs.4 'delta'
                  return r4

Tuple counts for valueFlowStepSsa#4#ffff/4@e22d39v5 after 1s:
  5749     ~0%     {4} r1 = JOIN SemanticSSA#aa9d1d08::SemSsaReadPosition::hasReadOfVar#1#dispred#ff WITH valueFlowStepSsaEqFlowCond#4#ffff ON FIRST 2 OUTPUT Lhs.1 'v', Lhs.0 'pos', Rhs.2 'e', Rhs.3 'delta'

  11571217 ~0%     {3} r2 = SCAN semSsaUpdateStep#3#fff OUTPUT In.0 'v', In.1 'e', f2i(In.2)
  11992425 ~0%     {4} r3 = JOIN r2 WITH SemanticSSA#aa9d1d08::SemSsaReadPosition::hasReadOfVar#1#dispred#ff_10#join_rhs ON FIRST 1 OUTPUT Lhs.0 'v', Rhs.1 'pos', Lhs.1 'e', Lhs.2 'delta'

  11998174 ~0%     {4} r4 = r1 UNION r3
                    return r4
```
This commit is contained in:
Mathias Vorreiter Pedersen
2023-08-24 12:20:41 +01:00
parent 4e6707fee5
commit d42e892097
3 changed files with 17 additions and 7 deletions

View File

@@ -39,6 +39,7 @@ predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {
* Holds if `guard` directly controls the position `controlled` with the
* value `testIsTrue`.
*/
pragma[nomagic]
predicate semGuardDirectlyControlsSsaRead(
SemGuard guard, SemSsaReadPosition controlled, boolean testIsTrue
) {

View File

@@ -17,19 +17,27 @@ private import RangeUtils
private import RangeAnalysisStage
module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
/**
* Holds if `e + delta` equals `v` at `pos`.
*/
private predicate valueFlowStepSsa(SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta) {
U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
or
pragma[nomagic]
private predicate valueFlowStepSsaEqFlowCond(
SemSsaReadPosition pos, SemSsaVariable v, SemExpr e, int delta
) {
exists(SemGuard guard, boolean testIsTrue |
pos.hasReadOfVar(v) and
guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue)
)
}
/**
* Holds if `e + delta` equals `v` at `pos`.
*/
pragma[nomagic]
private predicate valueFlowStepSsa(SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta) {
U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
or
pos.hasReadOfVar(v) and
valueFlowStepSsaEqFlowCond(pos, v, e, delta)
}
/**
* Holds if `add` is the addition of `larg` and `rarg`, neither of which are
* `ConstantIntegerExpr`s.

View File

@@ -49,6 +49,7 @@ module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::Ut
* - `isEq = true` : `v == e + delta`
* - `isEq = false` : `v != e + delta`
*/
pragma[nomagic]
SemGuard semEqFlowCond(
SemSsaVariable v, SemExpr e, D::Delta delta, boolean isEq, boolean testIsTrue
) {