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
