klee - 可以将函数调用的返回值设为符号以绕过执行该函数吗？

Question

我想避免进行程序间符号执行。也许有一个没有任何约束的返回值，并且可能解析为任何可能的具体值。

这样的事情甚至可能吗？

我想这样做的原因是我想避免执行某些具有非常大循环并且不真正修改全局数据的函数。

Answer 1

如果可以操作源代码，则可以将这些函数调用替换为make_symbolic函数，在该函数中，您基本上创建了一个新的符号变量并将其作为原始函数调用的返回值返回。或者你可以重写这些函数来返回一个新的符号值。

Answer 2

Klee 没有实现这样的功能。如果你想实现它，你必须自己去实现它。

您应该查看的文件是lib/Core/Executor.cpp。Executor 处理作业以象征性地执行指令。您需要更改的特定功能称为“executeCall”。您可以检查函数的名称。如果这与您的目标匹配，只需将程序计数器设置为下一条指令，并将返回值设为符号。

通过一些编程工作，我认为您的需求是可以实现的。