@@ -465,7 +465,7 @@ private class StructCanonicalPath extends MkStructCanonicalPath {
465465}
466466
467467/** Content stored in a field on a struct. */
468- private class StructFieldContent extends VariantContent , TStructFieldContent {
468+ private class StructFieldContent extends Content , TStructFieldContent {
469469 private StructCanonicalPath s ;
470470 private string field_ ;
471471
@@ -482,7 +482,7 @@ private class StructFieldContent extends VariantContent, TStructFieldContent {
482482 * NOTE: Unlike `struct`s and `enum`s tuples are structural and not nominal,
483483 * hence we don't store a canonical path for them.
484484 */
485- private class TuplePositionContent extends VariantContent , TTuplePositionContent {
485+ private class TuplePositionContent extends Content , TTuplePositionContent {
486486 private int pos ;
487487
488488 TuplePositionContent ( ) { this = TTuplePositionContent ( pos ) }
@@ -492,6 +492,11 @@ private class TuplePositionContent extends VariantContent, TTuplePositionContent
492492 override string toString ( ) { result = "tuple." + pos .toString ( ) }
493493}
494494
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+
495500/** A value that represents a set of `Content`s. */
496501abstract class ContentSet extends TContentSet {
497502 /** Gets a textual representation of this element. */
@@ -687,7 +692,7 @@ module RustDataFlow implements InputSig<Location> {
687692 pathResolveToVariantCanonicalPath ( p .getPath ( ) , v )
688693 }
689694
690- /** Holds if `p` destructs an struct `s`. */
695+ /** Holds if `p` destructs a struct `s`. */
691696 pragma [ nomagic]
692697 private predicate structDestruction ( RecordPat p , StructCanonicalPath s ) {
693698 pathResolveToStructCanonicalPath ( p .getPath ( ) , s )
@@ -722,7 +727,7 @@ module RustDataFlow implements InputSig<Location> {
722727 or
723728 exists ( FieldExprCfgNode access |
724729 // Read of a tuple entry
725- access . getNameRef ( ) . getText ( ) . toInt ( ) = c . ( TuplePositionContent ) . getPosition ( ) and
730+ fieldTuplePositionContent ( access , c ) and
726731 // TODO: Handle read of a struct field.
727732 node1 .asExpr ( ) = access .getExpr ( ) and
728733 node2 .asExpr ( ) = access
@@ -742,7 +747,7 @@ module RustDataFlow implements InputSig<Location> {
742747 pathResolveToVariantCanonicalPath ( re .getPath ( ) , v )
743748 }
744749
745- /** Holds if `re` constructs a struct value of type `v `. */
750+ /** Holds if `re` constructs a struct value of type `s `. */
746751 pragma [ nomagic]
747752 private predicate structConstruction ( RecordExpr re , StructCanonicalPath s ) {
748753 pathResolveToStructCanonicalPath ( re .getPath ( ) , s )
@@ -780,6 +785,13 @@ module RustDataFlow implements InputSig<Location> {
780785 node1 .asExpr ( ) = tuple .getField ( c .( TuplePositionContent ) .getPosition ( ) ) and
781786 node2 .asExpr ( ) = tuple
782787 )
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+ )
783795 )
784796 }
785797
@@ -788,12 +800,11 @@ module RustDataFlow implements InputSig<Location> {
788800 * any value stored inside `f` is cleared at the pre-update node associated with `x`
789801 * in `x.f = newValue`.
790802 */
791- predicate clearsContent ( Node n , ContentSet c ) {
803+ predicate clearsContent ( Node n , ContentSet cs ) {
792804 exists ( AssignmentExprCfgNode assignment , FieldExprCfgNode access |
793805 assignment .getLhs ( ) = access and
794806 n .asExpr ( ) = access .getExpr ( ) and
795- access .getNameRef ( ) .getText ( ) .toInt ( ) =
796- c .( SingletonContentSet ) .getContent ( ) .( TuplePositionContent ) .getPosition ( )
807+ fieldTuplePositionContent ( access , cs .( SingletonContentSet ) .getContent ( ) )
797808 )
798809 }
799810
0 commit comments