Changeset 2342
 Timestamp:
 Sep 26, 2012, 2:43:19 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2341 r2342 375 375 $\Sigma$assembled: list Byte $\times$ (BitVectorTrie costlabel 16). 376 376 policy is correct for program $\rightarrow$ 377 $\mid$program$\mid$ < $2^{16}$ $\rightarrow$ 378 $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$ 379 policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$ 380 policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$ $\wedge$ 381 $\forall$ppc: pseudo\_program\_counter such that ppc < $2^{16}$. 377 $\mid$program$\mid$ < $2^{16}$ $\rightarrow$ $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$ 378 (policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$ 379 (policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$)) $\wedge$ 380 $\forall$ppc: pseudo_program_counter. ppc < $2^{16}$ $\rightarrow$ 382 381 let pseudo_instr := fetch from program at ppc in 383 382 let assembled_i := assemble pseudo_instr in 384 383 $\mid$assembled_i$\mid$ $\leq$ $2^{16}$ $\wedge$ 385 $\forall$n: nat such that n < $\mid$assembled_i$\mid$. 386 $\exists$k: nat. 384 $\forall$n: nat. n < $\mid$assembled_i$\mid$ $\rightarrow$ $\exists$k: nat. 387 385 nth assembled_i n = nth assembled (policy ppc + k). 388 386 \end{lstlisting} 387 [dpm: update] 389 388 In plain words, the type of \texttt{assembly} states the following. 390 389 Suppose we are given a policy that is correct for the program we are assembling, and suppose the program to be assembled is fully addressable by a 16bit word. … … 404 403 $\forall$code_memory: BitVectorTrie Byte 16. 405 404 $\forall$assembled: list Byte. 406 assembled = assembl y1i $\rightarrow$407 let len := length $\ldots$ assembledin408 let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ len)in409 encoding_check code_memorypc pc_plus_len assembled $\rightarrow$410 let $\langle$instr, pc', ticks$\rangle$ := fetch code_memorypc in405 assembled = assemble i $\rightarrow$ 406 let len := $\mid$assembled$\mid$ in 407 let pc_plus_len := pc + len in 408 encoding_check pc pc_plus_len assembled $\rightarrow$ 409 let $\langle$instr, pc', ticks$\rangle$ := fetch pc in 411 410 instr = i $\wedge$ ticks = (ticks_of_instruction instr) $\wedge$ pc' = pc_plus_len. 412 411 \end{lstlisting} … … 421 420 lemma fetch_assembly_pseudo: 422 421 $\forall$program: pseudo_assembly_program. 423 $\forall$sigma: Word $\rightarrow$ Word. 424 $\forall$policy: Word $\rightarrow$ bool. 422 $\forall$policy. 425 423 $\forall$ppc. 426 424 $\forall$code_memory. 427 425 let $\langle$preamble, instr_list$\rangle$ := program in 428 426 let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in 429 let pc := sigmappc in430 let instrs := expand_pseudo_instructio n $\ldots$ sigma policy ppc $\ldots$pi in431 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction $\ldots$ sigma policy ppc $\ldots$pi in432 let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ l)in427 let pc := policy ppc in 428 let instrs := expand_pseudo_instructio sigma policy ppc pi in 429 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction sigma policy ppc pi in 430 let pc_plus_len := pc + l in 433 431 encoding_check code_memory pc pc_plus_len a $\rightarrow$ 434 432 fetch_many code_memory pc_plus_len pc instructions. … … 448 446 lemma fetch_assembly_pseudo2: 449 447 $\forall$program. 450 $\ forall$sigma.448 $\mid$snd program$\mid$ $\leq$ $2^{16}$ $\rightarrow$ 451 449 $\forall$policy. 452 $\forall$sigma_meets_specification.453 $\forall$ppc. 450 policy is correct for program $\rightarrow$ 451 $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$ 454 452 let $\langle$preamble, instr_list$\rangle$ := program in 455 453 let $\langle$labels, costs$\rangle$ := create_label_cost_map instr_list in 456 let $\langle$assembled, costs'$\rangle$ := $\pi_1$ $\ldots$(assembly program sigma policy) in454 let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program sigma policy) in 457 455 let cmem := load_code_memory assembled in 458 456 let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction instr_list ppc in 459 let instructions := expand_pseudo_instruction $\ldots$ sigma ppc $\ldots$pi in460 fetch_many cmem ( sigma newppc) (sigmappc) instructions.457 let instructions := expand_pseudo_instruction policy ppc pi in 458 fetch_many cmem (policy newppc) (policy ppc) instructions. 461 459 \end{lstlisting} 462 460 … … 506 504 We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM: 507 505 \begin{lstlisting} 506 definition address_entry := upper_lower $\times$ Byte. 507 508 508 definition internal_pseudo_address_map := 509 list ((BitVector 8) $\times$ (bool $\times$ Word)) $\times$ (option (bool $\times$ Word)). 510 \end{lstlisting} 509 (BitVectorTrie address_entry 7) $\times$ (BitVectorTrie address_entry 7) 510 $\times$ (option address_entry). 511 \end{lstlisting} 512 [dpm update] 511 513 The implementation of \texttt{internal\_pseudo\_address\_map} is complicated by some peculiarities of the MCS51's instruction set. 512 514 Note here that all addresses are 16 bit words, but are stored (and manipulated) as 8 bit bytes. … … 521 523 The function is currently axiomatised, and an associated set of axioms prescribe the behaviour of the function: 522 524 \begin{lstlisting} 523 axiom low_internal_ram_of_pseudo_low_internal_ram: 524 internal_pseudo_address_map$\rightarrow$BitVectorTrie Byte 7$\rightarrow$BitVectorTrie Byte 7. 525 definition low_internal_ram_of_pseudo_low_internal_ram: 526 internal_pseudo_address_map $\rightarrow$ policy $\rightarrow$ BitVectorTrie Byte 7 527 $\rightarrow$ BitVectorTrie Byte 7. 525 528 \end{lstlisting} 526 529 … … 531 534 definition status_of_pseudo_status: 532 535 internal_pseudo_address_map $\rightarrow$ $\forall$pap. $\forall$ps: PseudoStatus pap. 533 $\forall$sigma: Word $\rightarrow$ Word. $\forall$policy: Word $\rightarrow$ bool. 534 Status (code_memory_of_pseudo_assembly_program pap sigma policy) 536 $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap sigma policy) 535 537 \end{lstlisting} 536 538 … … 539 541 It thus decides the membership of a strict subset of the set of well behaved programs. 540 542 \begin{lstlisting} 541 definition next_internal_pseudo_address_map: internal_pseudo_address_map 542 $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map 543 \end{lstlisting} 543 definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$ 544 $\forall$cm. (Identifier $\rightarrow$ PseudoStatus cm $\rightarrow$ Word) $\rightarrow$ $\forall$s: PseudoStatus cm. 545 program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map 546 \end{lstlisting} 547 [dpm change] 544 548 Note, if we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed. 545 549 … … 548 552 \begin{lstlisting} 549 553 definition ticks_of0: 550 pseudo_assembly_program $\rightarrow$ ( Word $\rightarrow$ Word) $\rightarrow$ (Word $\rightarrow$ bool) $\rightarrow$Word $\rightarrow$551 pseudo_instruction $\rightarrow$ nat $\times$ nat := $\ldots$554 pseudo_assembly_program $\rightarrow$ (Identifier $\rightarrow$ Word) $\rightarrow$ $\forall$policy. Word $\rightarrow$ 555 pseudo_instruction $\rightarrow$ nat $\times$ nat 552 556 \end{lstlisting} 553 557 An additional function, \texttt{ticks\_of}, is merely a wrapper around this function. … … 559 563 $\forall$M, M': internal_pseudo_address_map. 560 564 $\forall$program: pseudo_assembly_program. 561 let $\langle$preamble, instr_list$\rangle$ := program in 562 $\forall$is_well_labelled: is_well_labelled_p instr_list. 563 $\forall$sigma: Word $\rightarrow$ Word. 564 $\forall$policy: Word $\rightarrow$ bool. 565 $\forall$sigma_meets_specification. 566 $\forall$ps: PseudoStatus program. 567 $\forall$program_counter_in_bounds. 568 next_internal_pseudo_address_map M program ps = Some $\ldots$ M' $\rightarrow$ 569 $\exists$n. execute n $\ldots$ (status_of_pseudo_status M $\ldots$ ps sigma policy) = 570 status_of_pseudo_status M' $\ldots$ (execute_1_pseudo_instruction 571 (ticks_of program sigma policy) program ps) sigma policy. 572 \end{lstlisting} 565 $\forall$program_in_bounds: $\mid$program$\mid$ $\leq$ $2^{16}$. 566 let maps := create_label_cost_map program in 567 let addr_of := ... in 568 program is well labelled $\rightarrow$ 569 $\forall$policy. policy is correct for program. 570 $\forall$ps: PseudoStatus program. ps < $\mid$program$\mid$. 571 next_internal_pseudo_address_map M program ... = Some M' $\rightarrow$ 572 $\exists$n. execute n (status_of_pseudo_status M ps policy) = 573 status_of_pseudo_status M' 574 (execute_1_pseudo_instruction program 575 (ticks_of program ($\lambda$id. addr_of id ps) policy) ps) policy. 576 \end{lstlisting} 577 [dpm change] 573 578 The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is wellbehaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}. 574 579 Further, we explicitly require proof that our policy is correct and the pseudo program counter lies within the bounds of the program.
Note: See TracChangeset
for help on using the changeset viewer.