序言

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

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

QL规范

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

//存在 exists 临时变量
exists(string c | t.getHairColor() = c)

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

谁是小偷？

地址：find-the-theif，主要考察聚合搜索。

v1.0版本：

高级用法，聚合搜索：

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

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

最终版，找到小偷是Hester

找到纵火犯

地址：catch-the-fire-starter

定义新谓词isSouthern：

import tutorial
//特征谓词
predicate isSouthern(Person p) {
    p.getLocation() = "south"
}
// 找到所有的南方人
from Person p
where isSouthern(p)
select p

或者可以定义一个类：

class Southerner extends Person {
    Southerner(){
        isSouthern(this)
    }
}
//找到全部
from Southerner sp
select sp

重载谓词：

class Child extends Person {
    Child(){
        this.getAge()<10
    }
    override predicate isAllowedIn(string region){
        this.getLocation() = region
    }
}

找到了纵火犯

加冕合法继承人

地址：crown-the-rightful-heir

覆盖成员谓词：

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的递归用法：


// 返回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)
}

QL递归举例：

// 找到0～100 之间所有的整数
int findNumber(){
    result = 0
    or 
    result <=100 and result = findNumber()+1
}
select findNumber()

// 找到0～100之间的所有偶数
int getAnEven() {
  result = 0
  or
  result <= 100 and result = getAnOdd() + 1
}
 
int getAnOdd() {
  result = getAnEven() + 1
}
 
select getAnEven()

过河

地址：cross-the-river

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

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