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 precondition 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 mean that if the world satisfies $P$ before executing $C$ then the world will satisfy $Q$ after.

The great thing about this approach is that we can compose the proofs of correctness of parts of the program into a proof of total correctness. Assume the 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. Essentially it means that given $\{P_1\}{C}_1\{Q_1\}$, and $\{P_2\}{C}_2\{Q_2\}$, and that the postcondition of $C_1$ implies the precondition of $C_2$ $(Q_1\Rightarrow P_2)$, are all true, we can also prove that $\{P\}{C}_1;C_2\{Q\}$.

This approach is every effective at describing the meaning of specific programs. This makes it it is very good for doing program verification, but is not used for program analysis in general.

Denotational Semantics §2.2

Another approach for writing down the semantics of the program is Denotational Semantics. The idea behind denotational semantics is to map the semantics of the program we want to analyse to something we know well. This can either be another programming language or math.

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

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

Here we explain that the semantic + means the same as mathematical operator $+$, that variables are the same as looking up the variable in a store, and that numbers should just be read as natural numbers.

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

If you think that this looks exactly like functional programming, you would be right. It is also best at describing Expression-oriented programming languages.

Operational Semantics §2.3

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

The Structural Operational Semantics or Small Step Semantics are written as judgments of the type $(\psi ⊢\sigma \to \bar{\sigma })$ which means given the environment $\psi$, the state of the program $\sigma$ can be turned into $\bar{\sigma }$.

The reason we call this approach the small step semantics is that we only execute a single operation at a time.

The Natural Operational Semantics or Big Step Semantics, are describing running the program until it halts. $(\psi ⊢\sigma \downarrow v)$ where $v$ is the final value of the program. Big step semantics often looks nicer than small step semantics, because it does not have to care about execution order.

Big Step semantics have the benefit of being easier to read, however, it has some big 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 the operational semantics by simply applying the single step semantics until the program terminates with a value:

Transition System and Traces §2.4

Using our new found 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 semantics rules, the JVM is run in a context. This context is the bytecode $𝚋𝚌$. For now we will define a simple operation $𝚋𝚌[\iota ]$ which looks up the bytecode instruction at $\iota$. $\iota$ is program counter, i.e., the name of the method and the offset in that method.

We use the following short hands:

To do this in Python you can should do something like this:

@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

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

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

The stack contains ints are signed 32 bit integers, floats are 32 bit floating point values (IEEE 754 Standard (JLS §1.7)), and references to the heap which are only 32 bits.

The heap can contain values from the stack, as well as bytes and chars that are 8 bits and 16 bits unsigned respectively, shorts are signed 16 bits, and arrays which a type and list of values, and objects which has a name and the values of the fields, which is a mapping from names to heap values.

In this course we'll not cover long and double as they are a pain in the *ss. Furthermore, we'll try to avoid inner classes and bootstrap methods as well.

The stack is a list of values: $\sigma ={𝐕}_{\sigma }*$. $ϵ$ denote 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 can be done like this:

@dataclass
class Stack[T]:
    items: list[T]

    def __bool__(self) -> bool:
        return len(self.items) > 0

    @classmethod
    def empty(cls):
        return cls([])

    def peek(self) -> T:
        return self.items[-1]

    def pop(self) -> T:
        return self.items.pop(-1)

    def push(self, value):
        self.items.append(value)
        return self

    def __str__(self):
        if not self:
            return "ϵ"
        return "".join(f"{v}" for v in self.items)

In the JVM saves local variables of type ${𝐕}_{\sigma }$ to a local array $\lambda$. This is were the inputs to the method goes and any data that should be saved on the method stack instead of in the heap. The local array is indexed normally $\lambda [0]$.

In its simplest form, the state of the JVM is a triplet $⟨\lambda ,\sigma ,\iota ⟩$ which we will call a frame, where $\lambda$ is the locals, $\sigma$ is the operator stack and $\iota$ is the program counter.

In Python, we would write:

@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

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(state: State) -> State | str:
    frame = state.frames.peek() # Get the current frame
    match bc[frame.pc]:
      case ...

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(value=v):
    frame.stack.push(v)
    frame.pc += 1
    return state

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]
    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

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:

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

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
        return state
    else:
        return "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=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

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 run interpreter.py "jpamb.cases.Simple.assertInteger:(I)V" "(1)"
... alot  ...
... of intermediate  ...
... results ...
ok

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