1 
#include<stdio.h>

#define N 6
#define M 10

typedef int bool;
#define true 1
#define false 0

unsigned int nondet_uint();  

typedef unsigned __CPROVER_bitvector[M] bitvector; 

unsigned int zeroTon(unsigned int n) {
   unsigned int result = nondet_uint();
   __CPROVER_assume(result >=0 && result <=n);
   return result ;
};


//Constrine the value between 0 and 1
unsigned int  nondet (){  
  unsigned int num = nondet_uint();
  __CPROVER_assume( num>= 0 && num  <= 1);
  return num;
}; 

void main() {
   unsigned int pos , i, j, k;

   unsigned int len = 0;
   bool Ch , Ck , C0 ;

  bitvector compartment1 , compartment2 , compartment3 , compartment4, compartment5, compartment6;
bitvector nodes[N] = {compartment1, compartment2, compartment3, compartment4, compartment5, compartment6};


// Represent the graph with given topology 
unsigned int graph[N][N];

for(i=0;i <N; i++) {
    for(j=0;j<N;j++) {
        graph[i][j] = nondet();
    }
}



unsigned int p[N] ;
unsigned int ticks;


   //Make sure that graph is one connected  : just find one hamiltonian cycle 
   //make sure elements are in between node no's and all are distinct

for(i=0; i<N; i++) {
    p[i] = zeroTon(5);
}

for(i=0; i <N; i++) {
     for(j=0; (j<N) && (j!=i) ; j++) {    
    if( p[i] != p[j]){
            C1 = C1 && 1;
        }
        else {
            C1 = C1 && 0;
        }

     }
}

 //hamiltonian One exists 
 for(i=0;i<N-1;i++) {
    if( graph[p[i]][p[i+1]] == 1) {
       Ch = Ch && 1;
    }
   else {
       Ch = Ch && 0;
   }
  }

 len =0;
 for(i=0;i<N;i++) {
   for(j=0;j<N; j++){
          if (graph[i][j] == 1) {
              len = len + 1;
          }
    }
  }

  //THIS IS GOING IN INFINITE LOOP ?? WHY ?? 
  for(i=0;i<len;i++) {
   printf("i'm a disco dancer ");

  }
  __CPROVER_assert(!(Ch && C1) , "Graph has an ham path");
}

我只是想得到一个具有哈密顿路径的总节点 6 的图表。这适用于上面的代码。但是，当我尝试使用 len 即总边缘数时，我在 cbmc run 中得到了无限展开。

上面的代码运行良好，除非我使用 len 进行迭代。cbmc 运行进入无限展开？？谁能解释一下。

4

1 回答 1

1

我不确定堆栈溢出的政策，但为了澄清这个问题，我发布了牛津大学的 Martin 在 CBMC 支持论坛上发布的答案。

上面的代码运行良好，除非我使用 len 进行迭代。cbmc 运行进入无限循环？？谁能解释一下。

简短的回答：是的，这是预期的，使用 --unwind

长答案：CBMC 对循环边界的检测相对简单；如果分支条件在符号执行期间可以静态简化为 false，它只会停止展开循环（没有循环展开限制）。

因为 graph 的值是非确定性的，所以 len 的值是非确定性的。当然，我们从其余代码的工作方式中知道 len <= N*N 但这不能仅通过简化来获得，因此 CBMC 不会“意识到”这一点，因此循环展开不会自行终止。

为什么我们不让边界检测更智能呢？比如说，跟踪变量的间隔？我们可以，但除非您在那里有完整的决策程序，否则您总会发现这样的案例。如果你在那里放置一个完整的决策程序，你要么在做基于路径的符号执行，这是我们的 symex 工具所做的，要么是在做增量 BMC（我们有可用的工具，它们可能会合并到下一个版本的 CBMC )，取决于您是单独还是一起决定展开和断言。

感谢大家的帮助。

于 2015-11-18T10:09:16.927 回答