frama-c - Frama-c 执行时间和堆内存边界证明

Question

Frama-C 是否提供任何工具来证明函数的运行时特性，例如执行时间（可能作为指令计数）和堆内存空间（作为分配的字节计数）？

标签： frama-c

Answer 1

关于执行时间估计

Frama-C 在 C 级别工作。Metrics 插件可以在非常接近原始版本 ( -metrics -metrics-ast cabs) 的源版本或它使用的规范化源（通常称为Cil 代码）上提供一些指标（例如语句计数）。但是，它没有任何汇编代码知识，因此无法提供有关此级别执行时间的精确信息。

由于编译器优化会影响代码生成，Frama-C 给出的数字可能接近也可能不接近编译器生成的数字，这取决于启用了哪些优化、对编译器和目标体系结构的了解等。一般情况下，Frama-C不能给予任何保证；在特定情况下，可以开发插件来提供一些这样的信息（例如Cost插件，这里提到的使用注解来尝试保持源代码和编译代码之间的一些对应关系，然后使用它们来提供一些执行时间信息）。

关于内存大小估计

有一个选项，-metrics-locals-size它可以粗略估计函数的堆栈内存使用情况。与前一种情况一样，这只是基于源代码的估计。编译器可能会为计算临时子表达式或寄存器溢出而堆栈分配临时变量，因此 Frama-C 给出的数字不能用于最坏情况的堆栈估计。

ACSL 支持动态内存分配，因此理论上可以编写有关它的注释。然而，当前的插件并没有提供一种直接的方式来精确地处理这个问题。它可能需要为 Eva 编写一个新插件，或者至少是一个抽象域。

Eva 目前处理动态分配，但可能还不够精确，无法以有趣的方式估计堆大小。可以为 Eva 开发一个抽象域来跟踪此信息（添加mallocs 和减去frees）并计算堆内存空间的过度逼近，但这需要能够限制包含分配的循环的迭代次数（否则上限将是无限的）。精度将取决于程序的复杂性。

对于运行时验证，E-ACSL 插件已经跟踪了一些堆栈/堆信息的使用情况（即使它当前没有导出给用户），所以理论上可以编写一个类似于 的断言//@ assert heap_size <= \old(heap_size) + 42;，并在运行时检查它，运行检测程序时。