[klee-dev] Adding assignments to state constraints

[Dan Liew]

Hi,

On 4 November 2015 at 09:11, felicia <felicia at comp.nus.edu.sg> wrote:
> Hi Tomek,
>
> The purpose I am doing this, is because I would like to ask the solver even
> at the point before x is used in the branch condition.

I don't understand what you mean. If you ask the solver if (x <= 0) is
satisfiable before executing the (x <=0) branch and the input x was
not constrained then of course (x <= 0) will be satisfiable.

> For example, in this code:
> int add(int p1, int p2, int p3, int x) {
>   if(x <= 0){
>           if(p1 > 8) x = x;
>                 else x = x + 1;
>           if(p2 > 8) x = x;
>                 else x = x + 2;
>
>           assert(x <= 3);
>   }
>   return x;
> }
>
> In this case, the code has 3 branches condition (p1 > 8), (p2 >8) and the
> assertion (x <= 3).
> Since KLEE normally do the FALSE condition first, it will execute (p1 <= 8)
> and it will do the addition (x + 1). At the second branch (p2 > 8), for
> example, I need to ask the solver whether x <= 0 by using
> solver->evaluate(current constraint, x <= 0, result) . Since the current
> constraints are only x <= 0 and p1<=8, the solver would say it is
> satisfiable (although it's actually not). Therefore, I would like to add
> constraint x + 1 at this point, so the solver aware about this.

I think talking about the constraints at the C level might be
confusing things. At the LLVM IR level the code is SSA form so once a
register is assigned to is never changed. There will be different
registers corresponding to different versions of "x" in the IR.  So I
don't think you need to add "assignment constraints" at all. You just
need to ask if latest version of "x" if <= 0.

Besides a constraint "x == x +1" is always false. The constraint you
give " (Add w32 1 (ReadLSB w32 0 x))" is also wrong. A constraint must
be expression of boolean type, "x + 1" does not give a boolean type.

Dan.