@@ -260,11 +260,13 @@ module Node {
260260 /** Gets the node before the state update. */
261261 Node getPreUpdateNode ( ) { result = TExprNode ( n ) }
262262
263+ override ExprCfgNode asExpr ( ) { result = n }
264+
263265 final override CfgScope getCfgScope ( ) { result = n .getScope ( ) }
264266
265267 final override Location getLocation ( ) { result = n .getLocation ( ) }
266268
267- final override string toString ( ) { result = n .toString ( ) }
269+ final override string toString ( ) { result = "[post] " + n .toString ( ) }
268270 }
269271
270272 final class CastNode = NaNode ;
@@ -286,6 +288,8 @@ module SsaFlow {
286288 or
287289 result .( SsaFlow:: ExprNode ) .getExpr ( ) = n .asExpr ( )
288290 or
291+ result .( SsaFlow:: ExprPostUpdateNode ) .getExpr ( ) = n .( Node:: PostUpdateNode ) .asExpr ( )
292+ or
289293 n = toParameterNode ( result .( SsaFlow:: ParameterNode ) .getParameter ( ) )
290294 }
291295
@@ -753,6 +757,15 @@ module RustDataFlow implements InputSig<Location> {
753757 pathResolveToStructCanonicalPath ( re .getPath ( ) , s )
754758 }
755759
760+ private predicate tupleAssignment ( Node node1 , Node node2 , TuplePositionContent c ) {
761+ exists ( AssignmentExprCfgNode assignment , FieldExprCfgNode access |
762+ assignment .getLhs ( ) = access and
763+ fieldTuplePositionContent ( access , c ) and
764+ node1 .asExpr ( ) = assignment .getRhs ( ) and
765+ node2 .asExpr ( ) = access .getExpr ( )
766+ )
767+ }
768+
756769 /**
757770 * Holds if data can flow from `node1` to `node2` via a store into `c`. Thus,
758771 * `node2` references an object with a content `c.getAStoreContent()` that
@@ -786,12 +799,7 @@ module RustDataFlow implements InputSig<Location> {
786799 node2 .asExpr ( ) = tuple
787800 )
788801 or
789- exists ( AssignmentExprCfgNode assignment , FieldExprCfgNode access |
790- assignment .getLhs ( ) = access and
791- fieldTuplePositionContent ( access , c ) and
792- node1 .asExpr ( ) = assignment .getRhs ( ) and
793- node2 .asExpr ( ) = access .getExpr ( )
794- )
802+ tupleAssignment ( node1 , node2 .( PostUpdateNode ) , c )
795803 )
796804 }
797805
@@ -801,11 +809,7 @@ module RustDataFlow implements InputSig<Location> {
801809 * in `x.f = newValue`.
802810 */
803811 predicate clearsContent ( Node n , ContentSet cs ) {
804- exists ( AssignmentExprCfgNode assignment , FieldExprCfgNode access |
805- assignment .getLhs ( ) = access and
806- n .asExpr ( ) = access .getExpr ( ) and
807- fieldTuplePositionContent ( access , cs .( SingletonContentSet ) .getContent ( ) )
808- )
812+ tupleAssignment ( _, n , cs .( SingletonContentSet ) .getContent ( ) )
809813 }
810814
811815 /**
0 commit comments