[cfe-dev] Symbolic Execution Path Order Problem

Pengfei Wang via cfe-dev cfe-dev at lists.llvm.org
Mon Dec 7 14:01:16 PST 2015


I am writing  a checker for the static analyzer with the following simple
test case:

void kernel_func(MSG *uptr){

    char * localbuffer =(char*) malloc(uptr->msglength);

    if (localbuffer != NULL) {

        memcpy(localbuffer, uptr->msg, uptr->msglength);


    printf("Kernel() Copied msg is %s\n", localbuffer);



In my opinion, there should be only two execution paths for the
path-sensitive symbolic execution, for the reason that there is only one
branch in the program. One execution steps into the IF statement, while the
other one not. However, the test results shows a much longer execution
trace. The forepart of the execution trace is similar to what I said above,
two paths, but the rest doesn't make any sense to me. It repeated executing
some part of the program that have already executed before, and not all the
repeated process starts from a branch, some even start from the beginning
of the program but without the taints I made before, which should be added
if execute the program from the start point.

I am not sure what happens, but I kinda feel like some sort of backward
order happens in the execution. Is branch the only point that create a new
path in the symbolic execution, or something else can also does the same

Can anyone tell me why this happen? Do I miss something or misunderstanding
how the path-sensitive symbolic execution works?  I'll be very appreciate
for any answers. Thank you!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20151207/777b1185/attachment.html>

More information about the cfe-dev mailing list