## Mite’s semantics## Reuben Thomas## 25th October 2000 |

## 1 Introduction

Mite’s semantics are defined in terms of an abstract machine, which consists of a state and a set of rules for transforming it according to a program.

## 2 Definitions

- Quantity
- a string of bits
- q[i… j]
- the quantity consisting of bits i to j inclusive of quantity q
- Width
- the number of bits in a quantity
- A
- either 32 or 64
- Word
- an A-bit quantity
- w-aligned
- a multiple of w
- Size
- an expression of the form b+w+r, where b, w, and r are non-negative integers, whose value is b+Aw+32⌊A/64⌋r
- ρ
- an undefined quantity of infinite width
- [S]
- a bit representing the truth of statement S; if S is true then [S] is one, otherwise it is zero
- q← E
- the assignment of expression E to quantity q; before assignment, E is truncated or zero-extended to make it the same width as q
- Stack
- a last-in-first-out stack whose items are said to be added to the top, and are numbered from one, counting from the bottom
- s[i]
- the ith item of stack s
- s[i… j]
- the stack consisting of items i to j inclusive of stack s
- s⊕ E
- the stack s with an extra item added whose value is E

## 3 State

Mite’s state consists of the following elements:

- Flags f
_{Z}, f_{N}, f_{C}, f_{V} - one bit each
- Execution pointer EP
- a word
- Temporary register T
- a word
- Memory M
- a quantity
- Permutation functions p
_{8}, p_{16}, p_{32}, p_{A} - Stack S
- a stack
- Frame stack F
- a stack

An index into M is called an address.

The function p_{w} takes a quantity of width w and returns it with its bytes permuted.

F is a stack of pairs of naturals. FP is the index of the top-most item in F. F_{S}(i) and F_{N}(i) denote respectively the first and second component of the ith item of F. A stack position is a natural p in the range 1… F_{N}(FP).

S holds items of two sorts: a register is a word created by NEW(), and a chunk is a quantity of arbitrary size created by NEW(c) (see section 5.7). The stack items are held in M at word-aligned addresses.

S_{p}, where p is a stack position, denotes S[F_{S}(FP)+p−1]; &S_{p} denotes the address of S_{p}. SP is an abbreviation for F_{S}(FP)+F_{N}(FP)−1.

## 4 Program

An instruction consists of an operation and a tuple of operands. Each operand has a type, given by its name; a subscript is added to distinguish operands of the same type. The allowable instructions are given in section 5. The program P is an array of instructions; P[i] denotes the ith element of P.

The types are:

- Stack position p
- a stack position
- Natural n
- a non-negative integer
- Register r
- a stack position p such that S
_{p}is a register, or T - Chunk c
- a stack position p such that S
_{p}is a chunk - Width w
- a member of the set {8,16,32,A}
- Size s
- a size

## 5 Instructions

The state is transformed by repeatedly performing EP← EP+1 then the semantics of P[EP−1]. The semantics of each instruction are given below in terms of assignments to state elements, and other instructions; the operations are performed sequentially. An underlined expression is a predicate that must evaluate to true when the instruction is executed; otherwise the instruction has no effect.

Arithmetic is integral, performed on A-digit binary numbers using two’s complement interpretation. Quantities are evaluated with bit zero as the least significant digit.

The semantics of every instruction have the assignment T← ρ prepended, and also, for all instructions except branches (see section 5.4), the following:

_{Z}← ρ

f

_{N}← ρ

f

_{C}← ρ

f

_{V}← ρ

For branches, the four instructions above are added to the end of the instruction’s semantics.

### 5.1 Assignment

S_{r1}← S_{r2}

f_{Z}← [S_{r1}=0]

f_{N}← [S_{r1}<0]
S_{r}← &S_{c}

f_{Z}← [S_{r1}=0]
T← S_{r1}

S_{r1}← S_{r2}

S_{r2}← T

### 5.2 Data processing

All the data processing instructions except MUL, DIVSZ and REMSZ have

_{Z}← [S

_{r1}=0]

f_{N}← [S_{r1}<0]

appended to the end of their semantics.

#### 5.2.1 Arithmetic

S_{r1}← −S_{r2}

f_{C}← [S_{r1}=0]

f_{V}← [S_{r1}=−2^{A−1}]
S_{r1}← S_{r2}+S_{r3}

f_{C}← carry out of most significant bit

f_{V}← [signed overflow occurred]
S_{r1}← S_{r2}−S_{r3}

f_{C}← carry out of most significant bit

f_{V}← [signed overflow occurred]
S_{r1}← S_{r2}× S_{r3}
S_{r3}≠ 0 S_{r1}← S_{r2}÷ S_{r3}, treating S_{r2} and S_{r3} as unsigned, and rounding the quotient to 0
S_{r3}≠ 0 S_{r1}← S_{r2}÷ S_{r3}, treating S_{r2} and S_{r3} as signed, and rounding the quotient to −∞
S_{r3}≠ 0 S_{r1}← S_{r2}÷ S_{r3}, treating S_{r2} and S_{r3} as signed, and rounding the quotient to 0
DIV(T,r_{2},r_{3})

r_{1}← r_{2}−T× r_{3}
DIVS(T,r_{2},r_{3})

r_{1}← r_{2}−T× r_{3}
DIVSZ(T,r_{2},r_{3})

r_{1}← r_{2}−T× r_{3}

#### 5.2.2 Logic

S_{r1}← one’s complement of S_{r2}
S_{r1}← bitwise and of S_{r2} and S_{r3}
S_{r1}← bitwise or of S_{r2} and S_{r3}
S_{r1}← bitwise exclusive-or of S_{r2} and S_{r3}
0≤ S_{r3}≤ A S_{r1}← S_{r2} shifted left S_{r3} places

f_{C}← carry out of most significant bit, if S_{r3}>0
0≤ S_{r3}≤ A S_{r1}← S_{r2} shifted right logically S_{r3} places

f_{C}← carry out of least significant bit, if S_{r3}>0
0≤ S_{r3}≤ A S_{r1}← S_{r2} shifted right arithmetically S_{r3} places

f_{C}← carry out of least significant bit, if S_{r3}>0

### 5.3 Memory

S_{r1}← 0

S_{r1}[0… w−1]← p_{w}(M[S_{r2}… S_{r2}+w−1])
M[S_{r2}… S_{r2}+w−1]← p_{w}^{−1}(S_{r1}[0… w−1])
S_{r1}+s≤ S_{r2} or S_{r2}+s≤ S_{r1} M[S_{r1}… S_{r1}+s−1]← M[S_{r2}… S_{r2}+s−1]
S_{r}+s≤ &S_{c} or &S_{c}+s≤ S_{r} M[S_{r}… S_{r}+s−1]← M[&S_{c}… &S_{c}+s−1]
&S_{c}+s≤ S_{r} or S_{r}+s≤ &S_{c} M[&S_{c}… &S_{c}+s−1]← M[S_{r}… S_{r}+s−1]
&S_{c1}+s≤ &S_{c2} or &S_{c2}+s≤ &S_{c1} M[&S_{c1}… &S_{c1}+s−1]← M[&S_{c2}… &S_{c2}+s−1]

### 5.4 Branch

EP← S_{r}
f_{Z}=1
EP← S_{r}
f_{Z}=0
EP← S_{r}
f_{N}=1
EP← S_{r}
f_{N}=0
EP← S_{r}
f_{C}=1
EP← S_{r}
f_{C}=0
EP← S_{r}
f_{V}=1
EP← S_{r}
f_{V}=0
EP← S_{r}
f_{C}=1 and f_{Z}=0
EP← S_{r}
f_{C}=0 or f_{Z}=1
EP← S_{r}
f_{N}≠ f_{V}
EP← S_{r}
f_{N}=f_{V}
EP← S_{r}
f_{Z}=1 or f_{N}≠ f_{V} EP← S_{r}
f_{Z}=0 and f_{N}=f_{V} EP← S_{r}

### 5.5 Call and return

NEW(s)

S[SP][o… o+A−1]← EP

EP← S_{r}

F[FP]← (F_{S}(FP),F_{N}(FP)−(p+1))

F← F⊕ (SP+1,p+1)
EP← S_{c}[o… o+A−1]

KILL(c)

F← F[1… FP−2]⊕ (F_{S}(FP−1),F_{N}(FP−1)+F_{N}(FP))

o and s may vary between instructions, but should be the same for corresponding CALLs and RETs; s is at least A, and 0≤ o≤ s−A.

### 5.6 Catch and throw

S_{r}← FP
EP← S_{r1}

F← F[1… S_{r2}]

S← S[1… SP−1]⊕ S_{r3}

### 5.7 Stack

S← S⊕ ρ [0… A−1]

F[FP]← (F_{S}(FP),F_{N}(FP)+1)
S← S⊕ ρ [0… s−1]

F[FP]← (F_{S}(FP),F_{N}(FP)+1)
S[F_{S}(FP)+p−1… SP−1]← S[F_{S}(FP)+p… SP]

F[FP]← (F_{S}(FP),F_{N}(FP)−1)

S← S[1… SP]

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.

*Last updated 2006/06/02*