Use generated actual decoders for ARM table:

src/trusted/validator_arm/armv7.table

 # ARMv7 Instruction Encodings
 #
 # This table is derived from the "ARM Architecture Reference Manual, ARMv7-A
 # and ARMv7-R edition" and is used here with the permission of ARM Limited.
 # Reproduction for purposes other than the development and distribution of
 # Native Client may require the explicit permission of ARM Limited.
 
 # This file defines the Native Client "instruction classes" assigned to every
 # possible ARMv7 instruction encoding.  It is organized into a series of tables,
 # and directly parallels the ARM Architecture Reference Manual cited above.
@@ skipping 1762 matching lines @@
                                  pattern := cccc01110101ddddaaaammmm11r1nnnn;
                                  rule := SMMLS;
 | else:                        = Undefined  # Note associated with table.
 +--
 
 +-- branch_branch_with_link_and_block_data_transfer (See Section A5.5)
 *RnRegs
   { cond(31:28), W(21), Rn(19:16), register_list(15:0) }
   registers := RegisterList(register_list); wback := W=1;
   base := Rn;
-  small_imm_base_wb := true;
+  small_imm_base_wb := wback;
   safety := Rn == Pc | NumGPRs(registers) < 1 => UNPREDICTABLE;
 *LdRnRegs *RnRegs
   baseline := LoadRegisterList;
   defs := Union({Rn if wback else None}, registers);
   uses := {Rn};
   safety := super.safety &
             wback & Contains(registers, Rn) => UNKNOWN &
             Contains(registers, Pc) => FORBIDDEN_OPERANDS;
 *StRnRegs *RnRegs
   baseline := StoreRegisterList;
   defs := {Rn if wback else None};
   uses := Union({Rn}, registers);
   safety := super.safety &
             wback & Contains(registers, Rn) &
             Rn != SmallestGPR(registers) => UNKNOWN;
 *Branch
   { Cond(31:28), imm24(23:0) }
   baseline := BranchImmediate24;
   imm32 := SignExtend(imm24:'00', 32);
   defs := {Pc};
   uses := {Pc};
   relative := true;
-  relative_offset := imm32;
+  relative_offset := imm32 + 8;  # r15 is 8 bytes ahead of instruction address.

[JF, 2013/02/11 19:40:38]

I'd change the comment to be the same as other places in the code that do this:

The ARM manual states that "PC reads as the address of the current instruction
plus 8".

[Karl, 2013/02/11 22:12:43]

Done.

   safety := true => MAY_BE_SAFE;
 *BranchLink *Branch
   defs := {Pc, Lr};
 *Forbidden
   baseline := ForbiddenCondDecoder;
 +--
 | op(25:20) R(15) Rn(19:16)
 | 0000x0    -     -         = *StRnRegs
                                pattern := cccc100000w0nnnnrrrrrrrrrrrrrrrr;
                                rule := STMDA_STMED;
@@ skipping 1987 matching lines @@
                     rule := VLD3_single_3_element_structure_to_all_lanes;
 | " "     0x11    = *VLSS4
                     pattern := 111101001d10nnnnddddss11aaaammmm;
                     rule := VLD4_single_4_element_structure_to_one_lane;
 | " "     1011    "
 | " "     1111    = *VLS4A
                     pattern := 111101001d10nnnndddd1111sstammmm;
                     rule := VLD4_single_4_element_structure_to_all_lanes;
 | else:           = Undefined
 +--