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

问题描述：

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（结构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; 
}

运行与

邮资-C-WP -wp即食-wp-INIT const的-wp模型类型化试验的尝试。 c

我以某种方式怀疑你描述的问题与你的内存位置的volatile性质有关（尽管这确实是其他问题的根源）。从你所描述的，我怀疑'MY_DEVICE_ADDRESS'是一个绝对的物理地址（例如0xdeadbeef）。你可以提供一个MWE，并指明你打算使用哪个插件（再次，我想这是WP，我恐怕无法证明绝对内存地址的任何内容） – Virgile

是的，它是WP和是的它是一个绝对的物理地址。这就是我害怕的，我会看看开发者是否有解决方案。 – Yifan

答

我认为有断言的唯一办法证明是把形式

/*@ 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)具有0一个base，所以具有shift（只修改offset）。 valid_rw的定义强加一个严格正数base，因此是矛盾的。

这必须固定在WP的水平。不过，也有提供一些解决办法，同时等待新的邮资-C版本：

，如果你不需要写物理位置，则可以通过\valid_read在公理代替\valid。模型中\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 }

（当然，需要注意的是这个答案不会以任何方式保证，这不会引入其他问题模型）。

我认为这是工作，但后来我意识到它使事情不一致。如果我这样做“// @ assert \ valid（（struct mydevice *）MY_DEVICE_ADDRESS）;”其次是“// @ assert \ false”，证明经过。 – Yifan

我无法重现此行为。我认为在这一点上你真的必须提供一个MWE来表明这种情况会导致什么。 – Virgile

我只是把它添加到我的主帖。 – Yifan

答

不是我所知道的（我也试过很多）。

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

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

你需要“实例”存储，因为这是底层LLVM所期待的。当然，通过ACSL表示强制这样做会很好。

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

相关推荐