From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Initializersproof.v | 222 +++++++++++++----------------------------- 1 file changed, 67 insertions(+), 155 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 75b73ff..c2ca135 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -333,45 +333,19 @@ Qed. (** * Soundness of the compile-time evaluator *) -(** [match_val v v'] holds if the compile-time value [v] - (with symbolic pointers) matches the run-time value [v'] - (with concrete pointers). *) - -Inductive match_val: val -> val -> Prop := - | match_vint: forall n, - match_val (Vint n) (Vint n) - | match_vfloat: forall f, - match_val (Vfloat f) (Vfloat f) - | match_vptr: forall id b ofs, - Genv.find_symbol ge id = Some b -> - match_val (Vptr (Zpos id) ofs) (Vptr b ofs) - | match_vundef: - match_val Vundef Vundef. - -Lemma match_val_of_bool: - forall b, match_val (Val.of_bool b) (Val.of_bool b). -Proof. - destruct b; constructor. -Qed. - -Hint Constructors match_val: mval. -Hint Resolve match_val_of_bool: mval. - -(** The [match_val] relation commutes with the evaluation functions - from [Csem]. *) - -Lemma sem_unary_match: - forall op ty v1 v v1' v', - sem_unary_operation op v1 ty = Some v -> - sem_unary_operation op v1' ty = Some v' -> - match_val v1 v1' -> - match_val v v'. -Proof. - intros. destruct op; simpl in *. - unfold sem_notbool in *. destruct (classify_bool ty); inv H1; inv H; inv H0; auto with mval. constructor. - unfold sem_notint in *. destruct (classify_notint ty); inv H1; inv H; inv H0; auto with mval. - unfold sem_neg in *. destruct (classify_neg ty); inv H1; inv H; inv H0; auto with mval. -Qed. +(** A global environment [ge] induces a memory injection mapping + our symbolic pointers [Vptr (Zpos id) ofs] to run-time pointers + [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *) + +Definition inj (b: block) := + match b with + | Zpos id => + match Genv.find_symbol ge id with + | Some b' => Some (b', 0) + | None => None + end + | _ => None + end. Lemma mem_empty_not_valid_pointer: forall b ofs, Mem.valid_pointer Mem.empty b ofs = false. @@ -387,104 +361,18 @@ Proof. now rewrite !mem_empty_not_valid_pointer. Qed. -Lemma sem_cmp_match: - forall c v1 ty1 v2 ty2 m v v1' v2' v', - sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v -> - sem_cmp c v1' ty1 v2' ty2 m = Some v' -> - match_val v1 v1' -> match_val v2 v2' -> - match_val v v'. -Proof. -Opaque zeq. - intros. unfold sem_cmp in *. - destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval. -- destruct (Int.eq n Int.zero); try discriminate. - unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor. -- destruct (Int.eq n Int.zero); try discriminate. - unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor. -- destruct (zeq (Z.pos id) (Z.pos id0)); discriminate. -Qed. - -Lemma sem_binary_match: - forall op v1 ty1 v2 ty2 m v v1' v2' v', - sem_binary_operation op v1 ty1 v2 ty2 Mem.empty = Some v -> - sem_binary_operation op v1' ty1 v2' ty2 m = Some v' -> - match_val v1 v1' -> match_val v2 v2' -> - match_val v v'. -Proof. - intros. unfold sem_binary_operation in *; destruct op. -(* add *) - unfold sem_add in *. destruct (classify_add ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* sub *) - unfold sem_sub in *. destruct (classify_sub ty1 ty2); inv H1; inv H2; try (inv H; inv H0; auto with mval; fail). - destruct (zeq (Zpos id) (Zpos id0)); try discriminate. - assert (b0 = b) by congruence. subst b0. rewrite zeq_true in H0. - destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H; inv H0; auto with mval. -(* mul *) - unfold sem_mul in *. destruct (classify_mul ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* div *) - unfold sem_div in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0. - inv H12. rewrite H11 in H2. inv H2. constructor. - inv H12. rewrite H11 in H2. inv H2. constructor. - inv H11. constructor. - inv H11. constructor. - inv H11. constructor. -(* mod *) - unfold sem_mod in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0. - inv H12. rewrite H11 in H2. inv H2. constructor. - inv H12. rewrite H11 in H2. inv H2. constructor. -(* and *) - unfold sem_and in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* or *) - unfold sem_or in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* xor *) - unfold sem_xor in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval. -(* shl *) - unfold sem_shl in *. destruct (classify_shift ty1 ty2); inv H1; inv H2; try discriminate. - destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. -(* shr *) - unfold sem_shr in *. destruct (classify_shift ty1 ty2); try discriminate; - destruct s; inv H1; inv H2; try discriminate. - destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. - destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor. -(* comparisons *) - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. - eapply sem_cmp_match; eauto. -Qed. - Lemma sem_cast_match: - forall v1 ty1 ty2 v2, sem_cast v1 ty1 ty2 = Some v2 -> - forall v1' v2', match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' -> - match_val v2' v2. + forall v1 ty1 ty2 v2 v1' v2', + sem_cast v1 ty1 ty2 = Some v2 -> + do_cast v1' ty1 ty2 = OK v2' -> + val_inject inj v1' v1 -> + val_inject inj v2' v2. Proof. - intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:?; inv H1. - unfold sem_cast in H; functional inversion Heqo; subst. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. inv H. constructor; auto. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. destruct (cast_float_int si2 f); inv H. inv H7. constructor. - rewrite H2 in H. inv H0. inv H. rewrite H7. constructor. - rewrite H2 in H. inv H0. inv H. rewrite H7. constructor. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. inv H0. inv H. constructor. - rewrite H2 in H. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. auto. - rewrite H2 in H. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. auto. - rewrite H5 in H. inv H. auto. + intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0. + exploit sem_cast_inject. eexact E. eauto. + intros [v' [A B]]. congruence. Qed. -Lemma bool_val_match: - forall v v' ty, - match_val v v' -> - bool_val v ty = bool_val v' ty. -Proof. - intros. inv H; auto. -Qed. - (** Soundness of [constval] with respect to the big-step semantics *) Lemma constval_rvalue: @@ -492,13 +380,13 @@ Lemma constval_rvalue: eval_simple_rvalue empty_env m a v -> forall v', constval a = OK v' -> - match_val v' v + val_inject inj v' v with constval_lvalue: forall m a b ofs, eval_simple_lvalue empty_env m a b ofs -> forall v', constval a = OK v' -> - match_val v' (Vptr b ofs). + val_inject inj v' (Vptr b ofs). Proof. (* rvalue *) induction 1; intros vres CV; simpl in CV; try (monadInv CV). @@ -509,11 +397,18 @@ Proof. (* addrof *) eauto. (* unop *) - revert EQ0. caseEq (sem_unary_operation op x (typeof r1)); intros; inv EQ0. - eapply sem_unary_match; eauto. + destruct (sem_unary_operation op x (typeof r1)) as [v1'|] eqn:E; inv EQ0. + exploit sem_unary_operation_inject. eexact E. eauto. + intros [v' [A B]]. congruence. (* binop *) - revert EQ2. caseEq (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty); intros; inv EQ2. - eapply sem_binary_match; eauto. + destruct (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. + exploit (sem_binary_operation_inj inj Mem.empty m). + intros. rewrite mem_empty_not_valid_pointer in H3; discriminate. + intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. + intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. + intros. rewrite mem_empty_not_valid_pointer in H3; discriminate. + eauto. eauto. eauto. + intros [v' [A B]]. congruence. (* cast *) eapply sem_cast_match; eauto. (* sizeof *) @@ -521,18 +416,26 @@ Proof. (* alignof *) constructor. (* seqand *) - rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. - monadInv EQ2. eapply sem_cast_match; eauto. eapply sem_cast_match; eauto. - rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. - monadInv EQ2. constructor. + destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b = true) by congruence. subst b. monadInv H5. + eapply sem_cast_match; eauto. eapply sem_cast_match; eauto. + destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b = false) by congruence. subst b. inv H2. auto. (* seqor *) - rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. - monadInv EQ2. eapply sem_cast_match; eauto. eapply sem_cast_match; eauto. - rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. - monadInv EQ2. constructor. + destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b = false) by congruence. subst b. monadInv H5. + eapply sem_cast_match; eauto. eapply sem_cast_match; eauto. + destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b = true) by congruence. subst b. inv H2. auto. (* conditional *) - rewrite (bool_val_match x v1 (typeof r1)) in EQ3; auto. - rewrite H0 in EQ3. destruct b; eapply sem_cast_match; eauto. + destruct (bool_val x (typeof r1)) as [b'|] eqn:E; inv EQ3. + exploit bool_val_inject. eexact E. eauto. intros E'. + assert (b' = b) by congruence. subst b'. + destruct b; eapply sem_cast_match; eauto. (* comma *) auto. (* paren *) @@ -543,12 +446,14 @@ Proof. (* var local *) unfold empty_env in H. rewrite PTree.gempty in H. congruence. (* var_global *) - constructor; auto. + econstructor. unfold inj. rewrite H0. eauto. auto. (* deref *) eauto. (* field struct *) rewrite H0 in CV. monadInv CV. exploit constval_rvalue; eauto. intro MV. inv MV. - simpl. replace x with delta by congruence. constructor. auto. + simpl. replace x with delta by congruence. econstructor; eauto. + rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. + simpl. auto. (* field union *) rewrite H0 in CV. eauto. Qed. @@ -569,7 +474,7 @@ Theorem constval_steps: forall f r m v v' ty m', star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') -> constval r = OK v -> - m' = m /\ ty = typeof r /\ match_val v v'. + m' = m /\ ty = typeof r /\ val_inject inj v v'. Proof. intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. intros [A [B C]]. intuition. eapply constval_rvalue; eauto. @@ -595,19 +500,23 @@ Proof. inv D. (* int *) destruct ty; try discriminate. - destruct i; inv EQ2. + destruct i0; inv EQ2. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. simpl in H2; inv H2. assumption. inv EQ2. simpl in H2; inv H2. assumption. + (* long *) + destruct ty; inv EQ2. simpl in H2; inv H2. assumption. (* float *) destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) - assert (data = Init_addrof id ofs0 /\ chunk = Mint32). + unfold inj in H. destruct b1; try discriminate. + assert (data = Init_addrof p ofs1 /\ chunk = Mint32). destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto. - destruct H4; subst. rewrite H. assumption. + destruct H4; subst. destruct (Genv.find_symbol ge p); inv H. + rewrite Int.add_zero in H3. auto. (* undef *) discriminate. Qed. @@ -624,12 +533,15 @@ Proof. destruct ty; try discriminate. destruct i0; inv EQ2; reflexivity. inv EQ2; reflexivity. + inv EQ2; reflexivity. + destruct ty; inv EQ2; reflexivity. destruct ty; try discriminate. destruct f0; inv EQ2; reflexivity. destruct b; try discriminate. destruct ty; try discriminate. destruct i0; inv EQ2; reflexivity. inv EQ2; reflexivity. + inv EQ2; reflexivity. Qed. Notation idlsize := Genv.init_data_list_size. -- cgit v1.2.3