Changeset 157

Timestamp:

Oct 6, 2010, 4:21:10 PM (9 years ago)

Author:

campbell

Message:

Make proposed memory spaces semantics more explicit.

File:

• C-semantics/8051-Memory/memory.tex (modified) (3 diffs)

C-semantics/8051-Memory/memory.tex

@@ -150 +150 @@
 \begin{itemize}
 \item Allow each of the ordinary storage classes from \sdcc, but forbid
-explicit addresses except for \lstinline'volatile' variables.  Note that this
-means that the semantics do not include accessing registers through a pointer.
-\item Leave out bit variables(?), provide `external functions' in the CompCert
-sense for bit access to SFRs but compile them to the corresponding instruction.\\
-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.
-\item Allow casting (and automatic promotion?) to generic pointer types.
+explicit addresses except for \lstinline'volatile' variables.  The compiler
+should ensure that \lstinline'volatile' variables do not overlap with any
+non-\lstinline'volatile' data.  Note that this means that the semantics do not
+include accessing registers through a pointer.
+\item No bit variables are provided to the programmer (although the compiler
+could choose to use them internally).
+\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
+rather than implemented with actual functions.
+\item Casting between pointer types for different memory space attributes is
+defined when the pointer can be represented in both.  In particular, conversion
+to and from a generic pointer type to a specific memory area pointer type is
+guaranteed to work on values pointing to that memory area, and conversions
+between \lstinline'__pdata' and \lstinline'__xdata' pointers will work on
+values that point to the \lstinline'__pdata' space.  Other conversions are
+undefined.
+\item Zeros of any integer type can be converted to any pointer type to give
+a null pointer.  Conversions of any other integer are undefined.  [We could
+extend this to give a semantics for more conversions, or restrict it to
+only deal with integer constant zeros.]
 \item Only provide equality, ordering and subtraction operations on pointer
 types with the same class (with promotion to generic?).  Note that comparison
 between pointers to different blocks is not specified by C or CompCert anyway.
+\item String literals are placed in \lstinline'__code' memory.
 \end{itemize}
 There are no alignment constraints on the 8051.
@@ -202 +216 @@
 As an extreme example, consider the following:
 \begin{lstlisting}
-(* fn1 is a global variable located in idata memory,
+/* fn1 is a global variable located in idata memory,
    which contains a pointer to a value in code memory,
    which is a function that takes and returns a pointer to an integer in xdata.
- *)
+ */
 __xdata int * __code (* __idata fn1)(__xdata int *);
 \end{lstlisting}
@@ -223 +237 @@
 \end{lstlisting}
 
-\begin{verbatim}
-TODO:
-
-Infinite abstract memory model?
-Concrete memory model at end?
-CIL changes?
-Null pointer (choice shouldn't affect C semantics?)
-
-Mention integer sizes in passing?
-Conversion to integer representation?
-
-CONSTANTS - always located in Code if address taken?
-\end{verbatim}
-
 \end{document}