aboutsummaryrefslogtreecommitdiffstats
path: root/common/Values.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/Values.v')
-rw-r--r--common/Values.v93
1 files changed, 71 insertions, 22 deletions
diff --git a/common/Values.v b/common/Values.v
index cfabb7a5..d086c69f 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -16,7 +16,6 @@
(** This module defines the type of values that is used in the dynamic
semantics of all our intermediate languages. *)
-Require Archi.
Require Import Coqlib.
Require Import AST.
Require Import Integers.
@@ -668,6 +667,12 @@ Definition modlu (v1 v2: val): option val :=
| _, _ => None
end.
+Definition addl_carry (v1 v2 cin: val): val :=
+ match v1, v2, cin with
+ | Vlong n1, Vlong n2, Vlong c => Vlong(Int64.add_carry n1 n2 c)
+ | _, _, _ => Vundef
+ end.
+
Definition subl_overflow (v1 v2: val) : val :=
match v1, v2 with
| Vlong n1, Vlong n2 => Vint (Int.repr (Int64.unsigned (Int64.sub_overflow n1 n2 Int64.zero)))
@@ -734,6 +739,15 @@ Definition shrxl (v1 v2: val): option val :=
| _, _ => None
end.
+Definition shrl_carry (v1 v2: val): val :=
+ match v1, v2 with
+ | Vlong n1, Vint n2 =>
+ if Int.ltu n2 Int64.iwordsize'
+ then Vlong(Int64.shr_carry' n1 n2)
+ else Vundef
+ | _, _ => Vundef
+ end.
+
Definition roll (v1 v2: val): val :=
match v1, v2 with
| Vlong n1, Vint n2 => Vlong(Int64.rol n1 (Int64.repr (Int.unsigned n2)))
@@ -746,9 +760,9 @@ Definition rorl (v1 v2: val): val :=
| _, _ => Vundef
end.
-Definition rolml (v: val) (amount mask: int64): val :=
+Definition rolml (v: val) (amount: int) (mask: int64): val :=
match v with
- | Vlong n => Vlong(Int64.rolm n amount mask)
+ | Vlong n => Vlong(Int64.rolm n (Int64.repr (Int.unsigned amount)) mask)
| _ => Vundef
end.
@@ -1073,7 +1087,7 @@ Proof.
symmetry. auto with ptrofs.
symmetry. rewrite Int.add_commut. auto with ptrofs.
- destruct (eq_block b b0); auto.
- f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs.
+ f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs.
Qed.
Theorem mul_commut: forall x y, mul x y = mul y x.
@@ -1133,6 +1147,28 @@ Proof.
generalize (Int.eq_spec i0 Int.zero). rewrite Heqb; auto.
Qed.
+Theorem modls_divls:
+ forall x y z,
+ modls x y = Some z -> exists v, divls x y = Some v /\ z = subl x (mull v y).
+Proof.
+ intros. destruct x; destruct y; simpl in *; try discriminate.
+ destruct (Int64.eq i0 Int64.zero
+ || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H.
+ exists (Vlong (Int64.divs i i0)); split; auto.
+ simpl. rewrite Int64.mods_divs. auto.
+Qed.
+
+Theorem modlu_divlu:
+ forall x y z,
+ modlu x y = Some z -> exists v, divlu x y = Some v /\ z = subl x (mull v y).
+Proof.
+ intros. destruct x; destruct y; simpl in *; try discriminate.
+ destruct (Int64.eq i0 Int64.zero) eqn:?; inv H.
+ exists (Vlong (Int64.divu i i0)); split; auto.
+ simpl. rewrite Int64.modu_divu. auto.
+ generalize (Int64.eq_spec i0 Int64.zero). rewrite Heqb; auto.
+Qed.
+
Theorem divs_pow2:
forall x n logn y,
Int.is_power2 n = Some logn -> Int.ltu logn (Int.repr 31) = true ->
@@ -1282,7 +1318,7 @@ Proof.
symmetry; apply zlt_true. change (Int.unsigned n < 32); omega.
symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32.
assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
- rewrite Int.unsigned_repr.
+ rewrite Int.unsigned_repr.
change (Int.unsigned Int.iwordsize) with 32; omega.
assert (32 < Int.max_unsigned) by reflexivity. omega.
Qed.
@@ -1384,7 +1420,7 @@ Proof.
symmetry. auto with ptrofs.
symmetry. rewrite Int64.add_commut. auto with ptrofs.
- destruct (eq_block b b0); auto.
- simpl; f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs.
+ simpl; f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs.
- rewrite Int64.add_commut. rewrite Int64.sub_add_r. auto.
Qed.
@@ -1462,7 +1498,7 @@ Proof.
|| Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq n Int64.mone); inv H3.
simpl. rewrite H0. decEq. decEq.
generalize (Int64.is_power2'_correct _ _ H); intro.
- unfold Int64.shrx'. rewrite Int64.shl'_mul_two_p. rewrite <- H1.
+ unfold Int64.shrx'. rewrite Int64.shl'_mul_two_p. rewrite <- H1.
rewrite Int64.mul_commut. rewrite Int64.mul_one.
rewrite Int64.repr_unsigned. auto.
Qed.
@@ -1491,6 +1527,19 @@ Proof.
simpl. decEq. symmetry. eapply Int64.modu_and; eauto.
Qed.
+Theorem shrxl_carry:
+ forall x y z,
+ shrxl x y = Some z ->
+ addl (shrl x y) (shrl_carry x y) = z.
+Proof.
+ intros. destruct x; destruct y; simpl in H; inv H.
+ destruct (Int.ltu i0 (Int.repr 63)) eqn:?; inv H1.
+ exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63. intros.
+ assert (Int.ltu i0 Int64.iwordsize' = true).
+ unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. omega.
+ simpl. rewrite H0. simpl. decEq. rewrite Int64.shrx'_carry; auto.
+Qed.
+
Theorem shrxl_shrl_2:
forall n x z,
shrxl x (Vint n) = Some z ->
@@ -1511,7 +1560,7 @@ Proof.
symmetry; apply zlt_true. change (Int.unsigned n < 64); omega.
symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64.
assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. }
- rewrite Int.unsigned_repr.
+ rewrite Int.unsigned_repr.
change (Int.unsigned Int64.iwordsize') with 64; omega.
assert (64 < Int.max_unsigned) by reflexivity. omega.
Qed.
@@ -1603,7 +1652,7 @@ Theorem swap_cmpu_bool:
Proof.
assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
{ destruct c; auto. }
- intros; unfold cmpu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.
+ intros; unfold cmpu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.
- rewrite Int.swap_cmpu. auto.
- rewrite Int.swap_cmpu. auto.
- destruct (eq_block b b0); subst.
@@ -1630,7 +1679,7 @@ Theorem swap_cmplu_bool:
Proof.
assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c).
{ destruct c; auto. }
- intros; unfold cmplu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.
+ intros; unfold cmplu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto.
- rewrite Int64.swap_cmpu. auto.
- destruct (eq_block b b0); subst.
rewrite dec_eq_true.
@@ -1937,7 +1986,7 @@ Qed.
Lemma offset_ptr_assoc:
forall v d1 d2, offset_ptr (offset_ptr v d1) d2 = offset_ptr v (Ptrofs.add d1 d2).
Proof.
- intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc.
+ intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc.
Qed.
(** * Values and memory injections *)
@@ -1988,7 +2037,7 @@ Hint Resolve inject_list_nil inject_list_cons.
Lemma inject_ptrofs:
forall mi i, inject mi (Vptrofs i) (Vptrofs i).
Proof.
- unfold Vptrofs; intros. destruct Archi.ptr64; auto.
+ unfold Vptrofs; intros. destruct Archi.ptr64; auto.
Qed.
Hint Resolve inject_ptrofs.
@@ -2002,7 +2051,7 @@ Lemma load_result_inject:
inject f v1 v2 ->
inject f (Val.load_result chunk v1) (Val.load_result chunk v2).
Proof.
- intros. inv H; destruct chunk; simpl; try constructor; destruct Archi.ptr64; econstructor; eauto.
+ intros. inv H; destruct chunk; simpl; try constructor; destruct Archi.ptr64; econstructor; eauto.
Qed.
Remark add_inject:
@@ -2012,11 +2061,11 @@ Remark add_inject:
inject f (Val.add v1 v2) (Val.add v1' v2').
Proof.
intros. unfold Val.add. destruct Archi.ptr64 eqn:SF.
-- inv H; inv H0; constructor.
+- inv H; inv H0; constructor.
- inv H; inv H0; simpl; auto.
-+ econstructor; eauto.
++ econstructor; eauto.
rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
-+ econstructor; eauto.
++ econstructor; eauto.
rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
Qed.
@@ -2029,7 +2078,7 @@ Proof.
intros. unfold Val.sub. destruct Archi.ptr64 eqn:SF.
- inv H; inv H0; constructor.
- inv H; inv H0; simpl; auto.
-+ econstructor; eauto.
++ econstructor; eauto.
rewrite Ptrofs.sub_add_l. auto.
+ destruct (eq_block b1 b0); auto.
subst. rewrite H1 in H. inv H. rewrite dec_eq_true.
@@ -2044,11 +2093,11 @@ Remark addl_inject:
Proof.
intros. unfold Val.addl. destruct Archi.ptr64 eqn:SF.
- inv H; inv H0; simpl; auto.
-+ econstructor; eauto.
++ econstructor; eauto.
rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
-+ econstructor; eauto.
++ econstructor; eauto.
rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut.
-- inv H; inv H0; constructor.
+- inv H; inv H0; constructor.
Qed.
Remark subl_inject:
@@ -2059,7 +2108,7 @@ Remark subl_inject:
Proof.
intros. unfold Val.subl. destruct Archi.ptr64 eqn:SF.
- inv H; inv H0; simpl; auto.
-+ econstructor; eauto.
++ econstructor; eauto.
rewrite Ptrofs.sub_add_l. auto.
+ destruct (eq_block b1 b0); auto.
subst. rewrite H1 in H. inv H. rewrite dec_eq_true.
@@ -2126,7 +2175,7 @@ Lemma cmpu_bool_inject:
Proof.
Local Opaque Int.add Ptrofs.add.
intros.
- unfold cmpu_bool in *; destruct Archi.ptr64;
+ unfold cmpu_bool in *; destruct Archi.ptr64;
inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1.
fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))).
generated by cgit (git 2.34.1) at 2024-06-13 08:27:55 +0000