[klee-dev] Adding assignments to state constraints

[Kuchta, Tomasz]

Hi Felicia,

Please correct me if I’m wrong: my understanding of your question is that we first added a constraint 
(x <= 0) and then changed x so you were not sure if the constraint still holds - is that correct?

If that is the question, then I believe KLEE should already handle the situation and you don’t need to ask the solver.
In principle, constraints should hold on an execution path if the path is feasible.

In general, if we consider a concrete execution, we could have a situation in the code 
where first x == 0, so we enter the fist condition if (x <= 0), then we increment x and that would still be a valid execution path.
// x == 0

if (x <= 0) {
  if (p < 5) {
   x++; // now x is 1, but we are on a valid execution path
  }
  foo(x);
  ...
}

Please let me know if I misunderstood you.
Kind regards,
Tomek

> On 4 Nov 2015, at 10:41, felicia <felicia at comp.nus.edu.sg> wrote:
> 
> 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.
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 6039 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20151104/5a802c07/attachment.bin>