# Changeset 2374 for Papers/cpp-asm-2012

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

...

File:
1 edited

### Legend:

Unmodified
 r2373 If 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. XXXXXXXXXXXXXXXXX We use an \texttt{internal\_pseudo\_address\_map} to trace addresses of code memory addresses in internal RAM: We now apply the previous idea to the MCS-51, which is an 8-bit processor whose code memory is word addressed. Therefore, all MCS-51 operations can only manipulate and store one half of the address at a time (lower or higher bits). For instance, a memory cell could contain just the lower 8 bits of an address \texttt{a}. The 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 retrieve also the higher 8 bits of \texttt{a}. We achieve this by storing the missing half of an address in the \texttt{AddrMap} --- called \texttt{internal\_pseudo\_address\_map} in the formalization. \begin{lstlisting} definition address_entry := upper_lower $\times$ Byte. $\times$ (option address_entry). \end{lstlisting} Here, \texttt{upper\_lower} is a type isomorphic to the booleans. 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. All \texttt{MOV} instructions in the MCS-51 must use the accumulator \texttt{A} as an intermediary, moving a byte at a time. 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. The first and second components, on the other hand, performs a similar task for the higher and lower external RAM. Again, we use our \texttt{upper\_lower} flag to describe whether a byte is the upper or lower component of a 16-bit address. 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}. A similar function exists for high internal RAM. Note that both RAM segments are indexed using addresses 7-bits long: \begin{lstlisting} 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} Next, we are able to translate \texttt{PseudoStatus} records into \texttt{Status} records using \texttt{status\_of\_pseudo\_status}. Translating a \texttt{PseudoStatus}'s code memory requires we expand pseudoinstructions and then assemble to obtain a trie of bytes. This never fails, provided that our policy is correct: Here, \texttt{upper\_lower} is an inductive type build from \texttt{Upper} and \texttt{Lower} and the map is made of three components to track addresses into lower and upper internal ram and into the A accumulator register. If 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. The relation between assembly pseudostatus at objecto code status is computed by the following function which deterministically maps each pseudostatus into the corresponding status. It 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. \begin{lstlisting} definition status_of_pseudo_status: \end{lstlisting} 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. 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. It thus decides the membership of a strict subset of the set of well-behaved programs. The function that implements tracking map update, previously denoted as $\llbracket - \rrbracket$, is called \texttt{next\_internal\_pseudo\_address\_map} in the formalization. For 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. Moreover, \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 to be the 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$}. These three operations are sufficient to implement the backend of the CerCo compiler. Other good behaviours could be recognized in the future, for instance to implement the C branch statement efficiently. \begin{lstlisting} definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$ program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} XXXXXXXXXX If we wished to allow `benign manipulations' of addresses, it would be this function that needs to be changed. Note we once again use dependent types to ensure that program counters are properly within bounds.