Semantics

Axiomatic Semantics §2.1

One of the first approaches invented to assign meaning to programs was Axiomatic Semantics. Here, the meaning of the program is described by assigning preconditions and postconditions to all statements in a program.

We can describe the semantics of a program by denoting three parts, the precondition $P$, the program $C$, and the postcondition $Q$, this is also called Hoare triplets.

A Hoare triplet means that if the world satisfies $P$ before executing $C$, then the world will satisfy $Q$ after. We can compose the proofs of correctness of program parts into a proof of total correctness. Assume a program $C_1;C_2$, where $C_2$ is executed after $C_1$. Then we can describe the correctness of $C_1;C_2$, like so:

If you are unfamiliar with the syntax above, it is natural deduction; see the section on natural deduction. Given $\{P_1\}{C}_1\{Q_1\}$, $\{P_2\}{C}_2\{Q_2\}$, and the implication that the postcondition of $C_1$ $ implies the precondition of $C_2$ $(Q_1\Rightarrow P_2)$ are true, we can also prove that $\{P\}{C}_1;C_2\{Q\}$.

This approach is effective at describing the meaning of specific programs. This approach excels at program verification but is not typically used for program analysis in general.

Denotational Semantics §2.2

Another approach to defining program semantics is Denotational Semantics. Denotational semantics maps the semantics of a program to something well-understood. This can be another programming language or mathematics.

Consider a very simple expressional language called $𝔼𝕏$, which has addition, variables $x$ and natural numbers $n$:

If you want to give meaning to the $𝔼𝕏$ program x + 5, we can define a map from expressions to a function from a store to integers: $ℰ:𝔼𝕏\to (\mathrm{\Sigma }\to \mathbb{N})$

Essentially, $ℰ$ gives meaning to numbers, variables, and addition. Numbers should be read as natural numbers. Variables correspond to looking up a value in a store. The semantic + is equivalent to the mathematical operator $+$.

Now we can see that x + 5 can be calculated in the store $\sigma =[x\mapsto 3]$, using normal math:

If you think this looks exactly like functional programming, you would be right. It is also particularly well-suited for describing Expression-oriented programming languages.

Operational Semantics §2.3

Next, we cover Operational Semantics, the semantic style we will focus on this semester. Operational semantics describes the semantics of a program as changes to a state. This makes it ideal for describing imperative languages like JVM bytecode. Furthermore, the Structural Operational Semantics is defined as you would write an interpreter, which is handy because you are going to write one.

The Structural Operational Semantics or Small Step Semantics is written as a judgment of the type $(\psi ⊢\sigma \to \bar{\sigma })$, indicating that given the environment $\psi$, the program state $\sigma$ transitions to $\bar{\sigma }$.

We call this approach small-step semantics because we only execute a single operation at a time.

The Natural Operational Semantics or Big Step Semantics describes running the program until it halts. $(\psi ⊢\sigma \downarrow v)$ where $v$ is the final value of the program. Big step semantics often appears simpler than small step semantics because it ignores the intermediate execution order.

Big Step semantics have the benefit of being easier to read; however, they have disadvantages, namely: we cannot reason about programs that run forever, and we cannot turn big step semantics into a working implementation. In contrast, small step semantics are easy to convert into an interpreter, and we can always recover the big step semantics from operational semantics by simply applying the single step semantics until the program terminates with a value:

Transition System and Traces §2.4

With our newfound definition of single-step semantics, we can define the meaning of a program $P$ as a Transition System:

A ${𝐓𝐫𝐚𝐜𝐞}_p$ is the possible infinite sequence of states and operations of the program.

The meaning of a program is now the set of traces that it exhibit:

This is also called the Maximal Trace Semantics. We can now define properties, like does a program halt, using relatively well defined math:

But more about this next time.

Building a Bytecode Syntactic Analysis §3.1

Now you should be able to build a syntactic analysis over the bytecode:

The Context and the Program Counter §4.1

As with all single-step semantic rules, the JVM runs in a context. This context is the bytecode $𝚋𝚌$. A simple operation $𝚋𝚌[\iota ]$ looks up the bytecode instruction at $\iota$. $\iota$ is the program counter, i.e., the name of the method and the offset in that method.

We use the following shorthands:

To do this in Python, you can use PC class from jvm.state

class PC:
    method: jvm.AbsMethodID
    offset: int

    ...

We can change offset using the following command:

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

To access the opcode, use the program counter as the index to the bytecode. Before that, we must access the bytecode using specific procedures.

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

The Values, Operator Stack, and Locals. §4.2

The JVM is a stack-based virtual machine; this means that instead of using named variables (registers) to store intermediate values, it uses an operator stack. Some values are stored in local method storage called locals, which can be accessed using indices. Finally, the machine can also store information in global memory, referred to as the heap.

The values in (our interpretation of) the JVM are dynamically typed; this means that every value carries information about its type. There are two kinds of values, stack values ${𝐕}_{\sigma }$ and heap values ${𝐕}_{\eta }$.

The stack contains signed 32-bit integers, 32-bit floating-point values (IEEE 754 Standard (JLS §1.7)), and 32-bit references to the heap. The heap can contain values from the stack, 8-bit bytes, 16-bit unsigned chars, signed 16-bit shorts, arrays (consisting of a type and a list of values), and objects (comprising a name and a mapping of field names to heap values).

In this course, we won't cover long and double to avoid unnecessary complexity. Furthermore, we'll try to avoid inner classes and bootstrap methods.

The stack is a list of values: $\sigma ={𝐕}_{\sigma }*$. $ϵ$ denotes the empty stack, and we add and remove elements from the end of the stack. A stack with the integers 1, 2, and 3 looks like this: $\sigma =ϵ(𝚒𝚗𝚝1)(𝚒𝚗𝚝2)(𝚒𝚗𝚝3)$. A simple implementation of this in Python is shown below:

class OperandStack:
    operands: deque[StackValue]

The JVM saves local variables of type ${𝐕}_{\sigma }$ to a local array $\lambda$. This array contains the method inputs and any data stored on the stack instead of the heap. The local array is indexed $\lambda [0]$.

class Locals:
   locals: list[StackValue | None]

In its simplest form, the JVM state is a triplet $⟨\lambda ,\sigma ,\iota ⟩$ called a frame, where $\lambda$ represents the local variables, $\sigma$ is the operand stack, and $\iota$ is the program counter.

In Python, we would write:

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

The Stepping Function §4.3

Most of our operations only operate on the frame, so we can already define our first simple SOS judgment like this:

Anticipating the definition of State in the next section, we define the stepping function, like so:

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

We are now ready for some examples. First we have the push operation $\mathtt{\text{(𝚙𝚞𝚜𝚑:𝙸}}v\mathtt{\text{)}}$:

Which we can encode in Python like this:

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

We can also load values from the locals using the $\mathtt{\text{(𝚕𝚘𝚊𝚍:𝙸}}n\mathtt{\text{)}}$ operation:

Which we can encode in Python like this:

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

In the JVM methods are capable of calling other methods. To support this we need a stack of frames, or a call stack $\mu$:

And now since we have multiple frames, we also need a way for the frames to share data. We call that the heap $\eta$. And it is just mapping from memory locations to ${𝐕}_{\eta }$.

The state is now just a tuple of the heap and the call stack: $⟨\eta ,\mu ⟩$. Which we can represent in Python like this:

class State:
    heap: Heap
    frames: CallStack

So now we have reached the correct definition of the stepping function, over the State.

We can use the operations we defined over frames, by lifting them into the state, by doing the frame operation on the top frame:

Our simplification of the JVM terminates when we exit from the last method, or we encounter an error. We do that with either an $\mathrm{\text{ok}}$ or an $\mathrm{\text{err}}(\mathtt{\text{‘𝚛𝚎𝚊𝚜𝚘𝚗’}})$.

In Python, we can represent terminating with no error by simply returning "ok" if the stack is empty:

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"

One example of throwing an error is the divide operation:

Which can be translated into a single case match in Python. In the case we terminate with an error, we just return the corresponding string:

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

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

So this is a very limited definition of semantics, the JVM; we have not covered threads or exceptions, and we probably won't in this course. But even with these restrictions, there are still many undefined rules left. It is your job to implement the rest of the instructions and build a working interpreter. To get started on this, we recommend you start small.

Finally, you should write an interpreter, which can interpret all the cases.

$ uv pip list
Package          Version Editable project location
---------------- ------- -----------------------------------------------------
dynamic          0.1.0   .../jpamb/solutions/dynamic
jpamb            0.6.0   .../jpamb
...

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

$ jpamb -vv interpret --filter Simple --step-wise dynamic-interpreter
┌ Reading cases from /home/chrg/Projects/Courses/jpamb/target/stats/cases.txt
└ Reading cases from /home/chrg/Projects/Courses/jpamb/target/stats/cases.txt
┌ Getting info about interpreter
│ SUCCESS Ran dynamic-interpreter info
└ Getting info about interpreter
┌ Trying to read state from cache
└ Trying to read state from cache
┌ Experiment 1/28 jpamb.cases.Simple.assertBoolean:(false) -> assertion error
│┌ Run experiment dynamic-interpreter 'jpamb.cases.Simple.assertBoolean:(Z)V' '(false)' 100
│└ Run experiment dynamic-interpreter 'jpamb.cases.Simple.assertBoolean:(Z)V' '(false)' 100
│ WARNING Ran dynamic-interpreter 'jpamb.cases.Simple.assertBoolean:(Z)V' '(false)' 100, and got error:
│ (state
│   :heap ()
│   :frames (
│     :00 (frame
│       :locals (
│         :00 (int 0)
│       )
│       :stack ()
│       :pc "jpamb.cases.Simple.assertBoolean:(Z)V:0"
│     )
│   )
│ )
│ Stepping jpamb.cases.Simple.assertBoolean:(Z)V:0:
│  > get static jpamb.cases.Simple.$assertionsDisabled:Z
│ (state
│   :heap ()
│   :frames (
│     :00 (frame
│       :locals (
│         :00 (int 0)
│       )
│       :stack (
│         :00 (int 0)
│       )
│       :pc "jpamb.cases.Simple.assertBoolean:(Z)V:1"
│     )
│   )
│ )
│ Stepping jpamb.cases.Simple.assertBoolean:(Z)V:1:
│  > ifz ne 8
│ Traceback (most recent call last):
│   File "/home/chrg/Projects/Courses/jpamb/.jpamb-eval/bin/dynamic-interpreter", line 10, in <module>
│     sys.exit(interpret())
│              ~~~~~~~~~^^
│   File "/home/chrg/Projects/Courses/jpamb/solutions/dynamic/src/dynamic.py", line 136, in interpret
│     pc, state = step(bc, state)
│                 ~~~~^^^^^^^^^^^
│   File "/home/chrg/Projects/Courses/jpamb/solutions/dynamic/src/dynamic.py", line 80, in step
│     raise NotImplementedError(a.help())
│ NotImplementedError: It seems Ifz(offset=3, condition=<CmpOpr.Ne: 1>, target=8) is not implemented! Instructions can be found at: https://docs.oracle.com/javase/specs/jvms/se23/html/jvms-6.html#jvms-6.5.if_cond
│ WARNING Invalid output: No reponse created
└ Experiment 1/28 jpamb.cases.Simple.assertBoolean:(false) -> assertion error
ERROR Stopping early

case jvm.Ifz(condition=op, target=target):
    value = frame.stack.pop()
    assert isinstance(value, jvmc.StackInt), f"expected int, but got {value}"

    if compare(op, value.value, 0):
        frame.pc %= target
    else:
        frame.pc += 1