@@ -69,6 +69,15 @@ module Make<LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Cfg::BasicB
6969 private import Cfg
7070 private import Input
7171
72+ /**
73+ * Holds if the edge from `bb1` to `bb2` implies both that `def` evaluates
74+ * to `v` and that `g` evaluates to `gv`. The latter implication is also a
75+ * biimplication in most cases, except when `g` is a short-circuiting
76+ * side-effecting construct.
77+ *
78+ * Checking that `bb1` to `bb2` is a dominating edge is sufficient to ensure
79+ * that the biimplication holds.
80+ */
7281 private predicate ssaControlsGuardEdge (
7382 SsaDefinition def , GuardValue v , Guard g , BasicBlock bb1 , BasicBlock bb2 , GuardValue gv
7483 ) {
@@ -81,9 +90,10 @@ module Make<LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Cfg::BasicB
8190 private predicate impossibleValue (
8291 Guard g , GuardValue gv , SsaDefinition def , BasicBlock bb , GuardValue v2
8392 ) {
84- exists ( GuardValue dual , GuardValue v1 |
85- // If `g` in `bb` evaluates to `gv` then `def` has value `v1`,
86- ssaControlsGuardEdge ( def , v1 , g , bb , _, gv ) and
93+ exists ( GuardValue dual , GuardValue v1 , BasicBlock bb2 |
94+ // If `g` evaluates to `gv` and its branch edge `(bb, bb2)` is a dominating edge then `def` has value `v1`,
95+ ssaControlsGuardEdge ( def , v1 , g , bb , bb2 , gv ) and
96+ dominatingEdge ( bb , bb2 ) and
8797 dual = gv .getDualValue ( ) and
8898 not gv .isThrowsException ( ) and
8999 not dual .isThrowsException ( ) and
0 commit comments