[klee-dev] All possible paths from source to destination function.

[Sailesh Sai Teja]

Hello all,

I am performing static analysis on a codebase and for that I am trying to
find all the possible paths from function 'A' to function 'B' along with
the conditions that are responsible while traversing that path. My input is
a large llvm IR file which contains all the functions definitions.

So if we consider the below toy example :-

int functionA(int a) {
if (a > 0) {
return functionB(20, 50);
}
else {
return functionC(100, 500);
}
}

int functionB(int x, int y) {
if(x > y){
return multiply(x, y);
}
else {
return divide(y, x);
}
}

int functionC(int x, int y) {
if(y > 0){
return divide(x, y);
}
else {
return multiply(y, x);
}
}

int multiply(int a, int b){
return a*b;
}

int divide(int x, int y){
return x/y;
}

So lets say I want to trace the execution path from function "functionA" to
function "divide", the following is the output I am expecting

1. "functionA && ((x < y) && divide)"
2. "functionA && ((y > 0) && divide)"

or it can be combined as "functionA && ((x < y) || (y > 0)) && divide"

I just want to know whether klee is capable of performing such analysis
(not exact as I knew I need to modify few things to arrive at the final
solution but you get the gist). If yes, can you please provide some
references and resources that I can look into.

Thank you.
-------------- next part --------------
HTML attachment scrubbed and removed