Commit e99d18c4 authored by xleroy's avatar xleroy
Browse files

Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext

  as bitwise operations rather than arithmetic ones.
CastOptimproof: fixed for ARM port.
Other files: adapted to changes in Integers.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 0438984d
......@@ -247,7 +247,7 @@ Proof.
decEq. rewrite Float.singleoffloat_idem; auto.
(* comparison *)
simpl in H0. destruct (eval_condition c rs##args); try discriminate.
destruct b; inv H0; auto.
destruct b; inv H0; compute; auto.
Qed.
Lemma approx_of_chunk_correct:
......@@ -434,8 +434,9 @@ Proof.
(* Iload *)
econstructor; split.
TransfInstr; intro. eapply exec_Iload; eauto.
TransfInstr; intro. eapply exec_Iload with (a := a). eauto.
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
eauto.
econstructor; eauto.
eapply analyze_correct with (pc := pc); eauto.
simpl; auto.
......@@ -444,8 +445,9 @@ Proof.
(* Istore *)
econstructor; split.
TransfInstr; intro. eapply exec_Istore; eauto.
TransfInstr; intro. eapply exec_Istore with (a := a). eauto.
rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
eauto.
econstructor; eauto.
eapply analyze_correct with (pc := pc); eauto.
simpl; auto.
......
......@@ -148,6 +148,7 @@ Lemma int_of_bytes_of_int:
Proof.
induction n; intros.
simpl. rewrite Zmod_1_r. auto.
Opaque Byte.wordsize.
rewrite inj_S. simpl.
replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega.
rewrite two_p_is_exp; try omega.
......@@ -155,6 +156,17 @@ Proof.
apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
Qed.
Lemma int_of_bytes_of_int_2:
forall n x,
(n = 1 \/ n = 2)%nat ->
Int.repr (int_of_bytes (bytes_of_int n (Int.unsigned x))) = Int.zero_ext (Z_of_nat n * 8) x.
Proof.
intros. rewrite int_of_bytes_of_int.
rewrite <- (Int.repr_unsigned (Int.zero_ext (Z_of_nat n * 8) x)).
decEq. symmetry. apply Int.zero_ext_mod.
destruct H; subst n; compute; auto.
Qed.
Lemma bytes_of_int_mod:
forall n x y,
Int.eqmod (two_p (Z_of_nat n * 8)) x y ->
......@@ -239,11 +251,16 @@ Lemma decode_encode_int:
end.
Proof.
intros. unfold decode_int, encode_int; destruct c; auto;
rewrite rev_if_be_involutive; rewrite int_of_bytes_of_int.
apply Int.sign_ext_zero_ext; vm_compute; auto.
apply Int.zero_ext_idem; vm_compute; auto.
apply Int.sign_ext_zero_ext; vm_compute; auto.
apply Int.zero_ext_idem; vm_compute; auto.
rewrite rev_if_be_involutive.
rewrite int_of_bytes_of_int_2; auto.
apply Int.sign_ext_zero_ext. compute; auto.
rewrite int_of_bytes_of_int_2; auto.
apply Int.zero_ext_idem. compute; auto.
rewrite int_of_bytes_of_int_2; auto.
apply Int.sign_ext_zero_ext. compute; auto.
rewrite int_of_bytes_of_int_2; auto.
apply Int.zero_ext_idem. compute; auto.
rewrite int_of_bytes_of_int.
transitivity (Int.repr (Int.unsigned x)).
apply Int.eqm_samerepr. apply Int.eqm_sym. apply Int.eqmod_mod. apply two_p_gt_ZERO. omega.
apply Int.repr_unsigned.
......@@ -267,8 +284,7 @@ Lemma encode_int8_zero_ext:
forall x,
encode_int Mint8unsigned (Int.zero_ext 8 x) = encode_int Mint8unsigned x.
Proof.
intros. apply encode_8_mod. apply Int.eqmod_sym.
apply Int.eqmod_two_p_zero_ext. compute; auto.
intros. apply encode_8_mod. apply Int.eqmod_zero_ext. compute; auto.
Qed.
Lemma encode_int8_sign_ext:
......@@ -276,8 +292,10 @@ Lemma encode_int8_sign_ext:
encode_int Mint8signed (Int.sign_ext 8 x) = encode_int Mint8signed x.
Proof.
intros. repeat rewrite encode_int8_signed_unsigned.
apply encode_8_mod. apply Int.eqmod_sym.
apply Int.eqmod_two_p_sign_ext. compute; auto.
apply encode_8_mod. eapply Int.eqmod_trans.
apply Int.eqm_eqmod_two_p. compute; auto.
apply Int.eqm_sym. apply Int.eqm_signed_unsigned.
apply Int.eqmod_sign_ext. compute; auto.
Qed.
Lemma encode_int16_signed_unsigned: forall n,
......@@ -298,8 +316,7 @@ Lemma encode_int16_zero_ext:
forall x,
encode_int Mint16unsigned (Int.zero_ext 16 x) = encode_int Mint16unsigned x.
Proof.
intros. apply encode_16_mod. apply Int.eqmod_sym.
apply (Int.eqmod_two_p_zero_ext 16). compute; auto.
intros. apply encode_16_mod. apply Int.eqmod_zero_ext. compute; auto.
Qed.
Lemma encode_int16_sign_ext:
......@@ -307,8 +324,10 @@ Lemma encode_int16_sign_ext:
encode_int Mint16signed (Int.sign_ext 16 x) = encode_int Mint16signed x.
Proof.
intros. repeat rewrite encode_int16_signed_unsigned.
apply encode_16_mod. apply Int.eqmod_sym.
apply Int.eqmod_two_p_sign_ext. compute; auto.
apply encode_16_mod. eapply Int.eqmod_trans.
apply Int.eqm_eqmod_two_p. compute; auto.
apply Int.eqm_sym. apply Int.eqm_signed_unsigned.
apply Int.eqmod_sign_ext. compute; auto.
Qed.
Lemma decode_int8_zero_ext:
......@@ -860,43 +879,6 @@ Proof.
split; auto. subst mvl. apply encode_pointer_shape.
Qed.
(*
Lemma proj_bytes_none:
forall mv,
match mv with Byte _ => False | _ => True end ->
forall mvl,
In mv mvl ->
proj_bytes mvl = None.
Proof.
induction mvl; simpl; intros.
elim H0.
destruct a; auto. destruct H0. subst mv. contradiction.
rewrite (IHmvl H0); auto.
Qed.
Lemma decode_val_undef:
forall chunk mv mv1 mvl,
match mv with
| Pointer b ofs n => n = pred (size_chunk_nat Mint32)
| Undef => True
| _ => False
end ->
In mv mvl ->
decode_val chunk (mv1 :: mvl) = Vundef.
Proof.
intros. unfold decode_val.
replace (proj_bytes (mv1 :: mvl)) with (@None (list byte)).
destruct chunk; auto. unfold proj_pointer. destruct mv1; auto.
case_eq (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n :: mvl)); intros.
exploit check_pointer_inv; eauto. simpl. intros. inv H2.
simpl in H0. intuition; subst mv; simpl in H; congruence.
auto.
symmetry. apply proj_bytes_none with mv.
destruct mv; tauto. auto with coqlib.
Qed.
*)
(** * Compatibility with memory injections *)
(** Relating two memory values according to a memory injection. *)
......
This diff is collapsed.
......@@ -1217,10 +1217,10 @@ Proof.
rewrite <- Int.shl_rolm. rewrite Int.shl_mul.
rewrite Int.mul_signed.
apply Int.signed_repr.
split. apply Zle_trans with 0. vm_compute; congruence. omega.
split. apply Zle_trans with 0. compute; congruence. omega.
omega.
vm_compute. reflexivity.
vm_compute. apply Int.mkint_eq. auto.
compute. reflexivity.
apply Int.mkint_eq. compute. reflexivity.
inv AT. simpl in H7.
set (k1 := Pbtbl GPR12 tbl :: transl_code f c).
set (rs1 := nextinstr (rs0 # GPR12 <- (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))))).
......
......@@ -79,41 +79,25 @@ Proof.
unfold high_s.
rewrite <- (Int.divu_pow2 (Int.sub n (low_s n)) (Int.repr 65536) (Int.repr 16)).
change (two_p (Int.unsigned (Int.repr 16))) with 65536.
assert (forall x y, y > 0 -> (x - x mod y) mod y = 0).
intros. apply Zmod_unique with (x / y).
generalize (Z_div_mod_eq x y H). intro. rewrite Zmult_comm. omega.
omega.
assert (Int.modu (Int.sub n (low_s n)) (Int.repr 65536) = Int.zero).
unfold Int.modu, Int.zero. decEq.
change (Int.unsigned (Int.repr 65536)) with 65536.
unfold Int.sub.
assert (forall a b, Int.eqm a b -> b mod 65536 = 0 -> a mod 65536 = 0).
intros a b [k EQ] H1. rewrite EQ.
change Int.modulus with (65536 * 65536).
rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto.
omega.
eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr.
unfold low_s. unfold Int.sign_ext.
change (two_p 16) with 65536. change (two_p (16-1)) with 32768.
set (N := Int.unsigned n).
case (zlt (N mod 65536) 32768); intro.
apply H0 with (N - N mod 65536). auto with ints.
apply H. omega.
apply H0 with (N - (N mod 65536 - 65536)). auto with ints.
replace (N - (N mod 65536 - 65536))
with ((N - N mod 65536) + 1 * 65536).
rewrite Z_mod_plus. apply H. omega. omega. ring.
assert (Int.repr 65536 <> Int.zero). compute. congruence.
generalize (Int.modu_divu_Euclid (Int.sub n (low_s n)) (Int.repr 65536) H1).
rewrite H0. rewrite Int.add_zero. intro. rewrite <- H2.
rewrite Int.sub_add_opp. rewrite Int.add_assoc.
replace (Int.add (Int.neg (low_s n)) (low_s n)) with Int.zero.
apply Int.add_zero. symmetry. rewrite Int.add_commut.
rewrite <- Int.sub_add_opp. apply Int.sub_idem.
set (x := Int.sub n (low_s n)).
assert (x = Int.add (Int.mul (Int.divu x (Int.repr 65536)) (Int.repr 65536))
(Int.modu x (Int.repr 65536))).
apply Int.modu_divu_Euclid. compute; congruence.
assert (Int.modu x (Int.repr 65536) = Int.zero).
unfold Int.modu, Int.zero. decEq.
change 0 with (0 mod 65536).
change (Int.unsigned (Int.repr 65536)) with 65536.
apply Int.eqmod_mod_eq. omega.
unfold x, low_s. eapply Int.eqmod_trans.
eapply Int.eqm_eqmod_two_p with (n := 16). compute; auto.
unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl.
replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'.
compute; auto.
rewrite H0 in H. rewrite Int.add_zero in H.
rewrite <- H. unfold x. rewrite Int.sub_add_opp. rewrite Int.add_assoc.
rewrite (Int.add_commut (Int.neg (low_s n))). rewrite <- Int.sub_add_opp.
rewrite Int.sub_idem. apply Int.add_zero.
reflexivity.
Qed.
......
......@@ -371,6 +371,80 @@ Definition sub (e1: expr) (e2: expr) :=
(** ** Rotates and immediate shifts *)
(** Recognition of integers that are acceptable as immediate operands
to the [rlwim] PowerPC instruction. These integers are of the form
[000011110000] or [111100001111], that is, a run of one bits
surrounded by zero bits, or conversely. We recognize these integers by
running the following automaton on the bits. The accepting states are
2, 3, 4, 5, and 6.
<<
0 1 0
/ \ / \ / \
\ / \ / \ /
-0--> [1] --1--> [2] --0--> [3]
/
[0]
\
-1--> [4] --0--> [5] --1--> [6]
/ \ / \ / \
\ / \ / \ /
1 0 1
>>
*)
Inductive rlw_state: Type :=
| RLW_S0 : rlw_state
| RLW_S1 : rlw_state
| RLW_S2 : rlw_state
| RLW_S3 : rlw_state
| RLW_S4 : rlw_state
| RLW_S5 : rlw_state
| RLW_S6 : rlw_state
| RLW_Sbad : rlw_state.
Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state :=
match s, b with
| RLW_S0, false => RLW_S1
| RLW_S0, true => RLW_S4
| RLW_S1, false => RLW_S1
| RLW_S1, true => RLW_S2
| RLW_S2, false => RLW_S3
| RLW_S2, true => RLW_S2
| RLW_S3, false => RLW_S3
| RLW_S3, true => RLW_Sbad
| RLW_S4, false => RLW_S5
| RLW_S4, true => RLW_S4
| RLW_S5, false => RLW_S5
| RLW_S5, true => RLW_S6
| RLW_S6, false => RLW_Sbad
| RLW_S6, true => RLW_S6
| RLW_Sbad, _ => RLW_Sbad
end.
Definition rlw_accepting (s: rlw_state) : bool :=
match s with
| RLW_S0 => false
| RLW_S1 => false
| RLW_S2 => true
| RLW_S3 => true
| RLW_S4 => true
| RLW_S5 => true
| RLW_S6 => true
| RLW_Sbad => false
end.
Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool :=
match n with
| O =>
rlw_accepting s
| S m =>
let (b, y) := Int.Z_bin_decomp x in
is_rlw_mask_rec m (rlw_transition s b) y
end.
Definition is_rlw_mask (x: int) : bool :=
is_rlw_mask_rec Int.wordsize RLW_S0 (Int.unsigned x).
(*
Definition rolm (e1: expr) :=
match e1 with
......@@ -414,7 +488,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) :=
| rolm_case2 amount1 mask1 t1 =>
let amount := Int.modu (Int.add amount1 amount2) Int.iwordsize in
let mask := Int.and (Int.rol mask1 amount2) mask2 in
if Int.is_rlw_mask mask
if is_rlw_mask mask
then Eop (Orolm amount mask) (t1:::Enil)
else Eop (Orolm amount2 mask2) (e1:::Enil)
| rolm_default e1 =>
......@@ -548,7 +622,7 @@ Definition mul (e1: expr) (e2: expr) :=
(** ** Bitwise and, or, xor *)
Definition andimm (n1: int) (e2: expr) :=
if Int.is_rlw_mask n1
if is_rlw_mask n1
then rolm e2 Int.zero n1
else Eop (Oandimm n1) (e2:::Enil).
......@@ -591,7 +665,7 @@ Definition or (e1: expr) (e2: expr) :=
match or_match e1 e2 with
| or_case1 amount1 mask1 t1 amount2 mask2 t2 =>
if Int.eq amount1 amount2
&& Int.is_rlw_mask (Int.or mask1 mask2)
&& is_rlw_mask (Int.or mask1 mask2)
&& same_expr_pure t1 t2
then Eop (Orolm amount1 (Int.or mask1 mask2)) (t1:::Enil)
else Eop Oor (e1:::e2:::Enil)
......
......@@ -355,7 +355,7 @@ Lemma eval_rolm:
Proof.
intros until x. unfold rolm; case (rolm_match a); intros; InvEval.
eauto with evalexpr.
case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)).
case (is_rlw_mask (Int.and (Int.rol mask1 amount) mask)).
EvalOp. simpl. subst x.
decEq. decEq.
symmetry. apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
......@@ -460,7 +460,7 @@ Theorem eval_andimm:
eval_expr ge sp e m le a (Vint x) ->
eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)).
Proof.
intros. unfold andimm. case (Int.is_rlw_mask n).
intros. unfold andimm. case (is_rlw_mask n).
rewrite <- Int.rolm_zero. apply eval_rolm; auto.
EvalOp.
Qed.
......@@ -500,7 +500,7 @@ Lemma eval_or:
Proof.
intros until y; unfold or; case (or_match a b); intros; InvEval.
caseEq (Int.eq amount1 amount2
&& Int.is_rlw_mask (Int.or mask1 mask2)
&& is_rlw_mask (Int.or mask1 mask2)
&& same_expr_pure t1 t2); intro.
destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H4).
generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment