如何強制內存位置在ACSL中有效？

我定義設備訪問如從而如何強制內存位置在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

來源

2017-07-20 Yifan

我以某種方式懷疑你描述的問題與你的內存位置的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 }

（當然，需要注意的是這個答案不會以任何方式保證，這不會引入其他問題模型）。

來源

2017-07-21 16:44:44 Virgile

我認爲這是工作，但後來我意識到它使事情不一致。如果我這樣做「// @ 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表示強制這樣做會很好。

來源

2017-07-21 13:56:49 sdive

問題是我需要將設備寄存器映射到特定的物理地址。我想我可以嘗試一些鏈接技巧，看看是否可行。 – Yifan

如何強制內存位置在ACSL中有效？

回答

相關問題