Constprop strength reduction (#17)

PowerPC port: add strength reduction for 64-bit operations

* Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748)
* Moved shru_rolml proof to Values.

3 files changed, 304 insertions, 16 deletions

diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 886655a0..0ed92e90 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -50,6 +50,14 @@ Nondetfunction cond_strength_reduction
       (Ccompuimm (swap_comparison c) n1, r2 :: nil)
   | Ccompu c, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Ccompuimm c n2, r1 :: nil)
+  | Ccompl c, r1 :: r2 :: nil, L n1 :: v2 :: nil =>
+      (Ccomplimm (swap_comparison c) n1, r2 :: nil)
+  | Ccompl c, r1 :: r2 :: nil, v1 :: L n2 :: nil =>
+      (Ccomplimm c n2, r1 :: nil)
+  | Ccomplu c, r1 :: r2 :: nil, L n1 :: v2 :: nil =>
+      (Ccompluimm (swap_comparison c) n1, r2 :: nil)
+  | Ccomplu c, r1 :: r2 :: nil, v1 :: L n2 :: nil =>
+      (Ccompluimm c n2, r1 :: nil)
   | _, _, _ =>
       (cond, args)
   end.
@@ -147,6 +155,77 @@ Definition make_xorimm (n: int) (r: reg) :=
   else if Int.eq n Int.mone then (Onot, r :: nil)
   else (Oxorimm n, r :: nil).
 
+Definition make_shllimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then (Omove, r1 :: nil)
+  else if Int.ltu n Int64.iwordsize' then
+    let n' := Int64.repr (Int.unsigned n) in
+    (Orolml n (Int64.shl Int64.mone n'), r1::nil)
+  else (Oshll, r1 :: r2 :: nil).
+
+Definition make_shrlimm (n: int) (r1 r2: reg) :=
+  if Int.eq n Int.zero then (Omove, r1 :: nil)
+  else (Oshrl, r1 :: r2 :: nil).
+
+Definition make_shrluimm_aux (n: int) (r1: reg) :=
+  if Int.eq n Int.zero then
+    (Omove, r1 :: nil)
+  else
+    let n' := Int64.repr (Int.unsigned n) in
+    (Orolml (Int.sub Int64.iwordsize' n) (Int64.shru Int64.mone n'), r1 :: nil).
+
+Definition make_shrluimm (n: int) (r1 r2: reg) :=
+  if Int.ltu n Int64.iwordsize' then
+    make_shrluimm_aux n r1
+  else
+    (Oshrlu, r1 :: r2 :: nil).
+
+Definition make_addlimm (n: int64) (r: reg) :=
+  if Int64.eq n Int64.zero
+  then (Omove, r :: nil)
+  else (Oaddlimm n, r :: nil).
+
+Definition make_mullimm (n: int64) (r1 r2: reg) :=
+  if Int64.eq n Int64.zero then
+    (Olongconst Int64.zero, nil)
+  else if Int64.eq n Int64.one then
+    (Omove, r1 :: nil)
+  else
+    match Int64.is_power2' n with
+    | Some l =>
+       let l' := Int64.repr (Int.unsigned l) in
+       (Orolml l (Int64.shl Int64.mone l'), r1 :: nil)
+    | None => (Omull, r1 :: r2 :: nil)
+    end.
+
+Definition make_andlimm (n: int64) (r: reg) (a: aval) :=
+  if Int64.eq n Int64.zero then (Olongconst Int64.zero, nil)
+  else if Int64.eq n Int64.mone then (Omove, r :: nil)
+  else (Oandlimm n, r :: nil).
+
+Definition make_orlimm (n: int64) (r: reg) :=
+  if Int64.eq n Int64.zero then (Omove, r :: nil)
+  else if Int64.eq n Int64.mone then (Olongconst Int64.mone, nil)
+  else (Oorlimm n, r :: nil).
+
+Definition make_xorlimm (n: int64) (r: reg) :=
+  if Int64.eq n Int64.zero then (Omove, r :: nil)
+  else if Int64.eq n Int64.mone then (Onotl, r :: nil)
+  else (Oxorlimm n, r :: nil).
+
+Definition make_divlimm n (r1 r2: reg) :=
+  match Int64.is_power2' n with
+  | Some l => if Int.ltu l (Int.repr 63)
+              then (Oshrxlimm l, r1 :: nil)
+              else (Odivl, r1 :: r2 :: nil)
+  | None   => (Odivl, r1 :: r2 :: nil)
+  end.
+
+Definition make_divluimm n (r1 r2: reg) :=
+  match Int64.is_power2' n with
+  | Some l => make_shrluimm_aux l r1
+  | None   => (Odivlu, r1 :: r2 :: nil)
+  end.
+
 Definition make_mulfimm (n: float) (r r1 r2: reg) :=
   if Float.eq_dec n (Float.of_int (Int.repr 2))
   then (Oaddf, r :: r :: nil)
@@ -187,6 +266,23 @@ Nondetfunction op_strength_reduction
   | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2
   | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2
   | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2
+  | Oaddl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_addlimm n1 r2
+  | Oaddl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_addlimm n2 r1
+  | Osubl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_addlimm (Int64.neg n2) r1
+  | Omull, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_mullimm n1 r2 r1
+  | Omull, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_mullimm n2 r1 r2
+  | Odivl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divlimm n2 r1 r2
+  | Odivlu, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_divluimm n2 r1 r2
+  | Oandl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_andlimm n1 r2 v2
+  | Oandl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_andlimm n2 r1 v1
+  | Oandlimm n, r1 :: nil, v1 :: nil => make_andlimm n r1 v1
+  | Oorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_orlimm n1 r2
+  | Oorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_orlimm n2 r1
+  | Oxorl, r1 :: r2 :: nil, L n1 :: v2 :: nil => make_xorlimm n1 r2
+  | Oxorl, r1 :: r2 :: nil, v1 :: L n2 :: nil => make_xorlimm n2 r1
+  | Oshll, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shllimm n2 r1 r2
+  | Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrlimm n2 r1 r2
+  | Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrluimm n2 r1 r2
   | Ocmp c, args, vl => make_cmp c args vl
   | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2
   | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index dd39dc10..e9d091ca 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -68,6 +68,10 @@ Ltac SimplVM :=
       let E := fresh in
       assert (E: v = Vint n) by (inversion H; auto);
       rewrite E in *; clear H; SimplVM
+  | [ H: vmatch _ ?v (L ?n) |- _ ] =>
+      let E := fresh in
+      assert (E: v = Vlong n) by (inversion H; auto);
+      rewrite E in *; clear H; SimplVM
   | [ H: vmatch _ ?v (F ?n) |- _ ] =>
       let E := fresh in
       assert (E: v = Vfloat n) by (inversion H; auto);
@@ -121,6 +125,10 @@ Proof.
 - auto.
 - apply Val.swap_cmpu_bool.
 - auto.
+- apply Val.swap_cmpl_bool.
+- auto.
+- apply Val.swap_cmplu_bool.
+- auto.
 - auto.
 Qed.
 
@@ -337,6 +345,149 @@ Proof.
   econstructor; split; eauto. auto.
 Qed.
 
+Lemma make_addlimm_correct:
+  forall n r,
+  let (op, args) := make_addlimm n r in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.addl rs#r (Vlong n)) v.
+Proof.
+  intros. unfold make_addlimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
+  subst. exists (rs#r); split; auto.
+  destruct (rs#r); simpl; auto. rewrite Int64.add_zero.  auto.
+  exists (Val.addl rs#r (Vlong n)); split; auto.
+Qed.
+
+Lemma make_mullimm_correct:
+  forall n r1 r2,
+  rs#r2 = Vlong n ->
+  let (op, args) := make_mullimm n r1 r2 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mull rs#r1 (Vlong n)) v.
+Proof.
+  intros; unfold make_mullimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst.
+  exists (Vlong Int64.zero); split; auto. destruct (rs#r1); simpl; auto. rewrite Int64.mul_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.one; intros. subst.
+  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto. rewrite Int64.mul_one; auto.
+  destruct (Int64.is_power2' n) eqn:?; intros.
+  assert (Int.ltu i Int64.iwordsize' = true) by (erewrite  Int64.is_power2'_range; eauto).
+  exists (Val.shll rs#r1 (Vint i)); split; auto.
+  rewrite Val.shll_rolml by apply H2. auto.
+  destruct (rs#r1); auto. simpl. rewrite H2.
+  erewrite Int64.mul_pow2'; auto.
+  econstructor ; split; auto. simpl. congruence.
+Qed.
+
+Lemma make_shllimm_correct:
+  forall n r1 r2,
+  rs#r2 = Vint n ->
+  let (op, args) := make_shllimm n r1 r2 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shll rs#r1 (Vint n)) v.
+Proof.
+  intros; unfold make_shllimm.
+  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
+  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto.
+  unfold Int64.shl'. rewrite Z.shiftl_0_r, Int64.repr_unsigned. auto.
+  destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl.
+  rewrite Val.shll_rolml by apply LT. eauto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
+Qed.
+
+Lemma make_shrlimm_correct:
+  forall n r1 r2,
+  rs#r2 = Vint n ->
+  let (op, args) := make_shrlimm n r1 r2 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shrl rs#r1 (Vint n)) v.
+Proof.
+  intros; unfold make_shrlimm.
+  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
+  exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto.
+  unfold Int64.shr'. rewrite Z.shiftr_0_r, Int64.repr_signed. auto.
+  econstructor; split. simpl. eauto. rewrite H; auto.
+Qed.
+
+Lemma make_shrluimm_aux_correct:
+  forall n r1,
+  Int.ltu n Int64.iwordsize' = true ->
+  let (op, args) := make_shrluimm_aux n r1 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shrlu rs#r1 (Vint n)) v.
+Proof.
+  intros; unfold make_shrluimm_aux.
+  predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
+  - exists (rs#r1); split; auto. destruct (rs#r1); simpl; auto.
+  unfold Int64.shru'. rewrite Z.shiftr_0_r, Int64.repr_unsigned. auto.
+ - rewrite Val.shrlu_rolml by apply H; auto. econstructor; split; eauto. auto.
+Qed.
+
+Lemma make_shrluimm_correct:
+  forall n r1 r2,
+  rs#r2 = Vint n ->
+  let (op, args) := make_shrluimm n r1 r2 in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shrlu rs#r1 (Vint n)) v.
+Proof.
+  intros; unfold make_shrluimm.
+  destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl.
+  apply make_shrluimm_aux_correct; auto.
+  rewrite H.  eauto.
+Qed.
+
+Lemma make_andlimm_correct:
+  forall n r x,
+  let (op, args) := make_andlimm n r x in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.andl rs#r (Vlong n)) v.
+Proof.
+  intros; unfold make_andlimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
+  subst n. exists (Vlong Int64.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.and_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
+  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.and_mone; auto.
+  econstructor; split; eauto. auto.
+Qed.
+
+Lemma make_orlimm_correct:
+  forall n r,
+  let (op, args) := make_orlimm n r in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.orl rs#r (Vlong n)) v.
+Proof.
+  intros; unfold make_orlimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
+  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.or_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
+  subst n. exists (Vlong Int64.mone); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.or_mone; auto.
+  econstructor; split; eauto. auto.
+Qed.
+
+Lemma make_xorlimm_correct:
+  forall n r,
+  let (op, args) := make_xorlimm n r in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.xorl rs#r (Vlong n)) v.
+Proof.
+  intros; unfold make_xorlimm.
+  predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
+  subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int64.xor_zero; auto.
+  predSpec Int64.eq Int64.eq_spec n Int64.mone; intros.
+  subst n. exists (Val.notl rs#r); split; auto.
+  econstructor; split; eauto. auto.
+Qed.
+
+Lemma make_divluimm_correct:
+  forall n r1 r2 v,
+  Val.divlu rs#r1 rs#r2 = Some v ->
+  rs#r2 = Vlong n ->
+  let (op, args) := make_divluimm n r1 r2 in
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w.
+Proof.
+  intros; unfold make_divluimm.
+  destruct (Int64.is_power2' n) eqn:?.
+  exploit Int64.is_power2'_range; eauto. intros RANGE.
+  replace v with (Val.shrlu rs#r1 (Vint i)).
+  apply make_shrluimm_aux_correct; auto.
+  rewrite H0 in H.
+  destruct (rs#r1); simpl in *; inv H. rewrite RANGE.
+  destruct (Int64.eq n Int64.zero); inv H2.
+  rewrite (Int64.divu_pow2' i0 n i) by auto. auto.
+  exists v; auto.
+Qed.
+
 Lemma make_mulfimm_correct:
   forall n r1 r2,
   rs#r2 = Vfloat n ->
@@ -350,6 +501,20 @@ Proof.
   simpl. econstructor; split; eauto.
 Qed.
 
+Lemma make_divlimm_correct:
+  forall n r1 r2 v,
+  Val.divls rs#r1 rs#r2 = Some v ->
+  rs#r2 = Vlong n ->
+  let (op, args) := make_divlimm n r1 r2 in
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w.
+Proof.
+  intros; unfold make_divlimm.
+  destruct (Int64.is_power2' n) eqn:?. destruct (Int.ltu i (Int.repr 63)) eqn:?.
+  rewrite H0 in H. econstructor; split. simpl; eauto. eapply Val.divls_pow2; eauto. auto.
+  exists v; auto.
+  exists v; auto.
+Qed.
+
 Lemma make_mulfimm_correct_2:
   forall n r1 r2,
   rs#r1 = Vfloat n ->
@@ -470,6 +635,47 @@ Proof.
   InvApproxRegs; SimplVM; inv H0. apply make_shrimm_correct; auto.
 (* shru *)
   InvApproxRegs; SimplVM; inv H0. apply make_shruimm_correct; auto.
+(* addl *)
+  InvApproxRegs; SimplVM; inv H0.
+  change (let (op', args') := make_addlimm n1 r2 in
+          exists w : val,
+          eval_operation ge (Vptr sp Ptrofs.zero) op' rs ## args' m = Some w /\
+          Val.lessdef (Val.addl (Vlong n1) rs#r2) w).
+  rewrite Val.addl_commut. apply make_addlimm_correct.
+  InvApproxRegs; SimplVM; inv H0. apply make_addlimm_correct.
+(* subl *)
+  InvApproxRegs; SimplVM; inv H0.
+  replace (Val.subl rs#r1 (Vlong n2)) with (Val.addl rs#r1 (Vlong (Int64.neg n2))).
+  apply make_addlimm_correct; auto.
+  unfold Val.addl, Val.subl. destruct Archi.ptr64 eqn:SF, rs#r1; auto.
+  rewrite Int64.sub_add_opp; auto.
+  rewrite Ptrofs.sub_add_opp. do 2 f_equal. auto with ptrofs.
+  rewrite Int64.sub_add_opp; auto.
+(* mull *)
+  InvApproxRegs; SimplVM; inv H0. fold (Val.mull (Vlong n1) rs#r2). rewrite Val.mull_commut. apply make_mullimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_mullimm_correct; auto.
+(* divl *)
+  assert (rs#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
+  apply make_divlimm_correct; auto.
+(* divlu *)
+  assert (rs#r2 = Vlong n2). clear H0. InvApproxRegs; SimplVM; auto.
+  apply make_divluimm_correct; auto.
+(* andl *)
+  InvApproxRegs; SimplVM; inv H0. fold (Val.andl (Vlong n1) rs#r2). rewrite Val.andl_commut. apply make_andlimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_andlimm_correct; auto.
+  inv H; inv H0. apply make_andlimm_correct; auto.
+(* orlimm *)
+  InvApproxRegs; SimplVM; inv H0. fold (Val.orl (Vlong n1) rs#r2). rewrite Val.orl_commut. apply make_orlimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_orlimm_correct; auto.
+(* xorlimm *)
+  InvApproxRegs; SimplVM; inv H0. fold (Val.xorl (Vlong n1) rs#r2). rewrite Val.xorl_commut. apply make_xorlimm_correct; auto.
+  InvApproxRegs; SimplVM; inv H0. apply make_xorlimm_correct; auto.
+(* shll *)
+  InvApproxRegs; SimplVM; inv H0. apply make_shllimm_correct; auto.
+(* shrl *)
+  InvApproxRegs; SimplVM; inv H0. apply make_shrlimm_correct; auto.
+(* shrlu *)
+  InvApproxRegs; SimplVM; inv H0. apply make_shrluimm_correct; auto.
 (* cmp *)
   inv H0. apply make_cmp_correct; auto.
 (* mulf *)
diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v
index 3e5e82d3..a214d131 100644
--- a/powerpc/SelectLongproof.v
+++ b/powerpc/SelectLongproof.v
@@ -240,18 +240,12 @@ Theorem eval_shllimm: forall n, unary_constructor_sound (fun e => shllimm e n) (
 Proof.
   intros; unfold shllimm. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shllimm; auto.
   red; intros.
-  assert (ROLM: forall n1 v,
-             Int.ltu n1 Int64.iwordsize' = true ->
-             Val.shll v (Vint n1) = Val.rolml v n1 (Int64.shl Int64.mone (Int64.repr (Int.unsigned n1)))).
-  { intros. destruct v; auto. simpl. rewrite H0. rewrite <- Int64.shl_rolm. unfold Int64.shl.
-    rewrite Int64.int_unsigned_repr. constructor. unfold Int64.ltu. rewrite Int64.int_unsigned_repr.
-    apply H0. }
   predSpec Int.eq Int.eq_spec n Int.zero.
   exists x; split; auto. subst n; destruct x; simpl; auto.
   destruct (Int.ltu Int.zero Int64.iwordsize'); auto.
   change (Int64.shl' i Int.zero) with (Int64.shl i Int64.zero). rewrite Int64.shl_zero; auto.
   destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl.
-- rewrite ROLM by apply LT. apply eval_rolml. auto.
+- rewrite Val.shll_rolml by apply LT. apply eval_rolml. auto.
 - TrivialExists. constructor; eauto.  constructor. EvalOp. simpl; eauto. constructor.
   constructor.
 Qed.
@@ -260,18 +254,10 @@ Theorem eval_shrluimm: forall n, unary_constructor_sound (fun e => shrluimm e n)
 Proof.
   unfold shrluimm; destruct Archi.splitlong. apply SplitLongproof.eval_shrluimm. auto.
   red; intros.
-  assert (ROLM: forall n1 v,
-             Int.ltu n1 Int64.iwordsize' = true ->
-             Val.shrlu v (Vint n1) = Val.rolml v (Int.sub Int64.iwordsize' n1) (Int64.shru Int64.mone (Int64.repr (Int.unsigned n1)))).
-  { intros. destruct v; auto. simpl. rewrite H0.
-    rewrite Int64.int_sub_ltu by apply H0. rewrite Int64.repr_unsigned. rewrite <- Int64.shru_rolm. unfold Int64.shru'.  unfold Int64.shru.
-    rewrite Int64.unsigned_repr. reflexivity. apply Int64.int_unsigned_range.
-    unfold Int64.ltu. rewrite Int64.int_unsigned_repr. auto.
-  }
   predSpec Int.eq Int.eq_spec n Int.zero.
   exists x. split. apply H. destruct x; simpl; auto. rewrite H0. rewrite Int64.shru'_zero. constructor.
   destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl.
-- rewrite ROLM by apply LT. apply eval_rolml. auto.
+- rewrite Val.shrlu_rolml by apply LT. apply eval_rolml. auto.
 - TrivialExists. constructor; eauto.  constructor. EvalOp. simpl; eauto. constructor.
   constructor.
 Qed.