| CSDL Overview | RTLs | Lambda-RTL | Basic RTL Operator Library | SPARC Description | Pentium excerpts |
This chapter shows how we use lambda-RTL to describe some aspects of the Pentium instruction set that don't have obvious analogs on the SPARC. Most Pentium instructions come in byte, word (16-bit), and doubleword variants, and these variants treat parts of the Pentium registers as first-class locations. We show how to work with these locations and how to give them their usual names. A single effective address can refer to different parts of a register depending on the opcode with which it is used, so we specify the meanings of effective addresses as triples from which one element is selected depending on context.
By a mixture of opcodes and instruction prefixes, the Pentium offers many variants of each basic operation, so factoring the specification is a concern. We use the logical instructions to illustrate aggressive factoring, different notations for instructions that implement binary operations, and a slightly different treatment of condition codes.
The large-scale structure of the Pentium description resembles that of
the SPARC description, except that we add some examples that use infix
and.
<intel.rtl>=
module Pentium is
import RTL
from StdOperators import [ + - := bit < > <= >= | = ? and or xor com shrl shl sx zx ]
<basics>
<effective-address utilities>
<effective addresses>
val [OF CF AF SF ZF PF] is [Reg.OF Reg.CF Reg.AF Reg.SF Reg.ZF Reg.PF]
<utilities>
local infixl 3 and
in default attribute of <instruction defaults using infix and>
end
default attribute of <instruction defaults>
end
DefinesAF,CF,OF,PF,SF,ZF(links are to index).
<basics>= (<-U) [D->] storage 'r' is 8 cells of 32 bits called "registers" 'm' is cells of 8 bits called "memory" aggregate using RTL.AGGL
<basics>+= (<-U) [<-D->] module Reg is <registers> end
--- --- --- #2
--- --- ---
#5 --- --- |height 10pt --- |#3 --- |#4|
--- 32 --- 16 ---
8 ---
0
--- ---
--- --- #1
--- --- |height 10pt ---
|#2|
--- 32 --- 16 ---
---
0
--- ---
--- --- #1
Register
EAXAXAHAL0
ECXCXCHCL1
EDXDXDHDL2
EBXBXBHBL3
ESPSP4
EBPBP5
ESISI6
EDIDI7
Intel Pentium registers [*]
It is straightforward to define these locations in lambda-RTL.
<registers>= (<-U) [D->]
locations
[ EAX ECX EDX EBX ESP EBP ESI EDI ] is $r[[0..7]]
-- EAX is $r[0], etc...
[ AX CX DX BX SP BP SI DI ] is $r[[0..7]] @ loc [0..15]
[ AL CL DL BL ] is [EAX ECX EDX EBX] @ loc [8 bits at 0]
[ AH CH DH BH ] is [EAX ECX EDX EBX] @ loc [8 bits at 8]
Dealing with the instruction encoding is more complex. Registers are referred to by number, but as can be seen from Figure [<-], the number doesn't uniquely determine the location. In fact, a register number maps to one of three locations, depending on context. These three arrays specify which register, or part thereof, is denoted by which number in which context:
<registers>+= (<-U) [<-D->] val byte is [. AL, CL, DL, BL, AH, CH, DH, BH .] val word is [. AX, CX, DX, BX, SP, BP, SI, DI .] val dword is [. EAX, ECX, EDX, EBX, ESP, EBP, ESI, EDI .]
Definesbyte,dword,word(links are to index).
To find out which location is denoted by a register number, we use the number to index the array chosen to represent the proper context.
EFLAGS and EIP.
EIP is the instruction pointer.
EFLAGS is a collection of 1-bit status flags
and 1- or 2-bit control and system flags.
<registers>+= (<-U) [<-D->] storage 'c' is 2 cells of 32 bits called "control registers" locations [ EFLAGS EIP ] is $c[[0..1]]
What are commonly called condition codes are referred to as status flags in Intel documentation. The Pentium has six.
<registers>+= (<-U) [<-D] locations [ CF PF AF ZF SF OF ] is EFLAGS @ loc [1 bit at [0 2 4 6 7 11]] -- carry parity auxiliary-carry zero sign overflow
Most instructions set flags in stylized ways, as shown in
Table 3-2 on page 3-14 of the Pentium manual [cite intel:pentium].
In particular, the values of
SF, ZF, and PF are determined by simple tests of the result of an
operation.
We capture this common semantics in the lambda-RTL function set_flags.
OF, AF, and CF are set based on conditions that are
different for different kinds of instructions, so we pass their
values to set_flags.
We pass a record, not a tuple, to set_flags, so the order in which
values are given does not matter.
<utilities>= (<-U) [D->]
rtlop parity : #n bits -> #1 bits -- (number of bits set) mod 2
fun set_flags {result, o, a, c} is
SF := bit (result < 0) |
ZF := bit (result = 0) |
PF := bit (parity (result@bits[0..7]) = 0) |
OF := o | AF := a | CF := c
Definesparity,set_flags(links are to index).
Defining the other flags within EFLAGS is straightforward, and
they are omitted from this example.
regb, regw, and regd to be used in
these contexts.
<effective-address utilities>= (<-U) [D->] fun regb n is Reg.byte sub n -- returns an 8-bit location fun regw n is Reg.word sub n -- returns a 16-bit location fun regd n is Reg.dword sub n -- returns a 32-bit location
Definesregb,regd,regw(links are to index).
The context is usually determined by the opcode, not within the
effective address itself. We would nevertheless like an effective
address to have a denotation (a default attribute) independent of any
context.
Our solution to this problem is to let the denotation be a record with
three elements---one for each context.
The R function creates such a record from a register number.
We name the elements b, w, and d to stand for the byte,
word, and doubleword locations.
<effective addresses>= (<-U) [D->]
fun R n is {b is regb n, w is regw n, d is regd n}
DefinesR(links are to index).
An address in memory also stands for one of three locations, depending
on context.
(Because a location includes size as well as address,
we get one byte, two bytes, or four bytes, all at the same address.)
The M function does for memory what R does for registers: turn
a number into a collection of locations, one of which will be used
based on context.
We use type casts to give the sizes of the locations.
<effective addresses>+= (<-U) [<-D->]
fun M address is { b is $m[address] : #8 loc
, w is $m[address] : #16 loc
, d is $m[address] : #32 loc
}
DefinesM(links are to index).
Finally, in order to make immediate operands look like register or
memory operands, we define an I function, which creates a record
that provides the same immediate value, no matter what the context.
There's a little problem with polymorphism, in that the argument
immed cannot simultaneously have types #8 bits, #16 bits,
and #32 bits.
We work around
the problem by inserting a specious zero extension (zx).
Eventually, we'll probably need different functions for each type of immediate value.
<effective addresses>+= (<-U) [<-D->]
fun I immed is { b is zx immed : #8 bits
, w is zx immed : #16 bits
, d is zx immed : #32 bits
}
DefinesI(links are to index).
Effective addresses denote registers or memory locations.[*] In order to support LEA (load effective address), effective addresses for memory operands are represented by the address alone.
<effective addresses>+= (<-U) [<-D] default attribute of Indir (r) is regd r Disp8 (d8, r) is sx d8 + regd r Disp32 (d32, r) is d32 + regd r Index ( base, index, ss) is regd base + regd index << ss Index8 (d8, base, index, ss) is regd base + sx d8 + regd index << ss Index32 (d32, base, index, ss) is regd base + d32 + regd index << ss ShortIndex (d8, index, ss) is sx d8 + regd index << ss Abs32 (a) is a E (Mem) is M Mem Reg (r) is R r
We define C notation for 32-bit shifts.
<effective-address utilities>+= (<-U) [<-D] val [>> <<] is \(n, k).[shrl shl] (32, n, k) infixl 8 [>> <<]
Defines>>(links are to index).
We can't have constructors without naming the types of the operands. Here are the types recovered automatically from the SLED specification.
<basics>+= (<-U) [<-D->] operand ss : #2 bits operand [ base index r16 r32 r8 sr16] : #3 bits operand i8 : #8 bits operand i16 : #16 bits operand i32 : #32 bits
And here are additional types written in by hand.
<basics>+= (<-U) [<-D]
operand d8 : #8 bits
operand [a d32] : #32 bits
operand [r reg] : #3 bits
operand Mem : #32 bits
operand addr : { b : #8 loc, w : #16 loc, d : #32 loc }
The Pentium architecture provides more opportunities for factoring than does the SPARC. Most instructions come in three size variants, and each variant uses one of the three contexts. These variants would be tedious to specify repetitiously, so we use lambda-RTL's higher-order functions and generators to reduce repetition. The rest of this chapter offers several alternative ways to handle this kind of variation, using the logical instructions as a running example.
A very common pattern of execution is the ``two-operand instruction,''
which we can write l :=l <x>r
where <x> is a generic binary operator,
l is an effective address dependent on context,
and r could be a context-dependent effective address or an immediate
value that has been ``put in context'' by the I function.
The lambda-RTL function llr embodies this pattern of computation.
It takes two (curried) arguments: the triple (l, <x>, r), and
a size function that determines the context by choosing the b,
w, or d element
from each operand record.
Actually, we wind up making size a pair of functions
(sl and sr), because Milner's type inference can't infer a
polymorphic type for a parameter, and therefore using a single
size function would force both left and right to have the
same type.
We don't want that, because we want freedom for right to be either
a location like left or for it to be a value.
<utilities>+= (<-U) [<-D->]
fun llr (left, op, right) (size as (sl, sr)) is sl left := op((sl left), sr right)
fun [b w d] {b, w, d} is [b w d] -- b, w, d select correct size from record
val [b w d] is [(b,b) (w,w) (d,d)] -- b, w, d renamed to pairs
Definesb,d,llr,w(links are to index).
The function pairs
b, w, and d are used below as size arguments.
In lambda-RTL, one can declare any identifier to be an infix operator.
Infix operators can be convenient when specifying single instructions,
as shown in the specification of these three variants of AND,
which operate on the A register.
<instruction defaults using infix and>= (<-U) [D->]
ANDiAL (i8) is Reg.AL := Reg.AL and i8
ANDiAX (i16) is Reg.AX := Reg.AX and i16
ANDiEAX (i32) is Reg.EAX := Reg.EAX and i32
Infix notation is less convenient when describing groups of
instructions.
Here we use the llr function defined above to define some variants
that work on two or three sizes of values.
The parentheses around (and) convert it from an infix operator to
an ordinary value that can be passed as a parameter to
llr.
<instruction defaults using infix and>+= (<-U) [<-D->]
ANDi ^[b w d] (addr, i) is llr (addr, (and), I i) [b w d]
ANDio^[w d]^b (addr, i) is llr (addr, (and), I (sx i)) [ w d]
ANDmr^[b ow od] (addr, reg) is llr (addr, (and), R reg) [b w d]
ANDrm^[b ow od] (addr, reg) is llr (R reg, (and), addr) [b w d]
The I and R functions create three-element records that are
selected from by the size functions also passed to
llr. [N.B. we probably are going to have to split up the
immediate instructions because the types of their second operands are different.]
Groups in square brackets are used to define multiple variants at
once.
Each variant uses either b, w, or d as a size function.
Note that the parameter addr also represents a three-element
record.
This type is inferred.
The llr function helps factor the specification, but the ordinary
function-application syntax is
not very evocative of what is going on.
Here, we use the infix operators <==, <, and > with
non-standard meanings, creating a sort of ``mixfix'' notation
that is more suggestive of the semantics:
dstWe use the notation first, then define it.<==l<<x>>r.
<instruction defaults using infix and>+= (<-U) [<-D]
ANDiAL (i8) is Reg.AL := Reg.AL and i8
ANDiAX (i16) is Reg.AX := Reg.AX and i16
ANDiEAX (i32) is Reg.EAX := Reg.EAX and i32
ANDi^[b w d](addr, i) is bin (addr <== addr <(and)> I i) [b w d]
ANDio^[ w d]^b (addr, i) is bin (addr <== addr <(and)> I (sx i)) [ w d]
ANDmr^[b ow od] (addr, reg) is bin (addr <== addr <(and)> R reg) [b w d]
ANDrm^[b ow od] (addr, reg) is bin (R reg <== R reg <(and)> addr) [b w d]
We implement the notation by defining <==, <, and > to
build up records, then defining bin to create the effect
describing the assignment.
Since < and > have existing definitions from Chapter [->], we
save those definitions in lt and gt.
<utilities>+= (<-U) [<-D->]
nonfix [< >]
val [lt gt] is [< >] -- save these for later
fun < (l, operator) is { l is l, operator is operator }
fun > ({l, operator}, r) is { l is l, operator is operator, r is r }
fun <== (dst, {l, operator, r}) is { dst is dst, l is l, operator is operator, r is r}
infixn ~10 <
infixn ~11 >
infixn ~12 <==
fun bin {dst, l, operator, r} (sdl, sr) is sdl dst := operator (sdl l, sr r)
Defines<,<==,>,bin,gt,lt(links are to index).
Note that dst and l must have the same type.
This restriction is just fine, since on the Pentium they always have
the same value---the reason both dst and l are parameters is
purely notational.
It turns out that OR and XOR have the same structure as AND, so we factor the description to include those instructions as well. Once we do that, there's no point in making the operators infix.
<instruction defaults>= (<-U) [D->]
[AND OR XOR]^iAL (i8) is Reg.AL := [and or xor] (Reg.AL, i8)
[AND OR XOR]^iAX (i16) is Reg.AX := [and or xor] (Reg.AX, i16)
[AND OR XOR]^iEAX (i32) is Reg.EAX := [and or xor] (Reg.EAX, i32)
[AND OR XOR]^i^[b w d](addr, i) is
bin (addr <== addr <[and or xor]> I i) [b w d]
[AND OR XOR]^i^[ow od]^b (addr, i) is
bin (addr <== addr <[and or xor]> I (sx i)) [ w d]
[AND OR XOR]^mr^[b ow od] (addr, reg) is
bin (addr <== addr <[and or xor]> R reg) [b w d]
[AND OR XOR]^rm^[b ow od] (addr, reg) is
bin (R reg <== R reg <[and or xor]> addr) [b w d]
Now that we have machinery in place, a minor extension
will enable us also to specify the effects of these instructions on
the status flags (condition codes).
Section 4.4.1 of the Pentium manual says ``The AND, OR, and XOR
instructions clear the OF and CF flags, leave the AF flag undefined,
and update the SF, ZF, and PF flags.''
The function logical_flags implements this behavior.
<utilities>+= (<-U) [<-D->]
fun logical_flags n is set_flags {result is n, o is 0, c is 0, a is ?}
Defineslogical_flags(links are to index).
In our description of the SPARC, we defined a ``main effect'' function
like bin and passed it a function that set the condition code.
Here, we use a slightly different approach---we define bin' to
return both the main effect and the result of the instruction, and we
pass bin' and its arguments to a function that sets the condition
code.
<utilities>+= (<-U) [<-D->]
fun bin' {dst, l, operator, r} (sdl, sr) is
let val result is operator (sdl l, sr r)
in {result is result, effect is sdl dst := result}
end
Definesbin'(links are to index).
logical combines the ``main effect'' and the effects on the flags.
<utilities>+= (<-U) [<-D->]
fun logical main arg size is
let val {result, effect} is main arg size
in effect | logical_flags result
end
Defineslogical(links are to index).
Here's the final definition of 42 Pentium instructions, including
their effects on the flags.
We have re-cast the first three groups so we can apply logical.
Because Reg.AL represents a single location, not a triple, we use
(\x.x,\x.x) (the identity function) as a ``size selector.''
The same trick applies to Reg.AX and Reg.EAX.
<instruction defaults>+= (<-U) [<-D->]
[AND OR XOR]^iAL (i8) is
logical bin' (Reg.AL <== Reg.AL <[and or xor]> i8) (\x.x,\x.x)
[AND OR XOR]^iAX (i16) is
logical bin' (Reg.AX <== Reg.AX <[and or xor]> i16) (\x.x,\x.x)
[AND OR XOR]^iEAX (i32) is
logical bin' (Reg.EAX <== Reg.EAX <[and or xor]> i32) (\x.x,\x.x)
[AND OR XOR]^i^[b w d](addr, i) is
logical bin' (addr <== addr <[and or xor]> I i) [b w d]
[AND OR XOR]^i^[ow od]^b (addr, i) is
logical bin' (addr <== addr <[and or xor]> I (sx i)) [ w d]
[AND OR XOR]^mr^[b ow od] (addr, reg) is
logical bin' (addr <== addr <[and or xor]> R reg) [b w d]
[AND OR XOR]^rm^[b ow od] (addr, reg) is
logical bin' (R reg <== R reg <[and or xor]> addr) [b w d]
Finally, we can try for aggressive factoring without the infix
notation.
The function llr' is curried, so that applications won't be
cluttered with parentheses and commas, and it takes an extra
argument for an additional effect.
<utilities>+= (<-U) [<-D->] fun llr' l op r (sl, sr) extra is sl l := op(sl l, sr r) | extra (op(sl l, sr r)) fun logical' l op r size is llr' l op r size logical_flags val idsize is (\x.x, \x.x)
Definesidsize,llr',logical'(links are to index).
<instruction defaults>+= (<-U) [<-D->] [AND OR XOR]^iAL (i8) is logical' Reg.AL [and or xor] i8 idsize [AND OR XOR]^iAX (i16) is logical' Reg.AX [and or xor] i16 idsize [AND OR XOR]^iEAX (i32) is logical' Reg.EAX [and or xor] i32 idsize [AND OR XOR]^i^[b w d](addr, i) is logical' addr [and or xor] (I i) [b w d] [AND OR XOR]^i^[ow od]^b (addr, i) is logical' addr [and or xor] (I (sx i)) [w d] [AND OR XOR]^mr^[b ow od] (addr, reg) is logical' addr [and or xor] (R reg) [b w d] [AND OR XOR]^rm^[b ow od] (addr, reg) is logical' (R reg) [and or xor] addr [b w d]
The remaining logical instruction, NOT, comes in only three variants,
and it does not affect the condition codes.
Even though NOT is unary, we still pass a pair of size functions, so
that we can reuse b, w, and d as defined above.
<instruction defaults>+= (<-U) [<-D->] NOT^[b ow od] (addr) is unary (com, addr) [b w d]
<utilities>+= (<-U) [<-D] fun unary (op, v) (size, _) is size v := op (size v)
Definesunary(links are to index).
<instruction defaults>+= (<-U) [<-D] LEAod (reg, Mem) is regd reg := Mem LEAow (reg, Mem) is regw reg := Mem @bits[16 bits at 0]
| CSDL Overview | RTLs | Lambda-RTL | Basic RTL Operator Library | SPARC Description | Pentium excerpts |
and>: U1, D2, D3, D4
| CSDL Overview | RTLs | Lambda-RTL | Basic RTL Operator Library | SPARC Description | Pentium excerpts |