@@ -430,6 +430,7 @@ 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
433434 not this instanceof NoNodeExpr and
434435 not this instanceof SwitchExpr and
435436 not this instanceof SwitchCaseExpr and
@@ -491,6 +492,93 @@ module Expressions {
491492 }
492493 }
493494
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
564+ first ( getExprChild ( this , i + 1 ) , succ )
565+ )
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+ )
579+ }
580+ }
581+
494582 /**
495583 * An expression that writes via an accessor, for example `x.Prop = 0`,
496584 * where `Prop` is a property.
@@ -516,6 +604,7 @@ module Expressions {
516604 QualifiedAccessorWrite ( ) {
517605 def .getExpr ( ) = this and
518606 def .getTargetAccess ( ) .( WriteAccess ) instanceof QualifiableExpr and
607+ not def instanceof AssignableDefinitions:: OutRefDefinition and
519608 not this instanceof AssignOperationWithExpandedAssignment
520609 }
521610
0 commit comments