[klee-dev] Constraints in SSA from

[Charitha Saumya]

Hi,

Can someone help me with this question. Thanks in advance!

Charitha


On 11/08/2017 10:21 PM, Charitha Saumya wrote:
> 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