From f1d3dbb3fa70233d1ad83ae88876dd384346a16a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 22 Feb 2018 16:57:02 +0100 Subject: Changed ptr64 to be always true --- mppa_k1c/Archi.v | 2 +- mppa_k1c/Asmgenproof1.v | 4 ++-- mppa_k1c/ConstpropOpproof.v | 2 -- mppa_k1c/Op.v | 6 ++---- mppa_k1c/SelectLongproof.v | 4 ---- mppa_k1c/SelectOpproof.v | 17 ++--------------- 6 files changed, 7 insertions(+), 28 deletions(-) diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v index a1664262..bbe66c5b 100644 --- a/mppa_k1c/Archi.v +++ b/mppa_k1c/Archi.v @@ -20,7 +20,7 @@ Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. -Parameter ptr64 : bool. +Definition ptr64 := true. Definition big_endian := false. diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v index 7f070c12..8bbdbd4c 100644 --- a/mppa_k1c/Asmgenproof1.v +++ b/mppa_k1c/Asmgenproof1.v @@ -553,9 +553,9 @@ Lemma transl_cond_int32s_correct: Proof. intros. destruct cmp; simpl. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. + split; intros; Simpl. destruct (rs##r1); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. + split; intros; Simpl. destruct (rs##r1); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. split; intros; Simpl. - econstructor; split. diff --git a/mppa_k1c/ConstpropOpproof.v b/mppa_k1c/ConstpropOpproof.v index 765aa035..b6c73281 100644 --- a/mppa_k1c/ConstpropOpproof.v +++ b/mppa_k1c/ConstpropOpproof.v @@ -201,7 +201,6 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. exists (e#r); split; auto. destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto. - destruct Archi.ptr64; auto. exists (Val.add e#r (Vint n)); split; auto. Qed. @@ -374,7 +373,6 @@ Proof. predSpec Int64.eq Int64.eq_spec n Int64.zero; intros. subst. exists (e#r); split; auto. destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto. - destruct Archi.ptr64; auto. exists (Val.addl e#r (Vlong n)); split; auto. Qed. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index bb04f786..74101f53 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -522,7 +522,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* addrsymbol *) - unfold Genv.symbol_address. destruct (Genv.find_symbol genv id)... (* addrstack *) - - destruct sp... apply Val.Vptr_has_type. + - destruct sp... (* castsigned *) - destruct v0... - destruct v0... @@ -532,8 +532,6 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* neg, sub *) - destruct v0... - unfold Val.sub. destruct v0; destruct v1... - unfold Val.has_type; destruct Archi.ptr64... - destruct Archi.ptr64... destruct (eq_block b b0)... (* mul, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... @@ -582,7 +580,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0... - unfold Val.subl. destruct v0; destruct v1... unfold Val.has_type; destruct Archi.ptr64... - destruct Archi.ptr64... destruct (eq_block b b0)... + destruct (eq_block b b0)... (* mull, mullhs, mullhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index 78a1935d..511dee92 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -123,7 +123,6 @@ Proof. predSpec Int64.eq Int64.eq_spec n Int64.zero. subst. exists x; split; auto. destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto. - destruct Archi.ptr64; auto. destruct (addlimm_match a); InvEval. - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto. - econstructor; split. EvalOp. simpl; eauto. @@ -169,7 +168,6 @@ Proof. destruct Archi.ptr64 eqn:SF; auto. apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; auto. - subst. econstructor; split. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto. destruct sp; simpl; auto. @@ -177,7 +175,6 @@ Proof. destruct Archi.ptr64 eqn:SF; auto. apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal. rewrite Ptrofs.add_commut. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; auto. - subst. replace (Val.addl (Val.addl v1 (Vlong n1)) y) with (Val.addl (Val.addl v1 y) (Vlong n1)). @@ -346,7 +343,6 @@ Proof. subst x. destruct v1; simpl; auto. simpl in B2; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_l. rewrite (Int64.mul_commut n). auto. - destruct Archi.ptr64; simpl; auto. - apply eval_mullimm_base; auto. Qed. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 90f077db..e7577fb5 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -143,15 +143,12 @@ Proof. - subst n. intros. exists x; split; auto. destruct x; simpl; auto. rewrite Int.add_zero; auto. - destruct Archi.ptr64; auto. rewrite Ptrofs.add_zero; auto. - case (addimm_match a); intros; InvEval; simpl. + TrivialExists; simpl. rewrite Int.add_commut. auto. + econstructor; split. EvalOp. simpl; eauto. unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. - destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. + econstructor; split. EvalOp. simpl; eauto. - destruct sp; simpl; auto. destruct Archi.ptr64; auto. - rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut m0). auto. + destruct sp; simpl; auto. + TrivialExists; simpl. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto. + TrivialExists. Qed. @@ -171,18 +168,10 @@ Proof. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto. rewrite Val.add_commut. destruct sp; simpl; auto. destruct v1; simpl; auto. - destruct Archi.ptr64 eqn:SF; auto. - apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. - rewrite (Ptrofs.add_commut (Ptrofs.of_int n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; auto. - subst. econstructor; split. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto. destruct sp; simpl; auto. destruct v1; simpl; auto. - destruct Archi.ptr64 eqn:SF; auto. - apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal. - rewrite Ptrofs.add_commut. auto with ptrofs. - destruct Archi.ptr64 eqn:SF; auto. - subst. replace (Val.add (Val.add v1 (Vint n1)) y) with (Val.add (Val.add v1 y) (Vint n1)). @@ -889,8 +878,7 @@ Proof. constructor. EvalOp. simpl. congruence. constructor. simpl. rewrite Ptrofs.add_zero. congruence. + exists (@nil val); split. constructor. simpl; auto. - exists (v1 :: nil); split. eauto with evalexpr. simpl. - destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. - simpl. auto. + destruct v1; simpl in H; try discriminate. - exists (v1 :: nil); split. eauto with evalexpr. simpl. destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. simpl. auto. @@ -917,7 +905,6 @@ Proof. - destruct Archi.ptr64 eqn:SF. + InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vlong n) else Val.add v1 (Vlong n)). repeat constructor; auto. - rewrite SF; auto. + constructor; auto. - constructor; auto. Qed. -- cgit