[klee-dev] Adding assignments to state constraints

[felicia]

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.

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.

Thank you.

On 2015-11-04 16:50, Kuchta, Tomasz wrote:
> Hi Felicia,
> 
> Why would you like to add assignments to the constraints?
> What do you want to achieve?
> In your example, if ‘x' is later on present in a branch condition,
> e.g. if (x < 5) , the symbolic expression that you quote
> will be incorporated in the condition instead of ‘x’. As a result you
> should end up with having something like
> (Add w32 1 (ReadLSB w32 0 x)) < 5 added to your constraint set (on the
> “then” side of the branch).
> 
> Kind regards,
> 
> Tomek
> 
> 
>> On 4 Nov 2015, at 08:18, felicia <felicia at comp.nus.edu.sg> wrote:
>> 
>> Hi,
>> 
>> I would like to ask on how to collect assignments in the state's 
>> constraints.
>> Because currently KLEE only collect the constraints at the branch 
>> condition.
>> I have tried to add the assignment expression in the state 
>> constraints.
>> For example, x = x + 1 has assignment expression like this (Add w32 1 
>> (ReadLSB w32 0 x)).
>> Then, I add (Add w32 1 (ReadLSB w32 0 x)) at state constraints.
>> However, this way always give me an assertion error.Please let me know 
>> if you have any suggestion regarding this.
>> 
>> Thank you.
>> 
>> 
>> 
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev