CSDL OverviewRTLsLambda-RTLBasic RTL Operator LibrarySPARC DescriptionPentium excerpts

A Library of basic RTL operators

This chapter describes RTL operators and functions that we expect to be useful for describing many different machines. As we do throughout this document, we use the noweb literate-programming tool [cite ramsey:simplified] to present examples of lambda-RTL. Noweb extracts the code from the same files used to produce this document, so we can run the examples through the lambda-RTL compiler and make sure everything compiles.

A noweb file contains explanatory text interleaved with named ``code chunks,'' which contain source code and references to other code chunks. The names of chunks appear italicized and in angle brackets, as in the following C code: 

<summarize the problem>= [D->]
printf("Inputs are: ");
<for every i that is an input, print i and a blank>
printf("\n");

<for every i that is an input, print i and a blank>= (<-U)
for (i = 1; i < argc; i++)
  printf("%s ", argv[i]);

The === sign indicates the definition of a chunk. Definitions of a chunk can be continued in a later chunk; noweb concatenates their contents. Such a concatenation is indicated by a +=== sign in the definition: 

<summarize the problem>+= [<-D]
printf("Must process %d files\n", argc-1);

noweb adds navigational aids to the document. Each chunk name ends with the number of the page on which the chunk's definition begins. When more than one definition appears on a page, they are distinguished by appending lower-case letters to the page number. When a chunk's definition is continued, noweb includes pointers to the previous and next definitions, written ``<-D'' and ``D->.'' The notation ``<-U'' shows where a chunk is used.

The layout of the module is as follows: 

<basic.rtl>=
module StdOperators is
  import RTL
  <definitions of standard RTL operators and functions>
end

Because lambda-RTL does not yet have modules, we use noweb to include the chunk <definitions of standard RTL operators and functions> in our descriptions of the SPARC and the Pentium.

Building RTLs

lambda-RTL is intended for building RTLs, not analying them, so it doesn't expose all the structure of RTLs; single effects, guarded effects, and full RTLs (lists of guarded effects) all have the same type rtl. The initial basis provides ways to create and combine effects. We define a more compact, infix notation for parts of the basis. 

<definitions of standard RTL operators and functions>= (<-U) [D->]
val do_nothing is RTL.SKIP : rtl
val --> is RTL.GUARD       : bool * rtl -> rtl
val := is RTL.STORE        -- type is #n loc * #n bits -> rtl
infixr 1 -->
infixn 2 :=
Defines -->, :=, do_nothing (links are to index).

In the underlying representation, the semantics of these operations is extended to full RTLs in the obvious way. For example, RTL.STORE produces an RTL containing a single effect whose guard is true.

We don't need an explicit FETCH, because fetches are inserted automatically, and we don't need an explicit CONST, because lambda-RTL compiles literal constants into RTL CONST nodes.

We use a vertical bar to combine simultaneous effects, and a semicolon for sequential composition. One day, the lambda-RTL translator will translate sequential composition to simultaneous composition, using forward substitution. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
val | is RTL.PAR   : rtl * rtl -> rtl
val ; is RTL.SEQ   : rtl * rtl -> rtl
infixl 0 |
infixl ~1 ;

Booleans

true, false, and RTL.NOT are the Boolean operators in lambda-RTL's initial basis. We prefer to use not to stand for Boolean negation. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
val not is RTL.NOT
Defines not (links are to index).

For writing other Boolean functions lambda-RTL has only if-then-else-fi, which lambda-RTL rewrites into suitable guards. We would like to have connectives andalso and orelse, but introducing them presents a choice about level of detail: should they be introduced as new RTL operators, whose semantics must be defined outside of lambda-RTL, or should they be defined in terms of the existing lambda-RTL primitives? We would like to try both alternatives, because they provide different levels of detail in the generated RTLs.

Eventually, lambda-RTL will have mechanisms to support multiple levels of abstraction, probably by using some sort of parameterized modules. For now, we resort to some literate-programming tricks that are equivalent to conditional compilation. noweb can extract this code in two versions, designated simple and full. Code chunks tagged ((simple)) and ((full)) appear only in the corresponding versions, and untagged code chunks appear in both versions.

In the simple version, the boolean connectives are left abstract. In the full version, we give them their standard definitions. The simple version has the advantage that the RTLs are smaller and easier to read, but the disadvantage that the semantics have to be specified elsewhere. In the full version, these connectives are expanded to primitives, so they automatically get their proper semantics. 

<definitions of standard RTL operators and functions ((simple))>= [D->]
rtlop [andalso orelse] : bool * bool -> bool
Defines andalso, orelse (links are to index).

<definitions of standard RTL operators and functions ((full))>= [D->]
fun andalso (p, q) is if p then q    else false fi
fun orelse  (p, q) is if p then true else q     fi
Defines andalso, orelse (links are to index).

No matter what their definitions, we want these connectives to be left-associative infix operators. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
infixl 3 orelse
infixl 4 andalso

In the long run, equality and inequality will probably have to have some built-in semantics, but for now, we leave them abstract. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
rtlop    [eq ne] : #n bits * #n bits -> bool
val [= <>] is [eq ne]
infixn 5 [= <>]
Defines <>, eq, ne (links are to index).

These operators are shown in TeX as = and !=. We have chosen to make inequality a primitive RTL operator, although we could have defined it in terms of equality by writing val <> is \(x,y). not (x = y).

We can convert between booleans and bits. Again we have the choice of making things abstract or concrete. 

<definitions of standard RTL operators and functions ((simple))>+= [<-D->]
rtlop bit  : bool -> #1 bits   -- turn boolean into bit
rtlop bool : #1 bits -> bool   -- turn bit into boolean
Defines bit, bool (links are to index).

<definitions of standard RTL operators and functions ((full))>+= [<-D->]
fun bit  p is if p then 1 else 0 fi
fun bool n is n <> 0
Defines bit, bool (links are to index).

Integer arithmetic and comparisons

These operations represent integer arithmetic performed on the bit-vector representation. Here are addition and subtraction. We have to define addition and carry separately, because lambda-RTL won't permit RTL operators that return records or tuples. [This restriction is not strictly necessary, but we believe it should simplify construction of automatic RTL-based tools.] 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
local
  rtlop [add sub] : #n bits * #n bits -> #n bits
in 
  val [+ -] is [add sub]
end
rtlop [carry borrow] : #n bits * #n bits * #1 bits -> #1 bits
rtlop neg : #n bits -> #n bits   -- two's-complement negation
Defines +, -, add, borrow, carry, neg, sub (links are to index).

Note that this definition hides the names add and sub, using + and - instead.

To define combined versions add and subtract, we need sign extension and zero extension. These operators are polymorphic in the sizes of the arguments and results.[*] 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
rtlop [sx zx] : #n bits -> #m bits -- must have m > n
Defines sx, zx (links are to index).

Now we can define add and subtract to combine result and carry/borrow. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
infixl 6 [+ -]
fun add      (n, m, c) is { result is n + m + zx c, carry  is carry  (n, m, c) }
fun subtract (n, m, b) is { result is n - m - zx b, borrow is borrow (n, m, b) }
Defines add, subtract (links are to index).

The intended semantics of add and subtract is ``add with carry'' and ``subtract with borrow.''

Integer multiplication and division may be signed or unsigned. There are two sets of signed division operators because division may truncate towards -infinity (divs and mods) or towards 0 (quots and rems). There is, of course, no such distinction for unsigned division. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
local
 rtlop [mul mulUn] : #n bits * #n bits -> #m bits -- m = 2 * n
 rtlop [divRz divRn divUn modRz modRn modUn] : #m bits * #n bits -> #n bits -- m = 2 * n
in
 val [mulu  muls divu  divs  quot  modu  mods  rem] is
     [mulUn mul  divUn divRn divRz modUn modRn modRz]
end
Defines divRn, divRz, divs, divu, divUn, modRn, modRz, mods, modu, modUn, mul, muls, mulu, mulUn, quot, rem (links are to index).

The lambda-RTL type system is unable to express the constraints on the types of multiplication and division. We could play some games with the definitions (e.g., return two words and merge them with bitInsert), but it's not worth it at this time.

This code highlights the unpleasant question of naming RTL operators. As of July 1999, the names used in rtlop declarations are consistent with the names used in the VPOI code-generation interfaces. These names are, however, re-bound to other names, which are used in the actual machine descriptions. Eventually, it is hoped that VPO, lambda-RTL, C--, and the Princeton proof-carrying code project will agree on a set of names for operators.

Two's-complement signed integer comparison. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
local
  rtlop [lt le gt ge] : #n bits * #n bits -> bool
in
  val [< <= > >=] is [lt le gt ge]
end
Defines <, <=, >, >=, ge, gt, le, lt (links are to index).

Comparisons are left abstract instead of being defined in terms of < and =.

Unsigned comparison. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
local
  rtlop [ltUn leUn gtUn geUn] : #n bits * #n bits -> bool
in
  val [ult ule ugt uge] is [ltUn leUn gtUn geUn]
end
Defines geUn, gtUn, leUn, ltUn, uge, ugt, ule, ult (links are to index).

The arithmetic operators obey the usual rules of precedence. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
infixl 7 [divs mods quots rems divu modu quotu remu]
infixl 6 [+ -]
infixn 5 [< <= > >=]

Logical operators

Most processors offer a variety of bitwise operations on bit vectors, including those shown here. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
rtlop [and or xor] : #n bits * #n bits -> #n bits
rtlop com          : #n bits -> #n bits -- `complement' because `not' is boolean
rtlop bitInsert    : {lsb : #k bits, wide : #w bits} * #n bits -> #w bits
val bitInsert is \x.\y.bitInsert (x, y) -- curry
Defines and, bitInsert, com, or, xor (links are to index).

bitInsert inserts into a w-bit (``wide'') value. The thing inserted or extracted is n bits (``narrow''), and the widths of both wide and narrow values are normally inferred by the type system. We don't need a corresponding bitExtract because we can use lambda-RTL's built-in slicing operator instead.

There are instructions that manipulate bit fields whose widths aren't known statically. These computations can't be expressed with bitInsert and slicing, because we can't assign a type (width) to the results. But we can define bitTransfer as a combination extraction and insertion, and in fact, this is the way such instructions must behave. Even an instruction that extracts k bits from a 32-bit word, where k is not known until run time, must still insert the result into some value of known size---typically a 32-bit word of all zeros. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
rtlop bitTransfer :
 { src : {value : #w bits, lsb : #k bits}
 , dst : {value : #w bits, lsb : #k bits}
 , width : #k bits
 } -> #w bits
-- extract width bits from src at lsb, insert into dst at lsb
Defines bitTransfer (links are to index).

The width and lsb specifiers are assumed to have the same type.

Most processors have shift instructions. We could make the shift operations primitive RTL operators, or we could define them in terms of bit transfer. If shift is specified in terms of bit transfer, the width of the value shifted must be specified. This means for compatibility, we must specify the width for the primitive versions also. This situation is very unsatisfying. 

<definitions of standard RTL operators and functions ((simple))>+= [<-D]
local
  rtlop [lshift rshift rshiftA] : #k bits * #n bits * #k bits -> #n bits
in
  val [shl shrl shra] is [lshift rshift rshiftA]
end
Defines lshift, rshift, rshiftA, shl, shra, shrl (links are to index).

<definitions of standard RTL operators and functions ((full))>+= [<-D]
fun shl (w, n, k) is
  bitTransfer {src is {value is n, lsb is 0}, 
               dst is {value is 0, lsb is k}, 
               width is w - k}
fun shrl (w, n, k) is
  bitTransfer {src is {value is n, lsb is k}, 
               dst is {value is 0, lsb is 0}, 
               width is w - k}
fun shra (w, n, k) is
  bitTransfer {src is {value is n, lsb is k}, 
               dst is {value is sx n@bits[1 bit at w-1], lsb is 0}, 
               width is w - k}
Defines shl, shra, shrl (links are to index).

One alternative might be to provide a primitive to convert a static width parameter #n into an ordinary value parameter n. This alternative would require a lot of extra machinery, since at present, static width parameters to functions are all handled implicitly by the lambda-RTL translator.

Undefined effects

As of July 199, the lambda-RTL translator does not support the kill effects. In a later implementation, we plan to use the question mark to stand for an ``undefined'' value. All lambda-RTL functions and RTL operators will be strict in this value, and RTL.STORE(loc, ?) will become RTL.KILL loc. Because we would like to use the question mark in our example descriptions, even though lambda-RTL doesn't yet have the machinery to give it its eventual meaning, we introduce it as a nullary RTL operator. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D->]
local
  rtlop undefined : #k bits
in
  val ? is undefined
end
Defines ?, undefined (links are to index).

Floating-point arithmetic

Floating-point operations need to come in different families, so for example we could distinguish IEEE 754 floating point from VAX floating point. It therefore seems reasonable to put these operators in their own nested module. 

<definitions of standard RTL operators and functions>+= (<-U) [<-D]
module IEEE754 is 
  <IEEE 754 floating point>
end

Many floating-point operations that we normally think of as binary can't be treated as binary in lambda-RTL, because their results depend on the rounding mode, which must be passed as an additional argument. 

<IEEE 754 floating point>= (<-U) [D->]
local
  rtlop [negF fabs]            : #k bits -> #k bits              -- exact (no rounding)
  rtlop [fsqrt]                : #k bits * #2 bits -> #k bits    -- rounded
  rtlop [addF subF mulF divF]  : #k bits * #k bits * #2 bits -> #k bits
  rtlop [fmulx]                : #k bits * #k bits -> #n bits    -- where #n = 2 #k 
in
  val [fneg fabs fsqrt fadd fsub fmul fdiv fmulx] is 
      [negF fabs fsqrt addF subF mulF divF fmulx]
end
Defines addF, divF, fabs, fadd, fdiv, fmul, fmulx, fneg, fsqrt, fsub, mulF, negF, subF (links are to index).

All these operators are polymorphic in the size of their operands, so they can be used for single-, double-, and extended-precision floats. fmulx (for ``exact'') produces an exact, double-size result, without rounding.

There are four rounding modes required by the standard. It's unfortunate that we seem to have to pick integer representations for these rounding modes, instead of leaving them more abstract, but lambda-RTL does not currently permit users to introduce abstract types. 

<IEEE 754 floating point>+= (<-U) [<-D->]
module Round is 
  rtlop [nearest zero down up] : #2 bits -- what to round toward
end
Defines down, nearest, up, zero (links are to index).

Conversions are polymorphic in two widths: the argument and result widths. The argument of type #2 bits represents the rounding mode. 

<IEEE 754 floating point>+= (<-U) [<-D->]
rtlop [i2f f2i f2f]        : #k bits * #2 bits -> #n bits
Defines f2f, f2i, i2f (links are to index).

There are the special values +/-0 and +/-infinity. 

<IEEE 754 floating point>+= (<-U) [<-D->]
rtlop [pzero mzero] : #n bits
rtlop [pinf  minf]  : #n bits
Defines minf, mzero, pinf, pzero (links are to index).

There are NaNs. 

<IEEE 754 floating point>+= (<-U) [<-D->]
rtlop NaN  : #k bits -> #n bits -- function from significand to value
Defines NaN (links are to index).

A floating-point comparison produces one of four results: less, equal, greater, or unordered. Because we don't want to fix particular 2-bit representations of these results, we create RTL operators to describe them. 

<IEEE 754 floating point>+= (<-U) [<-D]
module Comparison is 
  rtlop [float_lt float_eq float_gt unordered] : #2 bits
  val [< = >] is [float_lt float_eq float_gt]
end
local
  rtlop cmpF : #k bits * #k bits -> #2 bits
in
  val fcmp is cmpF
end
Defines <, >, cmpF, fcmp, float_eq, float_gt, float_lt, unordered (links are to index).

CSDL OverviewRTLsLambda-RTLBasic RTL Operator LibrarySPARC DescriptionPentium excerpts

Index of identifiers

List of code chunks

CSDL OverviewRTLsLambda-RTLBasic RTL Operator LibrarySPARC DescriptionPentium excerpts
Back to Lambda-RTL home page