Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r774 r961  
    2121
    2222inductive constant : Type[0] ≝
    23   | Ointconst: int → constant     (**r integer constant *)
    24   | Ofloatconst: float → constant (**r floating-point constant *)
    25   | Oaddrsymbol: ident → int → constant (**r address of the symbol plus the offset *)
    26   | Oaddrstack: int → constant.   (**r stack pointer plus the given offset *)
     23  | Ointconst: ∀sz. bvint sz → constant    (**r integer constant *)
     24  | Ofloatconst: float → constant          (**r floating-point constant *)
     25  | Oaddrsymbol: ident → nat → constant    (**r address of the symbol plus the offset *)
     26  | Oaddrstack: nat → constant.            (**r stack pointer plus the given offset *)
    2727
    2828inductive unary_operation : Type[0] ≝
    29   | Ocast8unsigned: unary_operation        (**r 8-bit zero extension  *)
    30   | Ocast8signed: unary_operation          (**r 8-bit sign extension  *)
    31   | Ocast16unsigned: unary_operation       (**r 16-bit zero extension  *)
    32   | Ocast16signed: unary_operation         (**r 16-bit sign extension *)
     29  | Ocastint: intsize → signedness → unary_operation (**r 8-bit zero extension  *)
    3330  | Onegint: unary_operation               (**r integer opposite *)
    3431  | Onotbool: unary_operation              (**r boolean negation  *)
     
    3734  | Oabsf: unary_operation                 (**r float absolute value *)
    3835  | Osingleoffloat: unary_operation        (**r float truncation *)
    39   | Ointoffloat: unary_operation          (**r signed integer to float *)
    40   | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
     36  | Ointoffloat: intsize → unary_operation (**r signed integer to float *)
     37  | Ointuoffloat: intsize → unary_operation (**r unsigned integer to float *)
    4138  | Ofloatofint: unary_operation           (**r float to signed integer *)
    4239  | Ofloatofintu: unary_operation          (**r float to unsigned integer *)
    4340  | Oid: unary_operation                   (**r identity (used to move between registers *)
    4441  | Optrofint: region → unary_operation    (**r int to pointer with given representation *)
    45   | Ointofptr: unary_operation.            (**r pointer to int *)
     42  | Ointofptr: intsize → unary_operation.  (**r pointer to int *)
    4643
    4744inductive binary_operation : Type[0] ≝
     
    6865  | Oaddp: binary_operation                (**r add an integer to a pointer *)
    6966  | Osubpi: binary_operation               (**r subtract int from a pointers *)
    70   | Osubpp: binary_operation               (**r subtract two pointers *)
     67  | Osubpp: intsize → binary_operation     (**r subtract two pointers *)
    7168  | Ocmpp: comparison → binary_operation.  (**r compare pointers *)
    7269
     
    8077λfind_symbol,sp,cst.
    8178  match cst with
    82   [ Ointconst n ⇒ Some ? (Vint n)
     79  [ Ointconst sz n ⇒ Some ? (Vint sz n)
    8380  | Ofloatconst n ⇒ Some ? (Vfloat n)
    8481  | Oaddrsymbol s ofs ⇒
    8582      match find_symbol s with
    8683      [ None ⇒ None ?
    87       | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset zero_offset ofs))
     84      | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))
    8885      ]
    8986  | Oaddrstack ofs ⇒
    90       Some ? (Vptr Any sp ? (shift_offset zero_offset ofs))
     87      Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))
    9188  ]. cases sp // qed.
    9289
     
    9491λop,arg.
    9592  match op with
    96   [ Ocast8unsigned ⇒ Some ? (zero_ext 8 arg)
    97   | Ocast8signed ⇒ Some ? (sign_ext 8 arg)
    98   | Ocast16unsigned ⇒ Some ? (zero_ext 16 arg)
    99   | Ocast16signed ⇒ Some ? (sign_ext 16 arg)
    100   | Onegint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (neg n1)) | _ ⇒ None ? ]
    101   | Onotbool ⇒ match arg with [ Vint n1 ⇒ Some ? (of_bool (eq n1 zero))
     93  [ Ocastint sz sg ⇒
     94      match sg with
     95      [ Unsigned ⇒ Some ? (zero_ext sz arg)
     96      |   Signed ⇒ Some ? (sign_ext sz arg)
     97      ]
     98  | Onegint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
     99  | Onotbool ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (of_bool (eq_bv ? n1 (zero ?)))
    102100                              | Vptr _ _ _ _ ⇒ Some ? Vfalse
    103101                              | Vnull _ ⇒ Some ? Vtrue
    104102                              | _ ⇒ None ?
    105103                              ]
    106   | Onotint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vint (not n1)) | _ ⇒ None ? ]
     104  | Onotint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
    107105  | Onegf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
    108106  | Oabsf ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
    109107  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
    110   | Ointoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intoffloat f1)) | _ ⇒ None ? ]
    111   | Ointuoffloat ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint (intuoffloat f1)) | _ ⇒ None ? ]
    112   | Ofloatofint ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofint n1)) | _ ⇒ None ? ]
    113   | Ofloatofintu ⇒ match arg with [ Vint n1 ⇒ Some ? (Vfloat (floatofintu n1)) | _ ⇒ None ? ]
     108  | Ointoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
     109  | Ointuoffloat sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
     110  | Ofloatofint ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
     111  | Ofloatofintu ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ]
    114112  | Oid ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
    115113  (* Only conversion of null pointers is specified. *)
    116   | Optrofint r ⇒ match arg with [ Vint n1 ⇒ if eq n1 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    117   | Ointofptr ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
     114  | Optrofint r ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     115  | Ointofptr sz ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    118116  ].
    119117
     
    122120λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].
    123121
    124 (* Individual operations, adapted from Values. *)
    125 
    126 definition ev_neg : val → option val ≝ λv.
    127   match v with
    128   [ Vint n ⇒ Some ? (Vint (neg n))
    129   | _ ⇒ None ?
    130   ].
    131 
    132 definition ev_negf : val → option val ≝ λv.
    133   match v with
    134   [ Vfloat f ⇒ Some ? (Vfloat (Fneg f))
    135   | _ ⇒ None ?
    136   ].
    137 
    138 definition ev_absf : val → option val ≝ λv.
    139   match v with
    140   [ Vfloat f ⇒ Some ? (Vfloat (Fabs f))
    141   | _ ⇒ None ?
    142   ].
    143 
    144 definition ev_intoffloat : val → option val ≝ λv.
    145   match v with
    146   [ Vfloat f ⇒ Some ? (Vint (intoffloat f))
    147   | _ ⇒ None ?
    148   ].
    149 
    150 definition ev_intuoffloat : val → option val ≝ λv.
    151   match v with
    152   [ Vfloat f ⇒ Some ? (Vint (intuoffloat f))
    153   | _ ⇒ None ?
    154   ].
    155 
    156 definition ev_floatofint : val → option val ≝ λv.
    157   match v with
    158   [ Vint n ⇒ Some ? (Vfloat (floatofint n))
    159   | _ ⇒ None ?
    160   ].
    161 
    162 definition ev_floatofintu : val → option val ≝ λv.
    163   match v with
    164   [ Vint n ⇒ Some ? (Vfloat (floatofintu n))
    165   | _ ⇒ None ?
    166   ].
    167 
    168 definition ev_notint : val → option val ≝ λv.
    169   match v with
    170   [ Vint n ⇒ Some ? (Vint (xor n mone))
    171   | _ ⇒ None ?
    172   ].
    173  
    174 definition ev_notbool : val → option val ≝ λv.
    175   match v with
    176   [ Vint n ⇒ Some ? (of_bool (int_eq n zero))
    177   | Vptr _ b _ ofs ⇒ Some ? Vfalse
    178   | Vnull _ ⇒ Some ? Vtrue
    179   | _ ⇒ None ?
    180   ].
    181 
    182 definition ev_zero_ext ≝ λnbits: nat. λv: val.
    183   match v with
    184   [ Vint n ⇒ Some ? (Vint (zero_ext nbits n))
    185   | _ ⇒ None ?
    186   ].
    187 
    188 definition ev_sign_ext ≝ λnbits:nat. λv:val.
    189   match v with
    190   [ Vint i ⇒ Some ? (Vint (sign_ext nbits i))
    191   | _ ⇒ None ?
    192   ].
    193 
    194 definition ev_singleoffloat : val → option val ≝ λv.
    195   match v with
    196   [ Vfloat f ⇒ Some ? (Vfloat (singleoffloat f))
    197   | _ ⇒ None ?
    198   ].
     122(* Individual operations, adapted from Values.  These differ in that they
     123   implement the plain Cminor/RTLabs operations (e.g., with separate addition
     124   for ints,floats and pointers) and use option rather than Vundef.  The ones
     125   in Value are probably not needed. *)
    199126
    200127definition ev_add ≝ λv1,v2: val.
    201128  match v1 with
    202   [ Vint n1 ⇒ match v2 with
    203     [ Vint n2 ⇒ Some ? (Vint (addition_n ? n1 n2))
     129  [ Vint sz1 n1 ⇒ match v2 with
     130    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     131                    (λn1. Some ? (Vint ? (addition_n ? n1 n2)))
     132                    (None ?)
    204133    | _ ⇒ None ? ]
    205134  | _ ⇒ None ? ].
     
    207136definition ev_sub ≝ λv1,v2: val.
    208137  match v1 with
    209   [ Vint n1 ⇒ match v2 with
    210     [ Vint n2 ⇒ Some ? (Vint (subtraction ? n1 n2))
     138  [ Vint sz1 n1 ⇒ match v2 with
     139    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     140                    (λn1. Some ? (Vint ? (subtraction ? n1 n2)))
     141                    (None ?)
    211142    | _ ⇒ None ? ]
    212143  | _ ⇒ None ? ].
     
    216147  match v1 with
    217148  [ Vptr r b1 p ofs1 ⇒ match v2 with
    218     [ Vint n2 ⇒ Some ? (Vptr r b1 p (shift_offset ofs1 n2))
     149    [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2))
    219150    | _ ⇒ None ? ]
    220151  | Vnull r ⇒ match v2 with
    221     [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ?
     152    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
    222153    | _ ⇒ None ?
    223154    ]
     
    227158  match v1 with
    228159  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    229     [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ofs1 n2))
    230     | _ ⇒ None ? ]
    231   | Vnull r ⇒ match v2 with [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
    232   | _ ⇒ None ? ].
    233 
    234 definition ev_subpp ≝ λv1,v2: val.
     160    [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2))
     161    | _ ⇒ None ? ]
     162  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     163  | _ ⇒ None ? ].
     164
     165definition ev_subpp ≝ λsz. λv1,v2: val.
    235166  match v1 with
    236167  [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    237168    [ Vptr r2 b2 p2 ofs2 ⇒
    238         if eq_block b1 b2 then Some ? (Vint (sub_offset ofs1 ofs2)) else None ?
    239     | _ ⇒ None ? ]
    240   | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
     169        if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ?
     170    | _ ⇒ None ? ]
     171  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    241172  | _ ⇒ None ? ].
    242173
    243174definition ev_mul ≝ λv1, v2: val.
    244175  match v1 with
    245   [ Vint n1 ⇒ match v2 with
    246     [ Vint n2 ⇒ Some ? (Vint (mul n1 n2))
     176  [ Vint sz1 n1 ⇒ match v2 with
     177    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     178                    (λn1. Some ? (Vint ? (\snd (split … (multiplication ? n1 n2)))))
     179                    (None ?)
    247180    | _ ⇒ None ? ]
    248181  | _ ⇒ None ? ].
     
    250183definition ev_divs ≝ λv1, v2: val.
    251184  match v1 with
    252   [ Vint n1 ⇒ match v2 with
    253     [ Vint n2 ⇒ option_map ?? Vint (division_s ? n1 n2)
     185  [ Vint sz1 n1 ⇒ match v2 with
     186    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     187                    (λn1. option_map ?? (Vint ?) (division_s ? n1 n2))
     188                    (None ?)
    254189    | _ ⇒ None ? ]
    255190  | _ ⇒ None ? ].
     
    257192definition ev_mods ≝ λv1, v2: val.
    258193  match v1 with
    259   [ Vint n1 ⇒ match v2 with
    260     [ Vint n2 ⇒ option_map ?? Vint (modulus_s ? n1 n2)
     194  [ Vint sz1 n1 ⇒ match v2 with
     195    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     196                    (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2))
     197                    (None ?)
    261198    | _ ⇒ None ?
    262199    ]
     
    266203definition ev_divu ≝ λv1, v2: val.
    267204  match v1 with
    268   [ Vint n1 ⇒ match v2 with
    269     [ Vint n2 ⇒ option_map ?? Vint (division_u ? n1 n2)
     205  [ Vint sz1 n1 ⇒ match v2 with
     206    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     207                    (λn1. option_map ?? (Vint ?) (division_u ? n1 n2))
     208                    (None ?)
    270209    | _ ⇒ None ?
    271210    ]
     
    275214definition ev_modu ≝ λv1, v2: val.
    276215  match v1 with
    277   [ Vint n1 ⇒ match v2 with
    278     [ Vint n2 ⇒ option_map ?? Vint (modulus_u ? n1 n2)
     216  [ Vint sz1 n1 ⇒ match v2 with
     217    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     218                    (λn1. option_map ?? (Vint ?) (modulus_u ? n1 n2))
     219                    (None ?)
    279220    | _ ⇒ None ?
    280221    ]
     
    284225definition ev_and ≝ λv1, v2: val.
    285226  match v1 with
    286   [ Vint n1 ⇒ match v2 with
    287     [ Vint n2 ⇒ Some ? (Vint (i_and n1 n2))
     227  [ Vint sz1 n1 ⇒ match v2 with
     228    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     229                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2)))
     230                    (None ?)
    288231    | _ ⇒ None ? ]
    289232  | _ ⇒ None ? ].
     
    291234definition ev_or ≝ λv1, v2: val.
    292235  match v1 with
    293   [ Vint n1 ⇒ match v2 with
    294     [ Vint n2 ⇒ Some ? (Vint (or n1 n2))
     236  [ Vint sz1 n1 ⇒ match v2 with
     237    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     238                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2)))
     239                    (None ?)
    295240    | _ ⇒ None ? ]
    296241  | _ ⇒ None ? ].
     
    298243definition ev_xor ≝ λv1, v2: val.
    299244  match v1 with
    300   [ Vint n1 ⇒ match v2 with
    301     [ Vint n2 ⇒ Some ? (Vint (xor n1 n2))
     245  [ Vint sz1 n1 ⇒ match v2 with
     246    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     247                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2)))
     248                    (None ?)
    302249    | _ ⇒ None ? ]
    303250  | _ ⇒ None ? ].
     
    305252definition ev_shl ≝ λv1, v2: val.
    306253  match v1 with
    307   [ Vint n1 ⇒ match v2 with
    308     [ Vint n2 ⇒
    309        if ltu n2 iwordsize
    310        then Some ? (Vint (shl n1 n2))
     254  [ Vint sz1 n1 ⇒ match v2 with
     255    [ Vint sz2 n2 ⇒
     256       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     257       then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
    311258       else None ?
    312259    | _ ⇒ None ? ]
     
    315262definition ev_shr ≝ λv1, v2: val.
    316263  match v1 with
    317   [ Vint n1 ⇒ match v2 with
    318     [ Vint n2 ⇒
    319        if ltu n2 iwordsize
    320        then Some ? (Vint (shr n1 n2))
     264  [ Vint sz1 n1 ⇒ match v2 with
     265    [ Vint sz2 n2 ⇒
     266       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     267       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
    321268       else None ?
    322269    | _ ⇒ None ? ]
    323270  | _ ⇒ None ? ].
    324271
    325 definition ev_shr_carry ≝ λv1, v2: val.
    326   match v1 with
    327   [ Vint n1 ⇒ match v2 with
    328     [ Vint n2 ⇒
    329        if ltu n2 iwordsize
    330        then Some ? (Vint (shr_carry n1 n2))
    331        else None ?
    332     | _ ⇒ None ? ]
    333   | _ ⇒ None ? ].
    334 
    335 definition ev_shrx ≝ λv1, v2: val.
    336   match v1 with
    337   [ Vint n1 ⇒ match v2 with
    338     [ Vint n2 ⇒
    339        if ltu n2 iwordsize
    340        then Some ? (Vint (shrx n1 n2))
    341        else None ?
    342     | _ ⇒ None ? ]
    343   | _ ⇒ None ? ].
    344 
    345272definition ev_shru ≝ λv1, v2: val.
    346273  match v1 with
    347   [ Vint n1 ⇒ match v2 with
    348     [ Vint n2 ⇒
    349        if ltu n2 iwordsize
    350        then Some ? (Vint (shru n1 n2))
    351        else None ?
    352     | _ ⇒ None ? ]
    353   | _ ⇒ None ? ].
    354 
    355 definition ev_rolm ≝
    356 λv: val. λamount, mask: int.
    357   match v with
    358   [ Vint n ⇒ Some ? (Vint (rolm n amount mask))
    359   | _ ⇒ None ?
    360   ].
    361 
    362 definition ev_ror ≝ λv1, v2: val.
    363   match v1 with
    364   [ Vint n1 ⇒ match v2 with
    365     [ Vint n2 ⇒
    366        if ltu n2 iwordsize
    367        then Some ? (Vint (ror n1 n2))
     274  [ Vint sz1 n1 ⇒ match v2 with
     275    [ Vint sz2 n2 ⇒
     276       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
     277       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false))
    368278       else None ?
    369279    | _ ⇒ None ? ]
     
    414324definition ev_cmp ≝ λc: comparison. λv1,v2: val.
    415325  match v1 with
    416   [ Vint n1 ⇒ match v2 with
    417     [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2))
     326  [ Vint sz1 n1 ⇒ match v2 with
     327    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     328                    (λn1. Some ? (of_bool (cmp_int ? c n1 n2)))
     329                    (None ?)
    418330    | _ ⇒ None ? ]
    419331  | _ ⇒ None ? ].
     
    438350definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
    439351  match v1 with
    440   [ Vint n1 ⇒ match v2 with
    441     [ Vint n2 ⇒ Some ? (of_bool (cmpu c n1 n2))
     352  [ Vint sz1 n1 ⇒ match v2 with
     353    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
     354                    (λn1. Some ? (of_bool (cmpu_int ? c n1 n2)))
     355                    (None ?)
    442356    | _ ⇒ None ? ]
    443357  | _ ⇒ None ? ].
     
    475389  | Oaddp ⇒ ev_addp
    476390  | Osubpi ⇒ ev_subpi
    477   | Osubpp ⇒ ev_subpp
     391  | Osubpp sz ⇒ ev_subpp sz
    478392  | Ocmpp c ⇒ ev_cmpp c
    479393  ].
Note: See TracChangeset for help on using the changeset viewer.