Given how predicates are subsumed by the Expr class, which performs automatic simplification (and, in particular, moves all operands of a comparison to the right), $\phi$ predicates are encoded in a very hacky way (via approximating the "support" for each branch condition leading to the phi node).
While I don't have an explicit counterexample, one doesn't seem too difficult to contrive: you just need branch conditions dependent on complex expressions of "atomic" registers (i.e., ones coming from reads or other $\phi$-nodes).
Originally, the $\phi$ predicates were supported over all value numbers computed up to that point. Although this is safe, it's way too slow (takes minutes to handle examples/gargi.ami).
A possible fix for this is to have the decomposition of branch conditions (via the PredicatedState class) also indicate which operands or expressions are actually stored in the underlying Comparisons instance for the state, rather than have the GVN algorithm class try to approximate it.
Given how predicates are subsumed by the$\phi$ predicates are encoded in a very hacky way (via approximating the "support" for each branch condition leading to the phi node).
Exprclass, which performs automatic simplification (and, in particular, moves all operands of a comparison to the right),While I don't have an explicit counterexample, one doesn't seem too difficult to contrive: you just need branch conditions dependent on complex expressions of "atomic" registers (i.e., ones coming from$\phi$ -nodes).
reads or otherOriginally, the$\phi$ predicates were supported over all value numbers computed up to that point. Although this is safe, it's way too slow (takes minutes to handle
examples/gargi.ami).A possible fix for this is to have the decomposition of branch conditions (via the
PredicatedStateclass) also indicate which operands or expressions are actually stored in the underlyingComparisonsinstance for the state, rather than have the GVN algorithm class try to approximate it.