# Changeset 3364

Ignore:
Timestamp:
Jun 17, 2013, 3:16:25 PM (5 years ago)
Message:
Location:
src/ASM/CPP2013-policy
Files:
3 edited

### Legend:

Unmodified
 r3363 from instruction labels to addresses in the assembly code. In the second pass it iterates over the code, translating every pseudo jump at address src to a label l associated to the assembly instruction at address dst to a jump of the size dictated by $(\sigma\ src)$ to at address $src$ to a label l associated to the assembly instruction at address $dst$ to a jump of the size dictated by $(\sigma\ src)$ to $(\sigma\ dst)$. In case of conditional jumps, the translated jump may be implemented with a series of instructions. The proof of correctness abstracts over the algorithm used and only relies on {\tt sigma\_policy\_specification} (page~\ref{sigmapolspec}). It is a variation of a standard 1-to-many forward simulation proof~\cite{compcert:2011}. The relation R between states just maps every code address ppc stored in of a standard 1-to-many forward simulation proof~\cite{Leroy2009}. The relation R between states just maps every code address $ppc$ stored in registers or memory to $(\sigma\ ppc)$. To identify the code addresses, an additional data structure is always kept together with the source state and is updated by the semantics. The semantics is preserved only for those programs whose source code operations $(f\ ppc1\ \ldots\ ppcn)$ applied to code addresses $ppc1 \ldots ppcn$ are such that $(f\ (\sigma\ ppc1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppcn))$. For example, an injective $\sigma$ preserves a binary equality test f for code addresses, but not pointer subtraction. $(f\ ppc_1\ \ldots\ ppc_n)$ applied to code addresses $ppc_1 \ldots ppc_n$ are such that $(f\ (\sigma\ ppc_1)\ ...\ (\sigma\ ppc) = f\ ppc\ ppc_n))$. For example, an injective $\sigma$ preserves a binary equality test f for code addresses, but not pointer subtraction. The main lemma (fetching simulation), which relies on\\ see~\cite{lastyear}. Instead of verifying the algorithm directly, another solution to the problem would be to run an optimisation algorithm, and then verify the safety of the result using a verified validator. Such a validator would be easier to verify than the algorithm itself, but it would still leave the question of termination open. In the case of a least fixed point algorithm, at least, the solution is not necessarily safe until the algorithm terminates, so this effort would still have to be expended. \subsection{Related work} displacement optimisation algorithm is not needed. An offshoot of the CompCert project is the CompCertTSO project, who add thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This compiler also generates assembly code and therefore does not include a branch displacement algorithm. An offshoot of the CompCert project is the CompCertTSO project, which adds thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This compiler also generates assembly code and therefore does not include a branch displacement algorithm. Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the formal verification of a compiler, but also of the machine architecture targeted by that compiler, a bespoke microprocessor called the FM9001. targeted by that compiler, a microprocessor called the FM9001. However, this architecture does not have different jump sizes (branching is simulated by assigning values to the program counter),
 r3363 In this section, we present the correctness proof for the algorithm in more detail.  The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}. detail. The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}. \label{sigmapolspec} the program. This worst case is reached if at every iteration, we change the encoding of exactly one branch instruction; since the encoding of any branch instructions can change first from short to absolute and then from absolute to long, there can be at most $2n$ changes. instructions can change first from short to absolute and then to long, there can be at most $2n$ changes. The proof has been carried out using the Russell'' style from~\cite{Sozeau2006}. \end{figure} We can now proceed with the lemmas that are needed for algorithm safety. The lemma in Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main property\\ ({\tt sigma\_policy\_specification}). Its main difference from the final version is that it uses {\tt instruction\_size\_jmplen} to compute the instruction size. This function uses $j$ to compute the span of branch instructions  (i.e. it uses the $\sigma$ function under construction), instead of looking at the distance between source and destination. This is because $\sigma$ is still under construction; later on we will prove that after the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main We now proceed with the safety lemmas. The lemma in Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main property {\tt sigma\_policy\_specification}. Its main difference from the final version is that it uses {\tt instruction\_size\_jmplen} to compute the instruction size. This function uses $j$ to compute the span of branch instructions  (i.e. it uses the $\sigma$ under construction), instead of looking at the distance between source and destination. This is because $\sigma$ is still under construction; we will prove below that after the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main property. \end{figure} The lemma in figure~\ref{sigmasafe} is a more direct safety property. It states The lemma in figure~\ref{sigmasafe} is a safety property. It states that branch instructions are encoded properly, and that no wrong branch instructions are chosen. We need this invariant to make sure that addresses do not overflow. The invariants that are taken directly from the fold invariants are trivial to prove. The invariants taken directly from the fold invariants are trivial to prove. The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},