0%

CodeQL学习笔记(三)

序言

襄阳好风日,留醉与山翁。

和CodeQL官方示例学习QL写法。

QL规范

总结从例子中学到的语法:

1
2
3
4
5
//存在 exists 临时变量
exists(string c | t.getHairColor() = c)

// 聚合 count, max, min, avg(average),sum
<aggregate>(<variable declarations> | <logical formula> | <expression>)

谁是小偷?

地址:find-the-theif,主要考察聚合搜索。

v1.0版本:

image-20211026162237269

高级用法,聚合搜索:

小偷是村子里年龄最大的人:

1
2
3
from Person t
where t.getAge() = max(int i | exists(Person p | p.getAge()) | i)
select t

有序聚合,有序选出最老的人:

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

image-20211026165232185

最终版,找到小偷是Hester

image-20211026185415157

找到纵火犯

地址:catch-the-fire-starter

定义新谓词isSouthern:

1
2
3
4
5
6
7
8
9
import tutorial
//特征谓词
predicate isSouthern(Person p) {
p.getLocation() = "south"
}
// 找到所有的南方人
from Person p
where isSouthern(p)
select p

或者可以定义一个类:

1
2
3
4
5
6
7
8
class Southerner extends Person {
Southerner(){
isSouthern(this)
}
}
//找到全部
from Southerner sp
select sp

重载谓词:

1
2
3
4
5
6
7
8
class Child extends Person {
Child(){
this.getAge()<10
}
override predicate isAllowedIn(string region){
this.getLocation() = region
}
}
image-20211026193151828

找到了纵火犯

image-20211026193936560

加冕合法继承人

地址:crown-the-rightful-heir

覆盖成员谓词:

1
2
3
4
5
6
7
8
9
10
class Child extends Person {

/* the characteristic predicate */
Child() { this.getAge() < 10 }

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

谓词isAllowedIn(string region)应用于表示村民的变量p上的时候,如果变量p的类型不是Child,则使用该谓词原来的定义;但是如果变量p的类型为Child,也就是说这个变量表示的村民是一个孩子,那么,该谓词将会使用Child类中的新定义,从而覆盖原来的代码。

QL的递归用法:

1
2
3
4
5
6
7
8
9
10

// 返回p的孩子 result是默认的返回值
Person childOf(Person p) { parentOf(result) = p }


//返回p的所有祖先 存在迭代关系
Person ancestorOf(Person p){
result = parentOf(p) or
result = parentOf(childOf(p))
}

transitive closure

传递闭包 QL里两个特殊的符号 + ,*

  • parentOf+(p) applies the parentOf() predicate to p one or more times. This is equivalent to ancestorOf(p).
  • parentOf*(p) applies the parentOf() predicate to p zero or more times, so it returns an ancestor of p or p itself.

+递归一次或者更多,和ancestorOf效果一样

*递归0次或者更多,返回p的一层祖先或者p自身

返回p的所有亲戚

1
2
3
Person relativeOf(Person p){
parentOf*(result) = parentOf*(p)
}
image-20211026204546706

QL递归举例:

1
2
3
4
5
6
7
// 找到0~100 之间所有的整数
int findNumber(){
result = 0
or
result <=100 and result = findNumber()+1
}
select findNumber()
1
2
3
4
5
6
7
8
9
10
11
12
// 找到0~100之间的所有偶数
int getAnEven() {
result = 0
or
result <= 100 and result = getAnOdd() + 1
}

int getAnOdd() {
result = getAnEven() + 1
}

select getAnEven()

过河

地址:cross-the-river

很有趣的一道题,推荐去看原文。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
import tutorial

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() }

/** man's move */
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) {
// Reachable in 1 step by ferrying a specific cargo
exists(Cargo cargo |
result = this.safeFerry(cargo) and
visitedStates = result and
path = "First " + cargo + " is ferried " + result.towards() + ","
)
or
// Reachable by first following pathSoFar and then ferrying cargo
exists(string pathSoFar, string visitedStatesSoFar, Cargo cargo |
result = this.reachesVia(pathSoFar, visitedStatesSoFar).safeFerry(cargo) and
// resulting state is not visited yet
not exists(int i | i = visitedStatesSoFar.indexOf(result)) and
visitedStates = visitedStatesSoFar + "_" + result and
path = pathSoFar + "\nthen " + cargo + " is ferried " + result.towards() + ","
)
}
}

/** 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 + "."

image-20211026220931326