# Changeset 2342 for Papers/cpp-asm-2012

Ignore:
Timestamp:
Sep 26, 2012, 2:43:19 PM (7 years ago)
Message:

simplified statements

File:
1 edited

### Legend:

Unmodified
 r2341 $\Sigma$assembled: list Byte $\times$ (BitVectorTrie costlabel 16). policy is correct for program $\rightarrow$ $\mid$program$\mid$ < $2^{16}$ $\rightarrow$ $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$ policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$ policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$ $\wedge$ $\forall$ppc: pseudo\_program\_counter such that ppc < $2^{16}$. $\mid$program$\mid$ < $2^{16}$ $\rightarrow$ $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$ (policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$ (policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$)) $\wedge$ $\forall$ppc: pseudo_program_counter. ppc < $2^{16}$ $\rightarrow$ let pseudo_instr := fetch from program at ppc in let assembled_i := assemble pseudo_instr in $\mid$assembled_i$\mid$ $\leq$ $2^{16}$ $\wedge$ $\forall$n: nat such that n < $\mid$assembled_i$\mid$. $\exists$k: nat. $\forall$n: nat. n < $\mid$assembled_i$\mid$ $\rightarrow$ $\exists$k: nat. nth assembled_i n = nth assembled (policy ppc + k). \end{lstlisting} [dpm: update] In plain words, the type of \texttt{assembly} states the following. 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 16-bit word. $\forall$code_memory: BitVectorTrie Byte 16. $\forall$assembled: list Byte. assembled = assembly1 i $\rightarrow$ let len := length $\ldots$ assembled in let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ len) in encoding_check code_memory pc pc_plus_len assembled $\rightarrow$ let $\langle$instr, pc', ticks$\rangle$ := fetch code_memory pc in assembled = assemble i $\rightarrow$ let len := $\mid$assembled$\mid$ in let pc_plus_len := pc + len in encoding_check pc pc_plus_len assembled $\rightarrow$ let $\langle$instr, pc', ticks$\rangle$ := fetch pc in instr = i $\wedge$ ticks = (ticks_of_instruction instr) $\wedge$ pc' = pc_plus_len. \end{lstlisting} lemma fetch_assembly_pseudo: $\forall$program: pseudo_assembly_program. $\forall$sigma: Word $\rightarrow$ Word. $\forall$policy: Word $\rightarrow$ bool. $\forall$policy. $\forall$ppc. $\forall$code_memory. let $\langle$preamble, instr_list$\rangle$ := program in let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in let pc := sigma ppc in let instrs := expand_pseudo_instruction $\ldots$ sigma policy ppc $\ldots$ pi in let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction $\ldots$ sigma policy ppc $\ldots$ pi in let pc_plus_len := add $\ldots$ pc (bitvector_of_nat $\ldots$ l) in let pc := policy ppc in let instrs := expand_pseudo_instructio sigma policy ppc pi in let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction sigma policy ppc pi in let pc_plus_len := pc + l in encoding_check code_memory pc pc_plus_len a $\rightarrow$ fetch_many code_memory pc_plus_len pc instructions. lemma fetch_assembly_pseudo2: $\forall$program. $\forall$sigma. $\mid$snd program$\mid$ $\leq$ $2^{16}$ $\rightarrow$ $\forall$policy. $\forall$sigma_meets_specification. $\forall$ppc. policy is correct for program $\rightarrow$ $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$ let $\langle$preamble, instr_list$\rangle$ := program in let $\langle$labels, costs$\rangle$ := create_label_cost_map instr_list in let $\langle$assembled, costs'$\rangle$ := $\pi_1$ $\ldots$ (assembly program sigma policy) in let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program sigma policy) in let cmem := load_code_memory assembled in let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction instr_list ppc in let instructions := expand_pseudo_instruction $\ldots$ sigma ppc $\ldots$ pi in fetch_many cmem (sigma newppc) (sigma ppc) instructions. let instructions := expand_pseudo_instruction policy ppc pi in fetch_many cmem (policy newppc) (policy ppc) instructions. \end{lstlisting} We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM: \begin{lstlisting} definition address_entry := upper_lower $\times$ Byte. definition internal_pseudo_address_map := list ((BitVector 8) $\times$ (bool $\times$ Word)) $\times$ (option (bool $\times$ Word)). \end{lstlisting} (BitVectorTrie address_entry 7) $\times$ (BitVectorTrie address_entry 7) $\times$ (option address_entry). \end{lstlisting} [dpm update] The implementation of \texttt{internal\_pseudo\_address\_map} is complicated by some peculiarities of the MCS-51's instruction set. Note here that all addresses are 16 bit words, but are stored (and manipulated) as 8 bit bytes. The function is currently axiomatised, and an associated set of axioms prescribe the behaviour of the function: \begin{lstlisting} axiom low_internal_ram_of_pseudo_low_internal_ram: internal_pseudo_address_map$\rightarrow$BitVectorTrie Byte 7$\rightarrow$BitVectorTrie Byte 7. definition low_internal_ram_of_pseudo_low_internal_ram: internal_pseudo_address_map $\rightarrow$ policy $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7. \end{lstlisting} definition status_of_pseudo_status: internal_pseudo_address_map $\rightarrow$ $\forall$pap. $\forall$ps: PseudoStatus pap. $\forall$sigma: Word $\rightarrow$ Word. $\forall$policy: Word $\rightarrow$ bool. Status (code_memory_of_pseudo_assembly_program pap sigma policy) $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap sigma policy) \end{lstlisting} It thus decides the membership of a strict subset of the set of well behaved programs. \begin{lstlisting} definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$ $\forall$cm. (Identifier $\rightarrow$ PseudoStatus cm $\rightarrow$ Word) $\rightarrow$ $\forall$s: PseudoStatus cm. program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} [dpm change] Note, if we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed. \begin{lstlisting} definition ticks_of0: pseudo_assembly_program $\rightarrow$ (Word $\rightarrow$ Word) $\rightarrow$ (Word $\rightarrow$ bool) $\rightarrow$ Word $\rightarrow$ pseudo_instruction $\rightarrow$ nat $\times$ nat := $\ldots$ pseudo_assembly_program $\rightarrow$ (Identifier $\rightarrow$ Word) $\rightarrow$ $\forall$policy. Word $\rightarrow$ pseudo_instruction $\rightarrow$ nat $\times$ nat \end{lstlisting} An additional function, \texttt{ticks\_of}, is merely a wrapper around this function. $\forall$M, M': internal_pseudo_address_map. $\forall$program: pseudo_assembly_program. let $\langle$preamble, instr_list$\rangle$ := program in $\forall$is_well_labelled: is_well_labelled_p instr_list. $\forall$sigma: Word $\rightarrow$ Word. $\forall$policy: Word $\rightarrow$ bool. $\forall$sigma_meets_specification. $\forall$ps: PseudoStatus program. $\forall$program_counter_in_bounds. next_internal_pseudo_address_map M program ps = Some $\ldots$ M' $\rightarrow$ $\exists$n. execute n $\ldots$ (status_of_pseudo_status M $\ldots$ ps sigma policy) = status_of_pseudo_status M' $\ldots$ (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy. \end{lstlisting} $\forall$program_in_bounds: $\mid$program$\mid$ $\leq$ $2^{16}$. let maps := create_label_cost_map program in let addr_of := ... in program is well labelled $\rightarrow$ $\forall$policy. policy is correct for program. $\forall$ps: PseudoStatus program. ps < $\mid$program$\mid$. next_internal_pseudo_address_map M program ... = Some M' $\rightarrow$ $\exists$n. execute n (status_of_pseudo_status M ps policy) = status_of_pseudo_status M' (execute_1_pseudo_instruction program (ticks_of program ($\lambda$id. addr_of id ps) policy) ps) policy. \end{lstlisting} [dpm change] The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}. Further, we explicitly require proof that our policy is correct and the pseudo program counter lies within the bounds of the program.