Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Easing Maintenance of Academic Static Analyzers

Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné

TL;DR

An automated way to measure precision that does not require any baseline of true bugs obtained by manually inspecting the results is described, and it improves transparency of the analysis, and helps discovering regressions during continuous integration.

Abstract

Academic research in static analysis produces software implementations. These implementations are time-consuming to develop and some need to be maintained in order to enable building further research upon the implementation. While necessary, these processes can be quickly challenging. This article documents the tools and techniques we have come up with to simplify the maintenance of Mopsa since 2017. Mopsa is a static analysis platform that aims at being sound. First, we describe an automated way to measure precision that does not require any baseline of true bugs obtained by manually inspecting the results. Further, it improves transparency of the analysis, and helps discovering regressions during continuous integration. Second, we have taken inspiration from standard tools observing the concrete execution of a program to design custom tools observing the abstract execution of the analyzed program itself, such as abstract debuggers and profilers. Finally, we report on some cases of automated testcase reduction.

Easing Maintenance of Academic Static Analyzers

TL;DR

An automated way to measure precision that does not require any baseline of true bugs obtained by manually inspecting the results is described, and it improves transparency of the analysis, and helps discovering regressions during continuous integration.

Abstract

Academic research in static analysis produces software implementations. These implementations are time-consuming to develop and some need to be maintained in order to enable building further research upon the implementation. While necessary, these processes can be quickly challenging. This article documents the tools and techniques we have come up with to simplify the maintenance of Mopsa since 2017. Mopsa is a static analysis platform that aims at being sound. First, we describe an automated way to measure precision that does not require any baseline of true bugs obtained by manually inspecting the results. Further, it improves transparency of the analysis, and helps discovering regressions during continuous integration. Second, we have taken inspiration from standard tools observing the concrete execution of a program to design custom tools observing the abstract execution of the analyzed program itself, such as abstract debuggers and profilers. Finally, we report on some cases of automated testcase reduction.
Paper Structure (30 sections, 1 equation, 8 figures, 4 tables)

This paper contains 30 sections, 1 equation, 8 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Contributions.
  3. An Overview of Mopsa
  4. Languages
  5. Precision
  6. Unified Signature.
  7. Configurations.
  8. Properties
  9. Measuring Precision
  10. Traditional Approaches to Measuring Precision
  11. Absolute precision: the case of manually annotated benchmarks.
  12. When no baseline exists: usual approaches to measuring precision.
  13. Reporting static analysis results in an automatic and transparent fashion
  14. Comparing analyses results using mopsa-diff
  15. Detecting breaking changes during continuous integration
  16. ...and 15 more sections

Figures (8)

  • Figure 1: High-level implementation change, to move from reporting alarms to a transparent report of alarms and successful checks.
  • Figure 2: Analysis report summary for the analysis of coreutilsfmt.
  • Figure 3: Illustrating selectivity computation on a toy C example.
  • Figure 4: Mopsa-diff output comparing the impact of different relational domains on some coreutils programs.
  • Figure 5: Flamegraph obtained using the abstract function profiling of Mopsa, when analyzing coreutilsfmt.
  • ...and 3 more figures