Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions shared/util/change-notes/2025-08-25-loc-option.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
---
* category: minorAnalysis
---
* Added `LocatableOption` and `OptionWithLocationInfo` as modules providing option types with location information.
100 changes: 100 additions & 0 deletions shared/util/codeql/util/Option.qll
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -45,3 +57,91 @@ module Option<TypeWithToString T> {
/** Gets the given element wrapped as an `Option`. */
Copy link
Preview

Copilot AI Aug 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot detected a code snippet with 13 occurrences. See search results for more details.

Matched Code Snippet
*
     * 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

Copilot uses AI. Check for mistakes.

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<TypeWithLocationInfo T> {
private module O = Option<T>;

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<LocationSig Location> {
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<LocationSig Location, WithLocation<Location>::LocatableType T> {
private module O = Option<T>;

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 }
}
Loading