标签: abstract-interpretation

数据流分析和抽象解释之间有什么区别,它们是否用于相同的目的？这两者相对于彼此的利弊是什么.

在下面,我只考虑纯 Prolog程序.这意味着我不是在谈论副作用和操作系统调用,它们会让逻辑领域做一些无法在Prolog中观察到的事情.

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

但是,据我所知,这个特殊的(我敢说:具体的)抽象测量并不能说明以下重要意义上的全部真相:

对于任何给定的Prolog目标G,让我们用t(G)表示:T →R在特定硬件上给定Prolog系统上G的实际执行时间,即从Herbrand项到实数的函数.让我们称一个度量α:T →R 真实 iff t(G)≈对于所有G的α(G),在这个意义上,这个值相差一个因子,该因子受所有目标G和所有"现实" 的常数限制硬件的类型(我必须稍微说明这一点,但为了简单起见,我在这里假设相同的Prolog实现在"典型"硬件上大致以相同的方式执行.我知道事实并非如此,并且相同实现可以在不同类型的硬件上表现出截然不同的特性.如果是这样,将定义限制为实现"大致"相同的硬件类型的子集.)

据我所知,逻辑推理的数量通常不是 Prolog目标的实际执行时间的真实度量,特别是因为执行统一所花费的时间不是由它来衡量的.可以构造这样的情况,即该度量与实际执行时间之间的差异不再受常数限制.

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

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

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

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

有没有人知道任何这样的例子,也许是从大学课程？

这是我的例子:

int in;
int sum(int n){
    int log_input = n;
    int log_global = in;
    return 0;
}

int main(){
    int n = Frama_C_interval(-10, 10);
    in = n;
    if (n > 0){
        sum(n + 4);
    }
    return 0;
}

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

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

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

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

if (in > 0){
    sum(in + 4);
}

我使用全局变量而不是n.这确实产生了正确的范围,但是这种解决方案不能很好地扩展到更复杂的功能和更深的调用堆栈.

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

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

鉴于以下程序：

#include <assert.h>
#include <limits.h>


/*@ requires order: min <= max;
    assigns \result \from min, max;
    ensures result_bounded: min <= \result <= max ;
 */
extern int Frama_C_interval(int min, int max);


int main() {

  int i,j;

  i = Frama_C_interval(INT_MIN, INT_MAX);

  j = i;

  assert(j == i);

  return 0;
}

我希望可以很容易地用任何跟踪平等的抽象域来证明这个断言。但是，调用

框架-c -eva -eva-equality-domain -eva-polka-equalities foo.c

给出：

[eva] Warning: The Apron domains binding is experimental.
[kernel] Parsing stupid_test.c (with preprocessing)
[eva] Analyzing a complete application starting at …