[klee-dev] Constraints in SSA from

[Charitha Saumya]

Thanks a lot for your insights.

I appreciate if other can also share their views on this.

Charitha


On 11/15/2017 12:24 AM, Andrew Santosa wrote:
> Hi Charitha,
>
> Perhaps others can provide better answer, but I believe it will 
> involve significant
> effort to implement what you want in KLEE.
>
> Since you also asked for other approaches, I am reminded of work I did 
> years back
> on symbolic execution using constraint logic programs, which perhaps 
> is closer to
> what 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 with
> before-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 <mailto:klee-dev at imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev 
> <https://secure-web.cisco.com/1FTy6JKWYhsZVz-RCyACgn9g6sE0BqY7btP1OGRAgKIcpW82rNYTnJKs3WjWIskmpGfkqGvhmd3S_U1VkHf08iNacXX3LeG2spBB1YpR77zGjlwuj-dcwxOFT_BEIma6P8CnpSZtjCwG-SfTCM6uUY5hD97312PmQz1qAqaDqnvt4B9jP7-GX9eiIEa6rJ068c0BbxtLqRaPqE25vmfETi5r80HDNRl8MaNYas8DlKGjPOy7HGW0jFPwMkgugGo7JBJXbWrqAr6h7IcMRDUYorD98uQa0VKU_9CWHhCx3rZ9mD1IYZEkRBzb3v3ubgbMpA8l7tAt8oUfZ7nNUBuVMSkpPMkzcr-o2IAo5AWj25Lk/https%3A%2F%2Fmailman.ic.ac.uk%2Fmailman%2Flistinfo%2Fklee-dev>

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

-------------- next part --------------
HTML attachment scrubbed and removed