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 <[email protected]> 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.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
