Re: [klee-dev] Mapping Path Constraint to the Actual Path in Source Code

[Cristian Cadar]

Hi,

KLEE does not provide this information, although you could add such 
metadata when adding a new constraint.  However, because constraint 
solving optimisations could combine constraints, obtaining the origin of 
a constraint might not be possible in the general case.


Best,
Cristian

On 25/01/2024 04:07, Bohan wrote:


收件人:klee-dev@imperial.ac.uk 
周三 2024/1/24 19:18

Hi,

I am new to Klee. I have a question about how to determine which path 
constraints generated in the KQuery file correspond to specific paths or 
lines of code in the original source code or in the IR?


For example; I have a dummy c code that have 3 path,

#include  #include  int main() {     int num; 
int a = 10;     // Make 'num' a symbolic variable 
klee_make_symbolic(, sizeof(num), "num");     if (num > a + 3) { 
     printf("branch 0.\n");     } else if (num < a) { 
printf("branch 1.\n");     } else {         printf("branch 2.\n");     } 
     return 0; }


And here is the Kquery file for a ktest file where the num = 2147483647, 
and it goes to branch 0.


|array num[4] : w32 -> w8 = symbolic (query [(Slt 13   
(ReadLSB w32 0 num))]         false) |


My question is there any info from Klee that tells this query is for the 
branch 0.


Thank you very much for help!


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] Mapping Path Constraint to the Actual Path in Source Code

[Bohan]

收件人:klee-dev@imperial.ac.uk
周三 2024/1/24 19:18

Hi,

I am new to Klee. I have a question about how to determine which path
constraints generated in the KQuery file correspond to specific paths or
lines of code in the original source code or in the IR?

For example; I have a dummy c code that have 3 path,

#include 
#include 

int main() {
int num;
int a = 10;

// Make 'num' a symbolic variable
klee_make_symbolic(, sizeof(num), "num");

if (num > a + 3) {
printf("branch 0.\n");
} else if (num < a) {
printf("branch 1.\n");
} else {
printf("branch 2.\n");
}

return 0;
}

And here is the Kquery file for a ktest file where the num = 2147483647,
and it goes to branch 0.

array num[4] : w32 -> w8 = symbolic
(query [(Slt 13
  (ReadLSB w32 0 num))]
false)

My question is there any info from Klee that tells this query is for the
branch 0.

Thank you very much for help!
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev