diff --git a/shared/util/change-notes/2025-08-25-loc-option.md b/shared/util/change-notes/2025-08-25-loc-option.md new file mode 100644 index 000000000000..dacbb6eea946 --- /dev/null +++ b/shared/util/change-notes/2025-08-25-loc-option.md @@ -0,0 +1,4 @@ +--- +* category: minorAnalysis +--- +* Added `LocatableOption` and `OptionWithLocationInfo` as modules providing option types with location information. \ No newline at end of file diff --git a/shared/util/codeql/util/Option.qll b/shared/util/codeql/util/Option.qll index 65a5e8724526..77cc89504f58 100644 --- a/shared/util/codeql/util/Option.qll +++ b/shared/util/codeql/util/Option.qll @@ -2,12 +2,24 @@ overlay[local?] module; +private import Location + /** A type with `toString`. */ private signature class TypeWithToString { bindingset[this] string toString(); } +/** A type with `toString` and `hasLocationInfo` */ +private signature class TypeWithLocationInfo { + bindingset[this] + string toString(); + + predicate hasLocationInfo( + string filePath, int startLine, int startColumn, int endLine, int endColumn + ); +} + /** * Constructs an `Option` type that is a disjoint union of the given type and an * additional singleton element. @@ -45,3 +57,91 @@ module Option { /** Gets the given element wrapped as an `Option`. */ Some some(T c) { result = TSome(c) } } + +/** + * Constructs an `Option` type that is a disjoint union of the given type and an + * additional singleton element, and has a `hasLocationInfo` predicate. + * `T` must have a `hasLocationInfo` predicate. + */ +module OptionWithLocationInfo { + private module O = Option; + + final private class BaseOption = O::Option; + + /** + * An option type. This is either a singleton `None` or a `Some` wrapping the + * given type. + */ + class Option extends BaseOption { + /** + * 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 + ) { + this.isNone() and + filePath = "" and + startLine = 0 and + startColumn = 0 and + endLine = 0 and + endColumn = 0 + or + this.asSome().hasLocationInfo(filePath, startLine, startColumn, endLine, endColumn) + } + } + + /** The singleton `None` element. */ + class None extends Option instanceof O::None { } + + /** A wrapper for the given type. */ + class Some extends Option instanceof O::Some { } + + /** Gets the given element wrapped as an `Option`. */ + Some some(T c) { result.asSome() = c } +} + +private module WithLocation { + signature class LocatableType { + bindingset[this] + string toString(); + + Location getLocation(); + } +} + +/** + * Constructs an `Option` type that is a disjoint union of the given type and an + * additional singleton element, and has a `getLocation` predicate. + * `T` must have a `getLocation` predicate with a result type of `Location`. + */ +module LocatableOption::LocatableType T> { + private module O = Option; + + final private class BaseOption = O::Option; + + /** + * An option type. This is either a singleton `None` or a `Some` wrapping the + * given type. + */ + class Option extends BaseOption { + Location getLocation() { + result = this.asSome().getLocation() + or + this.isNone() and + result.hasLocationInfo("", 0, 0, 0, 0) + } + } + + /** The singleton `None` element. */ + class None extends Option instanceof O::None { } + + /** A wrapper for the given type. */ + class Some extends Option instanceof O::Some { } + + /** Gets the given element wrapped as an `Option`. */ + Some some(T c) { result.asSome() = c } +}