如何强制内存位置在 ACSL 中有效？

Question

我这样定义设备访问

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS;

我已经使用

对访问进行了建模

@ volatile dev->somereg reads somereg_read writes somereg_write;

现在的问题是，当我启用 RTE 检查时，无法证明生成的有效性检查

/*@ assert rte: mem_access: \valid(dev->somereg); */

有什么方法可以注释我的代码，使 MY_DEVICE_ADDRESS 到 MY_DEVICE_ADDRESS+sizeof(struct mydevice) 被认为是有效的？

编辑：这是一个无效的尝试

#include <stdint.h>

#define MY_DEVICE_ADDRESS (0x80000000)

struct mydevice {
  uint32_t somereg;
  uint32_t someotherreg;
};

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS;

/*@ axiomatic Physical_Memory {
     axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS);
  } */

int main(int argc, const char *argv[]) {
  //@ assert \valid(dev);
  //@ assert \false;
  return 0;
}

运行和

frama-c-wp -wp-rte -wp-init-const -wp-model Typed test.c

Answer 1

我不知道（我也尝试了很多）。

我找到的唯一解决方法是：

struct mydevice MY_DEVICE_STRUCT;
volatile struct mydevice * const dev = & MY_DEVICE_STRUCT;

您需要 "instantiate" 内存，因为这是底层 LLVM 所期望的。当然，通过 ACSL 表示法强制执行此操作会很好。

Answer 2

我认为证明断言的唯一方法是放置一个形式为

的公理块

/*@ axiomatic Physical_Memory {
     axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS);
     // add more if you have other physical memory accesses
  } */

内核中有一个选项-absolute-valid-range <min-max>表明在给定的时间间隔内解除对指针的引用是可以的，但只有EVA可以利用它（恐怕这太低了- WP 内存模型的级别）。

另外请注意，您可以将选项 -wp-init-const 传递给 WP，以指示它应该在其上下文中添加全局 const 变量始终等于其初始值的事实。

编辑

如评论中所述，提出的公理确实与WP的内存模型不一致。大部分问题在于，在所述模型中，数字地址 0xnnnn 显然被定义为 shift(global(0),0xnnnn)。正如在例如中所见$FRAMAC_SHARE/wp/ergo/Memory.mlw、global(0) 的 base 为 0，shift 也是如此（仅修改 offset）。 valid_rw 的定义强加了一个严格正的 base，因此矛盾。

这必须在 WP 级别修复。但是，在等待新的 Frama-C 版本时有一些可用的解决方法：

如果不需要写入物理位置，可以将公理中的\valid换成\valid_read。模型中\valid_read的定义没有base>0的要求，因此公理不会自相矛盾。
如果您有能力修改源代码，请将 dev 设为 extern 声明（或将 dev 定义为等于 extern 声明 abstract_dev ), 并在公理中使用抽象常量: 这样就没有了逻辑模型中的等式dev.base==0, 消除了矛盾
最后，您可以在 $FRAMAC_SHARE/wp/ergo/Memory.mlw（以及 $FRAMAC_SHARE/wp/why3/Memory.why 和 $FRAMAC_SHARE/wp/coq/Memory.v 中修补内存模型，具体取决于您选择的证明者）。最简单的方法可能是使 global 依赖于抽象基础，如：

logic global_base: int

function global(b: int) : addr = { base = global_base + b; offset = 0 }

（当然请注意，这个答案绝不能保证这不会在模型中引入其他问题）。

如何强制内存位置在 ACSL 中有效？

How to force a memory location to be valid in ACSL?

frama-c

acsl