[klee-dev] On KLEE's ability to perform formula-slicing

[Andrea Aquino]

Dear all,

I succeeded in extracting the formulas generated by KLEE during the analysis of the coreutils tools. I am currently running KLEE (llvm version 2.9) on a Ubuntu-linux 32 bit virtual machine setting a timeout of 60 seconds with the following command:

klee --use-cache=false —use-cex-cache=false —use-query-log=all:smt2 —use-query-log=solver:smt2 --simplify-sym-indices --write-cvcs --write-cov --output-module --max-memory=1000 --disable-inlining --optimize --use-forked-solver --libc=uclibc --posix-runtime --allow-external-sym-calls --only-output-states-covering-new --environ=test.env --run-in=/tmp/sandbox --max-sym-array-size=4096 --max-instruction-time=30. --max-time=60. --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal --randomize-fork --search=random-path --search=nurs:covnew --use-batching-search --batch-instructions=10000 ./PROGRAM.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout

Everything is ok and several thousands of formulas are generated. Having disabled both the standard cache and the counter-example cache, the number of formulas in the logged files (all-formulas and solver-formulas) are the same.

Now I was trying to slice these formulas with my own procedure. Basically I am separating every formula into the set of its independent subformulas (i.e. subformulas that do not share any variable). To do so I create a graph consisting of a node for each clause in the original formula, then I connect the nodes representing two clauses iff they have at least a variable in common, finally I extract the connected components of the graph.

As far as I know, KLEE does this too (at least to some extent, that is using path condition slicing), that is why I was assuming my slicing procedure not to be able to slice any formula generated during the abovementioned analysis. Suprisingly, I found some formulas that was actually sliceable. 

I attach to this email a formula “sliceable.smt2” that my tool can slice in 9 independent subformulas. This formula belongs to the analysis of the coreutil program [.bc (test).
I manually double-checked it and it seems the formula can indeed be sliced into 9 subformulas (composed of a single variable each). Notice that even if the formula defines 12 variables only 9 of them are actually used in its assertion.

My questions are the followings: 

is it normal that KLEE generates formulas that are sliceable even if it performs formulas slicing? 

am I doing some mistake in the slicing of this formula or is it indeed sliceable in 9 subformulas? 

am I missing some flag to enable the slicing capability of KLEE?


Best regards,
Andrea Aquino

-------------- next part --------------
A non-text attachment was scrubbed...
Name: sliceable.smt2
Type: application/octet-stream
Size: 11765 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150302/7b9cb620/attachment.obj>