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. query6while 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
all-queries.smt2
Description: Binary data
solver-queries.smt2
Description: Binary data
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
