[klee-dev] Constraint independent and caching

[Tianhai Liu]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: all-queries.smt2
Type: application/octet-stream
Size: 5487 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140708/7e05384e/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: solver-queries.smt2
Type: application/octet-stream
Size: 2322 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140708/7e05384e/attachment-0001.obj>