From f849a03bc11b2bc3c6373213afc2a7023c636679 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 22 Jun 2016 10:38:21 +0200 Subject: 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. --- arm/ConstpropOpproof.v | 2 +- backend/NeedDomain.v | 44 ++++++++++++++++++++++++---------------- backend/ValueDomain.v | 54 +++++++++++++++++++++++++++++++++----------------- common/Values.v | 11 ++++++---- ia32/Op.v | 4 ++-- 5 files changed, 73 insertions(+), 42 deletions(-) diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 6f6afa8a..0b7643c6 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -98,7 +98,7 @@ Ltac SimplVM := Lemma eval_static_shift_correct: forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n). Proof. - intros. destruct s; simpl; rewrite s_range; auto. + intros. destruct s; simpl; rewrite ? s_range; auto. Qed. Lemma cond_strength_reduction_correct: 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 *) diff --git a/common/Values.v b/common/Values.v index 688e63ed..663bddf6 100644 --- a/common/Values.v +++ b/common/Values.v @@ -404,6 +404,12 @@ Definition shru (v1 v2: val): val := | _, _ => Vundef end. +Definition rol (v1 v2: val): val := + match v1, v2 with + | Vint n1, Vint n2 => Vint(Int.rol n1 n2) + | _, _ => Vundef + end. + Definition rolm (v: val) (amount mask: int): val := match v with | Vint n => Vint(Int.rolm n amount mask) @@ -412,10 +418,7 @@ Definition rolm (v: val) (amount mask: int): val := Definition ror (v1 v2: val): val := match v1, v2 with - | Vint n1, Vint n2 => - if Int.ltu n2 Int.iwordsize - then Vint(Int.ror n1 n2) - else Vundef + | Vint n1, Vint n2 => Vint(Int.ror n1 n2) | _, _ => Vundef end. diff --git a/ia32/Op.v b/ia32/Op.v index e6df3f2d..f21d7c6a 100644 --- a/ia32/Op.v +++ b/ia32/Op.v @@ -450,7 +450,7 @@ Proof with (try exact I). destruct v0; simpl in H0; try discriminate. destruct (Int.ltu i (Int.repr 31)); inv H0... destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)... destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... - destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... + destruct v0... destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)... destruct v1; simpl... destruct (Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize)... eapply type_of_addressing_sound; eauto. @@ -863,7 +863,7 @@ Proof. destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists. inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. - inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. + inv H4; simpl; auto. inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto. inv H2; simpl; auto. destruct (Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize); auto. eapply eval_addressing_inj; eauto. -- cgit