KLEE 使用（三）------ 使用 KLEE 为二分查找生成测试

在上一篇博文中，我们展示了如何用 KLEE 来为一个简单程序生成测试用例。在这篇博文中，我们将展示如何使用 KLEE 中的数组和断言。

0x1 测试无序数组

如下是二分查找的算法实现：

int binary_search(int arr[], int size, int target) {print_data(arr, size, target);int low = 0;int high = size - 1;int mid;while (low <= high) {mid = (low + high)/2;if (arr[mid] == target) {return mid;}if (arr[mid] < target) {low = mid + 1;}if (arr[mid] > target) {high = mid - 1;}}return -1;
}

为了测试这个函数，我们可以创建如下 C 文件（source_to_klee/examples/bin_search0/bin_search0.c）：

#include <klee/klee.h>
#include <stdio.h>
#include <assert.h>void print_data(int arr[], int size, int target) {printf("searching for %d in:\n[", target);for (int i=0; i < size-1; i++) {printf("%d, ", arr[i]);}printf("%d]\n", arr[size-1]);
}int binary_search(int arr[], int size, int target) {print_data(arr, size, target);int low = 0;int high = size - 1;int mid;while (low <= high) {mid = (low + high)/2;if (arr[mid] == target) {return mid;}if (arr[mid] < target) {low = mid + 1;}if (arr[mid] > target) {high = mid - 1;}}return -1;
}int main() {int a[10];int x;klee_make_symbolic(&a, sizeof(a), "a");klee_make_symbolic(&x, sizeof(x), "x");int result = binary_search(a, 10, x);printf("result = %d\n", result);// check correctnessif (result != -1) {assert(a[result] == x);} else {// if result == -1, then we didn't find it. Therefore, it shouldn't be in the arrayfor (int i = 0; i < 10; i++) {assert(a[i] != x);}}return 1;
}

在上述代码中，我们声明一个包含 10 个元素的符号数组 ‘a’ ，一个代表查找目标值的符号化整数变量，然后调用二分查找函数。如果结果不等于 -1，则代表找到目标值，所以数组对应位置上的值应该等于我们查找的目标值，否则没有任何元素应该等于查找的目标值。

接下来，运行如下命令行命令来运行 KLEE 进行分析。
clang-9 -I source_to_klee/include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone bin_search0.c
klee --external-calls=all bin_search0.bc

获取到如下输出：

输出中有一行红色的信息表明是断言错误。

通过如下命令来找到导致断言错误的输入：

clang-9 -I source_to_klee/include -L source_to_klee/cmake-build-debug/lib bin_search0.c -lkleeRuntest
export LD_LIBRARY_PATH=source_to_klee/cmake-build-debug/lib/:$LD_LIBRARY_PATH
ls -1 klee-last/*.ktest | awk '{printf("echo \"----------------\"\n echo %s\n KTEST_FILE=%s ./a.out\n", $0, $0)}' | sh

可以看到在如下的输出中，第八个测试用例导致了断言错误。

在 test000008.ktest 中，我们试图在数组中寻找已存在的元素 1，但是却显示数组中不存在元素 1。这是为什么呢？？原因就是这个数组是无序的！！！

0x2 测试有序数组

我们希望 KLEE 在测试前，数组已经是有序的。而幸运的是，KLEE 恰好给我们提供了一个 intrinsic 函数 klee_assume 来限定数组有序。以下是新版的二分查找代码（source_to_klee/examples/bin_search1/bin_search1.c）：

#include <klee/klee.h>
#include <stdio.h>
#include <assert.h>void print_data(int arr[], int size, int target) {printf("searching for %d in:\n[", target);for (int i=0; i < size-1; i++) {printf("%d, ", arr[i]);}printf("%d]\n", arr[size-1]);
}int binary_search(int arr[], int size, int target) {print_data(arr, size, target);int low = 0;int high = size - 1;int mid;while (low <= high) {mid = (low + high)/2;if (arr[mid] == target) {return mid;}if (arr[mid] < target) {low = mid + 1;}if (arr[mid] > target) {high = mid - 1;}}return -1;
}int sorted(int arr[], int size) {for (int i = 0; i < size-1; i++) {if (arr[i] > arr[i+1]) {return 0;}}return 1;
}int main() {unsigned short n;klee_make_symbolic(&n, sizeof(n), "n");klee_assume(n > 0);klee_assume(n < 65535);int a[n];int x;klee_make_symbolic(&a, sizeof(a), "a");klee_assume(sorted(a, 10));klee_make_symbolic(&x, sizeof(x), "x");int result = binary_search(a, 10, x);printf("result = %d\n", result);if (result != -1) {assert(a[result] == x);} else {// if result == -1, then we didn't find it. Therefore, it shouldn't be in the arrayfor (int i = 0; i < 10; i++) {assert(a[i] != x);}}return 1;
}

第 50 行表示 KLEE 应该假设数组已经排序，第 33 到 40 行实现了检查。但是，我们得到以下输出：

如果我们像之前一样运行测试，我们会看到断言始终保持不变，并且测试输入数组确实是排序的。

然而，如果你想确保 KLEE 不输出这种错误，你可以将 sort 函数转换成总是在结束的时候退出；同时要避免布尔逻辑，这反过来可能导致不同的编译器使用简短逻辑和输出不同的结果。

如下是我们新版的代码文件（source_to_klee/examples/bin_search/bin_search.c）：

#include <klee/klee.h>
#include <stdio.h>
#include <assert.h>void print_data(int arr[], int size, int target) {printf("searching for %d in:\n[", target);for (int i=0; i < size-1; i++) {printf("%d, ", arr[i]);}printf("%d]\n", arr[size-1]);
}int binary_search(int arr[], int size, int target) {print_data(arr, size, target);int low = 0;int high = size - 1;int mid;while (low <= high) {mid = (low + high)/2;if (arr[mid] == target) {return mid;}if (arr[mid] < target) {low = mid + 1;}if (arr[mid] > target) {high = mid - 1;}}return -1;
}int sorted(int arr[], int size) {int found_error = 0;for (int i = 0; i < size-1; i++) {found_error = found_error | (arr[i] > arr[i+1]);}return !found_error;
}int main() {int a[10];int x;klee_make_symbolic(&a, sizeof(a), "a");klee_assume(sorted(a, 10));klee_make_symbolic(&x, sizeof(x), "x");int result = binary_search(a, 10, x);printf("result = %d\n", result);if (result != -1) {assert(a[result] == x);} else {// if result == -1, then we didn't find it. Therefore, it shouldn't be in the arrayfor (int i = 0; i < 10; i++) {assert(a[i] != x);}}  return 1;
}

运行结果没有任何问题！

特别地，在每一个可能找到元素的位置都生成了测试用例：

ls -1 klee-last/*.ktest | awk '{printf("KTEST_FILE=%s ./a.out\n", $0)}' | sh  | grep result | sort

通过这种方法，我们成功地检查了二分查找（对于 10 个元素的数组）的正确性。

更有趣的事是，您可以尝试插入错误或更改代码。

例如，如果在 while 循环中我们用 < 更改 <= ，会发生什么?

while (low <= high)