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

[Martin Nowack]

Hi,

Which version of STP and KLEE are you using?

I cannot reproduce your issue and get the following output with the recent stable version of STP.

KLEE: output directory is "/tmp/klee-out-3"
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING ONCE: calling external: printf(51599888, 4)
4,4,KLEE: WARNING ONCE: calling external: puts(51458896)
we see this
we'll see this
this does work
this does work
this does work
uncommenting this will mean we never see any of the puts

KLEE: done: total instructions = 124
KLEE: done: completed paths = 5
KLEE: done: generated tests = 5

If your problem persists, please open a bug report here (https://github.com/klee/klee/issues) and we try to solve it from there.

Cheers,

Martin

> On 28 Aug 2015, at 11:08, Shivoa Birch <shivoa at gmail.com> wrote:
> 
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

---------------------------------------------------
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150907/9ba1dcfc/attachment.sig>