Hi Heming, Labels are global across the entire file, and are parsed in the order they are seen in the file. So it is fine to have a definition of a label be an inner expression.
On Tue, Jun 22, 2010 at 2:16 PM, Heming Cui <heming at cs.columbia.edu> wrote: > 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, Why do you say this is confusing? Labels are globally scoped, so it doesn't matter that the expression is inner. I tweaked the KQuery docs to make an explicit note about this. I have thought about adding explicit scoping for the labels, but haven't yet had a good reason. It does make it easier to concatenate two kquery files together. > // 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. I'm not sure what you mean by corrupt, and I only see one use and one def. The labels are immutable, and uses should always preceed defs, and duplicate definitions are illegal. The parser should reject any such cases and if it doesn't, it is a bug. > (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) > > ----------------------------------------------- I think what you are hitting here is that you are printing the expressions in distinct calls. The map used to assign expression labels is not shared across distinct calls to print(). If you want to print multiple expressions to one KQuery file, you should construct your own ExprPPrinter instance. Take a look at lib/Solver/PCLoggingSolver.cpp for an example. Please let me know if this doesn't resolve your problem. - Daniel > > > > > > > > > > > > > > > > ? 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 > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
