Change table data_processing_immediate to use the new notation. Also

src/trusted/validator_arm/armv7.table

Index: src/trusted/validator_arm/armv7.table
===================================================================
--- src/trusted/validator_arm/armv7.table	(revision 9758)
+++ src/trusted/validator_arm/armv7.table	(working copy)
@@ -105,8 +105,8 @@
 #
 # base: The register used as the base for the effective address
 #       for reads and writes.
-# target: The register use to compute an indirect branch,
-#       if defined (defaults to None).
+# clear_bits: True implies that the masked bits are cleared.
+#       (defaults to false). Corresponds to virtual clear_bits.
 # defs: The set of registers defined. (missing implies {}).
 # imm_defs: The set of registers that are set through
 #       immediate indexed addressing writeback, where the
@@ -120,10 +120,12 @@
 # relative_offset: Defines the constant offset used in a direct
 #       relative branch.
 # safety: How safety is defined for the class (missing implies true).
+# sets_Z_if_clear_bits: True implies that it sets the Z (condition)
+#       bit if mask bits are cleared. (defaults to false).
+#       Corresponds to defining virtual sets_Z_if_clear_bits.
+# target: The register use to compute an indirect branch,
+#       if defined (defaults to None).
 # uses: The set of registers  used. (missing imlies {})
-#
-# TODO(karl): How do we model class decoder virtuals clear_bits
-#    and sets_Z_if_bits_clear.
 ##############################################################
 
 ##############################################################
@@ -389,110 +391,121 @@
 # TestIfAddressMasked and MaskAddress. These two instructions are the
 # ones that we allow testing/setting of bits to mask data addresses
 # appropriately.
+*1 Binary2RegisterImmediateOp => Defs12To15
+   { cond(31:28), S(20), Rn(19:16), Rd(15:12), imm12(11:0) }
+   setflags := S=1; imm32 := ARMExpandImm(imm12);

[JF, 2012/09/19 01:14:23]

ARMExpandImm_C

[Karl, 2012/09/20 19:47:42]

Done.

+   defs := {Rd, NZCV if setflags else None};   
+   safety := (Rd=1111 & S=1) => UNDEFINED &  # ARM

[JF, 2012/09/19 01:14:23]

Rd=1111 & S=1 is actually the SUB PC, LR instruction, which is forbidden. Why
not just mark it as FORBIDDEN_OPERANDS?

[Karl, 2012/09/20 19:47:42]

The real problem is that we don't have a value that states we have a problem
with our decoder.

[Karl, 2012/09/20 19:47:42]

Changed to DECODER_ERROR.

+             Rd=1111 => FORBIDDEN_OPERANDS;  # NaCl
+   uses := {Rn};
+*2 Binary2RegisterImmediateOp => Defs12To15

[JF, 2012/09/19 01:14:23]

Why make this different from *1? The only difference is (Rn=1111 & S=0), but
that's not undefined: it's ADR. There would be a parse conflict if this weren't
the case. It seems like *2 uses could be folded into *1 uses.

[Karl, 2012/09/20 19:47:42]

Like above, made a DECODER_ERROR entry.

+   { cond(31:28), S(20), Rn(19:16), Rd(15:12), imm12(11:0) }
+   setflags := S=1; imm32 := ARMExpandImm(imm12);
+   defs := {Rd, NZCV if setflags else None};   
+   safety := (Rd=1111 & S=1) => UNDEFINED &  # ARM
+             (Rn=1111 & S=0) => UNDEFINED &
+             Rd=1111 => FORBIDDEN_OPERANDS;  # NaCl
+   uses := {Rn};
+*3 Unary1RegisterImmediateOp => Defs12To15
+   { cond(31:28), Rd(15:12), imm12(11:0) }
+   imm32 := ARMExpandImm(imm12); add := false;
+   defs := {Rd};
+   safety := Rd=1111 => FORBIDDEN_OPERANDS;      # NaCl
+   uses := {Pc};
+*4 Unary1RegisterImmediateOp => Defs12To15

[JF, 2012/09/19 01:14:23]

*4 is only different from *3 in the add variable. bit 23 is often the U bit, and
*3/*4 are the same with:
  add := U=1;

[Karl, 2012/09/20 19:47:42]

Merged.

+   { cond(31:28), Rd(15:12), imm12(11:0) }
+   imm32 := ARMExpandImm(imm12); add := true;
+   defs := {Rd};
+   safety := Rd=1111 => FORBIDDEN_OPERANDS;      # NaCl
+   uses := {Pc};
+*5 BinaryRegisterImmediateTest => DontCareInst
+   { cond(31:28), Rn(19:15), imm12(11:0) }

[JF, 2012/09/19 01:14:23]

Rn(19:16)

[Karl, 2012/09/20 19:47:42]

Done.

+   imm32 := AMRExpandImm(imm12);

[JF, 2012/09/19 01:14:23]

ARMExpandImm_C

[Karl, 2012/09/20 19:47:42]

Done.

+   defs := {NZCV};

[JF, 2012/09/19 01:14:23]

uses := {Rn};

[Karl, 2012/09/20 19:47:42]

Done.

+*6 MaskedBinaryRegisterImmediateTest => TestIfAddressMasked
+   # Note: This instruction is used to test if the immediate value
+   # appropriately (data address) masks the value in Rn. Otherwise,
+   # it would be the same as *5 above.
+   { cond(31:28), Rn(19:15), imm12(11:0) }

[JF, 2012/09/19 01:14:23]

Rn(19:16)

[Karl, 2012/09/20 19:47:42]

Done.

+   imm32 := AMRExpandImm(imm12);

[JF, 2012/09/19 01:14:23]

ARMExpandImm_C

[Karl, 2012/09/20 19:47:42]

Done.

+   defs := {NZCV};
+   sets_Z_if_bits_clear := true;

[JF, 2012/09/19 01:14:23]

uses := {Rn};

[Karl, 2012/09/20 19:47:42]

Done.

+*7 Unary1RegisterImmediateOp => Defs12To15

[JF, 2012/09/19 01:14:23]

*7 is wrong and encodes encoding A2, not A1. It should be:

{ cond(31:28), S(20), Rd(15:12), imm12(11:10) }
setflags := S=1; imm32 := ARMExpandImm_C(imm12);
defs := {Rd, NZCV if setflags else None};
safety := (Rd=1111 & S=1) => FORBIDDEN_OPERANDS &
           Rd=1111 => FORBIDDEN_OPERANDS;
uses := {};

[Karl, 2012/09/20 19:47:42]

Fixed.

+   { cond(31:28), imm4(19:16), Rd(15:12), imm12(11:0) }
+   setflags := false; imm32 := ZeroExtend(imm4:imm12, 32);
+   defs := {Rd};
+   safety := Rd=1111 => UNPREDICTABLE;           # ARM and NaCl
+*8 MaskedBinary2RegisterImmediateOp => MaskAddress
+   # Note: This instruction is used to mask memory addresses. Otherwise,
+   # it would be the same as *1.
+   { cond(31:28), S(20), Rn(19:16), Rd(15:12), imm12(11:0) }
+   setflags := S=1; imm32 := ARMExpandImm(imm12);

[JF, 2012/09/19 01:14:23]

ARMExpandImm_C

[Karl, 2012/09/20 19:47:42]

Done.

+   defs := {Rd, NZCV if setflags else None};
+   safety := (Rd=1111 & S=1) => UNDEFINED &  # ARM

[JF, 2012/09/19 01:14:23]

FORBIDDEN_OPERANDS, as above.

[Karl, 2012/09/20 19:47:42]

Changed to DECODER_ERROR.

+             Rd=1111 => FORBIDDEN_OPERANDS;  # NaCl
+   uses := {Rn};
+   clears_bits := true;
+*9 Unary1RegisterImmediateOp => Defs12To15

[JF, 2012/09/19 01:14:23]

This is the same as *7 that I've defined above (except for corrections above).

[Karl, 2012/09/20 19:47:42]

Merged.

+   { cond(31:28), S(20), Rd(15:12), imm12(11:0) }
+   setflags := S=1; imm32 := ARMExpandImm(imm12);
+   defs := {Rd, NZCV if setflags else None};
+   safety := (Rd=1111 & S=1) => UNDEFINED &  # ARM
+             Rd=1111 => FORBIDDEN_OPERANDS;  # NaCl
++--
 | op(24:20) Rn(19:16)
-| 0000x      -        = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           And_Rule_11_A1_P34
-                           cccc0010000snnnnddddiiiiiiiiiiii NotRdIsPcAndS
-| 0001x      -        = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           Eor_Rule_44_A1_P94
-                           cccc0010001snnnnddddiiiiiiiiiiii NotRdIsPcAndS
-| 0010x      ~1111    = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           Sub_Rule_212_A1_P420
-                           cccc0010010snnnnddddiiiiiiiiiiii
-                           NeitherRdIsPcAndSNorRnIsPcAndNotS
-                        # Note: Table says that op=0010x for ADR, but
-                        # patterns for ADR do not match (page A8-32).
-                        # Causes parsing conflicts with SUB (previous
-                        # row). Added restriction to ADR that bit 20
-                        # (updates flags register) must be 0 (rather than
-                        # x), to match what is on A8.6.10 (page A8-32).
-                        # Note that this also matches restrictions of
-                        # A8.6.212 (page A8-420).
-| 00100      1111     = Unary1RegisterImmediateOp
-                           => Defs12To15
-                           Adr_Rule_10_A2_P32
-                           cccc001001001111ddddiiiiiiiiiiii
-| 00101      1111     = ForbiddenCondDecoder => Forbidden
-                           Subs_Pc_Lr_and_related_instructions_Rule_A1a
-                           cccc00100101nnnn1111iiiiiiiiiiii
-| 0011x      -        = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           Rsb_Rule_142_A1_P284
-                           cccc0010011snnnnddddiiiiiiiiiiii NotRdIsPcAndS
-| 0100x      ~1111    = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           Add_Rule_5_A1_P22
-                           cccc0010100snnnnddddiiiiiiiiiiii
-                           NeitherRdIsPcAndSNorRnIsPcAndNotS
-                        # Note: Table says that op=0100x for ADR, but
-                        # patterns for ADR do not match (page A8-32).
-                        # Causes parsing conflicts with ADD (previous
-                        # row). Added restriction to ADR that bit 20
-                        # (updates flags register) must be 0 (rather than
-                        # x), to match what is on A8.6.10 (page A8-32).
-                        # Note that this also matches restrictions of
-                        # A8.6.5 (page A8-22).
-| 01000      1111     = Unary1RegisterImmediateOp
-                           => Defs12To15
-                           Adr_Rule_10_A1_P32
-                           cccc001010001111ddddiiiiiiiiiiii
-| 01001      1111     = ForbiddenCondDecoder => Forbidden
-                           Subs_Pc_Lr_and_related_instructions_Rule_A1b
-                           cccc00101001nnnn1111iiiiiiiiiiii
-| 0101x      -        = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           Adc_Rule_6_A1_P14
-                           cccc0010101snnnnddddiiiiiiiiiiii NotRdIsPcAndS
-| 0110x      -        = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           Sbc_Rule_151_A1_P302
-                           cccc0010110snnnnddddiiiiiiiiiiii NotRdIsPcAndS
-| 0111x      -        = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           Rsc_Rule_145_A1_P290
-                           cccc0010111snnnnddddiiiiiiiiiiii NotRdIsPcAndS
+| 0000x      -        = *1 pattern := cccc0010000snnnnddddiiiiiiiiiiii
+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Why this restriction? Won't the safety make this case UNDEFINED?

[Karl, 2012/09/20 19:47:42]

This is a testing infrastructure issue. It is needed to communicate to the
testing infrastructure that we should find a different decoder here.

However, looking closer, the conflicting instructions are system instructions
that aren't in our decoder tables, and that we disallow with the ARM restriction
Rd=~1111. Hence, I've removed them

+                        rule := AND_immediate_A1;
+| 0001x      -        = *1 pattern := cccc0010001snnnnddddiiiiiiiiiiii
+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := EOR_immediate_A1;
+| 0010x      ~1111    = *2 pattern := cccc0010010snnnnddddiiiiiiiiiiii

[JF, 2012/09/19 01:14:23]

As noted above, change *2 to *1.

[Karl, 2012/09/20 19:47:42]

Done.

+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+# Note: For arm, the case where Rn=SP is not a special case (only in thumb2).
+# Hence, parse restriction does not apply (See SUB (SP minus immediate)).

[JF, 2012/09/19 01:14:23]

Why this note? It confuses me.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := SUB_immediate_A1;
+| 0010x      1111     = *3 pattern := cccc001001001111ddddiiiiiiiiiiii;
+                        rule := ADR_A2;
+| 0011x      -        = *1 pattern := cccc0010011snnnnddddiiiiiiiiiiii
+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := RSB_immediate_A1;
+| 0100x      ~1111    = *2 pattern := cccc0010100snnnnddddiiiiiiiiiiii

[JF, 2012/09/19 01:14:23]

As noted above, change *2 to *1.

[Karl, 2012/09/20 19:47:42]

Done.

+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+# Note: For arm, the case where Rn=SP is not a special case (only in thumb2).
+# Hence, parse restriction does not apply (See ADD (SP plus immediate)).

[JF, 2012/09/19 01:14:23]

Ditto on my confusion.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := ADD_immediate_A1;
+| 0100x      1111     = *4 pattern := cccc001010001111ddddiiiiiiiiiiii;

[JF, 2012/09/19 01:14:23]

As noted above, change to *3.

[Karl, 2012/09/20 19:47:42]

Done.

+                        rule := ADR_A1;
+| 0101x      -        = *1 pattern := cccc0010101snnnnddddiiiiiiiiiiii
+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := ADC_immediate_A1;
+| 0110x      -        = *1 pattern := cccc0010110snnnnddddiiiiiiiiiiii
+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := SBC_immediate_A1;
+| 0111x      -        = *1 pattern := cccc0010111snnnnddddiiiiiiiiiiii
+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := RSC_immediate_A1;
 # TODO(jfb) op==10xx0 should be unreachable from here:
 #           the previous table should handle it.
-                        # Note: Following instruction is used to test
-                        # if the immediate value appropriately (data address)
-                        # masks the value in Rn.
-| 10001      -        = MaskedBinaryRegisterImmediateTest
-                           => TestIfAddressMasked
-                           Tst_Rule_230_A1_P454
-                           cccc00110001nnnn0000iiiiiiiiiiii
-| 10011      -        = BinaryRegisterImmediateTest
-                           => DontCareInst
-                           Teq_Rule_227_A1_P448
-                           cccc00110011nnnn0000iiiiiiiiiiii
-| 10101      -        = BinaryRegisterImmediateTest
-                           => DontCareInst
-                           Cmp_Rule_35_A1_P80
-                           cccc00110101nnnn0000iiiiiiiiiiii
-| 10111      -        = BinaryRegisterImmediateTest
-                           => DontCareInst
-                           Cmn_Rule_32_A1_P74
-                           cccc00110111nnnn0000iiiiiiiiiiii
-| 1100x      -        = Binary2RegisterImmediateOp
-                           => Defs12To15
-                           Orr_Rule_113_A1_P228
-                           cccc0011100snnnnddddiiiiiiiiiiii NotRdIsPcAndS
-| 1101x      -        = Unary1RegisterImmediateOp
-                           => Defs12To15
-                           Mov_Rule_96_A1_P194
-                           cccc0011101s0000ddddiiiiiiiiiiii NotRdIsPcAndS
-                        # Note: The following instruction is used to mask
-                        # memory addresses.
-| 1110x      -        = MaskedBinary2RegisterImmediateOp
-                           => MaskAddress
-                           Bic_Rule_19_A1_P50
-                           cccc0011110snnnnddddiiiiiiiiiiii NotRdIsPcAndS
-| 1111x      -        = Unary1RegisterImmediateOp
-                           => Defs12To15
-                           Mvn_Rule_106_A1_P214
-                           cccc0011111s0000ddddiiiiiiiiiiii NotRdIsPcAndS
+| 10001      -        = *6 pattern := cccc00110001nnnn0000iiiiiiiiiiii;
+                        rule := TST_immediate_A1;
+| 10011      -        = *5 pattern := cccc00110011nnnn0000iiiiiiiiiiii;
+                        rule := TEQ_immediate_A1;
+| 10101      -        = *5 pattern := cccc00110101nnnn0000iiiiiiiiiiii;
+                        rule := CMP_immediate_A1;
+| 10111      -        = *5 pattern := cccc00110111nnnn0000iiiiiiiiiiii;
+                        rule := CMN_immediate_A1;
+| 1100x      -        = *1 pattern := cccc0011100snnnnddddiiiiiiiiiiii
+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := ORR_immediate_A1;
+| 1101x      -        = *7 pattern := cccc0011101s0000ddddiiiiiiiiiiii;
+                        rule := MOV_immediate_A1;
+| 1110x      -        = *8 pattern := cccc0011110snnnnddddiiiiiiiiiiii
+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := BIC_immediate_A1;
+| 1111x      -        = *9 pattern := cccc0011111s0000ddddiiiiiiiiiiii

[JF, 2012/09/19 01:14:23]

Change to *7.

[Karl, 2012/09/20 19:47:42]

Done.

+                                      & not (Rd=1111 & S=1);

[JF, 2012/09/19 01:14:23]

Ditto on UNDEFINED restriction.

[Karl, 2012/09/20 19:47:42]

removed

+                        rule := MVN_immediate_A1;
 +--
 
 # Note: in all of these cases there's a currently unhandled restriction: