[analyzer] Documentation for ExprEngine?

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

[analyzer] Documentation for ExprEngine?

Leonard Chan via cfe-dev
Hello,

I have been looking through the static analyzer source code in an effort to better understand how it works and was wondering if there are any good resources on understanding the ExprEngine.

Specifically I am having some trouble understanding how statements inside of functions/loops/etc. are added to the worklist.

Thanks,
Brad

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [analyzer] Documentation for ExprEngine?

Leonard Chan via cfe-dev
CoreEngine and ExprEngine are pretty much a single entity; CoreEngine manages the worklist, while ExprEngine is a huge switch (aka visitor) over different kinds of program points it finds in the worklist that knows what to do on each of them.

Initially the program point that corresponds to "before the first statement" location of the top-level function we want to analyze, paired with the initial program state, is added to the worklist. CoreEngine takes this worklist item and realizes that he needs ExprEngine's help to model the actual statement. ExprEngine takes the item, adjusts the state of the program according to the effects of the statement, and puts zero or more "after that statement" items to the work list, paired with their respective updated program state. Then CoreEngine takes the new item, realizes that we're done with the respective statement, and looks up the CFG to see what the next statement (or a statementless CFGElement, such as a C++ automatic destructor call) is going to be. This goes on until the worklist is empty or we run out of budget and decide that the code is too complicated to analyze it further. The worklist itself is, since recently, a "priority stack" that puts unexplored statements in front of previously visited statements and works as a FIFO otherwise.

The above may be incorrect in detail, but that's the rough idea. I never really needed any deeper knowledge about that in years of working on the analyzer, so i'm kinda curious what sort of stuff you're trying to do.

In short, order of statements is controlled by the CFG, and you should be able to debug your problems by starting at CoreEngine::dispatchWorkItem().

On 4/12/18 5:37 PM, Brad S via cfe-dev wrote:
Hello,

I have been looking through the static analyzer source code in an effort to better understand how it works and was wondering if there are any good resources on understanding the ExprEngine.

Specifically I am having some trouble understanding how statements inside of functions/loops/etc. are added to the worklist.

Thanks,
Brad

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev