Changeset 157
- Timestamp:
- Oct 6, 2010, 4:21:10 PM (11 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
C-semantics/8051-Memory/memory.tex
r149 r157 150 150 \begin{itemize} 151 151 \item Allow each of the ordinary storage classes from \sdcc, but forbid 152 explicit addresses except for \lstinline'volatile' variables. Note that this 153 means that the semantics do not include accessing registers through a pointer. 154 \item Leave out bit variables(?), provide `external functions' in the CompCert 155 sense for bit access to SFRs but compile them to the corresponding instruction.\\ 156 CSC: 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. 152 explicit addresses except for \lstinline'volatile' variables. The compiler 153 should ensure that \lstinline'volatile' variables do not overlap with any 154 non-\lstinline'volatile' data. Note that this means that the semantics do not 155 include accessing registers through a pointer. 156 \item No bit variables are provided to the programmer (although the compiler 157 could choose to use them internally). 158 \item Bit and byte access to SFRs will be provided by `external functions' (in the CompCert sense). They could be compiled to the corresponding instruction 159 rather than implemented with actual functions. 160 \item Casting between pointer types for different memory space attributes is 161 defined when the pointer can be represented in both. In particular, conversion 162 to and from a generic pointer type to a specific memory area pointer type is 163 guaranteed to work on values pointing to that memory area, and conversions 164 between \lstinline'__pdata' and \lstinline'__xdata' pointers will work on 165 values that point to the \lstinline'__pdata' space. Other conversions are 166 undefined. 167 \item Zeros of any integer type can be converted to any pointer type to give 168 a null pointer. Conversions of any other integer are undefined. [We could 169 extend this to give a semantics for more conversions, or restrict it to 170 only deal with integer constant zeros.] 158 171 \item Only provide equality, ordering and subtraction operations on pointer 159 172 types with the same class (with promotion to generic?). Note that comparison 160 173 between pointers to different blocks is not specified by C or CompCert anyway. 174 \item String literals are placed in \lstinline'__code' memory. 161 175 \end{itemize} 162 176 There are no alignment constraints on the 8051. … … 202 216 As an extreme example, consider the following: 203 217 \begin{lstlisting} 204 (* fn1 is a global variable located in idata memory,218 /* fn1 is a global variable located in idata memory, 205 219 which contains a pointer to a value in code memory, 206 220 which is a function that takes and returns a pointer to an integer in xdata. 207 * )221 */ 208 222 __xdata int * __code (* __idata fn1)(__xdata int *); 209 223 \end{lstlisting} … … 223 237 \end{lstlisting} 224 238 225 \begin{verbatim}226 TODO:227 228 Infinite abstract memory model?229 Concrete memory model at end?230 CIL changes?231 Null pointer (choice shouldn't affect C semantics?)232 233 Mention integer sizes in passing?234 Conversion to integer representation?235 236 CONSTANTS - always located in Code if address taken?237 \end{verbatim}238 239 239 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.