%
% Mite's semantics
%
% Reuben Thomas
%
% made HeVeA-friendly 2/6/06
%


\documentclass{article}
\usepackage{a4,mite}
\renewcommand{\isdefinedas}{:}


\title{Mite's semantics}
\author{Reuben Thomas}
\date{25th October 2000}

\begin{document}
\maketitle

\section{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.


\section{Definitions}

\begin{description}
\item [Quantity]a string of bits
\item [${q[i\dots j]}$]the quantity consisting of bits $i$ to $j$ inclusive of quantity $q$
\item [Width]the number of bits in a quantity
\item [$A$]either $32$ or $64$
\item [Word]an $A$-bit quantity
\item [$w$-aligned]a multiple of $w$
\item [Size]an expression of the form $b+w+r$, where $b$, $w$, and $r$ are non-negative integers, whose value is $b+Aw+32\left\lfloor A/64\right\rfloor r$
\item [$\rho $]an undefined quantity of infinite width
\item [${[S]}$]a bit representing the truth of statement $S$; if $S$ is true then $[S]$ is one, otherwise it is zero
\item [$q\leftarrow 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$
\item [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
\item [${s[i]}$]the $i$th item of stack $s$
\item [${s[i\dots j]}$]the stack consisting of items $i$ to $j$ inclusive of stack $s$
\item [$s\oplus E$]the stack $s$ with an extra item added whose value is $E$
\end{description}

\section{State} \label{sem:state}

Mite's state consists of the following elements:

\begin{description}
\item [Flags~$f_{Z}$,~$f_{N}$,~$f_{C}$,~$f_{V}$]one bit each
\item [Execution~pointer~$\mathit{EP}$]a word
\item [Temporary~register~$T$]a word
\item [Memory~$M$]a quantity
\item [Permutation~functions~$p_{8}$,~$p_{16}$,~$p_{32}$,~$p_{A}$]~
\item [Stack~$S$]a stack
\item [Frame~stack~$F$]a stack
\end{description}
An index into $M$ is called an \define{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. $\mathit{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 $i$th item of $F$. A \define{stack position} is a natural $p$ in the range $1\dots F_{N}(FP)$.

$S$ holds items of two sorts: a \define{register} is a word created by \abs{NEW}$()$, and a \define{chunk} is a quantity of arbitrary size created by \abs{NEW}$(c)$ (see section~\ref{sem:stack}). The stack items are held in $M$ at word-aligned addresses.

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


\section{Program}

An \define{instruction} consists of an operation and a tuple of operands. Each operand has a \define{type}, given by its name; a subscript is added to distinguish operands of the same type. The allowable instructions are given in section~\ref{sem:instruction}. The program $P$ is an array of instructions; $P[i]$ denotes the $i$th element of $P$.

The types are:

\begin{description}
\item [Stack~position~$p$]a stack position
\item [Natural~$n$]a non-negative integer
\item [Register~$r$]a stack position $p$ such that $S_{p}$ is a register, or $T$
\item [Chunk~$c$]a stack position $p$ such that $S_{p}$ is a chunk
\item [Width~$w$]a member of the set $\{8,16,32,A\}$
\item [Size~$s$]a size
\end{description}

\section{Instructions\label{sem:instruction}}

The state is transformed by repeatedly performing $\mathit{EP}\leftarrow \mathit{EP}+1$ then the semantics of $P[\mathit{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\leftarrow \rho$ prepended, and also, for all instructions except branches (see section~\ref{sem:branch}), the following:

\begin{center}
$f_{Z}\leftarrow \rho $\\
$f_{N}\leftarrow \rho $\\
$f_{C}\leftarrow \rho $\\
$f_{V}\leftarrow \rho $
\end{center}

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

\subsection{Assignment}

\noindent \begin{bnfa}
\item[MOV$(r_{1},r_{2})$] $S_{r_{1}}\leftarrow S_{r_{2}}$\\
$f_{Z}\leftarrow [S_{r_{1}}=0]$\\
$f_{N}\leftarrow [S_{r_{1}}<0]$
\item[MOV$(r,c)$]$S_{r}\leftarrow \&S_{c}$\\
$f_{Z}\leftarrow [S_{r_{1}}=0]$
\item[SWAP$(r_{1},r_{2})$]$T\leftarrow S_{r_{1}}$\\
$S_{r_{1}}\leftarrow S_{r_{2}}$\\
$S_{r_{2}}\leftarrow T$
\end{bnfa}


\subsection{Data processing}

All the data processing instructions except \abs{MUL}, \abs{DIV\opt{S\opt{Z}}} and \abs{REM\opt{S\opt{Z}}} have

\begin{center}
$f_{Z}\leftarrow [S_{r_{1}}=0]$

$f_{N}\leftarrow [S_{r_{1}}<0]$
\end{center}
\noindent appended to the end of their semantics.


\subsubsection{Arithmetic}

\noindent \begin{bnfa*}
\item[NEG$(r_{1},r_{2})$]$S_{r_{1}}\leftarrow -S_{r_{2}}$\\
$f_{C}\leftarrow $ [$S_{r_{1}}=0$]\\
$f_{V}\leftarrow $ [$S_{r_{1}}=-2^{A-1}$]
\item[ADD$(r_{1},r_{2},r_{3})$]$S_{r_{1}}\leftarrow S_{r_{2}}+S_{r_{3}}$\\
$f_{C}\leftarrow $ carry out of most significant bit\\
$f_{V}\leftarrow $ [signed overflow occurred]
\item[SUB$(r_{1},r_{2},r_{3})$]$S_{r_{1}}\leftarrow S_{r_{2}}-S_{r_{3}}$\\
$f_{C}\leftarrow $ carry out of most significant bit\\
$f_{V}\leftarrow $ [signed overflow occurred]
\item[MUL$(r_{1},r_{2},r_{3})$]$S_{r_{1}}\leftarrow S_{r_{2}}\times S_{r_{3}}$
\item[DIV$(r_{1},r_{2},r_{3})$]\sidecond{$S_{r_{3}}\neq 0$} $S_{r_{1}}\leftarrow S_{r_{2}}\div S_{r_{3}}$, treating $S_{r_{2}}$ and $S_{r_{3}}$ as unsigned, and rounding the quotient to $0$
\item[DIVS$(r_{1},r_{2},r_{3})$]\sidecond{$S_{r_{3}}\neq 0$} $S_{r_{1}}\leftarrow S_{r_{2}}\div S_{r_{3}}$, treating $S_{r_{2}}$ and $S_{r_{3}}$ as signed, and rounding the quotient to $-\infty $
\item[DIVSZ$(r_{1},r_{2},r_{3})$]\sidecond{$S_{r_{3}}\neq 0$} $S_{r_{1}}\leftarrow S_{r_{2}}\div S_{r_{3}}$, treating $S_{r_{2}}$ and $S_{r_{3}}$ as signed, and rounding the quotient to $0$
\item[REM$(r_{1},r_{2},r_{3})$]\abs{DIV}$(T,r_{2},r_{3})$\\
$r_{1}\leftarrow r_{2}-T\times r_{3}$
\item[REMS$(r_{1},r_{2},r_{3})$]\abs{DIVS}$(T,r_{2},r_{3})$\\
$r_{1}\leftarrow r_{2}-T\times r_{3}$
\item[REMSZ$(r_{1},r_{2},r_{3})$]\abs{DIVSZ}$(T,r_{2},r_{3})$\\
$r_{1}\leftarrow r_{2}-T\times r_{3}$
\end{bnfa*}


\subsubsection{Logic}

\noindent \begin{bnfa*}
\item[NOT$(r_{1},r_{2})$]$S_{r_{1}}\leftarrow $ one's complement of $S_{r_{2}}$
\item[AND$(r_{1},r_{2},r_{3})$]$S_{r_{1}}\leftarrow $ bitwise and of $S_{r_{2}}$ and $S_{r_{3}}$
\item[OR$(r_{1},r_{2},r_{3})$]$S_{r_{1}}\leftarrow $ bitwise or of $S_{r_{2}}$ and $S_{r_{3}}$
\item[XOR$(r_{1},r_{2},r_{3})$]$S_{r_{1}}\leftarrow $ bitwise exclusive-or of $S_{r_{2}}$ and $S_{r_{3}}$
\item[SL$(r_{1},r_{2},r_{3})$]\sidecond{$0\leq S_{r_{3}}\leq A$} $S_{r_{1}}\leftarrow S_{r_{2}}$ shifted left $S_{r_{3}}$ places\\
$f_{C}\leftarrow $ carry out of most significant bit, if $S_{r_{3}}>0$
\item[SRL$(r_{1},r_{2},r_{3})$]\sidecond{$0\leq S_{r_{3}}\leq A$} $S_{r_{1}}\leftarrow S_{r_{2}}$ shifted right logically $S_{r_{3}}$ places\\
$f_{C}\leftarrow $ carry out of least significant bit, if $S_{r_{3}}>0$
\item[SRA$(r_{1},r_{2},r_{3})$]\sidecond{$0\leq S_{r_{3}}\leq A$} $S_{r_{1}}\leftarrow S_{r_{2}}$ shifted right arithmetically $S_{r_{3}}$ places\\
$f_{C}\leftarrow $ carry out of least significant bit, if $S_{r_{3}}>0$
\end{bnfa*}


\subsection{Memory}

\noindent \begin{bnfa}
\item[LD$(w,r_{1},r_{2})$]$S_{r_{1}}\leftarrow 0$\\
$S_{r_{1}}[0\dots w-1]\leftarrow p_{w}(M[S_{r_{2}}\dots S_{r_{2}}+w-1])$
\item[ST$(w,r_{1},r_{2})$]$M[S_{r_{2}}\dots S_{r_{2}}+w-1]\leftarrow p_{w}^{-1}(S_{r_{1}}[0\dots w-1])$
\item[COPY$(s,r_{1},r_{2})$]\sidecond{$S_{r_{1}}+s\leq S_{r_{2}}$ or $S_{r_{2}}+s\leq S_{r_{1}}$} $M[S_{r_{1}}\dots S_{r_{1}}+s-1]\leftarrow M[S_{r_{2}}\dots S_{r_{2}}+s-1]$
\item[COPY$(s,r,c)$]\sidecond{$S_{r}+s\leq \&S_{c}$ or $\&S_{c}+s\leq S_{r}$} $M[S_{r}\dots S_{r}+s-1]\leftarrow M[\&S_{c}\dots \&S_{c}+s-1]$
\item[COPY$(s,c,r)$]\sidecond{$\&S_{c}+s\leq S_{r}$ or $S_{r}+s\leq \&S_{c}$} $M[\&S_{c}\dots \&S_{c}+s-1]\leftarrow M[S_{r}\dots S_{r}+s-1]$
\item[COPY$(s,c_{1},c_{2})$]\sidecond{$\&S_{c_{1}}+s\leq \&S_{c_{2}}$ or $\&S_{c_{2}}+s\leq \&S_{c_{1}}$} $M[\&S_{c_{1}}\dots \&S_{c_{1}}+s-1]\leftarrow M[\&S_{c_{2}}\dots \&S_{c_{2}}+s-1]$
\end{bnfa}


\subsection{Branch\label{sem:branch}}

\noindent \begin{bnfa*}
\item[BAL$(r)$]$\mathit{EP}\leftarrow S_{r}$
\item[BEQ$(r)$]\sidecond{$f_{Z}=1$}
$\mathit{EP}\leftarrow S_{r}$
\item[BNE$(r)$]\sidecond{$f_{Z}=0$}
$\mathit{EP}\leftarrow S_{r}$
\item[BMI$(r)$]\sidecond{$f_{N}=1$}
$\mathit{EP}\leftarrow S_{r}$
\item[BPL$(r)$]\sidecond{$f_{N}=0$}
$\mathit{EP}\leftarrow S_{r}$
\item[BCS$(r)$]\sidecond{$f_{C}=1$}
$\mathit{EP}\leftarrow S_{r}$
\item[BCC$(r)$]\sidecond{$f_{C}=0$}
$\mathit{EP}\leftarrow S_{r}$
\item[BVS$(r)$]\sidecond{$f_{V}=1$}
$\mathit{EP}\leftarrow S_{r}$
\item[BVC$(r)$]\sidecond{$f_{V}=0$}
$\mathit{EP}\leftarrow S_{r}$
\item[BHI$(r)$]\sidecond{$f_{C}=1$ and $f_{Z}=0$}
$\mathit{EP}\leftarrow S_{r}$
\item[BLS$(r)$]\sidecond{$f_{C}=0$ or $f_{Z}=1$}
$\mathit{EP}\leftarrow S_{r}$
\item[BLT$(r)$]\sidecond{$f_{N}\neq f_{V}$}
$\mathit{EP}\leftarrow S_{r}$
\item[BGE$(r)$]\sidecond{$f_{N}=f_{V}$}
$\mathit{EP}\leftarrow S_{r}$
\item[BLE$(r)$]\sidecond{$f_{Z}=1$ or $f_{N}\neq f_{V}$} $\mathit{EP}\leftarrow S_{r}$
\item[BGT$(r)$]\sidecond{$f_{Z}=0$ and $f_{N}=f_{V}$} $\mathit{EP}\leftarrow S_{r}$
\end{bnfa*}


\subsection{Call and return}

\noindent \begin{bnfa}
\item[CALL$(r,p)$]\abs{NEW}$(s)$\\
$S[\mathit{SP}][o\dots o+A-1]\leftarrow \mathit{EP}$\\
$\mathit{EP}\leftarrow S_{r}$\\
$F[\mathit{FP}]\leftarrow (F_{S}(\mathit{FP}),F_{N}(\mathit{FP})-(p+1))$\\
$F\leftarrow F\oplus (\mathit{SP}+1,p+1)$
\item[RET$(c)$]$\mathit{EP}\leftarrow S_{c}[o\dots o+A-1]$\\
\abs{KILL}$(c)$\\
$F\leftarrow F[1\dots \mathit{FP}-2]\oplus (F_{S}(\mathit{FP}-1),F_{N}(\mathit{FP}-1)+F_{N}(\mathit{FP}))$
\end{bnfa}

\noindent $o$ and $s$ may vary between instructions, but should be the same for corresponding \abs{CALL}s and \abs{RET}s; $s$ is at least $A$, and $0\leq o\leq s-A$.


\subsection{Catch and throw}

\begin{bnfa}
\item[CATCH$(r)$]$S_{r}\leftarrow \mathit{FP}$
\item[THROW$(r_{1},r_{2},r_{3})$]$\mathit{EP}\leftarrow S_{r_{1}}$\\
$F\leftarrow F[1\dots S_{r_{2}}]$\\
$S\leftarrow S[1\dots \mathit{SP}-1]\oplus S_{r_{3}}$
\end{bnfa}


\subsection{Stack\label{sem:stack}}

\noindent \begin{bnfa}
\item[NEW$()$]$S\leftarrow S\oplus \rho [0\dots A-1]$\\
$F[\mathit{FP}]\leftarrow (F_{S}(\mathit{FP}),F_{N}(\mathit{FP})+1)$
\item[NEW$(s)$]$S\leftarrow S\oplus \rho [0\dots s-1]$\\
$F[\mathit{FP}]\leftarrow (F_{S}(\mathit{FP}),F_{N}(\mathit{FP})+1)$
\item[KILL$(p)$]$S[F_{S}(FP)+p-1\dots \mathit{SP}-1]\leftarrow S[F_{S}(FP)+p\dots \mathit{SP}]$\\
$F[\mathit{FP}]\leftarrow (F_{S}(\mathit{FP}),F_{N}(\mathit{FP})-1)$\\
$S\leftarrow S[1\dots \mathit{SP}]$
\end{bnfa}

\end{document}
