source: C-semantics/8051-Memory/memory.tex @ 149

Last change on this file since 149 was 149, checked in by campbell, 9 years ago

Fill in a few details about 8051 extensions.

File size: 9.9 KB
Line 
1\documentclass[a4paper]{article}
2\usepackage{graphics}
3\usepackage{listings}
4
5\lstset{language=C,basicstyle=\small\tt,columns=flexible,breaklines=false,
6        % numbers=left, numberstyle=\tiny, stepnumber=2, numbersep=5pt
7        %keywordstyle=\color{red}\bfseries,
8        %keywordstyle=[2]\color{blue},
9        %commentstyle=\color{green},
10        %stringstyle=\color{blue},
11        showspaces=false,showstringspaces=false}
12
13\newcommand{\sdcc}{\texttt{sdcc}}
14
15\begin{document}
16\title{C extensions for the 8051}
17\maketitle
18
19The 8051 (as modern implementations have it) features a rather complex memory
20arrangement, see Figure~\ref{fig:memory}.  This document outlines the C
21extensions present in the \sdcc\ compiler for dealing with them, and suggests
22what the corresponding extensions in the CerCo project should be.
23
24\begin{figure}[h]
25\setlength{\unitlength}{1pt}
26\begin{picture}(410,250)(-50,200)
27%\put(-50,200){\framebox(410,250){}}
28\put(12,410){\makebox(80,0)[b]{Internal (256B)}}
29\put(13,242){\line(0,1){165}}
30\put(93,242){\line(0,1){165}}
31\put(13,407){\line(1,0){80}}
32\put(12,400){\makebox(0,0)[r]{0h}}  \put(14,400){\makebox(0,0)[l]{Register bank 0}}
33\put(13,393){\line(1,0){80}}
34\put(12,386){\makebox(0,0)[r]{8h}}  \put(14,386){\makebox(0,0)[l]{Register bank 1}}
35\put(13,379){\line(1,0){80}}
36\put(12,372){\makebox(0,0)[r]{10h}}  \put(14,372){\makebox(0,0)[l]{Register bank 2}}
37\put(13,365){\line(1,0){80}}
38\put(12,358){\makebox(0,0)[r]{18h}} \put(14,358){\makebox(0,0)[l]{Register bank 3}}
39\put(13,351){\line(1,0){80}}
40\put(12,344){\makebox(0,0)[r]{20h}} \put(14,344){\makebox(0,0)[l]{Bit addressable}}
41\put(13,323){\line(1,0){80}}
42\put(12,316){\makebox(0,0)[r]{30h}}
43  \put(14,309){\makebox(0,0)[l]{\quad \vdots}}
44\put(13,291){\line(1,0){80}}
45\put(12,284){\makebox(0,0)[r]{80h}}
46  \put(14,263){\makebox(0,0)[l]{\quad \vdots}}
47\put(12,249){\makebox(0,0)[r]{ffh}}
48\put(13,242){\line(1,0){80}}
49
50\qbezier(-2,407)(-6,407)(-6,393)
51\qbezier(-6,393)(-6,324)(-10,324)
52\put(-12,324){\makebox(0,0)[r]{indirect}}
53\qbezier(-6,256)(-6,324)(-10,324)
54\qbezier(-2,242)(-6,242)(-6,256)
55
56\qbezier(94,407)(98,407)(98,393)
57\qbezier(98,393)(98,349)(102,349)
58\put(104,349){\makebox(0,0)[l]{direct/stack}}
59\qbezier(98,305)(98,349)(102,349)
60\qbezier(94,291)(98,291)(98,305)
61
62\put(102,242){\framebox(20,49){sfr}}
63% bit access to sfrs?
64
65\qbezier(124,291)(128,291)(128,277)
66\qbezier(128,277)(128,266)(132,266)
67\put(134,266){\makebox(0,0)[l]{direct}}
68\qbezier(128,257)(128,266)(132,266)
69\qbezier(124,242)(128,242)(128,256)
70
71\put(164,410){\makebox(80,0)[b]{External (64kB)}}
72\put(164,220){\line(0,1){187}}
73\put(164,407){\line(1,0){80}}
74\put(244,220){\line(0,1){187}}
75\put(164,242){\line(1,0){80}}
76\put(163,400){\makebox(0,0)[r]{0h}}
77\put(164,324){\makebox(80,0){paged access}}
78  \put(164,310){\makebox(80,0){direct/indirect}}
79\put(163,235){\makebox(0,0)[r]{80h}}
80  \put(164,228){\makebox(80,0){\vdots}}
81  \put(164,210){\makebox(80,0){direct/indirect}}
82
83\put(264,410){\makebox(80,0)[b]{Code (64kB)}}
84\put(264,220){\line(0,1){187}}
85\put(264,407){\line(1,0){80}}
86\put(344,220){\line(0,1){187}}
87\put(263,400){\makebox(0,0)[r]{0h}}
88  \put(264,228){\makebox(80,0){\vdots}}
89  \put(264,324){\makebox(80,0){direct}}
90  \put(264,310){\makebox(80,0){PC relative}}
91
92\end{picture}
93\caption{(extended) 8051 memory layout --- not to scale}
94\label{fig:memory}
95\end{figure}
96
97\section{\sdcc\ extensions}
98
99\sdcc\ adds a number of \emph{storage classes} to the standard C classes
100(\lstinline'auto', \lstinline'extern', and so on) to specify the memory space
101that should be used for storage.  They can also be used to refine pointer
102types for particular areas\footnote{One side effect of this dual meaning is
103that they appear as \emph{type specifiers} in the extended C grammar.}.  The
104new storage classes and corresponding pointer sizes are:
105\begin{table}[ht]
106\begin{tabular}{rcl}
107Attribute & Pointer size & Memory space \\\hline
108\lstinline'__data' & 1 & Internal, first half (0h -- 7fh) \\
109\lstinline'__idata' & 1 & Internal, indirect only (80h -- ffh) \\
110\lstinline'__pdata' & 1 & External, page access (usually 0h -- 7fh) \\
111\lstinline'__xdata' & 2 & External, any (0h -- ffffh) \\
112\lstinline'__code' & 2 & Code, any (0h -- ffffh) \\
113\emph{none}& 3 & Any / Generic pointer
114\end{tabular}
115\end{table}
116
117There are two areas of overlap between these classes: generic pointers overlap
118with everything else and one page of external memory can be accessed by both
119\lstinline'__pdata' and \lstinline'__xdata' pointers.
120
121Two types with an implied storage class are also defined.  The
122\lstinline'__bit' type declare a single bit variable, and \lstinline'__sbit',
123\lstinline'__sfr', \lstinline'__sfr16' and \lstinline'__sfr32' declare
124`variables' which access the \emph{Special Function Registers} (SFR).
125Pointers to these types are not allowed --- the corresponding 8051 instructions
126only allow direct addressing for them.
127
128These are all defined in Section~3.4.1 of the \sdcc\ manual.
129
130Explicit addresses can be given for variables, using the
131\lstinline'__at (0x1234)' syntax.  From the manual, it appears that these are
132sometimes used with \lstinline'volatile' in preference to using the SFR types,
133or where memory mapped I/O appears in the extended memory space.
134
135\subsection{Pointer operations}
136
137C allows pointers to be compared for equality and order, have integers added
138to them, and for subtraction of two pointers to yield an integer difference.
139
140\sdcc\ forbids comparison between incompatible pointer types, allows some
141form of subtraction for mixed pointers (even though it doesn't make much
142sense) and appears to reject mixed order comparisons, even when one of the
143pointers is generic.
144
145\section{Proposals}
146
147Where these are more restrictive than \sdcc, the intention is to prevent
148aliasing or reduce complexity.
149
150\begin{itemize}
151\item Allow each of the ordinary storage classes from \sdcc, but forbid
152explicit addresses except for \lstinline'volatile' variables.  Note that this
153means that the semantics do not include accessing registers through a pointer.
154\item Leave out bit variables(?), provide `external functions' in the CompCert
155sense for bit access to SFRs but compile them to the corresponding instruction.\\
156CSC: this is unclear to me. In order to address SFR's bits, this is easily achieved. But for the first half of the bit address space (the real bits), this is not the case since only a few bytes can be accessed this way. Thus, if the compiler wants to exploit bit variables, it must do some spilling and keep the bits in the right memory area.
157\item Allow casting (and automatic promotion?) to generic pointer types.
158\item Only provide equality, ordering and subtraction operations on pointer
159types with the same class (with promotion to generic?).  Note that comparison
160between pointers to different blocks is not specified by C or CompCert anyway.
161\end{itemize}
162There are no alignment constraints on the 8051.
163
164\section{Impact on formal C semantics}
165
166Values, types and the memory model are changed as follows:
167\begin{itemize}
168\item Each pointer value has a `class' associated with it, either generic or
169identifying a particular memory space.  Each pointer type has a corresponding
170space, too.
171\item Array types are also given a space, because the underlying values are
172pointers.
173\item Each block has a class associated with it, either `unspecified' or
174identifying a particular memory space.
175\end{itemize}
176The behaviour of casts between pointer types is defined only when the target
177pointer type is suitable for the memory space pointed at.  Thus casts now
178depend upon the memory rather than just the values and types.
179
180Stack memory is treated as in some `unspecified' space at present.  This has
181the problem that only generic pointers may be used to refer to it.  It may
182be possible to parametrise the semantics by the stack memory space to allow
183for a choice of memory model (like the \texttt{--model-}$\star$ options in
184\sdcc{}).
185
186SFR access (both by byte and by bit) do not require any changes as they will
187be implemented as `external' I/O functions.
188
189The definitions for alignment constraints from CompCert may be kept for
190consistency with CompCert, but made vacuous by only `requiring' byte alignment.
191Note that the size of pointer depends on the memory space associated with its
192type, and that we need to deal with 24 bit `chunks' for generic pointer values.
193
194\section{Changes to CIL and Clight conversion}
195
196The prototype compiler uses the CIL-derived C parser from CompCert.  This can
197be altered to accept the memory spaces as extra attributes for declarations.
198Note that this allows them to appear in meaningless places (such as local
199variable declarations which are always held in stack or registers), which
200ought to be rejected during translation to Clight.
201
202As an extreme example, consider the following:
203\begin{lstlisting}
204(* fn1 is a global variable located in idata memory,
205   which contains a pointer to a value in code memory,
206   which is a function that takes and returns a pointer to an integer in xdata.
207 *)
208__xdata int * __code (* __idata fn1)(__xdata int *);
209\end{lstlisting}
210
211As noted above, the Clight abstract syntax trees are extended by memory spaces
212added to the pointer and array types, and added to global variable declarations.
213To support this, the transformations in CIL are extended to keep track of the
214memory space for each expression during elaboration so that the appropriate
215pointer types and casts are inserted.
216
217The Clight version of the above variable declaration is:
218\begin{lstlisting}
219(mk_pair ?? (mk_pair ?? (mk_pair ?? (succ_pos_of_nat 143 (* fn1 *))
220    [(Init_space 4) ]) IData)
221    (Tpointer Code (Tfunction (Tcons (Tpointer XData (Tint I32 Signed  )) Tnil)
222                              (Tpointer XData (Tint I32 Signed  )))))]
223\end{lstlisting}
224
225\begin{verbatim}
226TODO:
227
228Infinite abstract memory model?
229Concrete memory model at end?
230CIL changes?
231Null pointer (choice shouldn't affect C semantics?)
232
233Mention integer sizes in passing?
234Conversion to integer representation?
235
236CONSTANTS - always located in Code if address taken?
237\end{verbatim}
238
239\end{document}
Note: See TracBrowser for help on using the repository browser.