@@ -290,9 +290,22 @@ private module Input3 implements InputSig3 {
290290
291291 class AstNode = Rust:: AstNode ;
292292
293- predicate getTypeAnnotation = getTypeAnnotation_ / 1 ;
293+ TypeMention getTypeAnnotation ( AstNode n ) {
294+ exists ( LetStmt let |
295+ n = let .getPat ( ) and
296+ result = let .getTypeRepr ( )
297+ )
298+ or
299+ result = n .( SelfParam ) .getTypeRepr ( )
300+ or
301+ exists ( Param p |
302+ n = p .getPat ( ) and
303+ result = p .getTypeRepr ( )
304+ )
305+ or
306+ result = n .( ShorthandSelfParameterMention )
307+ }
294308
295- /** A variable, for example a local variable or a field. */
296309 class Variable extends Rust:: Variable {
297310 AstNode getDefiningNode ( ) {
298311 result = this .getPat ( ) .getName ( ) or
@@ -511,28 +524,6 @@ private Type getCallExprTypeArgument(CallExpr ce, TypeArgumentPosition apos, Typ
511524 )
512525}
513526
514- /** Gets the type annotation that applies to `n`, if any. */
515- private TypeMention getTypeAnnotation_ ( AstNode n ) {
516- exists ( LetStmt let |
517- n = let .getPat ( ) and
518- result = let .getTypeRepr ( )
519- )
520- or
521- result = n .( SelfParam ) .getTypeRepr ( )
522- or
523- exists ( Param p |
524- n = p .getPat ( ) and
525- result = p .getTypeRepr ( )
526- )
527- or
528- result = n .( ShorthandSelfParameterMention )
529- }
530-
531- // /** Gets the type of `n`, which has an explicit type annotation. */
532- // pragma[nomagic]
533- // private Type inferAnnotatedType(AstNode n, TypePath path) {
534- // result = getTypeAnnotation(n).getTypeAt(path)
535- // }
536527pragma [ nomagic]
537528private Type inferFunctionBodyType ( AstNode n , TypePath path ) {
538529 exists ( Function f |
@@ -656,30 +647,6 @@ module CertainTypeInference_ {
656647 }
657648
658649 predicate certainTypeEquality_ ( AstNode n1 , TypePath prefix1 , AstNode n2 , TypePath prefix2 ) {
659- // prefix1.isEmpty() and
660- // prefix2.isEmpty() and
661- // (
662- // exists(Variable v | n1 = v.getAnAccess() |
663- // n2 = v.getPat().getName() or n2 = v.getParameter().(SelfParam)
664- // )
665- // or
666- // // // A `let` statement with a type annotation is a coercion site and hence
667- // // // is not a certain type equality.
668- // // exists(LetStmt let |
669- // // not let.hasTypeRepr() and
670- // // identLetStmt(let, n1, n2)
671- // // )
672- // // or
673- // // exists(LetExpr let |
674- // // // Similarly as for let statements, we need to rule out binding modes
675- // // // changing the type.
676- // // let.getPat().(IdentPat) = n1 and
677- // // let.getScrutinee() = n2
678- // // )
679- // // or
680- // n1 = n2.(ParenExpr).getExpr()
681- // )
682- // or
683650 n1 =
684651 any ( IdentPat ip |
685652 n2 = ip .getName ( ) and
@@ -708,31 +675,15 @@ module CertainTypeInference_ {
708675 )
709676 }
710677
711- // pragma[nomagic]
712- // private Type inferCertainTypeEquality(AstNode n, TypePath path) {
713- // exists(TypePath prefix1, AstNode n2, TypePath prefix2, TypePath suffix |
714- // result = inferCertainType(n2, prefix2.appendInverse(suffix)) and
715- // path = prefix1.append(suffix)
716- // |
717- // certainTypeEquality(n, prefix1, n2, prefix2)
718- // or
719- // certainTypeEquality(n2, prefix2, n, prefix1)
720- // )
721- // }
722678 /**
723679 * Holds if `n` has complete and certain type information and if `n` has the
724680 * resulting type at `path`.
725681 */
726682 Type inferCertainType_ ( AstNode n , TypePath path ) {
727- // result = inferAnnotatedType(n, path) and
728- // Stages::TypeInferenceStage::ref()
729- // or
730683 result = inferFunctionBodyType ( n , path )
731684 or
732685 result = inferCertainCallExprType ( n , path )
733686 or
734- // result = inferCertainTypeEquality(n, path)
735- // or
736687 result = inferLiteralType ( n , path , true )
737688 or
738689 result = inferRefPatType ( n ) and
@@ -771,48 +722,7 @@ module CertainTypeInference_ {
771722 n instanceof ClosureExpr and
772723 path .isEmpty ( ) and
773724 result = closureRootType ( )
774- // or
775- // infersCertainTypeAt(n, path, result.getATypeParameter())
776- }
777- // /**
778- // * Holds if `n` has complete and certain type information at the type path
779- // * `prefix.tp`. This entails that the type at `prefix` must be the type
780- // * that declares `tp`.
781- // */
782- // pragma[nomagic]
783- // private predicate infersCertainTypeAt(AstNode n, TypePath prefix, TypeParameter tp) {
784- // exists(TypePath path |
785- // exists(inferCertainType(n, path)) and
786- // path.isSnoc(prefix, tp)
787- // )
788- // }
789- // /**
790- // * Holds if `n` has complete and certain type information at `path`.
791- // */
792- // pragma[nomagic]
793- // predicate hasInferredCertainType(AstNode n, TypePath path) { exists(inferCertainType(n, path)) }
794- // /**
795- // * Holds if `n` having type `t` at `path` conflicts with certain type information
796- // * at `prefix`.
797- // */
798- // bindingset[n, prefix, path, t]
799- // pragma[inline_late]
800- // predicate certainTypeConflict(AstNode n, TypePath prefix, TypePath path, Type t) {
801- // inferCertainType(n, path) != t
802- // or
803- // // If we infer that `n` has _some_ type at `T1.T2....Tn`, and we also
804- // // know that `n` certainly has type `certainType` at `T1.T2...Ti`, `0 <= i < n`,
805- // // then it must be the case that `T(i+1)` is a type parameter of `certainType`,
806- // // otherwise there is a conflict.
807- // //
808- // // Below, `prefix` is `T1.T2...Ti` and `tp` is `T(i+1)`.
809- // exists(TypePath suffix, TypeParameter tp, Type certainType |
810- // path = prefix.appendInverse(suffix) and
811- // tp = suffix.getHead() and
812- // inferCertainType(n, prefix) = certainType and
813- // not certainType.getATypeParameter() = tp
814- // )
815- // }
725+ }
816726}
817727
818728private Type inferLogicalOperationType ( AstNode n , TypePath path ) {
@@ -864,27 +774,15 @@ private predicate bodyReturns(Expr body, Expr e) {
864774 * through the type equality.
865775 */
866776private predicate typeEquality_ ( AstNode n1 , TypePath prefix1 , AstNode n2 , TypePath prefix2 ) {
867- // CertainTypeInference::certainTypeEquality(n1, prefix1, n2, prefix2)
868- // or
869777 prefix1 .isEmpty ( ) and
870778 prefix2 .isEmpty ( ) and
871779 (
872- // exists(LetStmt let |
873- // let.getPat() = n1 and
874- // let.getInitializer() = n2
875- // )
876- // or
877780 n2 =
878781 any ( MatchExpr me |
879782 n1 = me .getAnArm ( ) .getExpr ( ) and
880783 me .getNumberOfArms ( ) = 1
881784 )
882785 or
883- // exists(LetExpr let |
884- // n1 = let.getScrutinee() and
885- // n2 = let.getPat()
886- // )
887- // or
888786 exists ( MatchExpr me |
889787 n1 = me .getScrutinee ( ) and
890788 n2 = me .getAnArm ( ) .getPat ( )
@@ -982,9 +880,6 @@ private predicate typeEquality_(AstNode n1, TypePath prefix1, AstNode n2, TypePa
982880 * [1]: https://doc.rust-lang.org/reference/type-coercions.html#r-coerce.least-upper-bound
983881 */
984882private predicate lubCoercion_ ( AstNode parent , AstNode child , TypePath prefix ) {
985- // child = parent.(IfExpr).getABranch() and
986- // prefix.isEmpty()
987- // or
988883 parent =
989884 any ( MatchExpr me |
990885 child = me .getAnArm ( ) .getExpr ( ) and
@@ -1032,18 +927,6 @@ private Type inferUnknownTypeFromAnnotation(AstNode n, TypePath path) {
1032927 * `n2`.
1033928 */
1034929private predicate typeEqualityAsymmetric_ ( AstNode n1 , TypePath prefix1 , AstNode n2 , TypePath prefix2 ) {
1035- // lubCoercion(n2, n1, prefix2) and
1036- // prefix1.isEmpty()
1037- // or
1038- // exists(AstNode mid, TypePath prefixMid, TypePath suffix |
1039- // typeEquality(n1, prefixMid, mid, prefix2) or
1040- // typeEquality(mid, prefix2, n1, prefixMid)
1041- // |
1042- // lubCoercion(mid, n2, suffix) and
1043- // not lubCoercion(mid, n1, _) and
1044- // prefix1 = prefixMid.append(suffix)
1045- // )
1046- // or
1047930 // When `n2` is `*n1` propagate type information from a raw pointer type
1048931 // parameter at `n1`. The other direction is handled in
1049932 // `inferDereferencedExprPtrType`.
@@ -1052,19 +935,6 @@ private predicate typeEqualityAsymmetric_(AstNode n1, TypePath prefix1, AstNode
1052935 prefix2 .isEmpty ( )
1053936}
1054937
1055- // pragma[nomagic]
1056- // private Type inferTypeEquality(AstNode n, TypePath path) {
1057- // exists(TypePath prefix1, AstNode n2, TypePath prefix2, TypePath suffix |
1058- // result = inferType(n2, prefix2.appendInverse(suffix)) and
1059- // path = prefix1.append(suffix)
1060- // |
1061- // typeEquality(n, prefix1, n2, prefix2)
1062- // or
1063- // typeEquality(n2, prefix2, n, prefix1)
1064- // or
1065- // typeEqualityAsymmetric(n2, prefix2, n, prefix1)
1066- // )
1067- // }
1068938pragma [ nomagic]
1069939private TupleType inferTupleRootType ( AstNode n ) {
1070940 // `typeEquality` handles the non-root cases
@@ -3362,6 +3232,19 @@ private Type getFieldExprLookupType(FieldExpr fe, string name, DerefChain derefC
33623232 )
33633233}
33643234
3235+ /**
3236+ * Gets the struct field that the field expression `fe` resolves to, if any.
3237+ */
3238+ cached
3239+ StructField resolveStructFieldExpr ( FieldExpr fe , DerefChain derefChain ) {
3240+ exists ( string name , DataType ty |
3241+ ty = getFieldExprLookupType ( fe , pragma [ only_bind_into ] ( name ) , derefChain )
3242+ |
3243+ result = ty .( StructType ) .getTypeItem ( ) .getStructField ( pragma [ only_bind_into ] ( name ) ) or
3244+ result = ty .( UnionType ) .getTypeItem ( ) .getStructField ( pragma [ only_bind_into ] ( name ) )
3245+ )
3246+ }
3247+
33653248pragma [ nomagic]
33663249private Type getTupleFieldExprLookupType ( FieldExpr fe , int pos , DerefChain derefChain ) {
33673250 exists ( string name |
@@ -3370,6 +3253,20 @@ private Type getTupleFieldExprLookupType(FieldExpr fe, int pos, DerefChain deref
33703253 )
33713254}
33723255
3256+ /**
3257+ * Gets the tuple field that the field expression `fe` resolves to, if any.
3258+ */
3259+ cached
3260+ TupleField resolveTupleFieldExpr ( FieldExpr fe , DerefChain derefChain ) {
3261+ exists ( int i |
3262+ result =
3263+ getTupleFieldExprLookupType ( fe , pragma [ only_bind_into ] ( i ) , derefChain )
3264+ .( StructType )
3265+ .getTypeItem ( )
3266+ .getTupleField ( pragma [ only_bind_into ] ( i ) )
3267+ )
3268+ }
3269+
33733270/**
33743271 * A matching configuration for resolving types of field expressions like `x.field`.
33753272 */
@@ -3897,50 +3794,9 @@ Addressable resolveCallTarget(InvocationExpr call, boolean dispatch) {
38973794 )
38983795}
38993796
3900- /**
3901- * Gets the struct field that the field expression `fe` resolves to, if any.
3902- */
3903- cached
3904- StructField resolveStructFieldExpr ( FieldExpr fe , DerefChain derefChain ) {
3905- exists ( string name , DataType ty |
3906- ty = getFieldExprLookupType ( fe , pragma [ only_bind_into ] ( name ) , derefChain )
3907- |
3908- result = ty .( StructType ) .getTypeItem ( ) .getStructField ( pragma [ only_bind_into ] ( name ) ) or
3909- result = ty .( UnionType ) .getTypeItem ( ) .getStructField ( pragma [ only_bind_into ] ( name ) )
3910- )
3911- }
3912-
3913- /**
3914- * Gets the tuple field that the field expression `fe` resolves to, if any.
3915- */
3916- cached
3917- TupleField resolveTupleFieldExpr ( FieldExpr fe , DerefChain derefChain ) {
3918- exists ( int i |
3919- result =
3920- getTupleFieldExprLookupType ( fe , pragma [ only_bind_into ] ( i ) , derefChain )
3921- .( StructType )
3922- .getTypeItem ( )
3923- .getTupleField ( pragma [ only_bind_into ] ( i ) )
3924- )
3925- }
3926-
39273797private Type inferType_ ( AstNode n , TypePath path ) {
3928- // // Stages::TypeInferenceStage::ref() and
3929- // // result = CertainTypeInference::inferCertainType(n, path)
3930- // // or
3931- // // Don't propagate type information into a node which conflicts with certain
3932- // // type information.
3933- // forall(TypePath prefix |
3934- // CertainTypeInference::hasInferredCertainType(n, prefix) and
3935- // prefix.isPrefixOf(path)
3936- // |
3937- // not CertainTypeInference::certainTypeConflict(n, prefix, path, result)
3938- // ) and
3939- // (
39403798 result = inferAssignmentOperationType ( n , path )
39413799 or
3942- // result = inferTypeEquality(n, path)
3943- // or
39443800 result = inferFunctionCallType ( n , path )
39453801 or
39463802 result = inferConstructionType ( n , path )
@@ -3966,7 +3822,6 @@ private Type inferType_(AstNode n, TypePath path) {
39663822 result = inferDeconstructionPatType ( n , path )
39673823 or
39683824 result = inferUnknownTypeFromAnnotation ( n , path )
3969- // )
39703825}
39713826
39723827/** Provides predicates for debugging the type inference implementation. */
0 commit comments