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

[Dan Liew]

Hi,

On 12 May 2015 at 14:50, Andrea Aquino <andrex.aquino at gmail.com> wrote:
> 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?

I think so. I remember this being reported on this list a while ago.

> 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?

AFAICT

> 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.

The relevant code is in ConstructSolverChain.cpp [1]. This constructs
a chain of ``SolverImpl`` objects that essentially form a pipeline for
solving queries. The "all queries" is at the beginning of the pipeline
and thus logs every single query sent to it by the Executor.

The "solver queries" are at the other end of the pipeline once the
queries have passed through the other ``SolverImpl`` objects. So this
records the actual queries sent to the underlying SMT solver (i.e. STP
by default). Note that the other ``SolverImpl`` objects in the chain
may change the query (e.g. IndependenceSolver) or prevent it from even
reaching the underlying SMT solver (e.g. CexCache).


[1] https://github.com/klee/klee/blob/master/lib/Basic/ConstructSolverChain.cpp


Hope that helps.

Dan.