Obtain symbolic values of some variables backward from some path-sensitive callback

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

Obtain symbolic values of some variables backward from some path-sensitive callback

Kristof Beyls via cfe-dev
Hello!  Need some help. 
How can I get symbolic values of some variables in function with memory copy loop. Exactly, I need symbolic values of variables in loop control expression, parent functions arguments, caller functions arguments, etc. i.e. some type of backward-analysis? 

As I understood I must use checkEndAnalysis callback and then iterate over ExplodedGraph nodes again and again and again. Does simpler way exist?

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

Re: Obtain symbolic values of some variables backward from some path-sensitive callback

Kristof Beyls via cfe-dev
Your question isn't well-defined because symbolic values of variables may change over time. Eg., the loop counter may be incremented and it'll have a different symbolic value before and after the increment. Additionally, the values may be different on different execution paths. You should specify which moment of time is of interest to you. Which most likely points you to the checker callback that fires at that exact moment of time, in which the values of the variables are immediately accessible.

If you want to compare the values in different moments of time across the same execution path, you can keep track of the previous values in the program state, so that they were also available when you're looking at the updated values - that's the intended programming model within the Static Analyzer.

If you want to compare the values in different execution paths, you have no choice but to use checkEndAnalysis. You can still save the necessary information in the program state, so that you only needed to iterate through the leaf nodes. But for that kind of analysis you need to always keep in mind that the Analyzer does not necessarily explore all execution paths, and there's no easy way to figure out if it did explore all execution paths during a specific analysis or not. If your analysis relies on gathering information about all execution paths, you're using the wrong tool: you should implement a custom data flow analysis over the Clang CFG instead.

Also note that iterating over the ExplodedGraph in checkEndAnalysis is fine as long as the number of visits is O(the number of nodes in the graph) - you'll still most likely be faster than the construction of the ExplodedGraph.

On 9/17/19 9:58 AM, Алексеев Кирилл via cfe-dev wrote:
Hello!  Need some help. 
How can I get symbolic values of some variables in function with memory copy loop. Exactly, I need symbolic values of variables in loop control expression, parent functions arguments, caller functions arguments, etc. i.e. some type of backward-analysis? 

As I understood I must use checkEndAnalysis callback and then iterate over ExplodedGraph nodes again and again and again. Does simpler way exist?

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


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