Changeset 149 for C-semantics

Oct 5, 2010, 1:50:40 PM (11 years ago)

Fill in a few details about 8051 extensions.

1 edited


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

    r94 r149  
    103103that they appear as \emph{type specifiers} in the extended C grammar.}.  The
    104104new storage classes and corresponding pointer sizes are:
    105 \begin{table}[h]
    107107Attribute & Pointer size & Memory space \\\hline
    117 There are two areas of overlap: generic pointers overlap with everything else
    118 and one page of external memory can be accessed by both \lstinline'__pdata'
    119 and \lstinline'__xdata' pointers.
     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.
    121121Two types with an implied storage class are also defined.  The
    123123\lstinline'__sfr', \lstinline'__sfr16' and \lstinline'__sfr32' declare
    124124`variables' which access the \emph{Special Function Registers} (SFR).
    125 Pointers to these types are not allowed. [Does this match the 8051 instruction
    126 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.]
     125Pointers to these types are not allowed --- the corresponding 8051 instructions
     126only allow direct addressing for them.
    128128These are all defined in Section~3.4.1 of the \sdcc\ manual.
    151151\item Allow each of the ordinary storage classes from \sdcc, but forbid
    152 explicit addresses except for \lstinline'volatile' variables.
     152explicit addresses except for \lstinline'volatile' variables.  Note that this
     153means that the semantics do not include accessing registers through a pointer.
    153154\item Leave out bit variables(?), provide `external functions' in the CompCert
    154155sense for bit access to SFRs but compile them to the corresponding instruction.\\
    159160between pointers to different blocks is not specified by C or CompCert anyway.
     162There are no alignment constraints on the 8051.
     164\section{Impact on formal C semantics}
     166Values, types and the memory model are changed as follows:
     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
     173\item Each block has a class associated with it, either `unspecified' or
     174identifying a particular memory space.
     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.
     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
     186SFR access (both by byte and by bit) do not require any changes as they will
     187be implemented as `external' I/O functions.
     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.
     194\section{Changes to CIL and Clight conversion}
     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.
     202As an extreme example, consider the following:
     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 *);
     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.
     217The Clight version of the above variable declaration is:
     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  )))))]
    166229Concrete memory model at end?
    167230CIL changes?
    168 SFR access / explicit addressing
    169 Where's the stack going?
    170231Null pointer (choice shouldn't affect C semantics?)
     233Mention integer sizes in passing?
     234Conversion to integer representation?
     236CONSTANTS - always located in Code if address taken?
Note: See TracChangeset for help on using the changeset viewer.