Crash in wp-interpolation branch

[rasoolmaghareh]

@xuanlinhha can you please check the following issue.

The wp-interpolant branch results in the following crash when running with the following program:

0  libLLVM-3.4.so  0x00007f1b167aa052 llvm::sys::PrintStackTrace(_IO_FILE*) + 50
1  libLLVM-3.4.so  0x00007f1b167a97c4
2  libpthread.so.0 0x00007f1b15ea7390
3  libc.so.6       0x00007f1b13845428 gsignal + 56
4  libc.so.6       0x00007f1b1384702a abort + 362
5  libc.so.6       0x00007f1b1383dbd7
6  libc.so.6       0x00007f1b1383dc82
7  klee            0x000000000051182d klee::TxWPHelper::substituteExpr(klee::ref<klee::Expr>, klee::ref<klee::Expr>, klee::ref<klee::Expr>) + 3645
8  klee            0x000000000050d88f klee::TxWeakestPreCondition::PushUp(std::vector<std::pair<klee::KInstruction*, int>, std::allocator<std::pair<klee::KInstruction*, int> > >) + 3231
9  klee            0x00000000004e7978 klee::TxTreeNode::generateWPInterpolant() + 1048
10 klee            0x00000000004e8f6b klee::TxSubsumptionTableEntry::TxSubsumptionTableEntry(klee::TxTreeNode*, std::vector<llvm::Instruction*, std::allocator<llvm::Instruction*> > const&) + 1051
11 klee            0x00000000004ece7b klee::TxTree::remove(klee::ExecutionState*, klee::TimingSolver*, bool) + 795
12 klee            0x000000000047c74e klee::Executor::updateStates(klee::ExecutionState*) + 526
13 klee            0x0000000000492bc7 klee::Executor::run(klee::ExecutionState&) + 3495
14 klee            0x0000000000493b97 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1703
15 klee            0x0000000000464d8d main + 12765
16 libc.so.6       0x00007f1b13830830 __libc_start_main + 240
17 klee            0x000000000046d809 _start + 41

Source code:

#include <klee/klee.h>

#define N 10
#define BOUND 66
int sum = 0;
int weight[] = {0,1,2,3,4,5,6,7,8,9,10};
int GOAL = 0;

int check_infeasible() {  if (sum > BOUND) exit(0); }
int check_goal(int x) { 
   if (x == N) {
    printf("Sum:%d\n",sum); 
    exit(0);
   }
}

int choice(int z, int flip) {

    if(flip){
        if (z != 0) z=1; 
        else z = 0;                                                                       
    }else{
        if (z != 1) z=0; 
        else z = 1;                                                                       
    }
    return z;
}

int sim(int x, int v) {
   sum += v * weight[x];
   check_infeasible();
   check_goal(x);
}

int main() {
       int x = 0;
       for (x = 1; x<=N; x++) { // can choose in another order
           int v;
           klee_make_symbolic(&v, sizeof(unsigned), "v");
           if (x % 2) v = choice(v, 0); else v = choice(v, 1);
           sim(x, v);
       }
}

[rasoolmaghareh]

The crash issue is from this function:

int check_goal(int x) { 
   if (x == N) {
    printf("Sum:%d\n",sum); 
    exit(0);
   }
}

[xuanlinhha]

info.txt Can you see if the command is like this @rasoolmaghareh ? On my side, there is no crash, I ran with this branch fix_skip_void_type

[rasoolmaghareh]

@xuanlinhha Thanks. The issue is fixed on the above program, but it still crashes on the following example:

#include <klee/klee.h>

#define N 10
#define BOUND 66
int weight[] = {0,1,2,3,4,5,6,7,8,9,10};
int GOAL = 0;

int main() {
       int sum = 0;
       int x = 0;
       for (x = 1; x<=N; x++) { 
           int v;
           klee_make_symbolic(&v, sizeof(unsigned), "v");
           if (v != 0) v=1; else v = 0;                                                                       
           sum += v * weight[x];
       if (sum > BOUND) exit(0);
       if (x == N) {printf("Sum:%d\n",sum); exit(0);} 
       }
       printf("Sum:%d\n",sum);
}

[xuanlinhha]

info.txt @rasoolmaghareh running this program has no crashes on my side too. on fix_skip_void_type branch

[xuanlinhha]

I have just made one commit to skip some more functions when we push up WP. 2 programs above I see it runs with no error. can you please check again?

[rasoolmaghareh]

The crash is fixed. Thanks. I am closing this issue.