Changeset 1013
 Timestamp:
 Jun 21, 2011, 1:52:37 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r1012 r1013 345 345 \end{lstlisting} 346 346 347 348 \begin{lstlisting} 349 axiom assembly_ok: ∀program,assembled,costs,labels. 350 Some $\ldots$ $\langle$labels, costs$\rangle$ = build_maps program $\rightarrow$ 351 Some $\ldots$ $\langle$assembled, costs$\rangle$ = assembly program $\rightarrow$ 352 let code_memory := load_code_memory assembled in 347 The following function, \texttt{build\_maps}, is used to construct a pair of mappings from program counters to labels and cost labels, respectively. 348 Cost labels are a technical device used in the CerCo prototype C compiler for proving that the compiler is cost preserving. 349 For our purposes in this paper, they can be safely ignored, though the interested reader may consult~\cite{amadio:certifying:2010} for an overview. 350 351 The label map, on the other hand, records the position of labels that appear in an assembly program, so that the pseudoinstruction expansion process can replace them with real memory addresses: 352 \begin{lstlisting} 353 definition build_maps: 354 $\forall$p. $\forall$pol: policy p. 355 $\Sigma$res : ((BitVectorTrie Word 16) $\times$ (BitVectorTrie Word 16)). 356 let $\langle$labels, costs$\rangle$ := res in 357 $\forall$id. occurs_exactly_once id ($\pi_2$ p) $\rightarrow$ 358 let addr := address_of_word_labels_code_mem ($\pi_2$ p) id in 359 lookup $\ldots$ id labels (zero $\ldots$) = sigma pseudo_program pol addr := $\ldots$ 360 \end{lstlisting} 361 The rather complex type of \texttt{build\_maps} owes to our use of Matita's Russell facility to provide a strong specification for the function in the type (c.f. the use of sigma types, through which Russell is implemented in Matita). 362 In particular, we express that any label should only appear exactly in any assembly program, and looking up a label in the newly created map is the same as applying the \texttt{sigma} function, recording the correspondence between pseudo program counters and program counters. 363 364 Using \texttt{build\_maps}, we can express the following lemma, expressing the correctness of the assembly function: 365 \begin{lstlisting} 366 lemma assembly_ok: $\forall$p,pol,assembled. 367 let $\langle$labels, costs$\rangle$ := build_maps program pol in 368 $\langle$assembled,costs$\rangle$ = assembly p pol $\rightarrow$ 369 let cmem := load_code_memory assembled in 353 370 let preamble := $\pi_1$ program in 354 let datalabels := construct_datalabels preamble in 355 let lk_labels := 356 $\lambda$x. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in 357 let lk_dlabels := $\lambda$x. lookup ? ? x datalabels (zero ?) in 358 ∀ppc,len,assembledi. 359 let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in 360 let assembly' := assembly_1_pseudoinstruction program ppc 361 (sigma program ppc) lk_labels lk_dlabels pi in 362 let newpc := (sigma program ppc) + len in 363 let echeck := 364 encoding_check code_memory (sigma program ppc) slen assembledi in 365 Some $\ldots$ $\langle$len, assembledi$\rangle$ = assembly' $\rightarrow$ 366 echeck $\wedge$ sigma program newppc = newpc. 367 \end{lstlisting} 371 let dlbls := construct_datalabels preamble in 372 let addr := address_of_word_labels_code_mem ($\pi_2$ program) in 373 let lk_lbls := λx. sigma program pol (addr x) in 374 let lk_dlbls := λx. lookup $\ldots$ x datalabels (zero ?) in 375 $\forall$ppc, pi, newppc. 376 $\forall$prf: $\langle$pi, newppc$\rangle$ = fetch_pseudo_instruction ($\pi_2$ program) ppc. 377 $\forall$len, assm. 378 let spol := sigma program pol ppc in 379 let spol_len := spol + len in 380 let echeck := encoding_check cmem spol spol_len assm in 381 let a1pi := assembly_1_pseudoinstruction in 382 $\langle$len, assm$\rangle$ = a1pi p pol ppc lk_lbls lk_dlbls pi (refl $\ldots$) (refl $\ldots$) ? $\rightarrow$ 383 echeck $\wedge$ sigma p pol newppc = spol_len. 384 \end{lstlisting} 385 Suppose also we assemble our program \texttt{p} in accordance with a policy \texttt{pol} to obtain \texttt{assembled}, loading the assembled program into code memory \texttt{cmem}. 386 %dpm finish 368 387 369 388 Theorem \texttt{fetch\_assembly} establishes that the \texttt{fetch} and \texttt{assembly1} functions interact correctly.
Note: See TracChangeset
for help on using the changeset viewer.