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 ie total no.of edge を使用しようとすると、 cbmc run で無限の巻き戻しが発生します。

上記のコードは、 len を使用して反復しない限りうまく機能します。cbmc の実行が無限の巻き戻しに入る ?? 誰でもそれを説明できますか。

4

1 に答える 1

1

スタックオーバーフローのポリシーについてはよくわかりませんが、問題を明確にするために、オックスフォード大学のマーティンが CBMC サポート フォーラムに投稿した回答を投稿しています。

上記のコードは、 len を使用して反復しない限りうまく機能します。cbmc の実行が無限ループに入る ?? 誰でもそれを説明できますか。

簡単な回答: はい、想定どおりです。 --unwind を使用してください

長い答え: CBMC のループ境界の検出は比較的単純です。シンボリック実行中に分岐条件を静的に false に単純化できる場合にのみ、(ループの巻き戻し制限なしで) ループの巻き戻しを停止します。

グラフの値は非決定論的であるため、len の値は非決定論的になります。もちろん、残りのコードの動作から len <= N*N であることはわかっていますが、単純化だけではこれを取得できないため、CBMC はこれを「認識」せず、ループの巻き戻しはそれ自体で終了しません。

境界検出をもっとスマートにしないのはなぜですか? たとえば、変数の間隔を追跡しますか? できますが、完全な決定手順がない限り、このようなケースが常に見つかります。そこに完全な決定手順を配置すると、symex ツールが行うパスベースのシンボリック実行を行うか、インクリメンタル BMC を行うことになります (これに使用できるツールがあり、CBMC の次のバージョンにマージされる可能性があります)。 )、巻き戻しとアサーションを別々に決定するか、一緒に決定するかによって異なります。

助けてくれてありがとう。

于 2015-11-18T10:09:16.927 に答える