Semantics

Let's give meaning to it all.

Christian Gram Kalhauge

Preliminaries: Natural Deduction
What are Semantics?
Java Bytecode
What are the Semantics of the JVM?

Questions

Is analysing bytecode a semantic analysis?
Name some ways can you describe the semantics of a program?
What does it mean to interpret a piece of code?

Preliminaries: Natural Deduction (§1)

Gentzen-style proofs

\frac{{𝑝 𝑟 𝑒 𝑚 𝑖 𝑠}_{1} \dots {𝑝 𝑟 𝑒 𝑚 𝑖 𝑠}_{n}}{𝑐 𝑜 𝑛 𝑐 𝑙 𝑢 𝑠 𝑖 𝑜 𝑛} (n a m e)

\frac{A B}{A \land B} (\land) \frac{A}{A \lor B} (\lor_{L}) \frac{B}{A \lor B} (\lor_{R})

What are Semantics? (§2)

Axiomatic Semantics
Denotational Semantics
Operational Semantics
Transition System and Traces

It's Meaning

Axiomatic Semantics (§2.1)

Meaning by specification

The flowchart from the original paper on semantics Assigning Meaning to Programs by Robert W. Floyd. The program computes the sum of an array.

Hoare Triplet

{P} C {Q}

Example: Composition

\frac{{P_{1}} C_{1} {Q_{1}} {P_{2}} C_{2} {Q_{2}} Q_{1} \Rightarrow P_{2}}{{P_{1}} C_{1}; C_{2} {Q_{2}}}

Denotational Semantics (§2.2)

Meaning by mapping

A simple expression language

e \in 𝔼 𝕏 := e_{1} + e_{2} | x | n

Mapped to Math

ℰ : 𝔼 𝕏 \to (Σ \to ℕ)

\begin{matrix} ℰ ⟦ 𝚗 ⟧ σ & = toNat (⟦ 𝚗 ⟧) \\ ℰ ⟦ 𝚡 ⟧ σ & = lookup (⟦ 𝚡 ⟧, σ) \\ ℰ ⟦ 𝚎_{𝟷} + 𝚎_{𝟸} ⟧ σ & = ℰ ⟦ 𝚎_{𝟷} ⟧ σ + ℰ ⟦ 𝚎_{𝟸} ⟧ σ \end{matrix}

Example: `x + 5`

\begin{matrix} ℰ ⟦ 𝚡 + 𝟻 ⟧ σ & = ℰ ⟦ 𝚡 ⟧ σ + ℰ ⟦ 𝟻 ⟧ σ \\ = lookup (⟦ 𝚡 ⟧, σ) + ℰ ⟦ 𝟻 ⟧ σ \\ = 3 + ℰ ⟦ 𝟻 ⟧ σ \\ = 3 + toNat (⟦ 𝟻 ⟧) \\ = 3 + 5 \\ = 8 \end{matrix}

Operational Semantics (§2.3)

Meaning by execution

Natural or Big-Step

ψ ⊢ σ ↓ v

Structural (SOS) or Small-Step

ψ ⊢ σ \to \overline{σ}

Beta Reduction in NOS

\frac{ψ ⊢ e_{1} ↓ λ x . e_{3} ψ ⊢ e_{2} ↓ v_{2} ψ [x \mapsto v_{2}] ⊢ e_{3} ↓ v}{ψ ⊢ e_{1} e_{2} ↓ v} (↓ β)

Beta Reduction in SOS

\frac{ψ ⊢ e_{1} \to {\overline{e}}_{1}}{ψ ⊢ e_{1} e_{2} \to {\overline{e}}_{1} e_{2}} (β^{1}) \frac{ψ ⊢ e_{2} \to {\overline{e}}_{2}}{ψ ⊢ (ψ_{1} | λ x . e_{1}) e_{2} \to (ψ_{1} | λ x . e_{1}) {\overline{e}}_{2}} (β^{2})

\frac{}{ψ ⊢ (ψ_{1} | λ x . e_{1}) v \to (ψ_{1} [x \mapsto v] | e_{1})} (β^{3})

But there is more...

\frac{ψ \cdot ψ_{1} ⊢ e_{1} \to {\overline{e}}_{1}}{ψ ⊢ (ψ_{1} | e_{1}) \to (ψ_{1} | \overline{e_{1}})} (ψ^{1}) \frac{ψ \cdot ψ_{1} ⊢ e_{1} \to v}{ψ ⊢ (ψ_{1} | e_{1}) \to v} (ψ^{2})

SOS is more expressive than NOS

\frac{ψ ⊢ σ \to \overline{σ} ψ ⊢ \overline{σ} ↓ v}{ψ ⊢ σ ↓ v} (step) \frac{ψ ⊢ σ \to v}{ψ ⊢ σ ↓ v} (done)

Transition System and Traces (§2.4)

A Transition System

A Transition system is a triplet $⟨ {𝐒 𝐭 𝐚 𝐭 𝐞}_{P}, δ_{P}, I_{P} ⟩$ where ${𝐒 𝐭 𝐚 𝐭 𝐞}_{P}$ is the set of program states, $δ_{P}$ is the transition relation (defined by the single step semantics) and $I_{P}$ are possible initial states.

{𝐓 𝐫 𝐚 𝐜 𝐞}_{P} = {𝐒 𝐭 𝐚 𝐭 𝐞}_{P}^{⋆}

\begin{matrix} Sem & : 𝐏 𝐫 𝐨 𝐠 𝐫 𝐚 𝐦 \to 2^{𝐓 𝐫 𝐚 𝐜 𝐞} \\ Sem & (P) = {τ \in {𝐒 𝐭 𝐚 𝐭 𝐞}_{P}^{n} | n \in [1, \infty], τ_{0} \in I_{P}, \forall i \in [1, n - 1], δ_{P} (τ_{i - 1}, τ_{i})} \end{matrix}

Example: The language of halt

ℒ_{halt} = {P | P \in ℒ, \forall τ \in Sem (P) . | τ | \neq \infty}

Java Bytecode (§3)

$ javap -cp target/classes -c jpamb.cases.Simple

.methods[] | select(.name=="assertFalse") | .code.bytecode

[ 
{ "field": { "class": "jpamb/cases/Simple", "name": "$assertionsDisabled", "type": "boolean" }, "offset": 0, "opr": "get", "static": true },
{ "condition": "ne", "offset": 3, "opr": "ifz", "target": 6 },
{ "class": "java/lang/AssertionError", "offset": 6, "opr": "new" },
{ "offset": 9, "opr": "dup", "words": 1 },
{ "access": "special", "method": { "args": [], "is_interface": false, "name": "<init>", "ref": { "kind": "class", "name": "java/lang/AssertionError" }, "returns": null }, "offset": 10, "opr": "invoke" },
{ "offset": 13, "opr": "throw" },
{ "offset": 14, "opr": "return", "type": null }
]

in#	opr	stack	description
`00`	`get`	`[]`	Get the `assertionsDisabled` boolean and put it on the stack
`01`	`ifz`	`[bool]`	if it is not equal to zero (false) jump to the 6th instruction (i.e. return)
`02`	`new`	`[]`	otherwise create a new AssertionError object.
`03`	`dup`	`[ref]`	dublicate the reference
`04`	`invoke`	`[ref, ref]`	call the init method on the AssertionErrror (consuming the top ref erence).
`05`	`throw`	`[ref]`	throw the assertion error.
`06`	`return`	`[]`	otherwise return.

$ uv run jpamb inspect "jpamb.cases.Simple.assertBoolean:(Z)V"

--format=...

Building a Bytecode Syntactic Analysis (§3.1)

Look at the solutions/bytecoder.py

What are the Semantics of the JVM? (§4)

Follow along in the solutions/interpreter.py

def step(s : State) -> State | str:
    ...

The Context and the Program Counter (§4.1)

$𝚋 𝚌 [ι]$

\begin{matrix} ι = ⟨ ι_{m}, ι_{o} ⟩ \\ ι + n = ⟨ ι_{m}, ι_{o} + n ⟩ \\ n / ι = ⟨ ι_{m}, n ⟩ \end{matrix}

@dataclass
class PC:
    method: jvm.AbsMethodID
    offset: int

    def __iadd__(self, delta):
        self.offset += delta
        return self

    def __add__(self, delta):
        return PC(self.method, self.offset + delta)

    def __str__(self):
        return f"{self.method}:{self.offset}"


@dataclass
class Bytecode:
    suite: jpamb.Suite
    methods: dict[jvm.AbsMethodID, list[jvm.Opcode]]

    def __getitem__(self, pc: PC) -> jvm.Opcode:
        try:
            opcodes = self.methods[pc.method]
        except KeyError:
            opcodes = list(self.suite.method_opcodes(pc.method))
            self.methods[pc.method] = opcodes

        return opcodes[pc.offset]

The Values, Operator Stack, and Locals. (§4.2)

\begin{matrix} 𝐕_{σ} & := (𝚒 𝚗 𝚝 n) | (𝚏 𝚕 𝚘 𝚊 𝚝 f) | (𝚛 𝚎 𝚏 r) \\ 𝐕_{η} & := 𝐕_{σ} | (𝚋 𝚢 𝚝 𝚎 b) | (𝚌 𝚑 𝚊 𝚛 c) | (𝚜 𝚑 𝚘 𝚛 𝚝 s) | (𝚊 𝚛 𝚛 𝚊 𝚢 t a) | (𝚘 𝚋 𝚓 𝚎 𝚌 𝚝 c n f s) \end{matrix}

The Operator Stack

$σ \in 𝐕_{σ} *$
$σ = ϵ (𝚒 𝚗 𝚝 1) (𝚒 𝚗 𝚝 2) (𝚒 𝚗 𝚝 3)$

The Locals

$λ \in ℕ \to 𝐕_{σ}$
$λ [10]$

A Frame

⟨ λ, σ, ι ⟩

@dataclass
class Frame:
    locals: dict[int, jvm.Value]
    stack: Stack[jvm.Value]
    pc: PC

    def __str__(self):
        locals = ", ".join(f"{k}:{v}" for k, v in self.locals.items())
        return f"<{{{locals}}}, {self.stack}, {self.pc}>"

The Stepping Function (§4.3)

𝚋 𝚌 ⊢ ⟨ λ, σ, ι ⟩ \to ⟨ \overline{λ}, \overline{σ}, \overline{ι} ⟩

def step(state: State) -> State | str:
    frame = state.frames.peek() # Get the current frame
    match bc[frame.pc]:
      case ...

Implementing $(𝚙𝚞𝚜𝚑:𝙸 v)$

\frac{𝚋 𝚌 [ι] = (𝚙𝚞𝚜𝚑:𝙸 v)}{𝚋 𝚌 ⊢ ⟨ λ, σ, ι ⟩ \to ⟨ λ, σ (𝚒 𝚗 𝚝 v), ι + 1 ⟩} (p u s h_{I})

case jvm.Push(value=v):
    frame.stack.push(v)
    frame.pc += 1
    return state

Implementing $(𝚕𝚘𝚊𝚍:𝙸 n)$

\frac{𝚋 𝚌 [ι] = (𝚕𝚘𝚊𝚍:𝙸 n) (𝚒 𝚗 𝚝 v) = λ [n]}{𝚋 𝚌 ⊢ ⟨ λ, σ, ι ⟩ \to ⟨ λ, σ (𝚒 𝚗 𝚝 v), ι + 1 ⟩} ({load}_{I})

case jvm.Load(type=jvm.Int(), index=n):
    v = frame.locals[n]
    assert v.type is jvm.Int()
    frame.stack.push(v)
    frame.pc += 1
    return state

The Call Stack, The Heap, and Terminating the Program (§4.4)

μ \sim \dots ⟨ λ_{2}, σ_{2}, ι_{2} ⟩ ⟨ λ_{1}, σ_{1}, ι_{1} ⟩

η \in ℕ \to 𝐕_{η}

⟨ η, μ ⟩ \in 𝐒 𝐭 𝐚 𝐭 𝐞

@dataclass
class State:
    heap: dict[int, jvm.Value]
    frames: Stack[Frame]

Do you even lift?

𝚋 𝚌 ⊢ ⟨ η, μ ⟩ \to ⟨ \overline{η}, \overline{μ} ⟩

\frac{𝚋 𝚌 ⊢ ⟨ λ, σ, ι ⟩ \to ⟨ \overline{λ}, \overline{σ}, \overline{ι} ⟩}{𝚋 𝚌 ⊢ μ ⟨ λ, σ, ι ⟩ \to μ ⟨ \overline{λ}, \overline{σ}, \overline{ι} ⟩} ({lift}_{μ})

\frac{𝚋 𝚌 ⊢ μ \to \overline{μ}}{𝚋 𝚌 ⊢ ⟨ η, μ ⟩ \to ⟨ η, \overline{μ} ⟩} ({lift}_{η})

We terminate with...

$ok$ or $err (‘𝚛𝚎𝚊𝚜𝚘𝚗’)$

Terminating with $ok$

\frac{𝚋 𝚌 [ι] = (𝚛𝚎𝚝𝚞𝚛𝚗:𝙸)}{𝚋 𝚌 ⊢ ⟨ η, ϵ ⟨ λ, σ (𝚒 𝚗 𝚝 v), ι ⟩ ⟩ \to ok} ({return}_{ϵ})

\frac{𝚋 𝚌 [ι] = (𝚛𝚎𝚝𝚞𝚛𝚗:𝙸) \begin{matrix} μ_{1} = ⟨ λ_{2}, σ_{2}, ι_{2} ⟩ \\ μ_{2} = ⟨ λ, σ (𝚒 𝚗 𝚝 v), ι ⟩ \end{matrix}}{𝚋 𝚌 ⊢ ⟨ η, μ μ_{1} μ_{2} ⟩ \to ⟨ η, μ ⟨ λ_{2}, σ_{2} (𝚒 𝚗 𝚝 v), ι_{2} + 1 ⟩ ⟩} ({return}_{μ})

In Python

case jvm.Return(type=jvm.Int()):
    v1 = frame.stack.pop()
    state.frames.pop()
    if state.frames:
        frame = state.frames.peek()
        frame.stack.push(v1)
        frame.pc += 1
        return state
    else:
        return "ok"

Terminating with $err (‘..’)$

\frac{𝚋 𝚌 [ι] = (𝚋𝚒𝚗𝚊𝚛𝚢:𝙸 𝚍𝚒𝚟) v_{2} = 0}{𝚋 𝚌 ⊢ ⟨ σ (𝚒 𝚗 𝚝 v_{1}) (𝚒 𝚗 𝚝 v_{2}), ι ⟩ \to err (‘𝚍𝚒𝚟𝚒𝚍𝚎 𝚋𝚢 𝚣𝚎𝚛𝚘’)} ({b d i v}_{I 0})

\frac{𝚋 𝚌 [ι] = (𝚋𝚒𝚗𝚊𝚛𝚢:𝙸 𝚍𝚒𝚟) v_{2} \neq 0 v_{3} = v_{1} /_{𝚒 𝟹𝟸} v_{2}}{𝚋 𝚌 ⊢ ⟨ σ (𝚒 𝚗 𝚝 v_{1}) (𝚒 𝚗 𝚝 v_{2}), ι ⟩ \to ⟨ σ (𝚒 𝚗 𝚝 v_{3}), ι + 1 ⟩} ({b d i v}_{I 1})

In Python

case jvm.Binary(type=jvm.Int(), operant=jvm.BinaryOpr.Div):
    v2, v1 = frame.stack.pop(), frame.stack.pop()
    assert v1.type is jvm.Int(), f"expected int, but got {v1}"
    assert v2.type is jvm.Int(), f"expected int, but got {v2}"
    if v2 == 0:
        return "divide by zero"

    frame.stack.push(jvm.Value.int(v1.value // v2.value))
    frame.pc += 1
    return state

What about the rest? (§4.5)

It's now up to you!

How can I figure out what everything means?

jvm2json/CODEC.txt at kalhauge/jvm2json: the decompiled codec (search for <ByteCodeInst>).
List of Java bytecode instructions - Wikipedia.
Chapter 4. The class File Format: the class file format. And, finally
Chapter 6. The Java Virtual Machine Instruction Set: the official specification of each instruction.

Write an interpreter

$ uv run interpreter.py "jpamb.cases.Simple.assertInteger:(I)V" "(1)"
... alot  ...
... of intermediate  ...
... results ...
ok

Write an interpreter

$ uv run jpamb interpret -W --filter Simple interpreter.py

Start small, one method at a time. You don't have to cover the entire language. Also you don't need a method stack or a heap for most of the cases — do them later.
It's okay to hack some things, like getting the $assertionsDisabled static field. You can assume that is always be false.
Print out the state to stderr at every step, this will help you debug.
Look at solutions/interpreter.py for inspiration, or extend it.
Use the --stepwise flag to run the last failed case next time.

Questions

Is analysing bytecode a semantic analysis?
Name some ways can you describe the semantics of a program?
What does it mean to interpret a piece of code?

Semantics

Table of Contents

Questions

Preliminaries: Natural Deduction (§1)

What are Semantics? (§2)

Axiomatic Semantics (§2.1)

Denotational Semantics (§2.2)

A simple expression language

Mapped to Math

Example: x + 5

Operational Semantics (§2.3)

Natural or Big-Step

Structural (SOS) or Small-Step

Beta Reduction in NOS

Beta Reduction in SOS

SOS is more expressive than NOS

Transition System and Traces (§2.4)

A Transition System

Example: The language of halt

Java Bytecode (§3)

Building a Bytecode Syntactic Analysis (§3.1)

What are the Semantics of the JVM? (§4)

The Context and the Program Counter (§4.1)

The Values, Operator Stack, and Locals. (§4.2)

The Operator Stack

The Locals

A Frame

The Stepping Function (§4.3)

Implementing (𝚙𝚞𝚜𝚑:𝙸 v)

Implementing (𝚕𝚘𝚊𝚍:𝙸 n)

The Call Stack, The Heap, and Terminating the Program (§4.4)

Do you even lift?

We terminate with...

Terminating with ok

Terminating with err(‘..’)

What about the rest? (§4.5)

How can I figure out what everything means?

Questions

Example: `x + 5`

Implementing $(𝚙𝚞𝚜𝚑:𝙸 v)$

Implementing $(𝚕𝚘𝚊𝚍:𝙸 n)$

Terminating with $ok$

Terminating with $err (‘..’)$