Changeset 809 for Deliverables/D4.1/ITPPaper
 Timestamp:
 May 16, 2011, 4:32:36 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r808 r809 36 36 mathescape=true, 37 37 } 38 \lstset{language=matitaocaml,basicstyle=\ small\tt,columns=flexible,breaklines=false,38 \lstset{language=matitaocaml,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false, 39 39 keywordstyle=\bfseries, %\color{red}\bfseries, 40 40 keywordstyle=[2]\bfseries, %\color{blue}, … … 336 336 type nibble = [`Sixteen] vect 337 337 type byte = [`Eight] vect 338 $\color{blue}{\mathtt{let}}$split_word w = split_nth 4 w339 $\color{blue}{\mathtt{let}}$split_byte b = split_nth 2 b338 let split_word w = split_nth 4 w 339 let split_byte b = split_nth 2 b 340 340 \end{lstlisting}} 341 341 \end{minipage} … … 371 371 \begin{lstlisting} 372 372 let rec split (A: Type[0]) (m,n: nat) on m: 373 Vector A ( plus m n) $\rightarrow$ (Vector A m) $\times$(Vector A n) := ...373 Vector A (m + n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ... 374 374 \end{lstlisting} 375 375 … … 391 391 inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝ 392 392 Leaf: A $\rightarrow$ BitVectorTrie A 0 393  Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) 393  Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ 394 BitVectorTrie A (S n) 394 395  Stub: ∀n. BitVectorTrie A n. 395 396 \end{lstlisting} … … 438 439 The internal state of the Matita emulator is represented as a record: 439 440 \begin{lstlisting} 440 record Status: Type[0] ≝ { 441 record Status: Type[0] := 442 { 441 443 code_memory: BitVectorTrie Byte 16; 442 444 low_internal_ram: BitVectorTrie Byte 7; … … 445 447 program_counter: Word; 446 448 special_function_registers_8051: Vector Byte 19; 447 special_function_registers_8052: Vector Byte 5;448 ...}.449 ... 450 }. 449 451 \end{lstlisting} 450 452 This record encapsulates the current memory contents, the program counter, the state of the current SFRs, and so on. … … 463 465 These costs are taken from a Siemens Semiconductor Group data sheet for the MCS51~\cite{siemens:2011}, and will likely vary between particular implementations. 464 466 \begin{lstlisting} 465 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat 467 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ 468 instruction $\times$ Word $\times$ nat 466 469 \end{lstlisting} 467 470 Instruction are assembled to bit encodings by \texttt{assembly1}: … … 473 476 A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced. 474 477 \begin{lstlisting} 475 definition assembly: 476 assembly_program $\rightarrow$option (list Byte $\times$ (BitVectorTrie String 16))478 definition assembly: assembly_program $\rightarrow$ 479 option (list Byte $\times$ (BitVectorTrie String 16)) 477 480 \end{lstlisting} 478 481 A single fetchdecodeexecute cycle is performed by \texttt{execute\_1}: … … 483 486 \texttt{execute\_1}: 484 487 \begin{lstlisting} 485 let rec execute (n: nat) (s: Status) on n: Status := ...488 let rec execute (n: nat) (s: Status): Status := ... 486 489 \end{lstlisting} 487 490 This differs from the O'Caml emulator, which executed a program indefinitely. … … 512 515 \begin{lstlisting} 513 516 type 'addr preinstruction = 514 517 [ `ADD of acc * [ reg  direct  indirect  data ] 515 518 ... 516 517 (acc * [ reg direct  indirect  data ],518 519 520 521 522 523 519  `MOV of 520 (acc * [ reg direct  indirect  data ], 521 [ reg  indirect ] * [ acc  direct  data ], 522 direct * [ acc  reg  direct  indirect  data ], 523 dptr * data16, 524 carry * bit, 525 bit * carry 526 ) union6 524 527 ... 525 528 \end{lstlisting} … … 538 541 We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against: 539 542 \begin{lstlisting} 540 inductive addressing_mode: Type[0] ≝543 inductive addressing_mode: Type[0] := 541 544 DIRECT: Byte $\rightarrow$ addressing_mode 542 545  INDIRECT: Bit $\rightarrow$ addressing_mode … … 547 550 The constructors of \texttt{addressing\_mode\_tag} are in onetoone correspondence with the constructors of \texttt{addressing\_mode}: 548 551 \begin{lstlisting} 549 inductive addressing_mode_tag : Type[0] ≝552 inductive addressing_mode_tag : Type[0] := 550 553 direct: addressing_mode_tag 551 554  indirect: addressing_mode_tag … … 554 557 The \texttt{is\_a} function checks if an \texttt{addressing\_mode} matches an \texttt{addressing\_mode\_tag}: 555 558 \begin{lstlisting} 556 let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d := 557 match d with 558 [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] 559  indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] 559 let rec is_a 560 (d: addressing_mode_tag) 561 (A: addressing_mode) on d := 562 match d with 563 [ direct $\Rightarrow$ 564 match A with [ DIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] 565  indirect $\Rightarrow$ 566 match A with [ INDIRECT _ $\Rightarrow$ true  _ $\Rightarrow$ false ] 560 567 ... 561 568 \end{lstlisting} … … 564 571 A \texttt{subaddressing\_mode} is an \emph{ad hoc} nonempty $\Sigma$type of \texttt{addressing\_mode}s constrained to be in a set of tags: 565 572 \begin{lstlisting} 566 record subaddressing_mode n (l: Vector addressing_mode_tag (S n)): Type[0] := 567 { subaddressing_modeel :> addressing_mode; 568 subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) }. 573 record subaddressing_mode 574 (n: nat) 575 (l: Vector addressing_mode_tag (S n)): Type[0] := 576 { 577 subaddressing_modeel :> addressing_mode; 578 subaddressing_modein: 579 bool_to_Prop (is_in ? l subaddressing_modeel) 580 }. 569 581 \end{lstlisting} 570 582 An implicit coercion is provided to promote vectors of tags (denoted with $\llbracket  \rrbracket$) to the corresponding \texttt{subaddressing\_mode} so that we can use a syntax close to that of O'Caml to specify \texttt{preinstruction}s: 571 583 \begin{lstlisting} 572 584 inductive preinstruction (A: Type[0]): Type[0] ≝ 573 ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A 574  ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A 585 ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ 586 preinstruction A 587  ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ 588 preinstruction A 575 589 ... 576 590 \end{lstlisting} … … 593 607 For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}: 594 608 \begin{lstlisting} 595 definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝ $~\lambda$s, v, a. 596 match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with 597 [ DPTR $\Rightarrow$ $\lambda$_: True. 598 let 〈 bu, bl 〉 := split $\ldots$ eight eight v in 599 let status := set_8051_sfr s SFR_DPH bu in 600 let status := set_8051_sfr status SFR_DPL bl in 601 status 602  _ $\Rightarrow$ $\lambda$_: False. $\bot$ ] 603 $~$(subaddressing_modein $\ldots$ a). 609 definition set_arg_16: 610 Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a. 611 match a return 612 $\lambda$x. bool_to_Prop (is_in ? $\llbracket$dptr$\rrbracket$ x) $\rightarrow$ ? with 613 [ DPTR $\Rightarrow$ $\lambda$_: True. 614 let $\langle$bu, bl$\rangle$ := split $\ldots$ eight eight v in 615 let status := set_8051_sfr s SFR_DPH bu in 616 let status := set_8051_sfr status SFR_DPL bl in 617 status 618  _ $\Rightarrow$ $\lambda$_: False. $\bot$ 619 ] $~$(subaddressing_modein $\ldots$ a). 604 620 \end{lstlisting} 605 621 We give a proof (the expression \texttt{(subaddressing\_modein} $\ldots$ \texttt{a)}) that the argument $a$ is in the set $\llbracket$ \texttt{dptr} $\rrbracket$ to the \texttt{match} expression. … … 633 649 \begin{lstlisting} 634 650 type line = 635 636 637 638 639 651 [ `P1 of byte  `P3 of byte 652  `SerialBuff of 653 [ `Eight of byte 654  `Nine of BitVectors.bit * byte ] 655 ] 640 656 type continuation = 641 642 643 657 [`In of time * line * 658 epsilon * continuation] option * 659 [`Out of (time > line > time * continuation)] 644 660 \end{lstlisting} 645 661 At each moment, the second projection of the continuation $k$ describes how the environment will react to an output event performed in the future by the processor.
Note: See TracChangeset
for help on using the changeset viewer.