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 <[email protected]> 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 > [email protected] > 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: [email protected] ----------------------------------------------------
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
