From 246ae564d9ce6c04ba4169b80d2ff9ce21deca34 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 14 Mar 2022 00:59:49 +0000 Subject: Fix proofs for ptr64 --- verilog/Asmgenproof1.v | 4 ++-- verilog/ConstpropOpproof.v | 7 +++++-- verilog/Op.v | 7 +++---- verilog/SelectLongproof.v | 16 ++-------------- verilog/SelectOpproof.v | 43 +------------------------------------------ 5 files changed, 13 insertions(+), 64 deletions(-) diff --git a/verilog/Asmgenproof1.v b/verilog/Asmgenproof1.v index 42ab8375..f37b85b4 100644 --- a/verilog/Asmgenproof1.v +++ b/verilog/Asmgenproof1.v @@ -728,9 +728,9 @@ Lemma transl_cond_int64s_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/verilog/ConstpropOpproof.v b/verilog/ConstpropOpproof.v index 74dc4a05..efeec6f6 100644 --- a/verilog/ConstpropOpproof.v +++ b/verilog/ConstpropOpproof.v @@ -17,6 +17,8 @@ Require Import Integers Floats Values Memory Globalenvs Events. Require Import Op Registers RTL ValueDomain. Require Import ConstpropOp. +#[local] Opaque Archi.ptr64. + Section STRENGTH_REDUCTION. Variable bc: block_classification. @@ -201,7 +203,8 @@ 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. + destruct Archi.ptr64 eqn:?; auto. + exists (Val.add e#r (Vint n)); split; auto. exists (Val.add e#r (Vint n)); split; auto. Qed. @@ -406,7 +409,7 @@ 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. + destruct Archi.ptr64 eqn:?; auto; exists (Val.addl e#r (Vlong n)); split; auto. Qed. diff --git a/verilog/Op.v b/verilog/Op.v index 9f94828f..87986f78 100644 --- a/verilog/Op.v +++ b/verilog/Op.v @@ -778,7 +778,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... @@ -790,6 +790,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - unfold Val.sub. destruct v0; destruct v1... unfold Val.has_type; destruct Archi.ptr64... destruct Archi.ptr64... destruct (eq_block b b0)... + destruct (eq_block b b0)... (* mul, mulhs, mulhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... @@ -839,9 +840,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - apply type_addl. (* negl, subl *) - destruct v0... - - unfold Val.subl. destruct v0; destruct v1... - unfold Val.has_type; destruct Archi.ptr64... - destruct Archi.ptr64... destruct (eq_block b b0)... + - unfold Val.subl. destruct v0; destruct v1... (* mull, mullhs, mullhu *) - destruct v0; destruct v1... - destruct v0; destruct v1... diff --git a/verilog/SelectLongproof.v b/verilog/SelectLongproof.v index 0fc578bf..cd88911d 100644 --- a/verilog/SelectLongproof.v +++ b/verilog/SelectLongproof.v @@ -124,15 +124,12 @@ 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. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. - destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. - econstructor; split. EvalOp. simpl; eauto. - destruct sp; simpl; auto. destruct Archi.ptr64; auto. - rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. + destruct sp; simpl; auto. - subst x. rewrite Val.addl_assoc. rewrite Int64.add_commut. TrivialExists. - TrivialExists. Qed. @@ -167,18 +164,10 @@ Proof. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto. rewrite Val.addl_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_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. 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.addl (Val.addl v1 (Vlong n1)) y) with (Val.addl (Val.addl v1 y) (Vlong n1)). @@ -347,7 +336,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/verilog/SelectOpproof.v b/verilog/SelectOpproof.v index f450fe6c..789e38dc 100644 --- a/verilog/SelectOpproof.v +++ b/verilog/SelectOpproof.v @@ -172,7 +172,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_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. @@ -180,7 +179,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.add (Val.add v1 (Vint n1)) y) with (Val.add (Val.add v1 y) (Vint n1)). @@ -965,43 +963,6 @@ Proof. destruct Archi.ptr64 eqn:PTR64. 2: discriminate. destruct ty; cbn in *; try discriminate. - - (* Tint *) - inv H. TrivialExists. - + cbn. repeat econstructor; eassumption. - + cbn. f_equal. rewrite ExtValues.normalize_select01. - rewrite H3. destruct b. - * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption. - * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption. - - - (* Tfloat *) - inv H. TrivialExists. - + cbn. repeat econstructor; eassumption. - + cbn. f_equal. rewrite ExtValues.normalize_select01. - rewrite H3. destruct b. - * rewrite ExtValues.select01_long_true. - apply ExtValues.float_bits_normalize. - * rewrite ExtValues.select01_long_false. - apply ExtValues.float_bits_normalize. - - - (* Tlong *) - inv H. TrivialExists. - + cbn. repeat econstructor; eassumption. - + cbn. f_equal. rewrite ExtValues.normalize_select01. - rewrite H3. destruct b. - * rewrite ExtValues.select01_long_true. reflexivity. - * rewrite ExtValues.select01_long_false. reflexivity. - - - (* Tsingle *) - inv H. TrivialExists. - + cbn. repeat econstructor; eassumption. - + cbn. f_equal. rewrite ExtValues.normalize_select01. - rewrite H3. destruct b. - * rewrite ExtValues.select01_long_true. - rewrite normalize_low_long by assumption. - apply ExtValues.single_bits_normalize. - * rewrite ExtValues.select01_long_false. - rewrite normalize_low_long by assumption. - apply ExtValues.single_bits_normalize. Qed. Theorem eval_addressing: @@ -1024,8 +985,7 @@ Proof. destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 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 (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto. Qed. @@ -1045,7 +1005,6 @@ Proof. + constructor; auto. + InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vint n) else Val.add v1 (Vint n)). repeat constructor; auto. - rewrite SF; auto. - 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. -- cgit