@@ -429,7 +429,7 @@ module Expressions {
429429 not this instanceof ObjectCreation and
430430 not this instanceof ArrayCreation and
431431 not this instanceof QualifiedWriteAccess and
432- not this instanceof AccessorWrite and
432+ not this instanceof QualifiedAccessorWrite and
433433 not this instanceof NoNodeExpr and
434434 not this instanceof SwitchExpr and
435435 not this instanceof SwitchCaseExpr and
@@ -446,21 +446,29 @@ module Expressions {
446446 }
447447
448448 /**
449- * A qualified write access. In a qualified write access, the access itself is
450- * not evaluated, only the qualifier and the indexer arguments (if any).
449+ * A qualified write access.
450+ *
451+ * The successor declaration in `QualifiedAccessorWrite` ensures that the access itself
452+ * is evaluated after the qualifier and the indexer arguments (if any)
453+ * and the right hand side of the assignment.
454+ *
455+ * When a qualified write access is used as an `out/ref` argument, the access itself is evaluated immediately.
451456 */
452457 private class QualifiedWriteAccess extends ControlFlowTree instanceof WriteAccess , QualifiableExpr
453458 {
454459 QualifiedWriteAccess ( ) {
455- this .hasQualifier ( )
456- or
457- // Member initializers like
458- // ```csharp
459- // new Dictionary<int, string>() { [0] = "Zero", [1] = "One", [2] = "Two" }
460- // ```
461- // need special treatment, because the accesses `[0]`, `[1]`, and `[2]`
462- // have no qualifier.
463- this = any ( MemberInitializer mi ) .getLValue ( )
460+ (
461+ this .hasQualifier ( )
462+ or
463+ // Member initializers like
464+ // ```csharp
465+ // new Dictionary<int, string>() { [0] = "Zero", [1] = "One", [2] = "Two" }
466+ // ```
467+ // need special treatment, because the accesses `[0]`, `[1]`, and `[2]`
468+ // have no qualifier.
469+ this = any ( MemberInitializer mi ) .getLValue ( )
470+ ) and
471+ not exists ( AssignableDefinitions:: OutRefDefinition def | def .getTargetAccess ( ) = this )
464472 }
465473
466474 final override predicate propagatesAbnormal ( AstNode child ) { child = getExprChild ( this , _) }
@@ -470,25 +478,25 @@ module Expressions {
470478 final override predicate last ( AstNode last , Completion c ) {
471479 // Skip the access in a qualified write access
472480 last ( getLastExprChild ( this ) , last , c )
481+ or
482+ // Qualifier exits with a null completion
483+ super .isConditional ( ) and
484+ last ( super .getQualifier ( ) , last , c ) and
485+ c .( NullnessCompletion ) .isNull ( )
473486 }
474487
475488 final override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
476489 exists ( int i |
477490 last ( getExprChild ( this , i ) , pred , c ) and
478491 c instanceof NormalCompletion and
492+ ( if i = 0 then not c .( NullnessCompletion ) .isNull ( ) else any ( ) ) and
479493 first ( getExprChild ( this , i + 1 ) , succ )
480494 )
481495 }
482496 }
483497
484- private class StatOrDynAccessorCall_ =
485- @dynamic_member_access_expr or @dynamic_element_access_expr or @call_access_expr;
486-
487- /** A normal or a (potential) dynamic call to an accessor. */
488- private class StatOrDynAccessorCall extends Expr , StatOrDynAccessorCall_ { }
489-
490498 /**
491- * An expression that writes via an accessor call , for example `x.Prop = 0`,
499+ * An expression that writes via a qualifiable expression , for example `x.Prop = 0`,
492500 * where `Prop` is a property.
493501 *
494502 * Accessor writes need special attention, because we need to model the fact
@@ -498,24 +506,33 @@ module Expressions {
498506 * ```csharp
499507 * x -> 0 -> set_Prop -> x.Prop = 0
500508 * ```
509+ *
510+ * For consistency, control flow is implemented the same way for other qualified writes.
511+ * For example, `x.Field = 0`, where `Field` is a field, we want a CFG that looks like
512+ *
513+ * ```csharp
514+ * x -> 0 -> x.Field -> x.Field = 0
515+ * ```
501516 */
502- class AccessorWrite extends PostOrderTree instanceof Expr {
517+ private class QualifiedAccessorWrite extends PostOrderTree instanceof Expr {
503518 AssignableDefinition def ;
504519
505- AccessorWrite ( ) {
520+ QualifiedAccessorWrite ( ) {
506521 def .getExpr ( ) = this and
507- def .getTargetAccess ( ) .( WriteAccess ) instanceof StatOrDynAccessorCall and
522+ def .getTargetAccess ( ) .( WriteAccess ) instanceof QualifiableExpr and
523+ not def instanceof AssignableDefinitions:: OutRefDefinition and
508524 not this instanceof AssignOperationWithExpandedAssignment
509525 }
510526
511527 /**
512528 * Gets the `i`th accessor being called in this write. More than one call
513529 * can happen in tuple assignments.
514530 */
515- StatOrDynAccessorCall getCall ( int i ) {
531+ QualifiableExpr getAccess ( int i ) {
516532 result =
517533 rank [ i + 1 ] ( AssignableDefinitions:: TupleAssignmentDefinition tdef |
518- tdef .getExpr ( ) = this and tdef .getTargetAccess ( ) instanceof StatOrDynAccessorCall
534+ tdef .getExpr ( ) = this and
535+ tdef .getTargetAccess ( ) instanceof QualifiableExpr
519536 |
520537 tdef order by tdef .getEvaluationOrder ( )
521538 ) .getTargetAccess ( )
@@ -528,7 +545,13 @@ module Expressions {
528545 final override predicate propagatesAbnormal ( AstNode child ) {
529546 child = getExprChild ( this , _)
530547 or
531- child = this .getCall ( _)
548+ child = this .getAccess ( _)
549+ }
550+
551+ final override predicate last ( AstNode last , Completion c ) {
552+ PostOrderTree .super .last ( last , c )
553+ or
554+ last ( getExprChild ( this , 0 ) , last , c ) and c .( NullnessCompletion ) .isNull ( )
532555 }
533556
534557 final override predicate first ( AstNode first ) { first ( getExprChild ( this , 0 ) , first ) }
@@ -538,24 +561,25 @@ module Expressions {
538561 exists ( int i |
539562 last ( getExprChild ( this , i ) , pred , c ) and
540563 c instanceof NormalCompletion and
564+ ( if i = 0 then not c .( NullnessCompletion ) .isNull ( ) else any ( ) ) and
541565 first ( getExprChild ( this , i + 1 ) , succ )
542566 )
543567 or
544568 // Flow from last element of last child to first accessor call
545569 last ( getLastExprChild ( this ) , pred , c ) and
546- succ = this .getCall ( 0 ) and
570+ succ = this .getAccess ( 0 ) and
547571 c instanceof NormalCompletion
548572 or
549573 // Flow from one call to the next
550- exists ( int i | pred = this .getCall ( i ) |
551- succ = this .getCall ( i + 1 ) and
574+ exists ( int i | pred = this .getAccess ( i ) |
575+ succ = this .getAccess ( i + 1 ) and
552576 c .isValidFor ( pred ) and
553577 c instanceof NormalCompletion
554578 )
555579 or
556580 // Post-order: flow from last call to element itself
557- exists ( int last | last = max ( int i | exists ( this .getCall ( i ) ) ) |
558- pred = this .getCall ( last ) and
581+ exists ( int last | last = max ( int i | exists ( this .getAccess ( i ) ) ) |
582+ pred = this .getAccess ( last ) and
559583 succ = this and
560584 c .isValidFor ( pred ) and
561585 c instanceof NormalCompletion
@@ -704,7 +728,9 @@ module Expressions {
704728 private class ConditionallyQualifiedExpr extends PostOrderTree instanceof QualifiableExpr {
705729 private Expr qualifier ;
706730
707- ConditionallyQualifiedExpr ( ) { this .isConditional ( ) and qualifier = getExprChild ( this , 0 ) }
731+ ConditionallyQualifiedExpr ( ) {
732+ this .isConditional ( ) and qualifier = getExprChild ( this , 0 ) and not this instanceof WriteAccess
733+ }
708734
709735 final override predicate propagatesAbnormal ( AstNode child ) { child = qualifier }
710736
0 commit comments