C#: Improve join order in `conditionalAssign()`

Fixes a bad join-order in `Guards::Internal::conditionalAssign#ffff#antijoin_rhs#1`:

```
[2019-01-25 14:12:03] (377s) Starting to evaluate predicate Guards::Internal::conditionalAssign#ffff#antijoin_rhs#1
[2019-01-25 14:20:41] (895s) Tuple counts:
                      9302551    ~1%     {7} r1 = JOIN ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getAPhiInput_dispred#ff WITH Guards::Internal::conditionalAssign#ffff#shared#1 ON ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getAPhiInput_dispred#ff.<0>=Guards::Internal::conditionalAssign#ffff#shared#1.<0> OUTPUT FIELDS {ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getAPhiInput_dispred#ff.<1>,Guards::Internal::conditionalAssign#ffff#shared#1.<1>,Guards::Internal::conditionalAssign#ffff#shared#1.<2>,Guards::Internal::conditionalAssign#ffff#shared#1.<0>,Guards::Internal::conditionalAssign#ffff#shared#1.<3>,Guards::Internal::conditionalAssign#ffff#shared#1.<4>,Guards::Internal::conditionalAssign#ffff#shared#1.<5>}
                      9302551    ~7%     {8} r2 = JOIN r1 WITH ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getBasicBlock_dispred#ff ON r1.<0>=ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getBasicBlock_dispred#ff.<0> OUTPUT FIELDS {r1.<1>,ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getBasicBlock_dispred#ff.<1>,r1.<2>,r1.<3>,r1.<4>,r1.<5>,r1.<6>,r1.<0>}
                      1223774650 ~0%     {8} r3 = JOIN r2 WITH Guards::Internal::Guard::preControlsDirect_dispred#fff ON r2.<0>=Guards::Internal::Guard::preControlsDirect_dispred#fff.<0> AND r2.<1>=Guards::Internal::Guard::preControlsDirect_dispred#fff.<1> OUTPUT FIELDS {r2.<6>,Guards::Internal::Guard::preControlsDirect_dispred#fff.<2>,r2.<0>,r2.<2>,r2.<3>,r2.<4>,r2.<5>,r2.<7>}
                      80626      ~0%     {7} r4 = JOIN r3 WITH Guards::AbstractValue::getDualValue_dispred#ff ON r3.<0>=Guards::AbstractValue::getDualValue_dispred#ff.<0> AND r3.<1>=Guards::AbstractValue::getDualValue_dispred#ff.<1> OUTPUT FIELDS {r3.<2>,r3.<3>,r3.<4>,r3.<5>,r3.<6>,r3.<0>,r3.<7>}
                      9293564    ~0%     {7} r5 = Guards::Internal::conditionalAssign#ffff#shared#2 AND NOT Guards::Internal::conditionalAssign#ffff#antijoin_rhs(Guards::Internal::conditionalAssign#ffff#shared#2.<0>,Guards::Internal::conditionalAssign#ffff#shared#2.<1>,Guards::Internal::conditionalAssign#ffff#shared#2.<2>,Guards::Internal::conditionalAssign#ffff#shared#2.<3>,Guards::Internal::conditionalAssign#ffff#shared#2.<4>,Guards::Internal::conditionalAssign#ffff#shared#2.<5>,Guards::Internal::conditionalAssign#ffff#shared#2.<6>)
                      9293564    ~1%     {7} r6 = SCAN r5 OUTPUT FIELDS {r5.<6>,r5.<0>,r5.<1>,r5.<2>,r5.<3>,r5.<4>,r5.<5>}
                      9293564    ~2%     {8} r7 = JOIN r6 WITH ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getBasicBlock_dispred#ff ON r6.<0>=ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getBasicBlock_dispred#ff.<0> OUTPUT FIELDS {ControlFlowGraph::ControlFlow::Internal::PreSsa::Definition::getBasicBlock_dispred#ff.<1>,r6.<2>,r6.<1>,r6.<3>,r6.<4>,r6.<5>,r6.<6>,r6.<0>}
                      1940       ~2%     {7} r8 = JOIN r7 WITH ControlFlowGraph::ControlFlow::Internal::PreBasicBlocks::PreBasicBlock::dominates_dispred#ff ON r7.<0>=ControlFlowGraph::ControlFlow::Internal::PreBasicBlocks::PreBasicBlock::dominates_dispred#ff.<0> AND r7.<1>=ControlFlowGraph::ControlFlow::Internal::PreBasicBlocks::PreBasicBlock::dominates_dispred#ff.<1> OUTPUT FIELDS {r7.<2>,r7.<1>,r7.<3>,r7.<4>,r7.<5>,r7.<6>,r7.<7>}
                      82566      ~0%     {7} r9 = r4 \/ r8
                                         return r9
```
This commit is contained in:
Tom Hvitved 2019-02-07 10:33:19 +01:00
Родитель 47ad280e34
Коммит 23e63e983c
1 изменённых файлов: 49 добавлений и 10 удалений

Просмотреть файл

@ -895,6 +895,48 @@ module Internal {
)
}
pragma[noinline]
private predicate conditionalAssign0(
Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
PreBasicBlocks::PreBasicBlock bbGuard
) {
e = upd.getDefinition().getSource() and
upd = def.getAPhiInput() and
guard.preControlsDirect(upd.getBasicBlock(), vGuard) and
bbGuard.getAnElement() = guard and
bbGuard.strictlyDominates(def.getBasicBlock()) and
not guard.preControlsDirect(def.getBasicBlock(), vGuard)
}
pragma[noinline]
private predicate conditionalAssign1(
Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
PreBasicBlocks::PreBasicBlock bbGuard, PreSsa::Definition other
) {
conditionalAssign0(guard, vGuard, def, e, upd, bbGuard) and
other != upd and
other = def.getAPhiInput()
}
pragma[noinline]
private predicate conditionalAssign2(
Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
PreBasicBlocks::PreBasicBlock bbGuard, PreSsa::Definition other
) {
conditionalAssign1(guard, vGuard, def, e, upd, bbGuard, other) and
guard.preControlsDirect(other.getBasicBlock(), vGuard.getDualValue())
}
pragma[noinline]
private predicate conditionalAssign3(
Guard guard, AbstractValue vGuard, PreSsa::Definition def, Expr e, PreSsa::Definition upd,
PreBasicBlocks::PreBasicBlock bbGuard, PreSsa::Definition other
) {
conditionalAssign1(guard, vGuard, def, e, upd, bbGuard, other) and
other.getBasicBlock().dominates(bbGuard) and
not PreSsa::ssaDefReachesEndOfBlock(guard.getConditionalSuccessor(vGuard), other, _)
}
/**
* Holds if the evaluation of `guard` to `vGuard` implies that `def` is assigned
* expression `e`.
@ -916,28 +958,25 @@ module Internal {
)
or
exists(PreSsa::Definition upd, PreBasicBlocks::PreBasicBlock bbGuard |
e = upd.getDefinition().getSource() and
upd = def.getAPhiInput() and
guard.preControlsDirect(upd.getBasicBlock(), vGuard) and
bbGuard.getAnElement() = guard and
bbGuard.strictlyDominates(def.getBasicBlock()) and
not guard.preControlsDirect(def.getBasicBlock(), vGuard) and
forall(PreSsa::Definition other | other != upd and other = def.getAPhiInput() |
conditionalAssign0(guard, vGuard, def, e, upd, bbGuard)
|
forall(PreSsa::Definition other |
conditionalAssign1(guard, vGuard, def, e, upd, bbGuard, other)
|
// For example:
// if (guard)
// upd = a;
// else
// other = b;
// def = phi(upd, other)
guard.preControlsDirect(other.getBasicBlock(), vGuard.getDualValue())
conditionalAssign2(guard, vGuard, def, e, upd, bbGuard, other)
or
// For example:
// other = a;
// if (guard)
// upd = b;
// def = phi(other, upd)
other.getBasicBlock().dominates(bbGuard) and
not PreSsa::ssaDefReachesEndOfBlock(guard.getConditionalSuccessor(vGuard), other, _)
conditionalAssign3(guard, vGuard, def, e, upd, bbGuard, other)
)
)
}