[cfe-dev] Symbolic Execution Path Order Problem

[Anna Zaks via cfe-dev]

> On Dec 7, 2015, at 2:01 PM, Pengfei Wang via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Hello,
> 
> 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);
> 
>     free(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.
> 
How are you examining the execution order? The best way of finding out what the graph looks like and what caused the splits is by dumping the ExplodedGraph as described in http://clang-analyzer.llvm.org/checker_dev_manual.html#testing <http://clang-analyzer.llvm.org/checker_dev_manual.html#testing>.

> Is branch the only point that create a new path in the symbolic execution, or something else can also does the same thing?
> 
There are various reasons for splitting. For example, checkers could create 2 successor states. Said that we try to keep the number of splits to the minimum.
> 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!
> 
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20151207/7aff8006/attachment.html>