[klee-dev] Transform cvc or pc queries into linear equation

[Daniel Liew]

Hi Varza,

I'm not aware of KLEE having this capability. Out of curiosity what do
you want to use it for?

This may not be useful to you but you can however convert .pc files
(kQuery language) into SMT-LIBv2 files. SMT-LIBv2 files are a more
"standard" format for SMT solvers which you might find more useful.

To do this run

$ kleaver --print-smtlib your-query.pc

The options
--smtlib-display-constants=
--smtlib-human-readable
--smtlib-use-let-expressions

may be useful to you when converting.

It is worth noting that the SMT logic used is the QF_ABV (Quantifier
free arrays of bitvectors) so every symbolic variable is actually
represented by an array of bitvectors. Constants are also represented
as bitvectors. Consequently you will not see syntax like "x <= 10"
anywhere. The SMT-LIBv2 syntax would be something like...

(set-logic QF_ABV )

#Declare a function x that takes no arguments and is of type (Array (_
BitVec 32) (_ BitVec 8) ) , the index is 32-bit and indexes bytes
#This is the symbolic variable
(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )

# check first byte in x is less than or equal to 10 (as 8-byte
unsigned integer) where both bitvectors are assumed to be unsigned
integers.
assert( (bvule (select x (_ bv0 32)) (_ bv10 8) ) )
(check-sat)

If you find the syntax confusing take a look the  The SMT-LIB v2
Language and Tools tutorial on http://www.smtlib.org/
Regards,
Dan Liew.

On 10 April 2013 21:13, varza victor <victor.varza at gmail.com> wrote:
> Hi,
>
> I'm new in KLEE and I have some cvc and pc queries generated by klee and I
> want to transform it into linear equations such as x <= 10; x >= 2. Can I do
> this using klee?
>
> Best regards,
> Victor