@@ -694,7 +694,7 @@ module Internal {
694694 predicate preControls ( PreBasicBlocks:: PreBasicBlock bb , AbstractValue v ) {
695695 exists ( AbstractValue v0 , Guard g |
696696 g .preControlsDirect ( bb , v0 ) |
697- impliesSteps ( g , v0 , this , v )
697+ preImpliesSteps ( g , v0 , this , v )
698698 )
699699 }
700700
@@ -781,7 +781,7 @@ module Internal {
781781 def .nullGuardedReturn ( ret , isNull )
782782 or
783783 exists ( NullValue nv |
784- impliesSteps ( ret , retVal , def .getARead ( ) , nv ) |
784+ preImpliesSteps ( ret , retVal , def .getARead ( ) , nv ) |
785785 if nv .isNull ( ) then isNull = true else isNull = false
786786 )
787787 )
@@ -1123,6 +1123,28 @@ module Internal {
11231123 def = guarded .getAnSsaQualifier ( )
11241124 )
11251125 }
1126+
1127+ /**
1128+ * Holds if the assumption that `g1` has abstract value `v1` implies that
1129+ * `g2` has abstract value `v2`, using one step of reasoning. That is, the
1130+ * evaluation of `g2` to `v2` dominates the evaluation of `g1` to `v1`.
1131+ *
1132+ * This predicate relies on the control flow graph.
1133+ */
1134+ cached
1135+ predicate impliesStep ( Guard g1 , AbstractValue v1 , Guard g2 , AbstractValue v2 ) {
1136+ preImpliesStep ( g1 , v1 , g2 , v2 )
1137+ or
1138+ forex ( ControlFlow:: Node cfn |
1139+ cfn = g1 .getAControlFlowNode ( ) |
1140+ exists ( Ssa:: ExplicitDefinition def |
1141+ def .getADefinition ( ) .getSource ( ) = g2 |
1142+ g1 = def .getAReadAtNode ( cfn ) and
1143+ v1 = g1 .getAValue ( ) and
1144+ v2 = v1
1145+ )
1146+ )
1147+ }
11261148 }
11271149 import Cached
11281150
@@ -1143,9 +1165,11 @@ module Internal {
11431165 * Holds if the assumption that `g1` has abstract value `v1` implies that
11441166 * `g2` has abstract value `v2`, using one step of reasoning. That is, the
11451167 * evaluation of `g2` to `v2` dominates the evaluation of `g1` to `v1`.
1168+ *
1169+ * This predicate does not rely on the control flow graph.
11461170 */
11471171 cached
1148- predicate impliesStep ( Guard g1 , AbstractValue v1 , Guard g2 , AbstractValue v2 ) {
1172+ predicate preImpliesStep ( Guard g1 , AbstractValue v1 , Guard g2 , AbstractValue v2 ) {
11491173 g1 = any ( BinaryOperation bo |
11501174 (
11511175 bo instanceof BitwiseAndExpr or
@@ -1279,6 +1303,26 @@ module Internal {
12791303 * Holds if the assumption that `g1` has abstract value `v1` implies that
12801304 * `g2` has abstract value `v2`, using zero or more steps of reasoning. That is,
12811305 * the evaluation of `g2` to `v2` dominates the evaluation of `g1` to `v1`.
1306+ *
1307+ * This predicate does not rely on the control flow graph.
1308+ */
1309+ predicate preImpliesSteps ( Guard g1 , AbstractValue v1 , Guard g2 , AbstractValue v2 ) {
1310+ g1 = g2 and
1311+ v1 = v2 and
1312+ v1 = g1 .getAValue ( )
1313+ or
1314+ exists ( Expr mid , AbstractValue vMid |
1315+ preImpliesSteps ( g1 , v1 , mid , vMid ) |
1316+ preImpliesStep ( mid , vMid , g2 , v2 )
1317+ )
1318+ }
1319+
1320+ /**
1321+ * Holds if the assumption that `g1` has abstract value `v1` implies that
1322+ * `g2` has abstract value `v2`, using zero or more steps of reasoning. That is,
1323+ * the evaluation of `g2` to `v2` dominates the evaluation of `g1` to `v1`.
1324+ *
1325+ * This predicate relies on the control flow graph.
12821326 */
12831327 predicate impliesSteps ( Guard g1 , AbstractValue v1 , Guard g2 , AbstractValue v2 ) {
12841328 g1 = g2 and
0 commit comments