Changeset 620 for Deliverables
 Timestamp:
 Mar 2, 2011, 3:56:18 PM (10 years ago)
 Location:
 Deliverables
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.1/Presentations/WP4dominicpresentation.tex
r618 r620 4 4 \logo{\includegraphics[height=1.0cm]{fetopen.png}} 5 5 6 \usepackage{amsfonts} 7 \usepackage{amsmath} 8 \usepackage{amssymb} 6 9 \usepackage[english]{babel} 7 \usepackage{inputenc} 10 \usepackage{color} 11 \usepackage[utf8x]{inputenc} 12 \usepackage{listings} 13 \usepackage{stmaryrd} 14 % \usepackage{microtype} 8 15 9 16 \author{Dominic P. Mulligan and Claudio Sacerdoti Coen} … … 13 20 \setlength{\parskip}{1em} 14 21 22 \lstdefinelanguage{matitaocaml} 23 {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to}, 24 morekeywords={[2]whd,normalize,elim,cases,destruct}, 25 morekeywords={[3]type,of,val,assert,let,function}, 26 mathescape=true, 27 } 28 \lstset{language=matitaocaml,basicstyle=\small\tt,columns=flexible,breaklines=false, 29 keywordstyle=\color{red}\bfseries, 30 keywordstyle=[2]\color{blue}, 31 keywordstyle=[3]\color{blue}\bfseries, 32 commentstyle=\color{green}, 33 stringstyle=\color{blue}, 34 showspaces=false,showstringspaces=false} 35 15 36 \begin{document} 16 37 … … 105 126 \end{frame} 106 127 107 \begin{frame} 128 \begin{frame}[fragile] 108 129 \frametitle{Polymorphic variants and phantom types} 109 \begin{itemize}110 \item111 130 The instruction set is highly nonorthogonal. 112 \item 113 We needed a way of 114 \end{itemize} 115 \end{frame} 116 117 \begin{frame} 118 \frametitle{Use of dependent types} 131 We used polymorphic variants and phantom types to capture this nonorthogonality in the type system. 132 For instance: 133 134 \begin{small} 135 \begin{lstlisting} 136 type direct = [ `DIRECT of byte ] 137 type indirect = [ `INDIRECT of bit ] 138 ... 139 type 'addr preinstruction = 140 [ `ADD of acc * [ reg  direct  indirect  data ] 141 ... 142  `MOV of 143 (acc * [ reg  direct  indirect  data ], 144 [ reg  indirect ] * [ acc  direct  data ], 145 direct * [ acc  reg  direct  indirect  data ], ...) 146 ... 147 \end{lstlisting} 148 \end{small} 149 \end{frame} 150 151 \begin{frame}[fragile] 152 \frametitle{Use of dependent types I} 153 This approach worked well in O'Caml, but Matita does not have polymorphic variants, so we need a substitute. 154 We use dependent types. 155 156 Introduce a type for addressing modes: 157 \begin{small} 158 \begin{lstlisting} 159 inductive addressing_mode: Type[0] := 160 DIRECT: Byte $\rightarrow$ addressing_mode 161 ... 162 \end{lstlisting} 163 \end{small} 164 And another type \texttt{addressing\_mode\_tag} of `tags' whose constructors are in correspondence with those of \texttt{addressing\_mode}. 165 \end{frame} 166 167 \begin{frame}[fragile] 168 \frametitle{Use of dependent types II} 169 We use vectors of \texttt{addressing\_mode\_tag}s in our type signatures for instructions. 170 For instance: 171 \begin{small} 172 \begin{lstlisting} 173 inductive preinstruction (A: Type[0]): Type[0] := 174 ADD: $\llbracket$ acc_a $\rrbracket$ 175 $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ 176 $\rightarrow$ preinstruction A 177 ... 178 \end{lstlisting} 179 \end{small} 180 We need: an \emph{ad hoc} $\Sigma$ type and two coercions. 181 One coercion automatically opens up a proof obligation when it is used, which requires some lemmas. 182 183 These lemmas and automation close all proof obligations generated (over 300 in typechecking the main interpreter function). 184 \end{frame} 185 186 \begin{frame} 187 \frametitle{Overlapping memory spaces and addressing modes} 188 MCS51 memory spaces overlap, and can be addressed using different modes and sized pointers. 189 The status record models memory merely as disjoint spaces, using a `tries with holes' datastructure. 190 191 All complications to do with overlapping are handled 119 192 \end{frame} 120 193 
Deliverables/D3.1/Report/report.tex
r417 r620 176 176 \qbezier(2,407)(6,407)(6,393) 177 177 \qbezier(6,393)(6,324)(10,324) 178 \put(12,324){\makebox(0,0)[r]{ indirect}}178 \put(12,324){\makebox(0,0)[r]{Indirect/Stack}} 179 179 \qbezier(6,256)(6,324)(10,324) 180 180 \qbezier(2,242)(6,242)(6,256) … … 182 182 \qbezier(94,407)(98,407)(98,393) 183 183 \qbezier(98,393)(98,349)(102,349) 184 \put(104,349){\makebox(0,0)[l]{ direct/stack}}184 \put(104,349){\makebox(0,0)[l]{Direct}} 185 185 \qbezier(98,305)(98,349)(102,349) 186 186 \qbezier(94,291)(98,291)(98,305) 187 187 188 \put(102,242){\framebox(20,49){ sfr}}188 \put(102,242){\framebox(20,49){SFR}} 189 189 % bit access to sfrs? 190 190 191 191 \qbezier(124,291)(128,291)(128,277) 192 192 \qbezier(128,277)(128,266)(132,266) 193 \put(134,266){\makebox(0,0)[l]{ direct}}193 \put(134,266){\makebox(0,0)[l]{Direct}} 194 194 \qbezier(128,257)(128,266)(132,266) 195 195 \qbezier(124,242)(128,242)(128,256) … … 201 201 \put(164,242){\line(1,0){80}} 202 202 \put(163,400){\makebox(0,0)[r]{0h}} 203 \put(164,324){\makebox(80,0){ paged access}}203 \put(164,324){\makebox(80,0){Paged access}} 204 204 \put(164,310){\makebox(80,0){direct/indirect}} 205 205 \put(163,235){\makebox(0,0)[r]{80h}} 206 206 \put(164,228){\makebox(80,0){\vdots}} 207 \put(164,210){\makebox(80,0){ direct/indirect}}207 \put(164,210){\makebox(80,0){Direct/indirect}} 208 208 209 209 \put(264,410){\makebox(80,0)[b]{Code (64kB)}} … … 213 213 \put(263,400){\makebox(0,0)[r]{0h}} 214 214 \put(264,228){\makebox(80,0){\vdots}} 215 \put(264,324){\makebox(80,0){ direct}}215 \put(264,324){\makebox(80,0){Dsirect}} 216 216 \put(264,310){\makebox(80,0){PC relative}} 217 217 \end{picture} 
Deliverables/D4.1/GCC/IntegerSquareRoot.c
r165 r620 1 #include "stdio.h"2 3 1 unsigned int isqrt(unsigned int n){ 4 2 unsigned int a; … … 11 9 int i = 0; 12 10 i = isqrt(16); 13 printf("%d", i); 11 if(i == 4) 12 return 1; 14 13 return 0; 15 14 } 
Deliverables/D4.1/Test.hex
r212 r620 1 :03000000020008F3 2 :0300610002000397 3 :0500030012006480FE04 4 :0A006400780575050FD69000002204 5 :06003700E478FFF6D8FD9D 6 :080015007900E94400601B7A48 7 :05001D00009000727864 8 :030022000075A0C6 9 :0A00250000E493F2A308B8000205FE 10 :08002F00A0D9F4DAF275A0FF7C 11 :08003D007800E84400600A7934 12 :030045000075A0A3 13 :0600480000E4F309D8FCFE 14 :08004E007800E84400600C7921 15 :0B00560000900000E4F0A3D8FCD9FAF1 16 :03000800758107F8 17 :0A000B0012006EE58260030200039C 18 :04006E007582002275 1 :100000000200081200A480FE7581071200BCE58280 2 :0E00100060030200037900E94400601B7A00DF 3 :10001E009000C0780075A000E493F2A308B8000227 4 :0F002E0005A0D9F4DAF275A0FFE478FFF6D8FD4B 5 :0F003D007800E84400600A790075A000E4F30938 6 :10004C00D8FC7800E84400600C7900900000E4F0E3 7 :10005C00A3D8FCD9FA020003AA82AB837C007D00F2 8 :10006C008C06EDCE25E0CE33FF0EBE00010FC3EAA9 9 :10007C009EEB9F401E8C068D070CBC00010DEFCE35 10 :10008C0025E0CE33FF0EBE00010FEAC39EFAEB9FB4 11 :10009C00FB80CD8C828D8322900010120064AA828A 12 :1000AC00AB83BA0407BB000490000122900000222D 13 :0400BC007582002227 19 14 :00000001FF
Note: See TracChangeset
for help on using the changeset viewer.