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.
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
Post by Daniel LiewHi 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.
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