@@ -465,7 +465,7 @@ private class StructCanonicalPath extends MkStructCanonicalPath {
465
465
}
466
466
467
467
/** Content stored in a field on a struct. */
468
- private class StructFieldContent extends VariantContent , TStructFieldContent {
468
+ private class StructFieldContent extends Content , TStructFieldContent {
469
469
private StructCanonicalPath s ;
470
470
private string field_ ;
471
471
@@ -482,7 +482,7 @@ private class StructFieldContent extends VariantContent, TStructFieldContent {
482
482
* NOTE: Unlike `struct`s and `enum`s tuples are structural and not nominal,
483
483
* hence we don't store a canonical path for them.
484
484
*/
485
- private class TuplePositionContent extends VariantContent , TTuplePositionContent {
485
+ private class TuplePositionContent extends Content , TTuplePositionContent {
486
486
private int pos ;
487
487
488
488
TuplePositionContent ( ) { this = TTuplePositionContent ( pos ) }
@@ -492,6 +492,11 @@ private class TuplePositionContent extends VariantContent, TTuplePositionContent
492
492
override string toString ( ) { result = "tuple." + pos .toString ( ) }
493
493
}
494
494
495
+ /** Holds if `access` indexes a tuple at an index corresponding to `c`. */
496
+ private predicate fieldTuplePositionContent ( FieldExprCfgNode access , TuplePositionContent c ) {
497
+ access .getNameRef ( ) .getText ( ) .toInt ( ) = c .getPosition ( )
498
+ }
499
+
495
500
/** A value that represents a set of `Content`s. */
496
501
abstract class ContentSet extends TContentSet {
497
502
/** Gets a textual representation of this element. */
@@ -687,7 +692,7 @@ module RustDataFlow implements InputSig<Location> {
687
692
pathResolveToVariantCanonicalPath ( p .getPath ( ) , v )
688
693
}
689
694
690
- /** Holds if `p` destructs an struct `s`. */
695
+ /** Holds if `p` destructs a struct `s`. */
691
696
pragma [ nomagic]
692
697
private predicate structDestruction ( RecordPat p , StructCanonicalPath s ) {
693
698
pathResolveToStructCanonicalPath ( p .getPath ( ) , s )
@@ -722,7 +727,7 @@ module RustDataFlow implements InputSig<Location> {
722
727
or
723
728
exists ( FieldExprCfgNode access |
724
729
// Read of a tuple entry
725
- access . getNameRef ( ) . getText ( ) . toInt ( ) = c . ( TuplePositionContent ) . getPosition ( ) and
730
+ fieldTuplePositionContent ( access , c ) and
726
731
// TODO: Handle read of a struct field.
727
732
node1 .asExpr ( ) = access .getExpr ( ) and
728
733
node2 .asExpr ( ) = access
@@ -742,7 +747,7 @@ module RustDataFlow implements InputSig<Location> {
742
747
pathResolveToVariantCanonicalPath ( re .getPath ( ) , v )
743
748
}
744
749
745
- /** Holds if `re` constructs a struct value of type `v `. */
750
+ /** Holds if `re` constructs a struct value of type `s `. */
746
751
pragma [ nomagic]
747
752
private predicate structConstruction ( RecordExpr re , StructCanonicalPath s ) {
748
753
pathResolveToStructCanonicalPath ( re .getPath ( ) , s )
@@ -780,6 +785,13 @@ module RustDataFlow implements InputSig<Location> {
780
785
node1 .asExpr ( ) = tuple .getField ( c .( TuplePositionContent ) .getPosition ( ) ) and
781
786
node2 .asExpr ( ) = tuple
782
787
)
788
+ 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
+ )
783
795
)
784
796
}
785
797
@@ -788,12 +800,11 @@ module RustDataFlow implements InputSig<Location> {
788
800
* any value stored inside `f` is cleared at the pre-update node associated with `x`
789
801
* in `x.f = newValue`.
790
802
*/
791
- predicate clearsContent ( Node n , ContentSet c ) {
803
+ predicate clearsContent ( Node n , ContentSet cs ) {
792
804
exists ( AssignmentExprCfgNode assignment , FieldExprCfgNode access |
793
805
assignment .getLhs ( ) = access and
794
806
n .asExpr ( ) = access .getExpr ( ) and
795
- access .getNameRef ( ) .getText ( ) .toInt ( ) =
796
- c .( SingletonContentSet ) .getContent ( ) .( TuplePositionContent ) .getPosition ( )
807
+ fieldTuplePositionContent ( access , cs .( SingletonContentSet ) .getContent ( ) )
797
808
)
798
809
}
799
810
0 commit comments