Bug in PushUp function due to the 'unwanted' store instruction

[ArpitaDutta]

New-WP branch sometimes generates wrong interpolants due to the unwanted 'store' instructions.

Let's consider these three programs:

Program 1:

#include <klee/klee.h>
#define BOUND 2
#define TARGET 4

int main() {
     int d = 1, choice, input = 0;
     for(;;) {
          if (d > BOUND) return 0;
          klee_make_symbolic(&choice, sizeof(int), "choice");  
          if (choice) d++; else break; 
     }
    while (d--) {
    int choice1; klee_make_symbolic(&choice1, sizeof(int), "choice1");
    if (choice1) input += 2; else input += 3;
    if (input == TARGET) klee_assert(0);     
    }
     return 0;
}

Program 2:

#include <klee/klee.h>
#define BOUND 2
#define TARGET 4

int main() {
     int d = 1, choice, input = 0;
     for(;;) {
          if (d > BOUND) return 0;
          klee_make_symbolic(&choice, sizeof(int), "choice");  
          if (choice) d++; else break; 
     }
    while (d) {
    d--;
    int choice1; klee_make_symbolic(&choice1, sizeof(int), "choice1");
    if (choice1) input += 2; else input += 3;
    if (input == TARGET) klee_assert(0);     
    }
     return 0;
}

Program 3:

#include <klee/klee.h>
#define BOUND 2
#define TARGET 4

int main() {
     int d = 1, choice, input = 0;
     for(;;) {
          if (d > BOUND) return 0;
          klee_make_symbolic(&choice, sizeof(int), "choice");  
          if (choice) d++; else break; 
     }
    for (;d;d--) {
    int choice1; klee_make_symbolic(&choice1, sizeof(int), "choice1");
    if (choice1) input += 2; else input += 3;
    if (input == TARGET) klee_assert(0);     
    }
     return 0;
}

All these three programs are logically the same. They are syntactically different only for their loop conditions. Program 1: while (d--) Program 2: while (d) { d--; Program 3: for (;d;d--) {

The llvm IRs for these programs corresponding to these statements (only the looping conditions) are: Program 1:
%17 = load i32* %d, align 4, !dbg !138 %18 = add nsw i32 %17, -1, !dbg !138 store i32 %18, i32* %d, align 4, !dbg !138 %19 = icmp ne i32 %17, 0, !dbg !138 br i1 %19, label %20, label %36, !dbg !138

Program 2 & 3:
%17 = load i32* %d, align 4, !dbg !138 %18 = icmp ne i32 %17, 0, !dbg !138 br i1 %18, label %19, label %37, !dbg !138

But the new-wp branch generates correct interpolants for programs 2 and 3 and not for program 1.

This is because of the extra store instruction in the llvm IR of program 1. This 'store' instruction is not required when we do the final condition check while exiting the loop.

Since, the pushup function mainly focuses on two instructions, 1. branch and 2. Store. It operates in this store instruction and stores the wrong value of the operand and which ultimately leads to wrong interpolants.

Suggestion For the time being, we can avoid writing loop break or exit conditions involving increment and decrement operators.

[rasoolmaghareh]

agreed, we can consider this as a limitation for now.