[klee-dev] Adding assignments to state constraints

[felicia]

Hi Dan,

In this case, at the very first time x was constrained x <= 0 and then
it is added with x + 1, and then asking the solver whether x <= 0 (at 
the point when x is already through addition operation, but still not 
used for branching). However, It produces Solver::True because it still 
does not aware of the latest version of x.

Thank you for explaining the idea in LLVM program.
Is it possible to update the constraint with the latest version of x in 
C program?

I also have tried to convert the addition expression into boolean type 
before added into the constraint by using equality expression.

  ref<Expr> result = EqExpr::create(left, AddExpr::create(left, right));
  state.addConstraint(result);

However, I got assertion error like this:
Assertion `a && "computeValidity() must have assignment"' failed

Thank you.
-Felicia


On 2015-11-04 17:40, Dan Liew wrote:
> 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.