hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-27 01:35:13 +02:00
Code Issues Packages Projects Releases Wiki Activity

QL language spec: Document built-in equivalence relation module

Browse Source
This commit is contained in:
Kasper Svendsen
2022-10-21 09:46:20 +02:00
parent ac013f9d19
commit 7faea53c18
1 changed files with 60 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

61
docs/codeql/ql-language-reference/modules.rst
View File

@@ -273,4 +273,63 @@ The ``<module_expression>`` itself can be a module name, a selection, or a quali
reference. For more information, see ":ref:`name-resolution`."
For information about how import statements are looked up, see "`Module resolution <https://codeql.github.com/docs/ql-language-reference/ql-language-specification/#module-resolution>`__"
in the QL language specification.
in the QL language specification.
Built-in modules
****************
QL defines a `QlBuiltins` module, which is a built-in module that all databases
include. Currently, it defines a single parameterized sub-module
`EquivalenceRelation`, that provides an efficient abstraction for working with
(partial) equivalence relations in QL.
Equivalence relations
=====================
The built-in `EquivalenceRelation` module is parameterized by a type `T` and a
binary base relation `eq` on `T`. The symmetric and transitive closure of `eq`
induces a partial equivalence relation on `T`. If `eq` is reflexive, then the
induced relation is an equivalence relation on `T`.
The `EquivalenceRelation` module exports a `getEquivalenceClass` predicate that
gets the equivalence class, if any, associated with a given `T` element by the
(partial) equivalence relation induced by `eq`.
The following example illustrates an application of the `EquivalenceRelation`
module to generate a custom equivalence relation on an :ref:`algebraic datatype <algebraic-datatypes>`:
.. code-block:: ql
newtype Node = MkNode(int x) { x in [1..6] }
predicate base(Node x, Node y) {(x = MkNode(1) and y = MkNode(2)) or (x = MkNode(3) and y = MkNode(4)) }
module Equiv = QlBuiltins::EquivalenceRelation<Node, base/2>;
from int x, int y
where Equiv::getEquivalenceClass(MkNode(x)) = Equiv::getEquivalenceClass(MkNode(y))
select x, y
Since `base` does not relate `MkNode(5)` or `MkNode(6)` to any nodes, the induced
relation is a partial equivalence relation on `Node` and does not relate `MkNode(5)`
or `MkNode(6)` to any nodes either.
The above select clause returns the following partial equivalence relation:
+---+---+
| x | y |
+===+===+
| 1 | 1 |
+---+---+
| 1 | 2 |
+---+---+
| 2 | 1 |
+---+---+
| 2 | 2 |
+---+---+
| 3 | 3 |
+---+---+
| 3 | 4 |
+---+---+
| 4 | 3 |
+---+---+
| 4 | 4 |
+---+---+