1 | \documentclass[11pt,epsf,a4wide]{article} |
---|
2 | \usepackage[utf8x]{inputenc} |
---|
3 | \usepackage{listings} |
---|
4 | \usepackage{../style/cerco} |
---|
5 | \newcommand{\ocaml}{OCaml} |
---|
6 | \newcommand{\clight}{Clight} |
---|
7 | \newcommand{\matita}{matita} |
---|
8 | |
---|
9 | \newcommand{\textSigma}{\ensuremath{\Sigma}} |
---|
10 | |
---|
11 | % LaTeX Companion, p 74 |
---|
12 | \newcommand{\todo}[1]{\marginpar{\raggedright - #1}} |
---|
13 | |
---|
14 | \lstdefinelanguage{coq} |
---|
15 | {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record}, |
---|
16 | morekeywords={[2]if,then,else}, |
---|
17 | } |
---|
18 | |
---|
19 | \lstdefinelanguage{matita} |
---|
20 | {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,Type}, |
---|
21 | morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct}, |
---|
22 | mathescape=true, |
---|
23 | } |
---|
24 | |
---|
25 | \lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false, |
---|
26 | keywordstyle=\color{red}\bfseries, |
---|
27 | keywordstyle=[2]\color{blue}, |
---|
28 | commentstyle=\color{green}, |
---|
29 | stringstyle=\color{blue}, |
---|
30 | showspaces=false,showstringspaces=false} |
---|
31 | |
---|
32 | \lstset{extendedchars=false} |
---|
33 | \lstset{inputencoding=utf8x} |
---|
34 | \DeclareUnicodeCharacter{8797}{:=} |
---|
35 | \DeclareUnicodeCharacter{10746}{++} |
---|
36 | \DeclareUnicodeCharacter{9001}{\ensuremath{\langle}} |
---|
37 | \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} |
---|
38 | |
---|
39 | |
---|
40 | \title{ |
---|
41 | INFORMATION AND COMMUNICATION TECHNOLOGIES\\ |
---|
42 | (ICT)\\ |
---|
43 | PROGRAMME\\ |
---|
44 | \vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}} |
---|
45 | |
---|
46 | \date{ } |
---|
47 | \author{} |
---|
48 | |
---|
49 | \begin{document} |
---|
50 | \thispagestyle{empty} |
---|
51 | |
---|
52 | \vspace*{-1cm} |
---|
53 | \begin{center} |
---|
54 | \includegraphics[width=0.6\textwidth]{../style/cerco_logo.png} |
---|
55 | \end{center} |
---|
56 | |
---|
57 | \begin{minipage}{\textwidth} |
---|
58 | \maketitle |
---|
59 | \end{minipage} |
---|
60 | |
---|
61 | |
---|
62 | \vspace*{0.5cm} |
---|
63 | \begin{center} |
---|
64 | \begin{LARGE} |
---|
65 | \bf |
---|
66 | Report n. D3.1\\ |
---|
67 | Executable Formal Semantics of C\\ |
---|
68 | \end{LARGE} |
---|
69 | \end{center} |
---|
70 | |
---|
71 | \vspace*{2cm} |
---|
72 | \begin{center} |
---|
73 | \begin{large} |
---|
74 | Version 1.0 |
---|
75 | \end{large} |
---|
76 | \end{center} |
---|
77 | |
---|
78 | \vspace*{0.5cm} |
---|
79 | \begin{center} |
---|
80 | \begin{large} |
---|
81 | Main Authors:\\ |
---|
82 | go here |
---|
83 | \end{large} |
---|
84 | \end{center} |
---|
85 | |
---|
86 | \vspace*{\fill} |
---|
87 | \noindent |
---|
88 | Project Acronym: \cerco{}\\ |
---|
89 | Project full title: Certified Complexity\\ |
---|
90 | Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\ |
---|
91 | |
---|
92 | \clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881} |
---|
93 | |
---|
94 | \tableofcontents |
---|
95 | |
---|
96 | \section{Introduction} |
---|
97 | |
---|
98 | We present an executable formal semantics of the C programming language which |
---|
99 | will serve as the specification of the input language for the \cerco{} |
---|
100 | verified compiler. Our semantics is based on Leroy et.~al.'s C semantics for |
---|
101 | the CompCert project~\cite{1111042,compcert-mm08}, which divides the treatment |
---|
102 | of C into two pieces. The first is an \ocaml{} stage which parses and |
---|
103 | elaborates C into an abstract syntax tree for the simpler \clight{} language, |
---|
104 | based 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 | This semantics is given in the form of inductive definitions, and so we have |
---|
107 | added a third part giving an equivalent functional presentation in \matita{}. |
---|
108 | |
---|
109 | The \cerco{} compiler also needs to deal with the constrained memory model of |
---|
110 | the target microcontroller (in our case, the 8051). Thus each part of the |
---|
111 | semantics 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 |
---|
118 | in Section~\ref{sec:valid}. |
---|
119 | |
---|
120 | \section{Port of CompCert \clight{} semantics to \matita{}} |
---|
121 | \label{sec:port} |
---|
122 | |
---|
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 |
---|
133 | information throughout the program, including extra casts for promotion, and |
---|
134 | performs 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. |
---|
138 | |
---|
139 | Note that the translation from C to \clight{} is not proven correct --- |
---|
140 | instead it effectively forms a semi-formal part of the whole C semantics. We |
---|
141 | can have some confidence in the code, however, because it has received testing |
---|
142 | in 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} |
---|
149 | |
---|
150 | The 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 |
---|
152 | big-step formalisation of \clight{} can be found in Leroy and |
---|
153 | Blazy~\cite{compcert-mm08}, although we started from a later version with a |
---|
154 | small-step semantics and hence support for \lstinline'goto' statements. |
---|
155 | Several parts of the semantics were shared with other parts of the CompCert |
---|
156 | development, notably: |
---|
157 | \begin{itemize} |
---|
158 | \item representation of primitive values (integers, pointers and undefined |
---|
159 | values, but not structures or unions) and operations on them, |
---|
160 | \item traces of I/O events, |
---|
161 | \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 |
---|
164 | semantics, |
---|
165 | \item data structures for local and global environments, and |
---|
166 | \item common error handling constructs, in particular an error monad. |
---|
167 | \end{itemize} |
---|
168 | We anticipate a similar arrangement for the \cerco{} verified compiler, |
---|
169 | although this means that there may be further changes to these parts of the |
---|
170 | semantics later in the project to harmonise the stages of the compiler. |
---|
171 | |
---|
172 | The main body of the small-step semantics is a number of inductive definitions |
---|
173 | giving details of the defined behaviour for casts, expressions and statements. |
---|
174 | Expressions are side-effect free in \clight{} and only produce a value as |
---|
175 | output. In our case we also need a trace of any cost labels that are |
---|
176 | `evaluated' so that we will be able to give fine-grained costs for |
---|
177 | the execution of compiled conditional expressions. |
---|
178 | |
---|
179 | As an example of one of the expression rules, consider an expression which |
---|
180 | evaluates a variable, \lstinline'Expr (Evar id) ty'. A variable is an example |
---|
181 | of a class of expressions called \emph{lvalues}, which are roughly those |
---|
182 | expressions which can be assigned to. Thus we use a general rule for lvalues, |
---|
183 | \label{page:evalvar} |
---|
184 | \begin{quote} |
---|
185 | \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 → |
---|
191 | eval_expr ge e m (Expr a ty) v tr |
---|
192 | \end{lstlisting} |
---|
193 | \end{quote} |
---|
194 | where the auxiliary relation \lstinline'eval_lvalue' yields the location of |
---|
195 | the value, \lstinline'psp,loc,ofs', consisting of memory space, memory block, |
---|
196 | and offset into the block, respectively. The expression can thus evaluate to |
---|
197 | the 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 → |
---|
205 | eval_lvalue ge e m (Expr (Evar id) ty) Any l zero E0 |
---|
206 | ... |
---|
207 | \end{lstlisting} |
---|
208 | \end{quote} |
---|
209 | simply looks up the variable in the local environment. A similar rule handles |
---|
210 | global variables, with an extra check to ensure that no local variable has the |
---|
211 | same name. Note that the two relations are defined using mutual recursion |
---|
212 | because \lstinline'eval_lvalue' uses \lstinline'eval_expr' for the evaluation |
---|
213 | of the pointer expression in the dereferencing rule. |
---|
214 | |
---|
215 | Casts also have an auxiliary relation to specify the allowed changes, and |
---|
216 | operations on values (including the changes in representation performed by |
---|
217 | casting) are given as functions. |
---|
218 | |
---|
219 | The only new expression in our semantics is the cost label which wraps around |
---|
220 | another 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. |
---|
223 | \todo{make the semantics of the cost labels clearer} |
---|
224 | |
---|
225 | As the expressions are side-effect free, all of the changes to the state are |
---|
226 | performed by statements. The state itself is represented by records of the |
---|
227 | form |
---|
228 | \begin{quote} |
---|
229 | \begin{lstlisting} |
---|
230 | ninductive state: Type := |
---|
231 | | State: |
---|
232 | ∀f: function. |
---|
233 | ∀s: statement. |
---|
234 | ∀k: cont. |
---|
235 | ∀e: env. |
---|
236 | ∀m: mem. state |
---|
237 | | Callstate: |
---|
238 | ∀fd: fundef. |
---|
239 | ∀args: list val. |
---|
240 | ∀k: cont. |
---|
241 | ∀m: mem. state |
---|
242 | | Returnstate: |
---|
243 | ∀res: val. |
---|
244 | ∀k: cont. |
---|
245 | ∀m: mem. state. |
---|
246 | \end{lstlisting} |
---|
247 | \end{quote} |
---|
248 | During normal execution the state contains the currently executing function's |
---|
249 | definition (used to find \lstinline'goto' labels and also to check whether the |
---|
250 | function is expected to return a value), the statement to be executed next, a |
---|
251 | continuation value to be executed afterwards (where successor statements and |
---|
252 | details of function calls and loops are stored), the local environment mapping |
---|
253 | variables to memory locations and the current memory state. |
---|
254 | \todo{need to note that all variables 'appear' to be memory allocated, even |
---|
255 | if they're subsequently optimised away.} |
---|
256 | The function call and return states appear to store less information because |
---|
257 | the details of the caller are contained in the continuation. |
---|
258 | |
---|
259 | An example of the statement execution rules is the assignment rule |
---|
260 | (corresponding to the C syntax \lstinline'a1 = a2'), |
---|
261 | \label{page:Sassign} |
---|
262 | \begin{quote} |
---|
263 | \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' → |
---|
269 | step ge (State f (Sassign a1 a2) k e m) |
---|
270 | (tr1⧺tr2) (State f Sskip k e m') |
---|
271 | ... |
---|
272 | \end{lstlisting} |
---|
273 | \end{quote} |
---|
274 | which can be read as, if |
---|
275 | \begin{itemize} |
---|
276 | \item \lstinline'a1' can evaluate to the location \lstinline'psp,loc,ofs', |
---|
277 | \item \lstinline'a2' evaluates to a value \lstinline'v2', and |
---|
278 | \item storing \lstinline'v2' at location \lstinline'psp,loc,ofs' succeeds, |
---|
279 | yielding the new memory state \lstinline-m'-, then |
---|
280 | \item the program can step from the state about to execute |
---|
281 | \lstinline'Sassign a1 a2' to a state with the updated memory \lstinline-m'- |
---|
282 | about to execute the no-op \lstinline'Sskip'. |
---|
283 | \end{itemize} |
---|
284 | This rule would be followed by one of the rules to which replaces the |
---|
285 | \lstinline'Sskip' statement with the `real' next statement constructed from |
---|
286 | the continuation \lstinline'k'. Note that the only true side-effect here is |
---|
287 | the change in memory --- the local environment is initialised once and for all |
---|
288 | on function entry, and the only events appearing in the trace are cost labels |
---|
289 | used purely for accounting. |
---|
290 | \todo{ordering imposed by cost labels?} |
---|
291 | |
---|
292 | The \clight{} language provides input and output effects through `external' |
---|
293 | functions and the step rule |
---|
294 | \begin{quote} |
---|
295 | \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 → |
---|
298 | step ge (Callstate (External id targs tres) vargs k m) |
---|
299 | t (Returnstate vres k m) |
---|
300 | \end{lstlisting} |
---|
301 | \end{quote} |
---|
302 | which allows the function to be invoked with and return any values subject to |
---|
303 | the enforcement of the typing rules in \lstinline'event_match', which also |
---|
304 | provides the trace. |
---|
305 | |
---|
306 | Cost label statements add the given label to the trace analogously to the cost |
---|
307 | label expressions above. |
---|
308 | |
---|
309 | \section{Executable semantics} |
---|
310 | \label{sec:exec} |
---|
311 | |
---|
312 | \todo{bit of a cheat to claim that it's equivalent without a completeness |
---|
313 | proof.} |
---|
314 | We have added an equivalent functional version of the \clight{} semantics that |
---|
315 | can be used to animate programs. The definitions roughly follow the inductive |
---|
316 | semantics, but are necessarily rearranged around pattern matching of the |
---|
317 | relevant parts of the state rather than presenting each case separately. |
---|
318 | |
---|
319 | The code corresponding to the variable lookup definitions on |
---|
320 | page~\pageref{page:evalvar} is |
---|
321 | \begin{quote} |
---|
322 | \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)) ≝ |
---|
324 | match e with |
---|
325 | [ Expr e' ty ⇒ |
---|
326 | match e' with |
---|
327 | [ ... |
---|
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〉) |
---|
332 | ... |
---|
333 | ] |
---|
334 | ] |
---|
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)) ≝ |
---|
336 | match e' with |
---|
337 | [ Evar id ⇒ |
---|
338 | 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 *) |
---|
341 | ] |
---|
342 | ... |
---|
343 | \end{lstlisting} |
---|
344 | \end{quote} |
---|
345 | where the result is placed in an error monad (the \lstinline'res' type |
---|
346 | constructor) so that \emph{undefined behaviour} such as dereferencing an |
---|
347 | invalid pointer can be rejected. We use \lstinline'do' notation similar to |
---|
348 | Haskell and CompCert, where |
---|
349 | \begin{quote} |
---|
350 | \begin{lstlisting} |
---|
351 | do x ← e; e' |
---|
352 | \end{lstlisting} |
---|
353 | \end{quote} |
---|
354 | means evaluate \lstinline'e' and if it yields a value then bind that to |
---|
355 | \lstinline'x' and evaluate \lstinline-e'-, and otherwise propogate the error. |
---|
356 | |
---|
357 | Note the $\Sigma$ type for the result of the function, which shows that |
---|
358 | successful executions are sound with respect to the inductive semantics. |
---|
359 | Matita automatically generates proof obligations for each case due to a |
---|
360 | coercion between the types |
---|
361 | \begin{center} |
---|
362 | \lstinline'option res T' \quad and \quad \lstinline'res (Σx:T. P x)' |
---|
363 | \end{center} |
---|
364 | (where a branch marked \lstinline'None' would generate a proof obligation to |
---|
365 | show that it is impossible, although the semantics do not use this feature). |
---|
366 | This is intended to mimic Sozeau's \textsc{Russell} language and elaboration |
---|
367 | into Coq~\cite{sozeau06}. The coercion also triggers an automatic mechanism |
---|
368 | in \matita{} to add equalities for each pattern matched. Each case of the |
---|
369 | soundness proof consists of extracting an equality for each computation in the |
---|
370 | monad, |
---|
371 | % "in the monad" is a bit vague here |
---|
372 | making any further case distinctions necessary and applying the corresponding |
---|
373 | rule from the inductive semantics. |
---|
374 | |
---|
375 | Evaluating a step of a statement is complicated by the presence of the |
---|
376 | `external' functions for I/O, which can return arbitrary values. These are |
---|
377 | handled 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{??}. |
---|
381 | The definition also incorporates errors, and uses a coercion to automatically |
---|
382 | transform values from the plain error monad. |
---|
383 | \todo{should perhaps give more details of the resumption monad?} |
---|
384 | |
---|
385 | The execution of assignments is straightforward, |
---|
386 | \begin{quote} |
---|
387 | \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))) ≝ |
---|
389 | match st with |
---|
390 | [ State f s k e m ⇒ |
---|
391 | 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'〉) |
---|
397 | ... |
---|
398 | \end{lstlisting} |
---|
399 | \end{quote} |
---|
400 | where \lstinline'!' is used in place of \lstinline'do' due to the change in |
---|
401 | monad. The content is essentially the same as the inductive rule given on |
---|
402 | page~\pageref{page:Sassign}. |
---|
403 | |
---|
404 | The handling of external calls uses the |
---|
405 | \begin{quote} |
---|
406 | \begin{lstlisting} |
---|
407 | do_io : ident → list eventval → IO eventval io_out eventval |
---|
408 | \end{lstlisting} |
---|
409 | \end{quote} |
---|
410 | function to suspend execution: |
---|
411 | \begin{quote} |
---|
412 | \begin{lstlisting} |
---|
413 | ... |
---|
414 | ] |
---|
415 | | Callstate f0 vargs k m ⇒ |
---|
416 | match f0 with |
---|
417 | [ ... |
---|
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〉) |
---|
423 | ... |
---|
424 | \end{lstlisting} |
---|
425 | \end{quote} |
---|
426 | \todo{say something more about the rest?} |
---|
427 | |
---|
428 | \todo{``the valid''?} |
---|
429 | Together with functions to provide a valid initial state for a program and to |
---|
430 | detect a final state we can write a function to run the program up to a given |
---|
431 | number of steps. Similarly, a corecursive function can return the entire |
---|
432 | execution as a stream of trace and state pairs. |
---|
433 | |
---|
434 | \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} |
---|
461 | |
---|
462 | \section{Validation} |
---|
463 | \label{sec:valid} |
---|
464 | |
---|
465 | \begin{verbatim} |
---|
466 | Animation of simple C programs. |
---|
467 | \end{verbatim} |
---|
468 | |
---|
469 | \begin{verbatim} |
---|
470 | MORE: |
---|
471 | library stuff: choice of integers, maps |
---|
472 | check for any axioms |
---|
473 | \end{verbatim} |
---|
474 | |
---|
475 | \bibliographystyle{plain} |
---|
476 | \bibliography{report} |
---|
477 | |
---|
478 | \end{document} |
---|