Abstract syntax and semantics for PowerPC assembly language

Abstract syntax

Integer registers, floating-point registers.

Symbolic constants. Immediate operands to an arithmetic instruction or an indexed memory access can be either integer literals, or the low or high 16 bits of a symbolic reference (the address of a symbol plus a displacement), or a 16-bit offset from the small data area register. These symbolic references are resolved later by the linker.

A note on constants: while immediate operands to PowerPC instructions must be representable in 16 bits (with sign extension or left shift by 16 positions for some instructions), we do not attempt to capture these restrictions in the abstract syntax nor in the semantics. The assembler will emit an error if immediate operands exceed the representable range. Of course, our PPC generator (file Asmgen) is careful to respect this range.

Bits in the condition register. We are only interested in the first 4 bits.

The instruction set. Most instructions correspond exactly to actual instructions of the PowerPC processor. See the PowerPC reference manuals for more details. Some instructions, described below, are pseudo-instructions: they expand to canned instruction sequences during the printing of the assembly code.

The pseudo-instructions are the following:

• Plabel: define a code label at the current program point
• Plfi: load a floating-point constant in a float register. Expands to a float load lfd from an address in the constant data section initialized with the floating-point constant:

          addis   r12, 0, ha16(lbl)
          lfd     rdst, lo16(lbl)(r12)
          .const_data
  lbl:    .double floatcst
          .text
  

Initialized data in the constant data section are not modeled here, which is why we use a pseudo-instruction for this purpose.

• Pfcti: convert a float to a signed integer. This requires a transfer via memory of a 32-bit integer from a float register to an int register, which our memory model cannot express. Expands to:

          fctiwz  f13, rsrc
          stfdu   f13, -8(r1)
          lwz     rdst, 4(r1)
          addi    r1, r1, 8
  

• Pfctiu: convert a float to an unsigned integer. The PowerPC way to do this is to compare the argument against the floating-point constant 2^31, subtract 2^31 if bigger, then convert to a signed integer as above, then add back 2^31 if needed. Expands to:

          addis   r12, 0, ha16(lbl1)
          lfd     f13, lo16(lbl1)(r12)
          fcmpu   cr7, rsrc, f13
          cror    30, 29, 30
          beq     cr7, lbl2
          fctiwz  f13, rsrc
          stfdu   f13, -8(r1)
          lwz     rdst, 4(r1)
          b       lbl3
  lbl2:   fsub    f13, rsrc, f13
          fctiwz  f13, f13
          stfdu   f13, -8(r1)
          lwz     rdst, 4(r1)
          addis   rdst, rdst, 0x8000
  lbl3:   addi    r1, r1, 8
          .const_data
  lbl1:   .long   0x41e00000, 0x00000000    # 2^31 in double precision
          .text
  

• Pictf: convert a signed integer to a float. This requires complicated bit-level manipulations of IEEE floats through mixed float and integer arithmetic over a memory word, which our memory model and axiomatization of floats cannot express. Expands to:

          addis   r12, 0, 0x4330
          stwu    r12, -8(r1)
          addis   r12, rsrc, 0x8000
          stw     r12, 4(r1)
          addis   r12, 0, ha16(lbl)
          lfd     f13, lo16(lbl)(r12)
          lfd     rdst, 0(r1)
          addi    r1, r1, 8
          fsub    rdst, rdst, f13
          .const_data
  lbl:    .long   0x43300000, 0x80000000
          .text
  

(Don't worry if you do not understand this instruction sequence: intimate knowledge of IEEE float arithmetic is necessary.)

• Piuctf: convert an unsigned integer to a float. The expansion is close to that Pictf, and equally obscure.

          addis   r12, 0, 0x4330
          stwu    r12, -8(r1)
          stw     rsrc, 4(r1)
          addis   r12, 0, ha16(lbl)
          lfd     f13, lo16(lbl)(r12)
          lfd     rdst, 0(r1)
          addi    r1, r1, 8
          fsub    rdst, rdst, f13
          .const_data
  lbl:    .long   0x43300000, 0x00000000
          .text
  

• Pallocframe lo hi ofs: in the formal semantics, this pseudo-instruction allocates a memory block with bounds lo and hi, stores the value of register r1 (the stack pointer, by convention) at offset ofs in this block, and sets r1 to a pointer to the bottom of this block. In the printed PowerPC assembly code, this allocation is just a store-decrement of register r1, assuming that ofs = 0:

          stwu    r1, (lo - hi)(r1)
  

This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed following a stack discipline.

• Pfreeframe ofs: in the formal semantics, this pseudo-instruction reads the word at offset ofs in the block pointed by r1 (the stack pointer), frees this block, and sets r1 to the value of the word at offset ofs. In the printed PowerPC assembly code, this freeing is just a load of register r1 relative to r1 itself:

          lwz     r1, ofs(r1)
  

Again, our memory model cannot comprehend that this operation frees (logically) the current stack frame.

• Pbtbl reg table: this is a N-way branch, implemented via a jump table as follows:

          addis   r12, reg, ha16(lbl)
          lwz     r12, lo16(lbl)(r12)
          mtctr   r12
          bctr    r12
  lbl:    .long   table[0], table[1], ...
  

Note that reg contains 4 times the index of the desired table entry.

Operational semantics

The PowerPC has a great many registers, some general-purpose, some very specific. We model only the following registers:

The semantics operates over a single mapping from registers (type preg) to values. We maintain (but do not enforce) the convention that integer registers are mapped to values of type Tint, float registers to values of type Tfloat, and boolean registers (CARRY, CR0_0, etc) to either Vzero or Vone.

Looking up instructions in a code sequence by position.

Position corresponding to a label

Some PowerPC instructions treat register GPR0 as the integer literal 0 when that register is used in argument position.

The two functions below axiomatize how the linker processes symbolic references symbol + offset and splits their actual values into two 16-bit halves.

The fundamental property of these operations is that, when applied to the address of a symbol, their results can be recombined by addition, rebuilding the original address.

The other axioms we take is that the results of the low_half and high_half functions are of type Tint, i.e. either integers, pointers or undefined values.

We also axiomatize the small data area. For simplicity, we claim that small data symbols can be accessed by absolute 16-bit offsets, that is, relative to GPR0. In reality, the linker rewrites the object code, transforming symb@sdarx(r0) addressings into offset(rN) addressings, where rN is the reserved register pointing to the base of the small data area containing symbol symb. We leave this transformation up to the linker.

Armed with the low_half and high_half functions, we can define the evaluation of a symbolic constant. Note that for const_high, integer constants are shifted left by 16 bits, but not symbol addresses: we assume (as in the low_high_half axioms above) that the results of high_half are already shifted (their 16 low bits are equal to 0).

The semantics is purely small-step and defined as a function from the current state (a register set + a memory state) to either OK rs' m' where rs' and m' are the updated register set and memory state after execution of the instruction at rs#PC, or Error if the processor is stuck.

Manipulations over the PC register: continuing with the next instruction (nextinstr) or branching to a label (goto_label).

Auxiliaries for memory accesses, in two forms: one operand (plus constant offset) or two operands.

Operations over condition bits.

Execution of a single instruction i in initial state rs and m. Return updated state. For instructions that correspond to actual PowerPC instructions, the cases are straightforward transliterations of the informal descriptions given in the PowerPC reference manuals. For pseudo-instructions, refer to the informal descriptions given above. Note that we set to Vundef the registers used as temporaries by the expansions of the pseudo-instructions, so that the PPC code we generate cannot use those registers to hold values that must survive the execution of the pseudo-instruction.

Translation of the LTL/Linear/Mach view of machine registers to the PPC view. PPC has two different types for registers (integer and float) while LTL et al have only one. The ireg_of and freg_of are therefore partial in principle. To keep things simpler, we make them return nonsensical results when applied to a LTL register of the wrong type. The proof in Asmgenproof will show that this never happens.

Note that no LTL register maps to GPR12 nor FPR13. These two registers are reserved as temporaries, to be used by the generated PPC code.

Extract the values of the arguments of an external call. We exploit the calling conventions from module Conventions, except that we use PPC registers instead of locations.

Execution of the instruction at rs#PC.

Execution of whole programs.