Introduction

Decidability

Christian Gram Kalhauge

Table of Contents

  1. Program Analysis
  2. The Kinds of Analysis
  3. Getting Started

Questions

  1. What makes program analysis hard?

  2. In what circumstances would you want a May vs a Must analysis?

  3. What does it mean that an analysis is sound?

Program Analysis (Β§1)

It all started with math.

What is a Program? (Β§1.1)

Program

A program is an object p∈L, from a language L, with a step function from machine state to machine state:

πšœπšπšŽπš™:LΓ—π’π­πšπ­πžβ†’π’π­πšπ­πž

Program Terms

  • Initial state s0βˆˆπ’π­πšπ­πž.

  • Trace, the sequence of states visited by a step function.

  • Running the program to completion.

What is Program Analysis? (Β§1.2)

Using automatic techniques to figure out facts about a computer program.

A Turing-Complete Mess (Β§1.3)

What is a turing complete language?

A language in which you can compute anything a (Turing) machine can compute.

Almost all real programming languages are Turing complete

It can...

  • fire the missiles,

  • not fire the missiles,

  • never terminate,

  • kill grandma, and worst of all

  • throw a null pointer exception!

The Halting problem (Β§1.4)

The halting problem

Given any program p∈L from the language L, decide if it is going to terminate (halt) when executed on a state s0.

E.g ., does there exist a sequence, which eventually stabilizes: s1=πšœπšπšŽπš™(p,s0), s2=πšœπšπšŽπš™(p,s1), ..., sn=πšœπšπšŽπš™(p,snβˆ’1), sn=πšœπšπšŽπš™(p,sn)

Do these programs halt?

def forever():
  while True:
    print("Running!")
def never():
  while False:
    print("Running!")

A harder one

def does_halt(p : Program) -> bool:
    # A program returns true if p halts
def main():
    while does_halt(main):
        print("Running")

Wait! That's illegal!

General Undecidability of Program Analysis (Β§1.5)

def main():
    something_that_might_go_forever()
    fire_the_nukes()

Rice's Theorem

This means... that there is no best solution.

Welcome to Art School.

Sound or Complete... Choose one. (Β§1.6)

Not all that glitters is gold

  • (Glitters) Provable: Σ⊒Φ

  • (Gold) Truth: Σ⊨Φ

Soundness

In a sound system, we can only prove true things. Or, if we can prove Φ given Σ (Σ⊒Φ), then Φ is true given Σ (Σ⊨Φ). Σ⊒Φ⟹Σ⊨Φ

Completeness

In a complete system, we can prove all true things. Or if Φ is true given Σ (Σ⊨Φ) then Φ is provable given Σ (Σ⊒Φ).

Σ⊨Φ⟹Σ⊒Φ

FP,TN,FN vs TP

An individual proposition Ξ¦ is either a true positive, true negative, false positive, or false negative, following the table below:

Σ⊨ΦΣ⊭Φ
Σ⊒ΦTPFP
Σ⋣ΦFNTN

A Note: Soundness Confusion (Β§1.6.1)

Program based questions, soundness and completeness. The solid blob is the set of good programs. The dashed line is the set of programs accepted by the analysis.

Trace based questions, soundness and completeness.

May and Must Analyses (Β§1.6.2)

  • May Analaysis Overapproximate all traces (No False Positives).

  • Must Analysis Underapproximate all traces (No False Negatives).

A Relaxed Goal (Β§1.7)

[...], virtually all published wholeprogram analyses are unsound and omit conservative handling of common language features when applied to real programming languages.

β€” In Defense of Soundiness: A Manifesto

Confidence not Absolutes

The Kinds of Analysis (Β§2)

Manual vs Automatic Analysis (Β§2.1)

Syntactic vs Semantic Analysis (Β§2.2)

Dynamic vs Static Analysis (Β§2.3)

Getting Started (Β§3)

The JPAMB (Β§3.1)

  • Write an analysis that given the name of a JVM method, predict the possible behaviors.

  • Evaluate it on the JPAMB suite.

  • Upload your results to AutoLab (link next week).

The Key Idea (Β§3.2)

@Case("(false) -> assertion error")
@Case("(true) -> ok")
public static void assertBoolean(boolean shouldFail) {
    assert shouldFail;
}
assertion error;100% # I'm totally sure this happens
ok;100%
<the-others>;0% # I'm totally sure this never happens.

Categories

assertion error;yes # I think this happens
ok;maybe # This might happen, I don't know
<the-others>;no # I think this does not happen

Questions

  1. What makes program analysis hard?

  2. In what circumstances would you want a May vs a Must analysis?

  3. What does it mean that an analysis is sound?