Iterative full-program analysis (Abstract interpretation ?)


Just want to post something :slightly_smiling_face:

Years ago, I was fascinated by Microsoft announcement here:

“Our Python Language Server uses iterative full-program analysis to track the types of all the variables in your project while simulating execution of all the code in your project. Normally this kind of approach can take hours for complex programs and require unlimited amounts of RAM, but we have used many tricks to make it complete quickly enough for IntelliSense use.”

I keep researching for more information on this approach. My question on stackoverflow hint that the technique is also called Abstract interpretation.

Does anybody has more information on this ?
Beside PTVS, is there any other language analyzer use this technique ?


Abstract interpretation is one way of doing static program analysis. Usually, abstract interpreters are designed to be sound, that is they make no false promises. For example, if the abstract interpreter says variable x has type int, then it will never contain a value of another type. If x might also contain string values, the abstract interpreter has to over-approximate the type, for example by int|string or any.

That being said, I’d be surprised if the Python language server would try to be sound. In particular, if they want the analysis to complete quickly they must either (i) drop soundness to make heuristic choices or (ii) loose precision by inferring any many times. I guess they opted for option (i).

If you want to learn more about abstract interpretation, you might find our Sturdy project interesting. In Sturdy, abstract interpreters look like regular interpreters: a recursive function that operates by pattern matching and case distinction. Sturdy is language-agnostic yet provides analysis components from which you can assemble a static analysis for your language. Note: Sturdy is a research project.

Paper Compositional Soundness Proofs of Abstract Interpreters
Paper Sound and Reusable Components for Abstract Interpretation