Tianhai Liu

2014-07-08 15:48:55 UTC

Hi,

I understand the techniques constraint independent and caching described

in KLEE paper, then I want to see how it works in KLEE, so I used KLEE to

analyze a small code. while I could not understand the generation.

When KLEE runs on the function as below: klee -use-query-log=all:smt2

-use-query-log=all:pc -use-query-log=solver:smt2 -use-query-log=solver:pc

-write-pcs -write-smt2s -write-cov -search=dfs constraint_independent.o

int constraint_independent(int x, int y) {

int c = 0;

if (x == 0) c = x++; // B1

else c = x--; // B2

if (y < 0) c = y++; // B3

else c = y--; // B4

return c;

}

Before optimization, I can see the KLEE generate Path conditions in the

order that (from file "all-queries.smt2"):

query0: [B2]

query1: [B2,B4]

query2: [B2,B4,True]

query3: [B2,B3,True]

query4: [B1,B3]

query5: [B1,B3,True]

query6: [B1,B4,True]

after optimizations, I presume the queries to the solver would be like :

query0: [B2] // wrt. query0.

query1: [B4] // wrt. query2. B1/B2 and B3/B4 are independent

query2: [B3] // wrt. query3

query3: [B1] // wrt. query4

query4: [B3] // wrt. query5

query5: [B4] // wrt. query6

while the actual queries to the solver is (from file

"solver-queries.smt2"):

query0: [True]

query1: [B2]

query2: [B3]

query3: [B2,B3,True]

Is my presumption correct if only considering the constraint independent

and caching? If not, do I need some options to disable other

optimizations? Btw, is there some reason to introduce the "True" for some

PCs? I appreciate any suggestion and help highly.

Best regards,

Tianhai

I understand the techniques constraint independent and caching described

in KLEE paper, then I want to see how it works in KLEE, so I used KLEE to

analyze a small code. while I could not understand the generation.

When KLEE runs on the function as below: klee -use-query-log=all:smt2

-use-query-log=all:pc -use-query-log=solver:smt2 -use-query-log=solver:pc

-write-pcs -write-smt2s -write-cov -search=dfs constraint_independent.o

int constraint_independent(int x, int y) {

int c = 0;

if (x == 0) c = x++; // B1

else c = x--; // B2

if (y < 0) c = y++; // B3

else c = y--; // B4

return c;

}

Before optimization, I can see the KLEE generate Path conditions in the

order that (from file "all-queries.smt2"):

query0: [B2]

query1: [B2,B4]

query2: [B2,B4,True]

query3: [B2,B3,True]

query4: [B1,B3]

query5: [B1,B3,True]

query6: [B1,B4,True]

after optimizations, I presume the queries to the solver would be like :

query0: [B2] // wrt. query0.

query1: [B4] // wrt. query2. B1/B2 and B3/B4 are independent

query2: [B3] // wrt. query3

query3: [B1] // wrt. query4

query4: [B3] // wrt. query5

query5: [B4] // wrt. query6

while the actual queries to the solver is (from file

"solver-queries.smt2"):

query0: [True]

query1: [B2]

query2: [B3]

query3: [B2,B3,True]

Is my presumption correct if only considering the constraint independent

and caching? If not, do I need some options to disable other

optimizations? Btw, is there some reason to introduce the "True" for some

PCs? I appreciate any suggestion and help highly.

Best regards,

Tianhai