From 51f96deb2e3dd04f05322e2effeea9e6fdc594b7 Mon Sep 17 00:00:00 2001 From: Joe Farebrother Date: Wed, 13 Aug 2025 10:41:07 +0100 Subject: [PATCH 1/5] Add shared LocOption module for optional types with locations --- shared/util/codeql/util/Option.qll | 59 ++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/shared/util/codeql/util/Option.qll b/shared/util/codeql/util/Option.qll index 65a5e872452..bc3c1651b4a 100644 --- a/shared/util/codeql/util/Option.qll +++ b/shared/util/codeql/util/Option.qll @@ -8,6 +8,16 @@ private signature class TypeWithToString { string toString(); } +/** A type with `toString` and `hasLocationInfo` */ +private signature class TypeWithToStringAndLocation { + 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 +55,52 @@ 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. + */ +module LocOption { + private module O = Option; + + final private class BOption = O::Option; + + final private class BNone = O::None; + + final private class BSome = O::Some; + + /** + * An option type. This is either a singleton `None` or a `Some` wrapping the + * given type. + */ + class Option extends BOption { + /** + * 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 BNone, Option { } + + /** A wrapper for the given type. */ + class Some extends BSome, Option { } + + /** Gets the given element wrapped as an `Option`. */ + Some some(T c) { result = O::some(c) } +} From fc5501b9c85c0c0b2cdaca5f5b16c53e7f774a5b Mon Sep 17 00:00:00 2001 From: Joe Farebrother Date: Wed, 13 Aug 2025 11:55:10 +0100 Subject: [PATCH 2/5] Add LocOption2 for types with `getLocation`. --- shared/util/codeql/util/Option.qll | 66 +++++++++++++++++++++++++++++- 1 file changed, 64 insertions(+), 2 deletions(-) diff --git a/shared/util/codeql/util/Option.qll b/shared/util/codeql/util/Option.qll index bc3c1651b4a..960fe6df8a5 100644 --- a/shared/util/codeql/util/Option.qll +++ b/shared/util/codeql/util/Option.qll @@ -9,7 +9,7 @@ private signature class TypeWithToString { } /** A type with `toString` and `hasLocationInfo` */ -private signature class TypeWithToStringAndLocation { +private signature class TypeWithLocationInfo { bindingset[this] string toString(); @@ -59,8 +59,9 @@ module Option { /** * 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 LocOption { +module LocOption { private module O = Option; final private class BOption = O::Option; @@ -104,3 +105,64 @@ module LocOption { /** Gets the given element wrapped as an `Option`. */ Some some(T c) { result = O::some(c) } } + +private module GetLocationType { + signature class TypeWithGetLocation { + 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 `hasLocationInfo` predicate. + * `T` must have a `getLocation` predicate with a result type of `Location`. + */ +module LocOption2::TypeWithGetLocation T> { + private module O = Option; + + final private class BOption = O::Option; + + final private class BNone = O::None; + + final private class BSome = O::Some; + + /** + * An option type. This is either a singleton `None` or a `Some` wrapping the + * given type. + */ + class Option extends BOption { + /** + * 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() + .getLocation() + .hasLocationInfo(filePath, startLine, startColumn, endLine, endColumn) + } + } + + /** The singleton `None` element. */ + class None extends BNone, Option { } + + /** A wrapper for the given type. */ + class Some extends BSome, Option { } + + /** Gets the given element wrapped as an `Option`. */ + Some some(T c) { result = O::some(c) } +} From 8e5efb5fba3fe30fe0faab8944e512ae0d1a5e55 Mon Sep 17 00:00:00 2001 From: Joe Farebrother Date: Mon, 25 Aug 2025 16:04:43 +0100 Subject: [PATCH 3/5] Add change note --- shared/util/change-notes/2025-08-25-loc-option.md | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 shared/util/change-notes/2025-08-25-loc-option.md 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 00000000000..767f642adb3 --- /dev/null +++ b/shared/util/change-notes/2025-08-25-loc-option.md @@ -0,0 +1,4 @@ +--- +* category: minorAnalysis +--- +* Added `LocOption` and `LocOption2` as modules providing option types with location information. \ No newline at end of file From 80ab35c3a0dfbc282009162684635fc81b08bd45 Mon Sep 17 00:00:00 2001 From: Joe Farebrother Date: Tue, 26 Aug 2025 10:44:24 +0100 Subject: [PATCH 4/5] Apply review suggestions - rename things and clean up style. --- .../change-notes/2025-08-25-loc-option.md | 2 +- shared/util/codeql/util/Option.qll | 63 +++++++------------ 2 files changed, 22 insertions(+), 43 deletions(-) diff --git a/shared/util/change-notes/2025-08-25-loc-option.md b/shared/util/change-notes/2025-08-25-loc-option.md index 767f642adb3..dacbb6eea94 100644 --- a/shared/util/change-notes/2025-08-25-loc-option.md +++ b/shared/util/change-notes/2025-08-25-loc-option.md @@ -1,4 +1,4 @@ --- * category: minorAnalysis --- -* Added `LocOption` and `LocOption2` as modules providing option types with location information. \ No newline at end of file +* 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 960fe6df8a5..64f9aed363f 100644 --- a/shared/util/codeql/util/Option.qll +++ b/shared/util/codeql/util/Option.qll @@ -2,6 +2,8 @@ overlay[local?] module; +private import Location + /** A type with `toString`. */ private signature class TypeWithToString { bindingset[this] @@ -61,20 +63,16 @@ module Option { * additional singleton element, and has a `hasLocationInfo` predicate. * `T` must have a `hasLocationInfo` predicate. */ -module LocOption { +module OptionWithLocationInfo { private module O = Option; - final private class BOption = O::Option; - - final private class BNone = O::None; - - final private class BSome = O::Some; + 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 BOption { + class Option extends BaseOption { /** * Holds if this element is at the specified location. * The location spans column `startColumn` of line `startLine` to @@ -97,17 +95,17 @@ module LocOption { } /** The singleton `None` element. */ - class None extends BNone, Option { } + class None extends Option instanceof O::Some { } /** A wrapper for the given type. */ - class Some extends BSome, Option { } + class Some extends Option instanceof O::None { } /** Gets the given element wrapped as an `Option`. */ - Some some(T c) { result = O::some(c) } + Some some(T c) { result.asSome() = c } } -private module GetLocationType { - signature class TypeWithGetLocation { +private module WithLocation { + signature class LocatableType { bindingset[this] string toString(); @@ -117,52 +115,33 @@ private module GetLocationType { /** * Constructs an `Option` type that is a disjoint union of the given type and an - * additional singleton element, and has a `hasLocationInfo` predicate. + * additional singleton element, and has a `getLocation` predicate. * `T` must have a `getLocation` predicate with a result type of `Location`. */ -module LocOption2::TypeWithGetLocation T> { +module LocatableOption::LocatableType T> { private module O = Option; - final private class BOption = O::Option; - - final private class BNone = O::None; - - final private class BSome = O::Some; + 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 BOption { - /** - * 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 + class Option extends BaseOption { + Location getLocation() { + result = this.asSome().getLocation() or - this.asSome() - .getLocation() - .hasLocationInfo(filePath, startLine, startColumn, endLine, endColumn) + this.isNone() and + result.hasLocationInfo("", 0, 0, 0, 0) } } /** The singleton `None` element. */ - class None extends BNone, Option { } + class None extends Option instanceof O::Some { } /** A wrapper for the given type. */ - class Some extends BSome, Option { } + class Some extends Option instanceof O::None { } /** Gets the given element wrapped as an `Option`. */ - Some some(T c) { result = O::some(c) } + Some some(T c) { result.asSome() = c } } From 1b808fed3429ab4af80653e855a19b664c30edd3 Mon Sep 17 00:00:00 2001 From: Joe Farebrother Date: Thu, 28 Aug 2025 11:16:22 +0100 Subject: [PATCH 5/5] Fix incorrect switch of None and Some cases --- shared/util/codeql/util/Option.qll | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/shared/util/codeql/util/Option.qll b/shared/util/codeql/util/Option.qll index 64f9aed363f..77cc89504f5 100644 --- a/shared/util/codeql/util/Option.qll +++ b/shared/util/codeql/util/Option.qll @@ -95,10 +95,10 @@ module OptionWithLocationInfo { } /** The singleton `None` element. */ - class None extends Option instanceof O::Some { } + class None extends Option instanceof O::None { } /** A wrapper for the given type. */ - class Some extends Option instanceof O::None { } + class Some extends Option instanceof O::Some { } /** Gets the given element wrapped as an `Option`. */ Some some(T c) { result.asSome() = c } @@ -137,10 +137,10 @@ module LocatableOption::LocatableTy } /** The singleton `None` element. */ - class None extends Option instanceof O::Some { } + class None extends Option instanceof O::None { } /** A wrapper for the given type. */ - class Some extends Option instanceof O::None { } + class Some extends Option instanceof O::Some { } /** Gets the given element wrapped as an `Option`. */ Some some(T c) { result.asSome() = c }