[klee-dev] Path constraints as equations of integers

[Dan Liew]

Hi,

On 1 November 2016 at 12:17, Papapanagiotakis-Bousy, Iason
<iason.papapanagiotakis-bousy.15 at ucl.ac.uk> wrote:
> Hello,
>
>
>
> I am a new user of KLEE, I was looking into symbolic execution in order to
> extract the constraints of the input variables of a program for each path in
> the code.
>
> Following the initial tutorials and searching on the web I’ve managed to get
> both the KQuery and SMT2 formatted constraints generated by KLEE.
>
>
>
> I was wondering if there is a (new) capability of KLEE or an available
> script/tool to generate the constraints as a systems of equations of
> integers and not Bit Vectors as the default output in KQuery and SMT2 is.

There is no option for this. KLEE analyses programs precisely so it
has no use for printing
expressions in an approximate form (i.e. using integers).

You of course could do this yourself by either modifying KLEE's
ExprSMTLIBPrinter class
to print KLEE's expressions differently or write your own tool to
parse QF_ABV queries
and rewrite them as AUFNIRA queries.

I don't know if there any existing tools to rewrite QF_ABV constraints
to AUFNIRA.

> While the output generated works fine with SMT solvers for the main purpose
> of KLEE, it would help a lot if constraints could also be presented in a
> human-friendly way.

KLEE does have a few options to make the printed SMT-LIBv2 queries
slightly easier
to read (`-smtlib-human-readable`, `-smtlib-abbreviation-mode`,
`-smtlib-display-constants`).
These might help you.

Thanks,
Dan.