A strange STP expression generated

[Qiuping Yi]

Hi, everybody,

Now I encountered a strange thing, and I need your help.

When I resolve stp to query the next result of the next expression from
KLEE,

(Eq false
(Slt 0
(ReadLSB w32 0 const_arr10)))

It told me that it is unsolvable, and I printed the expression in stp with
command *vc_printVarDecls(vc)* and *vc_printExpr(vc, e)*,
then it represented:

__tmpInt8 : BITVECTOR(8);
__tmpInt16 : BITVECTOR(16);
__tmpInt32 : BITVECTOR(32);
__tmpInt64 : BITVECTOR(64);
x_0x2d4edf0 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
y_0x2d4f560 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
z_0x2d45900 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
const_arr10_0x2d9d810 : ARRAY BITVECTOR(32) OF BITVECTOR(8); // var
declaration
*(LET let_k_0 = ((((const_arr10_0x2d9d810 WITH [0x00000000] := 0x00)*
* WITH [0x00000001] := 0x00)*
* WITH [0x00000002] := 0x00)*
* WITH [0x00000003] := 0x00)*
* IN *
( NOT( SBVLT(0x00000000,(let_k_0[0x00000003] @ (let_k_0[0x00000002] @
(let_k_0[0x00000001] @ let_k_0[0x00000000]
)
)
))
)))

Could you tell me what does the bold part mean?? I think only the red part
is needed for represent this expression.

In addition, when I query the next KLEE expression,

(Eq false
(Slt 0
(ReadLSB w32 0 x)))

the related stp expression just is:

( NOT( SBVLT(0x00000000,(x_0x2d4edf0[0x00000003] @ (x_0x2d4edf0[0x00000002]
@ (x_0x2d4edf0[0x00000001] @ x_0x2d4edf0[0x00000000]
)
)
))
))

SO, what's wrong? How can I query the result of the first expression with
STP?

Thank you all in advance.

--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences

[Cristian Cadar]

Hi,

The two expressions are indeed not equivalent, you seem to be printing
different things in CVC and Kleaver formats. You can use
--use-query-log=all:pc to print out the entire set of queries issued by
KLEE, using its own query language.

Cristian

Post by Qiuping Yi
Hi, everybody,
Now I encountered a strange thing, and I need your help.
When I resolve stp to query the next result of the next expression from
KLEE,
(Eq false
(Slt 0
(ReadLSB w32 0 const_arr10)))
It told me that it is unsolvable, and I printed the expression in stp
with command *vc_printVarDecls(vc)* and *vc_printExpr(vc, e)*,
__tmpInt8 : BITVECTOR(8);
__tmpInt16 : BITVECTOR(16);
__tmpInt32 : BITVECTOR(32);
__tmpInt64 : BITVECTOR(64);
x_0x2d4edf0 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
y_0x2d4f560 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
z_0x2d45900 : ARRAY BITVECTOR(32) OF BITVECTOR(8);
const_arr10_0x2d9d810 : ARRAY BITVECTOR(32) OF BITVECTOR(8); // var
declaration
*(LET let_k_0 = ((((const_arr10_0x2d9d810 WITH [0x00000000] := 0x00)*
* WITH [0x00000001] := 0x00)*
* WITH [0x00000002] := 0x00)*
* WITH [0x00000003] := 0x00)*
* IN *
)
)
))
)))
Could you tell me what does the bold part mean?? I think only the red
part is needed for represent this expression.
In addition, when I query the next KLEE expression,
(Eq false
(Slt 0
(ReadLSB w32 0 x)))
x_0x2d4edf0[0x00000000]
)
)
))
))
SO, what's wrong? How can I query the result of the first expression
with STP?
Thank you all in advance.
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev