@@ -430,7 +430,6 @@ module Expressions {
430430 not this instanceof ArrayCreation and
431431 not this instanceof QualifiedWriteAccess and
432432 not this instanceof QualifiedAccessorWrite and
433- not this instanceof QualifiedAccessorWriteOutParam and
434433 not this instanceof NoNodeExpr and
435434 not this instanceof SwitchExpr and
436435 not this instanceof SwitchCaseExpr and
@@ -447,25 +446,29 @@ module Expressions {
447446 }
448447
449448 /**
450- * A qualified write access. In a qualified write access, the access itself is
451- * not evaluated, only the qualifier and the indexer arguments (if any).
449+ * A qualified write access.
452450 *
453- * Note that the successor declaration in `QualifiedAccessorWrite` ensures that the access itself
451+ * The successor declaration in `QualifiedAccessorWrite` ensures that the access itself
454452 * is evaluated after the qualifier and the indexer arguments (if any)
455453 * 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.
456456 */
457457 private class QualifiedWriteAccess extends ControlFlowTree instanceof WriteAccess , QualifiableExpr
458458 {
459459 QualifiedWriteAccess ( ) {
460- this .hasQualifier ( )
461- or
462- // Member initializers like
463- // ```csharp
464- // new Dictionary<int, string>() { [0] = "Zero", [1] = "One", [2] = "Two" }
465- // ```
466- // need special treatment, because the accesses `[0]`, `[1]`, and `[2]`
467- // have no qualifier.
468- 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 )
469472 }
470473
471474 final override predicate propagatesAbnormal ( AstNode child ) { child = getExprChild ( this , _) }
@@ -486,101 +489,14 @@ module Expressions {
486489 exists ( int i |
487490 last ( getExprChild ( this , i ) , pred , c ) and
488491 c instanceof NormalCompletion and
489- ( i != 0 or not c .( NullnessCompletion ) .isNull ( ) ) and
490- first ( getExprChild ( this , i + 1 ) , succ )
491- )
492- }
493- }
494-
495- /**
496- * An expression that writes via an accessor in an `out` parameter, for example `s = M(out x.Field)`,
497- * where `Field` is a field.
498- *
499- * Note that `ref` parameters are not included here as they are considered reads before the call.
500- * Ideally, we would model `ref` parameters as both reads and writes, but that is not currently supported.
501- *
502- * Accessor writes need special attention, because we need to model that the
503- * access is written after the method call.
504- *
505- * In the example above, this means we want a CFG that looks like
506- *
507- * ```csharp
508- * x -> call M -> x.Field -> s = M(out x.Field)
509- * ```
510- */
511- private class QualifiedAccessorWriteOutParam extends PostOrderTree instanceof Expr {
512- QualifiedAccessorWriteOutParam ( ) {
513- exists ( AssignableDefinitions:: OutRefDefinition def |
514- def .getExpr ( ) = this and
515- def .getTargetAccess ( ) instanceof QualifiableExpr and
516- def .getTargetAccess ( ) .isOutArgument ( )
517- )
518- }
519-
520- private QualifiableExpr getOutAccess ( int i ) {
521- result =
522- rank [ i + 1 ] ( AssignableDefinitions:: OutRefDefinition def |
523- def .getExpr ( ) = this and
524- def .getTargetAccess ( ) instanceof QualifiableExpr and
525- def .getTargetAccess ( ) .isOutArgument ( )
526- |
527- def order by def .getIndex ( )
528- ) .getTargetAccess ( )
529- }
530-
531- private QualifiableExpr getLastOutAccess ( ) {
532- exists ( int last |
533- result = this .getOutAccess ( last ) and
534- not exists ( this .getOutAccess ( last + 1 ) )
535- )
536- }
537-
538- final override predicate propagatesAbnormal ( AstNode child ) { child = getExprChild ( this , _) }
539-
540- final override predicate first ( AstNode first ) {
541- first ( getExprChild ( this , 0 ) , first )
542- or
543- not exists ( getExprChild ( this , 0 ) ) and
544- first = this
545- }
546-
547- final override predicate last ( AstNode last , Completion c ) {
548- // The last ast node is the last out writeaccess.
549- // Completion from the call itself is propagated (required for eg. conditions).
550- last = this .getLastOutAccess ( ) and
551- c .isValidFor ( this )
552- }
553-
554- final override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
555- exists ( int i |
556- last ( getExprChild ( this , i ) , pred , c ) and
557- c instanceof NormalCompletion
558- |
559- // Post-order: flow from last element of last child to element itself
560- i = max ( int j | exists ( getExprChild ( this , j ) ) ) and
561- succ = this
562- or
563- // Standard left-to-right evaluation
492+ ( if i = 0 then not c .( NullnessCompletion ) .isNull ( ) else any ( ) ) and
564493 first ( getExprChild ( this , i + 1 ) , succ )
565494 )
566- or
567- // Flow from this element to the first write access.
568- pred = this and
569- succ = this .getOutAccess ( 0 ) and
570- c .isValidFor ( pred ) and
571- c instanceof NormalCompletion
572- or
573- // Flow from one access to the next
574- exists ( int i | pred = this .getOutAccess ( i ) |
575- succ = this .getOutAccess ( i + 1 ) and
576- c .isValidFor ( pred ) and
577- c instanceof NormalCompletion
578- )
579495 }
580496 }
581497
582498 /**
583- * An expression that writes via an accessor , for example `x.Prop = 0`,
499+ * An expression that writes via a qualifiable expression , for example `x.Prop = 0`,
584500 * where `Prop` is a property.
585501 *
586502 * Accessor writes need special attention, because we need to model the fact
@@ -591,7 +507,7 @@ module Expressions {
591507 * x -> 0 -> set_Prop -> x.Prop = 0
592508 * ```
593509 *
594- * For consistency, control flow is implemented this way for all accessor writes.
510+ * For consistency, control flow is implemented the same way for other qualified writes.
595511 * For example, `x.Field = 0`, where `Field` is a field, we want a CFG that looks like
596512 *
597513 * ```csharp
@@ -645,7 +561,7 @@ module Expressions {
645561 exists ( int i |
646562 last ( getExprChild ( this , i ) , pred , c ) and
647563 c instanceof NormalCompletion and
648- ( i ! = 0 or not c .( NullnessCompletion ) .isNull ( ) ) and
564+ ( if i = 0 then not c .( NullnessCompletion ) .isNull ( ) else any ( ) ) and
649565 first ( getExprChild ( this , i + 1 ) , succ )
650566 )
651567 or
0 commit comments