Improved handling of "rotate left" and "rotate right" operators

- Values: "rol" and "ror" are defined even if their second argument
  is not in the [0,31] range (for consistency with "rolm" and because
  the semantics is definitely well defined in this case).
- NeedDomain: more precise analysis of "rol" and "rolm", could
  benefit the PowerPC port.

2 files changed, 63 insertions, 35 deletions

diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index e40c1322..442352e7 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -539,25 +539,23 @@ Proof.
 - destruct v; auto with na.
 Qed.
 
-Definition rolm (x: nval) (amount mask: int) :=
+Definition rol (x: nval) (amount: int) :=
   match x with
   | Nothing => Nothing
-  | I m => I (Int.ror (Int.and m mask) amount)
-  | _ => I (Int.ror mask amount)
+  | I m => I (Int.ror m amount)
+  | All => All
   end.
 
-Lemma rolm_sound:
-  forall v w x amount mask,
-  vagree v w (rolm x amount mask) ->
-  vagree (Val.rolm v amount mask) (Val.rolm w amount mask) x.
+Lemma rol_sound:
+  forall v w x n,
+  vagree v w (rol x n) ->
+  vagree (Val.rol v (Vint n)) (Val.rol w (Vint n)) x.
 Proof.
-  unfold rolm; intros; destruct x; simpl in *.
+  unfold rol, Val.rol; intros.
+  destruct x; simpl in *.
 - auto.
-- unfold Val.rolm; InvAgree. unfold Int.rolm.
-  apply iagree_and. apply iagree_rol. auto.
-- unfold Val.rolm; InvAgree. apply Val.lessdef_same. f_equal. apply iagree_mone.
-  unfold Int.rolm. apply iagree_and. apply iagree_rol. rewrite Int.and_commut.
-  rewrite Int.and_mone. auto.
+- InvAgree. apply iagree_rol; auto.
+- inv H; auto.
 Qed.
 
 Definition ror (x: nval) (amount: int) :=
@@ -572,13 +570,25 @@ Lemma ror_sound:
   vagree v w (ror x n) ->
   vagree (Val.ror v (Vint n)) (Val.ror w (Vint n)) x.
 Proof.
-  unfold ror; intros. unfold Val.ror.
-  destruct (Int.ltu n Int.iwordsize).
+  unfold ror, Val.ror; intros.
   destruct x; simpl in *.
 - auto.
 - InvAgree. apply iagree_ror; auto.
 - inv H; auto.
-- destruct v; auto with na.
+Qed.
+
+Definition rolm (x: nval) (amount mask: int) := rol (andimm x mask) amount.
+
+Lemma rolm_sound:
+  forall v w x amount mask,
+  vagree v w (rolm x amount mask) ->
+  vagree (Val.rolm v amount mask) (Val.rolm w amount mask) x.
+Proof.
+  unfold rolm; intros.
+  assert (X: forall u, Val.rolm u amount mask = Val.and (Val.rol u (Vint amount)) (Vint mask)).
+  { destruct u; auto. }
+  rewrite ! X.
+  apply andimm_sound. apply rol_sound. auto.
 Qed.
 
 (** Modular arithmetic operations: add, mul, opposite.
@@ -935,7 +945,7 @@ Proof.
   assert (forall n, Int.ror n Int.zero = n).
   { intros. rewrite Int.ror_rol_neg by apply int_wordsize_divides_modulus.
     rewrite Int.neg_zero. apply Int.rol_zero. }
-  unfold rolm, andimm in *. destruct x; auto.
+  unfold rolm, rol, andimm in *. destruct x; auto.
   rewrite H in H0. auto.
   rewrite H in H0. auto.
 Qed.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index d72c577e..8b76f44d 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -1430,9 +1430,39 @@ Proof.
   intros. unfold Val.notint, notint; inv H; eauto with va.
 Qed.
 
+Definition rol (x y: aval) :=
+  match y, x with
+  | I j, I i => I(Int.rol i j)
+  | I j, Uns p n => uns p (n + Int.unsigned j)
+  | I j, Sgn p n => if zlt n Int.zwordsize then sgn p (n + Int.unsigned j) else ntop1 x
+  | _, _ => ntop1 x
+  end.
+
+Lemma rol_sound:
+  forall v w x y, vmatch v x -> vmatch w y -> vmatch (Val.rol v w) (rol x y).
+Proof.
+  intros.
+  assert (DEFAULT: forall p, vmatch (Val.rol v w) (Ifptr p)).
+  {
+    destruct v; destruct w; simpl; constructor.
+  }
+  unfold rol; destruct y; try apply DEFAULT; auto. inv H0. unfold Val.rol.
+  inv H; auto with va.
+- apply vmatch_uns. red; intros. rewrite Int.bits_rol by auto.
+  generalize (Int.unsigned_range n); intros.
+  rewrite Zmod_small by omega.
+  apply H1. omega. omega. 
+- destruct (zlt n0 Int.zwordsize); auto with va.
+  apply vmatch_sgn. red; intros. rewrite ! Int.bits_rol by omega.
+  generalize (Int.unsigned_range n); intros.
+  rewrite ! Zmod_small by omega.
+  rewrite H1 by omega. symmetry. rewrite H1 by omega. auto.
+- destruct (zlt n0 Int.zwordsize); auto with va.
+Qed.
+
 Definition ror (x y: aval) :=
   match y, x with
-  | I j, I i => if Int.ltu j Int.iwordsize then I(Int.ror i j) else ntop
+  | I j, I i => I(Int.ror i j)
   | _, _ => ntop1 x
   end.
 
@@ -1442,35 +1472,23 @@ Proof.
   intros.
   assert (DEFAULT: forall p, vmatch (Val.ror v w) (Ifptr p)).
   {
-    destruct v; destruct w; simpl; try constructor.
-    destruct (Int.ltu i0 Int.iwordsize); constructor.
+    destruct v; destruct w; simpl; constructor.
   }
   unfold ror; destruct y; try apply DEFAULT; auto. inv H0. unfold Val.ror.
-  destruct (Int.ltu n Int.iwordsize) eqn:LTU.
-  inv H; auto with va.
   inv H; auto with va.
 Qed.
 
 Definition rolm (x: aval) (amount mask: int) :=
-  match x with
-  | I i => I (Int.rolm i amount mask)
-  | _   => uns (provenance x) (usize mask)
-  end.
+  and (rol x (I amount)) (I mask).
 
 Lemma rolm_sound:
   forall v x amount mask,
   vmatch v x -> vmatch (Val.rolm v amount mask) (rolm x amount mask).
 Proof.
   intros.
-  assert (UNS_r: forall i j n, is_uns n j -> is_uns n (Int.and i j)).
-  {
-    intros; red; intros. rewrite Int.bits_and by auto. rewrite (H0 m) by auto.
-    apply andb_false_r.
-  }
-  assert (UNS: forall i, vmatch (Vint (Int.rolm i amount mask))
-                                (uns (provenance x) (usize mask))).
-  { intros. unfold Int.rolm. apply vmatch_uns. apply UNS_r. auto with va. }
-  unfold Val.rolm, rolm. inv H; auto with va.
+  replace (Val.rolm v amount mask) with (Val.and (Val.rol v (Vint amount)) (Vint mask)).
+  apply and_sound. apply rol_sound. auto. constructor. constructor.
+  destruct v; auto.
 Qed.
 
 (** Integer arithmetic operations *)