Hi, On 12 May 2015 at 14:50, Andrea Aquino <[email protected]> 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. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
