导语:在本文中,我们通过一个有趣的例子来介绍前面知识点的运用,同时,进一步深化了对于逻辑谓词的理解。
代码分析平台CodeQL学习手记(三)
在前面的文章中,我们学习了CodeQL平台中的基本数据类型等概念,不过,这些知识点比较零散,接下来,我们来看看如何将这些知识点串起来解决具体的问题。同时,我们还会顺便深入考察涉及到的逻辑谓词、连接词等知识点。
像处理数据一样处理代码
CodeQL平台一个非常重要的特点,就是可以像处理数据一样处理代码。因此,CodeQL平台的帮助资料中给出了几个有趣的例子,表面上看是用来处理数据的,可实际上同样的方法也可以用来处理代码。好了,下面我们先来看第一个例子。
小偷是谁?
第一个例子是如何通过数据分析找出小偷是谁的故事,期间顺便复习了逻辑谓词、连接词、量词等概念。下面,我们先来介绍一下案情:
有一个世外桃源般的村庄,按方位分为东、西、南、北四部分。有一天,位于村庄中心的神秘城堡发生了失窃案件:王冠被偷了。并且,已知这件事是村子里的人干的,我们的任务就是找出这个人是谁。
个人信息表
既然已经知道小偷肯定是这个村的村民,那么,就很有必要收集全村村民的个人信息,具体内容如下所示:
看到没,这实际上就是建立了一个表,看到表我们很容易就会联想到数据库。大家还记得第三篇的内容吗?在那里,我们也利用源代码建立了数据库——多么熟悉的味道啊!CodeQL的中心思想就是要想处理数据一样处理代码。
我们稍微解读一下这个数据库。首先,每一行就是一条个人记录,记录一个村民的相关信息。那么,都是包含哪些信息呢?这些信息分成多列,每一列代表一个属性,如年龄、身高等,在机器学习上面,又叫做特征。虽然叫法不同,但基本上都是一回事,就是事物某一个方面的信息。
已知的线索
话说回来,要想破案,单靠这些个人信息还是不够的,所以,我们还需要通过走访调查掌握尽可能多的线索。假设我们通过简单问答的形式获得了下列线索:
掌握了村民的个人信息以及小偷的相关线索后,我们就可以着手进行排查了。可问题是,如果村民较多的话,以手工方式进行排查是非常费时费力的,并且容易出错。这时候,QL查询语言就应该闪亮登场了!
首先,请打开一个查询控制台(https://lgtm.com/query),然后,随便选择一种语言和相应的演示项目,具体如下所示:
这时,控制台会自动插入上面红框中的代码,我们直接将其删除即可。
现成的侦查工具箱——QL库
为了帮助我们破案,平台已经定义好了许多QL谓词,以帮助我们从表中提取数据。很好,字面上看平台已经为我们提供了现成的、开箱即用的工具——QL谓词。
那什么是QL谓词呢?QL谓词是一个微型查询,用于表征数据之间的关系,并描述数据的某些属性。为了便于理解,我们不妨用自己的话来解读一下:这里所谓的“查询”,就是用QL语言编写的一个程序、一段代码,或者说是一个函数,专门用来表示数据之间的关系,或描述某些属性。就这里来说,可以将“谓词”看成是用来访问村民个人信息的库函数,例如个人的身高或年龄等。
为了便于使用,平台已经将这些谓词(即库函数)都保存到了一个名为tutorial.qll的QL库中了。当我们需要访问这个库的时候,直接在查询控制台中键入import tutorial语句即可。
导入这个库后,我们就可以直接使用相应的库函数,也就是谓词了——这就省去了每次使用前还得先定义的麻烦。例如,假设我们已经定义了一个表示村民的变量t,那么,直接通过t.getHeight()就可以读取村民的身高了。
这里,我们已经介绍了作为谓词的消费者如何使用它们,那么,我们不妨趁热打铁,进一步了解如何定义谓词。
如何定义谓词
我们知道,谓词是用于描述组成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”)}。因此,这两个谓词的元数分别为1和2。
通常,谓词中的所有元组都具有相同数量的元素。谓词的元数就是各个元组的元素数量,但不包括result变量(请参见带有返回结果的谓词)。
QL查询语言中提供了许多内置的谓词。对于这些内置的谓词来说,我们可以在查询中直接使用,而无需导入任何其他模块。除了使用这些内置谓词之外,我们还可以定义自己的谓词。为此,我们需要给出:
· 关键字predicate(适用于没有返回结果的谓词),或者返回结果的类型(适用于带有返回结果的谓词)。
· 谓词的名称:以小写字母开头的标识符。
· 谓词的参数,如果有的话,需要用逗号进行分隔。对于每个参数来说,需要指定参数类型和参数变量的标识符。
· 谓词主体本身,即用大括号括起来的逻辑公式。
需要注意的是,抽象谓词或外部谓词是没有主体部分的。要定义这样的谓词,需要用分号(;)来结束谓词的定义。
没有返回结果的谓词
定义这种类型的谓词的时候,需要以关键字predicate开头。如果一个值满足谓词主体中的逻辑属性,那么谓词对这个值成立。例如:
predicate isSmall(int i) { i in [1 .. 9] }
如果i是整数,那么当i的取值为小于10的正整数时,isSmall(i)成立。
带有返回结果的谓词
定义这种类型的谓词时,需要用返回结果的数据类型替换关键字predicate。这就引入了一个特殊的变量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”和“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”。
小结
在本文中,我们通过一个有趣的例子来介绍前面知识点的运用,同时,进一步深化了对于逻辑谓词的理解。在后面的文章中,随着对于破案故事的推进,我们将温故知新更多的知识点。
备注:本系列文章乃本人在学习CodeQL平台过程中所做的笔记,希望能够对大家有点滴帮助——若果真如此的话,本人将备感荣幸。
参考资料:
https://help.semmle.com/
转自:https://www.4hou.com/posts/lM9J
转载请注明:jinglingshu的博客 » 代码分析平台CodeQL学习手记(四)