Hybrid 64bit/32bit PowerPC port

This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.

The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.

In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.

1 files changed, 252 insertions, 26 deletions

diff --git a/powerpc/Op.v b/powerpc/Op.v
index e171c7d4..de4eee48 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -35,7 +35,6 @@ Require Import Globalenvs.
 Require Import Events.
 
 Set Implicit Arguments.
-Local Transparent Archi.ptr64.
 
 (** Conditions (boolean-valued operators). *)
 
@@ -43,11 +42,16 @@ Inductive condition : Type :=
   | Ccomp: comparison -> condition      (**r signed integer comparison *)
   | Ccompu: comparison -> condition     (**r unsigned integer comparison *)
   | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *)
-  | Ccompuimm: comparison -> int -> condition  (**r unsigned integer comparison with a constant *)
+  | Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *)
   | Ccompf: comparison -> condition     (**r floating-point comparison *)
   | Cnotcompf: comparison -> condition  (**r negation of a floating-point comparison *)
   | Cmaskzero: int -> condition         (**r test [(arg & constant) == 0] *)
-  | Cmasknotzero: int -> condition.     (**r test [(arg & constant) != 0] *)
+  | Cmasknotzero: int -> condition      (**r test [(arg & constant) != 0] *)
+(*c PPC64 specific conditions: *)
+  | Ccompl: comparison -> condition     (**r signed int64 comparison *)
+  | Ccomplu: comparison -> condition    (**r unsigned int64 comparison *)
+  | Ccomplimm: comparison -> int64 -> condition (**r signed int64 comparison with a constant *)
+  | Ccompluimm: comparison -> int64 -> condition. (**r unsigned int64 comparison with a constant *)
 
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
@@ -58,7 +62,7 @@ Inductive operation : Type :=
   | Ofloatconst: float -> operation     (**r [rd] is set to the given float constant *)
   | Osingleconst: float32 -> operation  (**r [rd] is set to the given float constant *)
   | Oaddrsymbol: ident -> ptrofs -> operation (**r [rd] is set to the the address of the symbol plus the offset *)
-  | Oaddrstack: ptrofs -> operation        (**r [rd] is set to the stack pointer plus the given offset *)
+  | Oaddrstack: ptrofs -> operation     (**r [rd] is set to the stack pointer plus the given offset *)
 (*c Integer arithmetic: *)
   | Ocast8signed: operation             (**r [rd] is 8-bit sign extension of [r1] *)
   | Ocast16signed: operation            (**r [rd] is 16-bit sign extension of [r1] *)
@@ -92,6 +96,34 @@ Inductive operation : Type :=
   | Oshru: operation                    (**r [rd = r1 >> r2] (unsigned) *)
   | Orolm: int -> int -> operation      (**r rotate left and mask *)
   | Oroli: int -> int -> operation      (**r rotate left and insert *)
+(*c PPC64 64-bit integer arithmetic: *)
+  | Olongconst: int64 -> operation      (**r [rd] is set to the given int64 constant *)
+  | Ocast32signed: operation            (**r [rd] is 64-bit sign extension of [r1] *)
+  | Ocast32unsigned: operation          (**r [rd] is 64-bit zero extension of [r1] *)
+  | Oaddl: operation                    (**r [rd = r1 + r2] *)
+  | Oaddlimm: int64 -> operation        (**r [rd = r1 + n] *)
+  | Osubl: operation                    (**r [rd = r1 - r2] *)
+  | Onegl: operation                    (**r [rd = - r1] *)
+  | Omull: operation                    (**r [rd = r1 * r2] *)
+  | Omullhs: operation                   (**r [rd = high part of r1 * r2, signed] *)
+  | Omullhu: operation                  (**r [rd = high part of r1 * r2, unsigned] *)
+  | Odivl: operation                    (**r [rd = r1 / r2] (signed) *)
+  | Odivlu: operation                   (**r [rd = r1 / r2] (unsigned) *)
+  | Oandl: operation                    (**r [rd = r1 & r2] *)
+  | Oandlimm: int64 -> operation        (**r [rd = r1 & n] *)
+  | Oorl: operation                     (**r [rd = r1 | r2] *)
+  | Oorlimm: int64 -> operation         (**r [rd = r1 | n] *)
+  | Oxorl: operation                    (**r [rd = r1 ^ r2] *)
+  | Oxorlimm: int64 -> operation        (**r [rd = r1 ^ n] *)
+  | Onotl: operation                    (**r [rd = ~r1] *)
+  | Oshll: operation                    (**r [rd = r1 << r2] *)
+  | Oshrl: operation                    (**r [rd = r1 >> r2] (signed) *)
+  | Oshrlimm: int -> operation          (**r [rd = r1 >> n] (signed) *)
+  | Oshrxlimm: int -> operation         (**r [rd = r1 / 2^n] (signed) *)
+  | Oshrlu: operation                   (**r [rd = r1 >> r2] (unsigned) *)
+  | Orolml: int -> int64 -> operation   (**r rotate left and mask *)
+  | Olongoffloat: operation             (**r [rd = signed_int64_of_float(r1)] *)
+  | Ofloatoflong: operation             (**r [rd = float_of_signed_int64(r1)] *)
 (*c Floating-point arithmetic: *)
   | Onegf: operation                    (**r [rd = - r1] *)
   | Oabsf: operation                    (**r [rd = abs(r1)] *)
@@ -120,27 +152,28 @@ Inductive operation : Type :=
 (*c Boolean tests: *)
   | Ocmp: condition -> operation.       (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
 
+
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
 
 Inductive addressing: Type :=
-  | Aindexed: int -> addressing         (**r Address is [r1 + offset] *)
-  | Aindexed2: addressing               (**r Address is [r1 + r2] *)
+  | Aindexed: int -> addressing            (**r Address is [r1 + offset] *)
+  | Aindexed2: addressing                  (**r Address is [r1 + r2] *)
   | Aglobal: ident -> ptrofs -> addressing (**r Address is [symbol + offset] *)
-  | Abased: ident -> ptrofs -> addressing (**r Address is [symbol + offset + r1] *)
+  | Abased: ident -> ptrofs -> addressing  (**r Address is [symbol + offset + r1] *)
   | Ainstack: ptrofs -> addressing.        (**r Address is [stack_pointer + offset] *)
 
 (** Comparison functions (used in module [CSE]). *)
 
 Definition eq_condition (x y: condition) : {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec; intro.
+  generalize Int.eq_dec Int64.eq_dec; intro.
   assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
   decide equality.
 Defined.
 
 Definition beq_operation: forall (x y: operation), bool.
-  generalize Int.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec  eq_condition; boolean_equality.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec ident_eq Float.eq_dec Float32.eq_dec  eq_condition; boolean_equality.
 Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
@@ -150,7 +183,7 @@ Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intro.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec ident_eq; intro.
   decide equality.
 Defined.
 
@@ -173,6 +206,10 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2)
   | Cmaskzero n, v1 :: nil => Val.maskzero_bool v1 n
   | Cmasknotzero n, v1 :: nil => option_map negb (Val.maskzero_bool v1 n)
+  | Ccompl c, v1 :: v2 :: nil => Val.cmpl_bool c v1 v2
+  | Ccomplu c, v1 :: v2 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 v2
+  | Ccomplimm c n, v1 :: nil => Val.cmpl_bool c v1 (Vlong n)
+  | Ccompluimm c n, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong n)
   | _, _ => None
   end.
 
@@ -219,6 +256,33 @@ Definition eval_operation
   | Orolm amount mask, v1::nil => Some (Val.rolm v1 amount mask)
   | Oroli amount mask, v1::v2::nil =>
       Some(Val.or (Val.and v1 (Vint (Int.not mask))) (Val.rolm v2 amount mask))
+  | Olongconst n, nil => Some (Vlong n)
+  | Ocast32signed, v1::nil => Some (Val.longofint v1)
+  | Ocast32unsigned, v1::nil => Some (Val.longofintu v1)
+  | Oaddl, v1::v2::nil => Some (Val.addl v1 v2)
+  | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n))
+  | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
+  | Onegl, v1::nil => Some (Val.negl v1)
+  | Omull, v1::v2::nil => Some (Val.mull v1 v2)
+  | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2)
+  | Omullhu, v1::v2::nil => Some (Val.mullhu v1 v2)
+  | Odivl, v1::v2::nil => Val.divls v1 v2
+  | Odivlu, v1::v2::nil => Val.divlu v1 v2
+  | Oandl, v1::v2::nil => Some(Val.andl v1 v2)
+  | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n))
+  | Oorl, v1::v2::nil => Some(Val.orl v1 v2)
+  | Oorlimm n, v1::nil => Some (Val.orl v1 (Vlong n))
+  | Oxorl, v1::v2::nil => Some(Val.xorl v1 v2)
+  | Oxorlimm n, v1::nil => Some (Val.xorl v1 (Vlong n))
+  | Onotl, v1::nil => Some(Val.notl v1)
+  | Oshll, v1::v2::nil => Some (Val.shll v1 v2)
+  | Oshrl, v1::v2::nil => Some (Val.shrl v1 v2)
+  | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n))
+  | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n)
+  | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2)
+  | Orolml amount mask, v1::nil => Some (Val.rolml v1 amount mask)
+  | Olongoffloat, v1::nil => Val.longoffloat v1
+  | Ofloatoflong, v1::nil => Val.floatoflong v1
   | Onegf, v1::nil => Some(Val.negf v1)
   | Oabsf, v1::nil => Some(Val.absf v1)
   | Oaddf, v1::v2::nil => Some(Val.addf v1 v2)
@@ -295,6 +359,10 @@ Definition type_of_condition (c: condition) : list typ :=
   | Cnotcompf _ => Tfloat :: Tfloat :: nil
   | Cmaskzero _ => Tint :: nil
   | Cmasknotzero _ => Tint :: nil
+  | Ccompl _ => Tlong :: Tlong :: nil
+  | Ccomplu _ => Tlong :: Tlong :: nil
+  | Ccomplimm _ _ => Tlong :: nil
+  | Ccompluimm _ _ => Tlong :: nil
   end.
 
 Definition type_of_operation (op: operation) : list typ * typ :=
@@ -337,6 +405,33 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oshru => (Tint :: Tint :: nil, Tint)
   | Orolm _ _ => (Tint :: nil, Tint)
   | Oroli _ _ => (Tint :: Tint :: nil, Tint)
+  | Olongconst _ => (nil, Tlong)
+  | Ocast32signed => (Tint :: nil, Tlong)
+  | Ocast32unsigned => (Tint :: nil, Tlong)
+  | Oaddl => (Tlong :: Tlong :: nil, Tlong)
+  | Oaddlimm _ => (Tlong :: nil, Tlong)
+  | Osubl => (Tlong :: Tlong :: nil, Tlong)
+  | Onegl => (Tlong :: nil, Tlong)
+  | Omull => (Tlong :: Tlong :: nil, Tlong)
+  | Omullhs => (Tlong :: Tlong :: nil, Tlong)
+  | Omullhu => (Tlong :: Tlong :: nil, Tlong)
+  | Odivl => (Tlong :: Tlong :: nil, Tlong)
+  | Odivlu => (Tlong :: Tlong :: nil, Tlong)
+  | Oandl => (Tlong :: Tlong :: nil, Tlong)
+  | Oandlimm _ => (Tlong :: nil, Tlong)
+  | Oorl => (Tlong :: Tlong :: nil, Tlong)
+  | Oorlimm _ => (Tlong :: nil, Tlong)
+  | Oxorl => (Tlong :: Tlong :: nil, Tlong)
+  | Oxorlimm _ => (Tlong :: nil, Tlong)
+  | Onotl => (Tlong :: nil, Tlong)
+  | Oshll => (Tlong :: Tint :: nil, Tlong)
+  | Oshrl => (Tlong :: Tint :: nil, Tlong)
+  | Oshrlimm _ => (Tlong :: nil, Tlong)
+  | Oshrxlimm _ => (Tlong :: nil, Tlong)
+  | Oshrlu => (Tlong :: Tint :: nil, Tlong)
+  | Orolml _ _ => (Tlong :: nil, Tlong)
+  | Olongoffloat => (Tfloat :: nil, Tlong)
+  | Ofloatoflong => (Tlong :: nil, Tfloat)
   | Onegf => (Tfloat :: nil, Tfloat)
   | Oabsf => (Tfloat :: nil, Tfloat)
   | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat)
@@ -428,6 +523,35 @@ Proof with (try exact I; try reflexivity).
   destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
   destruct v0...
   destruct v0; destruct v1...
+  exact I.
+  destruct v0...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1; simpl in *; inv H0.
+    destruct (Int64.eq i0 Int64.zero
+         || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2...
+  destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0...
+  destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
+  destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
+  destruct v0; simpl... destruct (Int.ltu i Int64.iwordsize')...
+  destruct v0; simpl in *; inv H0. destruct (Int.ltu i (Int.repr 63)); inv H2...
+  destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
+  destruct v0...
+  destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2...
+  destruct v0; simpl in H0; inv H0...
   destruct v0...
   destruct v0...
   destruct v0; destruct v1...
@@ -491,6 +615,10 @@ Definition negate_condition (cond: condition): condition :=
   | Cnotcompf c => Ccompf c
   | Cmaskzero n => Cmasknotzero n
   | Cmasknotzero n => Cmaskzero n
+  | Ccompl c => Ccompl(negate_comparison c)
+  | Ccomplu c => Ccomplu(negate_comparison c)
+  | Ccomplimm c n => Ccomplimm (negate_comparison c) n
+  | Ccompluimm c n => Ccompluimm (negate_comparison c) n
   end.
 
 Lemma eval_negate_condition:
@@ -506,6 +634,10 @@ Proof.
   repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0); auto. destruct b; auto.
   repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.maskzero_bool v i) as [[]|]; auto.
+  repeat (destruct vl; auto). apply Val.negate_cmpl_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmplu_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpl_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmplu_bool.
 Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
@@ -571,7 +703,7 @@ Lemma eval_offset_addressing:
   eval_addressing ge sp addr args = Some v ->
   eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))).
 Proof.
-  intros. 
+  intros.
   assert (D: Ptrofs.repr delta = Ptrofs.of_int (Int.repr delta)) by (symmetry; auto with ptrofs).
   destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
 - rewrite Val.add_assoc; auto.
@@ -599,6 +731,8 @@ Definition op_depends_on_memory (op: operation) : bool :=
   match op with
   | Ocmp (Ccompu _) => true
   | Ocmp (Ccompuimm _ _) => true
+  | Ocmp (Ccomplu _) => Archi.ppc64
+  | Ocmp (Ccompluimm _ _) => Archi.ppc64
   | _ => false
   end.
 
@@ -736,6 +870,10 @@ Proof.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; try discriminate; auto.
   inv H3; try discriminate; auto.
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+  inv H3; inv H2; simpl in H0; inv H0; auto.
+  inv H3; try discriminate; auto.
+  inv H3; try discriminate; auto.
 Qed.
 
 Ltac TrivialExists :=
@@ -773,7 +911,7 @@ Proof.
     destruct (Int.eq i0 Int.zero
          || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
   inv H4; inv H3; simpl in H1; inv H1. simpl.
-    destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
+  destruct (Int.eq i0 Int.zero); inv H2. TrivialExists.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto.
@@ -796,6 +934,36 @@ Proof.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
+    destruct (Int64.eq i0 Int64.zero
+         || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. TrivialExists.
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
+    destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  inv H4; simpl; auto. destruct (Int.ltu i Int64.iwordsize'); auto.
+  inv H4; simpl in *; inv H1. destruct (Int.ltu i (Int.repr 63)); inv H2. econstructor; eauto.
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  inv H4; simpl; auto.
+  inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2.
+  exists (Vlong i); auto.
+  inv H4; simpl in H1; inv H1; simpl. TrivialExists.
+  inv H4; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
@@ -993,7 +1161,7 @@ Proof.
   rewrite eval_shift_stack_addressing.
   eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
   intros. apply symbol_address_inject.
-  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 Lemma eval_operation_inject:
@@ -1013,7 +1181,7 @@ Proof.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
   intros. apply symbol_address_inject.
-  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 End EVAL_INJECT.
@@ -1042,14 +1210,14 @@ End EVAL_INJECT.
 *)
 
 Inductive rlw_state: Type :=
-  | RLW_S0 : rlw_state
-  | RLW_S1 : rlw_state
-  | RLW_S2 : rlw_state
-  | RLW_S3 : rlw_state
-  | RLW_S4 : rlw_state
-  | RLW_S5 : rlw_state
-  | RLW_S6 : rlw_state
-  | RLW_Sbad : rlw_state.
+  | RLW_S0
+  | RLW_S1
+  | RLW_S2
+  | RLW_S3
+  | RLW_S4
+  | RLW_S5
+  | RLW_S6
+  | RLW_Sbad.
 
 Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state :=
   match s, b with
@@ -1082,13 +1250,71 @@ Definition rlw_accepting (s: rlw_state) : bool :=
   | RLW_Sbad => false
   end.
 
-Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool :=
+Fixpoint is_mask_rec {A: Type} (trans: A -> bool -> A) (accept: A -> bool)
+                     (n: nat) (s: A) (x: Z) {struct n} : bool :=
   match n with
   | O =>
-      rlw_accepting s
+      accept s
   | S m =>
-      is_rlw_mask_rec m (rlw_transition s (Z.odd x)) (Z.div2 x)
+      is_mask_rec trans accept m (trans s (Z.odd x)) (Z.div2 x)
   end.
 
 Definition is_rlw_mask (x: int) : bool :=
-  is_rlw_mask_rec Int.wordsize RLW_S0 (Int.unsigned x).
+  is_mask_rec rlw_transition rlw_accepting Int.wordsize RLW_S0 (Int.unsigned x).
+
+(** For the 64-bit [rldicl] and [rldicr] instructions, the acceptable
+  masks are [1111100000] and [0000011111], that is, some ones in the
+  high bits and some zeroes in the low bits, or conversely.  All ones
+  is OK, but not all zeroes.  The corresponding automata are:
+<<
+      0          1
+     / \        / \
+     \ /        \ /          (accepting: [1])
+     [0] --1--> [1]
+
+
+                 1          0
+                / \        / \
+                \ /        \ /      (accepting: [1], [2])
+     [0] --1--> [1] --0--> [2]
+>>
+*)
+
+Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_Sbad.
+
+Definition rll_transition (s: rll_state) (b: bool) : rll_state :=
+  match s, b with
+  | RLL_S0, false => RLL_S0
+  | RLL_S0, true => RLL_S1
+  | RLL_S1, true => RLL_S1
+  | _, _ => RLL_Sbad
+  end.
+
+Definition rll_accepting (s: rll_state) : bool :=
+  match s with
+  | RLL_S1 => true
+  | _ => false
+  end.
+
+Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_S2 | RLR_Sbad.
+
+Definition rlr_transition (s: rlr_state) (b: bool) : rlr_state :=
+  match s, b with
+  | RLR_S0, true => RLR_S1
+  | RLR_S1, false => RLR_S2
+  | RLR_S1, true => RLR_S1
+  | RLR_S2, false => RLR_S2
+  | _, _ => RLR_Sbad
+  end.
+
+Definition rlr_accepting (s: rlr_state) : bool :=
+  match s with
+  | RLR_S1 | RLR_S2 => true
+  | _ => false
+  end.
+
+Definition is_rldl_mask (x: int64) : bool :=    (*r 0s in the high bits, 1s in the low bits *)
+  is_mask_rec rll_transition rll_accepting Int64.wordsize RLL_S0 (Int64.unsigned x).
+
+Definition is_rldr_mask (x: int64) : bool :=    (*r 1s in the high bits, 0s in the low bits *)
+  is_mask_rec rlr_transition rlr_accepting Int64.wordsize RLR_S0 (Int64.unsigned x).