From 51f96deb2e3dd04f05322e2effeea9e6fdc594b7 Mon Sep 17 00:00:00 2001 From: Joe Farebrother Date: Wed, 13 Aug 2025 10:41:07 +0100 Subject: [PATCH] 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) } +}