0

我这样定义设备访问

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 类型化 test.c

4

2 回答 2

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). 正如在 eg 中可以看到的$FRAMAC_SHARE/wp/ergo/Memory.mlw，global(0)有一个baseof 0，所以有 the 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依赖抽象基础，例如：
逻辑 global_base: int

函数 global(b: int) : addr = { base = global_base + b; 偏移量 = 0 }

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

于 2017-07-21T16:44:44.430 回答
0

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

我发现的唯一解决方法是：

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

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

于 2017-07-21T13:56:49.707 回答