Or maybe my format of storing expressions are not correct. Currently I am storing the two expressions within one kquery file. Maybe storing the two constraints in seperate KQuery files can solve the problem?
2010/6/22 Heming Cui <heming at cs.columbia.edu> > Dear Daniel, > I did some more expressions and it seems to me that something might be > wrong with the labeling mechanism in KLEE expressions. > > Once I collected two expressions and dump them to a file with KQuery > format: > > ------------------------------------------------- > (Eq 4294967279 > (Select w32 (Slt N0:(Xor w32 4294967295 > (ReadLSB w32 0 n)) > 4294967279) > 4294967279 > N0)) > > > // Actually I think this expression is a little confusing, because the > label N0 is withwin the inner most sub expression, > // so when parser is processing the second and the third "N0" (if it is top > down parsing, so the third "N0" is hit first?), it may corrupt the N0 in > this expression with the N0 in the expression above. > > > (Slt (Select w32 (Slt N0:(ReadLSB w32 0 n) > 16) > N0 > 16) > N0) > ------------------------------------------------- > > > > > > > However, when I use createDefaultExprBuilder() to load these two > expressions back and print them out to the screen, they are: > > ----------------------------------------------- > (Eq 4294967279 > (Select w32 (Slt N0:(Xor w32 4294967295 > (ReadLSB w32 0 n)) > 4294967279) > 4294967279 > N0)) > > > > (Slt (Select w32 (Slt N0:(ReadLSB w32 0 n) > 16) > N1:(Xor w32 4294967295 N0) // > Please pay attention here, this line is wrong, it should be "N0" or > "(ReadLSB w32 0 n)", but the N0 in this expression now is from the first > expression, "Xor". > 16) > N1) > > ----------------------------------------------- > > > > > > > > > > > > > > > > If I remove the labels in the second expression, and store them to a > KQuery file like this (actually I manually modify the second expression to > remove labels): > ------------------------------------------------- > (Eq 4294967279 > (Select w32 (Slt N0:(Xor w32 4294967295 > (ReadLSB w32 0 n)) > 4294967279) > 4294967279 > N0)) > > > (Slt (Select w32 (Slt (ReadLSB w32 0 n) > 16) > (ReadLSB w32 0 n) > 16) > (ReadLSB w32 0 n)) > ------------------------------------------------- > > > > > > > > > And now, I use createDefaultExprBuilder() to load them back and print > them out, they are: > -------------------------------------------------- > (Eq 4294967279 > (Select w32 (Slt N0:(Xor w32 4294967295 > (ReadLSB w32 0 n)) > 4294967279) > 4294967279 > N0)) > > > > (Slt (Select w32 (Slt N0:(ReadLSB w32 0 n) > 16) > > N0 // Please pay > attention to this line, now it is correct, the N0 in the first expression > does not flow to the second expression. > 16) > N0) > > -------------------------------------------------- > > > > > > > In a high level, it seems to me that the labels have been "flown" from > the first expression to the second one, or the generation of labels for the > second expression is confusing. What is the effective scope of a label? Is > there any easy way to disable labeling? > > I am looking forward to your comments. > > > > > > > > > > 2010/6/22 <hc2428 at columbia.edu> > > Dear folks, >> I am wondering how labels for expressions work? Could you please >> tell me which part of code is handling replacing sub-expressions with >> labels? >> For example, given the expression below: >> >> (Slt (Select w32 (Slt N0:(ReadLSB w32 0 n) >> 16) >> N0 >> 16) >> N0) >> >> If I want to disable the labels, i.e., I want the expression to be >> like this: >> >> (Slt (Select w32 (Slt (ReadLSB w32 0 n) >> 16) >> (ReadLSB w32 0 n) >> 16) >> (ReadLSB w32 0 n)) >> >> Which part of code should I look for? >> >> Thanks, >> Heming Cui >> _______________________________________________ >> klee-dev mailing list >> klee-dev at keeda.stanford.edu >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> > > > > -- > Regards, > Heming Cui > -- Regards, Heming Cui -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100622/2128daab/attachment-0001.html
