@@ -244,7 +244,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
244
244
}
245
245
246
246
/** 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 ) }
248
251
249
252
/** Holds if this value represents `null` or non-`null` as indicated by `isNull`. */
250
253
predicate isNullness ( boolean isNull ) { this = TValue ( TValueNull ( ) , isNull ) }
@@ -292,13 +295,13 @@ module Make<LocationSig Location, InputSig<Location> Input> {
292
295
}
293
296
294
297
private predicate constantHasValue ( ConstantExpr c , GuardValue v ) {
295
- c .isNull ( ) and v = TValue ( TValueNull ( ) , true )
298
+ c .isNull ( ) and v . isNullValue ( )
296
299
or
297
- v = TValue ( TValueTrue ( ) , c .asBooleanValue ( ) )
300
+ v . asBooleanValue ( ) = c .asBooleanValue ( )
298
301
or
299
- v = TValue ( TValueInt ( c .asIntegerValue ( ) ) , true )
302
+ v . asIntValue ( ) = c .asIntegerValue ( )
300
303
or
301
- v = TValue ( TValueConstant ( c .asConstantValue ( ) ) , true )
304
+ v . asConstantValue ( ) = c .asConstantValue ( )
302
305
}
303
306
304
307
private predicate exceptionBranchPoint ( BasicBlock bb1 , BasicBlock normalSucc , BasicBlock excSucc ) {
@@ -328,10 +331,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
328
331
}
329
332
330
333
private predicate caseBranchEdge ( BasicBlock bb1 , BasicBlock bb2 , GuardValue v , Case c ) {
331
- v = TValue ( TValueTrue ( ) , true ) and
334
+ v . asBooleanValue ( ) = true and
332
335
c .matchEdge ( bb1 , bb2 )
333
336
or
334
- v = TValue ( TValueTrue ( ) , false ) and
337
+ v . asBooleanValue ( ) = false and
335
338
c .nonMatchEdge ( bb1 , bb2 )
336
339
}
337
340
@@ -390,7 +393,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
390
393
* `bb2` exactly when evaluating to `branch`.
391
394
*/
392
395
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 ) )
394
397
}
395
398
396
399
/**
@@ -400,7 +403,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
400
403
* That is, `bb` is dominated by the `branch`-successor edge of this guard.
401
404
*/
402
405
predicate directlyControls ( BasicBlock bb , boolean branch ) {
403
- this .directlyValueControls ( bb , TValue ( TValueTrue ( ) , branch ) )
406
+ this .directlyValueControls ( bb , any ( GuardValue gv | gv . asBooleanValue ( ) = branch ) )
404
407
}
405
408
406
409
/**
@@ -434,9 +437,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
434
437
}
435
438
436
439
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
438
441
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
440
443
or
441
444
g1 .( NotExpr ) .getOperand ( ) = g2 and v1 .asBooleanValue ( ) .booleanNot ( ) = v2 .asBooleanValue ( )
442
445
or
@@ -451,7 +454,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
451
454
or
452
455
exists ( NonNullExpr nonnull |
453
456
eqtestHasOperands ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
454
- v2 = TValue ( TValueNull ( ) , false )
457
+ v2 . isNonNullValue ( )
455
458
)
456
459
or
457
460
exists ( Case c1 , Expr switchExpr |
@@ -700,7 +703,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
700
703
or
701
704
exists ( boolean isNull |
702
705
additionalNullCheck ( g1 , v1 , g2 , isNull ) and
703
- v2 = TValue ( TValueNull ( ) , isNull ) and
706
+ v2 . isNullness ( isNull ) and
704
707
not ( g2 instanceof NonNullExpr and isNull = false ) // disregard trivial guard
705
708
)
706
709
}
@@ -723,7 +726,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
723
726
private predicate exprHasValue ( Expr e , GuardValue v ) {
724
727
constantHasValue ( e , v )
725
728
or
726
- e instanceof NonNullExpr and v = TValue ( TValueNull ( ) , false )
729
+ e instanceof NonNullExpr and v . isNonNullValue ( )
727
730
or
728
731
exprHasValue ( e .( IdExpr ) .getEqualChildExpr ( ) , v )
729
732
or
@@ -745,7 +748,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
745
748
exists ( Expr nonnull |
746
749
exprHasValue ( nonnull , v2 ) and
747
750
eqtestHasOperands ( g1 , g2 , nonnull , v1 .asBooleanValue ( ) ) and
748
- v2 = TValue ( TValueNull ( ) , false )
751
+ v2 . isNonNullValue ( )
749
752
)
750
753
}
751
754
@@ -763,7 +766,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
763
766
// g1 === g2 ? e : ...;
764
767
// g1 === g2 ? ... : e;
765
768
g2 = cond .getCondition ( ) and
766
- v2 = TValue ( TValueTrue ( ) , branch .booleanNot ( ) )
769
+ v2 . asBooleanValue ( ) = branch .booleanNot ( )
767
770
or
768
771
// g1 === ... ? g2 : e
769
772
// g1 === ... ? e : g2
@@ -870,8 +873,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
870
873
* null if `isNull` is true, and non-null if `isNull` is false.
871
874
*/
872
875
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 ) ) )
875
878
}
876
879
877
880
private predicate hasAValueBranchEdge ( Guard guard , GuardValue v ) {
@@ -1066,7 +1069,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1066
1069
* also considers additional logical reasoning.
1067
1070
*/
1068
1071
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 ) )
1070
1073
}
1071
1074
1072
1075
/**
@@ -1078,7 +1081,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1078
1081
* also considers additional logical reasoning.
1079
1082
*/
1080
1083
predicate controls ( BasicBlock bb , boolean branch ) {
1081
- this .valueControls ( bb , TValue ( TValueTrue ( ) , branch ) )
1084
+ this .valueControls ( bb , any ( GuardValue gv | gv . asBooleanValue ( ) = branch ) )
1082
1085
}
1083
1086
}
1084
1087
}
0 commit comments