[klee-dev] Constraints in SSA from

[Charitha Saumya]

Hi,

Is it possible to hack KLEE to get the constraints in static single 
assignment(SSA) form. In other words I want the constraints to closely 
resemble what the input program is doing.

Consider the following example.


int a,b;
klee_make_symbolic(&a, sizeof(a), "a");

b = a+1;
if(b>5){
     b = b+10;
     if(b>20){
         assert(false); // crash
     }
}

Consider the path leads to an assertion failure.

Currently KLEE path condition will be in terms of ONLY the symbolic 
input variables.

(a+1>5) ^ (a+11 > 20)

I want the variable "b" (which is an indirect symbolic variable) to also 
appear in my constraint as follows,

(b0 == a0+1) ^ (b0 > 5)^(b1 == b0+10)^(b1>20)

Note that I denoted a variable as "[name][digit]" where digit 
corresponds to most recent version of the variable (to be consistent 
with SSA form).

One of the ways I think would work is to keep a version number for each 
memory location and update it accordingly whenever memory write occurs. 
I would like to have some feedback on how difficult would be to 
implement this on KLEE? And what are the other ways (if any) to do this?

Thanks in advance,
Charitha Saumya


-- 
Charitha Saumya
PhD Student
School of Electrical and Computer Engineering
Purdue University