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

What is the semantics of a program?
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 Natural

\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})

(ψ_{1} | e_{1}) - an expression e_{1} in scope ψ_{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} \subseteq {𝐒 𝐭 𝐚 𝐭 𝐞}_{p}^{⋆}

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

jq '.methods[] | select(.name=="assertFalse") | .code.bytecode' \
  target/decompiled/jpamb/cases/Simple.json

[ 
{ "opr": "get", "field": { "class": "jpamb/cases/Simple", "name": "$assertionsDisabled", "type": "boolean" },  "static": true },
{ "opr": "ifz", "condition": "ne", "target": 6 },
{ "opr": "new", "class": "java/lang/AssertionError" },
{ "opr": "dup", "words": 1 },
{ "opr": "invoke", "access": "special", "method": { "args": [], "is_interface": false, "name": "<init>", "ref": { "kind": "class", "name": "java/lang/AssertionError" }, "returns": null },  },
{ "opr": "throw" },
{ "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/syntactic/src/syntactic_bytecode.py

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

Follow along in solutions/dynamic and src/jvm/state.py

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

The Context and the Program Counter (§4.1)

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

>>> pc = PC(method, offset)
>>> pc += n # add n to the offset
>>> pc %= n # replace the offest with n

Using the JPAMB suite

>>> suite, eff = jpamb.setup()
>>> bc = jpamb.Bytecode(suite, eff, {})
>>> bc[pc]

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)$

class OperandStack:
    operands: deque[StackValue]

The Locals

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

class Locals:
   locals: list[StackValue | None]

A Frame

⟨ λ, σ, ι ⟩

class Frame:
    locals: Locals
    stack: OperandStack
    pc: PC

The Stepping Function (§4.3)

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

def step(bc: jpamb.Bytecode, state: State) -> tuple[PC, State | str]:
    frame = state.frames.peek()
    opr = bc[frame.pc]
    pc, output = frame.pc, state  # Default to outputting the state
    print(f"Stepping {pc}:\n > {opr}", file=sys.stderr)
    match opr:
        # The opcodes to handle ...
    return pc, output

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

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

case jvm.Push(type=t, value=v):
    if t is not jvm.Int():
        raise NotImplementedError(f"Don't know how to handle {t}")
    frame.stack.push(StackInt(v))
    frame.pc += 1

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

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

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

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

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

η \in ℕ \to 𝐕_{η}

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

class State:
    heap: Heap
    frames: CallStack

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} = ⟨ λ, σ (𝚒 𝚗 𝚝 v), ι ⟩ \\ μ_{2} = ⟨ λ_{2}, σ_{2}, ι_{2} ⟩ \end{matrix}}{𝚋 𝚌 ⊢ ⟨ η, μ μ_{2} μ_{1} ⟩ \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
    else:
        output = "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=op):
    v2, v1 = frame.stack.pop(), frame.stack.pop()
    assert isinstance(v1, jvmc.StackInt), f"expected int, but got {v1}"
    assert isinstance(v2, jvmc.StackInt), f"expected int, but got {v2}"

    value: int | str = binary(op, v1.value, v2.value)

    if isinstance(value, str):
        output = value
    else:
        frame.stack.push(jvmc.StackInt(value))
        frame.pc += 1

In Python

def binary(op, v1: int, v2: int) -> int | str:
    match op:
        case jvm.BinaryOpr.Div:
            try:
                return v1 // v2
            except ZeroDivisionError:
                return "divide by zero"
        case a:
            raise NotImplementedError(f"Unhandled binary {op!r}")

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

$ jpamb -vv interpret --filter Simple --step-wise dynamic-interpreter

Start small, one method at a time. You don't have to cover the entire language.
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 (already done in the example)
Use the --step-wise flag to run the last failed case next time.

Next time, we will turn the interpreter into an analysis!

Questions

What is the semantics of a program?
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 Natural

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)

Using the JPAMB suite

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?

Next time, we will turn the interpreter into an analysis!

Questions

Example: `x + 5`

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

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

Terminating with $ok$

Terminating with $err (‘..’)$