[637] | 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}, |
---|
[647] | 12 | morekeywords={[2]if,then,else,forall,Prop}, |
---|
[637] | 13 | } |
---|
| 14 | |
---|
| 15 | \lstdefinelanguage{matita} |
---|
[647] | 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}, |
---|
[637] | 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} |
---|
[647] | 84 | \item Proved equivalent to the inductive semantics |
---|
[637] | 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 |
---|
[651] | 236 | |
---|
| 237 | \begin{itemize} |
---|
| 238 | \item[$\triangleright$] Also additional trace for cost labels |
---|
| 239 | \end{itemize} |
---|
[637] | 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 |
---|
[647] | 329 | \item[$\triangleright$] providing separate theorems easier |
---|
[637] | 330 | \end{itemize} |
---|
[647] | 331 | \item Full executions trickier --- final result requires ability to |
---|
[637] | 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 | |
---|
[651] | 354 | \bigskip |
---|
| 355 | \textbf{Demo} |
---|
| 356 | |
---|
[637] | 357 | \end{frame} |
---|
| 358 | |
---|
| 359 | \begin{frame} |
---|
[651] | 360 | \frametitle{D3.1 summary} |
---|
| 361 | |
---|
| 362 | C semantics produced by |
---|
| 363 | \begin{itemize} |
---|
| 364 | \item using CIL and ported inductive semantics from CompCert, |
---|
[657] | 365 | \item adding 8051 memory extensions and cost labels, |
---|
[651] | 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} |
---|
[637] | 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} |
---|