嵌入式方向实践实验二

发表于 2024-12-15 分类于嵌入式方向阅读次数： Waline：本文字数： 3.3k 阅读时长 ≈ 6 分钟

实践二_通过约束生成测试用例输入实验报告

实验任务

本次实践的主要任务是将实践一转换得到的 CPP 代码通过约束求解得到的约束，借助大语言模型得到相应约束的测试用例输入，一是进一步评估大语言模型对于抽象表示的识别能力，二是探索生成测试用例输入的新方法，在下述样例中会详细阐述。在上交实践一成果后，助教会生成好对应代码的约束，分发给各位同学作为实践二的原始材料，不需要大家去仔细学习约束求解的过程，大概了解约束是怎样的东西即可，想了解的同学也可以查看附录内容自行探索。

举例：

以下仍旧以 008_sum_product.cpp 举例（下简称 008 ），我们聚焦于主函数（有略微改动，会解释原因）：

// other codes ...
 int main() {
 std::vector<int> numbers = {};
 std::tuple<int, int> result = sum_product(numbers);
 int sum = std::get<0>(result);
 int product = std::get<1>(result);
 return 0;
 }

在主函数中主要是对功能函数 sum_product() 的调用与测试，我们的约束则会聚焦于功能函数的入参，即 numbers 。（相较于实践一说明中的代码，这里将入参变为变量，方便后续操作） numbers 的类型为素 el vector ，对于该容器来说，约束求解会聚焦于其长度 ements 。在 size 以及其中的元 008 样例中，容器元素的变化并不会对约束产生影响（对于其他的代码，可能会产生影响），所以 008 样例求解生成的约束主要针对 size 。简单理解为，在 008 程序中，当 size 有不同的取值，程序就会运行不同的分支。抽象表示取值范围，就是所谓的约束。

此处仅为举例，在其他程序中，约束可能会同时针对多个变量，如 vector<> 的长度与元素都会有约束。

为了约束不那么冗长，助教在生成约束前会将类似 size 的变量限定在一个较小的范围内，如 [0,3) 。以下是 008 样例根据约束求解的要求更改后的代码：（这一步不需要大家完成，由助教来做，此处仅为示意，以解释约束是怎么得来的，是长什么样的）

// other codes ...
 int main() {
 std::vector<int> numbers = {};
 int size;
 klee_make_symbolic(&size, sizeof(size), "size"); // 这是约束求解用到的符号生成函
数
}
 // 约束求解时会使 size 变为不同的值，所以此处没有初始化
int elements[3] = {1, 2, 3}; // 该程序中元素不进入约束表达式
// 对于其他程序，也会为每个元素生成符号，加入约束求解中
if (size >= 0) {
 // 限定 numbers 的实际 size 在 [0,3) 范围内
for (int i = 0; i < size && i < 3; i++) {
 numbers.push_back(elements[i]);
 }
 }
 std::tuple<int, int> result = sum_product(numbers);
 // 由于只需要约束求解，所以不需要运行后续测试
return 0;
}

以下即为上述更改后的 008 样例求解得到的约束：

Constraints 1:
 (Eq false
 (Sle 0
 (ReadLSB w32 0 size)))----------------
 Constraints 2:
 (Sle 0
 (ReadLSB w32 0 size))
 (Eq false
 (Slt 0
 (ReadLSB w32 0 size)))----------------
 Constraints 3:
 (Sle 0
 (ReadLSB w32 0 size))
 (Slt 0
 (ReadLSB w32 0 size))
 (Eq false
 (Slt 1
 (ReadLSB w32 0 size)))----------------
 Constraints 4:
 (Sle 0
 (ReadLSB w32 0 size))
 (Slt 0
(ReadLSB w32 0 size))
 (Slt 1
 (ReadLSB w32 0 size))
 (Eq false
 (Slt 2
 (ReadLSB w32 0 size)))----------------
 Constraints 5:
 (Sle 0
 (ReadLSB w32 0 size))
 (Slt 0
 (ReadLSB w32 0 size))
 (Slt 1
 (ReadLSB w32 0 size))
 (Slt 2
 (ReadLSB w32 0 size))----------------

由于 008 代码十分简单，所以这些约束也相对规整。因为在 size 取不同的值时，程序都会运行到不同的分支（最终影响就是 numbers 的不同，即功能函数运行的分支不同），所以上述约束看起来就是枚举 size 的不同取值，用合取范式表示。解释一下，约束一表示的意思是 (0 <= size) == false，约束二表示的意思是 0 <= size && ((0 < size) == false)，以此类推。这样的约束文本就是大家在上交实践一成果后会得到的实践二原材料。请大家设计相应的提示语（prompt），让大语言模型理解这样的约束，并生成相应的测试用例输入。

注意，如 008 样例，约束中仅含有 size 变量，所以大语言模型可能只会生成不同的变量作为测试用例输入，但其实 008 需要的测试用例输入是一个 size vector 类型的变量，不止是它的 size ，所以请大家自行想办法生成合法的测试用例输入（即完整的 numbers ），例如使用随机数去填充容器，让大语言模型额外生成容器的元素等等。

实验报告

使用的大模型为chatgpt3.5；

设计的prompt为两部分，第一部分为给大模型一个例子用以理解和作为语境：

我们可以根据约束生成测试用例，以下是一个约束的例子：
Constraints:
(Sle 0
      (ReadLSB w32 0 size))
(Slt 0
      (ReadLSB w32 0 size))
(Eq false
     (Sle 0
          (ReadLSB w32 0 x0)))
(Eq false
     (Slt 1
          (ReadLSB w32 0 size)))
这些的含义是：
size >=0
size > 0
x0 > 0  为 false
size > 1 为 false
根据这几个条件可知，size 只能为1，x0为0或者负数，按照此随机生成一个测试用例为：size = 1，array = [0]
你现在理解约束的含义了吗

第二部分则把约束给大模型，让大模型根据约束生成测试用例，例如：

现在请理解以下约束的含义，并为此随机生成一个测试用例：
Constraints:
(Sle 0
      (ReadLSB w32 0 size))
(Slt 0
      (ReadLSB w32 0 size))
(Sle 0
      (ReadLSB w32 0 x0))
(Sle (ReadLSB w32 0 x0)
      3)
(Eq false
     (Slt 1
          (ReadLSB w32 0 size)))
(Eq false
     (Eq 1
         (SRem w32 (ReadLSB w32 0 x0)
                   2)))