问题标签 [abstract-interpretation]

我正在学习抽象解释的课程，但我还没有看到任何关于理论如何映射到实际代码的示例。

我正在寻找简短的代码示例，我最好不必使用整个编译器。分析不一定有用，我只想看一个分析得到然后实施的例子。

有谁知道任何这样的例子，也许来自大学课程？

我在一篇关于形式方法的论文中遇到了“必须折叠循环以确保终止”（准确地说是抽象解释）。我很清楚终止的含义，但我不知道折叠循环是什么，也不知道如何在循环上执行折叠。

有人可以向我解释一下折叠环是什么吗？如果它不是隐含在折叠循环的定义中，或者没有立即遵循，这如何确保终止？

谢谢

数据流分析和抽象解释之间有什么区别，它们是否用于相同的目的？这两者相对于彼此有什么优点和缺点。

我需要使用抽象解释来使用 LLVM 进行一些分析。这可能吗？或者我需要更轻松地使用分析工具。如果我可以通过 LLVM 做到这一点，哪些类将帮助我从原始源代码中制定语句以获取变量之间的关系（以及每个变量的可能值范围）

我正在寻找一种在没有用户提示的情况下对循环进行加宽的方法。我会用一个例子来解释：

在此代码上运行 frama-c 值分析时，全局变量z接收区间 [--,--]。因为z被设置为零并且循环由增量运算符组成，所以自动扩大方法应该能够推断出更准确的区间是[0，--]。是否可以在 Frama-C 中执行此操作？

假设我们有以下代码示例：

通过运行 frama-c 值分析工具，我可以推断出 a() 结果的间隔，结果如预期的那样是 [-50, 5100]。我现在要计算的是 a() 的函数摘要，即输入和输出之间的关系。我在上面的例子中寻找的结果看起来像这样：

请注意，我对基于上下文的摘要感兴趣，因此函数 a() 中的其他情况不太感兴趣。

实现这一目标的最佳方法是什么？

这是我的例子：

我想做的是在main中初始化时找到输入变量n的范围，从而达到函数sum。此示例中的正确范围是 [1, 10]。

在示例中，我想将原始输入“保存”在全局值中，并通过将其分配给变量log_global并将其重新引入函数 sum 中，从而发现导致到达函数的原始输入。在这个示例上运行 frama-c 时，我们得到 log_input 的范围是 [5, 14]，而 log_global 的范围是 [-10, 10]。我理解为什么会发生这种情况 - in 的值是在main的开头设置的，并且不受对n的进一步操作的影响。

我想知道在frama-c中是否有一种简单的方法来改变它？也许是对 frama-c 代码的简单修改？

我有一个不相关的想法是在 main 中操纵 if 语句：

我使用了全局变量而不是n。这确实导致了正确的范围，但是这个解决方案不能很好地扩展到更复杂的函数和更深的调用堆栈。

下面，我只考虑纯Prolog 程序。这意味着我不是在谈论离开逻辑领域去做一些在 Prolog 中无法观察到的副作用和操作系统调用。

Prolog 程序的运行时间成本有一个众所周知的抽象度量：逻辑推理的数量。通过“抽象”，我的意思是这个措施独立于任何特定的 Prolog 实现和实际的具体硬件。从某种意义上说，它是一种度量，它为我们提供了一些关于执行程序所需时间的信息。我们甚至可以通过说明 Prolog 系统每秒的推理次数来指定 Prolog 系统的性能 （LIPS），这被广泛使用，以至于人们可以将其称为系统性能的传统衡量标准。传统上，这个数字是通过特定的基准来衡量的，但是“推理次数”的一般概念当然也扩展到其他更复杂的 Prolog 程序。

但是，据我了解，这种特殊的（我敢说：具体的）抽象措施并不能说明以下重要意义的全部真相：

对于任何给定的 Prolog 目标 G，让我们用t (G) 表示：T →R 是 G 在特定硬件上给定 Prolog 系统上的实际执行时间，即从 Herbrand 项到实数的函数。让我们称量度为 α : T →R真实的， 当且仅当 t (G) ≈ α(G) 对于所有 G，在某种意义上，这些值的差异由一个以常数为界的因子对于所有目标 G 和所有“现实”类型的硬件（我必须稍微低估最后一点，但为了简单起见，我在这里假设相同的 Prolog 实现在“典型”硬件上以大致相同的方式执行。我知道这实际上并非如此，并且相同的实现可以在不同类型的硬件上表现出截然不同的特征。如果是这样，请将定义限制为实现“大致”相同的硬件类型的子集。）

据我所知，逻辑推理的数量通常不是 Prolog 目标实际执行时间的真实衡量标准，特别是因为执行统一所需的时间不是由它衡量的。可以构建这种测量与实际执行时间之间的差异不再受常数限制的情况。

因此，我的问题是： Prolog 目标的运行时间是否有真实的抽象度量？如果它一般不存在，请指定一个有意义的 Prolog 程序子集，其中可以定义这样的度量。例如，通过限制可能发生的统一类型。

这个问题具有很高的实际意义，例如在使用 Prolog 实现智能合约时：在这种情况下，您希望抽象地测量运行 Prolog 程序需要多长时间，即使您的程序运行在需要达成一致的不同机器上关于运行它所花费的时间，但您希望保留未来改进具体实现技术的可能性。因此，该措施应该只取决于实际给定的程序，而不是实现的任何具体特征，例如访问的存储单元的数量。

我对 Frama-C 18.0 版（Argon）的行为有点困惑。

给定以下程序：

我希望使用任何跟踪相等性的抽象域都可以很容易地证明该断言。但是，调用

frama-c -eva -eva-equality-domain -eva-polka-equalities foo.c

给出：

我错过了什么吗？

我是JBMC（有界模型检查器）的新手。我们需要找出在不运行Java程序的情况下可能发生在Java程序中的RunTime Exception的可能性。我们搜索了一些抽象解释框架，发现 JBMC 在这种情况下会有所帮助。

例如 ：

在上面的程序中，当循环在第 6 次迭代期间运行时，我们将得到 ArrayIndexOutOfBoundException。但是如何使用 JBMC 来预测呢？我们找到了提供 JBMC 中命令行选项详细信息的命令表，但我们无法找到命令组合以及如何使用它。是否有可用于 JBMC 的 Java API 或文档？

请推荐！！