Improve code generation for 64-bit signed integer division

Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port.

Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.

7 files changed, 256 insertions, 132 deletions

diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index d708afb7..1fc0b689 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -14,12 +14,8 @@
 
 Require Import Coqlib.
 Require Import Compopts.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Op.
-Require Import CminorSel.
-Require Import SelectOp.
+Require Import AST Integers Floats.
+Require Import Op CminorSel SelectOp SplitLong SelectLong.
 
 Open Local Scope cminorsel_scope.
 
@@ -201,6 +197,63 @@ Nondetfunction mods (e1: expr) (e2: expr) :=
   | _ => mods_base e1 e2
   end.
 
+(** 64-bit integer divisions *)
+
+Section SELECT.
+
+Context {hf: helper_functions}.
+
+Definition modl_from_divl (equo: expr) (n: int64) :=
+  subl (Eletvar O) (mullimm n equo).
+
+Definition divlu (e1 e2: expr) :=
+  match is_longconst e2, is_longconst e1 with
+  | Some n2, Some n1 => longconst (Int64.divu n1 n2)
+  | Some n2, _ =>
+      match Int64.is_power2' n2 with
+      | Some l => shrluimm e1 l
+      | None   => divlu_base e1 e2
+      end (* TODO: multiply-high *)
+  | _, _ => divlu_base e1 e2
+  end.
+
+Definition modlu (e1 e2: expr) :=
+  match is_longconst e2, is_longconst e1 with
+  | Some n2, Some n1 => longconst (Int64.modu n1 n2)
+  | Some n2, _ =>
+      match Int64.is_power2 n2 with
+      | Some l => andl e1 (longconst (Int64.sub n2 Int64.one))
+      | None   => modlu_base e1 e2
+      end
+  | _, _ => modlu_base e1 e2
+  end.
+
+Definition divls (e1 e2: expr) :=
+  match is_longconst e2, is_longconst e1 with
+  | Some n2, Some n1 => longconst (Int64.divs n1 n2)
+  | Some n2, _ =>
+      match Int64.is_power2' n2 with
+      | Some l => if Int.ltu l (Int.repr 63) then shrxlimm e1 l else divls_base e1 e2
+      | None   => divls_base e1 e2
+      end (* TODO: multiply-high *)
+  | _, _ => divls_base e1 e2
+  end.
+
+Definition modls (e1 e2: expr) :=
+  match is_longconst e2, is_longconst e1 with
+  | Some n2, Some n1 => longconst (Int64.mods n1 n2)
+  | Some n2, _ =>
+      match Int64.is_power2' n2 with
+      | Some l => if Int.ltu l (Int.repr 63)
+                  then Elet e1 (modl_from_divl (shrxlimm (Eletvar O) l) n2)
+                  else modls_base e1 e2
+      | None   => modls_base e1 e2
+      end
+  | _, _ => modls_base e1 e2
+  end.
+
+End SELECT.
+
 (** Floating-point division by a constant can also be turned into a FP
     multiplication by the inverse constant, but only for powers of 2. *)
 
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index 5621acd5..441f69b1 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -15,7 +15,7 @@
 Require Import Zquot Coqlib.
 Require Import AST Integers Floats Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
-Require Import SelectOp SelectOpproof SelectDiv.
+Require Import SelectOp SelectOpproof SplitLong SplitLongproof SelectLong SelectLongproof SelectDiv.
 
 Open Local Scope cminorsel_scope.
 
@@ -321,7 +321,10 @@ Qed.
 
 Section CMCONSTRS.
 
-Variable ge: genv.
+Variable prog: program.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared prog hf.
+Let ge := Genv.globalenv prog.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
@@ -543,6 +546,118 @@ Proof.
 - eapply eval_mods_base; eauto.
 Qed.
 
+Lemma eval_modl_from_divl:
+  forall le a n x y,
+  eval_expr ge sp e m le a (Vlong y) ->
+  nth_error le O = Some (Vlong x) ->
+  eval_expr ge sp e m le (modl_from_divl a n) (Vlong (Int64.sub x (Int64.mul y n))).
+Proof.
+  unfold modl_from_divl; intros.
+  exploit eval_mullimm; eauto. instantiate (1 := n). intros (v1 & A1 & B1).
+  exploit (eval_subl prog sp e m le (Eletvar O)). constructor; eauto. eexact A1.
+  intros (v2 & A2 & B2).
+  simpl in B1; inv B1. simpl in B2; inv B2. exact A2.
+Qed.
+
+Theorem eval_divlu:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.divlu x y = Some z ->
+  exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v.
+Proof.
+  unfold divlu; intros.
+  destruct (is_longconst b) as [n2|] eqn:N2.
+- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y.
+  destruct (is_longconst a) as [n1|] eqn:N1.
++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x.
+  simpl in H1. destruct (Int64.eq n2 Int64.zero); inv H1.
+  econstructor; split. apply eval_longconst. constructor.
++ destruct (Int64.is_power2' n2) as [l|] eqn:POW.
+* exploit Val.divlu_pow2; eauto. intros EQ; subst z. apply eval_shrluimm; auto.
+* eapply eval_divlu_base; eauto.     
+- eapply eval_divlu_base; eauto.
+Qed.
+
+Theorem eval_modlu:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.modlu x y = Some z ->
+  exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v.
+Proof.
+  unfold modlu; intros.
+  destruct (is_longconst b) as [n2|] eqn:N2.
+- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y.
+  destruct (is_longconst a) as [n1|] eqn:N1.
++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x.
+  simpl in H1. destruct (Int64.eq n2 Int64.zero); inv H1.
+  econstructor; split. apply eval_longconst. constructor.
++ destruct (Int64.is_power2 n2) as [l|] eqn:POW.
+* exploit Val.modlu_pow2; eauto. intros EQ; subst z. eapply eval_andl; eauto. apply eval_longconst.
+* eapply eval_modlu_base; eauto.     
+- eapply eval_modlu_base; eauto.
+Qed.
+
+Theorem eval_divls:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.divls x y = Some z ->
+  exists v, eval_expr ge sp e m le (divls a b) v /\ Val.lessdef z v.
+Proof.
+  unfold divls; intros.
+  destruct (is_longconst b) as [n2|] eqn:N2.
+- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y.
+  destruct (is_longconst a) as [n1|] eqn:N1.
++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x.
+  simpl in H1. 
+  destruct (Int64.eq n2 Int64.zero
+         || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1.
+  econstructor; split. apply eval_longconst. constructor.
++ destruct (Int64.is_power2' n2) as [l|] eqn:POW.
+* destruct (Int.ltu l (Int.repr 63)) eqn:LT.
+** exploit Val.divls_pow2; eauto. intros EQ. eapply eval_shrxlimm; eauto.
+** eapply eval_divls_base; eauto.  
+* eapply eval_divls_base; eauto.     
+- eapply eval_divls_base; eauto.
+Qed.
+
+Theorem eval_modls:
+  forall le a b x y z,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  Val.modls x y = Some z ->
+  exists v, eval_expr ge sp e m le (modls a b) v /\ Val.lessdef z v.
+Proof.
+  unfold modls; intros.
+  destruct (is_longconst b) as [n2|] eqn:N2.
+- assert (y = Vlong n2) by (eapply is_longconst_sound; eauto). subst y.
+  destruct (is_longconst a) as [n1|] eqn:N1.
++ assert (x = Vlong n1) by (eapply is_longconst_sound; eauto). subst x.
+  simpl in H1. 
+  destruct (Int64.eq n2 Int64.zero
+         || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); inv H1.
+  econstructor; split. apply eval_longconst. constructor.
++ destruct (Int64.is_power2' n2) as [l|] eqn:POW.
+* destruct (Int.ltu l (Int.repr 63)) eqn:LT.
+**destruct x; simpl in H1; try discriminate.
+  destruct (Int64.eq n2 Int64.zero
+         || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone) eqn:D; inv H1.
+  assert (Val.divls (Vlong i) (Vlong n2) = Some (Vlong (Int64.divs i n2))).
+  { simpl; rewrite D; auto. }
+  exploit Val.divls_pow2; eauto. intros EQ.
+  set (le' := Vlong i :: le).
+  assert (A: eval_expr ge sp e m le' (Eletvar O) (Vlong i)) by (constructor; auto).
+  exploit eval_shrxlimm; eauto. intros (v1 & A1 & B1). inv B1.
+  econstructor; split.
+  econstructor. eauto. eapply eval_modl_from_divl. eexact A1. reflexivity.      
+  rewrite Int64.mods_divs. auto.
+**eapply eval_modls_base; eauto.
+* eapply eval_modls_base; eauto.     
+- eapply eval_modls_base; eauto.
+Qed.
+
 (** * Floating-point division *)
 
 Theorem eval_divf:
diff --git a/backend/Selection.v b/backend/Selection.v
index 3aff446e..5cb5d119 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -27,7 +27,7 @@ Require Import Coqlib Maps.
 Require Import AST Errors Integers Globalenvs Switch.
 Require Cminor.
 Require Import Op CminorSel.
-Require Import SelectOp SelectDiv SplitLong SelectLong.
+Require Import SelectOp SplitLong SelectLong SelectDiv.
 Require Machregs.
 
 Local Open Scope cminorsel_scope.
@@ -138,9 +138,9 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Oaddl => addl arg1 arg2
   | Cminor.Osubl => subl arg1 arg2
   | Cminor.Omull => mull arg1 arg2
-  | Cminor.Odivl => divl arg1 arg2
+  | Cminor.Odivl => divls arg1 arg2
   | Cminor.Odivlu => divlu arg1 arg2
-  | Cminor.Omodl => modl arg1 arg2
+  | Cminor.Omodl => modls arg1 arg2
   | Cminor.Omodlu => modlu arg1 arg2
   | Cminor.Oandl => andl arg1 arg2
   | Cminor.Oorl => orl arg1 arg2
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 34157553..90e50338 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -305,9 +305,9 @@ Proof.
   eapply eval_addl; eauto.
   eapply eval_subl; eauto.
   eapply eval_mull; eauto.
-  eapply eval_divl; eauto.
+  eapply eval_divls; eauto.
   eapply eval_divlu; eauto.
-  eapply eval_modl; eauto.
+  eapply eval_modls; eauto.
   eapply eval_modlu; eauto.
   eapply eval_andl; eauto.
   eapply eval_orl; eauto.
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index 305e20f3..5891adef 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -255,38 +255,17 @@ Definition mull (e1 e2: expr) :=
   | _, _ => mull_base e1 e2
   end.
 
-Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) :=
-  match is_longconst e1, is_longconst e2 with
-  | Some n1, Some n2 => longconst (sem n1 n2)
-  | _, _ => Eexternal id sig_ll_l (e1 ::: e2 ::: Enil)
-  end.
-
-Definition divl e1 e2 := binop_long i64_sdiv Int64.divs e1 e2.
-Definition modl e1 e2 := binop_long i64_smod Int64.mods e1 e2.
-
-Definition divlu (e1 e2: expr) :=
-  let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in
-  match is_longconst e1, is_longconst e2 with
-  | Some n1, Some n2 => longconst (Int64.divu n1 n2)
-  | _, Some n2 =>
-      match Int64.is_power2' n2 with
-      | Some l => shrluimm e1 l
-      | None   => default
-      end
-  | _, _ => default
-  end.
-
-Definition modlu (e1 e2: expr) :=
-  let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in
-  match is_longconst e1, is_longconst e2 with
-  | Some n1, Some n2 => longconst (Int64.modu n1 n2)
-  | _, Some n2 =>
-      match Int64.is_power2 n2 with
-      | Some l => andl e1 (longconst (Int64.sub n2 Int64.one))
-      | None   => default
-      end
-  | _, _ => default
-  end.
+Definition shrxlimm (e: expr) (n: int) :=
+  if Int.eq n Int.zero then e else
+    Elet e (shrlimm (addl (Eletvar O)
+                          (shrluimm (shrlimm (Eletvar O) (Int.repr 63))
+                                    (Int.sub (Int.repr 64) n)))
+                    n).
+
+Definition divlu_base (e1 e2: expr) := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil).
+Definition modlu_base (e1 e2: expr) := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil).
+Definition divls_base (e1 e2: expr) := Eexternal i64_sdiv sig_ll_l (e1 ::: e2 ::: Enil).
+Definition modls_base (e1 e2: expr) := Eexternal i64_smod sig_ll_l (e1 ::: e2 ::: Enil).
 
 Definition cmpl_eq_zero (e: expr) :=
   splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)).
diff --git a/backend/SplitLongproof.v b/backend/SplitLongproof.v
index 1dbe25bd..57fc6b56 100644
--- a/backend/SplitLongproof.v
+++ b/backend/SplitLongproof.v
@@ -823,118 +823,79 @@ Proof.
 - apply eval_mull_base; auto.
 Qed.
 
-Lemma eval_binop_long:
-  forall id name sem le a b x y z,
-  (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) ->
-  helper_declared prog id name sig_ll_l ->
-  external_implements name sig_ll_l (x::y::nil) z ->
+Theorem eval_shrxlimm:
+  forall le a n x z,
+  Archi.ptr64 = false ->
   eval_expr ge sp e m le a x ->
-  eval_expr ge sp e m le b y ->
-  exists v, eval_expr ge sp e m le (binop_long id sem a b) v /\ Val.lessdef z v.
+  Val.shrxl x (Vint n) = Some z ->
+  exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold binop_long.
-  destruct (is_longconst a) as [p|] eqn:LC1.
-  destruct (is_longconst b) as [q|] eqn:LC2.
-  exploit is_longconst_sound. eexact LC1. eauto. intros EQ; subst x.
-  exploit is_longconst_sound. eexact LC2. eauto. intros EQ; subst y.
-  econstructor; split. EvalOp. erewrite H by eauto. rewrite Int64.ofwords_recompose. auto.
-  econstructor; split. eapply eval_helper_2; eauto. auto.
-  econstructor; split. eapply eval_helper_2; eauto. auto.
+  intros.
+  apply Val.shrxl_shrl_2 in H1. unfold shrxlimm.
+  destruct (Int.eq n Int.zero).
+- subst z; exists x; auto.
+- set (le' := x :: le).
+  edestruct (eval_shrlimm (Int.repr 63) le' (Eletvar O)) as (v1 & A1 & B1).
+  constructor. reflexivity.
+  edestruct (eval_shrluimm (Int.sub (Int.repr 64) n) le') as (v2 & A2 & B2).
+  eexact A1.
+  edestruct (eval_addl H le' (Eletvar 0)) as (v3 & A3 & B3).
+  constructor. reflexivity. eexact A2.
+  edestruct (eval_shrlimm n le') as (v4 & A4 & B4). eexact A3.
+  exists v4; split.
+  econstructor; eauto.
+  assert (X: forall v1 v2 n, Val.lessdef v1 v2 -> Val.lessdef (Val.shrl v1 (Vint n)) (Val.shrl v2 (Vint n))).
+  { intros. inv H2; auto. }
+  assert (Y: forall v1 v2 n, Val.lessdef v1 v2 -> Val.lessdef (Val.shrlu v1 (Vint n)) (Val.shrlu v2 (Vint n))).
+  { intros. inv H2; auto. }
+  subst z. eapply Val.lessdef_trans; [|eexact B4]. apply X.
+  eapply Val.lessdef_trans; [|eexact B3]. apply Val.addl_lessdef; auto.
+  eapply Val.lessdef_trans; [|eexact B2]. apply Y.
+  auto.
 Qed.
 
-Theorem eval_divl:
+Theorem eval_divlu_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
-  Val.divls x y = Some z ->
-  exists v, eval_expr ge sp e m le (divl a b) v /\ Val.lessdef z v.
+  Val.divlu x y = Some z ->
+  exists v, eval_expr ge sp e m le (divlu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. eapply eval_binop_long; eauto.
-  intros; subst; simpl in H1.
-  destruct (Int64.eq q Int64.zero
-         || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1.
-  auto.
-  DeclHelper. UseHelper.
+  intros; unfold divlu_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
-Theorem eval_modl:
+Theorem eval_modlu_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
-  Val.modls x y = Some z ->
-  exists v, eval_expr ge sp e m le (modl a b) v /\ Val.lessdef z v.
+  Val.modlu x y = Some z ->
+  exists v, eval_expr ge sp e m le (modlu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. eapply eval_binop_long; eauto.
-  intros; subst; simpl in H1.
-  destruct (Int64.eq q Int64.zero
-         || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1.
-  auto.
-  DeclHelper. UseHelper.
+  intros; unfold modlu_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
-Theorem eval_divlu:
+Theorem eval_divsu_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
-  Val.divlu x y = Some z ->
-  exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v.
+  Val.divls x y = Some z ->
+  exists v, eval_expr ge sp e m le (divls_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divlu.
-  set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)).
-  assert (DEFAULT:
-    exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v).
-  {
-    econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
-  }
-  destruct (is_longconst a) as [p|] eqn:LC1;
-  destruct (is_longconst b) as [q|] eqn:LC2.
-- exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
-  exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
-  econstructor; split. apply eval_longconst.
-  simpl in H1. destruct (Int64.eq q Int64.zero); inv H1. auto.
-- auto.
-- destruct (Int64.is_power2' q) as [l|] eqn:P2; auto.
-  exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
-  replace z with (Val.shrlu x (Vint l)).
-  apply eval_shrluimm. auto.
-  destruct x; simpl in H1; try discriminate.
-  destruct (Int64.eq q Int64.zero); inv H1.
-  simpl. erewrite Int64.is_power2'_range by eauto.
-  erewrite Int64.divu_pow2' by eauto.
-  auto.
-- auto.
+  intros; unfold divls_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
-Theorem eval_modlu:
+Theorem eval_modls_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
-  Val.modlu x y = Some z ->
-  exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v.
+  Val.modls x y = Some z ->
+  exists v, eval_expr ge sp e m le (modls_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold modlu.
-  set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)).
-  assert (DEFAULT:
-    exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v).
-  {
-    econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
-  }
-  destruct (is_longconst a) as [p|] eqn:LC1;
-  destruct (is_longconst b) as [q|] eqn:LC2.
-- exploit (is_longconst_sound le a); eauto. intros EQ; subst x.
-  exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
-  econstructor; split. apply eval_longconst.
-  simpl in H1. destruct (Int64.eq q Int64.zero); inv H1. auto.
-- auto.
-- destruct (Int64.is_power2 q) as [l|] eqn:P2; auto.
-  exploit (is_longconst_sound le b); eauto. intros EQ; subst y.
-  replace z with (Val.andl x (Vlong (Int64.sub q Int64.one))).
-  apply eval_andl. auto. apply eval_longconst.
-  destruct x; simpl in H1; try discriminate.
-  destruct (Int64.eq q Int64.zero); inv H1.
-  simpl.
-  erewrite Int64.modu_and by eauto. auto.
-- auto.
+  intros; unfold modls_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 Remark decompose_cmpl_eq_zero:
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 6b314904..bf88a450 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1938,6 +1938,22 @@ Proof.
   inv H; inv H0; auto with va. simpl. rewrite E. constructor.
 Qed.
 
+Definition shrxl (v w: aval) :=
+  match v, w with
+  | L i, I j => if Int.ltu j (Int.repr 63) then L(Int64.shrx' i j) else ntop
+  | _, _ => ntop1 v
+  end.
+
+Lemma shrxl_sound:
+  forall v w u x y, vmatch v x -> vmatch w y -> Val.shrxl v w = Some u -> vmatch u (shrxl x y).
+Proof.
+  intros.
+  destruct v; destruct w; try discriminate; simpl in H1.
+  destruct (Int.ltu i0 (Int.repr 63)) eqn:LTU; inv H1.
+  unfold shrxl; inv H; auto with va; inv H0; auto with va.
+  rewrite LTU; auto with va.
+Qed.
+
 (** Floating-point arithmetic operations *)
 
 Definition negf := unop_float Float.neg.
@@ -4544,7 +4560,7 @@ Hint Resolve cnot_sound symbol_address_sound
        shll_sound shrl_sound shrlu_sound
        andl_sound orl_sound xorl_sound notl_sound roll_sound rorl_sound
        negl_sound addl_sound subl_sound mull_sound
-       divls_sound divlu_sound modls_sound modlu_sound
+       divls_sound divlu_sound modls_sound modlu_sound shrxl_sound
        negf_sound absf_sound
        addf_sound subf_sound mulf_sound divf_sound
        negfs_sound absfs_sound