我想用Frama-c和WP插件表示，下面编写的stringCompare函数充当“应该” —即：给定相同的输入字符串，该函数返回0且结果不同于0如果字符串不相同。我已经注释了如下所示的相关功能，并希望能够证明WP产生的未经验证的目标，该怎么做？
我从尝试按原样运行带有注释的插件得到的输出可以在代码下面看到
#include <string.h>
#include <stdio.h>
/*@
requires validPointers: \valid_read(s1) && \valid_read(s2) ;
requires validLengthS1: 100 >= strlen(s1) >= 0;
requires validLengthS2: 100 >= strlen(s2) >= 0;
assigns \nothing ;
allocates \nothing ;
frees \nothing ;
behavior allEqual:
assumes \forall integer k; 0 <= k < n ==> s1[k] == s2[k];
ensures \result == 0;
behavior SomeDifferent:
assumes \exists integer k; 0 <= k < n ==> s1[k] != s2[k];
ensures \result != 0;
disjoint behaviors;
complete behaviors;
*/
int stringCompare(const char* s1, const char* s2, int n) {
if (s1 == s2)
return 0;
int i = 0;
/*@ assert \valid_read(s1) ; */
/*@ assert \valid_read(s2) ;*/
/*@ loop invariant 0 <= i;
loop assigns i , s1, s2; */
while (*s1 == *(s2++))
{
/*@ assert i <= 2147483647 ; */
++i;
if (*(s1++) == '\0')
return 0;
}
return *(unsigned char*)s1 - *(unsigned char*)(--s2);
}
/*@ assigns \nothing ;
ensures rightResult: \result == strlen(\old(str));
ensures rightEndCharacter: str[\result] == '\0' ; */
int stringLength(const char* str) {
int result = 0;
/*@ loop assigns result ;
loop invariant 0 <= result ; */
while (str[result++] != '\0');
return --result;
}
/*@ assigns \nothing ;
ensures \result == 0 ;*/
int main(void) {
const char* hello = "hello";
const char* helli = "helli";
/*@ assert \valid_read(hello) && \valid_read(helli) ; */
stringCompare(hello, helli, 5);
return 0;
}
WP正在使用以下命令运行：'frama-c -wp -wp-model“ Typed + var + int + real” -wp-timeout 20 strcmp.c'
WP插件生成的输出：
[wp] Warning: Missing RTE guards
[wp] strcmp.c:48: Warning:
Cast with incompatible pointers types (source: sint8*) (target: uint8*)
[wp] strcmp.c:48: Warning:
Cast with incompatible pointers types (source: sint8*) (target: uint8*)
[wp] 49 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_real_main_call_stringCompare_requires_validLengthS1 : Timeout (Qed:2ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_main_call_stringCompare_requires_validLengthS2 : Timeout (Qed:2ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_main_call_stringCompare_2_requires_validLengthS1 : Timeout (Qed:4ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_main_call_stringCompare_2_requires_validLengthS2 : Timeout (Qed:3ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_main_call_stringCompare_3_requires_validLengthS1 : Timeout (Qed:8ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_main_call_stringCompare_3_requires_validLengthS2 : Timeout (Qed:8ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_main_call_stringCompare_4_requires_validLengthS1 : Timeout (Qed:11ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_main_call_stringCompare_4_requires_validLengthS2 : Timeout (Qed:12ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_stringCompare_disjoint_SomeDifferent_allEqual : Timeout (Qed:3ms) (20s)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_stringCompare_allEqual_ensures : Timeout (Qed:15ms) (20s) (Stronger, 2 warnings)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_stringCompare_SomeDifferent_ensures : Timeout (Qed:14ms) (20s) (Stronger, 2 warnings)
[wp] [Alt-Ergo 2.2.0] Goal typed_real_stringLength_ensures_rightResult : Timeout (Qed:5ms) (20s)
[wp] Proved goals: 37 / 49
Qed: 30 (1ms-3ms-11ms)
Alt-Ergo 2.2.0: 7 (8ms-43ms-126ms) (464) (interrupted: 12)
这里有很多要点。首先，我要说的是，面对验证问题时，尝试使用内存模型可能不是第一件事（特别是，由于您没有使用浮点算法，因此该+real组件完全没有用）。因此，我建议-wp-model从等式中完全删除，默认选择通常足够好。另一方面，添加-wp-rte还检查潜在的运行时错误可能很有趣。
如果指定\valid_read(s1)，则表示可以访问s1[0]，但没有其他权限。如果您想谈谈几个存储单元的有效性，则可以使用\valid_read(s1 + (0 .. n))，或者在以N结尾的C字符串的情况下使用\valid_string(s1)。
你假定在这两个行为的条款stringCompare是不正确的：我们只是在寻找一个差异，直到strlen(s1)（含），直到n（其中的方式是相当无用的，很可能被删除：要指定strlen(s{1,2})是有界的，但SIZE_MAX在stdint.h应做到这一点）。此外，的相反\forall i, P(i) ==> Q(i)是\exists i, P(i) && !Q(i)（即，不要==>在之后使用\exists）。
最好将size_tC变量用作偏移量。否则，非常大的字符串可能会发生奇怪的事情。
您缺少一些不变性。基本上，stringCompare您必须在中捕获以下事实：
i停留在0和之间strlen(s1)（分别为strlen(s2)）s1实际上是\at(s1,Pre)+i（与的同上s2）s1和s2相等...由于Frama-C定位的默认体系结构使用char作为签名，unsigned char因此return语句中的转换会混淆WP。公认这是WP本身的弱点。
对于stringLength，也有必要要求类似valid_string(str)。但是，这一次您必须限制strlen(str)为严格小于SIZE_MAX（假设您更改了返回类型和声明result为be size_t），因为result必须向上执行strlen(str)+1而不会溢出。
同样，必须增强循环不变式：result由界定strlen(str)，并且我们必须指出到目前为止所有字符都不为0。
最后，在您的main函数中，WP的另一个弱点是无法检查是否满足stringCompare的前提条件。如果hello和helli被显式定义为char数组，那么一切都会很好。
tl; dr：以下代码可以用frama-c -wp -wp-rte file.c（Frama-C 22.0 Titanium和Alt-Ergo 2.2.0）完全证明
#include <stdint.h>
#include <string.h>
#include <stdio.h>
/*@
requires validPointers: valid_read_string(s1) && valid_read_string(s2);
requires validLengthS1: n >= strlen(s1) >= 0;
requires validLengthS2: n >= strlen(s2) >= 0;
assigns \nothing ;
allocates \nothing ;
frees \nothing ;
behavior allEqual:
assumes \forall integer k; 0 <= k <= strlen(s1) ==> s1[k] == s2[k];
ensures \result == 0;
behavior SomeDifferent:
assumes \exists integer k; 0 <= k <= strlen(s1) && s1[k] != s2[k];
ensures \result != 0;
disjoint behaviors;
complete behaviors;
*/
int stringCompare(const char* s1, const char* s2, size_t n) {
if (s1 == s2)
return 0;
size_t i = 0;
/*@ assert \valid_read(s1) ; */
/*@ assert \valid_read(s2) ;*/
/*@ loop invariant index: 0 <= i <= strlen(\at(s1,Pre));
loop invariant index_1: 0<= i <= strlen(\at(s2,Pre));
loop invariant s1_pos: s1 == \at(s1,Pre)+i;
loop invariant s2_pos: s2 == \at(s2,Pre)+i;
loop invariant equal: \forall integer j; 0<= j < i ==> \at(s1,Pre)[j] == \at(s2,Pre)[j];
loop invariant not_eos: \forall integer j; 0<= j < i ==> \at(s1,Pre)[j] != 0;
loop assigns i , s1, s2; */
while (*s1 == *(s2++))
{
/*@ assert i <= n ; */
++i;
if (*(s1++) == '\0')
return 0;
}
return *(s1) - *(--s2);
}
/*@
requires valid_string(str);
requires strlen(str) < SIZE_MAX;
assigns \nothing ;
ensures rightResult: \result == strlen(\old(str));
ensures rightEndCharacter: str[\result] == '\0' ; */
size_t stringLength(const char* str) {
size_t result = 0;
/*@ loop assigns result ;
loop invariant 0 <= result <= strlen(str);
loop invariant \forall integer i; 0<= i < result ==> str[i]!=0;
*/
while (str[result++] != '\0');
return --result;
}
/*@ assigns \nothing ;
ensures \result == 0 ;*/
int main(void) {
const char hello[] = { 'h', 'e', 'l', 'l', 'o', '\0'};
const char helli[] = { 'h', 'e', 'l', 'l', 'i', '\0'};
/*@ assert \valid_read(&hello[0]) && \valid_read(&helli[0]) ; */
stringCompare(hello, helli, 5);
return 0;
}
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句