@@ -252,10 +252,10 @@ module Node {
252252 * Nodes corresponding to AST elements, for example `ExprNode`, usually refer
253253 * to the value before the update.
254254 */
255- final class PostUpdateNode extends Node , TArgumentPostUpdateNode {
255+ final class PostUpdateNode extends Node , TExprPostUpdateNode {
256256 private ExprCfgNode n ;
257257
258- PostUpdateNode ( ) { this = TArgumentPostUpdateNode ( n ) }
258+ PostUpdateNode ( ) { this = TExprPostUpdateNode ( n ) }
259259
260260 /** Gets the node before the state update. */
261261 Node getPreUpdateNode ( ) { result = TExprNode ( n ) }
@@ -449,6 +449,49 @@ private class VariantFieldContent extends VariantContent, TVariantFieldContent {
449449 }
450450}
451451
452+ /** A canonical path pointing to a struct. */
453+ private class StructCanonicalPath extends MkStructCanonicalPath {
454+ CrateOriginOption crate ;
455+ string path ;
456+
457+ StructCanonicalPath ( ) { this = MkStructCanonicalPath ( crate , path ) }
458+
459+ /** Gets the underlying struct. */
460+ Struct getStruct ( ) { hasExtendedCanonicalPath ( result , crate , path ) }
461+
462+ string toString ( ) { result = this .getStruct ( ) .getName ( ) .getText ( ) }
463+
464+ Location getLocation ( ) { result = this .getStruct ( ) .getLocation ( ) }
465+ }
466+
467+ /** Content stored in a field on a struct. */
468+ private class StructFieldContent extends VariantContent , TStructFieldContent {
469+ private StructCanonicalPath s ;
470+ private string field_ ;
471+
472+ StructFieldContent ( ) { this = TStructFieldContent ( s , field_ ) }
473+
474+ StructCanonicalPath getStructCanonicalPath ( string field ) { result = s and field = field_ }
475+
476+ override string toString ( ) { result = s .toString ( ) + "." + field_ .toString ( ) }
477+ }
478+
479+ /**
480+ * Content stored at a position in a tuple.
481+ *
482+ * NOTE: Unlike `struct`s and `enum`s tuples are structural and not nominal,
483+ * hence we don't store a canonical path for them.
484+ */
485+ private class TuplePositionContent extends VariantContent , TTuplePositionContent {
486+ private int pos ;
487+
488+ TuplePositionContent ( ) { this = TTuplePositionContent ( pos ) }
489+
490+ int getPosition ( ) { result = pos }
491+
492+ override string toString ( ) { result = "tuple." + pos .toString ( ) }
493+ }
494+
452495/** A value that represents a set of `Content`s. */
453496abstract class ContentSet extends TContentSet {
454497 /** Gets a textual representation of this element. */
@@ -608,6 +651,14 @@ module RustDataFlow implements InputSig<Location> {
608651 */
609652 predicate jumpStep ( Node node1 , Node node2 ) { none ( ) }
610653
654+ /** Holds if path `p` resolves to struct `s`. */
655+ private predicate pathResolveToStructCanonicalPath ( Path p , StructCanonicalPath s ) {
656+ exists ( CrateOriginOption crate , string path |
657+ resolveExtendedCanonicalPath ( p , crate , path ) and
658+ s = MkStructCanonicalPath ( crate , path )
659+ )
660+ }
661+
611662 /** Holds if path `p` resolves to variant `v`. */
612663 private predicate pathResolveToVariantCanonicalPath ( Path p , VariantCanonicalPath v ) {
613664 exists ( CrateOriginOption crate , string path |
@@ -636,6 +687,12 @@ module RustDataFlow implements InputSig<Location> {
636687 pathResolveToVariantCanonicalPath ( p .getPath ( ) , v )
637688 }
638689
690+ /** Holds if `p` destructs an struct `s`. */
691+ pragma [ nomagic]
692+ private predicate structDestruction ( RecordPat p , StructCanonicalPath s ) {
693+ pathResolveToStructCanonicalPath ( p .getPath ( ) , s )
694+ }
695+
639696 /**
640697 * Holds if data can flow from `node1` to `node2` via a read of `c`. Thus,
641698 * `node1` references an object with a content `c.getAReadContent()` whose
@@ -652,10 +709,24 @@ module RustDataFlow implements InputSig<Location> {
652709 or
653710 exists ( RecordPatCfgNode pat , string field |
654711 pat = node1 .asPat ( ) and
655- recordVariantDestruction ( pat .getPat ( ) ,
656- c .( VariantFieldContent ) .getVariantCanonicalPath ( field ) ) and
712+ (
713+ // Pattern destructs a struct-like variant.
714+ recordVariantDestruction ( pat .getPat ( ) ,
715+ c .( VariantFieldContent ) .getVariantCanonicalPath ( field ) )
716+ or
717+ // Pattern destructs a struct.
718+ structDestruction ( pat .getPat ( ) , c .( StructFieldContent ) .getStructCanonicalPath ( field ) )
719+ ) and
657720 node2 .asPat ( ) = pat .getFieldPat ( field )
658721 )
722+ or
723+ exists ( FieldExprCfgNode access |
724+ // Read of a tuple entry
725+ access .getNameRef ( ) .getText ( ) .toInt ( ) = c .( TuplePositionContent ) .getPosition ( ) and
726+ // TODO: Handle read of a struct field.
727+ node1 .asExpr ( ) = access .getExpr ( ) and
728+ node2 .asExpr ( ) = access
729+ )
659730 )
660731 }
661732
@@ -671,30 +742,44 @@ module RustDataFlow implements InputSig<Location> {
671742 pathResolveToVariantCanonicalPath ( re .getPath ( ) , v )
672743 }
673744
745+ /** Holds if `re` constructs a struct value of type `v`. */
746+ pragma [ nomagic]
747+ private predicate structConstruction ( RecordExpr re , StructCanonicalPath s ) {
748+ pathResolveToStructCanonicalPath ( re .getPath ( ) , s )
749+ }
750+
674751 /**
675752 * Holds if data can flow from `node1` to `node2` via a store into `c`. Thus,
676753 * `node2` references an object with a content `c.getAStoreContent()` that
677754 * contains the value of `node1`.
678755 */
679756 predicate storeStep ( Node node1 , ContentSet cs , Node node2 ) {
680757 exists ( Content c | c = cs .( SingletonContentSet ) .getContent ( ) |
681- node2 .asExpr ( ) =
682- any ( CallExprCfgNode call , int pos |
683- tupleVariantConstruction ( call .getCallExpr ( ) ,
684- c .( VariantPositionContent ) .getVariantCanonicalPath ( pos ) ) and
685- node1 .asExpr ( ) = call .getArgument ( pos )
686- |
687- call
688- )
758+ exists ( CallExprCfgNode call , int pos |
759+ tupleVariantConstruction ( call .getCallExpr ( ) ,
760+ c .( VariantPositionContent ) .getVariantCanonicalPath ( pos ) ) and
761+ node1 .asExpr ( ) = call .getArgument ( pos ) and
762+ node2 .asExpr ( ) = call
763+ )
689764 or
690- node2 .asExpr ( ) =
691- any ( RecordExprCfgNode re , string field |
765+ exists ( RecordExprCfgNode re , string field |
766+ (
767+ // Expression is for a struct-like enum variant.
692768 recordVariantConstruction ( re .getRecordExpr ( ) ,
693- c .( VariantFieldContent ) .getVariantCanonicalPath ( field ) ) and
694- node1 .asExpr ( ) = re .getFieldExpr ( field )
695- |
696- re
697- )
769+ c .( VariantFieldContent ) .getVariantCanonicalPath ( field ) )
770+ or
771+ // Expression is for a struct.
772+ structConstruction ( re .getRecordExpr ( ) ,
773+ c .( StructFieldContent ) .getStructCanonicalPath ( field ) )
774+ ) and
775+ node1 .asExpr ( ) = re .getFieldExpr ( field ) and
776+ node2 .asExpr ( ) = re
777+ )
778+ or
779+ exists ( TupleExprCfgNode tuple |
780+ node1 .asExpr ( ) = tuple .getField ( c .( TuplePositionContent ) .getPosition ( ) ) and
781+ node2 .asExpr ( ) = tuple
782+ )
698783 )
699784 }
700785
@@ -703,7 +788,14 @@ module RustDataFlow implements InputSig<Location> {
703788 * any value stored inside `f` is cleared at the pre-update node associated with `x`
704789 * in `x.f = newValue`.
705790 */
706- predicate clearsContent ( Node n , ContentSet c ) { none ( ) }
791+ predicate clearsContent ( Node n , ContentSet c ) {
792+ exists ( AssignmentExprCfgNode assignment , FieldExprCfgNode access |
793+ assignment .getLhs ( ) = access and
794+ n .asExpr ( ) = access .getExpr ( ) and
795+ access .getNameRef ( ) .getText ( ) .toInt ( ) =
796+ c .( SingletonContentSet ) .getContent ( ) .( TuplePositionContent ) .getPosition ( )
797+ )
798+ }
707799
708800 /**
709801 * Holds if the value that is being tracked is expected to be stored inside content `c`
@@ -773,7 +865,9 @@ private module Cached {
773865 TExprNode ( ExprCfgNode n ) or
774866 TParameterNode ( ParamBaseCfgNode p ) or
775867 TPatNode ( PatCfgNode p ) or
776- TArgumentPostUpdateNode ( ExprCfgNode e ) { isArgumentForCall ( e , _, _) } or
868+ TExprPostUpdateNode ( ExprCfgNode e ) {
869+ isArgumentForCall ( e , _, _) or e = any ( FieldExprCfgNode access ) .getExpr ( )
870+ } or
777871 TSsaNode ( SsaImpl:: DataFlowIntegration:: SsaNode node )
778872
779873 cached
@@ -811,6 +905,12 @@ private module Cached {
811905 name = [ "Ok" , "Err" ]
812906 }
813907
908+ cached
909+ newtype TStructCanonicalPath =
910+ MkStructCanonicalPath ( CrateOriginOption crate , string path ) {
911+ exists ( Struct s | hasExtendedCanonicalPath ( s , crate , path ) )
912+ }
913+
814914 cached
815915 newtype TContent =
816916 TVariantPositionContent ( VariantCanonicalPath v , int pos ) {
@@ -826,6 +926,16 @@ private module Cached {
826926 } or
827927 TVariantFieldContent ( VariantCanonicalPath v , string field ) {
828928 field = v .getVariant ( ) .getFieldList ( ) .( RecordFieldList ) .getAField ( ) .getName ( ) .getText ( )
929+ } or
930+ TTuplePositionContent ( int pos ) {
931+ pos in [ 0 .. max ( [
932+ any ( TuplePat pat ) .getNumberOfFields ( ) ,
933+ any ( FieldExpr access ) .getNameRef ( ) .getText ( ) .toInt ( )
934+ ]
935+ ) ]
936+ } or
937+ TStructFieldContent ( StructCanonicalPath s , string field ) {
938+ field = s .getStruct ( ) .getFieldList ( ) .( RecordFieldList ) .getAField ( ) .getName ( ) .getText ( )
829939 }
830940
831941 cached
0 commit comments