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

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");
}

I'm only trying to get a graph that of Total nodes 6 that has a Hamiltonian path. That works well with above code. But when i try to use len i.e total no.of edges i'm getting infinite unwinding in cbmc run .

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

great Debug msg.. have you tried printing `len`? what's its value? — Minato, Nov 18 '15 at 07:15
Yes i did . That's why i first just calculate total edges and just printed the same. No problems whatsoever. i.e if i delete last for loop and just print len everything is fine. I don't understand that max len could be just (n * n-1) but why its taking infinite unwindings ? — user2754673, Nov 18 '15 at 07:21
`0<= graph[i][j] <= 1` should be `0 == graph[i][j] || graph[i][j] == 1`. — mch, Nov 18 '15 at 07:23
@mch that can't be a problem.. since at most len could never go past `n * n-1` — Minato, Nov 18 '15 at 07:26
How did that helps ?? graph[i][j] is unsigned int which can be between 0 and 1 that means zero or one. But yes your representation is far better. — user2754673, Nov 18 '15 at 07:26
@user2754673 I am not sure.. but can you try printing inside `len = len + 1;` does it print finite numbers — Minato, Nov 18 '15 at 07:27
@user2754673 put this `printf("%d",len);` before `len = len + 1;`.. and try using an increment operator `len++;` — Minato, Nov 18 '15 at 07:29
no prob. If i delete the last for loop and try to print len +1 each time. Starting with zero its printing 1...32. and len counts turns out to be 32 after the print. — user2754673, Nov 18 '15 at 07:30
@Minato no change , I think you guys are not targeting the prob. This problem happened as i turned the graph as input to any arbitrary graph. i thought this might be caused due to it might be constraining all the graphs of nodes 6 but i then changed the total nodes to 2 but still same prob, something going under cbmc hood ? — user2754673, Nov 18 '15 at 07:33
The problem could be.. Though I am not sure.. but some how the first/sign bit is being set in the `len` causing it to go berserk.. — Minato, Nov 18 '15 at 07:33
Let us [continue this discussion in chat](http://chat.stackoverflow.com/rooms/95412/discussion-between-user2754673-and-minato). — user2754673, Nov 18 '15 at 07:34

score 1 · Accepted Answer · answered Nov 18 '15 at 10:09

I'm Not sure about the policy of stack-overflow but in order to clarify the issue i'm posting an answer that was posted by Martin of oxford university on CBMC support forum.

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.

thanks all for helping.

The only thing that was puzzling me was the max value that len could pick is (n * n-1) so why infinite unwiding ! — user2754673, Nov 18 '15 at 10:12

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

1 Answers1