Changeset 976
 Timestamp:
 Jun 16, 2011, 12:02:07 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r974 r976 178 178 For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar. 179 179 We take time here to explain one of Matita's syntactic idiosyncracies, however. 180 The use of `$\mathtt{ \ldots}$' or `$\mathtt{?}$' in an argument position denotes a type to be inferred automatically by unification.180 The use of `$\mathtt{?}$' or `$\mathtt{\ldots}$' in an argument position denotes a type or types to be inferred automatically by unification respectively. 181 181 The use of `$\mathtt{?}$' in the body of a definition, lemma or axiom denotes an incomplete term that is to be closed, by hand, using tactics. 182 182 … … 288 288 \subsection{Total correctness of the assembler} 289 289 \label{subsect.total.correctness.of.the.assembler} 290 291 Using our policies, we now work toward proving the total correctness of the assembler. 292 By total correctness, we mean that the assembly process does not change the semantics of an assembly program. 293 Naturally, this necessitates keeping some sort of correspondence between program counters at the assembly level, and program counters at the machine code level. 294 For this, we use the \texttt{sigma} machinery defined at the end of Subsection~\ref{subsect.policies}. 290 295 291 296 CSC: no options using policy … … 310 315 \end{lstlisting} 311 316 317 We expand pseudoinstructions using the function \texttt{expand\_pseudo\_instruction}. 318 This function accepts a `policy decision'an element of type \texttt{jump\_length}that is used when expanding a \texttt{Call}, \texttt{Jmp} or conditional jump to a label into the correct machine instruction. 319 This \texttt{policy\_decision} is asssumed to originate from a policy as defined in Subsection~\ref{subsect.policies}. 312 320 \begin{lstlisting} 313 321 definition expand_pseudo_instruction: 314 322 ∀lookup_labels, lookup_datalabels, pc, policy_decision. 315 pseudo_instruciton $\rightarrow$ option list instruction := $\ldots$ 316 \end{lstlisting} 323 pseudo_instruction $\rightarrow$ option list instruction := $\ldots$ 324 \end{lstlisting} 325 Under the assumption that a correct policy exists, \texttt{expand\_pseudo\_instruction} should never fail, and therefore the option type may be dispensed with. 326 This is because the only failure conditions for \texttt{expand\_pseudo\_instruction} result from trying to expand a pseudoinstruction into an `impossible' combination of machine code instructions. 327 For instance, if the policy decision dictates that we should expand a \texttt{Call} pseudoinstruction into a `short jump', then we fail, as the MCS51's instruction set only features instructions \texttt{ACALL} and \texttt{LCALL}. 317 328 318 329 \begin{lstlisting} … … 337 348 \end{lstlisting} 338 349 350 Lemma \texttt{fetch\_assembly\_pseudo} establishes the correctness of expanding and then assembling pseudoinstructions: 339 351 \begin{lstlisting} 340 352 lemma fetch_assembly_pseudo: $\forall$program, ppc, lk_labels, lk_dlabels. … … 342 354 let jexp := jump_expansion ppc program in 343 355 let exp := 344 expand_pseudo_instruction l ookup_labels lookup_datalabels pc jexp pi356 expand_pseudo_instruction lk_labels lk_dlabels pc jexp pi 345 357 let ass := 346 358 assembly_1_pseudoinstruction program ppc pc lk_labels lk_dlabels pi in … … 350 362 fetch_many code_memory (pc + len) pc instructions. 351 363 \end{lstlisting} 364 Here, \texttt{len} is the number of machine code instructions the pseudoinstruction at hand has been expanded into, \texttt{encoding\_check} is a recursive function that checks for any possible corruption of the code memory, resulting from expanding the pseudoinstruction. 365 The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks. 366 367 Intuitively, lemma \texttt{fetch\_assembly\_pseudo} can be read as follows. 368 Suppose our policy \texttt{jump\_expansion} dictates that the pseudoinstruction indexed by the pseudo program counter \texttt{ppc} in assembly program \texttt{program} gives us the policy decision \texttt{jexp}. 369 Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{jexp}, obtaining an (optional) list of machine code instructions \texttt{exp}. 370 Suppose we also 352 371 353 372 \begin{lstlisting} 354 373 theorem fetch_assembly: $\forall$pc, i, cmem, assembled. 355 374 assembled = assembly1 i $\rightarrow$ 356 let len := length ...assembled in375 let len := length $\ldots$ assembled in 357 376 encoding_check cmem pc (pc + len) assembled $\rightarrow$ 358 377 let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in 359 378 let $\langle$instr_pc, ticks$\rangle$ := fetched in 360 let $\langle$instr, pc'$\rangle$ := instr_pc in379 let $\langle$instr, pc'$\rangle$ := instr_pc in 361 380 (eq_instruction instr i $\wedge$ 362 381 eqb ticks (ticks_of_instruction instr) $\wedge$ … … 398 417 theorem main_thm: 399 418 ∀M,M',ps,s,s''. 400 next_internal_pseudo_address_map M ps = Some ...M' $\rightarrow$401 status_of_pseudo_status M ps = Some ...s $\rightarrow$419 next_internal_pseudo_address_map M ps = Some $\ldots$ M' $\rightarrow$ 420 status_of_pseudo_status M ps = Some $\ldots$ s $\rightarrow$ 402 421 status_of_pseudo_status M' 403 422 (execute_1_pseudo_instruction 404 (ticks_of (code_memory ... ps)) ps) = Some ...s'' $\rightarrow$423 (ticks_of (code_memory $\ldots$ ps)) ps) = Some $\ldots$ s'' $\rightarrow$ 405 424 $\exists$n. execute n s = s''. 406 425 \end{lstlisting} … … 417 436 \label{sect.conclusions} 418 437 419 \begin{itemize} 420 \item use of dependent types to throw away wrong programs that would made 421 the statement for completeness complex. E.g. misuse of addressing modes, 422 jumps to non existent labels, etc. 423 \item try to go for small reflection; avoid inductive predicates that require 424 tactics (inversion, etc.) that do not work well with dependent types; small 425 reflection usually does 426 \item use coercions to simulate Russell; mix together the proof styles 427 a la Russell (for situations with heavy dependent types) and the standard 428 one 429 \end{itemize} 438 We have proved the total correctness of an assembler for MCS51 assembly language. 439 In particular, our assembly language featured labels, arbitrary conditional and unconditional jumps to labels, global data and instructions for moving this data into the MCS51's single 16bit register. 430 440 431 441 \subsection{Use of dependent types and Russell}
Note: See TracChangeset
for help on using the changeset viewer.