# Changeset 149 for C-semantics

Ignore:
Timestamp:
Oct 5, 2010, 1:50:40 PM (10 years ago)
Message:

Fill in a few details about 8051 extensions.

File:
1 edited

### Legend:

Unmodified
 r94 that they appear as \emph{type specifiers} in the extended C grammar.}.  The new storage classes and corresponding pointer sizes are: \begin{table}[h] \begin{table}[ht] \begin{tabular}{rcl} Attribute & Pointer size & Memory space \\\hline \end{table} There are two areas of overlap: generic pointers overlap with everything else and one page of external memory can be accessed by both \lstinline'__pdata' and \lstinline'__xdata' pointers. There are two areas of overlap between these classes: generic pointers overlap with everything else and one page of external memory can be accessed by both \lstinline'__pdata' and \lstinline'__xdata' pointers. Two types with an implied storage class are also defined.  The \lstinline'__sfr', \lstinline'__sfr16' and \lstinline'__sfr32' declare variables' which access the \emph{Special Function Registers} (SFR). Pointers to these types are not allowed. [Does this match the 8051 instruction set? CSC: in what sense? you cannot indirectly address any SFR register nor an SFR bit in 8051, so maybe this is the reason; it makes sense anyway.] Pointers to these types are not allowed --- the corresponding 8051 instructions only allow direct addressing for them. These are all defined in Section~3.4.1 of the \sdcc\ manual. \begin{itemize} \item Allow each of the ordinary storage classes from \sdcc, but forbid explicit addresses except for \lstinline'volatile' variables. 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.\\ between pointers to different blocks is not specified by C or CompCert anyway. \end{itemize} There are no alignment constraints on the 8051. \section{Impact on formal C semantics} Values, types and the memory model are changed as follows: \begin{itemize} \item Each pointer value has a class' associated with it, either generic or identifying a particular memory space.  Each pointer type has a corresponding space, too. \item Array types are also given a space, because the underlying values are pointers. \item Each block has a class associated with it, either unspecified' or identifying a particular memory space. \end{itemize} The behaviour of casts between pointer types is defined only when the target pointer type is suitable for the memory space pointed at.  Thus casts now depend upon the memory rather than just the values and types. Stack memory is treated as in some unspecified' space at present.  This has the problem that only generic pointers may be used to refer to it.  It may be possible to parametrise the semantics by the stack memory space to allow for a choice of memory model (like the \texttt{--model-}$\star$ options in \sdcc{}). SFR access (both by byte and by bit) do not require any changes as they will be implemented as external' I/O functions. The definitions for alignment constraints from CompCert may be kept for consistency with CompCert, but made vacuous by only requiring' byte alignment. Note that the size of pointer depends on the memory space associated with its type, and that we need to deal with 24 bit chunks' for generic pointer values. \section{Changes to CIL and Clight conversion} The prototype compiler uses the CIL-derived C parser from CompCert.  This can be altered to accept the memory spaces as extra attributes for declarations. Note that this allows them to appear in meaningless places (such as local variable declarations which are always held in stack or registers), which ought to be rejected during translation to Clight. As an extreme example, consider the following: \begin{lstlisting} (* 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} As noted above, the Clight abstract syntax trees are extended by memory spaces added to the pointer and array types, and added to global variable declarations. To support this, the transformations in CIL are extended to keep track of the memory space for each expression during elaboration so that the appropriate pointer types and casts are inserted. The Clight version of the above variable declaration is: \begin{lstlisting} (mk_pair ?? (mk_pair ?? (mk_pair ?? (succ_pos_of_nat 143 (* fn1 *)) [(Init_space 4) ]) IData) (Tpointer Code (Tfunction (Tcons (Tpointer XData (Tint I32 Signed  )) Tnil) (Tpointer XData (Tint I32 Signed  )))))] \end{lstlisting} \begin{verbatim} Concrete memory model at end? CIL changes? SFR access / explicit addressing Where's the stack going? 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}