Scaladays '15: Yoyak

Yoyak: Static data analysis

Author is a programming language theorist.

Abstract interpretation

Static Analysis

The result of abstract interpretation is inaccurate, but not incorrect. Roughly, but soundly execute the program.

Methods used

• symbolic execution
• data flow analysis
• syntactic analysis
• model checking, abstract interpretatio, type system

Soundness

• The analysis result should contain all possibilities which can happen in the runtime
• if the analysis uses an over-approximation, it is sound

Complemeteness

• The analysis result should not contain any possibility which cannot happen at runtime

Semantics

• Over-approximation semantics is a superset of
• program semantics is a superset of
• approximation semantics

Illustrating Semantics with several tiny languages called Javar.

Key Elements of Abstract Interpretation

• Domain
• Semantics
• Galois Connection: pair of functions: abstraction and concretination function
• CPO: three constraints: there exists a partial order…Lattice of Interval Domain…
• Continuous function: a function is continuous when it reserves the upper bounds

Concrete and Abstract Semantics are connected with a Galois connection.

Yoyak enables to reuse components

• CFG data types: construction, optimizatoin visualization
• Graph algorithms
• Intermediate language data types
• common abstract domains
• comman abstract semantics

It’s perfect to be a framework: The theory of abstract interpretation guarantees soundness and termination of the analysis if a user supplies valid operators.

Yoyak Components

• Abstract Domain
• Fixed-point Computation (using a work-list algorithm)
• Built-in Standard Object Model

Slides

What’s IL?

Discussion, links, and tweets

I care about lots other interesting things as well. Follow me on Twitter to get an impression of that. Or contact me directly on another channel or come along to visit me.

Tweet Follow @abstractourism