首页 > 其他分享> > QL语言参考-1谓词

QL语言参考-1谓词

2022-04-25 16:01:18 作者：互联网

关键词

关于 QL 语言：QL 是 CodeQL 的强大查询语言，用于分析代码。
谓词：谓词用于描述构成 QL 程序的逻辑关系。
查询：查询是 QL 程序的输出。他们评估结果集。
类型：QL 是一种静态类型语言，因此每个变量都必须有一个声明的类型。
模块：模块提供了一种通过将相关类型、谓词和其他模块组合在一起来组织 QL 代码的方法。
别名：别名是现有 QL 实体的替代名称。
变量：QL 中的变量与代数或逻辑中的变量的使用方式类似。它们代表一组值，这些值通常受公式限制。
表达式：表达式计算为一组值并具有类型。
公式：公式定义了表达式中使用的自由变量之间的逻辑关系。
注释：注释是一个字符串，您可以将其直接放在 QL 实体或名称的声明之前。
递归：QL 为递归提供了强大的支持。如果 QL 中的谓词直接或间接依赖于自身，则称其为递归谓词。
词法语法：QL 语法包括不同种类的关键字、标识符和注释。
名称解析：QL 编译器将名称解析为程序元素。
QL方案的评价：甲QL程序是在许多不同的步骤进行评价。
QL 语言规范： QL 语言的正式规范。它提供了有关 QL 的术语、语法和其他技术细节的全面参考。

谓词Predicates

官方文档

https://codeql.github.com/docs/ql-language-reference/predicates/

QL中的谓词用来声明逻辑关系。感觉谓词跟"函数"概念非常相似。

predicate isCountry(string country) {
  country = "Germany"
  or
  country = "Belgium"
  or
  country = "France"
}

predicate hasCapital(string country, string capital) {
  country = "Belgium" and capital = "Brussels"
  or
  country = "Germany" and capital = "Berlin"
  or
  country = "France" and capital = "Paris"
}

谓词 isCountry 是一个元组{(“ Belgium”) ，(“ Germany”) ，(“ France”)}的集合，而 hasCapital 是两个元组{(“ Belgium”，“ Brussels”) ，(“ Germany”，“ Berlin”) ，(“ France”，“ Paris”)}的集合。这些谓词的作用分别是一个和两个。

一般来说，谓词中的所有元组具有相同数目的元素。谓词的作用是指元素的数量，不包括可能的结果变量。有关更多信息，请参见“带结果的谓词”QL 中有许多内置谓词。您可以在任何查询中使用它们，而无需导入任何其他模块。除了这些内置谓词，您还可以定义自己的谓词:

定义谓词

在定义谓词时，应该指定:

关键字谓词(对于没有结果的谓词) ，或者结果的类型(对于带结果的谓词)。
谓词的名称。这是一个以小写字母开头的标识符。
谓词的参数(如果有的话)用逗号分隔。对于每个参数，为参数变量指定参数类型和标识符。
谓词体本身。这是一个用大括号括起来的逻辑公式。

注意: 抽象或外部谓词没有主体。要定义这样一个谓词，请用分号(;)结束谓词定义。

定义没有结果的谓词

这些谓词定义以关键字谓词开始。如果值满足主体中的逻辑属性，则谓词保留该值。

predicate isSmall(int i) {
  i in [1 .. 9]
}

如果 i 是一个整数，那么如果 i 是一个小于10的正整数，那么 isSmall (i)就成立。

定义带结果的谓词

通过将关键字谓词替换为结果的类型，可以使用 result 定义谓词。这就引入了特殊的变量结果。

int getSuccessor(int i) {
  result = i + 1 and
  i in [1 .. 9]
}

如果 i 是小于10的正整数，则谓词的结果是 i 的后继者。

请注意，您可以以与谓词的其他参数相同的方式使用 result。你可以用任何你喜欢的方式来表达结果和其他变量之间的关系。例如，给定一个返回 x 的父元素的谓词 getAParentOf (Person x) ，你可以定义一个如下的“反向”谓词:

Person getAChildOf(Person p) {
  p = getAParentOf(result)
}

一个谓词也可以对其参数的每个值有多个结果(或者根本没有结果)。例如:

string getANeighbor(string country) {
  country = "France" and result = "Belgium"
  or
  country = "France" and result = "Germany"
  or
  country = "Germany" and result = "Austria"
  or
  country = "Germany" and result = "Belgium"
}

在这种情况下:

谓词调用getANeighbor("Germany")，返回两个结果:"Austria" and 及"Belgium"。
谓词调用getANeighbor("Belgium") ，没有结果，因为getANeighbor，并没有定义"Belgium"的返回值。

递归谓词

QL 中的谓词可以是递归的，这意味着它直接或间接地依赖于自身。

例如，您可以使用递归来精炼上面的示例。

就目前情况而言，getANeighbor 中定义的关系是不对称的ーー它没有抓住这样一个事实，即如果 x 是 y 的邻居，那么 y 就是 x 的邻居。一个简单的方法就是递归调用这个谓词，如下所示:

string getANeighbor(string country) {
  country = "France" and result = "Belgium"
  or
  country = "France" and result = "Germany"
  or
  country = "Germany" and result = "Austria"
  or
  country = "Germany" and result = "Belgium"
  or
  country = getANeighbor(result)
}

现在，getANeighbor (“Belgium”)的结果为France和Germany。

有关递归谓词和查询的更一般性讨论，请参阅“递归”。

各种谓词

谓词有三种，即非成员谓词、成员谓词和特征谓词。

非成员谓词在类之外定义，也就是说，它们不是任何类的成员。

有关其他类型谓词的详细信息，请参阅“ Classes”主题中的特征谓词和成员谓词。

下面的例子展示了每种类型的谓词:

int getSuccessor(int i) {  // 1. Non-member predicate 非成员谓词
  result = i + 1 and
  i in [1 .. 9]
}

class FavoriteNumbers extends int {
  FavoriteNumbers() {  // 2. Characteristic predicate 特征谓词 类似构造函数
    this = 1 or
    this = 4 or
    this = 9
  }

  string getName() {   // 3. Member predicate for the class `FavoriteNumbers` 成员谓词 类似成员函数
    this = 1 and result = "one"
    or
    this = 4 and result = "four"
    or
    this = 9 and result = "nine"
  }
}

绑定行为

必须能够在有限的时间内计算谓词，因此它所描述的集合通常不允许是无限的。换句话说，一个谓词只能包含有限数量的元组。

QL 编译器报告了一个错误，当它能够证明谓词包含的变量没有被约束到有限数量的值。有关更多信息，请参见“绑定” 。

下面是一些无限谓词的例子:

/*
  Compilation errors:
  ERROR: "i" is not bound to a value.
  ERROR: "result" is not bound to a value.
  ERROR: expression "i * 4" is not bound to a value.
*/
int multiplyBy4(int i) {
  result = i * 4
}

/*
  Compilation errors:
  ERROR: "str" is not bound to a value.
  ERROR: expression "str.length()" is not bound to a value.
*/
predicate shortString(string str) {
  str.length() < 10
}

在 multilyby4中，参数 i 被声明为 int，这是一个无限类型。它被用在不绑定操作数的二元运算 * 中。Result 从一开始就是不绑定的，并且最终经过计算复制后仍然是不绑定的，因为它用于与 i * 4一起进行的相等性检查，而 i * 4也是不绑定的。

在 shortString 中，str 保持未绑定状态，因为它是用无限类型字符串声明的，并且内置函数 length ()不绑定它。

装订集

有时您可能无论如何都想定义一个“无限谓词”，因为您只打算在一组受限制的参数上使用它。在这种情况下，可以使用 bindingset 注释指定显式绑定集。此注释对于任何类型的谓词都有效。

bindingset[i]
int multiplyBy4(int i) {
  result = i * 4
}

from int i
where i in [1 .. 10]
select multiplyBy4(i)

虽然 multiplyby4是一个无限谓词，但是上面的 QL 查询是合法的。它首先使用 bindingset 注释声明谓词 multimyby4将是有限的，只要 i 绑定到有限数目的值。然后在 i 被限制为范围[1-10]中使用谓词。

也可以为一个谓词指定多个绑定集。这可以通过添加多个绑定集注释来实现，例如:

bindingset[x] bindingset[y]
predicate plusOne(int x, int y) {
  x + 1 = y
}

from int x, int y
where y = 42 and plusOne(x, y)
select x, y

以这种方式指定的多个绑定集彼此独立。以上示例表示：

如果x 是绑定的（有限的）, 那么x和y都是有限的。
如果y 是绑定的（有限的）, 那么x和y都是有限的。

也就是说 bindingset[x] bindingset[y]是x或者y其中一个必须被绑定，不同于bindingset[x, y]，x与y都必须被绑定。

当您希望声明一个带有接受多个输入参数的结果的谓词时，后者可能很有用。例如，下面的谓词接受一个字符串 str 并将其截断为 len 字符的最大长度:

bindingset[str, len]
string truncate(string str, int len) {
  if str.length() > len
  then result = str.prefix(len)
  else result = str
}

然后你可以在一个 select 子句中使用它，例如:

select truncate("hello world", 5)

数据库谓词

您查询的每个数据库都包含表示值之间关系的表。这些表(“数据库谓词”)的处理方式与 QL 中的其他谓词相同。

例如，如果一个数据库包含一个用于 person 的表，您可以编写 persons (x，firstName，_，age)来约束 x，firstName 和 age 成为该表中第一、第二和第四列的行。

唯一的区别是您不能在 QL 中定义数据库谓词。它们是由底层数据库定义的。因此，可用的数据库谓词根据要查询的数据库而有所不同。

标签：参考,int,country,绑定,result,谓词,QL
来源： https://www.cnblogs.com/macter/p/16190590.html