Почему итерация по общему количеству ребер не приводит к бесконечному или конечному числу раскручиваний петель?

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, то есть полное число ребер, я получаю бесконечное раскручивание при запуске cbmc.

Приведенный выше код работает хорошо, если я не использую len. Cbmc запускается в бесконечном раскручивании?? Может кто-нибудь это объяснит.

Answer 1

Я не уверен насчет политики переполнения стека, но чтобы прояснить проблему, я публикую ответ, который был размещен Мартином из Оксфордского университета на форуме поддержки CBMC.

Приведенный выше код работает хорошо, если я не использую len . Cbmc запускается в бесконечный цикл?? Может кто-нибудь это объяснит.

Краткий ответ: да, ожидается, используйте --unwind

Длинный ответ: CBMC обнаруживает границы цикла относительно просто; он только остановит разматывание цикла (без ограничения размотки цикла), если условие ветвления может быть статически упрощено до false во время символьного выполнения.

Поскольку значения графика недетерминированы, значение len будет недетерминированным. Конечно, из того, как работает остальная часть кода, мы знаем, что len <= N*N, но это не может быть получено только путем упрощения, поэтому CBMC не "осознает" это, и поэтому разматывание цикла не завершится само по себе.

Почему мы не делаем интеллектуальное обнаружение границ? Скажем, отслеживать интервалы для переменных? Мы могли бы, но если у вас нет полной процедуры принятия решения, вы всегда найдете такие случаи. Если вы поместите там полную процедуру принятия решения, вы либо выполняете символьное выполнение на основе пути, как это делает наш инструмент Symex, либо вы делаете инкрементальный BMC (для этого у нас есть инструменты, они могут быть объединены в следующую версию CBMC), в зависимости от того, решаете ли вы разматывать и утверждать отдельно или вместе.

спасибо всем за помощь.