c++ - 为程序中所有可能路径的运行生成数据

Question

我是 Z3 的新手，并在此处和 Google 上搜索了我的问题的答案。我没有成功。

这是产生问题的代码：

void test(string str) {
    if (str [0] == 'g') {
        cout << "\"The first letter g" case"<< endl;
        if (str [1] == 'a') cout << "Second letter is 'a'";
        else cout << "Second letter is not 'a'";
    } else {
        cout << "The non-g case" << endl;
        if (str [1] == 'b') cout << "Second letter is 'b'";
        else cout << "Second letter is not 'b'";
    }
}

我需要自动生成输入数据，以便代码一直运行。z3有可能做到这一点吗？如果是这样，我该如何使用 z3 C/C++API 做到这一点？

Answer 1

Z3不是测试用例生成器或模糊器，它是定理证明器。但是，Z3 用于实现模糊器和测试用例生成器。其中之一是Pex，一种用于 .NET 的白盒单元测试。Z3 还用于Sage中，这是一个用于 x86 二进制文件的白盒模糊器。不幸的是，我不知道有任何基于 Z3 的 C++ 测试用例生成器。

Answer 2

不直接回答您的问题，但之前已使用 SAT/SMT 求解器来生成此类“利用”向量，并取得了相当大的成功。例如，查看 Brumley 的 AEG 系统：http : //security.ece.cmu.edu/aeg/index.html 等。