Created from 2024-04-25.

环境部署

brew install codeql

# 检测安装成功
codeql --version

# Output
# CodeQL command-line toolchain release 2.16.4.
# Copyright (C) 2019-2024 GitHub, Inc.
# Unpacked in: /opt/homebrew/Caskroom/codeql/2.16.4/codeql
#    Analysis results depend critically on separately distributed query and
#    extractor modules. To list modules that are visible to the toolchain,
#    use 'codeql resolve qlpacks' and 'codeql resolve languages'.

创建数据库

References:
Preparing your code for CodeQL analysis – GitHub Docs

1. 从本地Repo构建数据库

codeql database create <database-path> --language=java --source-root <source-code-path>

codeql database create /Users/fe1w0/Project/CodeQL/databases/gpt_academic --language=java --source-root /Users/fe1w0/Project/CodeQL/sources/gpt_academic

2. 从Github中下载Repo构建的数据库

gh api /repos/<owner>/<repo>/code-scanning/codeql/databases

gh api /repos/<owner>/<repo>/code-scanning/codeql/databases/<language> -H 'Accept: application/zip' > path/to/local/database.zip

About CodeQL

• example.ql from About CodeQL queries — CodeQL (github.com)

/**
 *a's
 * Query metadata
 *
 */

import /* ... CodeQL libraries or modules ... */

/* ... Optional, define CodeQL classes and predicates ... */

from /* ... variable declarations ... */
where /* ... logical formula ... */
select /* ... expressions ... */
/** 
*	select element, string
*	- `element`: a code element that is identified by the query, which defines where the alert is displayed.
*	- `string`: a message, which can also include links and placeholders, explaining why the alert was generated.
*/

基本 – CodeQL

如 github/vscode-codeql-starter: Starter workspace to use with the CodeQL extension for Visual Studio Code. 项目中的 java/example/empty-block

/**
 * @name Empty block
 * @kind problem
 * @problem.severity warning
 * @id java/example/empty-block
 */

import java

from BlockStmt b
where b.getNumStmt() = 0
select b, "This is an empty block."

其中 @name、@kind、@problem.severity 和 @id 称之为 CodeQL queries 的 Metadata ，用于VsCode-CodeQL数据处理。

此外 CodeQL 中还有 qhelp 文件用于描述查询的目的，以及修复方案，如codeql/csharp/ql/src/Security Features/CWE-079/XSS.qhelp at main · github/codeql 。可以参考 Query help files — CodeQL (github.com) 。

在select 定义输出结果是，也可以采用占位符 (1个占位符，需要两个输入参数)，如（Defining the results of a query — CodeQL (github.com)）

select c, "This class extends the class $@.", superclass, superclass.getName()

此外，CodeQL 提供了将分析结果指向源代码原地址的查询能力，见 在 CodeQL 查询中提供位置 — CodeQL (github.com)。

基本 – 数据流分析

CodeQL 中的数据流分析存在两种方法:

• Local data flow，函数内的数据流分析
• Global data flow，函数间的数据流分析，包含全局变量

构建路径查询

/**
 * ...
 * @kind path-problem
 * ...
 */

import <language>
// For some languages (Java/C++/Python/Swift) you need to explicitly import the data flow library, such as
// import semmle.code.java.dataflow.DataFlow or import codeql.swift.dataflow.DataFlow
...

module Flow = DataFlow::Global<MyConfiguration>;
import Flow::PathGraph

from Flow::PathNode source, Flow::PathNode sink
where Flow::flowPath(source, sink)
select sink.getNode(), source, sink, "<message>"

除了路径图模块import Flow::PathGraph，数据流库还包含数据流分析中常用的其他classes、predicates和modules，见 CodeQL standard libraries (github.com) 。

下面定义新的谓词，来表达 edge 关系（与souffle 差不多）。

query predicate edges(PathNode a, PathNode b) {
  /* Logical conditions which hold if `(a,b)` is an edge in the data flow graph */
}

下面的是定义MyConfiguration的过程，用于设置 Source 和 Sink。

module MyFlow = DataFlow::Global<MyConfiguration>;

from MyFlow::PathNode source, MyFlow::PathNode sink

module MyConfiguration implements DataFlow::ConfigSig {
  predicate isSource(DataFlow::Node source) { ... }
  predicate isSink(DataFlow::Node source) { ... }
}

// 编写路径查询时，您通常会包含一个谓词，该谓词仅在数据从`source`流向`sink`时才成立。
// 可以使用`flowPath`为给定`Configuration`指定从`source`到`sink`的流：
where MyFlow::flowPath(source, sink)

// 设置输出分析结果样式
select element, source, sink, string

之后，需要设置 数据流的判断逻辑，如 where MyFlow::flowPath(source, sink) where 子句。where子句定义了应用于from子句中声明的变量以生成结果的逻辑条件。 此子句可以使用聚合、谓词和逻辑公式将感兴趣的变量限制为满足定义条件的较小集合。

最后，使用select element, source, sink, string 来设置输出分析结果样式。如果，想在结果中显示 source 信息，则应该 element 为 source.getNode() ；反之，使用 sink.getNode()

查询优化

在查询优化过程中，除了要避免 Datalog 中过大的笛卡尔积查询外，CodeQL 中的 谓词变量 还需要注意使用 “最具体的类型” ，以便查询优化器可以有效优化。

[!NOTE] Note
官网中这块优化器的描述是，”From the type context, the query optimizer deduces that some parts of the program are redundant and removes them, or specializes them.”

如果不确定 谓词变量 “最具体的类型 ” 应该是什么，可以使用 getAQlClass() 来获得实体的最具体的QL类型。如:

import java

from Expr e, Callable c
where
    c.getDeclaringType().hasQualifiedName("my.namespace.name", "MyClass")
    and c.getName() = "c"
    and e.getEnclosingCallable() = c
select e, e.getAQlClass()

上面的查询内容为，获取 my.namespace.name.MyClass: c() Method中的表达式及其最具体的类型

同时在优化过程中，需要注意 fixed-point 中的递归，并尽可能使递归为单调递归。

int depth(Stmt s) {
  exists(Callable c | c.getBody() = s | result = 0) // base case
  or
  result = depth(s.getParent()) + 1 // recursive call
}

上面的代码中 exists(Callable c | c.getBody() = s | result = 0) 并不是用 | 符号来表示 或的逻辑关系，而是在QL中用于划分 定义|逻辑判断|返回值处理 。同时，Callable 类似于 llvm 或者 soot 中的 Method 变量，用于表示存储 Statement (即，Stmt类)语句。

exists 表达式的结构通常包括三个部分：

1. 变量声明：指定哪种类型的对象或变量将被考虑。如上例中的 Callable c，宣告了变量 c，它的类型是 Callable。
2. 条件：定义变量需要满足的条件。例如 c.getBody() = s 指定了 c 的方法体必须等于 s。
3. 结果表达式（可选）：在 exists 用于更广泛的上下文时，可以指定一个结果表达式，当 exists 条件为真时，可以直接定义一个结果，如 result = 0。

[!NOTE] Note
Q: 比较困惑的时，在不动点计算的时候，上面的谓词定义会不会一直计算下去。

A: 不会，实际计算过程中，是从 c.getBody （函数的起始处）开始计算，并设置0；且在递归过程中，s.getParent() 有且只有一个唯一解，导致在递归过程中，可以确保计算收敛。

另外，也可以通过将大谓词拆分成多个小谓词，也可以有效优化计算过程，且最好遵循两个原则:

• linear, so that there is not too much branching.
  • 线性，这样就不会有太多的分支。
• tightly bound, so that the chunks join with each other on as many variables as possible.
  • 紧密绑定，以便块在尽可能多的变量上相互连接。

和souffle 差不多。

predicate similar(Element e1, Element e2) {
  e1.getName() = e2.getName() and
  e1.getFile() = e2.getFile() and
  e1.getLocation().getStartLine() = e2.getLocation().getStartLine()
}

具体来说，对于上面的 similar 谓词来说，每一次计算都需要计算 Name、File 和 Line 的相等性。但下面的查询中，locInfo 查询谓词会先计算每个单一 Element 的 name、file 和 line 信息，之后在 sameLoc 谓词的逻辑中，只需要判断是否存在 e1 和 e2 不同，但 name 、file 和 line 信息相同的数据，不必重新计算name、file 和 Line 信息，从而加速了分析。

predicate locInfo(Element e, string name, File f, int startLine) {
  name = e.getName() and
  f = e.getFile() and
  startLine = e.getLocation().getStartLine()
}

predicate sameLoc(Element e1, Element e2) {
  exists(string name, File f, int startLine |
    locInfo(e1, name, f, startLine) and
    locInfo(e2, name, f, startLine)
  )
}

对局部的数据流分析进行调试

References:
Debugging data-flow queries using partial flow — CodeQL (github.com)

[!NOTE] Note
CodeQL 的 Debug 功能，是Node在LimitSize内进行重新分析，且输出所有的可能的数据流部分，最后根据输出结果来判断失效的谓词。

基于souffle的静态分析是使用explain 的方式来调试，首先输入期望的输出结果，之后可以方便和直观地输出失效的谓词部分，而不是根据输出结果来推迟失效的谓词。

典型的数据流查询如下所示：

 module MyConfig implements DataFlow::ConfigSig {
  predicate isSource(DataFlow::Node node) { node instanceof MySource }
  
  predicate isSink(DataFlow::Node node) { node instanceof MySink }
}

module MyFlow = TaintTracking::Global<MyConfig>;

from MyFlow::PathNode source, MyFlow::PathNode sink
where MyFlow::flowPath(source, sink)
select sink.getNode(), source, sink, "Sink is reached from $@.", source.getNode(), "here"

QL 基本语法

Basic and some examples

基本类型:

• int
• boolean: true, false
• date
• float
• string

[!NOTE] 以下是QL中的内置 谓词
QL language specification — CodeQL (github.com)

以下是Docs introduction 中的一些 examples

from string s
where s = "fe1w0"
select s.length()
// 另一方法
select "fe1w0".length()

from float x, float y
where x = 3.pow(5) and y = 245.6
select x.minimum(y).sin()

from boolean b
where b = false
select b.booleanNot()

from date start, date end
where start = "10/06/2017".toDate() and end = "28/09/2017".toDate()
select start.daysTo(end)

// 多数据输出
from int x, int y, int z
where x in [1..10] and y in [1..10] and z in [1..10] and
      x*x + y*y = z*z
select x, y, z

// 利用类来简化上面的代码
class SmallInt extends int {
    SmallInt() { this in [1..10]}
    int square() { result = this*this}
}

from SmallInt x, SmallInt y, SmallInt z
where x.square() + y.square() = z.square()
select x, y, z

// 检查 python 程序中函数参数超过7个的函数
import python

from Function f
where count(f.getAnArg()) > 7
select f

// 查找 javascript 程序中注释包含 TODO单词的注释内容
import javascript

from Comment c
where c.getText().regexpMatch("(?si).*\\bTODO\\b.*")
select c

// 查找 哪些参数还没有被访问过
import java

from Parameter p
where not exists(p.getAnAccess())
select p

Tutorial

[!NOTE] 环境设置
建议在git clone --recursive https://github.com/github/vscode-codeql-starter.git 后，新建 vscode-codeql-starter/codeql-custom-queries-tutorial 文件夹来作为学习项目，并新建环境包qlpack.yml，最后在qlpack.yml下使用codeql pack instal来更新包

• qlpack.yml (fork from starter)

# Change 'getting-started' to a user name or organization that you have write access to
name: getting-started/codeql-extra-queries-tutorial
version: 0.0.0
dependencies:
  # This uses the latest version of the codeql/python-all library.
  # You may want to change to a more precise semver string.
  codeql/tutorial: "*"

Thief (using logical connectives, quantifiers, and aggregates)

exists and forall

[!NOTE] exists 为 QL 中的 量词

• exists
exists(<variable declarations> | <formula>)
  表示 formula 成立则exists也成立，也可以用exists(<variable declarations> | <formula 1> | <formula 2> 来表达两个 formula，但其实际含义等价于 exists(variable declarations>| <formaula 1> and <formula 2>)。
  个人理解: 在formula 1成立的情况下，至少有一个formula 2 成立

from int x
where exists(| x in [1..10] | x = 5)
select x

[!NOTE] forall 为 QL 中的 量词

• forall
forall(<variable declarations> | <formula 1> | <formula 2>)
forall的实际含义为not exists(<vars> | <formula 1> | not <formula 2>)
  个人理解: 在formula 1成立的情况下，所有的变量也都满足formula 2

from int y
where y in [1..10]
    and forall(int c | y = c | c > 0)
select y

The real investigation

问题	答案
1	小偷身高超过150厘米吗？	是的
2	小偷有金发吗？	没有
3	小偷是秃头吗？	没有
4	小偷小于30岁吗？	没有
5	小偷住在城堡东边吗？	是的
6	小偷有黑色或棕色的头发吗？	是的
7	小偷身高超过180厘米，身高低于190厘米吗？	没有
8	小偷是村里年龄最大的人吗？	没有

import tutorial

from Person person
where person.getHeight() > 150
    and not person.getHairColor() = "blond"
    and exists(string s | person.getHairColor() = s )
    and not person.getAge() < 30
    and person.getLocation() = "east"
    and (person.getHairColor() = "black" or person.getHairColor() = "brown")
    and not (person.getHeight() > 180 and person.getHeight() < 190)
    and exists(Person other | other.getAge() > person.getAge() )
select person, "may be a thief."

More advanced queries

常见的聚合有count、max、min、avg（平均值）和sum。
sum使用聚合的一般方法是：

<aggregate>(<variable declarations> | <logical formula> | <expression>)

可以使用max聚合来查找村庄中年龄最大的人的年龄：

max(int i | exists(Person p | p.getAge() = i) | i)

// 具体使用为
from Person t
where t.getAge() = max(int i | exists(Person p | p.getAge() = i) | i)
select t

使用有序聚合，可以直接返回最年老的村民。

select max(Person p | | p order by p.getAge())

Capture the culprit

问题	答案
…	…	…
9	小偷是村里最高的人吗？	没有
10	小偷比一般村民矮吗？	是的
11	小偷是村东最年长的人吗？	是的

import tutorial

from Person person
where person.getHeight() > 150
    and not person.getHairColor() = "blond"
    and exists(string s | person.getHairColor() = s )
    and not person.getAge() < 30
    and person.getLocation() = "east"
    and (person.getHairColor() = "black" or person.getHairColor() = "brown")
    and not (person.getHeight() > 180 and person.getHeight() < 190)
    // and exists(Person other | other.getAge() > person.getAge() )
    and not person = max(Person p | | p order by p.getAge())
    and person.getHeight() < avg(Person p|  | p.getHeight())
    and person = max(Person p | p.getLocation() = "east" | p order by p.getAge())
select person, "may be a thief."

Fire starter (using QL predicates and classes)

Travel restrictions

[!Note] 定义谓词

• 谓语的名字总是以小写字母开头。
• 也可以定义带有结果的谓词。在这种情况下，关键字predicate被替换为结果的类型。这就像引入一个新的参数，特殊变量result。

int getAge(){
	result = ...
}

• 列出所有的南方人

from Person p
where isSouthern(p)
select p

// 或者使用类来封装
class Southerner extends Person {
  Southerner() { isSouthern(this) }
}

// 使用类来进行查询
from Southerner s
select s

QL中的类表示一个逻辑属性：当一个值满足该属性时，它就是该类的成员。这意味着一个值可以在许多类中——在一个特定的类中并不会阻止它也在其他类中。其中与类名同名的谓词，成为特征谓词(characteristic predicate)，类中其他谓词称为成员谓词(member predicate)。

表达式isSouthern(this)定义了类表示的逻辑属性，称为其_特征谓词_。它使用一个特殊变量this，并指示Person“this“是一个Southerner，如果属性isSouthern(this)成立。

可以理解OOP语言中的this，只不过多了一轮谓词查询。

[!question]
即便 Docs 中强调不要将 Southerner() 理解为构造函数，但 Southerner() { isSouthern(this) 根据上下文来理解，还是和OOPL中的构建函数相似，只不过Southerner 类的返回可以理解为 某个具体的查询结果集合，而不是一个具体的对象；同时，在构造时，也是有默认生成的含义，如在使用from Southerner s时，可以理解为s是Southerner关系的查询结果集合，就是困惑是from Southerner s 导致调用Southerner() { isSouthern(this)，还是说当类定义时，已经调用Southerner() { isSouthern(this)。

个人猜测，是在具体使用from Southerner s时，才启动Southerner() { isSouthern(this)查询，就是这个思路的话，可能需要做一些优化，来提高性能。

同样，QL中的类，可以还用父类中的谓词，如

import tutorial

predicate isSouthern(Person p) {
    p.getLocation() = "south"
}

class Southerner extends Person {
    Southerner() { isSouthern(this) }
}

from Southerner s
select s, s.getAge()

定义 Child 类，小于10岁，需要提供谓词isAllowedIn，其规则是只允许 Child 前往 对应的Location

class Child extends Person {
    // the characteristic predicate
    Child() { this.getAge() < 10 }

    // a member predicate
    override predicate isAllowedIn(string region) {
        region = this.getLocation()
    }
}

// 查询可以前往 north 的 Child
from Child c, string region
where region = "north"
and c.isAllowedIn(region)
select c

[!question] Tutorial Q1
你知道纵火犯住在南方_，_他们一定能够去北方。写一个查询来找到可能的嫌疑犯。你也可以扩展select子句来列出嫌疑犯的年龄。这样你就可以清楚地看到所有的孩子都被排除在列表之外。

import tutorial

predicate isSouthern(Person p) {
    p.getLocation() = "south"
}

class Southerner extends Person {
    Southerner() { isSouthern(this) }
}

class Child extends Person {
    // the characteristic predicate
    Child() { this.getAge() < 10 }

    // a member predicate
    override predicate isAllowedIn(string region) {
        region = this.getLocation()
    }
}

from Southerner s
where s.isAllowedIn("north")
select s, s.getAge()

[!Done]

Identify the bald bandits

[!question] 您现在可以编写一个查询来选择允许进入北方的秃头南方人。

[!note] 注意可以构建新的谓词

predicate isBald(Person p) {
	not exists (string c | p.getHairColor() = c)
	}

import tutorial

predicate isSouthern(Person p) {
    p.getLocation() = "south"
}

class Southerner extends Person {
    Southerner() { isSouthern(this) }
}

class Child extends Person {
    /* the characteristic predicate */
    Child() { this.getAge() < 10 }
  
    /* a member predicate */
    override predicate isAllowedIn(string region) { region = this.getLocation() }
}

predicate isBald(Person p) { not exists(string c | p.getHairColor() = c) }

from Southerner s
where s.isAllowedIn("north") and isBald(s)
select s

[!done]

[!Question] 为什么 返回结果中没有小孩的年龄

个人理解: 在 s.isAllowedIn("north") 时，查询到一些Person数据，同时这些Person实际属于Child，导致其isAllowedIn谓词被复写，s.isAllowedIn("north") 的查询结果也将由Child中的isAllowedIn进行判别。

有点像Java中的继承问题

验证：
在Child的基础上，设计CC类来继承。验证结果显示，lraPerson在实际的isAllownedIn，为CC中isAllownedIn，且s被允许任何地方。

Heir (using recursion)

[!NOTE] 谓词中 result 的另一种用法

Person childOf(Person p) {
	// p = parentOf(result)，表示 p 是 result 的 parent
	p = parentOf(result)
}

递归 – Recursion

可以实现递归的方法来查找祖先

// 查找祖先
Person ancestorOf(Person p) {
    result = parentOf(p) or
    result = parentOf(ancestorOf(p) )
}

在QL中除了上面直接定义的递归方式外，还存在+ 和 * 两种特殊符号来实现递归:

• parentOf+(p)
  • 应用parentOf()谓词到p一次或多次。这相当于ancestorOf(p)。
• parentOf*(p)
  • 将parentOf()谓词应用于p零次或多次，因此它返回p的祖先或p本身。

[!question] 查找 King Basil 在世的亲人

import tutorial

// 查找亲子关系
Person childOf(Person p) {
    // p = parentOf(result)，表示 p 是 result 的 parent
    p = parentOf(result)
}

// 查找祖先
Person ancestorOf(Person p) {
    result = parentOf(p) or
    result = parentOf(ancestorOf(p) )
}

// 存在共同的祖先
Person relativeOf(Person p) {
    parentOf*(result) = parentOf*(p)
}

from Person p
// 注意也可以使用，但应该会多一些查询？
// where relativeOf(p) = relativeOf("King Basil")
where p = relativeOf("King Basil")
    and not p.isDeceased()
select p

[!Done]

Select the true heir

[!Question]
真在的检查人不能有案底，即不是小偷和放火人。

import tutorial

predicate hasCriminalRecord(Person p) {
    p = "Charlie"
    or p = "Hugh"
    or p = "Hester"
}

Person relativeOf(Person p) {
    parentOf*(result) = parentOf*(p)
}

from Person p
where p = relativeOf("King Basil")
    and not p.isDeceased()
    and not hasCriminalRecord(p)
select p

[!Done]
Clara is the true heir.

Cross the river

Ref: Cross the river — CodeQL (github.com)

[!Question] River crossing puzzle – 渡河拼图
A man is trying to ferry a goat, a cabbage, and a wolf across a river. His boat can only take himself and at most one item as cargo. His problem is that if the goat is left alone with the cabbage, it will eat it. And if the wolf is left alone with the goat, it will eat it. How does he get everything across the river?

一个男人正试图把一只山羊、一棵卷心菜和一只狼渡过一条河。他的船只能把自己和最多一件东西作为货物。他的问题是，如果山羊和卷心菜单独在一起，它会吃了它。如果狼和山羊单独在一起，它会吃了它。他是怎么把所有东西都弄过河的？

/** A possible cargo item. */
class Cargo extends string {
  Cargo() {
    this = "Nothing" or
    this = "Goat" or
    this = "Cabbage" or
    this = "Wolf"
  }
}

/** One of two shores. */
class Shore extends string {
  Shore() {
    this = "Left" or
    this = "Right"
  }

  /** Returns the other shore. */
  Shore other() {
    this = "Left" and result = "Right"
    or
    this = "Right" and result = "Left"
  }
}

/** Renders the state as a string. */
string renderState(Shore manShore, Shore goatShore, Shore cabbageShore, Shore wolfShore) {
  result = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore
}

/** A record of where everything is. */
class State extends string {
  Shore manShore;
  Shore goatShore;
  Shore cabbageShore;
  Shore wolfShore;

  State() { this = renderState(manShore, goatShore, cabbageShore, wolfShore) }

  /** Returns the state that is reached after ferrying a particular cargo item. */
  State ferry(Cargo cargo) {
    cargo = "Nothing" and
    result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore)
    or
    cargo = "Goat" and
    result = renderState(manShore.other(), goatShore.other(), cabbageShore, wolfShore)
    or
    cargo = "Cabbage" and
    result = renderState(manShore.other(), goatShore, cabbageShore.other(), wolfShore)
    or
    cargo = "Wolf" and
    result = renderState(manShore.other(), goatShore, cabbageShore, wolfShore.other())
  }

  /**
   * Holds if the state is safe. This occurs when neither the goat nor the cabbage
   * can get eaten.
   */
  predicate isSafe() {
    // The goat can't eat the cabbage.
    (goatShore != cabbageShore or goatShore = manShore) and
    // The wolf can't eat the goat.
    (wolfShore != goatShore or wolfShore = manShore)
  }

//   /**
//    * Returns all states that are reachable via safe ferrying.
//    * `path` keeps track of how it is achieved and `steps` keeps track of the number of steps it takes.
//    */
//   State reachesVia(string path, int steps) {
//     // Trivial case: a state is always reachable from itself
//     steps = 0 and this = result and path = ""
//     or
//     // A state is reachable using pathSoFar and then safely ferrying cargo.
//     exists(int stepsSoFar, string pathSoFar, Cargo cargo |
//       result = this.reachesVia(pathSoFar, stepsSoFar).safeFerry(cargo) and
//       steps = stepsSoFar + 1 and
//       // We expect a solution in 7 steps, but you can choose any value here.
//       steps <= 7 and
//       path = pathSoFar + "\n Ferry " + cargo
//     )
//   }

/**
   * Returns all states that are reachable via safe ferrying.
   * `path` keeps track of how it is achieved.
   * `visitedStates` keeps track of previously visited states and is used to avoid loops.
   */
  State reachesVia(string path, string visitedStates) {
    // Trivial case: a state is always reachable from itself.
    this = result and
    visitedStates = this and
    path = ""
    or
    // A state is reachable using pathSoFar and then safely ferrying cargo.
    exists(string pathSoFar, string visitedStatesSoFar, Cargo cargo |
      result = this.reachesVia(pathSoFar, visitedStatesSoFar).safeFerry(cargo) and
      // The resulting state has not yet been visited.
      not exists(visitedStatesSoFar.indexOf(result)) and
      visitedStates = visitedStatesSoFar + "/" + result and
      path = pathSoFar + "\n Ferry " + cargo
    )
  }

  /** Returns the state that is reached after safely ferrying a cargo item. */
  State safeFerry(Cargo cargo) { result = this.ferry(cargo) and result.isSafe() }
}

/** The initial state, where everything is on the left shore. */
class InitialState extends State {
  InitialState() { this = renderState("Left", "Left", "Left", "Left") }
}

/** The goal state, where everything is on the right shore. */
class GoalState extends State {
  GoalState() { this = renderState("Right", "Right", "Right", "Right") }
}

from string path
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
select path

[!Done]

[!Question] 1）reachesVia 初始化的具体过程；2）最终查询过程中 any 的作用

[!Answer] 1）reachesVia的初始化具体过程
reachesVia 方法是用来探索从初始状态出发，通过一系列安全的渡运操作，可以达到哪些状态。这个方法有两个重要的参数：path 和 visitedStates。path 记录从初始状态到当前状态的操作序列，visitedStates 记录已经访问过的状态，以避免循环。

• Trivial case：最简单的情况，即一个状态总是可以从自身到达自身，这时没有移动，没有新的状态加入到visitedStates，路径path为空字符串。
• General case：更通用的情况是，从某个已知可达的状态，通过安全地渡运一个货物（Cargo），达到一个新的状态。这里使用了递归的方式：
  • 从某个状态出发，尝试所有可能的安全渡运操作。
  • 每次渡运后，得到一个新状态，如果这个状态没有在visitedStates中出现过，那么这个新状态就是一个有效的状态。
  • 更新visitedStates和path，将新状态和对应的操作加入。

[!Answer] 最终查询过程中any的作用

这里的使用any(InitialState i)和any(GoalState g)表达的是：从任意一个初始状态（虽然在此场景中只定义了一个初始状态）到任意一个目标状态的转换路径。虽然实际上可能只定义了一个初始状态和一个目标状态，使用any()函数确保查询的通用性和正确性，可以处理存在多个初始或目标状态的情况。

from string path
where any(InitialState i).reachesVia(path, _) = any(GoalState g)
select path