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
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
