Towards Declarative Specification of Static Analysis for Programming Tools

Static program analysis plays a crucial role in ensuring the quality and security of software applications by detecting bugs and potential vulnerabilities in the code. Traditionally, these analyses are performed offline, either as part of the continuous integration/continuous deployment pipeline or overnight on the entire repository. However, this delayed feedback disrupts developer productivity, requiring context switches and adding overhead to the development process. Integrating these analysis results directly into the integrated development environment (IDE), similar to how type errors or code smells are reported, would enhance the development process. As developers increasingly rely on IDEs for real-time feedback, the efficiency and responsiveness of these tools have become critical. In such settings, developers expect immediate and precise results as they write and modify code, making it particularly challenging to achieve response times sufficiently low to not interrupt the thought process.
This thesis addresses these challenges by investigating the design and implementation of control-flow and dataflow analyses using the declarative Reference Attribute Grammars formalism. This formalism provides a high-level programming approach that enhances expressivity and modularity, making it easier to develop and maintain analyses.
Central to this thesis is the development of IntraCFG, a language-agnostic framework designed to perform control-flow and dataflow analyses directly on source code rather than relying on intermediate representations. By superimposing control-flow graphs onto the abstract syntax tree, IntraCFG removes the need for intermediate representations that are often lossy and expensive to generate. This approach allows for the construction of efficient but still precise dataflow analysis.
We demonstrate the effectiveness of IntraCFG through two case studies: IntraJ and IntraTeal. These case studies showcase the potential and flexibility of IntraCFG in diverse contexts, such as bug detection and education. IntraJ supports the Java programming language, while IntraTeal is a tool designed for teaching program analysis for the educational language Teal. IntraJ has proven to be faster than, and as precise as, well-known industrial tools.
Additionally, this thesis introduces a new algorithm for the demand-driven evaluation of fixed-point (i.e., circular) attributes, which has proven essential for the performance of dataflow analyses in IntraJ. This improvement allows IntraJ to achieve response times below 0.1 seconds, making it suitable for use in interactive development environments.