[klee-dev] Constructing constraints

[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

On 15/01/14 06:38, 李永超 wrote:
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>