Search code examples
kleesymbolic-execution

Why IR is needed for symbolic execution?

For example, KLEE works on LLVM bitcode.

Can we build symbolic execution directly on C source code?

Solution

  • Each LLVM IR contains only one simple operation, but one C statement could contains multiple operations. For example, a[i] = b[i]; could be split into:

    addr = b + i; // getElementPtr instruction
tmp = *addr; // load instruction
addr1 = a + i; // getElementPtr instruction
*addr1 = tmp; // store instruction

    So it's much more simple to process LLVM IR than source code for a symbolic executor.