@@ -244,7 +244,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
244244 }
245245
246246 /** Holds if this value represents `null`. */
247- predicate isNullValue ( ) { this = TValue ( TValueNull ( ) , true ) }
247+ predicate isNullValue ( ) { this .isNullness ( true ) }
248+
249+ /** Holds if this value represents non-`null`. */
250+ predicate isNonNullValue ( ) { this .isNullness ( false ) }
248251
249252 /** Holds if this value represents `null` or non-`null` as indicated by `isNull`. */
250253 predicate isNullness ( boolean isNull ) { this = TValue ( TValueNull ( ) , isNull ) }
@@ -292,13 +295,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
292295 }
293296
294297 private predicate constantHasValue ( ConstantExpr c , GuardValue v ) {
295- c .isNull ( ) and v = TValue ( TValueNull ( ) , true )
298+ c .isNull ( ) and v . isNullValue ( )
296299 or
297- v = TValue ( TValueTrue ( ) , c .asBooleanValue ( ) )
300+ v . asBooleanValue ( ) = c .asBooleanValue ( )
298301 or
299- v = TValue ( TValueInt ( c .asIntegerValue ( ) ) , true )
302+ v . asIntValue ( ) = c .asIntegerValue ( )
300303 or
301- v = TValue ( TValueConstant ( c .asConstantValue ( ) ) , true )
304+ v . asConstantValue ( ) = c .asConstantValue ( )
302305 }
303306
304307 private predicate exceptionBranchPoint ( BasicBlock bb1 , BasicBlock normalSucc , BasicBlock excSucc ) {
@@ -328,10 +331,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
328331 }
329332
330333 private predicate caseBranchEdge ( BasicBlock bb1 , BasicBlock bb2 , GuardValue v , Case c ) {
331- v = TValue ( TValueTrue ( ) , true ) and
334+ v . asBooleanValue ( ) = true and
332335 c .matchEdge ( bb1 , bb2 )
333336 or
334- v = TValue ( TValueTrue ( ) , false ) and
337+ v . asBooleanValue ( ) = false and
335338 c .nonMatchEdge ( bb1 , bb2 )
336339 }
337340
@@ -390,7 +393,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
390393 * `bb2` exactly when evaluating to `branch`.
391394 */
392395 predicate hasBranchEdge ( BasicBlock bb1 , BasicBlock bb2 , boolean branch ) {
393- this .hasValueBranchEdge ( bb1 , bb2 , TValue ( TValueTrue ( ) , branch ) )
396+ this .hasValueBranchEdge ( bb1 , bb2 , any ( GuardValue gv | gv . asBooleanValue ( ) = branch ) )
394397 }
395398
396399 /**
@@ -400,7 +403,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
400403 * That is, `bb` is dominated by the `branch`-successor edge of this guard.
401404 */
402405 predicate directlyControls ( BasicBlock bb , boolean branch ) {
403- this .directlyValueControls ( bb , TValue ( TValueTrue ( ) , branch ) )
406+ this .directlyValueControls ( bb , any ( GuardValue gv | gv . asBooleanValue ( ) = branch ) )
404407 }
405408
406409 /**
@@ -434,9 +437,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
434437 }
435438
436439 private predicate baseImpliesStep ( PreGuard g1 , GuardValue v1 , PreGuard g2 , GuardValue v2 ) {
437- g1 .( AndExpr ) .getAnOperand ( ) = g2 and v1 = TValue ( TValueTrue ( ) , true ) and v2 = v1
440+ g1 .( AndExpr ) .getAnOperand ( ) = g2 and v1 . asBooleanValue ( ) = true and v2 = v1
438441 or
439- g1 .( OrExpr ) .getAnOperand ( ) = g2 and v1 = TValue ( TValueTrue ( ) , false ) and v2 = v1
442+ g1 .( OrExpr ) .getAnOperand ( ) = g2 and v1 . asBooleanValue ( ) = false and v2 = v1
440443 or
441444 g1 .( NotExpr ) .getOperand ( ) = g2 and v1 .asBooleanValue ( ) .booleanNot ( ) = v2 .asBooleanValue ( )
442445 or
@@ -451,7 +454,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
451454 or
452455 exists ( NonNullExpr nonnull |
453456 eqtestHasOperands ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
454- v2 = TValue ( TValueNull ( ) , false )
457+ v2 . isNonNullValue ( )
455458 )
456459 or
457460 exists ( Case c1 , Expr switchExpr |
@@ -700,7 +703,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
700703 or
701704 exists ( boolean isNull |
702705 additionalNullCheck ( g1 , v1 , g2 , isNull ) and
703- v2 = TValue ( TValueNull ( ) , isNull ) and
706+ v2 . isNullness ( isNull ) and
704707 not ( g2 instanceof NonNullExpr and isNull = false ) // disregard trivial guard
705708 )
706709 }
@@ -723,7 +726,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
723726 private predicate exprHasValue ( Expr e , GuardValue v ) {
724727 constantHasValue ( e , v )
725728 or
726- e instanceof NonNullExpr and v = TValue ( TValueNull ( ) , false )
729+ e instanceof NonNullExpr and v . isNonNullValue ( )
727730 or
728731 exprHasValue ( e .( IdExpr ) .getEqualChildExpr ( ) , v )
729732 or
@@ -745,7 +748,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
745748 exists ( Expr nonnull |
746749 exprHasValue ( nonnull , v2 ) and
747750 eqtestHasOperands ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
748- v2 = TValue ( TValueNull ( ) , false )
751+ v2 . isNonNullValue ( )
749752 )
750753 }
751754
@@ -763,7 +766,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
763766 // g1 === g2 ? e : ...;
764767 // g1 === g2 ? ... : e;
765768 g2 = cond .getCondition ( ) and
766- v2 = TValue ( TValueTrue ( ) , branch .booleanNot ( ) )
769+ v2 . asBooleanValue ( ) = branch .booleanNot ( )
767770 or
768771 // g1 === ... ? g2 : e
769772 // g1 === ... ? e : g2
@@ -870,8 +873,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
870873 * null if `isNull` is true, and non-null if `isNull` is false.
871874 */
872875 predicate nullGuard ( Guard guard , GuardValue v , Expr e , boolean isNull ) {
873- impliesStep2 ( guard , v , e , TValue ( TValueNull ( ) , isNull ) ) or
874- additionalImpliesStep ( guard , v , e , TValue ( TValueNull ( ) , isNull ) )
876+ impliesStep2 ( guard , v , e , any ( GuardValue gv | gv . isNullness ( isNull ) ) ) or
877+ additionalImpliesStep ( guard , v , e , any ( GuardValue gv | gv . isNullness ( isNull ) ) )
875878 }
876879
877880 private predicate hasAValueBranchEdge ( Guard guard , GuardValue v ) {
@@ -1066,7 +1069,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
10661069 * also considers additional logical reasoning.
10671070 */
10681071 predicate controlsBranchEdge ( BasicBlock bb1 , BasicBlock bb2 , boolean branch ) {
1069- this .valueControlsBranchEdge ( bb1 , bb2 , TValue ( TValueTrue ( ) , branch ) )
1072+ this .valueControlsBranchEdge ( bb1 , bb2 , any ( GuardValue gv | gv . asBooleanValue ( ) = branch ) )
10701073 }
10711074
10721075 /**
@@ -1078,7 +1081,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
10781081 * also considers additional logical reasoning.
10791082 */
10801083 predicate controls ( BasicBlock bb , boolean branch ) {
1081- this .valueControls ( bb , TValue ( TValueTrue ( ) , branch ) )
1084+ this .valueControls ( bb , any ( GuardValue gv | gv . asBooleanValue ( ) = branch ) )
10821085 }
10831086 }
10841087 }
0 commit comments