[klee-dev] Constraints in SSA from

[Andrew Santosa]

Hi Charitha,
Perhaps others can provide better answer, but I believe it will involve significanteffort to implement what you want in KLEE.
Since you also asked for other approaches, I am reminded of work I did years backon symbolic execution using constraint logic programs, which perhaps is closer towhat you want. Some works in this area include the following:
Flanagan: "Automatic Software Model Checking using CLP", ESOP '03.
Delzanno and Podelski, "Model Checking in CLP", TACAS '99.
As you can see in those works, statements (state transitions) are translated into CLP rules withbefore-transition and after-transition symbolic variables.
 
Regards,Andrew
    On Monday, 13 November 2017, 10:41:34 am GMT+8, Charitha Saumya <cgusthin at purdue.edu> wrote:  
 
 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


_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
  
-------------- next part --------------
HTML attachment scrubbed and removed