Mite’s semanticsReuben Thomas25th 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:
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
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 by H^{E}V^{E}A.
Last updated 2006/06/02