1 | \documentclass{beamer} |
---|
2 | |
---|
3 | \usetheme{Frankfurt} |
---|
4 | \logo{\includegraphics[height=1.0cm]{fetopen.png}} |
---|
5 | |
---|
6 | \usepackage[english]{babel} |
---|
7 | \usepackage{inputenc} |
---|
8 | \usepackage{listings} |
---|
9 | |
---|
10 | \lstdefinelanguage{coq} |
---|
11 | {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record}, |
---|
12 | morekeywords={[2]if,then,else,forall,Prop}, |
---|
13 | } |
---|
14 | |
---|
15 | \lstdefinelanguage{matita} |
---|
16 | {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,and,on,return}, |
---|
17 | morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct,Prop,Type}, |
---|
18 | mathescape=true, |
---|
19 | } |
---|
20 | |
---|
21 | \lstset{language=matita,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false, |
---|
22 | keywordstyle=\color{red}\bfseries, |
---|
23 | keywordstyle=[2]\color{blue}, |
---|
24 | commentstyle=\color{green}, |
---|
25 | stringstyle=\color{blue}, |
---|
26 | showspaces=false,showstringspaces=false} |
---|
27 | |
---|
28 | \author{Brian Campbell, Randy Pollack and Ian Stark} |
---|
29 | \title{CerCo Work Package 3} |
---|
30 | \date{March 11, 2011} |
---|
31 | |
---|
32 | \begin{document} |
---|
33 | |
---|
34 | \begin{frame} |
---|
35 | \maketitle |
---|
36 | \end{frame} |
---|
37 | |
---|
38 | \begin{frame} |
---|
39 | \frametitle{Work Package 3} |
---|
40 | |
---|
41 | \begin{quote} |
---|
42 | This Work Package is devoted to the formal encoding and correctness verification of the compiler front end, from some |
---|
43 | abstract syntax tree representation of (a large subset of) the C language to three-address like intermediate code. |
---|
44 | \end{quote} |
---|
45 | |
---|
46 | \begin{description} |
---|
47 | \item[D3.1] Executable Formal Semantics of C |
---|
48 | \item[T3.2] Functional encoding in the Calculus of Inductive Constructions |
---|
49 | \item[T3.3] Formal semantics of intermediate languages |
---|
50 | \end{description} |
---|
51 | |
---|
52 | |
---|
53 | % introduction by quote about purpose of wp3 |
---|
54 | % main deliverable: D3.1 |
---|
55 | % start of T3.2, T3.3 |
---|
56 | \end{frame} |
---|
57 | |
---|
58 | % place work to date in context of project |
---|
59 | |
---|
60 | \definecolor{lightgreen}{rgb}{.7,1,.7} |
---|
61 | |
---|
62 | \begin{frame} |
---|
63 | \frametitle{D3.1: C semantics} |
---|
64 | |
---|
65 | \[ |
---|
66 | \begin{array}{r@{\ }l} |
---|
67 | \text{C} \Rightarrow \colorbox{yellow}{CIL parser} \Rightarrow \colorbox{yellow}{Clight} |
---|
68 | & \Rightarrow \colorbox{yellow}{inductive semantics} \\ |
---|
69 | & \Rightarrow \colorbox{lightgreen}{executable semantics} |
---|
70 | \end{array} |
---|
71 | \] |
---|
72 | |
---|
73 | \bigskip |
---|
74 | |
---|
75 | \colorbox{yellow}{Sections ported from CompCert Coq development.} \\ |
---|
76 | \begin{itemize} |
---|
77 | \item 8051 memory region extensions added. |
---|
78 | \item Cost labels added. |
---|
79 | \end{itemize} |
---|
80 | |
---|
81 | \medskip |
---|
82 | \colorbox{lightgreen}{New code.} |
---|
83 | \begin{itemize} |
---|
84 | \item Proved equivalent to the inductive semantics |
---|
85 | \end{itemize} |
---|
86 | \end{frame} |
---|
87 | |
---|
88 | \begin{frame} |
---|
89 | \frametitle{8051 memory region extensions} |
---|
90 | |
---|
91 | \begin{center} |
---|
92 | \scalebox{.7}{ |
---|
93 | \setlength{\unitlength}{1pt} |
---|
94 | \begin{picture}(410,250)(-50,200) |
---|
95 | %\put(-50,200){\framebox(410,250){}} |
---|
96 | \put(12,410){\makebox(80,0)[b]{Internal (256B)}} |
---|
97 | \put(13,242){\line(0,1){165}} |
---|
98 | \put(93,242){\line(0,1){165}} |
---|
99 | \put(13,407){\line(1,0){80}} |
---|
100 | \put(12,400){\makebox(0,0)[r]{0h}} \put(14,400){\makebox(0,0)[l]{Register bank 0}} |
---|
101 | \put(13,393){\line(1,0){80}} |
---|
102 | \put(12,386){\makebox(0,0)[r]{8h}} \put(14,386){\makebox(0,0)[l]{Register bank 1}} |
---|
103 | \put(13,379){\line(1,0){80}} |
---|
104 | \put(12,372){\makebox(0,0)[r]{10h}} \put(14,372){\makebox(0,0)[l]{Register bank 2}} |
---|
105 | \put(13,365){\line(1,0){80}} |
---|
106 | \put(12,358){\makebox(0,0)[r]{18h}} \put(14,358){\makebox(0,0)[l]{Register bank 3}} |
---|
107 | \put(13,351){\line(1,0){80}} |
---|
108 | \put(12,344){\makebox(0,0)[r]{20h}} \put(14,344){\makebox(0,0)[l]{Bit addressable}} |
---|
109 | \put(13,323){\line(1,0){80}} |
---|
110 | \put(12,316){\makebox(0,0)[r]{30h}} |
---|
111 | \put(14,309){\makebox(0,0)[l]{\quad \vdots}} |
---|
112 | \put(13,291){\line(1,0){80}} |
---|
113 | \put(12,284){\makebox(0,0)[r]{80h}} |
---|
114 | \put(14,263){\makebox(0,0)[l]{\quad \vdots}} |
---|
115 | \put(12,249){\makebox(0,0)[r]{ffh}} |
---|
116 | \put(13,242){\line(1,0){80}} |
---|
117 | |
---|
118 | \qbezier(-2,407)(-6,407)(-6,393) |
---|
119 | \qbezier(-6,393)(-6,324)(-10,324) |
---|
120 | \put(-12,324){\makebox(0,0)[r]{Indirect/Stack}} |
---|
121 | \qbezier(-6,256)(-6,324)(-10,324) |
---|
122 | \qbezier(-2,242)(-6,242)(-6,256) |
---|
123 | |
---|
124 | \qbezier(94,407)(98,407)(98,393) |
---|
125 | \qbezier(98,393)(98,349)(102,349) |
---|
126 | \put(104,349){\makebox(0,0)[l]{Direct}} |
---|
127 | \qbezier(98,305)(98,349)(102,349) |
---|
128 | \qbezier(94,291)(98,291)(98,305) |
---|
129 | |
---|
130 | \put(102,242){\framebox(20,49){SFR}} |
---|
131 | % bit access to sfrs? |
---|
132 | |
---|
133 | \qbezier(124,291)(128,291)(128,277) |
---|
134 | \qbezier(128,277)(128,266)(132,266) |
---|
135 | \put(134,266){\makebox(0,0)[l]{Direct}} |
---|
136 | \qbezier(128,257)(128,266)(132,266) |
---|
137 | \qbezier(124,242)(128,242)(128,256) |
---|
138 | |
---|
139 | \put(164,410){\makebox(80,0)[b]{External (64kB)}} |
---|
140 | \put(164,220){\line(0,1){187}} |
---|
141 | \put(164,407){\line(1,0){80}} |
---|
142 | \put(244,220){\line(0,1){187}} |
---|
143 | \put(164,242){\line(1,0){80}} |
---|
144 | \put(163,400){\makebox(0,0)[r]{0h}} |
---|
145 | \put(164,324){\makebox(80,0){Paged access}} |
---|
146 | \put(164,310){\makebox(80,0){direct/indirect}} |
---|
147 | \put(163,235){\makebox(0,0)[r]{80h}} |
---|
148 | \put(164,228){\makebox(80,0){\vdots}} |
---|
149 | \put(164,210){\makebox(80,0){Direct/indirect}} |
---|
150 | |
---|
151 | \put(264,410){\makebox(80,0)[b]{Code (64kB)}} |
---|
152 | \put(264,220){\line(0,1){187}} |
---|
153 | \put(264,407){\line(1,0){80}} |
---|
154 | \put(344,220){\line(0,1){187}} |
---|
155 | \put(263,400){\makebox(0,0)[r]{0h}} |
---|
156 | \put(264,228){\makebox(80,0){\vdots}} |
---|
157 | \put(264,324){\makebox(80,0){Direct}} |
---|
158 | \put(264,310){\makebox(80,0){PC relative}} |
---|
159 | \end{picture} |
---|
160 | }\\ |
---|
161 | \textbf{Memory model} |
---|
162 | \end{center} |
---|
163 | |
---|
164 | \end{frame} |
---|
165 | |
---|
166 | \begin{frame} |
---|
167 | \frametitle{8051 memory region extensions} |
---|
168 | |
---|
169 | \begin{tabular}{rcl} |
---|
170 | Attribute & Pointer size & Memory space \\ |
---|
171 | & (bytes) & \\\hline |
---|
172 | \lstinline'__data' & 1 & Internal, first half (0h -- 7fh) \\ |
---|
173 | \lstinline'__idata' & 1 & Internal, indirect only (80h -- ffh) \\ |
---|
174 | \lstinline'__pdata' & 1 & External, page access (usually 0h -- 7fh) \\ |
---|
175 | \lstinline'__xdata' & 2 & External, any (0h -- ffffh) \\ |
---|
176 | \lstinline'__code' & 2 & Code, any (0h -- ffffh) \\ |
---|
177 | \emph{none}& 3 & Any / Generic pointer |
---|
178 | \end{tabular} |
---|
179 | |
---|
180 | \bigskip |
---|
181 | \begin{itemize} |
---|
182 | \item Reuse syntax from \texttt{sdcc} compiler for compatibility. |
---|
183 | \item No support for direct access to registers, bits, etc. |
---|
184 | \end{itemize} |
---|
185 | |
---|
186 | \end{frame} |
---|
187 | |
---|
188 | \begin{frame} |
---|
189 | \frametitle{Port of CompCert semantics: CIL parser} |
---|
190 | \[ \text{C} \Rightarrow \text{CIL parser} \Rightarrow \text{Clight} \] |
---|
191 | |
---|
192 | \bigskip |
---|
193 | \begin{overprint} |
---|
194 | \onslide<1> |
---|
195 | \begin{itemize} |
---|
196 | \item Clight is a C-like language |
---|
197 | \item starting point of formal development |
---|
198 | \item[$\triangleright$] deterministic |
---|
199 | \item[$\triangleright$] side-effect free expressions |
---|
200 | \item[$\triangleright$] explicit casting |
---|
201 | \end{itemize} |
---|
202 | |
---|
203 | CIL parser provides semi-formal C semantics by translation to Clight |
---|
204 | |
---|
205 | \onslide<2> |
---|
206 | CIL parser essentially the same as CompCert, plus |
---|
207 | \begin{itemize} |
---|
208 | \item parsing of memory region extensions |
---|
209 | \item memory regions tracked during elaboration to provide extra type |
---|
210 | information |
---|
211 | \end{itemize} |
---|
212 | \end{overprint} |
---|
213 | |
---|
214 | % maybe example |
---|
215 | % - of clight? |
---|
216 | % - of elab (for type of &e need to know region of e) |
---|
217 | |
---|
218 | \end{frame} |
---|
219 | |
---|
220 | \begin{frame}[fragile] |
---|
221 | \frametitle{Port of CompCert semantics: Clight inductive semantics} |
---|
222 | \alt<1>{CompCert provides a small-step semantics for Clight (in Coq)} |
---|
223 | {We provide a small-step semantics for Clight (in Matita)} |
---|
224 | \begin{overprint} |
---|
225 | \onslide<1-2> |
---|
226 | \begin{itemize} |
---|
227 | \item executable memory model, maps, etc |
---|
228 | \item operations defined by functions |
---|
229 | \item relations for casts, expressions (`lvalues' and `rvalues') |
---|
230 | and statements |
---|
231 | \end{itemize} |
---|
232 | |
---|
233 | \onslide<3> |
---|
234 | \bigskip |
---|
235 | \textbf{Not so easy} --- no sections, different library, bugs\dots |
---|
236 | |
---|
237 | \begin{itemize} |
---|
238 | \item[$\triangleright$] Also additional trace for cost labels |
---|
239 | \end{itemize} |
---|
240 | \end{overprint} |
---|
241 | |
---|
242 | \begin{overprint} |
---|
243 | \onslide<1> |
---|
244 | \begin{lstlisting}[language=Coq] |
---|
245 | Inductive eval_expr: expr -> val -> Prop := |
---|
246 | |
---|
247 | ... |
---|
248 | | eval_Elvalue: forall a ty loc ofs v, |
---|
249 | eval_lvalue (Expr a ty) loc ofs -> |
---|
250 | load_value_of_type ty m loc ofs = Some v -> |
---|
251 | eval_expr (Expr a ty) v |
---|
252 | \end{lstlisting} |
---|
253 | |
---|
254 | \onslide<2-3> |
---|
255 | \begin{lstlisting} |
---|
256 | ninductive eval_expr (ge:genv) (e:env) (m:mem) : |
---|
257 | expr $\rightarrow$ val $\rightarrow$ trace $\rightarrow$ Prop := |
---|
258 | ... |
---|
259 | | eval_Elvalue: $\forall$a,ty,psp,loc,ofs,v,tr. |
---|
260 | eval_lvalue ge e m (Expr a ty) psp loc ofs tr $\rightarrow$ |
---|
261 | load_value_of_type ty m psp loc ofs = Some ? v $\rightarrow$ |
---|
262 | eval_expr ge e m (Expr a ty) v tr |
---|
263 | \end{lstlisting} |
---|
264 | \end{overprint} |
---|
265 | |
---|
266 | \end{frame} |
---|
267 | |
---|
268 | \begin{frame}[fragile] |
---|
269 | \frametitle{Clight executable semantics} |
---|
270 | |
---|
271 | Input in the inductive semantics is treated non-deterministically: |
---|
272 | \begin{itemize} |
---|
273 | \item execution derivation includes arbitrary input value |
---|
274 | \item program behaviour may not be defined on all inputs |
---|
275 | \end{itemize} |
---|
276 | |
---|
277 | For the executable semantics, we use resumptions |
---|
278 | \begin{itemize} |
---|
279 | \item return suspended semantics as a function of the input value |
---|
280 | \item combined resumption + error monad |
---|
281 | \item lift properties over arbitrary values where appropriate: |
---|
282 | \end{itemize} |
---|
283 | \begin{lstlisting} |
---|
284 | nlet rec P_io O I (A:Type) (P:A $\rightarrow$ Prop) (v:IO O I A) on v : Prop := |
---|
285 | match v return $\lambda$_.Prop with |
---|
286 | [ Wrong $\Rightarrow$ True |
---|
287 | | Value z $\Rightarrow$ P z |
---|
288 | | Interact out k $\Rightarrow$ $\forall$v'.P_io O I A P (k v') |
---|
289 | ]. |
---|
290 | \end{lstlisting} |
---|
291 | \end{frame} |
---|
292 | |
---|
293 | \begin{frame}[fragile] |
---|
294 | \frametitle{Clight executable semantics} |
---|
295 | |
---|
296 | Follows the (largely syntax-directed) inductive semantics closely. |
---|
297 | \begin{itemize} |
---|
298 | \item rearranged around pattern matching |
---|
299 | \end{itemize} |
---|
300 | \begin{lstlisting} |
---|
301 | nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val$\times$trace) ≝ |
---|
302 | match e with |
---|
303 | [ Expr e' ty $\Rightarrow$ |
---|
304 | match e' with |
---|
305 | [ ... |
---|
306 | | Evar _ $\Rightarrow$ |
---|
307 | do $\langle$l,tr$\rangle$ $\leftarrow$ exec_lvalue' ge en m e' ty; |
---|
308 | do v $\leftarrow$ opt_to_res ? (load_value_of_type' ty m l); |
---|
309 | OK ? $\langle$v,tr$\rangle$ |
---|
310 | ... |
---|
311 | \end{lstlisting} |
---|
312 | |
---|
313 | A cofixpoint gives a stream of $\langle$trace, state$\rangle$ pairs for whole |
---|
314 | executions. |
---|
315 | |
---|
316 | % executable semantics |
---|
317 | |
---|
318 | \end{frame} |
---|
319 | |
---|
320 | \begin{frame} |
---|
321 | \frametitle{Validation: proof} |
---|
322 | |
---|
323 | Have shown inductive and executable semantics equivalent: |
---|
324 | \begin{itemize} |
---|
325 | \item single-step soundness and completeness straightforward |
---|
326 | \item experimented with requiring soundness in result type |
---|
327 | \begin{itemize} |
---|
328 | \item[$\triangleright$] proof terms get in the way later on |
---|
329 | \item[$\triangleright$] providing separate theorems easier |
---|
330 | \end{itemize} |
---|
331 | \item Full executions trickier --- final result requires ability to |
---|
332 | commit to (non-)termination |
---|
333 | \begin{itemize} |
---|
334 | \item[$\triangleright$] reusing commitment technique from CompCert made |
---|
335 | proof tractable |
---|
336 | \end{itemize} |
---|
337 | \end{itemize} |
---|
338 | |
---|
339 | \end{frame} |
---|
340 | |
---|
341 | \begin{frame} |
---|
342 | \frametitle{Validation: testing} |
---|
343 | |
---|
344 | Executing C programs using the semantics is feasible |
---|
345 | \begin{itemize} |
---|
346 | \item use CIL parser to produce Matita Clight AST |
---|
347 | \item feed AST to executable semantics |
---|
348 | \item extract state at $n$th step and normalise term |
---|
349 | \end{itemize} |
---|
350 | |
---|
351 | Labour intensive --- so only light, targeted testing until we have program |
---|
352 | extraction. |
---|
353 | |
---|
354 | \bigskip |
---|
355 | \textbf{Demo} |
---|
356 | |
---|
357 | \end{frame} |
---|
358 | |
---|
359 | \begin{frame} |
---|
360 | \frametitle{D3.1 summary} |
---|
361 | |
---|
362 | C semantics produced by |
---|
363 | \begin{itemize} |
---|
364 | \item using CIL and ported inductive semantics from CompCert, |
---|
365 | \item adding 8051 memory extensions and cost labels, |
---|
366 | \item writing executable semantics, |
---|
367 | \item proving inductive and executable semantics equivalent, |
---|
368 | \item executable testing. |
---|
369 | \end{itemize} |
---|
370 | \end{frame} |
---|
371 | |
---|
372 | \begin{frame} |
---|
373 | \frametitle{T3.2 / T3.3} |
---|
374 | Started after D3.1 delivery. |
---|
375 | \begin{description} |
---|
376 | \item[T3.2] Functional encoding in the Calculus of Inductive Constructions |
---|
377 | \item[T3.3] Formal semantics of intermediate languages |
---|
378 | \end{description} |
---|
379 | |
---|
380 | \bigskip |
---|
381 | Begun work with |
---|
382 | \begin{itemize} |
---|
383 | \item Harmonisation of common code |
---|
384 | \begin{itemize} |
---|
385 | \item with D4.1, e.g. representation of the integers |
---|
386 | \item with prototype, e.g. bugs found with pointer regions |
---|
387 | \end{itemize} |
---|
388 | \item Started construction of RTLabs semantics |
---|
389 | \begin{itemize} |
---|
390 | \item Need to start RTL languages early as they cross between the front and |
---|
391 | back end |
---|
392 | \end{itemize} |
---|
393 | \end{itemize} |
---|
394 | |
---|
395 | \end{frame} |
---|
396 | |
---|
397 | % maybe something about post 3.1 |
---|
398 | |
---|
399 | \end{document} |
---|