Changeset 2376 for Papers/cpp-asm-2012


Ignore:
Timestamp:
Sep 28, 2012, 6:13:33 PM (7 years ago)
Author:
mulligan
Message:

To avoid conflicts

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2375 r2376  
    574574If all the operations accepted by the address update map are well-behaved, this is sufficient to show preservation of the semantics for those computation steps that are well-behaved, i.e. such that the map update does not fail.
    575575
    576 We now apply the previous idea to the MCS-51, which is an 8-bit processor whose
    577 code memory is word addressed. Therefore, all MCS-51 operations can only
    578 manipulate and store one half of the address at a time (lower or higher bits).
    579 For instance, a memory cell could contain just the lower 8 bits of an
    580 address \texttt{a}. The corresponding cell at object code level must therefore
    581 hold the lower 8 bits of \texttt{policy(a)}, which can be computed only
    582 if we can retrieve also the higher 8 bits of \texttt{a}. We achieve this
    583 by storing the missing half of an address in the
    584 \texttt{AddrMap} --- called \texttt{internal\_pseudo\_address\_map}
    585 in the formalization.
     576We now apply the previous idea to the MCS-51, an 8-bit processor whose code memory is word addressed.
     577All MCS-51 operations can therefore only manipulate and store one half of the address at a time (lower or higher bits).
     578For instance, a memory cell could contain just the lower 8 bits of an address \texttt{a}.
     579The corresponding cell at object code level must therefore hold the lower 8 bits of \texttt{policy(a)}, which can be computed only if we can also retrieve the higher 8 bits of \texttt{a}.
     580We achieve this by storing the missing half of an address in the \texttt{AddrMap} --- called \texttt{internal\_pseudo\_address\_map} in the formalisation.
    586581\begin{lstlisting}
    587582definition address_entry := upper_lower $\times$ Byte.
     
    591586    $\times$ (option address_entry).
    592587\end{lstlisting}
    593 Here, \texttt{upper\_lower} is an inductive type build from \texttt{Upper} and
    594 \texttt{Lower} and the map is made of three components to track addresses
    595 into lower and upper internal ram and into the A accumulator register.
    596 If an assembly address \texttt{a} holds \texttt{h} and if the
    597 current \texttt{internal\_pseudo\_address\_map} maps \texttt{a} to
    598 \texttt{$\langle$ Upper, l$\rangle$}, then \texttt{h} is the upper part of the
    599 \texttt{h$\cdot$l} address and \texttt{a} will hold the upper part of
    600 \texttt{policy(h$\cdot$l)} in the object code status.
    601 
    602 The relation between assembly pseudostatus at objecto code status is computed
    603 by the following function which deterministically maps each pseudostatus into
    604 the corresponding status. It takes in input the policy and both the current
    605 pseudostatus and the current tracking map in order to identify those memory
    606 cells and registers that hold fragments of addresses to be mapped using
    607 \texttt{policy} as previously explained. It also calls the assembler to
    608 replace the code memory of the assembly status (i.e. the assembly program)
    609 with the object code produced by the assembler.
     588Here, \texttt{upper\_lower} is an inductive type with two constructors: \texttt{Upper} and \texttt{Lower}.
     589The map consists of three components to track addresses in lower and upper internal ram and also in the accumulator \texttt{A}.
     590If an assembly address \texttt{a} holds \texttt{h} and if the current \texttt{internal\_pseudo\_address\_map} maps \texttt{a} to \texttt{$\langle$ Upper, l$\rangle$}, then \texttt{h} is the upper part of the \texttt{h$\cdot$l} address and \texttt{a} will hold the upper part of \texttt{policy(h$\cdot$l)} in the object code status.
     591
     592The relationship between assembly pseudostatus and object code status is computed by the following function which deterministically maps each pseudostatus into a corresponding status.
     593It takes in input the policy and both the current pseudostatus and the current tracking map in order to identify those memory cells and registers that hold fragments of addresses to be mapped using \texttt{policy} as previously explained.
     594It also calls the assembler to replace the code memory of the assembly status (i.e. the assembly program) with the object code produced by the assembler.
    610595\begin{lstlisting}
    611596definition status_of_pseudo_status:
     
    613598 $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap policy)
    614599\end{lstlisting}
    615 
    616 The function that implements tracking map update, previously denoted as
    617 $\llbracket - \rrbracket$, is called
    618 \texttt{next\_internal\_pseudo\_address\_map} in the formalization.
    619 For the time being, we decided to accept as good behaviours the copy of
    620 addresses among memory cells and the accumulator (\texttt{MOV}
    621 pseudoinstruction) and the use of the \texttt{CJNE} conditional jump that
    622 compares two addresses and jumps to a given label if the two labels are equal.
    623 Moreover, \texttt{RET} to return from a function call is well behaved iff
    624 the lower and upper parts of the return address, fetched from the stack, are
    625 both marked to be the complementary parts of the same address
    626 (i.e. \texttt{h} is tracked as \texttt{$\langle$Upper,l$\rangle$} and
    627 \texttt{l} is tracked as \texttt{$\langle$Lower,h$\rangle$}.
    628 These three operations are sufficient to implement the backend of the CerCo
    629 compiler. Other good behaviours could be recognized in the future, for instance
    630 to implement the C branch statement efficiently.
     600The function that implements the tracking map update, previously denoted by $\llbracket - \rrbracket$, is called \texttt{next\_internal\_pseudo\_address\_map} in the formalisation.
     601For the time being, we decided to accept as good behaviours the copy of addresses among memory cells and the accumulator (\texttt{MOV} pseudoinstruction) and the use of the \texttt{CJNE} conditional jump that compares two addresses and jumps to a given label if the two labels are equal.
     602Moreover, \texttt{RET} to return from a function call is well behaved iff the lower and upper parts of the return address, fetched from the stack, are both marked as complementary parts of the same address (i.e. \texttt{h} is tracked as \texttt{$\langle$Upper,l$\rangle$} and \texttt{l} is tracked as \texttt{$\langle$Lower,h$\rangle$}.
     603These three operations are sufficient to implement the backend of the CerCo compiler.
     604Other good behaviours could be recognised in the future, for instance in order to implement the C branch statement efficiently.
    631605\begin{lstlisting}
    632606definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$
Note: See TracChangeset for help on using the changeset viewer.