问题标签 [symbolic-execution]

静态分析的实现和符号执行有什么区别？

符号执行和模型检查（例如在模型转换中）有什么区别？我不明白他们的区别。他们是一样的吗？！

我如何在不使用和例如的情况下实现symbolic executionfor ？我需要有关它的详细信息。例如，我可以通过什么语言来实现这个符号执行以及我需要知道的其他事情？particular languagemodel checkingFinite State Machine (FSM)notJava Path Finder

符号执行的应用是什么？只symbolic execution生成? path condition如何使用符号执行来验证contract？

符号执行的最佳技术是什么？您能帮我找到纯符号执行和纯concolic测试工具（我的意思是，例如它不包括模型检查等）及其来源吗？

我试图了解符号执行引擎的工作原理。本文调查了使用 C 的技术。他们提到了符号记忆：

3.1 全符号记忆

在最高级别的通用性上，引擎可以将内存地址视为完全符号...

以紧凑的形式表示内存。这种方法在 [32] 中采用，它将符号（而不是具体）地址表达式映射到数据，表示使用紧凑、隐式形式的符号地址引用内存所产生的可能替代状态

本文还对 Java 的符号堆进行了一些探讨：

4.1 符号状态表示

符号状态 s 由符号堆 H、原始类型字段的估值、路径条件 PC 和程序计数器组成。

我想知道这在实践中意味着什么，这个符号堆。对我来说，这意味着符号执行中使用的所有数据结构都将使用符号内存而不是实际内存。这意味着像数组这样的结构需要有符号模型。我想知道这些模型是什么样的。我看不到您如何“对数组长度进行符号建模”。在我看来，它是一个整数，所以它将是一个整数值。但作为一个象征性的价值，想知道这意味着什么。我还没有看到。想知道是否可以从高层次上解释如何对一些数据结构（如数组或具有一些不同字段值的结构）进行符号建模，因此它在符号执行中很有用。

这篇较旧的论文提到：

还可以为不需要使用真实数据对象但可以用任意符号表示的编程语言定义另一种“符号执行”语义。

不知道这看起来如何。

I have a static-length list of values ks :: [SInt16] and an index x :: SInt16. I'd like to index into the list using x:

I would expect to be able to use (.!) with a sufficiently constrained x like this:

However, this fails with the error coming from (.!).

Of course, in my real program, I use (.!) all over the place in locations where there is no suitable default value to use in select. How can I index into a list with a constrained-to-be-in-bounds index?

我有一个建模为i -> RWS r w s a. 我想给它一个输入cmds :: [i]；目前我做批发：

我可以尝试搜索预定大小的输入，如下所示：

但是，这给了我在 SBV 本身中的可怕性能，即在调用 Z3 之前（我可以看到情况就是这样，因为verbose输出显示我在调用之前花费的所有时间(check-sat)）。即使inputLength设置为像 4 这样的小值也是如此。

但是，inputLength设置为 1 或 2 时，整个过程非常快速。所以这让我希望有一种方法可以运行 SBV 来获得单步行为的模型i -> s -> (s, a)，然后告诉 SMT 求解器继续针对n不同i的 s 迭代该模型。

所以这是我的问题：在这样的有状态计算中，我想将SMT 变量作为输入提供给有状态计算，有没有办法让 SMT 求解器转动曲柄以避免 SBV 的不良性能？

我想一个简化的“模型问题”是如果我有一个函数f :: St -> St和一个谓词p :: St -> SBool，我想解决n :: SInt这样p (iterateN n f x0)的问题，假设用 SBV 做这件事的推荐方法是什么Mergeable St？

编辑：我已将整个代码上传到 Github，但请记住这不是一个最小化的示例；事实上，它甚至还不是很好的 Haskell 代码。

基于这个非常有用的答案，我重写了我的solver-for-a-stateful-program 以使用Querymonad 和一个不断增加的SMT 变量列表来代表输入。我期望由此产生的两个结果之一：第一部分（生成 SMTLib 输出）被加速并变得可用，或者它仍然很慢以至于它可能无法工作。

但是，相反，我从 SMT 求解器（在我的情况下为 Z3）收到一条错误消息，抱怨 SMTLib 输出中缺少 SMT 变量。看看输出verbose = True，你看，确实有一个变量只被引用，但没有定义：

（ Github 上的完整代码）。我该如何调试？这甚至可能是我程序中的错误，还是 SBV 本身的错误？

编辑：我设法用一个独立的模块重现了这个，除了 MTL/Transformers，当然还有 SBV 本身，没有外部依赖项：

完整的 SMTLib 输出：

错误信息：

我正在寻找一种将 anSInt16变成SString. 对于我的用例，它为具体值做正确的事情就足够了，即我只会查看具体值的SString结果SInt16。

我注意到有一个 的Show实例SInt16，它（当然）返回一个String. 它几乎可以满足我的需求：对于符号值，它返回"<symbolic> :: SInt16"，对于具体值，例如 42，它返回"42 :: SInt16"。所以如果不是那个讨厌的类型标签，我可以literal . show @SInt16用作我的SInt16 -> SString功能。

有没有比编辑的返回值show剪掉类型标签更好的方法？