Rust: implement synthesized Locations

rust/ql/lib/codeql/Locations.qll

@@ -1,6 +1,7 @@
 /** Provides classes for working with locations. */
 
 import files.FileSystem
+private import codeql.rust.elements.internal.LocationImpl
 
 /**
  * A location as given by a file, a start line, a start column,
@@ -8,61 +9,7 @@ import files.FileSystem
  *
  * For more information about locations see [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
  */
-class Location extends @location_default {
-  /** Gets the file for this location. */
-  File getFile() { locations_default(this, result, _, _, _, _) }
-
-  /** Gets the 1-based line number (inclusive) where this location starts. */
-  int getStartLine() { locations_default(this, _, result, _, _, _) }
-
-  /** Gets the 1-based column number (inclusive) where this location starts. */
-  int getStartColumn() { locations_default(this, _, _, result, _, _) }
-
-  /** Gets the 1-based line number (inclusive) where this location ends. */
-  int getEndLine() { locations_default(this, _, _, _, result, _) }
-
-  /** Gets the 1-based column number (inclusive) where this location ends. */
-  int getEndColumn() { locations_default(this, _, _, _, _, result) }
-
-  /** Gets the number of lines covered by this location. */
-  int getNumLines() { result = this.getEndLine() - this.getStartLine() + 1 }
-
-  /** Gets a textual representation of this element. */
-  bindingset[this]
-  pragma[inline_late]
-  string toString() {
-    exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
-      this.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
-      result = filepath + "@" + startline + ":" + startcolumn + ":" + endline + ":" + endcolumn
-    )
-  }
-
-  /**
-   * Holds if this element is at the specified location.
-   * The location spans column `startcolumn` of line `startline` to
-   * column `endcolumn` of line `endline` in file `filepath`.
-   * For more information, see
-   * [Providing locations in CodeQL queries](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
-   */
-  predicate hasLocationInfo(
-    string filepath, int startline, int startcolumn, int endline, int endcolumn
-  ) {
-    exists(File f |
-      locations_default(this, f, startline, startcolumn, endline, endcolumn) and
-      filepath = f.getAbsolutePath()
-    )
-  }
-
-  /** Holds if this location starts strictly before the specified location. */
-  pragma[inline]
-  predicate strictlyBefore(Location other) {
-    this.getStartLine() < other.getStartLine()
-    or
-    this.getStartLine() = other.getStartLine() and this.getStartColumn() < other.getStartColumn()
-  }
-}
+final class Location = LocationImpl::Location;
 
 /** An entity representing an empty location. */
-class EmptyLocation extends Location {
-  EmptyLocation() { empty_location(this) }
-}
+final class EmptyLocation = LocationImpl::EmptyLocation;

rust/ql/lib/codeql/rust/Diagnostics.qll

@@ -1,6 +1,7 @@
 /** Provides classes relating to extraction diagnostics. */
 
 private import codeql.Locations
+private import codeql.rust.elements.internal.LocationImpl
 
 /** A diagnostic emitted during extraction, such as a parse error */
 class Diagnostic extends @diagnostic {
@@ -10,7 +11,12 @@ class Diagnostic extends @diagnostic {
   string fullMessage;
   Location location;
 
-  Diagnostic() { diagnostics(this, severity, tag, message, fullMessage, location) }
+  Diagnostic() {
+    exists(@location_default loc |
+      diagnostics(this, severity, tag, message, fullMessage, loc) and
+      location = LocationImpl::TLocationDefault(loc)
+    )
+  }
 
   /**
    * Gets the numerical severity level associated with this diagnostic.

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

@@ -5,6 +5,7 @@
  */
 
 import codeql.Locations
+private import codeql.rust.elements.internal.LocationImpl
 private import codeql.rust.elements.internal.generated.Locatable
 private import codeql.rust.elements.internal.generated.Synth
 private import codeql.rust.elements.internal.generated.Raw
@@ -17,9 +18,21 @@ module Impl {
   class Locatable extends Generated::Locatable {
     pragma[nomagic]
     final Location getLocation() {
-      exists(Raw::Locatable raw |
-        raw = Synth::convertLocatableToRaw(this) and
-        locatable_locations(raw, result)
+      exists(@location_default location |
+        result = LocationImpl::TLocationDefault(location) and
+        locatable_locations(Synth::convertLocatableToRaw(this), location)
+      )
+      or
+      not locatable_locations(Synth::convertLocatableToRaw(this), _) and
+      exists(File file, int beginLine, int beginColumn, int endLine, int endColumn |
+        this.hasLocationInfo(file.getAbsolutePath(), beginLine, beginColumn, endLine, endColumn)
+      |
+        result = LocationImpl::TLocationSynth(file, beginLine, beginColumn, endLine, endColumn)
+        or
+        exists(@location_default location |
+          result = LocationImpl::TLocationDefault(location) and
+          locations_default(location, file, beginLine, beginColumn, endLine, endColumn)
+        )
       )
     }
 
@@ -34,10 +47,6 @@ module Impl {
       string filepath, int startline, int startcolumn, int endline, int endcolumn
     ) {
       this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
-      or
-      not exists(this.getLocation()) and
-      pragma[only_bind_out](any(EmptyLocation e))
-          .hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
     }
 
     /**

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

@@ -0,0 +1,94 @@
+private import codeql.files.FileSystem
+
+module LocationImpl {
+  newtype TLocation =
+    TLocationDefault(@location_default location) or
+    TLocationSynth(File file, int beginLine, int beginColumn, int endLine, int endColumn) {
+      not locations_default(_, file, beginLine, beginColumn, endLine, endColumn) and none()
+    }
+
+  /**
+   * A location as given by a file, a start line, a start column,
+   * an end line, and an end column.
+   *
+   * For more information about locations see [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
+   */
+  abstract class Location extends TLocation {
+    /** Gets the file for this location. */
+    File getFile() { this.hasLocationInfo(result.getAbsolutePath(), _, _, _, _) }
+
+    /** Gets the 1-based line number (inclusive) where this location starts. */
+    int getStartLine() { this.hasLocationInfo(_, result, _, _, _) }
+
+    /** Gets the 1-based column number (inclusive) where this location starts. */
+    int getStartColumn() { this.hasLocationInfo(_, _, result, _, _) }
+
+    /** Gets the 1-based line number (inclusive) where this location ends. */
+    int getEndLine() { this.hasLocationInfo(_, _, _, result, _) }
+
+    /** Gets the 1-based column number (inclusive) where this location ends. */
+    int getEndColumn() { this.hasLocationInfo(_, _, _, _, result) }
+
+    /** Gets the number of lines covered by this location. */
+    int getNumLines() { result = this.getEndLine() - this.getStartLine() + 1 }
+
+    /** Gets a textual representation of this element. */
+    bindingset[this]
+    pragma[inline_late]
+    string toString() {
+      exists(string filepath, int startline, int startcolumn, int endline, int endcolumn |
+        this.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn) and
+        result = filepath + "@" + startline + ":" + startcolumn + ":" + endline + ":" + endcolumn
+      )
+    }
+
+    /**
+     * Holds if this element is at the specified location.
+     * The location spans column `startcolumn` of line `startline` to
+     * column `endcolumn` of line `endline` in file `filepath`.
+     * For more information, see
+     * [Providing locations in CodeQL queries](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
+     */
+    abstract predicate hasLocationInfo(
+      string filepath, int startline, int startcolumn, int endline, int endcolumn
+    );
+
+    /** Holds if this location starts strictly before the specified location. */
+    pragma[inline]
+    predicate strictlyBefore(Location other) {
+      this.getStartLine() < other.getStartLine()
+      or
+      this.getStartLine() = other.getStartLine() and this.getStartColumn() < other.getStartColumn()
+    }
+  }
+
+  private class LocationDefault extends Location, TLocationDefault {
+    @location_default self;
+
+    LocationDefault() { this = TLocationDefault(self) }
+
+    override predicate hasLocationInfo(
+      string filepath, int startline, int startcolumn, int endline, int endcolumn
+    ) {
+      exists(File f |
+        locations_default(self, f, startline, startcolumn, endline, endcolumn) and
+        filepath = f.getAbsolutePath()
+      )
+    }
+  }
+
+  /** An entity representing an empty location. */
+  class EmptyLocation extends LocationDefault {
+    EmptyLocation() { empty_location(self) }
+  }
+
+  private class LocationSynth extends Location, TLocationSynth {
+    override predicate hasLocationInfo(
+      string filepath, int startline, int startcolumn, int endline, int endcolumn
+    ) {
+      this =
+        TLocationSynth(any(File f | f.getAbsolutePath() = filepath), startline, startcolumn,
+          endline, endcolumn)
+    }
+  }
+}