如何用frama -c wp中的计算证明迭代循环？

Question

我有我的测试代码(研究WP循环不变量),它在数组单元格中添加两个长整数,每个数字的表示形式:

int main(int argc, const char * argv[]) {

char a[32], b[32];//size can be very big
memset(a, 0, sizeof(a));
memset(b, 0, sizeof(b));
scanf("%s %s", a, b);
unsigned int size1 = strlen(a);
unsigned int size2 = strlen(b);
//code to reverse a string. currently proved 
reverse(a, size1);
reverse(b, size2);
for (unsigned int i = 0; i < size1; i++) a[i]-='0'; //move from chars to integers
for (unsigned int j = 0; j < size2; j++) b[j]-='0';
unsigned int maxsize = size1;
if (size2 > maxsize) maxsize = size2;
int over = 0;
//actual computation code

/*@
loop invariant maxsize == \max(size1, size2);
loop invariant bound: 0 <= k <= maxsize;
loop invariant ov: \forall integer i; 0 < i < k ==> \at(a[i], Here) == (\at(a[i], Pre) + b[i]+ Over((char *)a, (char *)b, i)) % 10;
loop assigns k, a[0..maxsize-1],over;
loop variant maxsize - k;
*/
for (unsigned int k = 0; k < maxsize; k++)
{
    char sum=a[k] + b[k] + over; 
    //over=overflow is for 9+9 = 18, result=8, over=1
    a[k] = sum % 10;
    over = sum / 10;
}
if (over != 0) a[maxsize++] = over;
//...
return 0;
}

我想只指定最后一个循环不变量.我已经用\ at(a [i],LoopCurrent)尝试了一些ACSL代码.我收到了未知状态或超时.最后,我完成了一个公理的递归解决方案,没有任何成功.

我现在没有任何想法,我还应该尝试验证这一点.救命？

更新:为实际计算创建了一个函数.改进的公理.仍然有超时状态.使用默认设置(超时= 10,证明者Alt-Ergo)使用opam的Frama-C最新版本.

/*@
@predicate
Unchanged{K,L}(char* a, integer first, integer last) = \forall integer i; first <= i < last ==> \at(a[i],K) == \at(a[i],L);

axiomatic ReminderAxiomatic
{
logic integer Reminder {l} (integer x, integer y);
axiom ReminderEmpty: \forall integer x, integer y; x < y ==> Reminder(x, y) == x;
axiom ReminderNext: \forall integer x, integer y; x>=y ==> Reminder(x, y) == Reminder(x-y, y)+0; 
}

axiomatic DivAxiomatic
{
logic integer Div {l} (integer x, integer y);
axiom DivEmpty: \forall integer x, integer y; x < y ==> Div(x, y) == 0 ;
axiom DivNext: \forall integer x, integer y; x >= y ==> Div(x, y) == Div(x - y, y) + 1 ;
}

axiomatic OverAxiomatic
{
logic integer Over {L}(char *a, char * b, integer step) reads a[0..step-1], b[0..step-1];
axiom OverEmpty: \forall char *a, char * b, integer step; step <= 0 ==> Over(a, b, step) == 0;
axiom OverNext: \forall char *a, char * b, integer step; step > 0 && a[step-1]<10 && a[step-1]>=0 && b[step-1]<10 && b[step-1]>=0
==> Over(a, b, step) ==  Div((int) a[step-1]+(int)b[step-1]+(int)Over(a,b,step-1), 10);
}
*/
/*@
requires 0 <= maxsize < 10;
requires \valid (a+(0..maxsize-1));
requires \valid (b+(0..maxsize-1));
requires \valid (res+(0..maxsize));
requires \forall integer i; 0 <= i < maxsize ==> 0 <= (int)a[i] < 10;
requires \forall integer i; 0 <= i < maxsize ==> 0 <= (int)b[i] < 10;
*/
void summ(char *a, char *b, char *res, unsigned int maxsize) {

char over = 0;

/*@
loop invariant bound: 0 <= k <=maxsize;
loop invariant step: \forall integer i; 0 <= i < k ==> res[i] == (char) Reminder((int)a[i]+ (int)b[i]+ (int)Over((char *)a, (char *)b, i) , 10);
loop invariant unch: Unchanged{Here,LoopEntry}((char *)res, k, maxsize);
loop assigns k, over, res[0..maxsize-1];
loop variant maxsize-k;
*/
for (unsigned int k = 0; k < maxsize; k++)
{
 char sum = a[k] + b[k] + over;
 res[k] = sum % 10;
 over = sum / 10;
}

//
if (over != 0) res[maxsize++] = over;

}

Answer 1

首先,如果你的问题包含一个MCVE会更好,在当前情况下包括你正在处理的C函数(而不仅仅是它的正文),以及你写的ACSL注释,代码中的确切位置.用于启动Frama-C的命令行也不会受到影响,以及您遇到问题的注释列表.

除此之外,这里有一些可能与您的问题有关的事情(再次,没有确切的描述,很难确定).

• 这loop assigns是错的:你over在循环中分配,但在那里没有提到.
• 我不确定\maxWP 能否得到很好的支持.
• 模数和整数除法是两个操作自动化的证明者倾向于挣扎.您可能需要一些额外的断言和/或公理来帮助他们.
• 你loop invariant没有对a[i]for 的价值说什么k <= i< maxsize.由于loop assigns表明a可能已修改了所有可能的单元格,因此必须添加一个不变量,告知目前尚未触及具有较高索引的单元格.
• 我不完全确定你的用法\at(a[i],Pre):Pre表示当前函数的开头.因此,如果scanf和reverse它在循环中具有相同的功能(再次,MCVE会澄清这一点),这不是真的.您可能想要谈论\at(a[i],Loop_entry)在第一次进入循环的状态中引用单元格的值.

UPDATE

我担心WP无法完全证明你的注释,但我设法获得了一个版本,其中只有一个lemma,基本上是reads该Over函数的子句的扩展版本未被证实(我相信有没有办法在WP的C存储器的实际表示下证明它.请注意,它意味着使用WP的TIP功能.下面提供了代码和脚本,但我将首先评论您的原始版本:

• 没有必要Div和Reminder.如果有的话,他们会混淆证明者.你可以坚持xxx/10和xxx%10.事实上,我对分裂和模数的评论有点过于谨慎.在目前的情况下,一切似乎都很好.
• 同样,Unchanged可以内联,但保持这种方式不应该受到伤害.
• 我使用unsigned char而不是char,因为它避免了由于整数提升导致的一些虚假转换,并删除了逻辑中的任何强制转换.您通常不必在ACSL注释中引入此类强制转换,除非可能表示某些计算保持在适当的范围内(如\let x = y + z; x == (int) x;).这些演员阵容在证明义务中被转换为函数调用,并且它再次混淆了证明者.
• 缺少一个不变量来表示over确实包含了前一步骤的潜在进位(同样,一个很好的暗示,你错过了一个不变量,就是所提到的位置loop assigns没有出现在任何位置loop invariant).
• 最后,还有一个小小的微妙之处:如果你没有以某种方式表明over只能是0或者1,没有任何东西阻止加法溢出unsigned char(使得无法证明C计算unsigned char与其无条件整数的ACSL对应物给出了同样的结果).由于的递归性质Over的功能,这可以通过所谓的建立引理功能,其中数学归纳法由简单的for循环用适当的不变量进行
• 另外,我已经明确地添加了作为不变量a并且b保持不变.这通常暗示loop assigns,但有这些明确的假设使脚本更容易.

总结一下,这是最终的代码:

/*@
axiomatic Carry {
 logic integer Over {L}(unsigned char* a, unsigned char* b, integer step)
 reads a[0 .. step - 1], b[0 .. step - 1];

 axiom null_step: \forall unsigned char* a, *b, integer step;
                  step <= 0 ==> Over(a,b,step) == 0;
 axiom prev_step: \forall unsigned char* a, *b, integer step;
                  step > 0 ==>
                  Over(a,b,step) ==
                  (a[step-1] + b[step - 1] + Over(a,b,step-1)) / 10;

lemma OverFootPrint{L1,L2}:
\forall unsigned char* a, unsigned char*b, integer step;
(\forall integer i; 0<=i<step ==> \at(a[i],L1) == \at(a[i],L2)) &&
(\forall integer i; 0<=i<step ==> \at(b[i],L1) == \at(b[i],L2)) ==>
Over{L1}(a,b,step) == Over{L2}(a,b,step);
}
*/

/*@
  requires \valid(a+(0 .. step-1));
  requires \valid(b+(0 .. step - 1));
  requires \forall integer i; 0<=i<step ==> 0<=a[i]<10 && 0<=b[i]<10;
  assigns \nothing;
  ensures 0<= Over(a,b,step) <= 1;
*/
void lemma_function(unsigned char* a, unsigned char* b, unsigned int step) {
  /*@
      loop invariant 0<=i<=step;
      loop invariant \forall integer k; 0<=k<=i ==> 0 <= Over(a, b, k) <= 1;
      loop assigns i;
  */
  for (int i = 0; i < step; i++);
}

/*@
requires 0 <= maxsize < 10;
requires \valid (a+(0..maxsize-1));
requires \valid (b+(0..maxsize-1));
requires \valid (res+(0..maxsize));
requires \separated (a+(0..maxsize-1),res+(0..maxsize));
requires \separated (b+(0..maxsize-1),res+(0..maxsize));
requires \forall integer i; 0 <= i < maxsize ==> 0 <= a[i] < 10;
requires \forall integer i; 0 <= i < maxsize ==> 0 <= b[i] < 10;
*/
void summ(unsigned char* a, unsigned char*b, unsigned char* res,
          unsigned int maxsize) {

unsigned char over = 0;

/*@
loop invariant bound: 0 <= k <=maxsize;
loop invariant step: \forall integer i; 0 <= i < k ==> res[i] == (a[i]+ b[i]+ Over(a,b,i)) % 10;
loop invariant over: over == Over(a,b,k);
loop invariant a_unchanged: \forall integer i; 0 <= i < maxsize ==>
\at(a[i],LoopEntry) == a[i];
loop invariant b_unchanged: \forall integer i; 0 <= i < maxsize ==>
\at(b[i],LoopEntry) == b[i];
loop invariant unch: \forall integer i; k<=i<=maxsize ==> \at(res[i],LoopEntry) == res[i];
loop assigns k, over, res[0..maxsize-1];
loop variant maxsize-k;
*/
for (unsigned int k = 0; k < maxsize; k++)
{
 unsigned char sum = a[k] + b[k] + over;
 res[k] = sum % 10;
 over = sum / 10;
 lemma_function(a,b,k);
}

//
if (over != 0) res[maxsize++] = over;

}

这两个TIP脚本可在这里.要使用它们,请将它们放在scripts/typed代码旁边的目录中(比如说file.c)并使用以下命令行:

frama-c[-gui] -wp -wp-prover alt-ergo,script -wp-session scripts file.c

您可以根据需要更改scripts目录的名称(它必须与参数匹配-wp-session),但typed脚本的文件名必须是给定的,因为WP将使用它们来检测它们应该证明哪个证明义务.在GUI模式下,您可以查看脚本,但可能很难理解并解释每个步骤都不适合SO的答案.