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
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100622/b829c972/attachment.html
