代码分析平台CodeQL学习手记（八）
导语：在本文中，我们为读者详细介绍如何综合利用类、谓词和递归等知识来编写QL查询代码，从而解决经典的过河问题。
过河问题是一个经典的逻辑问题，它要求在一定约束下将山羊、卷心菜和狼运到对岸。在本文中，我们将为读者详细介绍如何综合利用类、谓词和递归等知识点来编写查询代码，从而解决这个经典的逻辑问题。
关于过河问题
一位农夫带着一头狼，一只山羊和一筐卷心菜过河，河边有一条小船，农夫划船每次只能载狼、山羊、卷心菜三者中的一个过河。农夫不在旁边时，狼会吃掉山羊，山羊会吃卷心菜。问农夫该如何过河？
这个问题的答案，实际上就是关于如何摆渡这些货物过河的详细步骤，比如“首先摆渡山羊过河，回来时什么都不带。然后，把卷心菜运过去，并将某货物带回来……”
实际上，解决这个问题的方法有很多，并且，这些方法都可以通过QL语言进行实现。在实现这些解决方法的过程中，需要通过QL语言来定义相应的类、谓词以及递归等概念，对于不熟悉这些概念的读者，可以先阅读之前的文章，那里有相关的介绍。当然，这里给出的解决方法，只是各种可行的方法中的一种而已，感兴趣的读者，也可以编写自己的查询！
模拟问题中的各种元素
在这个过河问题中，基本的组成元素可以分为两类：货物和河岸。其中，货物包括山羊、卷心菜和狼；而河岸实际上包括河流两边的对岸。现在，我们将这些表示为QL语言中的类。
首先，定义一个包含不同货物的Cargo类。需要注意的是，由于这个农夫也可以自己渡河，啥也不带，所以，直接将“Nothing”明确定义为一件货物是很有帮助的。
/** A possible cargo item. */
class Cargo extends string {
Cargo() {
this = "Nothing" or
this = "Goat" or
this = "Cabbage" or
this = "Wolf"
}
}其次，任何货物都可以位于两个河岸中的一个上面。为了便于区分，这里将河岸分别命名为“左岸”和“右岸”。为此，我们可以定义一个Shore类来表示河岸，其中包含“Left”和“Right”，本别表示“左岸"和"右岸"。
此外，农夫可能需要在两岸之间多次摆渡，这就涉及到“对岸”的概念，所以，我们可以在Shore类中定义一个成员谓词，专门求对岸，例如，给出左岸，该谓词将返回右岸，反之亦然。
/** 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"
}
}此外，我们还需要设法跟踪农夫、山羊、卷心菜和狼的位置。在这里，我们把这些组合在一起的位置信息称为“状态”。为此，我们可以定义一个类State，来表示每件货物的位置。例如，如果农夫在左岸，山羊在右岸，卷心菜和狼在左岸，那么，当前的状态应该是左、右、左、左。
大家可能已经发现，如果我们引入一些变量来表示农夫和货物所在河岸的话，将是非常有帮助的。在类的定义中，这些临时变量被称为字段。
/** A record of where everything is. */
class State extends string {
Shore manShore;
Shore goatShore;
Shore cabbageShore;
Shore wolfShore;
State() { this = manShore + "," + goatShore + "," + cabbageShore + "," + wolfShore }
}为了解决这个过河问题，我们对其中的两种特定的状态非常关注，即初始状态和目标状态。假设刚开始的时候，所有货物都在左岸，成功渡河后，所有货物都在右岸，那么，我们可以通过State类派生两个子类，一个是表示初始状态的InitialState类，另一个是表示目标状态的GoalState类。
/** The initial state, where everything is on the left shore. */
class InitialState extends State {
InitialState() { this = "Left" + "," + "Left" + "," + "Left" + "," + "Left" }
}
/** The goal state, where everything is on the right shore. */
class GoalState extends State {
GoalState() { this = "Right" + "," + "Right" + "," + "Right" + "," + "Right" }
}需要注意的是，我们可以引入一个助手谓词renderState，来帮我们以适当的形式呈现状态数据。
好了，到目前为止，我们的QL代码如下所示：
/** 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) }
}
/** 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") }
}模拟“摆渡”动作
摆渡就是将农夫和一种货物送到对岸，这时，自然会产生一个新的状态。
为了模拟这种行为，我们可以在State类中引入一个成员谓词，比如将其命名为ferry，让它来指出在摆渡特定货物后状态会变成什么样子。在编写这个谓词时，我们可以借助于前面定义的谓词other。
/** 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())
}当然，并非所有的摆渡动作都是可行的。所以，我们需要添加一些额外的限制，以确保摆渡过程是“安全的”。也就是说，摆渡过程中不能出现山羊或卷心菜被吃掉的情况。例如，我们可以：
1. 定义一个谓词isSafe，使其在状态本身是安全的时候才成立。实际上，我们就是用它来表示山羊和卷心菜都不会被吃掉的条件。
2. 定义一个谓词safeFerry，用以约束谓词ferry只能执行安全的摆渡动作。
/**
* 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 the state that is reached after safely ferrying a cargo item. */
State safeFerry(Cargo cargo) { result = this.ferry(cargo) and result.isSafe() }寻找状态迁移的路径
实际上，我们要编写的查询的主要目的，就是寻找一条能够从初始状态到达目标状态的路径，即由连续摆渡动作组成的一个列表。我们可以通过用换行符（“\n”）分隔的各个货物来表示这种“列表”。
在寻找答案的过程中，我们必须要避免“没有尽头的”路径。例如，农夫可以把山羊来回摆渡很多次，虽然这种动作是不会触发不安全的状态的，但是，即使不停重复这个动作，只会徒增渡河次数，却对于解决问题没有任何帮助。
为了帮助我们将路径的渡河次数限制在一定的范围内，可以定一个成员谓词State reachesVia(string path, int steps)，其返回结果是可以从当前状态（this）通过给定路径以指定的有限步数到达的所有状态。
实际上，我们可以将其写成递归型谓词，具体的终止条件和递归步骤如下所示：
· 如果this是结果状态，那么它（可以直接）通过一个空路径零步到达结果状态。
· 如果this可以到达某个中间状态（对应于path和steps的某些值），并且从该中间状态到结果状态存在safeFerry操作，则可以达到任何其他状态。
为了确保谓词的执行次数是有限的，我们应该将steps限制为特定的值，例如steps<=7。
/**
* 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
)
}然而，尽管这确保了渡河方案的步数是有限的，但如果步数的上界很大的话，其中仍然可能包含循环。换句话说，由于存在多次重复经历相同的状态，所以，渡河方案的效率是非常低的。
实际上，我们可以完全避免计算步数，这样也就无需为步数选择上限而操心了。例如，如果我们跟踪已经历过的状态，并确保每个摆渡操作都通向一个新的状态的话，那么得到的渡河方案就肯定不会包含任何循环。
为此，我们可以将之前定义的成员谓词更改为State reachesVia(string path, string visitedStates)。这个该谓词的返回结果，就是可以通过给定路径，从当前状态（this）开始，在不重复之前经历过的状态的情况下，可以到达的所有状态。
· 和前面一样，如果this是结果状态，那么它（通常可）通过一个空路径和一个表示已经历状态的空字符串到达结果状态。
· 如果this可以通过某路径在不重复之前经历过的状态的情况下达到某个中间状态，并且存在从中间状态到结果状态的safeFerry操作的话，则可以到达任何其他状态。需要注意的是，要想检查某个状态以前是否被经历过，可以检查是否存在该状态发生时的visitedStates索引。
/**
* 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(int i | i = visitedStatesSoFar.indexOf(result)) and
visitedStates = visitedStatesSoFar + "/" + result and
path = pathSoFar + "\n Ferry " + cargo
)
}展示找到的路径
定义好相关的类和谓词之后，我们就可以编写一个select子句来返回找到的路径了。
from string path where any(InitialState i).reachesVia(path, _) = any(GoalState g) select path
其中，谓词reachesVia的第二个参数是一个特殊的符号，即_，它代表visitedStates的任意值。实际上，我们通常在无需关心，或可以忽略的地方使用这个符号。
下面，我们给出完整的代码：
/**
* A solution to the river crossing puzzle.
*/
/** 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 the state that is reached after safely ferrying a cargo item. */
State safeFerry(Cargo cargo) { result = this.ferry(cargo) and result.isSafe() }
string towards() {
manShore = "Left" and result = "to the left"
or
manShore = "Right" and result = "to the right"
}
/**
* 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(int i | i = visitedStatesSoFar.indexOf(result)) and
visitedStates = visitedStatesSoFar + "/" + result and
path = pathSoFar + "\n Ferry " + cargo
)
}
}
/** 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 + "."运行结果如下图所示：
目前，谓词reachesVia中定义的路径只显示货物的摆渡顺序。所以，我们还可改进这个谓词和相应的select子句，以使得返回的渡河方案更加容易理解，例如：
· 显示更多信息，如货物的运送方向，例如“将山羊送到左岸”。
· 详细描述每一步的状态，例如“山羊：左，农夫：左，卷心菜：右，狼：右”。
· 以更“可视化”的方式显示路径，例如使用箭头显示状态之间的转换。
其他示例查询
下面是一些解决渡河问题的其他示例查询:
· 该查询使用一个改进版的path变量来更细致地描述结果路径。：
完整的代码请参阅网页https://lgtm.com/query/659603593702729237/。
· 该查询使用了抽象类和谓词，以不同的方式对农夫和货物进行建模。此外，它还提供了更可视化的方式来显示结果路径。
完整的代码请参阅页面https://lgtm.com/query/1025323464423811143/。
· 这个查询将通过代数数据类型来对各种情形进行建模，而不是将所有要素都定义为String的子类。
完整的代码请参阅页面https://lgtm.com/query/7260748307619718263/。
小结
在本文中，我们为读者详细介绍如何综合利用类、谓词和递归等知识来编写QL查询代码，从而解决经典的过河问题。希望通过这些具体的例子，能够帮助大家进一步熟悉这些重要的概念。
备注：本系列文章乃本人在学习CodeQL平台过程中所做的笔记，希望能够对大家有点滴帮助——若果真如此的话，本人将备感荣幸。
参考资料：
https://help.semmle.com/
发表评论
提供云计算服务