# source:Deliverables/D1.2/CompilerProofOutline/outline.tex@1717

Last change on this file since 1717 was 1717, checked in by mulligan, 9 years ago

added diagrams.sty for drawing commutative diagrams

File size: 3.6 KB
Line
1\documentclass[a4paper, 10pt]{article}
2
3\usepackage{a4wide}
4\usepackage{amsfonts}
5\usepackage{amsmath}
6\usepackage{amssymb}
7\usepackage[english]{babel}
8\usepackage{diagrams}
10\usepackage{microtype}
11
12\title{Proof outline for the correctness of the CerCo compiler}
13\date{\today}
14\author{The CerCo team}
15
16\begin{document}
17
18\maketitle
19
20\section{Introduction}
21\label{sect.introduction}
22
23\section{The RTLabs to RTL translation}
24\label{sect.rtlabs.rtl.translation}
25
26% dpm: type system and casting load (???)
27We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model:
28
29\begin{displaymath}
30\mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{int}_i \mid \mathtt{ptr}_i
31\end{displaymath}
32
33We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
34
35\begin{displaymath}
36\mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha)
37\end{displaymath}
38
39where
40
41\begin{displaymath}
42\mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
43\end{displaymath}
44
45\begin{displaymath}
46\mathtt{BEMem} = \mathtt{Mem} \mathtt{Value}
47\end{displaymath}
48
49\begin{displaymath}
50\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
51\end{displaymath}
52
53\begin{displaymath}
54\mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null})
55\end{displaymath}
56
57\begin{center}
58\begin{picture}(2, 2)
59% picture of sigma mapping memory to memory
60TODO
61\end{picture}
62\end{center}
63
64\begin{displaymath}
65\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
66\end{displaymath}
67
68\begin{displaymath}
69\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
70\end{displaymath}
71
72\begin{displaymath}
73\begin{array}{rll}
74\mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
75               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
76               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
77\end{array}
78\end{displaymath}
79
80\begin{displaymath}
81\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
82\end{displaymath}
83
84\begin{displaymath}
85\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
86\end{displaymath}
87
88\begin{displaymath}
89\sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{Frame})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem}))
90\end{displaymath}
91
92\begin{displaymath}
93\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
94\end{displaymath}
95
96\begin{displaymath}
97\sigma(\mathtt{State}(-)) \longrightarrow \sigma \circ \text{state one step}
98\end{displaymath}
99
100\begin{diagram}
101\end{diagram}
102
103\section{The RTL to ERTL translation}
104\label{sect.rtl.ertl.translation}
105
106\section{The ERTL to LTL translation}
107\label{sect.ertl.ltl.translation}
108
109\section{The LTL to LIN translation}
110\label{sect.ltl.lin.translation}
111
112\section{The LIN to ASM translation}
113\label{sect.lin.asm.translation}
114
115\section{The ASM to MCS-51 machine code translation}
116\label{sect.asm.mcs-51.machine.code.translation}
117
118\end{document}
Note: See TracBrowser for help on using the repository browser.