5.3.2 字符串约束描述语言
本书利用数组模型对字符串进行建模和求解,首要任务是将源程序中的字符串约束转换为数组模型表示的约束。本节对于大部分字符串函数的语义进行了分析,然后定义了一种描述语言对字符串函数的约束进行描述。
1.字符串操作语言L Str
首先我们引入字符串操作语言L Str来描述包含字符串函数的原始程序约束,L Str是一个包含如下元素的多类型一阶逻辑语言[25]。
①集合:A表示有限数量的字符表。字符串集合S是A的幂集。I和B分别表示整数集合以及布尔值集合,每一个集合都包含有限个变元,以小写字母来表示。
②常量:L Str中的常量包括所有的整数以及所有的字符串常量。
③谓词:包括整数集上的谓词,以及字符串函数中查询字符串的属性并返回布尔值B的部分。
④函数:包括整数集上的运算,以及字符串函数中查询或者修改字符串并返回整数值I或者字符串S的部分。
所有的字符串函数都可归类为L Str中的谓词或者函数,因此包含字符串函数的约束可以通过语言L Str中的公式来表示。
2.原子字符串语言L Atom
我们定义了原子字符串语言L Atom,其中包含描述不同操作范围的原子函数,其数量远少于L Atom的非逻辑符号,利用原子函数的组合描述L Atom中的字符串函数的语义。L Atom中的集合与常量L Atom一致,区别在于包含如下的谓词和函数。
①谓词:包括整数集上的谓词,不包括字符串函数。
②函数:L Atom包括表示字符串长度的函数L(s),以及3个原子函数,原子函数表示了不同操作范围的字符数组成员。
·Char At(s,i):表示在字符串S中位置为i的字符成员,其中s∈S,表示被操作的字符串,i∈I,表示位置变量,简写为S[i]。
·Char At(s,
,i):表示在字符串S中位置从i ~到i的一系列字符成员,其中i ~,i∈
表示位置之间的最小间隔;Γ表示非法位置。Char At(s,N)被简写为s(N)。
L Atom中的公式根据以下规则递归生成。(https://www.daowen.com)
①所有的变量和常量都是项。
②令f为L Atom中的函数符号,t 1,…,tn是L Atom中的项,则f(t 1,…,tn)也是L Atom的项。
③令F为L Atom中的谓词符号,t 1,…,t n是L Atom中的项,则F(t 1,…,t n)是L Atom的公式。
④公式之间利用、∧、∨等逻辑运算符连接起来得到的表达式也是公式。
L Str与文献[24]中定义的核心字符串语言C L类似,但是L Atom比C L包含更多的函数,因此L Atom能够表示更广泛的操作范围。L Atom作为L Str到数组类型的约束的中间语言,不仅能够表示L Str的约束,还能够被约束求解器求解。下一节介绍从L Str到L Atom的转换过程。
3.L Str到L Atom转换
本节以表5-6中的3种类型的代表性函数为例,介绍字符串函数的语义以及转换为L Atom的公式表示的过程。
从覆盖测试的角度考虑,所生成的字符串测试用例应当尽可能触发字符串函数的合理功能,避免一些意外行为,如空字符串触发异常处理等,因此本书将字符串函数的语义分为两部分:有效条件和语义定义。有效条件限制了函数的输入必须在合法的范围内,不会导致程序崩溃或者不确定的结果,是转换的前提条件;语义定义是函数在合法范围内的操作语义,在利用原子函数表示语义定义的过程中,会引入表示下标的辅助变量,在约束求解过程中需要为所有的下标变量给出合法且确定的取值。一些查询功能的函数(如strhr和strcmp)的语义定义与返回值的取值相关,需要分情况讨论。具体的转换规则如表5-6所示。
表5-6 L Str到L Atom转换
其中C是一个字符常量,语义定义中以逗号表示公式之间的合取。这里对语义定义进行解释。
①j=strchr(s,c):函数的功能是查询字符c在s中出现的位置,当返回值在0＜j＜s 之间时,表示在s中的位置j处存在字符c,并且在位置[0,j-1]处没有字符c。
②j=strcmp(s 1,s 2):函数的功能是比较s 1和s 2的每一个字符。非零的返回值意味着至少在位置i处有s 1[i]≠s 2[i]。返回值为零表示s 1和s 2不仅具有相同的长度,并且每一个字符都相同。
③s 4=strrpl(s 1,s 2,s 3):函数的功能是把s 1中所有的s 2替换为s 3。这里将有效条件限制为s 2和s 3必须具有相同的长度,此时的语义定义由以下部分组成。
·Γ:{I}是一个非法位置集合,表示了N中元素所不能取的值,例如,当s 2是确定的字符串“qwer”并且s1[2]是字符‘b’,则s 2在s1中的开始位置不能是{0,1,2}。
原子函数的组合提供了准确描述各种字符串库函数的能力,表5-6中同类型的其他字符串函数也能以类似方式进行组合表示。转换之后的表达式是有量词的谓词表达式,因此需要在求解的过程中在边界确定之后将量词消除。
