[klee-dev] STP Error: BVTypeCheck: terms in atomic formulas must be of equal length

[Shivoa Birch]

Hi, I'm wondering is anyone with knowledge of the llvm ir to STP problem
translation stage could provide me with some illumination. I'm having
issues getting Klee to process a symbolic integer value that has undergone
division.

As printed below, I get an exploration of the program paths working exactly
as I expect it (with output from all printf commands). The moment I
uncomment the final test, the only printf commands that trigger are the top
two (printing "4,") and then it always crashes with:

valuewidth of lhs of EQ: 32
valuewidth of rhs of EQ: 64
indexwidth of lhs of EQ: 0
indexwidth of rhs of EQ: 0
Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length

302:(EQ
  122:0x00000003
  300:0x000000000000003F)

I am unsure where this equality comparison is percolating up from with the
mismatched size. Any assistance would be welcome.

The cast to int is superfluous (as seen in the llvm ir):

#include <klee/klee.h>
int main(void) {
int a = klee_int("4-byte value"); //store *i32* %2, i32* %a, align 4
int b = 100; //store *i32 100*, i32* %b, align 4
printf("%lu,", sizeof a); //@printf(..., i64 *4*)
printf("%lu,", sizeof b);
if (a >= b) //*icmp sge i32* %5, %6 (%5/6 = load i32* %a/b)
puts("we see this");
if (a >= (long long)(b + 1)) //*icmp sge i64* %12, %15
puts("we'll see this");
if (a >= b/10) //sdiv i32 %21, 10; sdiv i32 %21, 10
puts("this does work");
/* if ((int)(a/10) >= b) //sdiv i32 %27, 10; *icmp sge i32* %28, %29
puts("uncommenting this will mean we never see any of the puts");
*/}

I just can't see what the difference is - I noted this issue arise in
several real-world examples I was testing and tried to make a small example
to demonstrate what seems to be triggering it. Full block of the llvm ir
that works and (shown commented above) that causes this crash/STP fail:

  %20 = load i32* %a, align 4
  %21 = load i32* %b, align 4
  %22 = sdiv i32 %21, 10
  %23 = icmp sge i32 %20, %22
  br i1 %23, label %24, label %26

; <label>:24                                      ; preds = %19
  %25 = call i32 (i8*, ...)* bitcast (i32 (...)* @puts to i32 (i8*,
...)*)(i8* getelementptr inbounds ([15 x i8]* @.str4, i32 0, i32 0))
  br label %26

; <label>:26                                      ; preds = %24, %19
  %27 = load i32* %a, align 4
  %28 = sdiv i32 %27, 10
  %29 = load i32* %b, align 4
  %30 = icmp sge i32 %28, %29
  br i1 %30, label %31, label %33

; <label>:31                                      ; preds = %26
  %32 = call i32 (i8*, ...)* bitcast (i32 (...)* @puts to i32 (i8*,
...)*)(i8* getelementptr inbounds ([57 x i8]* @.str5, i32 0, i32 0))
  br label %33
-------------- next part --------------
HTML attachment scrubbed and removed