 Timestamp:
 Sep 27, 2012, 5:36:44 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2362 r2363 308 308 As a consequence, we allow the programmer to mangle, change and generally adjust addresses as they want, under the proviso that the translation process may not be able to preserve the semantics of programs that do this. 309 309 The only limitation introduced by this approach is that the size of 310 assembly programs is bounded by $2^ 16$.310 assembly programs is bounded by $2^{16}$. 311 311 This will be further discussed in Subsect.~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}. 312 312 … … 317 317 \subsection{The assembler} 318 318 \label{subsect.the.assembler} 319 The assembler takes in input an assembly program to expand and a 320 branch displacement policy for it. 321 It returns both the assembled program (a list of bytes to be 322 loaded in code memory for execution) and the costing of the source program. 319 323 320 324 Conceptually the assembler works in two passes. 321 The first pass expands every pseudoinstruction into a list of machine code instructions using the function \texttt{expand\_pseudo\_instruction}. 325 The first pass expands every pseudoinstruction into a list of machine code instructions using the function \texttt{expand\_pseudo\_instruction}. The policy 326 determines which expansion among the alternatives will be choosed for 327 pseudojumps and pseudocalls. Once the expansion is performed, the cost 328 of the pseudoinstruction is defined as the cost of the expansion. 322 329 The second pass encodes as a list of bytes the expanded instruction list by mapping the function \texttt{assembly1} across the list, and then flattening. 323 The program obtained as a list of bytes is ready to be loaded in code memory324 for execution.325 330 \begin{displaymath} 326 331 \hspace{0.5cm} 327 332 \mbox{\fontsize{7}{9}\selectfont$[\mathtt{P_1}, \ldots \mathtt{P_n}]$} \underset{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly}$}}{\xrightarrow{\left(P_i \underset{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly\_1\_pseudo\_instruction}$}}{\xrightarrow{\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand\_pseudo\_instruction}$}} \mathtt{[I^1_i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{~~~~~~~~assembly1^{*}~~~~~~~~}$}} \mathtt{[0110]}}} \mathtt{[0110]}\right)^{*}}} \mbox{\fontsize{7}{9}\selectfont$\mathtt{[\ldots0110\ldots]}$} 328 333 \end{displaymath} 329 The most complex of the two passes is the first, which expands pseudoinstructions and must perform the task of branch displacement~\cite{hyde:branch:2006}. 330 The function \texttt{assembly\_1\_pseudo\_instruction} used in the body of the paper is essentially the composition of the two passes. 331 332 The branch displacement problem refers to the task of expanding pseudojumps into their concrete counterparts, preferably as efficiently as possible. 333 For instance, the MCS51 features three unconditional jump instructions: \texttt{LJMP} and \texttt{SJMP}`long jump' and `short jump' respectivelyand an 11bit oddity of the MCS51, \texttt{AJMP}. 334 Each of these three instructions expects arguments in different sizes and behaves in markedly different ways: \texttt{SJMP} may only perform a `local jump'; \texttt{LJMP} may jump to any address in the MCS51's memory space and \texttt{AJMP} may jump to any address in the current memory page. 335 Consequently, the size of each opcode is different, and to squeeze as much code as possible into the MCS51's limited code memory, the smallest possible opcode that will suffice should be selected. 334 In order to understand the type for the policy, we briefly hint at the 335 branch displacement problem for the MCS51. A detailed description is found 336 in~\cite{boender:correctness:2012}. 337 The MCS51 features three unconditional jump instructions: \texttt{LJMP} and \texttt{SJMP}`long jump' and `short jump' respectivelyand an 11bit oddity of the MCS51, \texttt{AJMP}. 338 Each of these three instructions expects arguments in different sizes and behaves in markedly different ways: \texttt{SJMP} may only perform a `local jump' to an address closer then $2^{7}$ bytes; \texttt{LJMP} may jump to any address in the MCS51's memory space and \texttt{AJMP} may jump to any address in the current memory page. Memory pages partition the code memory into $2^8$ disjoint areas. 339 The size of each opcode is different, with long jumps being larger than the 340 other two. Because of the presence of \texttt{AJMP}, an optimal global solution 341 may be locally unoptimal, employing a long jump where a shorter one could be 342 used to force later jumps to stay inside single memory pages. 336 343 337 344 Similarly, a conditional pseudojump must be translated potentially into a configuration of machine code instructions, depending on the distance to the jump's target. … … 347 354 \end{array} 348 355 \end{displaymath}}} 349 Here, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.350 356 Naturally, if \texttt{label} is `close enough', a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \texttt{label} is not sufficiently local. 351 357 352 In order to implement branch displacement it is impossible to really make the \texttt{expand\_pseudo\_instruction} function completely independent of the encoding function. 353 This is due to branch displacement requiring the distance in bytes of the target of the jump. 354 Moreover the standard solutions for solving the branch displacement problem find their solutions iteratively, by either starting from a solution where all jumps are long, and shrinking them when possible, or starting from a state where all jumps are short and increasing their length as needed. 355 Proving the correctness of such algorithms is already quite involved and the correctness of the assembler as a whole does not depend on the `quality' of the solution found to a branch displacement problem. 356 For this reason, we try to isolate the computation of a branch displacement problem from the proof of correctness for the assembler by parameterising our \texttt{expand\_pseudo\_instruction} by a `policy'. 357 358 \begin{lstlisting} 359 definition expand_pseudo_instruction: 360 $\forall$lookup_labels: Identifier $\rightarrow$ Word. 361 $\forall$policy. 362 $\forall$ppc: Word. 363 $\forall$lookup_datalabels: Identifier $\rightarrow$ Word. 364 $\forall$pi: pseudo_instruction. 365 list instruction := ... 366 \end{lstlisting} 367 Here, the functions \texttt{lookup\_labels} and \texttt{lookup\_datalabels} are the functions that map labels and datalabels to program counters respectively, both of them used in the semantics of assembly. 368 The input \texttt{pi} is the pseudoinstruction to be expanded and is found at address \texttt{ppc} in the assembly program. 369 The function takes \texttt{policy} as an input. 370 In reality, this is a pair of functions, but for the purposes of this paper we simplify. 371 The \texttt{policy} maps pseudoprogram counters to program counters: the encoding of the expansion of the pseudoinstruction found at address \texttt{a} in the assembly code should be placed into code memory at address \texttt{policy(a)}. 372 Of course this is possible only if the policy is correct, which means that the encoding of consecutive assembly instructions must be consecutive in code memory. 373 \begin{displaymath} 374 \texttt{policy}(\texttt{ppc} + 1) = \texttt{pc} + \texttt{current\_instruction\_size} 375 \end{displaymath} 376 Here, \texttt{current\_instruction\_size} is the size in bytes of the encoding of the expanded pseudoinstruction found at \texttt{ppc}. 377 Note that the entanglement we hinted at is only partially solved in this way: the assembler code can ignore the implementation details of the algorithm that finds a policy; 378 however, the algorithm that finds a policy must know the exact behaviour of the assembly program because it needs to predict the way the assembly will expand and encode pseudoinstructions, once fed with a policy. 379 A companion submission to this one~\cite{boender:correctness:2012} certifies an algorithm that finds branch displacement policies for the assembler described in this paper. 380 381 The \texttt{expand\_pseudo\_instruction} function uses the \texttt{policy} map to determine the size of jump required when expanding pseudojumps, computing the jump size by examining the size of the differences between program counters. 382 For instance, if at address \texttt{ppc} in the assembly program we found \texttt{Jmp l} such that \texttt{lookup\_labels l = a}, if the offset \texttt{d = policy(a)  policy(ppc + 1)} is such that \texttt{d} $< 128$ then \texttt{Jmp l} is normally translated to the best local solution, the short jump \texttt{SJMP d}. 383 A global best solution to the branch displacement problem, however, is not always made of locally best solutions. 384 Therefore, in some circumstances, it is necessary to force the assembler to expand jumps into larger ones. 385 This is achieved by another booleanvalued function such that if the function applied to \texttt{ppc} returns true then a \texttt{Jmp l} at address \texttt{ppc} is always translated to a long jump. 386 An essentially identical mechanism exists for call instructions. 358 %In order to implement branch displacement it is impossible to really make the \texttt{expand\_pseudo\_instruction} function completely independent of the encoding function. 359 %This is due to branch displacement requiring the distance in bytes of the target of the jump. 360 %Moreover the standard solutions for solving the branch displacement problem find their solutions iteratively, by either starting from a solution where all jumps are long, and shrinking them when possible, or starting from a state where all jumps are short and increasing their length as needed. 361 %Proving the correctness of such algorithms is already quite involved and the correctness of the assembler as a whole does not depend on the `quality' of the solution found to a branch displacement problem. 362 %For this reason, we try to isolate the computation of a branch displacement problem from the proof of correctness for the assembler by parameterising our \texttt{expand\_pseudo\_instruction} by a `policy'. 363 364 The \texttt{expand\_pseudo\_instruction} function is driven by a policy 365 in the choice of expansion of pseudoinstructions. The simplest idea 366 is then to define policies as functions that maps jumps to their size. 367 This simple idea, however, is impractical because short jumps require the 368 offset of the target. For instance, suppose that at address \texttt{ppc} in 369 the assembly program we found \texttt{Jmp l} such that $l$ is associated to the 370 pseudoaddress \texttt{a} and the policy wants the \texttt{Jmp} to become a 371 \texttt{SJMP $\delta$}. To compute $\delta$, we need to know what the addresses 372 \texttt{ppc+1} and \texttt{a} will become in the assembled program to compute 373 their difference. 374 The address \texttt{a} will be associated to is a function of the expansion 375 of all the pseudoinstructions between \texttt{ppc} and \texttt{a}, which is 376 still to be performed when expanding the instruction at \texttt{ppc}. 377 378 To solve the issue, we define the policy \texttt{policy} as a maps 379 from a valid pseudoaddress to the corresponding address in the assembled 380 program. 381 Therefore, $\delta$ in the example above can be computed simply as 382 \texttt{sigma(a)  sigma(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that 383 $\delta < 128$. When this is not the case, the function emits an 384 \texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always 385 picking the locally best solution. 386 In order to accomodate those optimal solutions that require local suboptimal 387 choices, the policy may also return a boolean used to force 388 the translation of a \texttt{Jmp} into a \texttt{LJMP} even if 389 $\delta < 128$. An essentially identical mechanism exists for call 390 instructions and conditional jumps. 391 392 In order for the translation of a jump to be correct, the address associated to 393 \texttt{a} by the policy and by the assembler must coincide. The latter is 394 the sum of the size of all the expansions of the pseudoinstructions that 395 preceed the one at address \texttt{a}: the assembler just concatenates all 396 expansions one after another. To grant this property, we impose a 397 correctness criterion over policies. A policy is correct when for all 398 valid pseudoaddresses \texttt{ppc} 399 $${\texttt{policy(ppc+1) = policy(ppc) + instruction\_size(ppc)}}$$ 400 Here \texttt{instruction\_size(ppc)} is the size in bytes of the expansion 401 of the pseudoinstruction found at \texttt{pcc}, i.e. the length of 402 $\texttt{assembly\_1\_pseudo\_instruction(ppc)}$. 403 387 404 388 405 %  %
Note: See TracChangeset
for help on using the changeset viewer.