@@ -227,7 +227,7 @@ private module LogicInput implements GuardsImpl::LogicInputSig {
227227 e instanceof DereferenceableExpr and
228228 ct .getAnArgument ( ) = e and
229229 ct .getAnArgument ( ) = arg and
230- arg = any ( NullValue nv | nv . isNonNull ( ) ) . getAnExpr ( ) and
230+ nonNullValueImplied ( arg ) and
231231 ck = ct .getComparisonKind ( ) and
232232 e != arg and
233233 isNull = false and
@@ -314,7 +314,7 @@ class Guard extends Guards::Guard {
314314 * In case `cfn` or `sub` access an SSA variable in their left-most qualifier, then
315315 * so must the other (accessing the same SSA variable).
316316 */
317- predicate controlsNode ( ControlFlow:: Nodes:: ElementNode cfn , AccessOrCallExpr sub , AbstractValue v ) {
317+ predicate controlsNode ( ControlFlow:: Nodes:: ElementNode cfn , AccessOrCallExpr sub , GuardValue v ) {
318318 isGuardedByNode ( cfn , this , sub , v )
319319 }
320320
@@ -324,26 +324,31 @@ class Guard extends Guards::Guard {
324324 * Note: This predicate is inlined.
325325 */
326326 pragma [ inline]
327- predicate controlsNode ( ControlFlow:: Nodes:: ElementNode cfn , AbstractValue v ) {
327+ predicate controlsNode ( ControlFlow:: Nodes:: ElementNode cfn , GuardValue v ) {
328328 guardControls ( this , cfn .getBasicBlock ( ) , v )
329329 }
330330
331331 /**
332332 * Holds if basic block `bb` is guarded by this expression having value `v`.
333333 */
334- predicate controlsBasicBlock ( BasicBlock bb , AbstractValue v ) { guardControls ( this , bb , v ) }
334+ predicate controlsBasicBlock ( BasicBlock bb , GuardValue v ) { guardControls ( this , bb , v ) }
335335
336336 /**
337337 * Gets a valid value for this guard. For example, if this guard is a test, then
338338 * it can have Boolean values `true` and `false`.
339339 */
340- deprecated AbstractValue getAValue ( ) { isGuard ( this , result ) }
340+ deprecated GuardValue getAValue ( ) { isGuard ( this , result ) }
341341}
342342
343- class AbstractValue = GuardValue ;
343+ /** DEPRECATED: Use `GuardValue` instead. */
344+ deprecated class AbstractValue = GuardValue ;
344345
345- /** Provides different types of `AbstractValues`s. */
346- module AbstractValues {
346+ /**
347+ * DEPRECATED: Use `GuardValue` member predicates instead.
348+ *
349+ * Provides different types of `AbstractValues`s.
350+ */
351+ deprecated module AbstractValues {
347352 class BooleanValue extends AbstractValue {
348353 BooleanValue ( ) { exists ( this .asBooleanValue ( ) ) }
349354
@@ -369,8 +374,6 @@ module AbstractValues {
369374 }
370375}
371376
372- private import AbstractValues
373-
374377/** Gets the value resulting from matching `null` against `pat`. */
375378private boolean patternMatchesNull ( PatternExpr pat ) {
376379 pat instanceof NullLiteral and result = true
@@ -428,35 +431,11 @@ class DereferenceableExpr extends Expr {
428431 /** Holds if this expression has a nullable type `T?`. */
429432 predicate hasNullableType ( ) { isNullableType = true }
430433
431- /**
432- * Gets an expression that tests via nullness whether this expression is `null`.
433- *
434- * If the returned expression evaluates to `null` (`v.isNull()`) or evaluates to
435- * non-`null` (`not v.isNull()`), then this expression is guaranteed to be `null`
436- * if `isNull` is true, and non-`null` if `isNull` is false.
437- *
438- * For example, if `x` evaluates to `null` in `x ?? y` then `y` is evaluated, and
439- * `x` is guaranteed to be `null`.
440- */
441- private Expr getANullnessNullCheck ( NullValue v , boolean isNull ) {
442- exists ( NullnessCompletion c | c .isValidFor ( this ) |
443- result = this and
444- if c .isNull ( )
445- then (
446- v .isNull ( ) and
447- isNull = true
448- ) else (
449- v .isNonNull ( ) and
450- isNull = false
451- )
452- )
453- }
454-
455434 /** Holds if `guard` suggests that this expression may be `null`. */
456435 predicate guardSuggestsMaybeNull ( Guards:: Guard guard ) {
457436 not nonNullValueImplied ( this ) and
458437 (
459- guard = this . getANullnessNullCheck ( _ , true )
438+ exists ( NullnessCompletion c | c . isValidFor ( this ) and c . isNull ( ) and guard = this )
460439 or
461440 LogicInput:: additionalNullCheck ( guard , _, this , true )
462441 or
@@ -513,8 +492,8 @@ class EnumerableCollectionExpr extends Expr {
513492 )
514493 }
515494
516- private Expr getABooleanEmptinessCheck ( BooleanValue v , boolean isEmpty ) {
517- exists ( boolean branch | branch = v .getValue ( ) |
495+ private Expr getABooleanEmptinessCheck ( GuardValue v , boolean isEmpty ) {
496+ exists ( boolean branch | branch = v .asBooleanValue ( ) |
518497 result =
519498 any ( ComparisonTest ct |
520499 exists ( boolean lowerBound |
@@ -578,7 +557,7 @@ class EnumerableCollectionExpr extends Expr {
578557 * For example, if the expression `x.Length != 0` evaluates to `true` then the
579558 * expression `x` is guaranteed to be non-empty.
580559 */
581- Expr getAnEmptinessCheck ( AbstractValue v , boolean isEmpty ) {
560+ Expr getAnEmptinessCheck ( GuardValue v , boolean isEmpty ) {
582561 result = this .getABooleanEmptinessCheck ( v , isEmpty )
583562 }
584563}
@@ -692,14 +671,14 @@ class GuardedExpr extends AccessOrCallExpr {
692671 * left-most qualifier, then so must the other (accessing the same SSA
693672 * variable).
694673 */
695- Guard getAGuard ( Expr sub , AbstractValue v ) { isGuardedByExpr ( this , result , sub , v ) }
674+ Guard getAGuard ( Expr sub , GuardValue v ) { isGuardedByExpr ( this , result , sub , v ) }
696675
697676 /**
698677 * Holds if this expression must have abstract value `v`. That is, this
699678 * expression is guarded by a structurally equal expression having abstract
700679 * value `v`.
701680 */
702- predicate mustHaveValue ( AbstractValue v ) {
681+ predicate mustHaveValue ( GuardValue v ) {
703682 exists ( Guard g | g = this .getAGuard ( g , v ) ) or ssaMustHaveValue ( this , v )
704683 }
705684
@@ -713,7 +692,7 @@ class GuardedExpr extends AccessOrCallExpr {
713692 * variable).
714693 */
715694 predicate isGuardedBy ( Expr cond , Expr sub , boolean b ) {
716- cond = this .getAGuard ( sub , any ( BooleanValue v | v .getValue ( ) = b ) )
695+ cond = this .getAGuard ( sub , any ( GuardValue v | v .asBooleanValue ( ) = b ) )
717696 }
718697}
719698
@@ -738,7 +717,7 @@ class GuardedExpr extends AccessOrCallExpr {
738717class GuardedControlFlowNode extends ControlFlow:: Nodes:: ElementNode {
739718 private Guard g ;
740719 private AccessOrCallExpr sub0 ;
741- private AbstractValue v0 ;
720+ private GuardValue v0 ;
742721
743722 GuardedControlFlowNode ( ) { g .controlsNode ( this , sub0 , v0 ) }
744723
@@ -753,7 +732,7 @@ class GuardedControlFlowNode extends ControlFlow::Nodes::ElementNode {
753732 * left-most qualifier, then so must the other (accessing the same SSA
754733 * variable).
755734 */
756- Guard getAGuard ( Expr sub , AbstractValue v ) {
735+ Guard getAGuard ( Expr sub , GuardValue v ) {
757736 result = g and
758737 sub = sub0 and
759738 v = v0
@@ -764,7 +743,7 @@ class GuardedControlFlowNode extends ControlFlow::Nodes::ElementNode {
764743 * control flow node is guarded by a structurally equal expression having
765744 * abstract value `v`.
766745 */
767- predicate mustHaveValue ( AbstractValue v ) { g = this .getAGuard ( g , v ) }
746+ predicate mustHaveValue ( GuardValue v ) { g = this .getAGuard ( g , v ) }
768747}
769748
770749/**
@@ -788,7 +767,7 @@ class GuardedControlFlowNode extends ControlFlow::Nodes::ElementNode {
788767class GuardedDataFlowNode extends DataFlow:: ExprNode {
789768 private Guard g ;
790769 private AccessOrCallExpr sub0 ;
791- private AbstractValue v0 ;
770+ private GuardValue v0 ;
792771
793772 GuardedDataFlowNode ( ) {
794773 exists ( ControlFlow:: Nodes:: ElementNode cfn | exists ( this .getExprAtNode ( cfn ) ) |
@@ -807,7 +786,7 @@ class GuardedDataFlowNode extends DataFlow::ExprNode {
807786 * left-most qualifier, then so must the other (accessing the same SSA
808787 * variable).
809788 */
810- Guard getAGuard ( Expr sub , AbstractValue v ) {
789+ Guard getAGuard ( Expr sub , GuardValue v ) {
811790 result = g and
812791 sub = sub0 and
813792 v = v0
@@ -818,17 +797,17 @@ class GuardedDataFlowNode extends DataFlow::ExprNode {
818797 * data flow node is guarded by a structurally equal expression having
819798 * abstract value `v`.
820799 */
821- predicate mustHaveValue ( AbstractValue v ) { g = this .getAGuard ( g , v ) }
800+ predicate mustHaveValue ( GuardValue v ) { g = this .getAGuard ( g , v ) }
822801}
823802
824803/** An expression guarded by a `null` check. */
825804class NullGuardedExpr extends GuardedExpr {
826- NullGuardedExpr ( ) { this .mustHaveValue ( any ( NullValue v | v .isNonNull ( ) ) ) }
805+ NullGuardedExpr ( ) { this .mustHaveValue ( any ( GuardValue v | v .isNonNullValue ( ) ) ) }
827806}
828807
829808/** A data flow node guarded by a `null` check. */
830809class NullGuardedDataFlowNode extends GuardedDataFlowNode {
831- NullGuardedDataFlowNode ( ) { this .mustHaveValue ( any ( NullValue v | v .isNonNull ( ) ) ) }
810+ NullGuardedDataFlowNode ( ) { this .mustHaveValue ( any ( GuardValue v | v .isNonNullValue ( ) ) ) }
832811}
833812
834813/** INTERNAL: Do not use. */
@@ -931,7 +910,7 @@ module Internal {
931910 bao .getAnOperand ( ) = o and
932911 // The other operand must be provably non-null in order
933912 // for `only if` to hold
934- o = any ( NullValue nv | nv . isNonNull ( ) ) . getAnExpr ( ) and
913+ nonNullValueImplied ( o ) and
935914 e != o
936915 )
937916 }
@@ -973,7 +952,7 @@ module Internal {
973952 nonEmptyValue ( def .getDefinition ( ) .getSource ( ) )
974953 }
975954
976- deprecated predicate isGuard ( Expr e , AbstractValue val ) {
955+ deprecated predicate isGuard ( Expr e , GuardValue val ) {
977956 (
978957 e .getType ( ) instanceof BoolType and
979958 not e instanceof BoolLiteral and
@@ -1207,7 +1186,7 @@ module Internal {
12071186 * Holds if basic block `bb` only is reached when guard `g` has abstract value `v`.
12081187 */
12091188 cached
1210- predicate guardControls ( Guard g , BasicBlock bb , AbstractValue v ) {
1189+ predicate guardControls ( Guard g , BasicBlock bb , GuardValue v ) {
12111190 g .( Guards:: Guard ) .valueControls ( bb , v )
12121191 }
12131192
@@ -1220,7 +1199,7 @@ module Internal {
12201199 pragma [ nomagic]
12211200 private predicate nodeIsGuardedBySameSubExpr0 (
12221201 ControlFlow:: Node guardedCfn , BasicBlock guardedBB , AccessOrCallExpr guarded , Guard g ,
1223- AccessOrCallExpr sub , AbstractValue v
1202+ AccessOrCallExpr sub , GuardValue v
12241203 ) {
12251204 Stages:: GuardsStage:: forceCachingInSameStage ( ) and
12261205 guardedCfn = guarded .getAControlFlowNode ( ) and
@@ -1233,7 +1212,7 @@ module Internal {
12331212 pragma [ nomagic]
12341213 private predicate nodeIsGuardedBySameSubExpr (
12351214 ControlFlow:: Node guardedCfn , BasicBlock guardedBB , AccessOrCallExpr guarded , Guard g ,
1236- AccessOrCallExpr sub , AbstractValue v
1215+ AccessOrCallExpr sub , GuardValue v
12371216 ) {
12381217 nodeIsGuardedBySameSubExpr0 ( guardedCfn , guardedBB , guarded , g , sub , v ) and
12391218 guardControlsSub ( g , guardedBB , sub )
@@ -1242,7 +1221,7 @@ module Internal {
12421221 pragma [ nomagic]
12431222 private predicate nodeIsGuardedBySameSubExprSsaDef0 (
12441223 ControlFlow:: Node cfn , BasicBlock guardedBB , AccessOrCallExpr guarded , Guard g ,
1245- ControlFlow:: Node subCfn , BasicBlock subCfnBB , AccessOrCallExpr sub , AbstractValue v ,
1224+ ControlFlow:: Node subCfn , BasicBlock subCfnBB , AccessOrCallExpr sub , GuardValue v ,
12461225 Ssa:: Definition def
12471226 ) {
12481227 nodeIsGuardedBySameSubExpr ( cfn , guardedBB , guarded , g , sub , v ) and
@@ -1253,7 +1232,7 @@ module Internal {
12531232 pragma [ nomagic]
12541233 private predicate nodeIsGuardedBySameSubExprSsaDef (
12551234 ControlFlow:: Node guardedCfn , AccessOrCallExpr guarded , Guard g , ControlFlow:: Node subCfn ,
1256- AccessOrCallExpr sub , AbstractValue v , Ssa:: Definition def
1235+ AccessOrCallExpr sub , GuardValue v , Ssa:: Definition def
12571236 ) {
12581237 exists ( BasicBlock guardedBB , BasicBlock subCfnBB |
12591238 nodeIsGuardedBySameSubExprSsaDef0 ( guardedCfn , guardedBB , guarded , g , subCfn , subCfnBB , sub ,
@@ -1264,17 +1243,15 @@ module Internal {
12641243
12651244 pragma [ noinline]
12661245 private predicate isGuardedByExpr0 (
1267- AccessOrCallExpr guarded , Guard g , AccessOrCallExpr sub , AbstractValue v
1246+ AccessOrCallExpr guarded , Guard g , AccessOrCallExpr sub , GuardValue v
12681247 ) {
12691248 forex ( ControlFlow:: Node cfn | cfn = guarded .getAControlFlowNode ( ) |
12701249 nodeIsGuardedBySameSubExpr ( cfn , _, guarded , g , sub , v )
12711250 )
12721251 }
12731252
12741253 cached
1275- predicate isGuardedByExpr (
1276- AccessOrCallExpr guarded , Guard g , AccessOrCallExpr sub , AbstractValue v
1277- ) {
1254+ predicate isGuardedByExpr ( AccessOrCallExpr guarded , Guard g , AccessOrCallExpr sub , GuardValue v ) {
12781255 isGuardedByExpr0 ( guarded , g , sub , v ) and
12791256 forall ( ControlFlow:: Node subCfn , Ssa:: Definition def |
12801257 nodeIsGuardedBySameSubExprSsaDef ( _, guarded , g , subCfn , sub , v , def )
@@ -1285,7 +1262,7 @@ module Internal {
12851262
12861263 cached
12871264 predicate isGuardedByNode (
1288- ControlFlow:: Nodes:: ElementNode guarded , Guard g , AccessOrCallExpr sub , AbstractValue v
1265+ ControlFlow:: Nodes:: ElementNode guarded , Guard g , AccessOrCallExpr sub , GuardValue v
12891266 ) {
12901267 nodeIsGuardedBySameSubExpr ( guarded , _, _, g , sub , v ) and
12911268 forall ( ControlFlow:: Node subCfn , Ssa:: Definition def |
0 commit comments