Changeset 2376 for Papers/cpp-asm-2012

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

To avoid conflicts

File:
1 edited

Legend:

Unmodified
 r2375 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. 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. We now apply the previous idea to the MCS-51, an 8-bit processor whose code memory is word addressed. All MCS-51 operations can therefore 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 also retrieve 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 formalisation. \begin{lstlisting} definition address_entry := upper_lower $\times$ Byte. $\times$ (option address_entry). \end{lstlisting} 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. It 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. Here, \texttt{upper\_lower} is an inductive type with two constructors: \texttt{Upper} and \texttt{Lower}. The map consists of three components to track addresses in lower and upper internal ram and also in the accumulator \texttt{A}. 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 relationship between assembly pseudostatus and object code status is computed by the following function which deterministically maps each pseudostatus into a 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. It 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. \begin{lstlisting} definition status_of_pseudo_status: $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap policy) \end{lstlisting} 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. The function that implements the tracking map update, previously denoted by $\llbracket - \rrbracket$, is called \texttt{next\_internal\_pseudo\_address\_map} in the formalisation. 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 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$}. These three operations are sufficient to implement the backend of the CerCo compiler. Other good behaviours could be recognised in the future, for instance in order to implement the C branch statement efficiently. \begin{lstlisting} definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$