CodeQL 文档
CodeQL 资源

公式

公式定义了表达式中使用的自由变量之间的逻辑关系。

根据分配给这些 自由变量 的值，公式可以为真或假。当公式为真时，我们通常说公式成立。例如，公式 x = 4 + 5 当 9 分配给 x 时成立，但对于其他分配给 x 的值则不成立。某些公式没有任何自由变量。例如 1 < 2 始终成立，而 1 > 2 从不成立。

通常在类、谓词和 select 子句的正文中使用公式来限制它们引用的值的集合。例如，您可以定义一个类，其中包含所有满足公式 i in [0 .. 9] 的整数 i。

以下部分描述了 QL 中可用的公式类型。

比较

比较公式的形式为

<expression> <operator> <expression>

请参见下表以概述可用的比较运算符。

顺序

要使用这些顺序运算符之一比较两个表达式，每个表达式都必须具有类型，并且这些类型必须是 兼容 且 可排序 的。

名称 符号
大于 >
大于或等于 >=
小于 <
小于或等于 <=

例如，公式 "Ann" < "Anne" 和 5 + 6 >= 11 都成立。

相等

要使用 = 比较两个表达式，至少一个表达式必须具有类型。如果两个表达式都具有类型，那么它们的类型必须是 兼容 的。

要使用 != 比较两个表达式，两个表达式都必须具有类型。这些类型也必须是 兼容 的。

名称 符号
等于 =
不等于 !=

例如，x.sqrt() = 2 当 x 为 4 时成立，而 4 != 5 始终成立。

对于表达式 A 和 B，公式 A = B 成立，当存在一对值（一个来自 A，一个来自 B）相同时。换句话说，A 和 B 至少有一个共同的值。例如，[1 .. 2] = [2 .. 5] 成立，因为两个表达式都具有值 2。

因此，A != B 与 否定 not A = B 的含义截然不同 [1]

  • A != B 成立，当存在一对值（一个来自 A，一个来自 B）不相同时。
  • not A = B 成立，当不存在一对值相同时。换句话说，A 和 B 没有共同的值。

示例

  1. 如果两个表达式都具有单个值（例如 1 和 0），那么比较很简单
    • 1 != 0 成立。
    • 1 = 0 不成立。
    • not 1 = 0 成立。
  2. 现在比较 1 和 [1 .. 2]
    • 1 != [1 .. 2] 成立，因为 1 != 2。
    • 1 = [1 .. 2] 成立，因为 1 = 1。
    • not 1 = [1 .. 2] 不成立，因为存在一个共同的值 (1)。
  3. 比较 1 和 int empty() { none() }（定义空整数集的谓词）
    • 1 != empty() 不成立，因为 empty() 中没有值，因此没有值不等于 1。
    • 1 = empty() 也不成立，因为 empty() 中没有值，因此没有值等于 1。
    • not 1 = empty() 成立，因为不存在共同的值。

类型检查

类型检查是一个公式，其形式为

<expression> instanceof <type>

您可以使用类型检查公式来检查表达式是否具有特定类型。例如，x instanceof Person 当变量 x 具有类型 Person 时成立。

范围检查

范围检查是一个公式，其形式为

<expression> in <range>

您可以使用范围检查公式来检查数字表达式是否在给定的 范围 内。例如，x in [2.1 .. 10.5] 当变量 x 介于值 2.1 和 10.5 之间（包括 2.1 和 10.5 本身）时成立。

请注意，<expression> in <range> 等效于 <expression> = <range>。这两个公式都检查由 <expression> 表示的值集是否与由 <range> 表示的值集相同。

对谓词的调用

调用是一个公式或 表达式，它包含对谓词的引用和多个参数。

例如，isThree(x) 可以是对谓词的调用，当参数 x 为 3 时成立，而 x.isEven() 可以是对成员谓词的调用，当 x 为偶数时成立。

对谓词的调用也可以包含闭包运算符，即 * 或 +。例如，a.isChildOf+(b)是对 isChildOf() 的 传递闭包 的调用，因此当 a 是 b 的后代时成立。

谓词引用必须解析为一个谓词。有关谓词引用解析方式的更多信息，请参见“名称解析。”

如果调用解析为没有结果的谓词，那么调用就是一个公式。

也可以调用具有结果的谓词。这种调用是 QL 中的表达式，而不是公式。有关更多信息，请参见“对谓词的调用（具有结果）。”

成员谓词仅适用于特定类的成员，并且对成员谓词的调用具有匹配类型的接收者。从语法上讲，如果调用包含点，则点之前的表达式指定调用的接收者。例如，x 是调用 x.isEven() 的接收者。

对于对封闭类成员谓词的调用（即 this 的值），可以从语法上省略接收者。在这种情况下，我们说该调用具有隐式 this 接收者。例如，在以下示例中，isOdd() 中的 isEven() 调用是具有隐式 this 接收者的成员谓词调用，并且该调用等效于 this.isEven()

class OneTwoThree extends int {
  OneTwoThree() { this = 1 or this = 2 or this = 3 }

  predicate isEven() { this = 2 }

  predicate isOdd() { not isEven() }
}

使用隐式 this 接收者可能会使难以发现通过未能将隐式 this 变量与其他变量相关联而引入笛卡尔积的谓词，这会对查询性能产生负面影响。有关笛卡尔积的更多信息，请参阅“故障排除查询性能”。

可以通过 warnOnImplicitThis 属性为 CodeQL 包 启用有关隐式 this 接收者的警告。

带括号的公式

带括号的公式是指任何用括号 ( 和 ) 包围的公式。此公式与封闭公式具有完全相同的含义。括号通常有助于提高可读性并将某些公式组合在一起。

量化公式

量化公式引入临时变量并在其主体中的公式中使用它们。这是一种从现有公式创建新公式的方法。

显式量词

以下显式“量词”与数学逻辑中常见的 exist 和 forall 量词相同。

exists

此量词具有以下语法

exists(<variable declarations> | <formula>)

您还可以编写 exists(<variable declarations> | <formula 1> | <formula 2>)。这等效于 exists(<variable declarations> | <formula 1> and <formula 2>)。

此量化公式引入了一些新变量。如果变量可以取至少一组值，使得主体中的公式为真，则它成立。

例如，exists(int i | i instanceof OneTwoThree) 引入了一个类型为 int 的临时变量，如果该变量的任何值都具有类型 OneTwoThree，则它成立。

forall

此量词具有以下语法

forall(<variable declarations> | <formula 1> | <formula 2>)

forall 引入了一些新变量，并且通常在主体中具有两个公式。如果 <formula 2> 对 <formula 1> 成立的每个值都成立，则它成立。

例如，forall(int i | i instanceof OneTwoThree | i < 5) 成立，如果所有属于 OneTwoThree 类的整数也小于 5。换句话说，如果 OneTwoThree 中存在一个大于或等于 5 的值，则该公式不成立。

请注意，forall(<vars> | <formula 1> | <formula 2>) 在逻辑上与 not exists(<vars> | <formula 1> | not <formula 2>) 相同。

forex

此量词具有以下语法

forex(<variable declarations> | <formula 1> | <formula 2>)

此量词作为以下内容的简写形式存在

forall(<vars> | <formula 1> | <formula 2>) and
exists(<vars> | <formula 1> | <formula 2>)

换句话说，forex 的工作方式与 forall 类似，但它确保至少存在一个 <formula 1> 成立的值。要了解这为什么有用，请注意 forall 量词可能会平凡地成立。例如，forall(int i | i = 1 and i = 2 | i = 3) 成立：不存在等于 1 和 2 的整数 i，因此主体的第二部分 (i = 3) 对第一部分成立的每个整数都成立。

由于这通常不是您在查询中想要的行为，因此 forex 量词是一个有用的简写形式。

隐式量词

可以使用“不关心表达式”引入隐式量化变量。当您需要引入一个变量作为谓词调用的参数使用，但并不关心其值时，可以使用它们。有关更多信息，请参阅“不关心表达式”。

逻辑连接词

您可以在 QL 中的公式之间使用一些逻辑连接词。它们允许您将现有公式组合成更长、更复杂的公式。

要指示公式的哪些部分应该优先，可以使用括号。否则，优先级顺序从最高到最低如下

  1. 否定 (not)
  2. 条件公式 (if … then … else)
  3. 合取 (and)
  4. 析取 (or)
  5. 蕴涵 (implies)

例如，A and B implies C or D 等效于 (A and B) implies (C or D)。

类似地，A and not if B then C else D 等效于 A and (not (if B then C else D))。

请注意，上面示例中的 括号不是必需的，因为它们突出了默认优先级。您通常只添加括号来覆盖默认优先级，但您也可以添加它们以使代码更易读（即使它们不是必需的）。

QL 还具有两个表示始终为真的公式的空连接词，any()，以及表示始终为假的公式，none()。

QL 中的逻辑连接词的工作方式类似于其他编程语言中的布尔连接词。以下是一些简要概述

any()

内置谓词 any() 是一个始终成立的公式。

示例

以下谓词定义了所有表达式的集合。

Expr allExpressions() {
  any()
}

none()

内置谓词 none() 是一个永远不成立的公式。

示例

以下谓词定义了空的整数集合。

int emptySet() {
  none()
}

not

您可以在公式之前使用关键字 not。生成的公式称为否定。

not A 正好在 A 不成立时成立。

示例

以下查询选择不是 HTML 文件的文件。

from File f
where not f.getFileType().isHtml()
select f

注意

在递归定义中使用 not 时要小心，因为这会导致非单调递归。有关更多信息，请参阅“非单调递归”。

if ... then ... else

您可以使用这些关键字来编写条件公式。这是简化符号的另一种方法：if A then B else C 与编写 (A and B) or ((not A) and C) 相同。

示例

使用以下定义，visibility(c) 如果 x 是一个公共类，则返回 "public"，否则返回 "private"

string visibility(Class c){
  if c.isPublic()
  then result = "public"
  else result = "private"
}

and

您可以在两个公式之间使用关键字 and。生成的公式称为合取。

A and B 成立，当且仅当 A 和 B 都成立。

示例

以下查询选择具有js扩展名且代码行数少于 200 行的文件。

from File f
where f.getExtension() = "js" and
  f.getNumberOfLinesOfCode() < 200
select f

or

您可以在两个公式之间使用关键字or。得到的公式称为析取式。

A or B成立，如果A或B至少有一个成立。

示例

根据以下定义，如果一个整数等于1、2或3，那么它属于OneTwoThree类。

class OneTwoThree extends int {
  OneTwoThree() {
    this = 1 or this = 2 or this = 3
  }
}

implies

您可以在两个公式之间使用关键字implies。得到的公式称为蕴涵式。这只是一个简化的表示法：A implies B与(not A) or B等价。

示例

以下查询选择任何是奇数或 4 的倍数的SmallInt。

class SmallInt extends int {
  SmallInt() { this = [1 .. 10] }
}

from SmallInt x
where x % 2 = 0 implies x % 4 = 0
select x

脚注

[1]

A != B和not A = B之间的区别在于底层的量词。如果您将A和B视为值集，那么A != B表示

exists( a, b | a in A and b in B | a != b )

另一方面，not A = B表示

not exists( a, b | a in A and b in B | a = b )

这等价于forall( a, b | a in A and b in B | a != b )，这与第一个公式有很大不同。
  • ©GitHub, Inc.
  • 条款
  • 隐私