Initial draft of PNaCl bitcode files document.

native_client_sdk/src/doc/reference/pnacl-bitcode-manual.rst

Index: native_client_sdk/src/doc/reference/pnacl-bitcode-manual.rst
diff --git a/native_client_sdk/src/doc/reference/pnacl-bitcode-manual.rst b/native_client_sdk/src/doc/reference/pnacl-bitcode-manual.rst
new file mode 100644
index 0000000000000000000000000000000000000000..dba258082834b409e07a9b73d8f1f21b004a8c24
--- /dev/null
+++ b/native_client_sdk/src/doc/reference/pnacl-bitcode-manual.rst
@@ -0,0 +1,4740 @@
+===================================
+PNaCl Bitcode File Reference Manual
+===================================
+
+.. contents::
+   :local:
+   :backlinks: none
+   :depth: 3
+
+
+Introduction
+============
+
+This document is a reference manual for the contents of PNaCl bitcode files. It
+is presented using assembly language *PNaClAsm*. PNaClAsm uses a *static single

[jvoung (off chromium), 2014/06/06 20:09:14]

Perhaps mention that there are three layers up front (PNaClAsm, PNaCl records,
bit sequencing with abbreviations), since this section introduces the three?

[Karl, 2014/06/30 22:09:06]

Good suggestion. Done.

+assignment* (SSA) based representation that requires generated results to have a
+single (assignment) source. PNaClAsm is the textual version of the bitcode file.
+
+PNaClAsm focuses on the semantic content of the file, not the bit-encoding of
+that content. However, it does provide annotations that allow one to specify how
+the PNaCl bitcode writer converts the semantic content of a PNaClAsm program,
+into a specific bit sequence.
+
+Below PNaClAsm is the high-level form of the data stored in PNaCl bitcode

[jvoung (off chromium), 2014/06/06 20:09:15]

"Below PNaClAsm is the high-level..."

Sounds a bit odd, like the description must have started at a pretty high level
for "below" to still have another "high-level" under it =)

Do you mean "abstraction" ?

[Karl, 2014/06/30 22:09:03]

Decided to just call it the "textual" form.

+files. Each construct in PNaClAsm defines a corresponding *PNaCl record* [ref].
+A PNaCl bitcode file is simply a sequence of PNaCl records. The goal of PNaClAsm
+is to make records easier to read, and not to define a high-level user
+programming language.
+
+PNaCl records are an abstract encoding of structured data, similar to XML. Like
+XML, PNaCl records have a notion of tags (i.e. the first element in a record,
+called a *code*), and nested structures. The nested structures are defined by
+corresponding *enter* and *exit* block records.
+
+These block records must be used like balanced parentheses to define the block
+structure that is imposed on top of records. Each exit record must be preceded
+by a corresponding enter record. Blocks can be nested by nesting enter/exit
+records appropriately.
+
+The *PNaCl bitcode writer* takes the sequence of records, defined by a PNaClAsm
+program, and converts each record into a (variable) sequence of bits. The output
+of each bit sequence is appended together. The resulting generated sequence of
+bits is the contents of the PNaCl bitcode file.
+
+For every kind of record, there is a default method for converting records into
+bit sequences. These methods correspond to a notion of *abbreviations*
+[ref]. Each abbreviation defines a specific bit sequence conversion to be
+applied. The default conversion methods are simply predefined abbreviations.
+
+The default abbreviations can be overridden with user-specified abbreviations.
+All user-specified abbreviations are included in the generated bitcode
+file. Each abbreviation defines how a record is converted to a bit sequences. The

[Jim Stichnoth, 2014/06/06 18:24:46]

80-col
either "to bit sequences" or "to a bit sequence"

+*PNaCl bitcode writer* uses these abbreviations to convert the corresponding
+record sequence into a corresponding bit sequence. As a result, all records have
+an abbreviation (user or default) associated with them.
+
+The *PNaCl bitcode reader* then uses these abbreviations to convert the bit
+sequences back into the corresponding records.
+
+Conceptually, abbreviations are used to define how to pack the contents of
+records into bit sequences.  The main reason for defining abbreviations is to
+save space. The default abbreviations are simplistic and are intended to handle
+all possible records. The default abbreviations do not really worry about being
+efficient, in terms of the number of bits generated.
+
+By separating the concepts of PNaCl records and abbreviations, the notion of
+data compression is cleanly separated from semantic content. This allows
+different use cases to decide how much effort should be spent on compressing
+records.
+
+For a JIT compiler that produces bitcode, little (if any) compression should be
+applied. In fact, the API to the JIT may just be the records themselves.  The
+goal of a JIT is to perform the final translation to machine code as quickly as
+possible.  On the other hand, when delivering across the web, one may want to
+compress the sequence of bits considerably, to reduce costs in delivering web
+pages.
+
+Data Model
+==========
+
+The data model for PNaCl bitcode is fixed at little-endian ILP32: pointers are
+32 bits in size. 64-bit integer types are also supported natively via the i64
+type (for example, a front-end can generate these from the C/C++ type *long
+long*).
+
+Integers are assumed to be modeled using two's complement.  Floating point
+support is fixed at IEEE 754 32-bit and 64-bit values (f32 and f64,

[jvoung (off chromium), 2014/06/06 20:09:13]

I think it's called "double" and "float" in the asm syntax actually?

[Karl, 2014/06/30 22:09:06]

Done.

+respectively).
+
+
+Identifiers
+===========

[jvoung (off chromium), 2014/06/06 20:09:14]

Feels a bit early to talk about identifiers. Should the Blocks be introduced
first? After all, the first sentence of this Identifiers section introduces
blocks. Can the blocks section be described without introducing identifiers?

Also, the identifiers depend on the specific blocks, and which specific blocks
are available aren't introduced yet.

[Karl, 2014/06/30 22:09:04]

Good point. Moving after PNaCl blocks.

+
+A program is defined as a sequence of top-level *blocks*. Blocks can be nested
+within other blocks. Each block defines a sequence of records.
+
+Most of the records, within a block, also define unique values.  Each unique
+value is given a corresponding unique identifier (i.e. *ID*). In PNaClAsm. each
+kind of block defines its own kind of identifiers. The names of these
+identifiers are defined by concatenating a prefix character ('@' or '%'), the
+kind of block (a single character), and a suffix index. The suffix index is
+defined by the positional location of the defined value within the records of
+the corresponding block. The indices are all zero based, meaning that the first
+defined value (within a block) is defined using index 0.
+
+Identifiers are categorized into two types, *local* and *global*. Local
+identifiers are identifiers that are associated with the implementation of a
+single function. In that sense, they are local to the block they appear in.
+
+All other identifiers are global. This split is intentional. Global identifiers
+are used by multiple functions, and therefore must be known in all function
+implementations. Local identifiers only apply to a single function, and can be
+reused between functions.  The *PNaCl translator* uses this separation to
+parallelize the compilation of functions.
+
+In general, global identifiers are tied to a specific type of block. Local identifiers

[Jim Stichnoth, 2014/06/06 18:24:50]

80-col

+are unique to the function block they appear in.
+
+Local abbreviation identifiers are unique to the block they appear in. Global
+abbreviation identifiers are only unique to the block type they are defined
+for. Different block types can reuse global abbreviation identifiers.
+
+Global identifiers use the prefix character *'@'* while local identifiers use
+the prefix character *'%'*.
+
+Note that by using positional location to define identifiers (within a block),
+the values defined in PNaCl bitcode files need not be explicitly included in the
+bitcode file. Rather, they are inferred by the (ordered) position of the record
+in the block.  This is also intentional. It is used to reduce the amount of data
+that must be (explicitly) passed to the PNaCl translator, and downloaded though
+the internet.
+
+In general, most of the records within blocks are assumed to be topologically
+sorted, putting value definitions before their uses.  This implies that records
+do not need to encode data if they can deduce the corresponding information from
+their uses.
+
+The most common use of this is that many instructions use the type of their
+operands to determine the type of the instruction. Again, this is
+intentional. It allows less information to be stored.
+
+However, for function blocks (which define instructions), no topological sort
+exists. Loop carried value dependencies simply do not allow topologically
+sorting. To deal with this, function blocks have a notion of a forward
+(instruction value) declaration. These declarations must appear before any of
+the uses of that value, if the (instruction) value is defined later in the
+function than its first use [ref - Forward type declarations].
+
+The kinds of identifiers used in PNaClAsm are:
+
+@a
+  Global abbreviation identifier.
+
+%a
+  Block local abbreviation identifier.
+
+%b
+  Function local basic block identifier.
+
+%c
+  Function local constant identifier.
+
+@f
+  Global function address identifier.
+
+@g
+  Global variable/constant address identifier.
+
+%p
+  Function local parameter identifier.
+
+@t
+  Global type identifier.
+
+%v
+  Function local instruction generated value identifier.
+
+PNaCl Blocks
+============
+
+Blocks are used to organize records in the bitcode file.  The kinds of blocks
+defined in PNaClAsm are:
+
+Module block
+  A top-level block defining the program. This block defines global information
+  used by the program, followed by function blocks defining the implementation
+  of functions within the program.
+
+Types block
+  Defines the set of types used by the program. All types used in the program
+  must be defined in this block. These types consist of primitive types as well
+  as high level constructs such as vectors and function signatures.
+
+Globals block
+  Defines the set of global addresses of global variables and constants used by
+  the program. It also defines how each global (associated with the global
+  address) is initialized.
+
+Valuesymtab block
+  Defines textual names for global and function addresses.
+
+Function block
+  Each function (implemented) in a program has its own block that defines the
+  implementation of the corresponding function.
+
+Constants block
+  Each implemented function, that uses constants in its instructions, defines a
+  constant block. Constants blocks appear within the corresponding function
+  block.
+
+Abbreviations block
+  Defines global abbreviations that are used to compress PNaCl records. This
+  block is segmented into multiple sections, one section for each kind of
+  block. This block appears at the beginning of the module block.
+
+This section is only intented as a high-level discussion of blocks. Later

[Jim Stichnoth, 2014/06/06 18:24:49]

intended

[Karl, 2014/06/30 22:09:05]

Done.

+subsections will dive more deeply into the constraints on how blocks must be
+layed out. This section only presents the overall concepts of what types of data

[Jim Stichnoth, 2014/06/06 18:24:49]

laid

+is stored in each of the modules.

[Jim Stichnoth, 2014/06/06 18:24:46]

are stored

+
+A PNaCl program consists of a header record and a module block. The header
+defines a sequence of bytes uniquely identifying the file as a bitcode file. The
+module block defines the program to run.
+
+Each block, within a bitcode file, defines values. These values are associated

[jvoung (off chromium), 2014/06/06 20:09:13]

regarding the earlier comment about swapping the order of Blocks and
Identifiers, maybe this specific paragraph can be moved to the beginning of the
identifiers block?

+with IDs. Each type of block defines different kinds of IDs.  The module, types,
+globals, and abbreviations blocks define global identifiers, and only a single
+instance can appear.  The function and constant blocks define local identifiers,
+and can have mlutiple instances (one for each implemented function).

[Jim Stichnoth, 2014/06/06 18:24:48]

multiple

[jvoung (off chromium), 2014/06/06 20:09:15]

multiple

+
+Each *function block* [ref] defines the implementation of a single
+function. Each function block defines the intermediate representation of the
+function, consisting of basic blocks and instructions. If constants are used
+within instructions, they are defined in a *constants block*, nested within the
+corresponding function block.
+
+All function blocks are associated with a corresponding function address. This
+association is (again) positional rather than explicit. That is, the Nth
+function block in a module block corresponds to the Nth defining (rather than
+declared) function address record in the module block.
+
+Hence, within a function block, there is no explicit reference to the
+function address the block defines. For readability, PNaClAsm uses the
+corresponding function heading, associated with the corresponding
+function address record, even though that data does not appear in the
+corresponding records.
+
+PNaCl Records
+=============
+
+A PNaCl record is a non-empty sequence of unsigned, 64-bit, integers. A record
+is identified by the record *code*, which is the first element in the
+sequence. Record codes are unique within a specific kind of block, but are not
+necessarily unique across different kinds of blocks. The record code acts as the
+variant discriminator (i.e. tag) within a block, to identify what kind of record
+it is.
+
+Record codes that are local to a specific kind of block are small values
+(staring from zero). In an ideal world, they would be a consecutive sequence of

[Jim Stichnoth, 2014/06/06 18:24:49]

starting

[Karl, 2014/06/30 22:09:04]

Done.

+integers, starting at zero. However, the reality is that PNaCl records evolved
+over time (and actually started as LLVM records [ref]).  For backwards
+compatibility, old numbers have not been reused, leaving gaps in the actual
+record code values used.
+
+Global record codes are record codes that have the same meaning in multiple
+kinds of block. To separate global record codes from local record codes, large
+values are used.  Currently there are four global record codes.  To make these
+cases clear, and to leave room for lots of future growth in PNaClAsm, these
+special records have record codes close to the value 2**16. Note: Well-formed
+PNaCl bitcode files do not have record codes >= 2**16.
+ 
+A PNaCl record is denoted as follows:
+
+.. naclcode::
+
+  a: <v0, v1, ... , vN>
+
+The value *v0* is the record code. The remaining values, *v1* through *vN*, are
+parameters that fill in additional information needed by the construct it
+represents. All records must have a record code. Hence, empty PNaCl records are
+not allowed.
+
+While most records (for a given record code) are of the same length, it is not
+true of all record codes. Some record codes can have arbitrary length. In
+particular, function type signatures, call instructions, phi nodes, switch
+instructions, and global variable initialization records all have variable
+length.

[jvoung (off chromium), 2014/06/06 20:09:14]

Should this reference a section that describes how a reader might determine the
length then (or describe inline)?

[Karl, 2014/06/30 22:09:04]

Added a couple of sentences trying to clarify this.

+
+Records are converted to bit sequences using an abbreviation. Let *a* the the index

[Jim Stichnoth, 2014/06/06 18:24:50]

the the --> be the
also, 80-col

[Karl, 2014/06/30 22:09:05]

Removed paragraph. presented too early to be useful.

+identifying the abbreviation that is used to convert the record to a sequence of
+bits. If a user-defined abbreviation *%aA* (or *@aA* if global) is specified in
+the syntax, then *a = AbbrevIndex(%aA)*.
+
+The PNaCl bitcode writer, which converts records to bit sequences, does this by
+writing out the abbreviation index used to encode the record, followed by the
+contents of the record. The details of this are left to section on abbreviations

[Jim Stichnoth, 2014/06/06 18:24:47]

to section --> to the section
(though this will probably go away when refs are filled in...)

[Karl, 2014/06/30 22:09:03]

Done.

+[ref]. However, at the record level, one important aspect of this appears in
+block enter records.  These records must define how many bits are required to
+hold abbreviation indices associated with records of that block.
+
+There are 4 predefined (default) abbreviation indices, used as the default
+abbreviations for PNaCl records. They are:
+
+0
+  Abbreviation index for the abbreviation used to bit-encode an exit block
+  record.
+
+1
+  Abbreviation index for the abbreviation used to bit-encode a enter block

[Jim Stichnoth, 2014/06/06 18:24:47]

a enter --> an enter

[Karl, 2014/06/30 22:09:04]

Done.

+  record.
+
+2
+  Abbreviation index for the abbreviation used to bit-encode a user-defined

[jvoung (off chromium), 2014/06/06 20:09:14]

I don't know if it's too redundant, or clear as is, but my on first read the
phrase "a user-defined abbreviation record" didn't seem to denote strongly
enough that this where the user-supplied abbrevs get defined. Not sure if others
feel the same.

I think because of the semi-circularity: records are bit-encoded w/
abbreviations, but user-supplied abbreviation definitions are encoded as records
too!

[Karl, 2014/06/30 22:09:04]

I agree this isn't obvious. Added a sentence to help explain.

+  abbreviation record.
+
+3
+  Abbreviation index for the default abbreviation to bit-encode all other
+  records in the bitcode file.
+
+A block may (in addition), define a list of block specific, user-defined,
+abbreviations (of length *U*). The number of bits *B* specified for an enter
+record must be sufficiently large such that
+
+.. naclcode::
+
+   2**B >= U + 4
+
+In addition, the upper limit for B is 32.
+
+PNaClAsm requires that you specify the number of bits needed to read
+abbreviations as part of the enter block record. This allows the PNaCl bitcode
+reader/writer to use the specified number of bits to encode abbreviation
+indices.
+
+Conventions for describing records

[jvoung (off chromium), 2014/06/06 20:09:14]

nit: consistency in capitalization of section headers? (here plus elsewhere)

+==================================
+
+PNaClAsm is the textual representation of PNaCl records.  Each PNaCl record is
+described by a corresponding PNaClAsm construct. These constructs are described
+using syntax rules, and semantics on how they are converted to records. The

[jvoung (off chromium), 2014/06/06 20:09:14]

This is the first time "the parser" is mentioned.

"The parser also has state" or "A PNaClAsm parser would also have state"?

[Karl, 2014/06/30 22:09:04]

Tried to clear up that there is "global" state that gets updated by syntax
rules, and is used to capture positional context.

+parser also has state, that is updated after the record is processed.  These

[Jim Stichnoth, 2014/06/06 18:24:49]

either "state that" or "state, which"

+state updates are part of the semantics of the corresponding record construct.
+
+For each PNaCl construct, we define multiple subsections. The **Syntax**
+subsection defines a syntax rule for the construct. The **Record** subsection
+defines the corresponding record associated with the syntax rule. The
+**Semantics** subsection describes the semantics associated with the record, in
+terms of data within the parse state and the corresponding syntax. It also
+includes other high-level semantics, when appropriate.
+
+The **Constraints** subsection (if present) defines any constraints associated
+with the construct. The **Updates** subsection (if present) defines how the
+parse state is updated when the construct is parsed.  The **Examples**
+subsection gives one (or more) examples of using the corresponding PNaClAsm
+construct.
+
+Some semantics subsections use functions to compute values. The meaning of
+functions can be found in *Support Functions* [ref].
+
+Within a syntax rule, there may specifications about abbreviations.  These

[jvoung (off chromium), 2014/06/06 20:09:14]

"there may be specifications" ?

+abbreviation specifications, if allowed, are at the end of the construct, and
+enclosed in *<* and *>* brackets. These abbreviation specifications are optional
+in the syntax, and can be omitted. If they are used, the abbreviation brackets
+are part of the actual syntax of the construct. To make it clear that
+abbreviation specifications are optional, syntax rules separate abbreviation
+specifications using plenty of whitespace.
+
+Abbreviation specifications consist of user-defined abbreviations, abbreviation
+identifiers, and the number of bits required to represent abbreviations in a
+block. These notations appear, as appropriate, in the corresponding syntax
+rules.
+
+The most common abbreviation syntax is the corresponding abbreviation identifier
+to use to read/write the corresponding record. In such cases, if the specified
+abbreviation identifier is omitted, the corresponding default abbreviation will
+be used by the PNaCl reader/writer.
+
+Also, within the syntax rule, all alphabetic characters are lower case unless
+they appear within a literal value. Hence, if we mix lower and upper case
+letters within a name appearing in a syntax rule, the lower case letters are
+literal while the upper case sequence of letters denote (rule specific)

[jvoung (off chromium), 2014/06/06 20:09:13]

Earlier "all alphabetic characters are lower case unless they appear in a
literal value" (makes me think literal values will be upper case).

Now "the lower case letters are literal while the upper case... denote values"
(makes me think literal values will be lower case)

?

[Karl, 2014/06/30 22:09:04]

Rewrote. Hopefully clarified.

+values. If an upper case sequence of letters is followed by digits, the
+corresponding embedded name includes both the upper case letters and the digits.
+The valid values for each of these names will be defined in the corresponding
+semantics subsection.
+
+For example, consider the following syntax rule:
+
+.. naclcode::
+
+   %vN = add T O1, O2;                            <A>
+
+This rule defines a PNaClAsm add instruction.  This construct defines an
+instruction that adds two values (*O1* and *O2*) to generate instruction
+value *%vN*. The types of the arguments, and the result, are all of type
+*T*. Since abbreviation ID *A* is present, the record is encoded using that
+abbreviation.
+
+To be concrete, the syntactic rule above defines the structure of the following
+PNaClAsm examples.
+
+.. naclcode::
+
+  %v10 = add i32 %v1, %v2;  <@a5>
+  %v11 = add i32 %v10, %v3;
+
+In addition to specifying the syntax, each syntax rule also specifies the
+contents of the corresponding record in the corresponding record subsection. In
+simple cases, the elements of the corresponding record are predefined (literal)
+constants. Otherwise the record element is a name that is defined by the other
+subsections associated with the construct.
+
+Factorial Example
+=================
+
+This section provides a simple example of a PNaCl bticode file. Its contents

[Jim Stichnoth, 2014/06/06 18:24:49]

bitcode

[Karl, 2014/06/30 22:09:04]

Done.

+describes a bitcode file that only defines a function to compute the factorial

[Jim Stichnoth, 2014/06/06 18:24:47]

describe

+value of a number.
+
+In C, the factorial function can be defined as:
+
+.. naclcode::
+
+  int fact(int n) {
+    if (n == 0) return 1;
+    return n * fact(n-1);
+  }
+
+Compiling this into a PEXE file, and dumping out its contents with utility

[Jim Stichnoth, 2014/06/06 18:24:48]

Just checking - are we calling this a PEXE file in prose, or something like
PNaCl bitcode file?

[Karl, 2014/06/30 22:09:04]

Good point. I should call it the bitcode file, not a PEXE file to be consistent.

+*pnacl-bcdis*, the corresponding output is:
+
+.. naclcode::
+
+    0:0|<65532, 80, 69, 88, 69, 1, 0,|Magic Number: 'PEXE' (80, 69, 88, 69)
+       | 8, 0, 17, 0, 4, 0, 2, 0, 0, |PNaCl Version: 2
+       | 0>                          |
+   16:0|1: <65535, 8, 3>             |module {  // BlockID = 8
+   24:0|  3: <1, 1>                  |  version 1;
+   26:5|  1: <65535, 0, 2>           |  abbreviations {  // BlockID = 0
+   36:0|  0: <65534>                 |  }
+   40:0|  1: <65535, 17, 4>          |  types {  // BlockID = 17

[jvoung (off chromium), 2014/06/06 20:09:13]

Abbrev index bitwidth says "4", even though no user-defined abbrevs are defined.
I guess this is using the laxness of the rule that says the bitwidth doesn't
need to be minimal + a quirk in the way your tool erases abbreviations after the
fact.

Maybe for the example, just pretend abbrevs were erased optimally and say 2? 
Depends on if/what you add below, describing some of column 2.

Up to you... my reasoning is that reproducing this result where there are 0
abbreviations takes several steps. Also, if someone was to make a from-scratch
writer w/ no user-defined abbreviations, they would probably do it so that this
entry is "2".

[Karl, 2014/06/30 22:09:05]

Thanks for noting this. I didn't realize that we should fix this value when
removing abbreviations in pnacl-bccompress.

+   48:0|    3: <1, 4>                |    count 4;
+   50:6|    3: <7, 32>               |    @t0 = i32;
+   54:2|    3: <2>                   |    @t1 = void;
+   56:2|    3: <21, 0, 0, 0>         |    @t2 = i32 (i32);
+   60:4|    3: <7, 1>                |    @t3 = i1;
+   63:2|  0: <65534>                 |  }
+   64:0|  3: <8, 2, 0, 0, 0>         |  define external i32 @f0(i32);
+   68:7|  1: <65535, 19, 4>          |  globals {  // BlockID = 19
+   76:0|    3: <5, 0>                |    count 0;
+   78:6|  0: <65534>                 |  }
+   80:0|  1: <65535, 14, 4>          |  valuesymtab {  // BlockID = 14
+   88:0|    3: <1, 0, 102, 97, 99,   |    @f0 : "fact";
+       |        116>                 |
+   96:6|  0: <65534>                 |  }
+  100:0|  1: <65535, 12, 5>          |  function i32 @f0(i32 %p0) {  
+       |                             |                   // BlockID = 12
+  108:0|    3: <1, 3>                |    blocks 3;
+  110:7|    1: <65535, 11, 4>        |    constants {  // BlockID = 11
+  120:0|      3: <1, 0>              |      i32:
+  122:6|      3: <4, 2>              |        %c0 = i32 1;
+  125:4|      3: <4, 0>              |        %c1 = i32 0;
+  128:2|    0: <65534>               |      }
+       |                             |  %b0:
+  132:0|    3: <28, 1, 2, 32>        |    %v0 = icmp eq i32 %c1, %c0;
+  137:1|    3: <11, 1, 2, 1>         |    br i1 %v0, %b1, %b2;
+       |                             |  %b1:
+  141:4|    3: <10, 3>               |    ret i32 %c0;
+       |                             |  %b2:
+  144:3|    3: <2, 4, 3, 1>          |    %v1 = sub i32 %p0, %c0;
+  148:6|    3: <34, 0, 6, 1>         |    %v2 = call i32 @f0(i32 %p0);
+  153:7|    3: <2, 6, 1, 2>          |    %v2 = mul i32 @f0, %v1;
+  158:2|    3: <10, 1>               |    ret i32 %v2;
+  161:1|  0: <65534>                 |  }
+  164:0|0: <65534>                   |}
+
+
+Note that there are three columns in this output. The first column contains the
+bit positions of the records within the bitcode file. The second column contains
+the sequence of records within the bitcode file. The third column contains the
+corresponding PNaClAsm program.
+
+Bit positions are defined by a pair *B:N*. *B* is the number of bytes, while *N*
+is the bit offset within the *B+1* byte. Hence, the bit position (in bits) is:
+
+.. naclcode::
+
+  B*8 + N
+
+Hence, the first *header* record is at bit offset 0 (0*8+0). The second record
+is at bit offset 128 (16*8+0).  The third record is at bit offset 192 (24*8+0).
+The fourth record is at bit offset 213 (26*8+5).
+
+The header record is a sequence of 16 bytes, defining the contents of the first
+16 bytes of the bitcode file. The first four bytes define the magic number of
+the file. That is, 'PEXE'. All PEXE bitcode files begin with these four bytes.

[Jim Stichnoth, 2014/06/06 18:24:50]

the file, i.e. 'PEXE'.

[Karl, 2014/06/30 22:09:03]

Done.

+Byte 13 defines the PNaCl bitcode version of the file. Currently, only version 2

[jvoung (off chromium), 2014/06/06 20:09:13]

Only byte 13, or byte 13, 14, 15, and 16?

[Karl, 2014/06/30 22:09:06]

Simplified this to just state they shouldn't change for PNaCl version 2 files. 

+is allowed.

[jvoung (off chromium), 2014/06/06 20:09:14]

What about the bytes in between (5 through 12)? Considered opaque, or must be X,
Y, Z?

[Karl, 2014/06/30 22:09:06]

Done.

+
+All but the header record has an abbreviation index associated with it. Since no
+user-defined abbreviations are provided, all records use the default
+abbreviation.
+
+The types block (starting at bit address 40:0), defines 4 types: *i1*, *i32*,
+*void*, and function signature *i32(i32)*.
+
+Bit address 64:0 declares the factorial function address @f0, and its
+corresponding type signature. Bit address 88:0 associates the name "fact" with
+function address @f0.
+
+Bit address 100:0 defines the function block that implemnts function "fact". The

[Jim Stichnoth, 2014/06/06 18:24:47]

implements

+entry point is %b0 (at bit address 132:0). It uses the 32-bit integer constants
+1 and 0 (defined at bit addresses 122:6 and 125:4). Bit address 132:0 defines an
+equality comparison of the argument %p0 with 0 (constant %c1). Bit address 137:1
+defines a conditional branch. If the result of the previous comparison (%v0) is true,

[Jim Stichnoth, 2014/06/06 18:24:46]

80-col

+the program will branch to block %b1. Otherwise it will branch to block %b2.
+
+Bit address 141:4 returns constant 1 (%c0) when the input parameter is 0.
+Instructions between bit address 144:3 and 158:2 compute and return "n *
+fact(n-1)".

[jvoung (off chromium), 2014/06/06 20:09:13]

The second column isn't really described in this example?

[Karl, 2014/06/30 22:09:05]

yes.

+
+Parse State
+===========
+
+This section describes the parse state of the PNaClAsm assembler. It is used to
+define contextual data that is carried between records. The following
+subsections describe each element of the parse state.
+
+Typing
+------
+
+Associated with most identifiers is a type. This type defines what type the
+corresponding value has. It is defined by the (initially empty) map
+
+.. naclcode::
+
+  TypeOf: ID -> Type
+
+For each type in the *types block* [ref], a corresponding inverse map
+
+.. naclcode::
+
+  TypeID: Type -> ID
+
+is maintained to convert syntactic types to the corresponding type ID.
+
+Note: This document assumes that map *TypeID* is automatically maintained during
+updates to map *TypeOf* (when given a type ID). Hence, *updates* subsections
+will not contain assignments to this map.
+
+Associated with each function identifier is its type signature. This is
+different than the type of the function identifier, since function identifiers

[jvoung (off chromium), 2014/06/06 20:09:14]

would it help to say that "..., since function identifiers represent the
function  address which is a pointer (and pointers are always implemented as a
32-bit integer following the ILP32 data model)." or something to that effect?

[Karl, 2014/06/30 22:09:02]

Done.

+are pointers (and always implemented as a 32-bit integer).
+
+Function type signatures are maintained using:
+
+.. naclcode::
+
+  TypeOfFcn: ID -> Type
+
+In addition, if a function address has an implementing block, there is a
+corresponding implementation associated with the function address. To capture
+this association, we use the set:
+
+.. naclcode::
+
+  DefiningFcnIDs: set(ID)
+
+ID Counters
+-----------
+
+Each block defines one (or more) kinds of values.  Value indices are generated
+sequentially, starting at zero. To capture this, the following counters are
+defined:
+
+NumTypes
+  The number of types defined so far (in the types block)
+
+NumFuncAddresses
+  The number of function addresses defined so far (in the module block).
+
+NumDefinedFcnAddresses

[jvoung (off chromium), 2014/06/06 20:09:14]

How is this different from NumFuncAddresses? Update rules only mention
NumFuncAddresses.

[Karl, 2014/06/30 22:09:04]

These are two different values. Added additional sentences to clarify.

+  The number of defining function addresses defined so far (in the module
+  block).
+
+NumFuncImpls
+  The number of implemented functions defined so far (in the module block).
+
+NumGlobalAddresses
+  The number of global variable/constant addresses defined so far (in the
+  globals block).
+
+NumParams
+  The number of parameters defined for a function.
+
+NumFcnConsts
+  The number of constants defined in a function.

[jvoung (off chromium), 2014/06/06 20:09:13]

so far?

Depends on how you define the update rule in constants blocks.

Seems like NumParams is the only one where you know up front how many there
should be (via the function signature).

[Karl, 2014/06/30 22:09:03]

Done.

+
+NumBasicBlocks
+  The number of basic blocks defined so far (within a function block).
+
+NumValuedInsts
+  The number of instructions, generating values, defined so far (within a
+  function block).
+
+Size Variables
+--------------
+
+A number of blocks define expected sizes of constructs. These sizes are recorded
+in the following size variables:
+
+ExpectedBasicBlocks
+  The expected number of basic blocks within a function implementation.
+
+ExpectTypes
+  The expected number of types defined in the types block.
+
+ExpectedGlobals
+  The expected number of global variable/constant addresses in the globals
+  block.
+
+ExpectedInitializers
+  The expected number of initializers for a global variable/constant address in
+  the globals block.
+
+Other Variables
+---------------
+
+EnclosingFcnID
+  The function ID of the function block being processed.
+
+Global records
+==============
+
+There are four global PNaCl records, each having its own record code. These
+global records are:
+
+Header
+  The header record is the first record of a PNaCl bitcode file, and identifies
+  the file's magic number, as well as the bitcode version it uses. The record
+  defines the sequence of bytes that make up the header and uniquely identifies
+  the file as a PNaCl bitcode file.
+
+Enter
+  An enter record defines the beginning of a block. Since blocks can be nested,
+  one can appear inside other blocks, as well as at the top level.
+
+Exit
+  An exit record defines the end of a block. Hence, it must appear in every
+  block, to end the block.
+
+Abbreviation
+  An abbreviation record defines a user-defined abbreviation to be applied to
+  records within blocks.  Abbreviation records appearing in the abbreviations
+  block define global abbreviations. All other abbreviations are local to the
+  block they appear in, and can only be used in that block.
+
+All special records can't have user-defined abbreviations associated with
+them. The default abbreviation is always used.
+
+The following subsections define valid special records, other than abbreviation
+records. Abbreviation records are described in the Abbreviations [ref] section.
+
+Header Record
+-------------
+
+The header record must be the first record in the file. It is the only record in
+the bitcode file that doesn't have a corresponding construct in
+PNaClAsm.
+
+**Syntax**
+
+There is no syntax for header records in PNaClAsm. It is automatically inserted
+by the PNaCl bitcode writer.
+
+**Record**
+
+.. naclcode::
+
+   <65532, 80, 69, 88, 69, 1, 0, 8, 0, 17, 0, 4, 0, 2, 0, 0, 0>
+
+**Semantics**
+
+The header record defines the initial sequence of bytes that must appear at the
+beginning of all (PNaCl bitcode version 2) files. That sequence is the list of
+bytes inside the record (excluding the record code). As such, it uniquely
+identifies PNaCl bitcode files.
+
+**Examples**
+
+There are no examples for the header record, since it is not part of PNaClAsm.
+
+Enter Block Record
+------------------
+
+Block records can be top-level, as well as nested in other blocks. Blocks must
+begin with an *enter* record, and end with an *exit* record.
+
+**Syntax**
+
+.. naclcode::
+
+  N {                                             <B>
+
+**Record**
+
+.. naclcode::
+
+  1: <65535, ID, B>
+
+**Semantics**
+
+Enter block records define the beginning of a block.  *B*, if present, is the
+number of bits needed to represent all possible abbreviation indices used within
+the block. If omitted, B=2 is assumed.
+
+The block *ID* value is dependent on the name *N*. Valid names and corresponding
+*BlockID* values are defined as follows:
+
+============= ========
+N             Block ID
+============= ========
+abbreviations 0
+constants     11
+function      12
+globals       19
+module        8
+types         17
+valuesymtab   14
+============= ========
+
+Note: For readability, PNaClAsm allows a more readable form of a function block
+enter record.  See *function blocks* [ref] for more details.
+
+**Examples**
+
+.. naclcode::
+
+  module {
+    types {
+      count: 0;
+    }
+    globals {
+      count: 0;
+    }
+  }
+
+This example defines a module, types, and globals block. Both the type and the
+globals block appear within the module block.
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 8, 2>
+  1: <65535, 17, 2>
+  3: <1, 0>
+  0: <65534>
+  1: <65535, 19, 2>
+  3: <5, 0>
+  0: <65534>
+  0: <65534>
+
+Exit Block Record
+-----------------
+
+Block records can be top-level, as well as nested, records. Blocks must begin
+with an *enter* record, and end with an *exit* record.
+
+**Syntax**
+
+.. naclcode::
+
+  }
+
+**Record**
+
+.. naclcode::
+
+  0: <65534>
+
+**Semantics**
+
+All exit records are identical, no matter what block they are ending. An exit
+record defines the end of the block.
+
+**Examples**
+
+.. naclcode::
+
+  module {
+    types {
+      count: 0;
+    }
+    globals {
+      count: 0;
+    }
+  }
+
+This example defines a module, types, and globals block. Both the type and the
+globals block appear within the module block.
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 8, 2>
+  1: <65535, 17, 2>
+  3: <1, 0>
+  0: <65534>
+  1: <65535, 19, 2>
+  3: <5, 0>
+  0: <65534>
+  0: <65534>
+

[jvoung (off chromium), 2014/06/06 20:09:14]

Description for the remaining global record (abbreviation definition records)?
Or refer to a later section?

[Karl, 2014/06/30 22:09:04]

This was already stated in the enclosing section.

+Types Block
+===========
+
+The types block defines all types used in a program. It must appear in the
+module block, before any function address records, the globals block, the
+valuesymtab block, and any function blocks.
+
+All types used in a program must be defined in the types block. Many PNaClAsm
+constructs allow one to use explicit type names, rather than the type
+identifiers defined by this block. However, they are internally converted to the
+corresponding type identifer in the types block. Hence, the requirement that the
+types block must appear early in the module block.
+
+Each record in the types block defines a type used by the program.  Types can be
+broken into the following groups:
+
+Primitive Value types
+  Defines the set of base types for values. This includes various sizes of
+  integral and floating types.
+
+Void type
+  A primitive type that doesn't represent any value and has no size.
+
+Function types
+  The type signatures of functions.
+
+Vector type
+  Defines vectors of primitive types.
+
+In addition, any type that is not defined using another type is a primitive
+type.  All other types (i.e. function and vector) are composite types.
+
+Types must be defined in a topological order, causing primitive types to appear
+before the composite types that use them. Each type must be unique. There are no
+additional restrictions on the order that types can be defined in a types block.
+
+The following subsections introduce each valid PNaClAsm type, and the
+corresponding PNaClAsm construct that defines the type. Types not defined in the
+types block, can't be used in a PNaCl program.
+
+The first record of a types block must be a *count* record, defining how many
+types are defined by the types block. All remaining records defines a type. The
+following subsections define valid records within a types block. The order of
+type records is important. The position of each defining record implicitly
+defines the type ID that will be used to denote that type, within other PNaCl
+records of the bitcode file.
+
+To make this more concrete, consider the following example types block:
+
+.. naclcode::
+
+  types {
+    count: 4;
+    @t0 = void;
+    @t1 = i32;
+    @t2 = float;
+    @t3 = void (i32, float);
+  }
+
+This example defines a types block that defines four type IDs:
+
+0. The void type.
+1. A 32-bit integer type.
+2. A 32-bit floating type.
+3. A function, taking 32-bit integer and float arguments that returns void.
+
+Note that the order defines the corresponding identifier that will be used for
+that type, and is based on the position of the type within the types
+record. Hence, the assignment to identifier *@tN* can never appear before the
+assignment to identifier *@tN-1*. Further, if type identifier *@tN* is assigned,
+it must appear immediately after the assignment to identifier *@tN-1*.
+
+Count Record
+------------
+
+The *count record* defines how many types are defined in the types
+block. Following the types count record are records that define types used by
+the PNaCl program.
+
+**Syntax**
+
+.. naclcode::
+
+  count: N;                                       <A>
+
+**Record**
+
+  AA: <1, N>
+
+**Semantics**
+
+This construct defines the number of types used by the PNaCl program.  *N* is
+the number of types defined in the types block. It is an error to define more
+(or fewer) types than value *N*, within the enclosing types block. *A* is the
+(optional) abbreviation associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  0 == NumTypes
+
+**Updates**
+
+.. naclcode::
+
+  ExpectedTypes = N;
+
+**Examples**
+
+.. naclcode::
+
+  types {
+    count: 2;
+    @t0 = float;
+    @t1 = i32;
+  }
+
+This example defines two types.  A 32 bit integer and a 32 bit floating types.
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 17, 2>
+  3: <1, 2>
+  3: <3>
+  3: <7, 32>
+  0: <65534>
+
+Void Type
+---------
+
+The *void* type record defines the void type, which corresponds to the type that
+doesn't define any value, and has no size.
+
+**Syntax**
+
+.. naclcode::
+
+  @tN = void;                                     <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2>
+
+**Semantics**
+
+The void type record defines the type that has no values and has no size.  *A*
+is the (optional) abbreviation associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  N == NumTypes
+  NumTypes < ExpectedTypes
+
+**Updates**
+
+.. naclcode::
+
+  ++NumTypes;
+  TypeOf(@tN) = void;
+
+**Examples**
+
+.. naclcode::
+
+   @t0 = void;
+
+defines the record
+
+.. naclcode::
+
+  3: <2>
+
+Integer Types
+-------------
+
+PNaClAsm allows integral types for various bit sizes. Valid bit sizes are 1, 8,
+16, 32, and 64. Integers can be signed or unsigned, but the signed component of
+an integer is not specified by the type. Rather, individual instructions
+determine whether the value is assumed to be signed or unsigned.
+
+It should be noted that in PNaClAsm, all pointers are implemented as 32-bit
+(unsigned) integers.  There isn't a separate type for pointers. The only way to
+tell that a 32-bit integer is a pointer, is when it is used in an instruction
+that requires a pointer (such as load and store instructions).
+
+**Syntax**
+
+.. naclcode::
+
+  @tN = iB;                                      <A>
+
+**Record**
+
+  AA: <7, B>
+
+**Semantics**
+
+An integer type record defines an integral type. *B* defines the number of bits
+of the integral type.  *A* is the (optional) abbreviation associated with the
+record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  N == NumTypes
+  NumTypes < ExpectedTypes
+  B in {1, 8, 16, 32, 64}
+
+**Updates**
+
+.. naclcode::
+
+  ++NumTypes;
+  TypeOf(@tN) = iB;
+
+**Examples**
+
+.. naclcode::
+
+  @t1 = i32;
+  @t2 = i1;
+  @t3 = i64;
+
+defines the records
+
+.. naclcode::
+
+  3: <7, 32>
+  3: <7, 1>
+  3: <7, 64>
+
+32-Bit Floating Type
+--------------------
+
+PNaClAsm allows computation on 32-bit floating values. A floating type record

[jvoung (off chromium), 2014/06/06 20:09:13]

"floating type record" --> "float type record" ?

+defines the 32-bit floating type.
+
+**Syntax**
+
+.. naclcode::
+
+  @tN = float;                                    <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <3>
+
+**Semantics**
+
+A floating type record defines the 32-bit floating type.  *A* is the (optional)
+abbreviation associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A).
+  N == NumTypes
+  NumTypes < ExpectedTypes
+
+**Updates**
+
+.. naclcode::
+
+  ++NumTypes;
+  TypeOf(@tN) = float;
+
+**Examples**
+
+.. naclcode::
+
+  @t5 = float;
+
+defines the record
+
+.. naclcode::
+
+  3: <3>
+
+64-bit Floating Type
+--------------------
+
+PNaClAsm allows computation on 64-bit floating values. A double type record
+defines the 64-bit floating type.
+
+**Syntax**
+
+.. naclcode::
+
+  @tN = double;                                   <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <4>
+
+**Semantics**
+
+A double type record defines the 64-bit floating type.  *A* is the (optional)
+abbreviation associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  N == NumTypes
+  NumTypes < ExpectedTypes
+
+**Updates**
+
+.. naclcode::
+
+  ++NumTypes;
+  TypeOf(@tN) = double;
+
+**Examples**
+
+.. naclcode::
+
+  @t3 = double;
+
+defines the record
+
+.. naclcode::
+
+  3: <4>
+
+Vector Types
+------------
+
+TODO(kschimpf) <N x T>
+
+TODO(kschimpf) Define integral and floating vector types.
+
+Function Type
+-------------
+
+The *function* type can be thought of as a function signature. It consists of a
+return type, and a (possibly empty) list of formal parameter types.
+
+**Syntax**
+
+.. naclcode::
+
+  %tN = RT (T1, ... , TM)                         <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <21, 0, IRT, IT1, ... , ITM>
+
+**Semantics**
+
+The function type defines the signature of a function. *RT* is the return type
+of the function, while types *T1* through *TM* are the types of the
+arguments. Indicies to the corresponding type identifiers is stored in the

[Jim Stichnoth, 2014/06/06 18:24:48]

are stored

[Jim Stichnoth, 2014/06/06 18:24:48]

Indices

[Karl, 2014/06/30 22:09:03]

Done.

[Karl, 2014/06/30 22:09:06]

Done.

+corresponding record.
+
+The return value must either be a primitive type, type *void*, or a vector type.
+Parameter types can be a primitive or vector type.
+
+For the integral types, only i32 and i64 can be used for a return or parameter
+type. All other integral types are not allowed.
+
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  M >= 0
+  IRT = AbsoluteIndex(TypeID(RT))
+  IT1 = AbsoluteIndex(TypeID(T1))
+  ...
+  ITM = AbsoluteIndex(TypeID(TM))
+  N == NumTypes
+  NumTypes < ExpectedTypes
+
+**Updates**
+
+.. naclcode::
+
+  ++NumTypes;
+  TypeOf(@tN) = RT (T1, ... , TM)
+
+**Examples**
+
+The following example defines two function signatures (*@t4* and *@t5*):
+
+.. naclcode:
+
+  types {
+    count: 6;
+    @t0 = i32;
+    @t1 = i64;
+    @t2 = float;
+    @t3 = void;
+    @t4 = void (i32, float, i64);
+    @t5 = i32();
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 17, 2>
+  3: <1, 6>
+  3: <7, 32>
+  3: <7, 64>
+  3: <3>
+  3: <2>
+  3: <21, 3, 0, 2, 1>
+  3: <21, 0>
+  0: <65534>
+
+Globals block
+=============
+
+The globals block defines global addresses of variables and constants, used by
+the PNaCl program. It also defines the memory associated with the global
+addresses, and how to initialize each global variable/constant. It must appear
+in the module block. It must appear after the types block, as well as after all
+function address records. But, it must also appear before the valuesymtab block,
+and any function blocks.
+
+The globals block begins with a count record, defining how many global addresses
+are defined by the PNaCl program. It is then followed by a sequence of records
+that defines how each global address is initialized.
+
+The standard sequence, for defining global addresses, begins with a global
+address record.  It is then followed by a sequence of records defining how the
+global address is initialized.  If the initializer is simple, a single record is
+used. Otherwise, the initializer is preceded with a compound record, specifying
+a number *N*, followed by sequence of *N* simple initializer records.
+
+The size of the memory referenced by each global address is defined by its
+initializer records. All simple initializer records define a sequence of
+bytes. A compound initializer defines the sequence of bytes by concatenating the
+corresponding sequence of bytes for each of its simple initializer records.
+
+For notational convenience, PNaClAsm begins a compound record with a "{", and
+inserts a "}" after the last initializer record associated compound record. This
+latter "}" does not correspond to any record. It is implicitly assumed by the
+size specified in the compound record, and is added only to improve readability.
+
+Explicit alignment is specified for global addresses, and must be a power
+of 2. If the alignment is 0, the alignment of the global is set by the target to
+whatever it feels convenient. If the value is greater than zero, the global is
+forced to have exactly that alignment.
+
+For example, consider the following:
+
+.. naclcode::
+
+  globals {
+    count: 2;
+    const @g0 =
+      zerofill 8;
+    var @g1 =
+      initializers 2 {
+        {1, 2, 3, 4},
+        zerofill 2;
+      }
+  }
+
+
+TODO: Generate a pnacl-dis output to show relationship?
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 19, 2>
+  3: <5, 2>
+  3: <0, 0, 1>
+  3: <2, 8>
+  3: <0, 0, 0>
+  3: <1, 2>
+  3: <3, 1, 2, 3, 4>
+  3: <2, 2>
+  0: <65534>
+
+Count Record
+------------
+
+The count record defines the number of global addresses used by the PNaCl
+program.
+
+**Syntax**
+
+.. naclcode::
+
+  count: N;                                       <A>
+
+**Record**
+
+.. naclcode::
+
+   AA: <5, N>
+
+**Semantics**
+
+This record must appear first in the globals block.  The count record defines
+the number of global addresses used by the program. *A* is the (optional)
+abbreviation associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+
+**Updates**
+
+.. naclcode::
+
+  ExpectedGlobals = N;
+  ExpectedInitializers = 0;
+
+Global Variable Addressses
+--------------------------
+
+A global variable address record defines a global address to global data.  The
+global variable address record must be immediately followed by initializer
+record(s) that define how the corresponding global variable is initialized.
+
+**Syntax**
+
+.. naclcode::
+
+  var @gN, align V =                              <A>
+  var @gN =                                       <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <0, VV, 0>
+
+**Semantics**
+
+A global variable address record defines a global address for a global variable.
+*V* is the alignment to for the global variable.  The alignment *V* clause can
+be omitted if *V* is zero. *A* is the (optional) abbreviation associated with
+the record.
+
+It is assumed that the memory, referenced by the global variable address, can be
+both read and written to.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  N = NumGlobalAddresses
+  NumGlobalAddresses < ExpectedGlobals
+  ExpectedInitializers = 0
+  VV = Log2(V+1)
+
+**Updates**
+
+.. naclcode::
+
+  ++NumGlobalAddresses;
+  ExpectedInitializers = 1;
+  TypeOf(@gN) = i32;
+
+**Examples**
+
+.. naclcode::
+
+   var @g0 =
+     zerofill 8;
+   var @g1 =
+     {1, 2, 3, 4}
+
+This example defines two global variable addresses, *@g0* and *@g1*. Both use
+memory alignment of 0. *@g0* is an 8 byte variable initialized to zero.  *@g1*
+is a 4 byte variable, initialized by the sequence of bytes 1, 2, 3, and 4.
+
+The corresponding records defined by the example above are:
+
+.. naclcode::
+
+  3: <0, 0, 0>
+  3: <2, 8>
+  3: <0, 0, 0>
+  3: <3, 1, 2, 3, 4>
+
+Global Constant Addresses
+-------------------------
+
+A global constant address record defines an address corresponding to a global
+constant that can't be modified by the program. The global constant address
+record must be immediately followed by initializer record(s) that define how
+the corresponding global constant is initialized.
+
+**Syntax**
+
+.. naclcode::
+
+  const @gN, align V =                            <A>
+  const @gN =                                     <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <0, VV, 1>
+
+**Semantics**
+
+A global constant address record defines a global address for a global constant.
+*V* is the memory alignment for the global constant. *VV* is the corresponding
+number of bits associated with alignment *V* (see *constraints*).  The alignment
+*V* caluse can be omitted if *V* is zero. *A* is the (optional) abbreviation

[Jim Stichnoth, 2014/06/06 18:24:48]

clause

[Karl, 2014/06/30 22:09:03]

Done.

+associated with the record.
+
+It is assumed that the memory, referenced by the global constant
+address, is only read, and can't be written to.
+
+Note that the only difference between a global variable address and a global
+constant address record is the third element of the record. If the value is
+zero, it defines a global variable address. If the value is one, it defines a
+global constant address.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  N = NumGlobalAddresses
+  NumGlobalAddresses < ExpectedGlobals
+  ExpectedInitializers = 0
+  VV = Log2(V+1)
+
+**Updates**
+
+.. naclcode::
+
+  ++NumGlobalAddresses;
+  ExpectedInitializers = 1;
+  TypeOf(@gN) = i32;
+
+**Examples**
+
+.. naclcode::
+
+  const @g0 =
+    zerofill 8;
+  var @g1 =
+    {1, 2}
+
+This example defines two global constants, with global addresses *@g0* and
+*@g1*. *@g0* is an 8 byte constant initialized to zero.  *@g1* is a 2 byte
+variable, initialized by the sequence of bytes 1 and 2.
+
+The corresponding PNaCl bitcode records are:
+
+.. naclcode::
+
+  3: <0, 0, 1>
+  3: <2, 8>
+  3: <0, 0, 1>
+  3: <3, 1, 2>
+
+Zerofill Initializer
+--------------------
+
+The zerofill initializer record initializes a sequence of bytes, associated with
+a global address, with zeros.
+
+**Syntax**
+
+.. naclcode::
+
+  zerofill N;                                     <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, N>
+
+**Semantics**
+
+A zerofill initializer record intializes a sequence of bytes, associated with a
+global address, with zeros. *A* is the (optional) abbreviation of the associated
+record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  ExpectedInitializers > 0;
+
+**Updates**
+
+.. naclcode::
+
+  --ExpectedInitializers;
+
+**Examples**
+
+.. naclcode::
+
+  const @g0 =
+    zerofill 8;
+  var @g1 =
+    zerofill 4;
+
+This example defines two global constants, with global addresses *@g0* and
+*@g1*.  The global memory associated with address *@g0*, is an eight byte value,
+initialized to zero.  The global memory associated with address *@g1*, is a 4
+byte value, initialized to zero.
+
+The corresponding PNaCl records are:
+
+.. naclcode::
+
+  3: <0, 0, 1>
+  3: <2, 8>
+  3: <0, 0, 1>
+  3: <2, 4>
+
+Data Initializer
+----------------
+
+Data records define a sequence of bytes. These bytes define the initial value of
+the contents of the corresponding memory.
+
+**Syntax**
+
+.. naclcode::
+
+  { B1 , .... , BN }                              <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <3, B1, ..., BN>
+
+**Semantics**
+
+A data record defines a sequence of bytes *B1* through *BN*, that initialize *N*
+bytes of memory. *A* is the (optional) abbreviation associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  ExpectedInitializers > 0
+
+**Updates**
+
+.. naclcode::
+
+  --ExpectedInitializers;
+
+**Examples**
+
+.. naclcode::
+
+  const @g0 =
+    {1, 2, 97, 36, 44, 88, 44}
+  const @g1 =
+    initializers 3 {
+      {4, 5, 6, 7}
+      reloc @f1;
+      {99, 66, 22, 12}
+    }
+
+The corresponding PNaCl records are:
+
+.. naclcode::
+
+  3: <0, 0, 1>
+  3: <3, 1, 2, 97, 36, 44, 88, 44>
+  3: <0, 0, 1>
+  3: <1, 3>
+  3: <3, 4, 5, 6, 7>
+  3: <4, 1>
+  3: <3, 99, 66, 22, 12>
+
+Relocation Initializer
+----------------------
+
+A relocation initializer record allows one to define the initial value of a
+global address with the value of another global address (i.e. either function,
+variable, or constant). Since addresses are pointers, a relocation initializer
+record defines 4 bytes of memory.
+
+**Syntax**
+
+.. naclcode::
+
+  reloc V;                                        <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <4, VV>
+
+**Semantics**
+
+A relocation initializer record defines a 4-byte value containing the specified
+global address *V*. *A* is the (optional) abbreviation associated with the
+record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  VV = AbsoluteIndex(V);
+  ExpectedInitializers > 0
+
+**Updates**
+
+.. naclcode::
+
+  --ExpectedInitializers;
+
+**Examples**
+
+.. naclcode::
+
+  var @g0 =
+    initializers 3 {
+      reloc @f1;
+      reloc @g0;
+      reloc @g10;
+    }
+
+This example defines global address *@g0*. It defines 12 bytes of memory, and is
+initialized with three addresses *@f1*, *@g0*, and *@g10*. Note that all globals
+can be used in a relocation initialization record, even if it isn't defined yet.
+
+Assuming
+
+.. naclcode::
+
+  100 = AbsoluteIndex(@g0))
+
+The corresponding PNaCl bitcode records are:
+
+.. naclcode::
+
+  3: <0, 0, 0>
+  3: <1, 3>
+  3: <4, 1>
+  3: <4, 100>
+  3: <4, 110>
+
+Subfield Relocation Initializer
+-------------------------------
+
+A subfield relocation initializer record allows one to define the initial value
+of a global address with the value of another (non-function) global address
+(i.e. either variable or constant), plus a constant. Since addresses are
+pointers, a relocation initializer record defines 4 bytes of memory.
+
+**Syntax**
+
+.. naclcode::
+
+  reloc V + O;                                    <A>
+  reloc V - O;                                    <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <4, VV, OOO>
+
+**Semantics**
+
+A relocation initializer record defines a 4-byte value containing the specified
+global (non-function) address *V*, modified by the unsigned offset *O*. *OO* is
+the corresponding signed offset. In the first form, *OO == O*. In the second
+form, *OO == - O*.  *A* is the (optional) abbreviation associated with the
+record. *a* is the corresponding abbreviation index of *A*. When *A* is omitted,
+*a=3*.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  VV == AbsoluteIndex(V)
+  ExpectedInitializers > 0
+  OOO == SignRotate(OO)
+
+**Updates**
+
+.. naclcode::
+
+  --ExpectedInitializers;
+
+**Examples**
+
+.. naclcode::
+
+  var @g0 =
+    initializers 3 {
+      reloc @f1;
+      reloc @g0 + 4;
+      reloc @g10 - 3;
+    }
+
+This example defines global address *@g0*, and is initialized with three
+pointers, addresses *@f1*, *@g0+4*, and *@g10-3*. Note that all global addresses
+can be used in a relocation initialization record, even if it isn't defined
+yet. Validity of the reference can be verified, since a global address *@g10*
+must be smaller than the value specified in the globals count record.
+
+Assuming
+
+.. naclcode::
+
+  100 = AbsoluteIndex(@g0))
+
+The corresponding PNaCl bitcode records are:
+
+.. naclcode::
+
+  3: <0, 0, 0>
+  3: <1, 3>
+  3: <4, 1>
+  3: <4, 100, 8>
+  3: <4, 110, 7>
+
+Compound Initializer
+--------------------
+
+The compound initializer record must immediately follow a global
+variable/constant address record. It defines how many (non-compound) initializer
+records are used to define the initializer. The size of the corresponding memory
+is the sum of the bytes needed for each of the succeeding initializers.
+
+**Syntax**
+
+.. naclcode::
+
+  initializers N {                                <A>
+   ...
+  }
+
+**Record**
+
+.. naclcode::
+
+  AA: <1, N>
+
+**Semantics**
+
+Defines that the next *N* initializers should be associated with the global
+address of the previous record. *A* is the (optional) abbreviation index
+associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  ExpectedInitializers == 1
+
+**Updates**
+
+.. naclcode::
+
+  ExpectedInitializers = N;
+
+**Examples**
+
+.. naclcode::
+
+  const @g1 =
+    initializers 3 {
+      {4, 5, 6, 7}
+      reloc @f1;
+      {99, 66, 22, 12}
+    }
+
+The corresponding PNaCl records are:
+
+.. naclcode::
+
+  3: <0, 0, 1>
+  3: <1, 3>
+  3: <3, 4, 5, 6, 7>
+  3: <4, 1>
+  3: <3, 99, 66, 22, 12>
+
+Valuesymtab Block
+=================
+
+TODO(kschimpf)
+
+
+The *valuesymtab block* [ref] does not define any values. Rather, its only goal
+is to associate text names with previously defined global addresses
+(i.e. function, constant, and variable).  Each association is defined by a
+record in the valuesymtab block. Currently, only *intrinsic* [ref] function
+addresses need a name. All other entries in this block are considered as a hint
+for debugging. The PNaCl translator may (or may not) pass these names to the
+running executable, allowing the (runtime) debugger to associate names with
+addresses.
+
+
+Module Block
+============
+
+The module block, like all blocks, is enclosed in a pair of enter/exit records,
+using block ID 8. A well-formed module block consists of the following records
+(in order):
+
+A version record
+   The version record communicates which version of the PNaCl bitcode
+   reader/writer should be used. Note that this is different than the PNaCl
+   bitcode (ABI) version. The PNaCl bitcode (ABI) version defines what is
+   expected in records, and is defined in the header record of the bitcode
+   file. The version record defines the version of the PNaCL bitcode

[Jim Stichnoth, 2014/06/06 18:24:48]

PNaCL --> PNaCl

[Jim Stichnoth, 2014/06/06 18:24:48]

PNaCL --> PNaCl

[Karl, 2014/06/30 22:09:03]

Done.

+   reader/writer to use to convert records into bit sequences.
+
+Optional local abbreviations
+   Defines a list of local abbreviations to use for records within the module
+   block.
+
+An abbreviations block
+   The abbreviations block defines user-defined, global abbreviations that are
+   used to convert PNaCl records to bit sequences in blocks following the
+   abbreviations block.
+
+A types block
+   The types block defines the set of all types used in the program.
+
+A non-empty sequence of function address records
+   Each record defines a function address used by the program. Function
+   addresses must either be external, or defined internally by the program. If
+   they are defined by the program, there must be a function block (appearing
+   later in the module) that defines the sequence of instructions for each
+   defined function.
+
+A globals block defining the global variables.
+   This block defines the set of global variable (addresses) used by the
+   program. In addition to the addresses, each global variable also defines how
+   the corresponding global variable is initialized.
+
+An optional value symbol table block.
+   This block, if defined, provides textual names for function and global
+   variable addresses (previously defined in the module). Note that only names
+   for intrinsic functions must be provided [ref]. Any additional names are
+   hints that may (or may not) be used by the PNaCl translator, and be available
+   for debugging when executed.
+
+A sequence of function blocks.
+   Each function block defines the corresponding control flow graph for each
+   defined function. The order of function blocks is used to associate them with
+   function addresses.  The order of the defined function blocks must follow the
+   same order as the corresponding function addresses defined in the module
+   block.
+
+Descriptions of the abbreviations [ref], types [ref], global variables [ref],
+value symbol table [ref], and function [ref] blocks are not provided here. See
+the appropriate reference for more details. The following subsections describe
+each of the records that can appear in a module block.
+
+Version
+-------
+
+The version record defines the implementation of the PNaCl reader/writer to
+use. That is, the implementation that converts PNaCl records to bit
+sequences. Note that this is different than the PNaCl version of the bitcode
+file (encoded in the header record of the bitcode file).  The PNaCl version
+defines the valid forms of PNaCl records. The version record is specific to the
+PNaCl version, and may have different values for different PNaCl versions.
+
+Note that currently, only PNaCl bitcode version 2, and version record value 1 is
+defined.
+
+**Syntax**
+
+.. naclcode::
+
+  version N;                                  <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <1, N>
+
+**Semantics**
+
+The version record defines which PNaCl reader/writer rules should be
+followed. *N* is the version number. Currently *N* must be 1. Future versions of
+PNaCl may define additional legal values. *A* is the (optional) abbreviation
+index associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+
+*Examples*
+
+.. naclcode::
+
+   version 1;
+
+The corresponding record is:
+
+.. naclcode::
+
+  3: <1, 1>
+
+Function Address
+----------------
+
+A function address record defines a function address. Defining a function
+address also implies a corresponding implementation. *Defined* function
+addresses define implementations while *declared* function addresses do not.
+
+The implementation of a *defined* function address is provided by a
+corresponding function block, appearing later in the module block. The
+association of defining function address with the corresponding function block
+is based on position.  The *Nth* defining function address record, in the module
+block, has its implementation in the *Nth* function block of that module block.
+
+**Syntax**
+
+.. naclcode::
+
+  PN LN T0 @fN ( T1 , ... , TM );                 <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <8, T, C, P, L>
+
+**Semantics**
+
+Defines the function address *@fN*. *PN* is the name that specifies
+the prototype value *P* associated with the function. A function
+address is defined only if *P==0*. Otherwise, it is only declared.
+The type of the function is defined by function type *@tT*. *L*
+is the linkage specification corresponding to name *LN*. *C* is the
+calling convention used by the function. *A* is the
+(optional) abbreviation associated with the record.
+
+Note that the function signature must be defined by a function type in the types
+block. Hence, the return value must either be a primitive type, type *void*, or
+a vector type.  Parameter types can be a primitive or vector type.  For the
+integral types, only i32 and i64 can be used for a return or parameter type. All
+other integer types are not allowed.
+
+Valid prototype names *PN*, and corresponding *P* values, are:
+
+= =======
+P PN
+= =======
+1 declare
+0 define
+= =======
+
+Valid linkage names *LN*, and corresponding *L* values, are:
+
+= ========
+L LN
+= ========
+3 internal
+0 external
+= ========
+
+Currently, only one calling convention *C* is supported:
+
+= ====================
+C Calling Convention
+= ====================
+0 C calling convention
+= ====================
+
+**Constraint**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  T = TypeID(TypeOf(T0 ( T1 , ... , TN )))
+  N = NumFuncAddresses
+
+**Updates**
+
+.. naclcode::
+
+  ++NumFuncAddresses;
+  TypeOf(@fN) = TypeOf(TypeID(i32));
+  TypeOfFcn(@fN) = TypeOf(@tT);
+
+  if PN == 0:
+    DefiningFcnIDs += @FN;
+    ++NumDefinedFunctionAddresses;
+
+**Examples**
+
+.. naclcode::
+
+  module {
+    ...
+    types {
+      @t0 = void;
+      @t1 = i32;
+      @t3 = float;
+      @t4 = void (i32, float);
+      @t5 = i32 ();
+    }
+    ...
+    declare external void @f0(i32, float);
+    define internal i32 @f1();
+
+This defines function addresses *@f0* and *@f1*. Function address *@f0* is
+defined externally while *@f1* has an implementation (defined by a corresponding
+function block). The type signature of *@f0* is defined by type *@t4* while the
+type signature of *@f1* is *@t5*.
+
+The corresponding records for these two function addresses are:
+
+.. naclcode::
+
+  3: <8, 4, 0, 1, 0>
+  3: <8, 5, 0, 0, 1>
+
+Constants Blocks
+================
+
+TODO(kschimpf)
+
+Function Blocks
+===============
+
+A function block defines the implementation of a *defined* function address. The
+function address it defines is based on the position of the corresponding
+*defined* function address. The Nth *defined* function address always
+corresponds to the Nth function block in the module block.
+
+A function definition contains a list of basic blocks, forming the CFG (control
+flow graph). Each basic block contains a list of instructions, and ends with a
+*terminator* [ref] (e.g. branch) instruction.
+
+Basic blocks are not represented by records. Rather, context is implicit. The
+first basic block begins with the first instruction record in the function
+block.  Blocks boundaries are determined by *terminator* instructions. The
+instruction that follows a temrinator instruction begins a new basic block.

[Jim Stichnoth, 2014/06/06 18:24:48]

terminator

[Karl, 2014/06/30 22:09:03]

Done.

+
+The first basic block in a function is special in two ways: it is immediately
+executed on entrance to the function, and it is not allowed to have predecessor
+basic blocks (i.e. there can't be any branches to the entry block of a
+function). Because the entry block has no predecessors, it also can't have any
+*PHI instructions* [ref].
+
+The parameters are implied by the type of the corresponding function
+address. One parameter is defined for each argument of the function type
+signature.
+
+The number of basic blocks is defined by the count record. Each terminator
+instruction ends the current basic block, and the next instruction begins a new
+basic block.  Basic blocks are numbered by the order they appear (starting with
+index 0). Basic block IDs have the form *%bN*, where *N* corresponds to the
+position of the basic block within the function block.
+
+Each instruction, within a function block, corresponds to a corresponding PNaCl
+record.  The layout of a function block is the (basic block) count record,
+followed by a sequence of instruction records.
+
+For readability, PNaClAsm introduces block IDs. These block IDs do not
+correspond to PNaCl records, since basic block boundaries are defined
+implicitly, after terminator instructions. They appear only for readability.
+
+Operands are typically defined using an *absolute index* [ref]. This absolute
+index implicitly encodes function addresses, global addresses, parameters,
+constants, and instructions that generate values. The encoding takes advantage
+of the implied ordering of these values in the bitcode file, defining a block of
+indices for each kind of identifier.  That is, Indices are ordered by putting

[Jim Stichnoth, 2014/06/06 18:24:47]

Indices --> indices

[Karl, 2014/06/30 22:09:04]

Done.

+function identifier indices first, followed by global address identifiers,
+followed by parameter identifiers, followed by constant identifiers, and lastly
+instruction value identifiers.
+
+Most operands of instructions are encoded using a relative index value, rather
+than absolute. The is done because most instruction operands refer to values

[Jim Stichnoth, 2014/06/06 18:24:49]

The is done --> This is done

[Karl, 2014/06/30 22:09:04]

Done.

+defined earlier in the (same) basic block.  As a result, the relative distance
+(back) from the next value defining instruction is frequently a small
+number. Small numbers tend to require fewer bits when they are converted to bit
+sequences.
+
+The following subsections define records that can appear in a function block.
+
+Function enter
+--------------
+
+PNaClAsm defines a function enter block construct. The corresponding record is
+simply an enter block record, with BlockID value 12. All context about the
+defining address is implicit by the position of the function block, and the
+corresponding defining function address. To improve readability, PNaClAsm
+includes the function signature into the syntax rule.
+
+**Syntax**
+
+.. naclcode::
+
+  function TR @fN ( T0 %p0, ... , TM %pM) {             <B>
+
+**Record**
+
+  1: <65535, 12, B>
+
+**Semantics**
+
+*B* is the number of bits reserved for abbreviations in the block. See
+enter block records [ref] for more details.
+
+The value of *N* corresponds to the positional index of the corresponding
+defining function address this block is associated with. *M* is the number of
+defined parameters (minus one) in the function heading.
+
+**Constraints**
+
+.. naclcode::
+
+  N == NumFcnImpls
+  @fN in DefiningFcnIDs
+  TypeOfFcn(@fN) == TypeOf(TypeID(TR (T0, ... , TM)))
+
+**Updates**
+
+.. naclcode::
+
+  ++NumFcnImpls;
+  EnclosingFcnID = @fN;
+  NumBasicBlocks = 0;
+  ExpectedBlocks = 0;
+  NumParams = M;
+  for I in [0..M]:
+    TypeOf(%pI) = TypeOf(TypeID(TI));
+
+**Examples**
+
+.. naclcode::
+
+  types {
+    ...
+    @t10 = void (i32, float);
+    ...
+  }
+  ...
+  define internal void @f12(i32, float);
+  ...
+  function void @f12(i32 %p0, float %p1) {
+  ...
+  }
+
+defines the enter block record:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+
+Count Record
+------------
+
+The count record, within a function block, defines the number of basic blocks
+used to define the function implementation. It should be the first record in the
+function block.
+
+**Syntax**
+
+.. naclcode::
+
+    blocks: N;                                    <A>
+  %b0:
+
+**Record**
+
+.. naclcode::
+
+  AA: <1, N>
+
+**Semantics**
+
+The count record defines the number *N* of basic blocks in the implemented
+function. *A* is the (optional) abbreviation associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  ExpectedBasicBlocks = 0
+  NumBasicBlocks = 0
+
+**Updates**
+
+.. naclcode::
+
+  ExpectedBlocks = N;
+
+**Examples**
+
+.. naclcode::
+
+  blocks: 5
+
+The corresponding PNaCl bitcode record is:
+
+.. naclcode::
+
+  3: <1, 5>
+
+Terminator Instructions
+-----------------------
+
+Terminator instructions are instructions that appear in a function block, and
+define the end of the current basic block. A terminator instruction indicates
+which block should be executed after the current block is finished. The function
+block is well formed only if the number of terminator instructions, in the
+function block, corresponds to the value defined by the corresponding count
+block.
+
+Return Void Instruction
+^^^^^^^^^^^^^^^^^^^^^^^
+
+The return void instruction is used to return control from a function back to
+the caller, without returning any value.
+
+**Syntax**
+
+.. naclcode::
+
+    ret;                                          <A>
+  %bB:
+
+**Record**
+
+.. naclcode::
+
+   AA: <10>
+
+**Semantics**
+
+The return instruction returns control to the calling function.
+
+*B* is the number associated with the next basic block. Label *%bB:* only
+appears if *B < ExpectedBasicBlocks*. That is, the label is omitted only if this
+terminator instruction is the last instruction in the function block.  *A* is
+the (optional) abbreviation index associated with the record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  B == NumBasicBlocks + 1
+  NumBasicBlocks < ExpectedBasicBLocks
+  ReturnType(TypeOf(EnclosingFcnID)) == void
+
+**Updates**
+
+.. naclcode::
+
+  ++NumBasicBlocks;
+
+**Examples**
+
+The following shows the implementation of a function that simply returns.
+
+.. naclcode::
+
+  function void @f5() {
+    blocks: 1;
+  %b0:
+    ret;
+  }
+
+The corresponding PNaCl records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <10>
+  0: <65534>
+
+Return Value Instruction
+^^^^^^^^^^^^^^^^^^^^^^^^
+
+The return value instruction is used to return control from a function back to
+the caller, including a value. The value must correspond to the return type of
+the enclosing function.
+
+**Syntax**
+
+.. naclcode::
+
+    ret T V;                                      <A>
+  %bB:
+
+**Record**
+
+.. naclcode::
+
+   AA: <10, VV>
+
+**Semantics**
+
+The return value instruction returns control to the calling function, returning
+the provided value.
+
+*V* is the value to return. Type *T* must be of the type returned by the
+function.  It must also be the type associated with value *V*.  *A* is the
+(optional) abbreviation index associated with the record.
+
+*B* is the number associated with the next basic block.  Label *%bB:* only
+appears if *B < ExpectedBasicBlocks*. That is, the label is omitted only if this
+terminator instruction is the last instruction in the function block.
+
+The return type *T* must either be a primitive type, or a vector type. If the
+return type is an integral type, it must be either i32 or i64.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  VV = RelativeIndex(V)
+  B = NumBasicBlocks + 1
+  NumBasicBlocks < ExpectedBasicBlocks
+  T = TypeOf(V) = ReturnType(TypeOf(EnclosingFcnID))
+
+**Updates**
+
+.. naclcode::
+
+  ++NumBasicBlocks;
+
+**Examples**
+
+The following shows a return statement that returns the value generated by the
+previous instruction:
+
+.. naclcode::
+
+  function i32 @f5(i32 %p0) {
+    blocks: 1;
+  @b0:
+    ret i32 @p0;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <10, 1>
+  0: <65534>
+
+Unconditional Branch Instruction
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The unconditional branch instruction is used to cause control flow to transfer
+to a different basic block of the function.
+
+**Syntax**
+
+.. naclcode::
+
+    br %bN;                                       <A>
+  %bB:
+
+**Record**
+
+.. naclcode::
+
+  AA: <11, N>
+
+**Semantics**
+
+The unconditional branch instruction causes control flow to transfer to basic
+block *N*.  *A* is the (optional) abbreviation index associated with the record.
+
+*B* is the number associated with the next basic block. Label *%bB:* only
+appears if *B < ExpectedBasicBlocks*. That is, the label is omitted only if this
+terminator instruction is the last instruction in the function block.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  0 < N
+  N < ExpectedBasicBlocks
+  B = NumBasicBlocks + 1
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumBasicBlocks;
+
+**Examples**
+
+.. naclcode::
+
+    br %b2;
+
+This branch instruction branches to the 3rd basic block of the function. It
+defines the following PNaCl record:
+
+.. naclcode::
+
+  3: <11, 2>
+
+Conditional Branch Instruction
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The conditional branch instruction is used to cause control flow to transfer to
+a different basic block of the function, based on a boolean test condition.
+
+**Syntax**
+
+.. naclcode::
+
+    br i1 C, %bT, %bBF;                          <A>
+  %bB:
+
+**Record**
+
+.. naclcode::
+
+  AA: <11, T, F, V>
+
+**Semantics**
+
+Upon execution of a conditional branch instruction, the *i1* (boolean) argument
+*C* is evaluated. If the value is *true*, control flows to basic block
+*%bT*. Otherwise control flows to basic block *%bF*.  *A* is the (optional)
+abbreviation index associated with the record.
+
+*B* is the number associated with the next basic block. Label *%bB:* only
+appears if *B < ExpectedBasicBlocks*. That is, the label is omitted only if this
+terminator instruction is the last instruction in the function block.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  V = RelativeIndex(C)
+  0 < T
+  B1 < ExpectedBasicBlocks 
+  0 < F
+  B2 < ExpectedBasicBlocks
+  B = NumBasicBlocks + 1
+  NumBasicBlocks < ExpectedBasicBlocks
+  TypeOf(C) == i1
+
+**Updates**
+
+.. naclcode::
+
+  ++NumBasicBlocks;
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f2(i32 %p0, i32 %p1) {
+    blocks: 3;
+  %b0:
+    %v0 = cmp eq i32 %p0, %p1;
+    br i1 %v0, %b1, %b2;
+  %b1:
+    ret i32 %p0;
+  %b2:
+    ret i32 %p1;
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 3>
+  3: <28, 2, 1, 32>
+  3: <11, 2, 1, 1>
+  3: <10, 3>
+  3: <10, 2>
+  0: <65534>
+
+Unreachable
+^^^^^^^^^^^
+
+The unreachable instruction has no defined semantics. The instruction is used to
+inform the *PNaCl translator* that control can't reach this instruction.
+
+**Syntax**
+
+.. naclcode::
+
+    unreachable;                                  <A>
+  %bB:
+
+**Record**
+
+.. naclcode::
+
+  AA: <15>
+
+**Semantics**
+
+Directive to the *PNaCl translator* that this instruction is unreachable.  *A*
+is the (optional) abbreviation index associated with the record.
+
+*B* is the number associated with the next basic block. Label *%bB:* only
+appears if *B < ExpectedBasicBlocks*. That is, the label is omitted only if this
+terminator instruction is the last instruction in the function block.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  B = NumBasicBlocks + 1
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumBasicBlocks;
+
+**Examples**
+
+TODO(kschimpf)
+
+Switch Instruction
+^^^^^^^^^^^^^^^^^^
+
+TODO(kschimpf)
+
+Integer Binary Instructions
+-----------------------------
+
+Binary instructions are used to do most of the computation in a program. This
+section focusses on binary instructions that operator on integral values, or

[Jim Stichnoth, 2014/06/06 18:24:49]

focusses --> focuses

[jvoung (off chromium), 2014/06/06 20:09:15]

focuses

+vectors of integral values.
+
+All binary operations require two operands of the same type, execute an
+operation on them, and produce a value. The value may represent multiple values
+if the type is a vector type.  The result value always has the same type as its
+operands.
+
+Some integer binary operations can be applied to both signed and unsigned
+integers. Others, the sign is significant. In general, if the sign plays a role
+in the instruction, the sign information is encoded into the name of the
+instruction.
+
+For most binary operations (except some of the logical operations), integral
+type i1 is disallowed.
+
+Integer Add
+^^^^^^^^^^^
+
+The integer add instruction returns the sum of its two arguments. Both arguments
+and the result must be of the same type. That type must be integral, or an
+integral vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = add T V1, V2;                             <A>
+
+**Record**
+
+  AA: <2, VV1, VV2, 0>
+
+**Semantics**
+
+The integer add instruction returns the sum of its two arguments. Arguments *V1* and

[Jim Stichnoth, 2014/06/06 18:24:47]

80-col

[Karl, 2014/06/30 22:09:05]

Done.

+*V2*, and the result *%vN*, must be of type *T*. *T* must be an integral type,
+or an integral vector type.  *N* is defined by the record position, defining the
+corresponding value generated by the instruction.  *A* is the (optional)
+abbreviation associated with the corresponding record.
+
+Overflow conditions are ignored, and the result returned is the mathematical

[jvoung (off chromium), 2014/06/06 20:09:15]

"Overflow conditions are ignored, and ..."

Is "ignored" meant to refer to the LLVM nsw, nuw, overflow behavior attributes?
If so, I think you can omit the "ignored" part since nsw/nuw aren't even
mentioned anywhere.  Just go ahead and say overflow is supposed to be handled
via the modulo?

Similar for other instances?

[Karl, 2014/06/30 22:09:04]

Done.

+result modulo *exp(2,n)*, where *n* is the bitwidth of the integer result.
+
+Because integers are assumed to use a two's complement representation,
+this instruction is appropriate for both signed and unsigned integers.
+
+In the add instruction, Integral type i1 (and vectors on integral type i1) is

[Jim Stichnoth, 2014/06/06 18:24:49]

Integral --> integral

[Karl, 2014/06/30 22:09:05]

Done.

+disallowed.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  VV1 = RelativeIndex(V1)
+  VV2 = RelativeIndex(V2)
+  T = TypeOf(V1) = TypeOf(V2)
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  N = NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = add i32 %p0, %p1;
+    %v1 = add i32 %p0, %v0;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 0>
+  3: <2, 3, 1, 0>
+  3: <10, 1>
+  0: <65534>
+
+Integer Subtract
+^^^^^^^^^^^^^^^^
+
+The integer subtract instruction returns the difference of its two arguments.
+Both arguments and the result must be of the same type. That type must be
+integral, or an integral vector type.
+
+Note: Since there isn't a negate instruction, subtraction from constant zero
+should be used to negate values.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = sub T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 1>
+
+**Semantics**
+
+The integer subtract returns the difference of its two arguments. Arguments *V1*
+and *V2*, and the result *%vN* must be of type *T*. *T* must be an integral
+type, or an integral vector type. *N* is defined by the record position, defining

[Jim Stichnoth, 2014/06/06 18:24:49]

80-col

+the corresponding value generated by the instruction. *A* is the (optional)
+abbreviation ¯associated with the corresponding record.
+
+Underflow conditions are ignored, and the result returned is the mathematical
+result modulo *exp(2, n)*, where *n* is the integer bitwidth of the result.
+
+Because integers are assumed to use a two's complement representation,
+this instruction is appropriate for both signed and unsigned integers.
+
+In the subtract instruction, Integral type i1 is disallowed.

[Jim Stichnoth, 2014/06/06 18:24:48]

Integral --> integral

+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = sub i32 %p0, %p1;
+    %v1 = sub i32 %p0, %v0;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 1>
+  3: <2, 3, 1, 1>
+  3: <10, 1>
+  0: <65534>
+
+Integer Multiply
+^^^^^^^^^^^^^^^^
+
+The integer multiply instruction returns the product of its two arguments.  Both
+arguments and the result must be of the same type. That type must be integral,
+or an integral based vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  &vN = mul T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 2>
+
+**Semantics**
+
+The intebger multiply instruction returns the product of its two

[Jim Stichnoth, 2014/06/06 18:24:46]

integer

[Karl, 2014/06/30 22:09:05]

Done.

+arguments. Arguments *V1* and *V2*, and the result *%vN*, must be of type *T*.
+*T* must be an integral type, or an integral vector type. *N* is defined by the
+record position, defining the corresponding value generated by the
+instruction. *A* is the (optional) abbreviation associated with the
+corresponding record.
+
+Overflow conditions are ignored, and the result returned is the mathematical
+result modulo *exp(2, n)*, where *n* is the bitwidth of the result.
+
+Because integers are assumed to use a two's complement representation,
+this instruction is appropriate for both signed and unsigned integers.
+
+In the subtract instruction, Integral type i1 is disallowed.

[Jim Stichnoth, 2014/06/06 18:24:47]

Integral --> integral

[Karl, 2014/06/30 22:09:05]

Done.

+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = mul i32 %p0, %p1;
+    %v1 = mul i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 2>
+  3: <2, 1, 2, 2>
+  3: <10, 1>
+  0: <65534>
+
+Signed Integer Divide
+^^^^^^^^^^^^^^^^^^^^^
+
+The signed integer divide instruction returns the quotient of its two arguments.
+Both arguments and the result must be of the same type. That type must be
+integral, or an integral vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = sdiv T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 4>
+
+**Semantics**
+
+The divide instruction returns the quotient of its two arguments. Arguments *V1*
+and *V2*, and the result *%vN*, must be of type *T*. *T* must be a integral
+type, or an integral vector type. *N* is defined by the record position,
+defining the corresponding value generated by the instruction. *A* is the
+(optional) abbreviation associated with the corresponding record.
+
+Signed values are assumed.  Note that signed and unsigned integer division are
+distinct operations. For unsigned integer division use the unsigned integer
+divide instruction (udiv).
+
+In the signed integer divide instruction, integral type i1 is
+disallowed. Integer division by zero is guaranteed to trap. Overflow is also
+undefined.

[jvoung (off chromium), 2014/06/06 20:09:14]

Maybe keep the clarification that overflow happens when dividing the max
negative negative integer by -1?

I wonder if this is a bit of undefined behavior we could just make defined, but
at the cost of some performance -- similar to divide by zero. E.g., Java makes
the result stay as the max negative number.

[Karl, 2014/06/30 22:09:03]

While I agree we should consider tightening this, I don't know the cost.

+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = sdiv i32 %p0, %p1;
+    %v1 = sdiv i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 4>
+  3: <2, 1, 2, 4>
+  3: <10, 1>
+  0: <65534>
+
+Unsigned Integer Divide
+^^^^^^^^^^^^^^^^^^^^^^^
+
+The unsigned integer divide instruction returns the quotient of its two
+arguments. Both the arguments and the result must be of the same type. That type
+must be integral, or an integral vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = udiv T V1, V2;                            <a>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, A1, A2, 3>
+
+**Semantics**
+
+The unsigned integer divide instruction returns the quotient of its two
+arguments. Arguments *V1* and *V2*, and the result *%vN*, must be of type
+*T*. *T* must be an integral type, or an integral vector type.  *N* is defined
+by the record position, defining the corresponding value generated by the
+instruction. *A* is the (optional) abbreviation associated with the
+corresponding record.
+
+Unsigned integral values are assumed.  Note that signed and unsigned integer
+division are distinct operations. For signed integer division use the signed
+integer divide instruction (sdiv).
+
+In the unsigned integer divide instruction, Integral type i1 is

[Jim Stichnoth, 2014/06/06 18:24:46]

Integral --> integral

[Karl, 2014/06/30 22:09:05]

Done.

+disallowed. Division by zero is guaranteed to trap. Overflow is also undefined.

[jvoung (off chromium), 2014/06/06 20:09:14]

When would overflow happen, if these are unsigned? (for the signed case this
happens when you divide by -1)

[Karl, 2014/06/30 22:09:03]

Removing sentence.

+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = udiv i32 %p0, %p1;
+    %v1 = udiv i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 3>
+  3: <2, 1, 2, 3>
+  3: <10, 1>
+  0: <65534>
+
+Signed Integer Remainder
+^^^^^^^^^^^^^^^^^^^^^^^^
+
+The signed integer remainder instruction returns the remainder of the quotient
+of its two arguments. Both arguments and the result must be of the same
+type. That type must be integral, or an integral based vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = srem T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 6>
+
+**Semantics**
+
+The signed integer remainder instruction returns the remainder of the quotient
+of its two arguments. Arguments *V1* and *V2*, and the result *%vN*, must be of
+type *T*. *T* must be a integral type, or an integral vector type. *N* is
+defined by the record position, defining the corresponding value generated by
+the instruction. *A* is the (optional) abbreviation associated with the
+corresponding record.
+
+Signed values are assumed.  Note that signed and unsigned integer division are
+distinct operations. For unsigned integer division use the unsigned integer
+remainder instruction (urem).
+
+In the signed integer remainder instruction, Integral type i1 is disallowed.

[Jim Stichnoth, 2014/06/06 18:24:47]

Integral --> integral

+Division by zero is guaranteed to trap. Overflow is also undefined.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = srem i32 %p0, %p1;
+    %v1 = srem i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 6>
+  3: <2, 1, 2, 6>
+  3: <10, 1>
+  0: <65534>
+
+Unsigned Integer Remainder Instruction
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The unsigned integer remainder instruction returns the remainder of the quotient
+of its two arguments. Both the arguments and the result must be of the same
+type. The type must be integral, or an integral vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = urem T V1, V2;                            <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, A1, A2, 5>
+
+**Semantics**
+
+The unsigned integer remainder instruction returns the remainder of the quotient
+of its two arguments. Arguments *V1* and *V2*, and the result *%vN*, must be of
+type *T*. *T* must be an integral type, or an integral vector type.  *N* is
+defined by the record position, defining the corresponding value generated by
+the instruction. *A* is the (optional) abbreviation associated with the
+corresponding record.
+
+Unsigned values are assumed. Note that signed and unsigned integer division are
+distinct operations. For signed integer division use the remainder instruction
+(srem).
+
+In the unsigned integer remainder instruction, Integral type i1 is disallowed.

[Jim Stichnoth, 2014/06/06 18:24:46]

Integral --> integral

+Division by zero is guaranteed to trap. Overflow is also undefined.

[jvoung (off chromium), 2014/06/06 20:09:14]

similar, overflow?

[Karl, 2014/06/30 22:09:03]

Done.

+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = srem i32 %p0, %p1;
+    %v1 = srem i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 5>
+  3: <2, 1, 2, 5>
+  3: <10, 1>
+  0: <65534>
+
+Shift Left
+^^^^^^^^^^
+
+The (integer) shift left instruction returns the first operand, shifted to the
+left a specified number of bits with zero fill. The shifted value must be
+integral, or an integral vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = shl T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 7>
+
+**Semantics**
+
+This instruction performs a shift left operation. Argument *V1* and the result
+*%vN* must be of type *T*. *T* nust be an integral, or a vector of
+integrals. *V2* must be an integral type. *N* is defined by the record position,
+defining the corresponding value generated by the instruction.  *A* is the
+(optional) abbreviation associated with the corresponding record.
+
+*V2* is assumed to be unsigned.  The least significant bits of the result will
+be filled with zero bits after the shift. If *V2* is (statically or dynamically)
+is negative or equal to or larger than the number of bits in *V1*, the result is
+undefined. If the arguments are vectors, each vector element of *V1* is shifted
+by the corresponding shift amount in *V2*.
+
+In the shift left instruction, Integral type i1 is disallowed for either

[Jim Stichnoth, 2014/06/06 18:24:50]

Integral --> integral

+argument.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1)
+  IsInteger(TypeOf(V2))
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  UnderlyingType(TypeOf(V2)) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = shl i32 %p0, %p1;
+    %v1 = shl i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 7>
+  3: <2, 1, 2, 7>
+  3: <10, 1>
+  0: <65534>
+
+Logical Shift Right
+^^^^^^^^^^^^^^^^^^^
+ 
+The logical shift right instruction returns the first operand, shifted
+to the right a specified number of bits with zero fill.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = lshr T V1, V2;                            <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 8>
+
+**Semantics**
+
+This instruction performs a logical shift right operation. Arguments *V1* and
+the result *%vN* must be of type *T*. *T* nust be an integral, or a vector of
+integrals. *V2* must be an integral type. *N* is defined by the record position,
+defining the corresponding value generated by the instruction.  *A* is the
+(optional) abbreviation associated with the corresponding record.
+
+*V2* is assumed to be unsigned. The most significant bits of the result will be
+filled with zero bits after the shift. If *V2* is (statically or dynamically)
+negative or equal to or larger than the number of bits in *V1*, the result is
+undefined. If the arguments are vectors, each vector element of *V1* is shifted
+by the corresponding shift amount in *V2*.
+
+In the logical shift right instruction, Integral type i1 is disallowed for

[Jim Stichnoth, 2014/06/06 18:24:49]

Integral --> integral

+either argument.
+
+**Constraints**
+
+.. naclcode::
+
+  AA = AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1)
+  IsInteger(TypeOf(V2))
+  IsInteger(UnderlyingType(T))
+  UnderlyingType(T) != i1
+  UnderlyingType(TypeOf(V2)) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = lshr i32 %p0, %p1;
+    %v1 = lshr i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 8>
+  3: <2, 1, 2, 8>
+  3: <10, 1>
+  0: <65534>
+
+Arithmetic Shift Right
+^^^^^^^^^^^^^^^^^^^^^^
+ 
+The arithmetic shift right instruction returns the first operand,
+shifted to the right a specified number of bits with sign extension.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = ashr T V1, V2;                            <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VVA2, 9>
+
+**Semantics**
+
+This instruction performs an arithmetic shift right operation. Arguments *V1*
+and the result *%vN* must be of type *T*. *T* nust be an integral, or a vector
+of integrals. *V2* must be an integral type. *N* is defined by the record
+position, defining the corresponding value generated by the instruction.  *A* is
+the (optional) abbreviation associated with the corresponding record.
+
+*V2* is assumed to be unsigned. The most significant bits of the result will be
+filled with the sign bit of *V1*. If *V2* is (statically or dynamically)
+negative or equal to or larger than the number of bits in *V1*, the result is
+undefined. If the arguments are vectors, each vector element of *V1* is shifted
+by the corresponding shift amount in *V2*.
+
+In the arithmetic shift right instruction, integral type i1 is disallowed for
+either argument.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1)
+  IsInteger(TypeOf(V2))
+  UnderlyingType(T) != i1
+  UnderlyingType(TypeOf(V2)) != i1
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = ashr i32 %p0, %p1;
+    %v1 = ashr i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 9>
+  3: <2, 1, 2, 9>
+  3: <10, 1>
+  0: <65534>
+
+Logical And
+^^^^^^^^^^^
+
+The *and* instruction returns the bitwise logical and of its two operands.
+
+**Syntax**
+ 
+.. naclcode::
+
+  %vN = and T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 10>
+
+**Semantics**
+
+This instruction performs a bitwise logical and of its arguments.  Arguments
+*V1* and *V2*, and the result *%vN* must be of type *T*. *T* nust be an
+integral, or a vector of integrals. *N* is defined by the record position,
+defining the corresponding value generated by the instruction.  *A* is the
+(optional) abbreviation associated with the corresponding record.
+
+The truth table used for the *and* instruction is:
+
+===== ===== ======
+Arg 1 Arg 2 Result
+===== ===== ======
+0     0     0
+0     1     0
+1     0     0
+1     1     1
+===== ===== ======
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T)))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = and i32 %p0, %p1;
+    %v1 = and i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 10>
+  3: <2, 1, 2, 10>
+  3: <10, 1>
+  0: <65534>
+
+Logical Or
+^^^^^^^^^^
+ 
+The *or* instruction returns the bitwise logical inclusive or of its
+two operands.
+
+**Syntax**
+ 
+.. naclcode::
+
+  %vN = or T V1, V2;                              <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 11>
+
+**Semantics**
+
+This instruction performs a bitwise logical inclusive or of its arguments.
+Arguments *V1* and *V2*, and the result *%vN* must be of type *T*. *T* nust be
+an integral, or a vector of integrals. *N* is defined by the record position,
+defining the corresponding value generated by the instruction.  *A* is the
+(optional) abbreviation associated with the corresponding record.
+
+The truth table used for the *or* instruction is:
+
+===== ===== ======
+Arg 1 Arg 2 Result
+===== ===== ======
+0     0     0
+0     1     1
+1     0     1
+1     1     1
+===== ===== ======
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T)))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = or i32 %p0, %p1;
+    %v1 = or i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 11>
+  3: <2, 1, 2, 11>
+  3: <10, 1>
+  0: <65534>
+
+Logical Xor
+^^^^^^^^^^^
+ 
+The *xor* instruction returns the bitwise logical exclusive or of its
+two operands.
+
+**Syntax**
+ 
+.. naclcode::
+
+  %vN = xor T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 12>
+
+**Semantics**
+
+This instruction performs a bitwise logical exclusive or of its
+arguments.  Arguments *V1* and *V2*, and the result *%vN* must be of
+type *T*. *T* nust be an integral, or a vector of integrals. *N* is
+defined by the record position, defining the corresponding value
+generated by the instruction.  *A* is the (optional) abbreviation
+associated with the corresponding record.
+
+The truth table used for the *or* instruction is:
+
+===== ===== ======
+Arg 1 Arg 2 Result
+===== ===== ======
+0     0     0
+0     1     1
+1     0     1
+1     1     0
+===== ===== ======
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  A1 == RelativeIndex(V1)
+  A2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsInteger(UnderlyingType(T)))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function i32 @f0(i32 %p0, i32 %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = xor i32 %p0, %p1;
+    %v1 = xor i32 %v0, %p1;
+    ret i32 %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 12>
+  3: <2, 1, 2, 12>
+  3: <10, 1>
+  0: <65534>
+
+Floating Binary Instructions

[jvoung (off chromium), 2014/06/06 20:09:15]

Floating Point Binary?

[Karl, 2014/06/30 22:09:03]

Done.

+------------------------------
+
+Floating Binary instructions require two operands of the same type, execute an

[Jim Stichnoth, 2014/06/06 18:24:49]

Do you want binary capitalized?

[Karl, 2014/06/30 22:09:05]

Done.

+operation on them, and produce a value. The value may represent multiple values
+if the type is a vector type.  The result value always has the same type as its
+operands.
+
+Float Add
+^^^^^^^^^
+
+The float add instruction returns the sum of its two arguments. Both arguments
+and the result must be of the same type. That type must be floating, or a
+floating vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = add T V1, V2;                             <A>
+
+**Record**
+
+  AA: <2, VV1, VV2, 0>
+
+**Semantics**
+
+The float add instruction returns the sum of its two arguments. Arguments *V1*
+and *V2* and the result *%vN* must be of type *T*. *T* must be a floating type,
+or a floating vector type. *N* is defined by the record position, defining the
+corresponding value generated by the instruction.  *A* is the (optional)
+abbreviation associated with the corresponding record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsFloat(UnderlyingType(T))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function float @f0(float %p0, float %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = add float %p0, %p1;
+    %v1 = add float %p0, %v0;
+    ret float %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 0>
+  3: <2, 3, 1, 0>
+  3: <10, 1>
+  0: <65534>
+
+Float Subtract
+^^^^^^^^^^^^^^
+
+The floatsubtract instruction returns the difference of its two arguments. Both

[Jim Stichnoth, 2014/06/06 18:24:46]

float subtract

[Karl, 2014/06/30 22:09:05]

Done.

+arguments and the result must be of the same type. That type must be a floating,
+or an floating based vector type.

[Jim Stichnoth, 2014/06/06 18:24:48]

an floating --> a floating

[Karl, 2014/06/30 22:09:05]

Done.

+
+**Syntax**
+
+.. naclcode::
+
+  %vN = sub T V1, V2;                             <a>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 1>
+
+**Semantics**
+
+The float subtract instruction returns the difference of its two
+arguments. Arguments *V1* and *V2*, and the result *%vN* must be of type
+*T*. *T* must be an floating type, or a floating vector type. *N* is defined by

[Jim Stichnoth, 2014/06/06 18:24:49]

a floating

[Karl, 2014/06/30 22:09:05]

Done.

+the record position, defining the corresponding value generated by the
+instruction. *A* is the (optional) abbreviation ¯associated with the

[Jim Stichnoth, 2014/06/06 18:24:49]

You have an interesting unicode character between "abbreviation" and
"associated".

[Karl, 2014/06/30 22:09:05]

Done.

+corresponding record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsFloat(UnderlyingType(T))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function float @f0(float %p0, float %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = sub float %p0, %p1;
+    %v1 = sub float %p0, %v0;
+    ret float %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 1>
+  3: <2, 3, 1, 1>
+  3: <10, 1>
+  0: <65534>
+
+Float Multiply
+^^^^^^^^^^^^^^
+
+The float multiply instruction returns the product of its two arguments. Both
+arguments and the result must be of the same type. That type must be floating,
+or a floating based vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  &vN = mul T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 2>
+
+**Semantics**
+
+The multiply instruction returns the product of its two arguments. Arguments
+*V1* and *V2*, and the result *%vN* must be of type *T*.  *T* must be an
+floating type, or a floating vector type. *N* is defined by the record position,
+defining the corresponding value generated by the instruction. *A* is the
+(optional) abbreviation associated with the corresponding record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsFloat(UnderlyingType(T))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function float @f0(float %p0, float %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = mul float %p0, %p1;
+    %v1 = mul float %p0, %v0;
+    ret float %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 2>
+  3: <2, 3, 1, 2>
+  3: <10, 1>
+  0: <65534>
+
+Float Divide
+^^^^^^^^^^^^
+
+The float divide instruction returns the quotient of its two arguments. Both
+arguments and the result must be of the same type. That type must be a floating
+type, or a floating based vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = div T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, V1, V2, 4>
+
+**Semantics**
+
+The float divide instruction returns the quotient of its two
+arguments. Arguments *V1* and *V2*, and the result *%vN* must be of type
+*T*. *T* must be a floating type, or a floating vector type. *N* is defined by
+the record position, defining the corresponding value generated by the
+instruction. *A* is the (optional) abbreviation associated with the
+corresponding record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV22 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsFloat(UnderlyingType(T))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function double @f0(double %p0, double %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = div double %p0, %p1;
+    %v1 = div double %p0, %v0;
+    ret double %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 4>
+  3: <2, 3, 1, 4>
+  3: <10, 1>
+  0: <65534>
+
+Float Remainder
+^^^^^^^^^^^^^^^
+
+The float remainder instruction returns the remainder of the quotient of its two
+arguments. Both arguments and the result must be of the same type. That type
+must be a floating type, or a floating based vector type.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = rem T V1, V2;                             <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <2, VV1, VV2, 6>
+
+**Semantics**
+
+The float remainder instruction returns the remainder of the quotient of its two
+arguments. Arguments *V1* and *V2*, and the result *%vN* must be of type
+*T*. *T* must be a floating type, or a floating vector type. *N* is defined by
+the record position, defining the corresponding value generated by the
+instruction. *A* is the (optional) abbreviation associated with the
+corresponding record.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV1 == RelativeIndex(V1)
+  VV2 == RelativeIndex(V2)
+  T == TypeOf(V1) == TypeOf(V2)
+  IsFloat(UnderlyingType(T))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T
+
+**Examples**
+
+.. naclcode::
+
+  function double @f0(double %p0, double %p1) {
+    blocks: 1;
+  %b0:
+    %v0 = rem double %p0, %p1;
+    %v1 = rem double %p0, %v0;
+    ret double %v1;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <2, 2, 1, 6>
+  3: <2, 3, 1, 6>
+  3: <10, 1>
+  0: <65534>
+
+Memory creation and access Instructions

[Jim Stichnoth, 2014/06/06 18:24:47]

Do something more consistent with capitalization.

+---------------------------------------
+
+A key design point of SSA-based representation is how it represents
+memory. In PNaCl bitcode files, no memory locations are in SSA
+form. This makes things very simple.
+
+Alloca Instruction
+^^^^^^^^^^^^^^^^^^
+
+The *alloca* instruction allocates memory on the stack frame of the
+currently executing function. This memory is automatically released
+when the function returns to its caller.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = alloca i8, i32 S, align V;                <A>
+  %vN = alloca i8, i32 S;                         <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <19, SS, VV>
+
+**Semantics**
+
+The *alloca* instruction allocates memory on the stack frame of the currently
+executing function.  The resulting value is a pointer to the allocated memory
+(i.e. of type i32). *S* is the number of bytes that are allocated on the
+stack. *S* must be of integral type i32. *V* is the aligment of the generated

[Jim Stichnoth, 2014/06/06 18:24:47]

alignment

[Karl, 2014/06/30 22:09:05]

Done.

+stack address. *A* is the corresponding number of bits associated with the
+record.
+
+Alignment must be a power of 2. A value of 0 means that the address
+has the ABI alignment of the target. If alignment is not specified,
+zero is used. Alignment on the stack is guaranteed to be aligned to at least
+the boundary specified by the alignment.
+
+TODO(kschimpf) Other alignment issues?
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  VV == Log2(V+1)
+  SS == RelativeIndex(S)
+  i32 == TypeOf(S)
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = i32;
+
+**Examples**
+
+The following instructions allocates memory for a 32-bit integer and a

[Jim Stichnoth, 2014/06/06 18:24:48]

instructions allocate

+64-bit floating value:
+
+.. naclcode::
+
+  function void @f() {
+    blocks: 1;
+    constants {
+      i32:
+        %c0 = 4;  // == sizeof(i32)
+        %c1 = 8;  // == sizeof(double)
+    }
+  %b0:
+    %v0 = alloca i8, i32 %c0;
+    %v1 = alloca i8, i32 %c1;
+    ret;
+  }
+
+Assuming *TypeId(i32) == @t1*, the corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  1: <65535, 11, 2>
+  3: <1, 1>
+  3: <4, 8>
+  3: <4, 16>
+  0: <65534>
+  3: <19, 2, 0>
+  3: <19, 2, 0>
+  3: <10>
+  0: <65534>
+
+Load Instruction
+^^^^^^^^^^^^^^^^
+
+The *load* instruction is used to read from memory.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = load T* P, align V;                       <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <20, PP, VV, TT>
+
+**Semantics**
+
+The load instruction is used to read from memory. *P* is identifier of the

[Jim Stichnoth, 2014/06/06 18:24:48]

is the identifier

[Karl, 2014/06/30 22:09:03]

Done.

+memory address to read. The type of *P* must be an i32 integer.  *T* is the type
+of value to read. *V* is the alignment of the memory address.  *A* is the

[jvoung (off chromium), 2014/06/06 20:09:14]

Should we say more about alignment? What happens if the alignments don't match
what is in the table below?

[Karl, 2014/06/30 22:09:05]

Done.

+(optional) abbreviation associated with the record.
+
+Type *T* must be an integral or floating type. Both float and double types
+are allowed for floating types. All integral types except i1 is allowed.

[Jim Stichnoth, 2014/06/06 18:24:47]

are allowed

[Karl, 2014/06/30 22:09:03]

Done.

+
+Valid alignment *V* values are:
+
+=== =================
+*V* Types
+=== =================
+1   i8, i16, i32, i64
+4   float
+8   double
+=== =================
+
+**Constraints**
+
+  AA == AbbrevIndex(A)
+  i32 == TypeOf(P)
+  PP == RelativeIndex(P)
+  VV == Log2(V+1)
+  %tTT == TypeID(T)
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T;
+
+**Examples**
+
+The following instructions load an i32 integer and a 64-bit floating value:
+
+.. naclcode::
+
+  function void @f(i32 %p0) {
+    blocks: 1;
+  %b0:
+    %v0 = load i32* %p0, align 1;
+    %v1 = load double* %v0, align 8;
+    ret;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <20, 1, 1>
+  3: <20, 1, 4>
+  3: <10>
+  0: <65534>
+
+Store Instruction
+^^^^^^^^^^^^^^^^^
+
+The *store* instruction is used to write to memory.
+
+**Syntax**
+
+.. naclcode::
+
+  store T S, T* P, align V;                     <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <24, PP, SS, VV>
+
+**Semantics**
+
+The store instruction is used to write to memory. *P* is the identifier of the
+memory address to write to.  The type of *P* must be an i32 integer.  *T* is the
+type of value to store. *S* is the value to store, and must be of type *T*.  *V*
+is the alignment of the memory address.  *A* is the (optional) abbreviation
+index associated with the record.
+
+Type *T* must be an integral or floating type. Both float and double types
+are allowed for floating types. All integral types except i1 is allowed.

[Jim Stichnoth, 2014/06/06 18:24:46]

are allowed

[Karl, 2014/06/30 22:09:03]

Done.

+
+Valid alignment *V* values are:
+
+=== =================
+*V* Types
+=== =================
+1   i8, i16, i32, i64
+4   float
+8   double
+=== =================
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  i32 == TypeOf(P)
+  PP == RelativeIndex(P)
+  VV == Log2(V+1)
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Examples**
+
+The following instructions store an i32 integer and a 32-bit floating
+value.
+
+.. naclcode::
+
+  function void @f(i32 %p0, i32 %p1, i32 %p2, float %p3) {
+    blocks: 1;
+  %b0:
+    store i32 %p1, i32* %p2, align 1;
+    store float %p3, float* %p3, align 4;
+    ret;
+  }
+
+The corresponding records are:
+
+.. naclcode::
+
+  1: <65535, 12, 2>
+  3: <1, 1>
+  3: <24, 4, 3, 1>
+  3: <24, 1, 2, 4>
+  3: <10>
+  0: <65534>
+
+Conversion Instructions
+-----------------------
+
+Conversion instructions all take a single operand and a type. The
+value is converted to the corresponding type.
+
+Integer truncating Instruction

[Jim Stichnoth, 2014/06/06 18:24:48]

capitalization?

[Karl, 2014/06/30 22:09:06]

Done.

+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The integer truncating instruction takes a value to truncate, and a type
+defining the truncated type. Both types must be integer types, or integral
+vectors of the same size. The bit size of the value must be larger than the bit
+size of the destination type. Equal sized types are not allowed.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = trunc T1 V to T2;                         <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <3, VV, TT2, 0>
+
+**Semantics**
+
+The integer truncating instruction takes a value *V*, and truncates to type
+*T2*. *A* is the (optional) abbreviation associated with the corresponding
+record. Both *T1* and *T2* must be integer types, or integral vectors of the

[jvoung (off chromium), 2014/06/06 20:09:14]

same number of elements instead of same "size" ?

T1 has to be wider than T2 (no nops or expansions)

If the value doesn't fit in T2, then the higher order bits dropped (vs fptrunc
which says it's undefined behavior if value cannot be represented precisely as a
less precise float)

[Karl, 2014/06/30 22:09:04]

This was implied by the constratiants, but I agree it is worth mentioning
verbally also.

+same size.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  TypeOf(V) = T1

[jvoung (off chromium), 2014/06/06 20:09:15]

Earlier you use == for these TypeOf constraints, but here and below you use =.
This is not meant to be an update like in the Updates section?

[Karl, 2014/06/30 22:09:05]

You are right. I am inconsistent with this. Fixing...

+  *VV* == RelativeIndex(*V*)
+  %tTT2 = TypeID(T2)
+  BitSizeOf(UnderlyingType(T1)) > BitSizeOf(UnderlyingType(T2))
+  UnderlyingCount(T1) == UnderlyingCount(T2)
+  IsInteger(UnderlyingType(T1))
+  IsInteger(UnderlyingType(T2))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T2;
+
+**Examples**
+
+.. naclcode::
+
+  %v10 = trunc i32 %v9 to i8;
+
+Assuming
+
+.. naclcode::
+
+  @t2 = i8;
+
+the corresponding record is:
+
+.. naclcode::
+
+  <3, 1, 2, 0>
+
+Floating truncating Instruction

[Jim Stichnoth, 2014/06/06 18:24:49]

capitalization?

+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The floating truncating instruction takes a value to truncate, and a type
+defining the truncated type. Both types must be floating types, or floating
+vectors of the same size. The bit size of the value must be larger than the bit
+size of the destination type. Equal sized types are not allowed.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = fptrunc T1 V to T2;                       <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <3, VV, TT2, 7>
+
+**Semantics**
+
+The floating truncating instruction takes a value *V*, and truncates to type
+*T2*. *A* is the (optional) abbreviation associated with the corresponding
+record. Both *T1* and *T2* must be integer types, or integral vectors of the

[jvoung (off chromium), 2014/06/06 20:09:14]

floating point types / vectors (seems copy pasted from trunc)

T1 has to be wider than T2 (so that it's a truncation).

[Karl, 2014/06/30 22:09:04]

Done.

+same size.
+
+If the value can't fit within the destination type *T2*, the results are
+undefined.
+
+**Constraints**
+
+.. naclcode::
+
+  TypeOf(V) = T1
+  double == UnderlyingType(T1)
+  float == UnderlyingType(T2)
+  *VV* == RelativeIndex(*V*)
+  %tTT2 = TypeID(T2)
+  BitSizeOf(UnderlyingType(T1)) > BitSizeOf(UnderlyingType(T2))
+  UnderlyingCount(T1) == UnderlyingCount(T2)
+  IsFloat(UnderlyingType(T1))
+  IsFloat(UnderlyingType(T2))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T2;
+
+**Examples**
+
+.. naclcode::
+
+  %v10 = fptrunc double %v9 to float;
+
+Assuming
+
+.. naclcode::
+
+  @t4 = float;
+
+the corresponding record is:
+
+.. naclcode::
+
+  <3, 1, 4, 7>
+
+Zero Extending Instruction
+^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The zero extending instruction takes an value to cast, and a type to extend it

[Jim Stichnoth, 2014/06/06 18:24:47]

a value

+to. Both types must be integer types, or integral vectors of the same size. The
+bit size of the value must be smaller than the bitsize of the destination

[Jim Stichnoth, 2014/06/06 18:24:47]

bitsize --> bit size

[Karl, 2014/06/30 22:09:05]

Done.

+type. Equal sized types are not allowed.
+
+**Syntax**
+
+.. naclcode::
+
+  %vN = zext T1 V to T2;                          <A>
+
+**Record**
+
+.. naclcode::
+
+  AA: <3, VV, TT2, 1>
+
+
+**Semantics**
+
+The zero extending instruction takes a value *V*, and expands it to type
+*T2*. *I* is the (optional) abbreviation associated with the corresponding
+record.  Both *T1* and *T2* must be integer types, or vectors of the same number
+of integers.
+
+The instruction fills the high order bits of the value with zero bits
+until it reaches the size of the destination type. When zero extending
+from i1, the result will always be either 0 or 1.
+
+**Constraints**
+
+.. naclcode::
+
+  AA == AbbrevIndex(A)
+  TypeOf(V) = T1
+  *VV* == RelativeIndex(*V*)
+  %tTT2 = TypeID(T2)
+  BitSizeOf(UnderlyingType(T1)) < BitSizeOf(UnderlyingType(T2))
+  UnderlyingCount(T1) == UnderlyingCount(T2)
+  IsInteger(UnderlyingType(T1))
+  IsInteger(UnderlyingType(T2))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T2;
+
+**Examples**
+
+.. naclcode::
+
+  %v12 = zext i8 %v11 to i32;
+
+Assuming
+
+.. naclcode::
+
+  @t0 = i32;
+
+the corresponding record is:
+
+.. naclcode::
+
+  <3, 1, 0, 2>
+
+Sign Extending Instruction
+^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The sign extending instruction takes an value to cast, and a type to

[Jim Stichnoth, 2014/06/06 18:24:47]

a value

[Karl, 2014/06/30 22:09:04]

Done.

+extend it to. Both types must be integer types, or vectors of the same
+number of integers. The bit size of the value must be smaller than the
+bitsize of the destination type. Equal sized types are not allowed.

[Jim Stichnoth, 2014/06/06 18:24:47]

bit size

[Karl, 2014/06/30 22:09:04]

Done.

+
+**Syntax**
+
+.. naclcode::
+
+  %vN = sext T1 V to T2;                          <I>
+
+**Record**
+
+.. naclcode::
+
+  I: <3, VV, TT2, 2>
+
+
+**Semantics**
+
+The sign extending instruction takes a value *V*, and expands it to
+type *T2*. *VV* is the relative index of *V*. *I* is the (optional)
+abbreviation associated with the corresponding record. Both *T1* and
+*T2* must be integer types, or vectors of the same number of integers.
+
+When sign extending, the instruction fills the high order bits of the
+value with the (current) high order bit of the value. When sign
+extending from i1, the extension always results in -1 or 0.
+
+**Constraints**
+
+.. naclcode::
+
+  TypeOf(V) = T1
+  *VV* == RelativeIndex(*V*)
+  %tTT2 = TypeID(T2)
+  BitSizeOf(UnderlyingType(T1)) < BitSizeOf(UnderlyingType(T2))
+  UnderlyingCount(T1) == UnderlyingCount(T2)
+  IsInteger(UnderlyingType(T1))
+  IsInteger(UnderlyingType(T2))
+  N == NumValuedInsts
+  NumBasicBlocks < ExpectedBasicBlocks
+
+**Updates**
+
+.. naclcode::
+
+  ++NumValuedInsts;
+  TypeOf(%vN) = T2;
+
+**Examples**
+
+.. naclcode::
+
+  %v12 = sext i8 %v11 to i32;
+
+Assuming
+
+.. naclcode::
+
+  @t0 = i32;
+
+the corresponding record is:
+
+.. naclcode::
+
+  <3, 1, 0, 2>
+
+fpext
+^^^^^
+
+TODO(kschimpf)
+
+fptoui
+^^^^^^
+
+TODO(kschimpf)
+
+fptosi
+^^^^^^
+
+TODO(kschimpf)
+
+sitofp
+^^^^^^
+
+TODO(kschimpf)
+
+bitcast
+^^^^^^^
+
+TODO(kschimpf)
+
+Comparison Instructions
+-----------------------
+
+TODO(kschimpf): cmp
+
+Other Instructions
+------------------
+
+TODO(kschimpf)
+
+Forward type declarations
+^^^^^^^^^^^^^^^^^^^^^^^^^
+
+TODO(kschimpf)
+
+Phi Instruction
+^^^^^^^^^^^^^^^
+
+TODO(kschimpf)
+
+
+Select Instruction
+^^^^^^^^^^^^^^^^^^
+
+TODO(kschimpf)
+
+Call Instructions
+^^^^^^^^^^^^^^^^^
+
+TODO(kschimpf)
+
+Intrinsic Functions
+-------------------
+
+TODO(kschimpf)
+
+Support Functions
+=================
+
+Defines functions used to convert syntactic representation to corresponding
+records.
+
+SignRotate
+----------
+
+The SignRotate function encodes a signed integer in an easily compressable

[Jim Stichnoth, 2014/06/06 18:24:48]

compressible

[Karl, 2014/06/30 22:09:04]

Done.

+form. This is done by rotating the sign bit to the rightmost bit, rather than
+the leftmost bit. By doing this rotation, both small positive and negative
+integers are small (unsigned) integers. Therefore, all small integers can be
+encoded as a small (unsigned) integers.
+
+The definition of SignRotate(N) is:
+
+======== ============= =========
+Argument Value         Condition
+======== ============= =========
+N        abs(N)<<1     N >= 0
+N        abs(N)<<1 + 1 N < 0
+======== ============= =========
+
+AbsoluteIndex
+-------------
+
+Bitcode ID's of the forms *@fN*, *@gN*, *%pN*, *%cN*, and *%vN*, are combined
+into a single index space. This can be done because of the ordering imposed by
+PNaClAsm. All function address bitcode IDs must be defined before any of the
+other forms of bitcode IDs. All global address bitcode IDs must be defined
+before any local bitcode IDs. Within a function block, the parameter bitcode IDs
+must be defined before constant IDs, and constant IDs must be defined before
+instruction value IDs.
+
+Hence, within a function block, it is safe to refer to all of these
+bitcode IDs using a single *absolute* index. The absolute index for
+each kind of bitcode ID is computed as follows:
+
+========== ==========================================================================
+Bitcode ID AbsoluteIndex
+========== ==========================================================================
+@fN        N
+@gN        N + NumDefinedFcnAddresses
+@pN        N + NumDefinedFcnAddresses + NumGlobalAddresses
+@cN        N + NumDefinedFcnAddresses + NumGlobalAddresses + NumParams
+@vN        N + NumDefinedFcnAddresses + NumGlobalAddresses + NumParams + NumFcnConsts
+========== ==========================================================================
+
+RelativeIndex
+-------------
+
+Relative indices are used to refer to values within instructions of a
+function.  The relative index of an ID is always defined in terms of
+the index associated with the next value generating instruction. It is
+defined as follows:
+
+.. naclcode::
+
+   RelativeIndex(J) = AbsoluteIndex(NumValuedInsts) - AbsoluteIndex(J)
+
+AbbrevIndex
+-----------
+
+This function converts user-defined abbreviation indices to the corresponding
+internal abbreviation index saved in the bitcode file. It adds 4 to its argument,

[Jim Stichnoth, 2014/06/06 18:24:47]

80-col

[Karl, 2014/06/30 22:09:03]

Done.

+since there are 4 predefined internal abbreviation indices (0, 1, 2, and 3).
+
+========= ==============
+N         AbbrevIndex(N)
+========= ==============
+undefined 3
+%aA       A + 4
+@aA       A + 4
+========= ==============
+
+Log2
+----
+
+This is the 32-bit log2 value of its argument.
+
+exp
+---
+
+.. naclcode::
+
+  exp(n, m)
+
+Denotes the *m* power of *n*.
+
+BitSizeOf
+---------
+
+Returns the number of bits needed to represent its argument (a type).
+
+UnderlyingType
+--------------
+
+Returns the primitive type of the type construct. For primitive types,
+the *UnderlyingType* is itself. For vector types, the base type of the
+vector is the underlying type.

[Jim Stichnoth, 2014/06/06 18:24:47]

What if the type is a vector of vectors?  (or is that even possible?)

[Karl, 2014/06/30 22:09:06]

This isn't possible.

+
+UnderlyingCount
+---------------
+
+Returns the number of primitive types in the construct. For primitive
+types, the *UnderlyingCount* is 1. For vector types, it returns the
+number of elements in the vector.
+
+IsInteger
+---------
+
+Returns true if the argument is in {i1, i8, i16, i32, i64}.
+
+IsFloat
+-------
+
+Returns true if the argument is in {float, double}.
+
+Abbreviations
+-------------
+
+TODO(kschimpf)
+
+Introduction
+^^^^^^^^^^^^
+
+TODO(kschimpf)
+
+* Blocks
+* Data Records
+* Abbreviations
+* Abbreviation Ids.
+
+Bitstream Format
+^^^^^^^^^^^^^^^^
+
+TODO(kschimpf)
+
+* Header
+* Block Structure
+* Primitives
+* Abbreviations
+* BlockInfoBlock
+
+The *abbreviations block* [ref] is the first block in the module buld.. The

[Jim Stichnoth, 2014/06/06 18:24:46]

buld?

[Karl, 2014/06/30 22:09:03]

Done.

+block is divided into sections.  Each section is a sequence of records. Each
+record in the sequence defines a user-defined abbreviation.  Each section
+defines abbreviations that can be applied to all (succeeding) blocks of a
+particular kind. These abbreviations are denoted by the (global) ID of the form
+*@aN*.
+
+Reference Implementation
+------------------------
+
+TODO(kschimpf)
+