Constructing constraints

[李永超]

Hi,
I am reading KLEE source code recently to add some functionality to it.
Now I am confused about the constructing of constraints. As far as I know about
KLEE implementation, constraints are essentially represented by Expr. But this
is still not clear enough, say, consider I want to represent a constraint like
'buf[i] != 0', where buf is an array of char and i is an integer. How should I construct
an Expr so that I can add this constraint to current path constraints?


Thanks,
Yongchao.

[Paul Marinescu]

You can break this down into two steps:
1. Figure out what the Expr for your constraint looks like
2. Figure out how to build that constraint

For 1, the easiest thing is to create a simple program that uses
klee_print_expr on your expression then run the program through klee.
For example

int main() {
int i = 0;
char buf[10];
klee_make_symbolic(&buf, sizeof(buf), "buf");

klee_print_expr("buf[i] != 0", buf[i] != 0);

return 0;
}

prints
buf[i] != 0:(ZExt w32 (Eq false
(Eq 0 (Read w8 0 buf))))

if you also make i symbolic you get
buf[i] != 0:(ZExt w32 (Eq false
(Eq 0
(Read w8 (Extract w32 0 (SExt w64 (ReadLSB w32 0 i)))
buf))))

For 2, there's no quick solution, just farmiliarize yourself with the
Expr API. include/klee/Expr.h is a good starting point

Paul

Post by 李永超
Hi,
I am reading KLEE source code recently to add some functionality to it.
Now I am confused about the constructing of constraints. As far as I know about
KLEE implementation, constraints are essentially represented by /Expr/.
But this
is still not clear enough, say, consider I want to represent a
constraint like
/'buf[i] != 0'/, where /buf/ is an array of char and /i/ is an integer.
How should I construct
an /Expr/ so that I can add this constraint to current path constraints?
Thanks,
Yongchao.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev