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
<cgust...@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@imperial.ac.uk <mailto:klee-dev@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
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
