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[ij]
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
qE
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[ij]
the stack consisting of items i to j inclusive of stack s
sE
the stack s with an extra item added whose value is E

3  State

Mite’s state consists of the following elements:

Flags fZfNfCfV
one bit each
Execution pointer EP
a word
Temporary register T
a word
Memory M
a quantity
Permutation functions p8p16p32pA
 
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 EPEP+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

Sr1Sr2
fZ← [Sr1=0]
fN← [Sr1<0] Sr← &Sc
fZ← [Sr1=0] TSr1
Sr1Sr2
Sr2T

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] Sr1Sr2+Sr3
fC← carry out of most significant bit
fV← [signed overflow occurred] Sr1Sr2Sr3
fC← carry out of most significant bit
fV← [signed overflow occurred] Sr1Sr2× Sr3 Sr3≠ 0 Sr1Sr2÷ Sr3, treating Sr2 and Sr3 as unsigned, and rounding the quotient to 0 Sr3≠ 0 Sr1Sr2÷ Sr3, treating Sr2 and Sr3 as signed, and rounding the quotient to −∞ Sr3≠ 0 Sr1Sr2÷ Sr3, treating Sr2 and Sr3 as signed, and rounding the quotient to 0 DIV(T,r2,r3)
r1r2T× r3 DIVS(T,r2,r3)
r1r2T× r3 DIVSZ(T,r2,r3)
r1r2T× 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≤ Sr3A Sr1Sr2 shifted left Sr3 places
fC← carry out of most significant bit, if Sr3>0 0≤ Sr3A Sr1Sr2 shifted right logically Sr3 places
fC← carry out of least significant bit, if Sr3>0 0≤ Sr3A Sr1Sr2 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[Sr2Sr2+w−1]) M[Sr2Sr2+w−1]← pw−1(Sr1[0… w−1]) Sr1+sSr2 or Sr2+sSr1 M[Sr1Sr1+s−1]← M[Sr2Sr2+s−1] Sr+s≤ &Sc or &Sc+sSr M[SrSr+s−1]← M[&Sc… &Sc+s−1] &Sc+sSr or Sr+s≤ &Sc M[&Sc… &Sc+s−1]← M[SrSr+s−1] &Sc1+s≤ &Sc2 or &Sc2+s≤ &Sc1 M[&Sc1… &Sc1+s−1]← M[&Sc2… &Sc2+s−1]

5.4  Branch

EPSr fZ=1 EPSr fZ=0 EPSr fN=1 EPSr fN=0 EPSr fC=1 EPSr fC=0 EPSr fV=1 EPSr fV=0 EPSr fC=1 and fZ=0 EPSr fC=0 or fZ=1 EPSr fNfV EPSr fN=fV EPSr fZ=1 or fNfV EPSr fZ=0 and fN=fV EPSr

5.5  Call and return

NEW(s)
S[SP][oo+A−1]← EP
EPSr
F[FP]← (FS(FP),FN(FP)−(p+1))
FF⊕ (SP+1,p+1) EPSc[oo+A−1]
KILL(c)
FF[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≤ osA.

5.6  Catch and throw

SrFP EPSr1
FF[1… Sr2]
SS[1… SP−1]⊕ Sr3

5.7  Stack

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

This document was translated from LATEX by HEVEA.

Last updated 2006/06/02