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
<[email protected]> 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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
