Changeset 157 for C-semantics

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

Make proposed memory spaces semantics more explicit.

1 edited


  • C-semantics/8051-Memory/memory.tex

    r149 r157  
    151151\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.
     152explicit addresses except for \lstinline'volatile' variables.  The compiler
     153should ensure that \lstinline'volatile' variables do not overlap with any
     154non-\lstinline'volatile' data.  Note that this means that the semantics do not
     155include accessing registers through a pointer.
     156\item No bit variables are provided to the programmer (although the compiler
     157could 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
     159rather than implemented with actual functions.
     160\item Casting between pointer types for different memory space attributes is
     161defined when the pointer can be represented in both.  In particular, conversion
     162to and from a generic pointer type to a specific memory area pointer type is
     163guaranteed to work on values pointing to that memory area, and conversions
     164between \lstinline'__pdata' and \lstinline'__xdata' pointers will work on
     165values that point to the \lstinline'__pdata' space.  Other conversions are
     167\item Zeros of any integer type can be converted to any pointer type to give
     168a null pointer.  Conversions of any other integer are undefined.  [We could
     169extend this to give a semantics for more conversions, or restrict it to
     170only deal with integer constant zeros.]
    158171\item Only provide equality, ordering and subtraction operations on pointer
    159172types with the same class (with promotion to generic?).  Note that comparison
    160173between pointers to different blocks is not specified by C or CompCert anyway.
     174\item String literals are placed in \lstinline'__code' memory.
    162176There are no alignment constraints on the 8051.
    202216As an extreme example, consider the following:
    204 (* fn1 is a global variable located in idata memory,
     218/* fn1 is a global variable located in idata memory,
    205219   which contains a pointer to a value in code memory,
    206220   which is a function that takes and returns a pointer to an integer in xdata.
    207  *)
     221 */
    208222__xdata int * __code (* __idata fn1)(__xdata int *);
    225 \begin{verbatim}
    226 TODO:
    228 Infinite abstract memory model?
    229 Concrete memory model at end?
    230 CIL changes?
    231 Null pointer (choice shouldn't affect C semantics?)
    233 Mention integer sizes in passing?
    234 Conversion to integer representation?
    236 CONSTANTS - always located in Code if address taken?
    237 \end{verbatim}
Note: See TracChangeset for help on using the changeset viewer.