Introduction

Decidability

Christian Gram Kalhauge

Table of Contents

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

Questions

  1. Is program analysis easy?

  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 structured object p∈L, from a language L, with a step function from state to state:

𝚜𝚝𝚎𝚙:𝐒𝐭𝐚𝐭𝐞→𝐒𝐭𝐚𝐭𝐞

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 s.

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:
    ...
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)

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)

Language L Incomplete INCOMPLETE Unsound UNSOUND False Negative False Negative False Positive False Positive

Program based questions, soundness and completeness

Execution Incomplete INCOMPLETE Unsound UNSOUND Danger Zone Analysis False Negative False Negative False Positive False Positive Program Execution

Trace based questions, soundness and completeness

In case of confusion, use may and must instead.

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

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 Game (§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 ???.

$> ./your-analysis "info"
<please-dump-info>
$> ./your-analysis "jpamb.cases.Simple.assertPositive:(I)V"
assertion error;<probability of error>
import jpamb

methodid = jpamb.getmethodid("test", "0.0", 
    "The Rice Theorem Cookers", [], 
    for_science=True)

print("assertion error;80%")
print("ok;5")
print("*;-10")
print("divide by zero;10%")
print("out of bounds;0%")

Test it like so:

$> uvx jpamb test python ./guess.py 
... test output ...

And evaluate it like so:

$> uvx jpamb evaluate python ./guess.py > result.json

Which you should upload to ??

Also research is done on this!

But, you can opt out if you like

Questions

  1. Is program analysis easy?

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

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