Changeset 2374 for Papers/cpp-asm-2012


Ignore:
Timestamp:
Sep 28, 2012, 5:54:08 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r2373 r2374  
    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 XXXXXXXXXXXXXXXXX
    577 
    578 We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM:
     576We now apply the previous idea to the MCS-51, which is an 8-bit processor whose
     577code memory is word addressed. Therefore, all MCS-51 operations can only
     578manipulate and store one half of the address at a time (lower or higher bits).
     579For instance, a memory cell could contain just the lower 8 bits of an
     580address \texttt{a}. The corresponding cell at object code level must therefore
     581hold the lower 8 bits of \texttt{policy(a)}, which can be computed only
     582if we can retrieve also the higher 8 bits of \texttt{a}. We achieve this
     583by storing the missing half of an address in the
     584\texttt{AddrMap} --- called \texttt{internal\_pseudo\_address\_map}
     585in the formalization.
    579586\begin{lstlisting}
    580587definition address_entry := upper_lower $\times$ Byte.
     
    584591    $\times$ (option address_entry).
    585592\end{lstlisting}
    586 Here, \texttt{upper\_lower} is a type isomorphic to the booleans.
    587 The implementation of \texttt{internal\_pseudo\_address\_map} is complicated by some peculiarities of the MCS-51's instruction set.
    588 Note here that all addresses are 16 bit words, but are stored (and manipulated) as 8 bit bytes.
    589 All \texttt{MOV} instructions in the MCS-51 must use the accumulator \texttt{A} as an intermediary, moving a byte at a time.
    590 The third component of \texttt{internal\_pseudo\_address\_map} therefore states whether the accumulator currently holds a piece of an address, and if so, whether it is the upper or lower byte of the address (using the \texttt{upper\_lower} flag) complete with the corresponding source address in full.
    591 The first and second components, on the other hand, performs a similar task for the higher and lower external RAM.
    592 Again, we use our \texttt{upper\_lower} flag to describe whether a byte is the upper or lower component of a 16-bit address.
    593 
    594 The \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} function converts the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}.
    595 A similar function exists for high internal RAM.
    596 Note that both RAM segments are indexed using addresses 7-bits long:
    597 \begin{lstlisting}
    598 definition low_internal_ram_of_pseudo_low_internal_ram:
    599  internal_pseudo_address_map $\rightarrow$ policy $\rightarrow$ BitVectorTrie Byte 7
    600   $\rightarrow$ BitVectorTrie Byte 7.
    601 \end{lstlisting}
    602 
    603 Next, we are able to translate \texttt{PseudoStatus} records into \texttt{Status} records using \texttt{status\_of\_pseudo\_status}.
    604 Translating a \texttt{PseudoStatus}'s code memory requires we expand pseudoinstructions and then assemble to obtain a trie of bytes.
    605 This never fails, provided that our policy is correct:
     593Here, \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
     595into lower and upper internal ram and into the A accumulator register.
     596If an assembly address \texttt{a} holds \texttt{h} and if the
     597current \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
     602The relation between assembly pseudostatus at objecto code status is computed
     603by the following function which deterministically maps each pseudostatus into
     604the corresponding status. It takes in input the policy and both the current
     605pseudostatus and the current tracking map in order to identify those memory
     606cells and registers that hold fragments of addresses to be mapped using
     607\texttt{policy} as previously explained.
    606608\begin{lstlisting}
    607609definition status_of_pseudo_status:
     
    610612\end{lstlisting}
    611613
    612 The \texttt{next\_internal\_pseudo\_address\_map} function is responsible for run time monitoring of the behaviour of assembly programs, in order to detect well-behaved ones.
    613 It returns a map that traces memory addresses in internal RAM after execution of the next pseudoinstruction, failing when the instruction tampers with memory addresses in unanticipated (but potentially correct) ways.
    614 It thus decides the membership of a strict subset of the set of well-behaved programs.
     614The function that implements tracking map update, previously denoted as
     615$\llbracket - \rrbracket$, is called
     616\texttt{next\_internal\_pseudo\_address\_map} in the formalization.
     617For the time being, we decided to accept as good behaviours the copy of
     618addresses among memory cells and the accumulator (\texttt{MOV}
     619pseudoinstruction) and the use of the \texttt{CJNE} conditional jump that
     620compares two addresses and jumps to a given label if the two labels are equal.
     621Moreover, \texttt{RET} to return from a function call is well behaved iff
     622the lower and upper parts of the return address, fetched from the stack, are
     623both marked to be the complementary parts of the same address
     624(i.e. \texttt{h} is tracked as \texttt{$\langle$Upper,l$\rangle$} and
     625\texttt{l} is tracked as \texttt{$\langle$Lower,h$\rangle$}.
     626These three operations are sufficient to implement the backend of the CerCo
     627compiler. Other good behaviours could be recognized in the future, for instance
     628to implement the C branch statement efficiently.
    615629\begin{lstlisting}
    616630definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$
     
    618632   program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map
    619633\end{lstlisting}
     634XXXXXXXXXX
    620635If we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed.
    621636Note we once again use dependent types to ensure that program counters are properly within bounds.
Note: See TracChangeset for help on using the changeset viewer.