Rust: Address comments on documentation

Author: paldepind

rust/ql/lib/codeql/rust/elements/internal/MethodCallExprImpl.qll

@@ -56,6 +56,8 @@ module Impl {
     }
 
     override Function getStaticTarget() {
+      // Functions in source code also gets extracted as library code, due to
+      // this duplication we prioritize functions from source code.
       result = this.getStaticTargetFrom(true)
       or
       not exists(this.getStaticTargetFrom(true)) and

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

@@ -19,6 +19,16 @@ private module Input1 implements InputSig1<Location> {
 
   class TypeParameter = T::TypeParameter;
 
+  /**
+   * A type abstraction. I.e., a place in the program where type variables are
+   * introduced.
+   *
+   * Example:
+   * ```rust
+   * impl<A, B> Foo<A, B> { }
+   * //  ^^^^^^ a type abstraction
+   * ```
+   */
   class TypeAbstraction = T::TypeAbstraction;
 
   private newtype TTypeArgumentPosition =
@@ -118,6 +128,13 @@ private module Input2 implements InputSig2 {
     result = tp.(SelfTypeParameter).getTrait()
   }
 
+  /**
+   * Use the constraint mechanism in the shared type inference library to
+   * support traits. In Rust `constraint` is always a trait.
+   *
+   * See the documentation of `conditionSatisfiesConstraint` in the shared type
+   * inference module for more information.
+   */
   predicate conditionSatisfiesConstraint(
     TypeAbstraction abs, TypeMention condition, TypeMention constraint
   ) {

shared/typeinference/codeql/typeinference/internal/TypeInference.qll

@@ -327,20 +327,25 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
      * //      ^^^^^^^^^^^^^ `constraint`
      * ```
      *
-     * Note that the type parameters in `abs` significantly change the meaning
-     * of type parameters that occur in `condition`. For instance, in the Rust
-     * example
+     * To see how `abs` change the meaning of the type parameters that occur in
+     * `condition`, consider the following examples in Rust:
      * ```rust
-     * fn foo<T: Trait>() { }
+     * impl<T> Trait for T { }
+     * //  ^^^ `abs`     ^ `condition`
+     * //      ^^^^^ `constraint`
      * ```
-     * we have that the type parameter `T` satisfies the constraint `Trait`. But,
-     * only that specific `T` satisfy the constraint. Hence we would not have
-     * `T` in `abs`. On the other hand, in the Rust example
+     * Here the meaning is "for all type parameters `T` it is the case that `T`
+     * implements `Trait`". On the other hand, in
      * ```rust
-     * impl<T> Trait for T { }
+     * fn foo<T: Trait>() { }
+     * //     ^ `condition`
+     * //        ^^^^^ `constraint`
      * ```
-     * the constraint `Trait` is in fact satisfied for all types, and we would
-     * have `T` in `abs` to make it free in the condition.
+     * the meaning is "`T` implements `Trait`" where the constraint is only
+     * valid for the specific `T`. Note that `condition` and `condition` are
+     * identical in the two examples. To encode the difference, `abs` in the
+     * first example should contain `T` whereas in the seconds example `abs`
+     * should be empty.
      */
     predicate conditionSatisfiesConstraint(
       TypeAbstraction abs, TypeMention condition, TypeMention constraint
@@ -359,9 +364,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
     signature module IsInstantiationOfInputSig<TypeTreeSig App> {
       /**
-       * Holds if `abs` is a type abstraction under which `tm` occurs and if
-       * `app` is potentially the result of applying the abstraction to type
-       * some type argument.
+       * Holds if `abs` is a type abstraction, `tm` occurs under `abs`, and
+       * `app` is potentially an application/instantiation of `abs`.
+       *
+       * For example:
+       * ```rust
+       * impl<A> Foo<A, A> {
+       * //  ^^^ `abs`
+       * //      ^^^^^^^^^ `tm`
+       *   fn bar(self) { ... }
+       * }
+       * // ...
+       *    foo.bar();
+       * // ^^^ `app`
+       * ```
+       * Here `abs` introduces the type parameter `A` and `tm` occurs under
+       * `abs` (i.e., `A` is bound in `tm` by `abs`). On the last line,
+       * accessing the `bar` method of `foo` potentially instantiates the `impl`
+       * block with a type argument for `A`.
        */
       predicate potentialInstantiationOf(App app, TypeAbstraction abs, TypeMention tm);