Skip to content

Commit 921ccae

Browse files
MesablooMesabloo
committed
split the 'mov' instruction into several distinct instructions
1 parent b217d12 commit 921ccae

File tree

7 files changed

+268
-14
lines changed

7 files changed

+268
-14
lines changed

‎part2-nstar.tex‎

Lines changed: 175 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -778,38 +778,200 @@ \subsection{Pointer offsetting using a register}\label{subsec:nstar-common-unsaf
778778

779779
\chapter{Instruction set}\label{chap:nstar-instructionset}
780780

781-
\section{\texttt{mov}}\label{sec:nstar-instructionset-mov}
781+
\section{\texttt{mv}}\label{sec:nstar-instructionset-mv}
782782

783-
The \texttt{mov} instruction moves a value into a register or at a given address (literal address or pointer address).
784-
Grammar is given in Figure~\ref{fig:nstar-instructionset-mov-grammar}.
785-
Type inference rules are given in Figure~\ref{fig:nstar-instructionset-mov-typerules}.
783+
The \texttt{mv} instruction moves a value (immediate value or stored in a register) into a register.
784+
Grammar is given in Figure~\ref{fig:nstar-instructionset-mv-grammar}.
785+
Type inference rules are given in Figure~\ref{fig:nstar-instructionset-mv-typerules}.
786786

787787
\begin{figure}[H]
788788
\centering
789789
\scalebox{.5}{
790790
\includegraphics{nstar/instructions/mov-grammar}
791791
}
792-
\caption{Grammar of the \texttt{mov} instruction.}
793-
\label{fig:nstar-instructionset-mov-grammar}
792+
\caption{Grammar of the \texttt{mv} instruction.}
793+
\label{fig:nstar-instructionset-mv-grammar}
794+
\end{figure}
795+
796+
\begin{figure}[H]
797+
\centering
798+
799+
\begin{prooftree}
800+
\hypo{$r, d are registers$}
801+
\hypo{\Xi;\chi;\sigma;\epsilon\vdash^T_{code}$ r : $\forall$().ctx$}
802+
\infer2[move cont from register to register]{\Xi;\chi;\sigma;$ r $\vdash^I$ mv r, d $\dashv\chi,$d : $\forall$().ctx$;\sigma;$ d$}
803+
\end{prooftree}
804+
\\\vspace{\baselineskip}
805+
\begin{prooftree}
806+
\hypo{$r is a register$}
807+
\hypo{$n $\leq 8}
808+
\hypo{\Gamma\vdash^K$ t : Tn$}
809+
\hypo{\Xi;\chi;\sigma;\epsilon\vdash^T_{code}$ e : t$}
810+
\infer4[move value to register]{\Xi;\chi;\sigma;\epsilon\vdash^I$ mv e, r $\dashv\chi\setminus$r, r : t$;\sigma;\epsilon}
811+
\end{prooftree}
812+
813+
\caption{Type inference rules for the \texttt{mv} instruction.}
814+
\label{fig:nstar-instructionset-mv-typerules}
815+
\end{figure}
816+
817+
\section{\texttt{sst}}\label{sec:nstar-instructionset-sst}
818+
819+
The \texttt{sst} instruction stores a value at the given index on the stack.
820+
Grammar and inference rules are given in Figure~\ref{fig:nstar-instructionset-sst-grammar} and Figure~\ref{fig:nstar-instructionset-sst-typerules}.
821+
822+
\begin{figure}[H]
823+
\centering
824+
825+
\scalebox{.5}{
826+
\includegraphics{nstar/instructions/sst-grammar}
827+
}
828+
829+
\caption{Grammar for the \texttt{sst} instruction.}
830+
\label{fig:nstar-instructionset-sst-grammar}
831+
\end{figure}
832+
833+
\begin{figure}[H]
834+
\centering
835+
836+
\begin{prooftree}
837+
\hypo{$r is a register$}
838+
\hypo{$n $\in\mathbb{N}}
839+
\hypo{\hat{\sigma}=$ t$_0$::t$_1$::\ldots::t$_p$::s$}
840+
\infer[no rule, rule margin=1.0ex]3{\Gamma\vdash^K$ t : T8\hspace{1.5em}$%
841+
$n $\leq$ p$}
842+
\infer[no rule, rule margin=1.0ex]1{\hat{\sigma}^\prime=\hat{\sigma}[\forall$().ctx$\setminus$t$_n]$\hspace{1.5em}$%
843+
\Xi;\chi;\hat{\sigma};\epsilon\vdash^T_{code}$ r : $\forall$().ctx\hspace{1.5em}$%
844+
$t$_n\sim$ t$}
845+
\infer1[store cont from register to stack]{\Xi;\chi;\hat{\sigma};$ r $\vdash^I$ sst r, n $\dashv\chi;\hat{\sigma}^\prime;$ n$}
846+
\end{prooftree}
847+
\\\vspace{\baselineskip}
848+
\begin{prooftree}
849+
\hypo{$n $\in\mathbb{N}}
850+
\hypo{\hat{\sigma}=$ t$_0$::t$_1$::\ldots::t$_p$::s$}
851+
\hypo{$n $\leq$ p$}
852+
\hypo{\Xi;\chi;\hat{\sigma};\epsilon\vdash^T_{code}$ e : t$_n}
853+
\infer4[store value in stack]{\Xi;\chi;\hat{\sigma};\epsilon\vdash^I$ sst e, n $\dashv\chi;\hat{\sigma};\epsilon}
854+
\end{prooftree}
855+
856+
857+
\caption{Type inference rules for the \texttt{sst} instruction.}
858+
\label{fig:nstar-instructionset-sst-typerules}
859+
\end{figure}
860+
861+
\section{\texttt{sld}}\label{sec:nstar-instructionset-sld}
862+
863+
The \texttt{sld} instruction stores the value at the given index on the stack in a register.
864+
Grammar and inference rules are given in Figure~\ref{fig:nstar-instructionset-sld-grammar} and Figure~\ref{fig:nstar-instructionset-sld-typerules}.
865+
866+
\begin{figure}[H]
867+
\centering
868+
869+
\scalebox{.5}{
870+
\includegraphics{nstar/instructions/sld-grammar}
871+
}
872+
873+
\caption{Grammar for the \texttt{sld} instruction.}
874+
\label{fig:nstar-instructionset-sld-grammar}
794875
\end{figure}
795876

796877
\begin{figure}[H]
797878
\centering
798879

799880
\begin{prooftree}
800-
\hypo{\Delta\vdash^T_{code}$ e : t$}
801881
\hypo{$r is a register$}
802-
\infer2[\texttt{mov} to register]{\Delta;\Xi\vdash^I$ mov e, r $\dashv\Delta\setminus$ r, r : t $}
882+
\hypo{$n $\in\mathbb{N}}
883+
\hypo{$n $\leq$ p$}
884+
\infer[no rule, rule margin=1.0ex]3{\hat{\sigma}=$ t$_0$::t$_1$::\ldots::t$_p$::s\hspace{1.5em}$%
885+
$t$_n\sim\forall$().ctx$}
886+
\infer1[load cont from stack in register]{\Xi;\chi;\hat{\sigma};$ n $\vdash^I$ sld n, r $\dashv\chi,$ r : t$_n;\hat{\sigma};$ r$}
803887
\end{prooftree}
804888
\\\vspace{\baselineskip}
805889
\begin{prooftree}
806-
\hypo{\Delta\vdash^T_{code}$ e : t$}
807-
\hypo{\Delta\vdash^T_{code}$ m(d) : t$}
808-
\infer2[\texttt{mov} to pointer offset]{\Delta;\Xi\vdash^I$ mov e, m(d) $\dashv\Delta}
890+
\hypo{$r is a register$}
891+
\hypo{$n, k $\in\mathbb{N}}
892+
\infer[no rule, rule margin=1.0ex]2{$n $\leq$ p\hspace{1.5em}$%
893+
$k $\leq8$\hspace{1.5em}$%
894+
\hat{\sigma}=$ t$_0$::t$_1$::\ldots::t$_p$::s\hspace{1.5em}$%
895+
\Gamma\vdash^K$ t$_n$ : Tk$}
896+
\infer1[load value from stack]{\Xi;\chi;\hat{\sigma};\epsilon\vdash^I$ sld n, r $\dashv\chi,$ r : t$_n;\hat{\sigma};\epsilon}
897+
\end{prooftree}
898+
899+
\caption{Type inference rules for the \texttt{sld} instruction.}
900+
\label{fig:nstar-instructionset-sld-typerules}
901+
\end{figure}
902+
903+
\section{\texttt{st}}\label{sec:nstar-instructionset-st}
904+
905+
The \texttt{st} instruction stores a value into a memory area denoted by pointer offset.
906+
The grammar and inference rules are given in Figure~\ref{fig:nstar-instructionset-st-grammar} and Figure~\ref{fig:nstar-instructionset-st-typerules}.
907+
908+
\begin{figure}[H]
909+
\centering
910+
911+
\scalebox{.5}{
912+
\includegraphics{nstar/instructions/st-grammar}
913+
}
914+
915+
\caption{Grammar for the \texttt{st} instruction.}
916+
\label{fig:nstar-instructionset-st-grammar}
917+
\end{figure}
918+
919+
\begin{figure}[H]
920+
\centering
921+
922+
\begin{prooftree}
923+
\hypo{\Xi;\chi;\sigma;\epsilon\vdash^T_{code}$ e : t$}
924+
\hypo{$e $\neq\epsilon}
925+
\hypo{\Xi;\chi;\sigma;\epsilon\vdash^T_{code}$ o(p) : *t$}
926+
\infer3[store value in pointer byte offset]{\Xi;\chi;\sigma;\epsilon\vdash^I$ st e, o(p) $\dashv\chi;\sigma;\epsilon}
927+
\end{prooftree}
928+
\\\vspace{\baselineskip}
929+
\begin{prooftree}
930+
\hypo{\Xi;\chi;\sigma;\epsilon\vdash^T_{code}$ e : t$}
931+
\hypo{$e $\neq\epsilon}
932+
\hypo{\Xi;\chi;\sigma;\epsilon\vdash^T_{code}$ p[o] : *t$}
933+
\infer3[store value in pointer base offset]{\Xi;\chi;\sigma;\epsilon\vdash^I$ st e, p[o] $\dashv\chi;\sigma;\epsilon}
934+
\end{prooftree}
935+
936+
\caption{Type inference rules for the \texttt{st} instruction.}
937+
\label{fig:nstar-instructionset-st-typerules}
938+
\end{figure}
939+
940+
\section{\texttt{ld}}\label{sec:nstar-instructionset-ld}
941+
942+
The \texttt{ld} instruction loads a value from a memory area into a register.
943+
Grammar and inference rules are given in Figure~\ref{fig:nstar-instructionset-ld-grammar} and Figure~\ref{fig:nstar-instructionset-ld-typerules}.
944+
945+
\begin{figure}[H]
946+
\centering
947+
948+
\scalebox{.5}{
949+
\includegraphics{nstar/instructions/ld-grammar}
950+
}
951+
952+
\caption{Grammar for the \texttt{ld} instruction.}
953+
\label{fig:nstar-instructionset-ld-grammar}
954+
\end{figure}
955+
956+
\begin{figure}[H]
957+
\centering
958+
959+
\begin{prooftree}
960+
\hypo{$r is a register$}
961+
\hypo{$r $\neq\epsilon}
962+
\hypo{\Xi;\chi;\sigma;\epsilon\vdash^T_{code}$ o(p) : *t$}
963+
\infer3[load value from pointer byte offset]{\Xi;\chi;\sigma;\epsilon\vdash^I$ ld o(p), r $\dashv\chi,$ r : t$;\sigma;\epsilon}
964+
\end{prooftree}
965+
\\\vspace{\baselineskip}
966+
\begin{prooftree}
967+
\hypo{$r is a register$}
968+
\hypo{$r $\neq\epsilon}
969+
\hypo{\Xi;\chi;\sigma;\epsilon\vdash^T_{code}$ p[o] : *t$}
970+
\infer3[load value from pointer base offset]{\Xi;\chi;\sigma;\epsilon\vdash^I$ ld p[o], r $\dashv\chi,$ r : t$;\sigma;\epsilon}
809971
\end{prooftree}
810972

811-
\caption{Type inference rules for the \texttt{mov} instruction.}
812-
\label{fig:nstar-instructionset-mov-typerules}
973+
\caption{Type inference rules for the \texttt{ld} instruction.}
974+
\label{fig:nstar-instructionset-ld-typerules}
813975
\end{figure}
814976

815977
\section{\texttt{jmp}}\label{sec:nstar-instructionset-jmp}

‎railroad-diagrams.py‎

Lines changed: 93 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -427,4 +427,96 @@ def udata_line():
427427

428428
return mk_diagram('udata-line', inner)
429429

430-
ptr_offset().writeSvg(sys.stdout.write)
430+
def mv_instruction():
431+
inner = Sequence(
432+
Terminal('mv'),
433+
Group(
434+
Choice(
435+
0,
436+
NonTerminal('register'),
437+
NonTerminal('integer-value')
438+
),
439+
'source'
440+
),
441+
Terminal(','),
442+
Group(
443+
NonTerminal('register'),
444+
'destination'
445+
)
446+
)
447+
448+
return mk_diagram('mv-instruction', inner)
449+
450+
def sst_instruction():
451+
inner = Sequence(
452+
Terminal('sst'),
453+
Group(
454+
Choice(
455+
0,
456+
NonTerminal('register'),
457+
NonTerminal('integer-value')
458+
),
459+
'source'
460+
),
461+
Terminal(','),
462+
Group(
463+
NonTerminal('positive-integer'),
464+
'stack index destination'
465+
)
466+
)
467+
468+
return mk_diagram('sst-instruction', inner)
469+
470+
def sld_instruction():
471+
inner = Sequence(
472+
Terminal('sld'),
473+
Group(
474+
NonTerminal('positive-integer'),
475+
'stack index source'
476+
),
477+
Terminal(','),
478+
Group(
479+
NonTerminal('register'),
480+
'destination'
481+
)
482+
)
483+
484+
return mk_diagram('sld-instruction', inner)
485+
486+
def st_instruction():
487+
inner = Sequence(
488+
Terminal('st'),
489+
Group(
490+
Choice(
491+
0,
492+
NonTerminal('register'),
493+
NonTerminal('integer-value')
494+
),
495+
'source'
496+
),
497+
Terminal(','),
498+
Group(
499+
NonTerminal('pointer-offset'),
500+
'destination'
501+
)
502+
)
503+
504+
return mk_diagram('st-instruction', inner)
505+
506+
def ld_instruction():
507+
inner = Sequence(
508+
Terminal('ld'),
509+
Group(
510+
NonTerminal('pointer-offset'),
511+
'source'
512+
),
513+
Terminal(','),
514+
Group(
515+
NonTerminal('register'),
516+
'destination'
517+
)
518+
)
519+
520+
return mk_diagram('ld-instruction', inner)
521+
522+
ld_instruction().writeSvg(sys.stdout.write)

‎res/nstar/instructions/ld-grammar.png‎

10.4 KB
Loading

‎res/nstar/instructions/mov-grammar.png‎

2.02 KB
Loading

‎res/nstar/instructions/sld-grammar.png‎

11.8 KB
Loading

‎res/nstar/instructions/sst-grammar.png‎

14.6 KB
Loading

‎res/nstar/instructions/st-grammar.png‎

13.7 KB
Loading

0 commit comments

Comments
 (0)