mirror of
https://github.com/github/codeql.git
synced 2026-04-26 17:25:19 +02:00
Merge pull request #2547 from shati-patel/ql/tutorial
QL tutorials: Update formatting and style
This commit is contained in:
James Fletcher
@@ -1,7 +1,7 @@
|
||||
Find the thief: Introduction
|
||||
============================
|
||||
|
||||
There is a small village hidden away in the mountains. The village is divided into four parts - north, south, east, and west - and in the center stands a dark and mysterious castle... Inside the castle, locked away in the highest tower, lies the king's valuable golden crown. One night, a terrible crime is committed. A thief breaks into the tower and steals the crown!
|
||||
There is a small village hidden away in the mountains. The village is divided into four parts—north, south, east, and west—and in the center stands a dark and mysterious castle... Inside the castle, locked away in the highest tower, lies the king's valuable golden crown. One night, a terrible crime is committed. A thief breaks into the tower and steals the crown!
|
||||
|
||||
You know that the thief must live in the village, since nobody else knew about the crown. After some expert detective work, you obtain a list of all the people in the village and some of their personal details.
|
||||
|
||||
|
||||
@@ -82,7 +82,7 @@ Notice that we have only temporarily introduced the variable ``c`` and we didn't
|
||||
|
||||
Note
|
||||
|
||||
If you are familiar with logic, you may notice that ``exists`` in QL corresponds to the existential `quantifier <https://help.semmle.com/QL/ql-handbook/formulas.html#quantified-formulas>`__ in logic. QL also has a universal quantifier ``forall(vars | formula 1 | formula 2)`` which is logically equivalent to ``not(exists(vars | formula 1 | not formula 2))``.
|
||||
If you are familiar with logic, you may notice that ``exists`` in QL corresponds to the existential `quantifier <https://help.semmle.com/QL/ql-handbook/formulas.html#quantified-formulas>`__ in logic. QL also has a universal quantifier ``forall(vars | formula 1 | formula 2)`` which is logically equivalent to ``not exists(vars | formula 1 | not formula 2)``.
|
||||
|
||||
The real investigation
|
||||
----------------------
|
||||
@@ -124,8 +124,8 @@ Hints
|
||||
|
||||
from Person t
|
||||
where <condition 1> and
|
||||
not <condition 2> and
|
||||
...
|
||||
not <condition 2> and
|
||||
...
|
||||
select t
|
||||
|
||||
Once you have finished, you will have a list of possible suspects. One of those people must be the thief!
|
||||
|
||||
@@ -12,50 +12,50 @@ Read the examples below to learn how to define predicates and classes in QL. The
|
||||
Select the southerners
|
||||
----------------------
|
||||
|
||||
This time you only need to consider a specific group of villagers, namely those living in the south of the village. Instead of writing ``getLocation() = "south"`` in all your queries, you could define a new `predicate <https://help.semmle.com/QL/ql-handbook/predicates.html>`__ ``southern``:
|
||||
This time you only need to consider a specific group of villagers, namely those living in the south of the village. Instead of writing ``getLocation() = "south"`` in all your queries, you could define a new `predicate <https://help.semmle.com/QL/ql-handbook/predicates.html>`__ ``isSouthern``:
|
||||
|
||||
.. code-block:: ql
|
||||
|
||||
predicate southern(Person p) {
|
||||
p.getLocation() = "south"
|
||||
predicate isSouthern(Person p) {
|
||||
p.getLocation() = "south"
|
||||
}
|
||||
|
||||
The predicate ``southern(p)`` takes a single parameter ``p`` and checks if ``p`` satisfies the property ``p.getLocation() = "south"``.
|
||||
The predicate ``isSouthern(p)`` takes a single parameter ``p`` and checks if ``p`` satisfies the property ``p.getLocation() = "south"``.
|
||||
|
||||
.. pull-quote::
|
||||
|
||||
Note
|
||||
|
||||
- The name of a predicate always starts with a lowercase letter.
|
||||
- You can also define predicates with a result. In that case, the keyword ``predicate`` is replaced with the type of the result. This is like introducing a new argument, the special variable ``result``. For example, ``int getAge() {result = ...}`` returns an ``int``.
|
||||
- You can also define predicates with a result. In that case, the keyword ``predicate`` is replaced with the type of the result. This is like introducing a new argument, the special variable ``result``. For example, ``int getAge() { result = ... }`` returns an ``int``.
|
||||
|
||||
You can now list all southerners using:
|
||||
|
||||
.. code-block:: ql
|
||||
|
||||
/* define predicate `southern` as above */
|
||||
/* define predicate `isSouthern` as above */
|
||||
|
||||
from Person p
|
||||
where southern(p)
|
||||
where isSouthern(p)
|
||||
select p
|
||||
|
||||
This is already a nice way to simplify the logic, but we could be more efficient. Currently, the query looks at every ``Person p``, and then restricts to those who satisfy ``southern(p)``. Instead, we could define a new `class <https://help.semmle.com/QL/ql-handbook/types.html#classes>`__ ``Southerner`` containing precisely the people we want to consider.
|
||||
This is already a nice way to simplify the logic, but we could be more efficient. Currently, the query looks at every ``Person p``, and then restricts to those who satisfy ``isSouthern(p)``. Instead, we could define a new `class <https://help.semmle.com/QL/ql-handbook/types.html#classes>`__ ``Southerner`` containing precisely the people we want to consider.
|
||||
|
||||
.. code-block:: ql
|
||||
|
||||
class Southerner extends Person {
|
||||
Southerner() { southern(this) }
|
||||
Southerner() { isSouthern(this) }
|
||||
}
|
||||
|
||||
A class in QL represents a logical property: when a value satisfies that property, it is a member of the class. This means that a value can be in many classes - being in a particular class doesn't stop it from being in other classes too.
|
||||
A class in QL represents a logical property: when a value satisfies that property, it is a member of the class. This means that a value can be in many classes—being in a particular class doesn't stop it from being in other classes too.
|
||||
|
||||
The expression ``southern(this)`` defines the logical property represented by the class, called its *characteristic predicate*. It uses a special variable ``this`` and indicates that a ``Person`` "``this``" is a ``Southerner`` if the property ``southern(this)`` holds.
|
||||
The expression ``isSouthern(this)`` defines the logical property represented by the class, called its *characteristic predicate*. It uses a special variable ``this`` and indicates that a ``Person`` "``this``" is a ``Southerner`` if the property ``isSouthern(this)`` holds.
|
||||
|
||||
.. pull-quote::
|
||||
|
||||
Note
|
||||
|
||||
If you are familiar with object-oriented programming languages, you might be tempted to think of the characteristic predicate as a *constructor*. However, this is **not** the case - it is a logical property which does not create any objects.
|
||||
If you are familiar with object-oriented programming languages, you might be tempted to think of the characteristic predicate as a *constructor*. However, this is **not** the case—it is a logical property which does not create any objects.
|
||||
|
||||
You always need to define a class in QL in terms of an existing (larger) class. In our example, a ``Southerner`` is a special kind of ``Person``, so we say that ``Southerner`` *extends* ("is a subset of") ``Person``.
|
||||
|
||||
@@ -66,7 +66,7 @@ Using this class you can now list all people living in the south simply as:
|
||||
from Southerner s
|
||||
select s
|
||||
|
||||
You may have noticed that some predicates are appended, for example ``p.getAge()``, while others are not, for example ``southern(p)``. This is because ``getAge()`` is a member predicate, that is, a predicate that only applies to members of a class. You define such a member predicate inside a class. In this case, ``getAge()`` is defined inside the class ``Person``. In contrast, ``southern`` is defined separately and is not inside any classes. Member predicates are especially useful because you can chain them together easily. For example, ``p.getAge().sqrt()`` first gets the age of ``p`` and then calculates the square root of that number.
|
||||
You may have noticed that some predicates are appended, for example ``p.getAge()``, while others are not, for example ``isSouthern(p)``. This is because ``getAge()`` is a member predicate, that is, a predicate that only applies to members of a class. You define such a member predicate inside a class. In this case, ``getAge()`` is defined inside the class ``Person``. In contrast, ``isSouthern`` is defined separately and is not inside any classes. Member predicates are especially useful because you can chain them together easily. For example, ``p.getAge().sqrt()`` first gets the age of ``p`` and then calculates the square root of that number.
|
||||
|
||||
Travel restrictions
|
||||
-------------------
|
||||
@@ -88,20 +88,19 @@ Start by defining a class ``Child`` containing all villagers under 10 years old.
|
||||
.. code-block:: ql
|
||||
|
||||
class Child extends Person {
|
||||
/* the characteristic predicate */
|
||||
Child() { this.getAge() < 10 }
|
||||
|
||||
/* the characteristic predicate */
|
||||
Child() { this.getAge() < 10 }
|
||||
|
||||
/* a member predicate */
|
||||
override predicate isAllowedIn(string region) {
|
||||
region = this.getLocation()
|
||||
}
|
||||
/* a member predicate */
|
||||
override predicate isAllowedIn(string region) {
|
||||
region = this.getLocation()
|
||||
}
|
||||
}
|
||||
|
||||
Now try applying ``isAllowedIn(string region)`` to a person ``p``. If ``p`` is not a child, the original definition is used, but if ``p`` is a child, the new predicate definition overrides the original.
|
||||
|
||||
You know that the fire starters live in the south *and* that they must have been able to travel to the north. Write a query to find the possible suspects. You could also extend the ``select`` clause to list the age of the suspects. That way you can clearly see that all the children have been excluded from the list.
|
||||
|
||||
➤ `See the answer in the query console <https://lgtm.com/query/2164870087/>`__
|
||||
➤ `See the answer in the query console <https://lgtm.com/query/2551838470440192723/>`__
|
||||
|
||||
Continue to the :doc:`next page <fire-2>` to gather more clues and find out which of your suspects started the fire...
|
||||
|
||||
@@ -11,27 +11,27 @@ This is a very helpful clue. Remember that you wrote a QL query to select all ba
|
||||
where not exists (string c | p.getHairColor() = c)
|
||||
select p
|
||||
|
||||
To avoid having to type ``not exists (string c | p.getHairColor() = c)`` every time you want to select a bald person, you can instead define another new predicate ``bald``.
|
||||
To avoid having to type ``not exists (string c | p.getHairColor() = c)`` every time you want to select a bald person, you can instead define another new predicate ``isBald``.
|
||||
|
||||
.. code-block:: ql
|
||||
|
||||
predicate bald(Person p) {
|
||||
not exists (string c | p.getHairColor() = c)
|
||||
predicate isBald(Person p) {
|
||||
not exists (string c | p.getHairColor() = c)
|
||||
}
|
||||
|
||||
The property ``bald(p)`` holds whenever ``p`` is bald, so you can replace the previous query with:
|
||||
The property ``isBald(p)`` holds whenever ``p`` is bald, so you can replace the previous query with:
|
||||
|
||||
.. code-block:: ql
|
||||
|
||||
from Person p
|
||||
where bald(p)
|
||||
where isBald(p)
|
||||
select p
|
||||
|
||||
The predicate ``bald`` is defined to take a ``Person``, so it can also take a ``Southerner``, as ``Southerner`` is a subtype of ``Person``. It can't take an ``int`` for example - that would cause an error.
|
||||
The predicate ``isBald`` is defined to take a ``Person``, so it can also take a ``Southerner``, as ``Southerner`` is a subtype of ``Person``. It can't take an ``int`` for example—that would cause an error.
|
||||
|
||||
You can now write a query to select the bald southerners who are allowed into the north.
|
||||
|
||||
➤ `See the answer in the query console <https://lgtm.com/query/1505746995987/>`__
|
||||
➤ `See the answer in the query console <https://lgtm.com/query/2572701606358725253/>`__
|
||||
|
||||
You have found the two fire starters! They are arrested and the villagers are once again impressed with your work.
|
||||
|
||||
|
||||
@@ -1,9 +1,9 @@
|
||||
Crown the rightful heir
|
||||
=======================
|
||||
|
||||
Phew! No more crimes in the village - you can finally leave the village and go home.
|
||||
Phew! No more crimes in the village—you can finally leave the village and go home.
|
||||
|
||||
But then... During your last night in the village, the old king - the great King Basil - dies in his sleep and there is chaos everywhere!
|
||||
But then... During your last night in the village, the old king—the great King Basil—dies in his sleep and there is chaos everywhere!
|
||||
|
||||
The king never married and he had no children, so nobody knows who should inherit the king's castle and fortune. Immediately, lots of villagers claim that they are somehow descended from the king's family and that they are the true heir. People argue and fight and the situation seems hopeless.
|
||||
|
||||
@@ -38,8 +38,8 @@ We know that the king has no children himself, but perhaps he has siblings. Writ
|
||||
.. code-block:: ql
|
||||
|
||||
from Person p
|
||||
where parentOf(p) = parentOf("King Basil") and
|
||||
not p = "King Basil"
|
||||
where parentOf(p) = parentOf("King Basil") and
|
||||
not p = "King Basil"
|
||||
select p
|
||||
|
||||
He does indeed have siblings! But you need to check if any of them are alive... Here is one more predicate you might need:
|
||||
@@ -56,8 +56,8 @@ Use this predicate to see if the any of the king's siblings are alive.
|
||||
|
||||
from Person p
|
||||
where parentOf(p) = parentOf("King Basil") and
|
||||
not p = "King Basil"
|
||||
and not p.isDeceased()
|
||||
not p = "King Basil"
|
||||
and not p.isDeceased()
|
||||
select p
|
||||
|
||||
Unfortunately, none of King Basil's siblings are alive. Time to investigate further. It might be helpful to define a predicate ``childOf()`` which returns a child of the person. To do this, the ``parentOf()`` predicate can be used inside the definition of ``childOf()``. Remember that someone is a child of ``p`` if and only if ``p`` is their parent:
|
||||
@@ -65,7 +65,7 @@ Unfortunately, none of King Basil's siblings are alive. Time to investigate furt
|
||||
.. code-block:: ql
|
||||
|
||||
Person childOf(Person p) {
|
||||
p = parentOf(result)
|
||||
p = parentOf(result)
|
||||
}
|
||||
|
||||
.. pull-quote::
|
||||
@@ -80,7 +80,7 @@ Try to write a query to find out if any of the king's siblings have children:
|
||||
|
||||
from Person p
|
||||
where parentOf(p) = parentOf("King Basil") and
|
||||
not p = "King Basil"
|
||||
not p = "King Basil"
|
||||
select childOf(p)
|
||||
|
||||
The query returns no results, so they have no children. But perhaps King Basil has a cousin who is alive or has children, or a second cousin, or...
|
||||
@@ -100,8 +100,8 @@ You can translate this into QL as follows:
|
||||
.. code-block:: ql
|
||||
|
||||
Person ancestorOf(Person p) {
|
||||
result = parentOf(p) or
|
||||
result = parentOf(ancestorOf(p))
|
||||
result = parentOf(p) or
|
||||
result = parentOf(ancestorOf(p))
|
||||
}
|
||||
|
||||
As you can see, you have used the predicate ``ancestorOf()`` inside its own definition. This is an example of `recursion <https://help.semmle.com/QL/ql-handbook/recursion.html>`__.
|
||||
@@ -120,12 +120,12 @@ Here is one way to define ``relativeOf()``:
|
||||
.. code-block:: ql
|
||||
|
||||
Person relativeOf(Person p) {
|
||||
parentOf*(result) = parentOf*(p)
|
||||
parentOf*(result) = parentOf*(p)
|
||||
}
|
||||
|
||||
Don't forget to use the predicate ``isDeceased()`` to find relatives that are still alive.
|
||||
|
||||
➤ `See the answer in the query console <https://lgtm.com/query/2164460071/>`__
|
||||
➤ `See the answer in the query console <https://lgtm.com/query/6710025057257064639/>`__
|
||||
|
||||
Select the true heir
|
||||
--------------------
|
||||
@@ -136,9 +136,9 @@ To decide who should inherit the king's fortune, the villagers carefully read th
|
||||
|
||||
*"The heir to the throne is the closest living relative of the king. Any person with a criminal record will not be considered. If there are multiple candidates, the oldest person is the heir."*
|
||||
|
||||
As your final challenge, define a predicate ``criminalRecord`` so that ``criminalRecord(p)`` holds if ``p`` is any of the criminals you unmasked earlier (in the :doc:`Find the thief <find-thief-1>` and :doc:`Catch the fire starter <fire-1>` tutorials).
|
||||
As your final challenge, define a predicate ``hasCriminalRecord`` so that ``hasCriminalRecord(p)`` holds if ``p`` is any of the criminals you unmasked earlier (in the :doc:`Find the thief <find-thief-1>` and :doc:`Catch the fire starter <fire-1>` tutorials).
|
||||
|
||||
➤ `See the answer in the query console <https://lgtm.com/query/1505745996002/>`__
|
||||
➤ `See the answer in the query console <https://lgtm.com/query/1820692755164273290/>`__
|
||||
|
||||
Experimental explorations
|
||||
-------------------------
|
||||
|
||||
@@ -16,9 +16,9 @@ some simple examples.
|
||||
|
||||
Currently the following detective tutorials are available:
|
||||
|
||||
- :doc:`Find the thief <find-thief-1>` - a three part mystery that introduces logical connectives, quantifiers, and aggregates
|
||||
- :doc:`Catch the fire starter <fire-1>` - an intriguing search that introduces predicates and classes
|
||||
- :doc:`Crown the rightful heir <heir>` - a detective puzzle that introduces recursion
|
||||
- :doc:`Find the thief <find-thief-1>`—a three part mystery that introduces logical connectives, quantifiers, and aggregates
|
||||
- :doc:`Catch the fire starter <fire-1>`—an intriguing search that introduces predicates and classes
|
||||
- :doc:`Crown the rightful heir <heir>`—a detective puzzle that introduces recursion
|
||||
|
||||
Further resources
|
||||
-----------------
|
||||
|
||||
Reference in New Issue
Block a user