[klee-dev] KLEE without SMT solver

[Martin Nowack]

Hi,
> On 11 Sep 2015, at 23:12, Jeff Wilson <jeffwilson1369 at gmail.com> wrote:
> 
> Is there a way to disable the queries that KLEE makes to the SMT solver? I would like to only get the path constraints in SMT2 format as outputs from KLEE.
> 
In general, if you want to generate SMT2 output use following arguments (-use-query-log):
 =all:smt2 to get all solver queries (i.e. every call, before any optimisations, caches, …) and/or
 =solver:smt2 to get queries which reach the real solver (e.g. the ones which could not be solved using caches, …)

As an example:
klee -use-query-log=all:smith,solver:smt2 foobar.bc

Now, even you would like to get the path constraints only, you still need to invoke the solver
to progress a state (i.e. should KLEE fork a state on a conditional branch instruction, which path is valid?).

Maybe a hacky work around:
* add a global flag in KLEE which you can toggle on/off before and after a state fork (https://github.com/klee/klee/blob/master/lib/Core/Executor.cpp#L703)
* in the QueryLoggignSolver::flushBuffer  (https://github.com/klee/klee/blob/master/lib/Solver/QueryLoggingSolver.cpp#L76)
  check for that flag and flush in that case

This way, only queries for path constraints get logged.

HTH.

Cheers,
Martin
---------------------------------------------------
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150914/7bc805a8/attachment.sig>