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 fZ, fN, fC, fV
one bit each
Execution pointer EP
a word
Temporary register T
a word
Memory M
a quantity
Permutation functions p8, p16, p32, pA
 
Stack S
a stack
Frame stack F
a stack

An index into M is called an address.

The function pw 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. FS(i) and FN(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… FN(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.

Sp, where p is a stack position, denotes S[FS(FP)+p−1]; &Sp denotes the address of Sp. SP is an abbreviation for FS(FP)+FN(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 Sp is a register, or T
Chunk c
a stack position p such that Sp 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:

fZ← ρ
fN← ρ
fC← ρ
fV← ρ

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

5.1 Assignment

Sr1← Sr2
fZ← [Sr1=0]
fN← [Sr1<0] Sr← &Sc
fZ← [Sr1=0] T← Sr1
Sr1← Sr2
Sr2← T

5.2 Data processing

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

fZ← [Sr1=0]

fN← [Sr1<0]

appended to the end of their semantics.

5.2.1 Arithmetic

Sr1← −Sr2
fC← [Sr1=0]
fV← [Sr1=−2A−1] Sr1← Sr2+Sr3
fC← carry out of most significant bit
fV← [signed overflow occurred] Sr1← Sr2−Sr3
fC← carry out of most significant bit
fV← [signed overflow occurred] Sr1← Sr2× Sr3 Sr3≠ 0 Sr1← Sr2÷ Sr3, treating Sr2 and Sr3 as unsigned, and rounding the quotient to 0 Sr3≠ 0 Sr1← Sr2÷ Sr3, treating Sr2 and Sr3 as signed, and rounding the quotient to −∞ Sr3≠ 0 Sr1← Sr2÷ Sr3, treating Sr2 and Sr3 as signed, and rounding the quotient to 0 DIV(T,r2,r3)
r1← r2−T× r3 DIVS(T,r2,r3)
r1← r2−T× r3 DIVSZ(T,r2,r3)
r1← r2−T× r3

5.2.2 Logic

Sr1← one’s complement of Sr2 Sr1← bitwise and of Sr2 and Sr3 Sr1← bitwise or of Sr2 and Sr3 Sr1← bitwise exclusive-or of Sr2 and Sr3 0≤ Sr3≤ A Sr1← Sr2 shifted left Sr3 places
fC← carry out of most significant bit, if Sr3>0 0≤ Sr3≤ A Sr1← Sr2 shifted right logically Sr3 places
fC← carry out of least significant bit, if Sr3>0 0≤ Sr3≤ A Sr1← Sr2 shifted right arithmetically Sr3 places
fC← carry out of least significant bit, if Sr3>0

5.3 Memory

Sr1← 0
Sr1[0… w−1]← pw(M[Sr2… Sr2+w−1]) M[Sr2… Sr2+w−1]← pw−1(Sr1[0… w−1]) Sr1+s≤ Sr2 or Sr2+s≤ Sr1 M[Sr1… Sr1+s−1]← M[Sr2… Sr2+s−1] Sr+s≤ &Sc or &Sc+s≤ Sr M[Sr… Sr+s−1]← M[&Sc… &Sc+s−1] &Sc+s≤ Sr or Sr+s≤ &Sc M[&Sc… &Sc+s−1]← M[Sr… Sr+s−1] &Sc1+s≤ &Sc2 or &Sc2+s≤ &Sc1 M[&Sc1… &Sc1+s−1]← M[&Sc2… &Sc2+s−1]

5.4 Branch

EP← Sr fZ=1 EP← Sr fZ=0 EP← Sr fN=1 EP← Sr fN=0 EP← Sr fC=1 EP← Sr fC=0 EP← Sr fV=1 EP← Sr fV=0 EP← Sr fC=1 and fZ=0 EP← Sr fC=0 or fZ=1 EP← Sr fN≠ fV EP← Sr fN=fV EP← Sr fZ=1 or fN≠ fV EP← Sr fZ=0 and fN=fV EP← Sr

5.5 Call and return

NEW(s)
S[SP][o… o+A−1]← EP
EP← Sr
F[FP]← (FS(FP),FN(FP)−(p+1))
F← F⊕ (SP+1,p+1) EP← Sc[o… o+A−1]
KILL(c)
F← F[1… FP−2]⊕ (FS(FP−1),FN(FP−1)+FN(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

Sr← FP EP← Sr1
F← F[1… Sr2]
S← S[1… SP−1]⊕ Sr3

5.7 Stack

S← S⊕ ρ [0… A−1]
F[FP]← (FS(FP),FN(FP)+1) S← S⊕ ρ [0… s−1]
F[FP]← (FS(FP),FN(FP)+1) S[FS(FP)+p−1… SP−1]← S[FS(FP)+p… SP]
F[FP]← (FS(FP),FN(FP)−1)
S← S[1… SP]

This document was translated from LATEX by HEVEA.
Last updated 2006/06/02