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

[Daniel Liew]

Perhaps you could do this. When running klee use the --write-pcs
option (there are similar options for SMT-LIBv2 as well) which will
write the constraints of a completely explored path for each test case
into the folder klee-last/

For example:
$ cat simple.c
int main()
{
  int a;
  klee_make_symbolic(&a,sizeof(a),"a");

  if(a > 10)
  {
     return 0;
  }
  else
  {
    return 1;
  }
}

$ llvm-gcc -emit-llvm -c simple.c
$ klee --write-pcs simple.o
...
$ cat klee-last/test000001.pc
array a[4] : w32 -> w8 = symbolic
(query [(Slt 10
             (ReadLSB w32 0 a))]
       false)

In the KQuery language the constraints are inside the square brackets.
Personally I don't like the KQuery language that much because it
queries for validity because I think querying for satisfiability is
easier to understand. The SMT-LIBv2 language works in terms of
satisfiability so you could use --write-smt2s instead. You would get
this instead for the example I have given.

(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (and (bvslt  (_ bv10 32) (concat  (select  a (_ bv3 32) )
(concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) )
(select  a (_ bv0 32) ) ) ) ) ) true ) )
(check-sat)
(exit)

Each (assert ...) statement is a constraint for the path explored.
That long concatenation expression is required because a is an array
of bytes so 4 elements need to be concatenated to make up an integer
on the architecture I'm using.

I think these are the constraints you are after. You probably need to
write some sort of parser that converts the constraints into a format
you can work with. You could use the kQuery parser in KLEE as a
starting point and write your own printer that takes the built Expr
tree and prints it out as you wish. However I think it would be better
for you to work with SMT-LIBv2 files though as more work has been done
with this format (for example there is a parser for it at
https://es.fbk.eu/people/griggio/misc/smtlib2parser.html ). You can
find more SMT-LIBv2 tools at http://www.smtlib.org/

Hope that help,

Regards,
Dan Liew.

On 11 April 2013 11:11, varza victor <victor.varza at gmail.com> wrote:
> Hi Liew,
>
> Thank you for answering me. I want to use it for a 'hybrid fuzzer'. In this
> way I use KLEE to find all paths from a given application. After this I use
> PPL (Parma Polyedra Library) to generate random input for the input space
> described by the constraints generated by KLEE. I saw that KLEEcan olny
> output the query for a constraint solver, not the constaints, so I'm looking
> for a slution to resolve my issue. I think that I have to implement a small
> application for this.
>
> Regards,
> Victor Varza
>
>
> 2013/4/11 Daniel Liew <daniel.liew at imperial.ac.uk>
>>
>> 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
>
>