Skip to content
master
Go to file
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
 
 
 
 
lib
 
 
pcf
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

README.md

Sturdy build-status

Sturdy Logo

Sturdy is a library to create sound static analyses in Haskell. Static analyses are tools that produce information about computer programs without actually running the program. Examples of static analyses are type checkers, bug finders (e.g. Java FindBugs), analyses for security (e.g. taint analyses), and analyses that are used for compiler optimizations.

This project focuses on sound static analyses. A static analysis is sound if the results of the analysis reflect the actual runtime behavior of the program and users can rely on the results. For example, if a static analysis used for compiler optimizations were unsound, the optimization might change the semantics of the program, which leads to unexpected behavior at runtime. To this end, Sturdy follows the theory of Compositional Soundness Proofs of Abstract Interpreters and Sound and Reusable Components for Abstract Interpretation to simplify soundness proofs of static analyses.

Sturdy Overview

Sturdy factorizes the concrete interpreter and abstract interpreter (the static analysis) into a generic interpreter. This generic interpreter is parameterized by interfaces that contain primitive operations that describe the semantics of the language, such as try, catch and finally for exceptions. The concrete and abstract interpreter then instantiate the generic interpreter by implementing these interfaces. This reorganization not only decouples different concerns in the implementation of the static analysis, but also simplifies its soundness proof. More details can be found in our ICFP paper.

Sturdy allows to construct static analyses modularly from reusable analysis components. Each analysis component encapsulates a single analysis concern and can be proven sound independently from the analysis where it is used. Furthermore, the theory of analysis components guarantees that a static analysis is sound, if all its analysis components are sound. This means that analysis developers do not have to worry about soundness as long as they reuse sound analysis components. More details can be found in our OOPSLA paper.

Getting Started

To build, install the Stack build tool and run stack build from the root directory of the project.

The sturdy project currently contains concrete and abstract and generic interpreters for the following languages:

  • PCF, a higher-order functional language
  • While, an imperative language with conditionals and while loops
  • Scheme, a functional language language in the LISP family.
  • Stratego, a language for program transformations
  • LambdaJS, an intermediate representation for JavaScript
  • Jimple, a Java Bytecode suitable for static analysis (work in progress)

To run the tests of a particular language use stack test sturdy-$(lang), e.g.,

stack test sturdy-pcf

Publications

Sound and Reusable Components for Abstract Interpretation
Sven Keidel and Sebastian Erdweg.
Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). ACM, 2019 [pdf] [Talk]

Compositional Soundness Proofs of Abstract Interpreters
Sven Keidel, Casper Bach Poulsen and Sebastian Erdweg.
International Conference on Functional Programming (ICFP). ACM, 2018 [pdf] [Talk]

A Systematic Approach to Abstract Interpretation of Program Transformations
Sven Keidel and Sebastian Erdweg.
Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 2020. [pdf]

Acknowledgments

I want to thank everyone that has contributed to this project (in alphabetical order):

Casper Bach Poulsen, Jente Hidskes, Matthijs Bijman, Sarah Müller, Sebastian Erdweg, Tobias Hombücher, Wouter Raateland

You can’t perform that action at this time.