Changeset 207 for Deliverables/D3.1


Ignore:
Timestamp:
Oct 27, 2010, 4:27:28 PM (9 years ago)
Author:
campbell
Message:

Add memory extensions and rework parts of D3.1.

Location:
Deliverables/D3.1/Report
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/Report/report.tex

    r197 r207  
    22\usepackage[utf8x]{inputenc}
    33\usepackage{listings}
    4 \usepackage{../style/cerco}
     4\usepackage{../../style/cerco}
    55\newcommand{\ocaml}{OCaml}
    66\newcommand{\clight}{Clight}
    77\newcommand{\matita}{matita}
     8\newcommand{\sdcc}{\texttt{sdcc}}
    89
    910\newcommand{\textSigma}{\ensuremath{\Sigma}}
     
    5253\vspace*{-1cm}
    5354\begin{center}
    54 \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png}
     55\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
    5556\end{center}
    5657
     
    8081\begin{large}
    8182Main Authors:\\
    82  go here
     83Brian~Campbell, Randy~Pollack
    8384\end{large}
    8485\end{center}
     
    103104elaborates C into an abstract syntax tree for the simpler \clight{} language,
    104105based on the CIL C parser.  The second part is a small step semantics for
    105 \clight{} formalised by in the proof tool, which we have ported to \matita{}.
     106\clight{} formalised in the proof tool, which we have ported from Coq to the
     107\matita{} theorem prover.
    106108This semantics is given in the form of inductive definitions, and so we have
    107109added a third part giving an equivalent functional presentation in \matita{}.
    108110
    109 The \cerco{} compiler also needs to deal with the constrained memory model of
     111The \cerco{} compiler needs to deal with the constrained memory model of
    110112the target microcontroller (in our case, the 8051).  Thus each part of the
    111113semantics has been extended to allow explicit handling of the
    112 microcontroller's memory spaces.
    113 
    114 The port of the two stages of the CompCert \clight{} semantics is described in
    115 Section~\ref{sec:port}.  The new executable semantics is then discussed in
    116 Section~\ref{sec:exec}, followed by the extensions for memory spaces in
    117 Section~\ref{sec:memory}.  Finally we discuss how the semantics can be tested
     114microcontroller's memory spaces.  \emph{Cost labels} have also been added to
     115the \clight{} semantics to support the labelling approach to cost annotations
     116presented in~\cite{d2.1}.
     117
     118The following section discusses the C language extensions for memory spaces.
     119Then the port of the two stages of the CompCert \clight{} semantics is
     120described in Section~\ref{sec:port}, followed by the new executable semantics
     121in Section~\ref{sec:exec}.  Finally we discuss how the semantics can be tested
    118122in Section~\ref{sec:valid}.
     123
     124\section{Language extensions for the 8051 memory model}
     125\label{sec:ext}
     126
     127The choice of an extended 8051 target for the \cerco{} compiler imposes an
     128irregular memory model with tight resource constraints.  The different memory
     129spaces and access modes are summarised in Figure~\ref{fig:memorymodel} ---
     130essentially the development of the 8051 family has fragmented memory into
     131four regions:  one half of the `internal' memory is fully accessible but also
     132contains the register banks, the second half cannot be directly addressed
     133because it is shadowed by the `Special Function Registers' (SFRs) for I/O;
     134`external memory' provides the bulk of memory in a separate address space; and
     135the code is in its own read-only space.
     136
     137To make efficient use of the limited amount of memory, compilers for 8051
     138microcontrollers provide extra keywords to allocate global variables to
     139particular memory spaces, and to limit pointers to address a particular space.
     140The freely available \sdcc{} compiler provides the following extensions for
     141the 8051 memory spaces:
     142\begin{table}[ht]
     143\begin{tabular}{rcl}
     144Attribute & Pointer size & Memory space \\\hline
     145\lstinline'__data' & 1 & Internal, first half (0h -- 7fh) \\
     146\lstinline'__idata' & 1 & Internal, indirect only (80h -- ffh) \\
     147\lstinline'__pdata' & 1 & External, page access (usually 0h -- 7fh) \\
     148\lstinline'__xdata' & 2 & External, any (0h -- ffffh) \\
     149\lstinline'__code' & 2 & Code, any (0h -- ffffh) \\
     150\emph{none}& 3 & Any / Generic pointer
     151\end{tabular}
     152\end{table}
     153The generic pointers are a tagged union of the other kinds of pointers.
     154
     155We intend the \cerco{} compiler to support extensions that are broadly
     156compatible with \sdcc{} to enable the compilation of programs with either.  In
     157particular, this would allow the comparison of the behaviour of test cases
     158compiled with both compilers.  Thus the C syntax and semantics have been
     159extended with the memory space attributes listed above.  The syntax follows
     160\sdcc{} and in the semantics we track the memory space that each block was
     161allocated in and only permit access via the appropriate kinds of pointers.
     162The details on these changes are given in the following sections.
     163
     164The \sdcc{} compiler also supports special variable types for accessing the
     165SFRs, which provide the standard I/O mechanism for the 8051 family.  (Note
     166that pointers to these types are not allowed because only direct addressing of
     167the SFRs is allowed.)  We intend to use CompCert-style `external functions'
     168instead of special types.  These are functions which are declared, but no C
     169implementation is provided.  Instead they are provided by the runtime or
     170compiled directly to the corresponding machine code.  This has the advantage
     171that no changes from the CompCert semantics are required, and a compatibility
     172library can be provided for \sdcc{} if necessary.  The 8051 and the \sdcc{}
     173compiler also provide bit-level access to a small region of internal memory.
     174We do not intend to expose this feature to C programs in the \cerco{}
     175compiler, and so no extension is provided for it.
    119176
    120177\section{Port of CompCert \clight{} semantics to \matita{}}
    121178\label{sec:port}
    122179
    123 \begin{verbatim}
    124 Small-step inductive semantics.
    125 Use CIL-based parser from CompCert 1.7.1 (same as unverified prototype).
    126 COST LABELS
    127 \end{verbatim}
    128 
    129 The first stage from the CompCert semantics is the parsing and elaboration of
    130 C programs into the simpler \clight{} language.  This is based upon the CIL
    131 library for parsing, analysing and transforming C programs by Necula
    132 et.~al.~\cite{cil02}.  The elaboration performed provides explicit type
     180The first stage taken from the CompCert semantics is the parsing and
     181elaboration of C programs into the simpler \clight{} language.  This is based
     182upon the CIL library for parsing, analysing and transforming C programs by
     183Necula et.~al.~\cite{cil02}.  The elaboration performed provides explicit type
    133184information throughout the program, including extra casts for promotion, and
    134185performs simplifications such as breaking up expressions with side effects
    135 into statements which perform the effects and effect-free expressions.  The
    136 resulting \clight{} programs are much more manageable and lack the ambiguities
    137 of C, but remain easily understood by C programmers.
     186into statements that perform the effects using effect-free expressions.  The
     187transformed \clight{} programs are much more manageable and lack the ambiguities
     188of C, but also remain easily understood by C programmers.
     189
     190The parser has been extended with the 8051 memory spaces attributes given
     191above.  The resulting abstract syntax tree records them on global variable
     192declarations and pointer types.  However, we also need to deal with them
     193during the elaboration process to produce all of the required information.
     194For example, when the address-of operator \lstinline'&' is used it must decide
     195which kind of pointer should be used.  Thus the extended elaboration process
     196keeps track of the memory space (if any) that the value of each
     197expression resides in.  Where the memory space is not known, a generic pointer
     198will be used instead.  Moreover, we also include the pointer kind when
     199determining whether a cast must be inserted so that conversions between
     200pointer representations can be performed.
     201
     202
     203Thus the elaboration turns the C code
     204\begin{quote}
     205\begin{lstlisting}[language=C]
     206int g(int *x) { return 5; }
     207
     208int f(__data int *x, int *y) {
     209  return x==y ? g(x) : *x;
     210}
     211
     212__data int i = 1;
     213
     214int main(void) {
     215  return f(&i, &i);
     216}
     217\end{lstlisting}
     218\end{quote}
     219into the following Clight program:
     220\begin{quote}
     221\begin{lstlisting}[language=C]
     222int g(int *x) { return 5; }
     223
     224int f(__data int * x, int * y)
     225{
     226  int t;
     227  if (x == (__data int * )y) {
     228    t = g((int * )x);
     229  } else {
     230    t = *x;
     231  }
     232  return t;
     233}
     234
     235int main(void)
     236{
     237  int t;
     238  t = f(&i, (int * )(&i));
     239  return t;
     240}
     241\end{lstlisting}
     242\end{quote}
     243The expressions in \lstinline'f' and \lstinline'main' had to be broken up due
     244to side-effects, and casts have been added to change between generic pointers
     245and pointers specific to the \lstinline'__data' section of memory.  The
     246underlying data structure also has types attached to every expression, but
     247these are inconvenient to show in source form.
    138248
    139249Note that the translation from C to \clight{} is not proven correct ---
     
    141251can have some confidence in the code, however, because it has received testing
    142252in the \cerco{} prototype, and it is very close to the version used in
    143 CompCert.  As we also have an executable semantics we can perform testing of
    144 it without involving the rest of the compiler.  Moreover, the careful
    145 programmer could choose to inspect the \clight{} code, or even work entirely
    146 in the \clight{} language.
    147 \todo{cite compcert discussion on CIL}
    148 \todo{some details on what CIL does and example before/after}
     253CompCert.  We can also perform testing of the semantics without involving the
     254rest of the compiler because we have an executable semantics.  Moreover, the
     255cautious programmer could choose to inspect the \clight{} code, or even work
     256entirely in the \clight{} language.
    149257
    150258The semantics for \clight{} itself has been ported from the Coq development
    151 used in CompCert to \matita{} for use in CerCo.  Details about the original
     259used in CompCert to \matita{} for use in \cerco{}.  Details about the original
    152260big-step formalisation of \clight{} can be found in Leroy and
    153 Blazy~\cite{compcert-mm08}, although we started from a later version with a
     261Blazy~\cite{compcert-mm08} (including a discussion of the translation from C
     262in \S 4.1), although we started from a later version with a
    154263small-step semantics and hence support for \lstinline'goto' statements.
    155264Several parts of the semantics were shared with other parts of the CompCert
     
    160269\item traces of I/O events,
    161270\item a memory model that keeps conceptually distinct sections of memory
    162 separate (assigning `undefined behaviour' to a buffer overflow, for instance),
    163 \item resulting about composing execution steps of arbitrary small-step
     271strictly separate (assigning `undefined behaviour' to a buffer overflow, for
     272instance),
     273\item results about composing execution steps of arbitrary small-step
    164274semantics,
    165275\item data structures for local and global environments, and
     
    167277\end{itemize}
    168278We anticipate a similar arrangement for the \cerco{} verified compiler,
    169 although this means that there may be further changes to these parts of the
     279although this means that there may be further changes to the common parts of the
    170280semantics later in the project to harmonise the stages of the compiler.
    171281
     
    184294\begin{quote}
    185295\begin{lstlisting}
    186 ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
    187 ...
    188   | eval_Elvalue: a,ty,psp,loc,ofs,v,tr.
    189       eval_lvalue ge e m (Expr a ty) psp loc ofs tr
    190       load_value_of_type ty m psp loc ofs = Some ? v
     296ninductive eval_expr (ge:genv) (e:env) (m:mem) : expr $\rightarrow$ val $\rightarrow$ trace $\rightarrow$ Prop ≝
     297...
     298  | eval_Elvalue: $\forall$a,ty,psp,loc,ofs,v,tr.
     299      eval_lvalue ge e m (Expr a ty) psp loc ofs tr $\rightarrow$
     300      load_value_of_type ty m psp loc ofs = Some ? v $\rightarrow$
    191301      eval_expr ge e m (Expr a ty) v tr
    192302\end{lstlisting}
     
    196306and offset into the block, respectively.  The expression can thus evaluate to
    197307the value \lstinline'v' if \lstinline'v' can be loaded from that location.
    198 One corresponding part of the \lstinline'eval_lvalue' definition,
    199 \begin{quote}
    200 \begin{lstlisting}
    201 ...
    202 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → memory_space → block → int → trace → Prop ≝
    203   | eval_Evar_local:   ∀id,l,ty.
    204       get ??? id e = Some ? l →
     308One corresponding part of the \lstinline'eval_lvalue' definition is
     309\begin{quote}
     310\begin{lstlisting}
     311...
     312with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) :
     313        expr $\rightarrow$ memory_space $\rightarrow$ block $\rightarrow$ int $\rightarrow$ trace $\rightarrow$ Prop ≝
     314  | eval_Evar_local:   $\forall$id,l,ty.
     315      get ??? id e = Some ? l $\rightarrow$
    205316      eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0
    206317...
     
    219330The only new expression in our semantics is the cost label which wraps around
    220331another expression.  It does not change the result, but merely adds the given
    221 label to the trace so as to identify the branches taken in conditional
    222 expressions so that accurate cost information can be attached to the program.
     332label to the trace to identify the branches taken in conditional
     333expressions so that accurate cost information can be attached to the program:
     334\begin{quote}
     335\begin{lstlisting}
     336  | eval_Ecost: $\forall$a,ty,v,l,tr.
     337      eval_expr ge e m a v tr $\rightarrow$
     338      eval_expr ge e m (Expr (Ecost l a) ty) v (tr++Echarge l)
     339\end{lstlisting}
     340\end{quote}
    223341\todo{make the semantics of the cost labels clearer}
    224342
     
    230348ninductive state: Type :=
    231349  | State:
    232       f: function.
    233       s: statement.
    234       k: cont.
    235       e: env.
    236       m: mem.  state
     350      $\forall$f: function.
     351      $\forall$s: statement.
     352      $\forall$k: cont.
     353      $\forall$e: env.
     354      $\forall$m: mem.  state
    237355  | Callstate:
    238       fd: fundef.
    239       args: list val.
    240       k: cont.
    241       m: mem. state
     356      $\forall$fd: fundef.
     357      $\forall$args: list val.
     358      $\forall$k: cont.
     359      $\forall$m: mem. state
    242360  | Returnstate:
    243       res: val.
    244       k: cont.
    245       m: mem. state.
     361      $\forall$res: val.
     362      $\forall$k: cont.
     363      $\forall$m: mem. state.
    246364\end{lstlisting}
    247365\end{quote}
     
    262380\begin{quote}
    263381\begin{lstlisting}
    264 ninductive step (ge:genv) : state → trace → state → Prop ≝
    265   | step_assign:   f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.
    266       eval_lvalue ge e m a1 psp loc ofs tr1
    267       eval_expr ge e m a2 v2 tr2
    268       store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m'
     382ninductive step (ge:genv) : state $\rightarrow$ trace $\rightarrow$ state $\rightarrow$ Prop ≝
     383  | step_assign:   $\forall$f,a1,a2,k,e,m,psp,loc,ofs,v2,m',tr1,tr2.
     384      eval_lvalue ge e m a1 psp loc ofs tr1 $\rightarrow$
     385      eval_expr ge e m a2 v2 tr2 $\rightarrow$
     386      store_value_of_type (typeof a1) m psp loc ofs v2 = Some ? m' $\rightarrow$
    269387      step ge (State f (Sassign a1 a2) k e m)
    270            (tr1tr2) (State f Sskip k e m')
    271 ...
    272 \end{lstlisting}
    273 \end{quote}
    274 which can be read as, if
     388           (tr1++tr2) (State f Sskip k e m')
     389...
     390\end{lstlisting}
     391\end{quote}
     392which can be read as:
    275393\begin{itemize}
    276 \item \lstinline'a1' can evaluate to the location \lstinline'psp,loc,ofs',
     394\item if \lstinline'a1' can evaluate to the location \lstinline'psp,loc,ofs',
    277395\item \lstinline'a2' evaluates to a value \lstinline'v2', and
    278396\item storing \lstinline'v2' at location \lstinline'psp,loc,ofs' succeeds,
     
    294412\begin{quote}
    295413\begin{lstlisting}
    296   | step_external_function: id,targs,tres,vargs,k,m,vres,t.
    297       event_match (external_function id targs tres) vargs t vres
     414  | step_external_function: $\forall$id,targs,tres,vargs,k,m,vres,t.
     415      event_match (external_function id targs tres) vargs t vres $\rightarrow$
    298416      step ge (Callstate (External id targs tres) vargs k m)
    299417            t (Returnstate vres k m)
     
    321439\begin{quote}
    322440\begin{lstlisting}
    323 nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val×trace. eval_expr ge en m e (\fst r) (\snd r)) ≝
     441nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e :
     442               res ($\Sigma$r:val$\times$trace. eval_expr ge en m e (\fst r) (\snd r)) ≝
    324443match e with
    325 [ Expr e' ty
     444[ Expr e' ty $\Rightarrow$
    326445  match e' with
    327446  [ ...
    328   | Evar _ Some ? (
    329       do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
    330       do v opt_to_res ? (load_value_of_type' ty m l);
    331       OK ? 〈v,tr〉)
     447  | Evar _ $\Rightarrow$ Some ? (
     448      do $\langle$l,tr$\rangle$ $\leftarrow$ exec_lvalue' ge en m e' ty;
     449      do v $\leftarrow$ opt_to_res ? (load_value_of_type' ty m l);
     450      OK ? $\langle$v,tr$\rangle$)
    332451...
    333452  ]
    334453]
    335 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
     454and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' :
     455    res ($\Sigma$r:memory_space $\times$ block $\times$ int $\times$ trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
    336456  match e' with
    337   [ Evar id
     457  [ Evar id $\Rightarrow$
    338458      match (get … id en) with
    339       [ None ⇒ Some ? (do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *)
    340       | Some loc ⇒ Some ? (OK ? 〈〈〈Any,loc〉,zero〉,E0〉) (* local *)
     459      [ None $\Rightarrow$ Some ? (do $\langle$sp,l$\rangle$ $\leftarrow$ opt_to_res ? (find_symbol ? ? ge id); OK ? $\langle$$\langle$$\langle$sp,l$\rangle$,zero$\rangle$,E0$\rangle$) (* global *)
     460      | Some loc $\Rightarrow$ Some ? (OK ? $\langle$$\langle$$\langle$Any,loc$\rangle$,zero$\rangle$,E0$\rangle$) (* local *)
    341461      ]
    342462...
     
    349469\begin{quote}
    350470\begin{lstlisting}
    351 do x e; e'
     471do x $\leftarrow$ e; e'
    352472\end{lstlisting}
    353473\end{quote}
     
    360480coercion between the types
    361481\begin{center}
    362 \lstinline'option res T' \quad and \quad \lstinline'res (Σx:T. P x)'
     482\lstinline'option (res T)' \quad and \quad \lstinline'res ($\Sigma$x:T. P x)'
    363483\end{center}
    364484(where a branch marked \lstinline'None' would generate a proof obligation to
     
    376496`external' functions for I/O, which can return arbitrary values.  These are
    377497handled by a resumption monad, which on encountering some I/O returns a
    378 suspension that when applied to a value resumes the evaluation of the
    379 semantics.  Resumption monads are a standard tool for providing denotational
    380 semantics for input~\cite{Moggi199155} and interleaved concurrency~\cite{??}.
     498suspension. When the suspension is applied to a value the evaluation of the
     499semantics is resumed.  Resumption monads are a standard tool for providing
     500denotational semantics for input~\cite{Moggi199155} and interleaved
     501concurrency~\cite{??}.
    381502The definition also incorporates errors, and uses a coercion to automatically
    382503transform values from the plain error monad.
     
    386507\begin{quote}
    387508\begin{lstlisting}
    388 nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
     509nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out ($\Sigma$r:trace $\times$ state. step ge st (\fst r) (\snd r))) ≝
    389510match st with
    390 [ State f s k e m
     511[ State f s k e m $\Rightarrow$
    391512  match s with
    392   [ Sassign a1 a2 Some ? (
    393     ! 〈l,tr1〉 ← exec_lvalue ge e m a1;:
    394     ! 〈v2,tr2〉 ← exec_expr ge e m a2;:
    395     ! m' store_value_of_type' (typeof a1) m l v2;:
    396     ret ? 〈tr1⧺tr2, State f Sskip k e m'〉)
     513  [ Sassign a1 a2 $\Rightarrow$ Some ? (
     514    ! $\langle$l,tr1$\rangle$ $\leftarrow$ exec_lvalue ge e m a1;:
     515    ! $\langle$v2,tr2$\rangle$ $\leftarrow$ exec_expr ge e m a2;:
     516    ! m' $\leftarrow$ store_value_of_type' (typeof a1) m l v2;:
     517    ret ? $\langle$tr1++tr2, State f Sskip k e m'$\rangle$)
    397518...
    398519\end{lstlisting}
     
    405526\begin{quote}
    406527\begin{lstlisting}
    407 do_io : ident → list eventval → IO eventval io_out eventval
     528do_io : ident $\rightarrow$ list eventval $\rightarrow$ IO eventval io_out eventval
    408529\end{lstlisting}
    409530\end{quote}
     
    413534...
    414535  ]
    415 | Callstate f0 vargs k m
     536| Callstate f0 vargs k m $\Rightarrow$
    416537  match f0 with
    417538  [ ...
    418   | External f argtys retty Some ? (
    419       ! evargs check_eventval_list vargs (typlist_of_typelist argtys);:
    420       ! evres do_io f evargs;:
    421       ! vres check_eventval evres (proj_sig_res (signature_of_type argtys rett
    422       ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
     539  | External f argtys retty $\Rightarrow$ Some ? (
     540      ! evargs $\leftarrow$ check_eventval_list vargs (typlist_of_typelist argtys);:
     541      ! evres $\leftarrow$ do_io f evargs;:
     542      ! vres $\leftarrow$ check_eventval evres (proj_sig_res (signature_of_type argtys rett
     543      ret ? $\langle$(Eextcall f evargs evres), Returnstate vres k m$\rangle$)
    423544...
    424545\end{lstlisting}
     
    426547\todo{say something more about the rest?}
    427548
    428 \todo{``the valid''?}
    429 Together with functions to provide a valid initial state for a program and to
     549Together with functions to provide the initial state for a program and to
    430550detect a final state we can write a function to run the program up to a given
    431551number of steps.  Similarly, a corecursive function can return the entire
     
    433553
    434554\todo{completeness?}
    435 
    436 \begin{verbatim}
    437 Functional version of the semantics.
    438 Soundness given in dependent type of execution functions, using Russell-style
    439 separation of terms and proofs.  Pattern matching mimicks inductive definitions from small-step semantics.  Error monad to deal with undefined behaviour;
    440 IO monad with handling of I/O by resumption (which incorporates errors too).
    441 \end{verbatim}
    442 
    443 \section{8051 memory spaces}
    444 \label{sec:memory}
    445 
    446 \begin{verbatim}
    447 Share quite a bit with the 8051 doc.
    448 
    449 Outline of 8051 memory.
    450 
    451 Semantic changes: Values: Blocks in the memory model carry space they are in
    452 (or \texttt{Any} if unspecified; pointers carry space they can point at (or
    453 \texttt{Any} for a generic pointer which can refer to any block).  Types:
    454 pointers carry space corresponding to the allowed pointer values (arrays similar
    455 because they degrade into pointers).  (Not
    456 redundant: pointers can be put into a sufficiently large integer then recast to
    457 their original type.  Cast must be undefined if spaces don't match.)  Operations: casts, comparisons, addition and subtraction.
    458 
    459 Syntactic changes: Clight, pointer and array types, and global decls have spaces added.  CIL similarly changed, but had to tracking space for expr in the elaboration to discover spaces for types.
    460 \end{verbatim}
    461555
    462556\section{Validation}
Note: See TracChangeset for help on using the changeset viewer.