Fully Declarative Specification of Static Code Checkers

Static code checkers are tools that help software engineers by automatically finding defects without executing the programs. These tools contain a set of detectors that rely on static program analyses to find common programming defects or to enforce coding guidelines.

While existing code checker frameworks package a rich collection of detectors, aimed at common bug defects, the effort to adapt these detectors to specific project needs is not trivial. In their definition, the detectors rely on checker-specific program representations and auxiliary data structures, which incurs a high up-front cost for customization attempts. Being encoded in a general-purpose programming language, the detectors inherit the evaluation model of the host programming language. This precludes the adoption of evaluation schemes that fit the dynamics of the project, such as incremental evaluation or caching of partial results.

In this thesis we address the hindrances to adaptability in current checker frameworks by combining two declarative techniques: syntactic pattern matching and logic programming in Datalog. We use syntactic pattern matching to identify the program fragments that are of interest for a detector and Datalog logical rules to enable non-local reasoning between these fragments of interest. Syntactic patterns allow us to decouple the detector specification from the internal representations of programs, while the use of Datalog-style rules enables the adoption of alternative evaluation modes, such as incremental evaluation.

We materialize our techniques in declarative specification languages and runtimes that facilitate the construction of declarative static code checking frameworks for the C and Java languages. We show that these declarative specification languages enable concise description of bug detectors, while achieving analysis quality and runtime performance that is comparable with established frameworks.