Rust: Generalize certain type inference logic

Author: hvitved

rust/ql/lib/codeql/rust/internal/TypeInference.qll

@@ -257,11 +257,6 @@ private Type inferAnnotatedType(AstNode n, TypePath path) {
 
 /** Module for inferring certain type information. */
 private module CertainTypeInference {
-  /** Holds if the type mention does not contain any inferred types `_`. */
-  predicate typeMentionIsComplete(TypeMention tm) {
-    not exists(InferTypeRepr t | t.getParentNode*() = tm)
-  }
-
   /**
    * Holds if `ce` is a call where we can infer the type with certainty and if
    * `f` is the target of the call and `p` the path invoked by the call.
@@ -343,6 +338,8 @@ private module CertainTypeInference {
         let.getPat() = n1 and
         let.getInitializer() = n2
       )
+      or
+      n1 = n2.(ParenExpr).getExpr()
     )
     or
     n1 =
@@ -373,13 +370,57 @@ private module CertainTypeInference {
   Type inferCertainType(AstNode n, TypePath path) {
     exists(TypeMention tm |
       tm = getTypeAnnotation(n) and
-      typeMentionIsComplete(tm) and
       result = tm.resolveTypeAt(path)
     )
     or
     result = inferCertainCallExprType(n, path)
     or
     result = inferCertainTypeEquality(n, path)
+    or
+    result = inferLiteralType(n, path, true)
+    or
+    infersCertainTypeAt(n, path, result.getATypeParameter())
+  }
+
+  /**
+   * Holds if `n` has complete and certain type information at the type path
+   * `prefix.tp`. This entails that the type at `prefix` must be the type
+   * that declares `tp`.
+   */
+  pragma[nomagic]
+  private predicate infersCertainTypeAt(AstNode n, TypePath prefix, TypeParameter tp) {
+    exists(TypePath path |
+      exists(inferCertainType(n, path)) and
+      path.isSnoc(prefix, tp)
+    )
+  }
+
+  /**
+   * Holds if `n` has complete and certain type information at _some_ type path.
+   */
+  pragma[nomagic]
+  predicate hasInferredCertainType(AstNode n) { exists(inferCertainType(n, _)) }
+
+  /**
+   * Holds if `n` having type `t` at `path` conflicts with certain type information.
+   */
+  bindingset[n, path, t]
+  pragma[inline_late]
+  predicate certainTypeConflict(AstNode n, TypePath path, Type t) {
+    inferCertainType(n, path) != t
+    or
+    // If we infer that `n` has _some_ type at `T1.T2....Tn`, and we also
+    // know that `n` certainly has type `certainType` at `T1.T2...Ti`, then
+    // it must be the case that `T(i+1)` is a type parameter of `certainType`,
+    // otherwise there is a conflict.
+    //
+    // Below, `prefix` is `T1.T2...Ti` and `tp` is `T(i+1)`.
+    exists(TypePath prefix, TypePath suffix, TypeParameter tp, Type certainType |
+      path = prefix.appendInverse(suffix) and
+      tp = suffix.getHead() and
+      inferCertainType(n, prefix) = certainType and
+      not certainType.getATypeParameter() = tp
+    )
   }
 }
 
@@ -432,8 +473,6 @@ private predicate typeEquality(AstNode n1, TypePath prefix1, AstNode n2, TypePat
       let.getInitializer() = n2
     )
     or
-    n1 = n2.(ParenExpr).getExpr()
-    or
     n1 = n2.(IfExpr).getABranch()
     or
     n1 = n2.(MatchExpr).getAnArm().getExpr()
@@ -531,9 +570,6 @@ private predicate typeEquality(AstNode n1, TypePath prefix1, AstNode n2, TypePat
 
 pragma[nomagic]
 private Type inferTypeEquality(AstNode n, TypePath path) {
-  // Don't propagate type information into a node for which we already have
-  // certain type information.
-  not exists(CertainTypeInference::inferCertainType(n, _)) and
   exists(TypePath prefix1, AstNode n2, TypePath prefix2, TypePath suffix |
     result = inferType(n2, prefix2.appendInverse(suffix)) and
     path = prefix1.append(suffix)
@@ -1308,17 +1344,22 @@ pragma[nomagic]
 private StructType getStrStruct() { result = TStruct(any(Builtins::Str s)) }
 
 pragma[nomagic]
-private Type inferLiteralType(LiteralExpr le, TypePath path) {
+private Type inferLiteralType(LiteralExpr le, TypePath path, boolean certain) {
   path.isEmpty() and
   exists(Builtins::BuiltinType t | result = TStruct(t) |
     le instanceof CharLiteralExpr and
-    t instanceof Builtins::Char
+    t instanceof Builtins::Char and
+    certain = true
     or
     le =
       any(NumberLiteralExpr ne |
-        t.getName() = ne.getSuffix()
+        t.getName() = ne.getSuffix() and
+        certain = true
         or
+        // When a number literal has no suffix, the type may depend on the context.
+        // For simplicity, we assume either `i32` or `f64`.
         not exists(ne.getSuffix()) and
+        certain = false and
         (
           ne instanceof IntegerLiteralExpr and
           t instanceof Builtins::I32
@@ -1329,7 +1370,8 @@ private Type inferLiteralType(LiteralExpr le, TypePath path) {
       )
     or
     le instanceof BooleanLiteralExpr and
-    t instanceof Builtins::Bool
+    t instanceof Builtins::Bool and
+    certain = true
   )
   or
   le instanceof StringLiteralExpr and
@@ -1338,7 +1380,8 @@ private Type inferLiteralType(LiteralExpr le, TypePath path) {
     or
     path = TypePath::singleton(TRefTypeParameter()) and
     result = getStrStruct()
-  )
+  ) and
+  certain = true
 }
 
 pragma[nomagic]
@@ -2282,62 +2325,71 @@ private module Cached {
     Stages::TypeInferenceStage::ref() and
     result = CertainTypeInference::inferCertainType(n, path)
     or
-    result = inferAnnotatedType(n, path)
-    or
-    result = inferLogicalOperationType(n, path)
-    or
-    result = inferAssignmentOperationType(n, path)
-    or
-    result = inferTypeEquality(n, path)
-    or
-    result = inferImplicitSelfType(n, path)
-    or
-    result = inferStructExprType(n, path)
-    or
-    result = inferTupleRootType(n) and
-    path.isEmpty()
-    or
-    result = inferPathExprType(n, path)
-    or
-    result = inferCallExprBaseType(n, path)
-    or
-    result = inferFieldExprType(n, path)
-    or
-    result = inferTupleIndexExprType(n, path)
-    or
-    result = inferTupleContainerExprType(n, path)
-    or
-    result = inferRefNodeType(n) and
-    path.isEmpty()
-    or
-    result = inferTryExprType(n, path)
-    or
-    result = inferLiteralType(n, path)
-    or
-    result = inferAsyncBlockExprRootType(n) and
-    path.isEmpty()
-    or
-    result = inferAwaitExprType(n, path)
-    or
-    result = inferArrayExprType(n) and
-    path.isEmpty()
-    or
-    result = inferRangeExprType(n) and
-    path.isEmpty()
-    or
-    result = inferIndexExprType(n, path)
-    or
-    result = inferForLoopExprType(n, path)
-    or
-    result = inferDynamicCallExprType(n, path)
-    or
-    result = inferClosureExprType(n, path)
-    or
-    result = inferCastExprType(n, path)
-    or
-    result = inferStructPatType(n, path)
-    or
-    result = inferTupleStructPatType(n, path)
+    // Don't propagate type information into a node which conflicts with certain
+    // type information.
+    (
+      if CertainTypeInference::hasInferredCertainType(n)
+      then not CertainTypeInference::certainTypeConflict(n, path, result)
+      else any()
+    ) and
+    (
+      result = inferAnnotatedType(n, path)
+      or
+      result = inferLogicalOperationType(n, path)
+      or
+      result = inferAssignmentOperationType(n, path)
+      or
+      result = inferTypeEquality(n, path)
+      or
+      result = inferImplicitSelfType(n, path)
+      or
+      result = inferStructExprType(n, path)
+      or
+      result = inferTupleRootType(n) and
+      path.isEmpty()
+      or
+      result = inferPathExprType(n, path)
+      or
+      result = inferCallExprBaseType(n, path)
+      or
+      result = inferFieldExprType(n, path)
+      or
+      result = inferTupleIndexExprType(n, path)
+      or
+      result = inferTupleContainerExprType(n, path)
+      or
+      result = inferRefNodeType(n) and
+      path.isEmpty()
+      or
+      result = inferTryExprType(n, path)
+      or
+      result = inferLiteralType(n, path, false)
+      or
+      result = inferAsyncBlockExprRootType(n) and
+      path.isEmpty()
+      or
+      result = inferAwaitExprType(n, path)
+      or
+      result = inferArrayExprType(n) and
+      path.isEmpty()
+      or
+      result = inferRangeExprType(n) and
+      path.isEmpty()
+      or
+      result = inferIndexExprType(n, path)
+      or
+      result = inferForLoopExprType(n, path)
+      or
+      result = inferDynamicCallExprType(n, path)
+      or
+      result = inferClosureExprType(n, path)
+      or
+      result = inferCastExprType(n, path)
+      or
+      result = inferStructPatType(n, path)
+      or
+      result = inferTupleStructPatType(n, path)
+    )
   }
 }
 
@@ -2438,6 +2490,11 @@ private module Debug {
     c = max(countTypePaths(_, _, _))
   }
 
+  Type debugInferCertainType(AstNode n, TypePath path) {
+    n = getRelevantLocatable() and
+    result = CertainTypeInference::inferCertainType(n, path)
+  }
+
   Type debugInferCertainNonUniqueType(AstNode n, TypePath path) {
     n = getRelevantLocatable() and
     Consistency::nonUniqueCertainType(n, path) and

rust/ql/test/library-tests/type-inference/main.rs

@@ -2074,7 +2074,7 @@ mod indexers {
         // implicit dereference. We cannot currently handle a position that is
         // both implicitly dereferenced and implicitly borrowed, so the extra
         // type sneaks in.
-        let x = slice[0].foo(); // $ target=foo type=x:S target=index SPURIOUS: type=slice:[]
+        let x = slice[0].foo(); // $ target=foo type=x:S target=index
     }
 
     pub fn f() {