aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/ConstpropOpproof.v2
-rw-r--r--backend/NeedDomain.v44
-rw-r--r--backend/ValueDomain.v54
-rw-r--r--common/Values.v11
-rw-r--r--ia32/Op.v4
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.
generated by cgit (git 2.34.1) at 2024-06-11 16:08:53 +0000