[klee-dev] More about all/solver-queries.smt2 files

[Andrea Aquino]

Dear all,

I analyzed the coreutils of the linux kernel using KLEE (llvm version 2.9 on host 1386-pc-linux-gnu (Ubuntu 32 bits)).

I configured KLEE to use both caches, to timeout after 1 minute, to produce no output and to log all queries in smt2 format to a file and the queries that reach the solver to another file. The complete command I used is the following one (used in a bash script where $1 represents the name of a given coreutils program).

klee --use-cache --use-cex-cache --no-output --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=$MAX_TIME. --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 ./$1.bc --sym-args 0 1 10 --sym-args 0 2 2 --sym-files 1 8 --sym-stdout &> /dev/null

What I found is that the formulas in the all-queries.smt2 file seem to be still sliceable (that is, they can be separated in many more independent subformulas (i.e., formulas that do not share variables)). Is this normal?

On a second thought, this might be due to the fact that the slicing procedure I implemented takes in input a formula and returns all of its subformulas that do not share variables, while KLEE slices a formula with respect to the last path condition on the branch the current formula belongs to. Is my intuition correct?

Given this I would like to understand clearly how the all-queries.smt2 and solver-queries.smt2 are populated (that is, the conditions that must hold for a formula to be logged in one file or the other and what is the relation between the formulas in these two files). I had a look at the code but it did not help.


Best regards,
Andrea Aquino