为什么迭代总边缘数会导致无限或有限多个循环展开？

Question

#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 即总 no.of 边缘时，我在 cbmc 运行 .

中得到无限展开

除非我使用 len 进行迭代，否则上面的代码运行良好。 cbmc 运行进入无限平仓 ??谁能解释一下。

Answer 1

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

The above code works well unless i iterate using len . The cbmc run going into infinite loop ?? Can anyone explains that.

Short answer : Yes, it is expected, use --unwind

Long answer : CBMC's detection of loop bounds is relatively simple; it will only stop unwinding a loop (without a loop unwind limit) if the branch condition can be statically simplified to false during symbolic execution.

Because the values of graph are non-deterministic, so the value of len will be non-deterministic. Ofcourse we know from the way the rest of the code works that len <= N*N but this cannot be obtained by simplification alone, thus CBMC does not 'realise' this and so the loop unwinding will not terminate by itself.

Why don't we make the bound detection smarter? Say, track intervals for variables? We could but unless you have a complete decision procedure there, you will always find cases like this. If you put a complete decision procedure there you are either doing path-based symbolic execution, which is what our symex tool does, or you are doing incremental BMC (we have tools available for this, they may be merged into the next version of CBMC), depending on if you are deciding on unwinding and assertions separately or together.

感谢大家的帮助。

为什么迭代总边缘数会导致无限或有限多个循环展开？

Why iterating over total no of edges causing infinite or finitely many loop unwindings?

c

infinite-loop

cbmc