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/SimplLocalsproof.v | 244 +++++++++---------------------------------- 1 file changed, 48 insertions(+), 196 deletions(-) (limited to 'cfrontend/SimplLocalsproof.v') diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index e3aa4e23..1dcf630e 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -202,16 +202,22 @@ Inductive val_casted: val -> type -> Prop := | val_casted_float: forall sz attr n, cast_float_float sz n = n -> val_casted (Vfloat n) (Tfloat sz attr) + | val_casted_long: forall si attr n, + val_casted (Vlong n) (Tlong si attr) | val_casted_ptr_ptr: forall b ofs ty attr, val_casted (Vptr b ofs) (Tpointer ty attr) | val_casted_int_ptr: forall n ty attr, val_casted (Vint n) (Tpointer ty attr) | val_casted_ptr_int: forall b ofs si attr, val_casted (Vptr b ofs) (Tint I32 si attr) - | val_casted_struct: forall id fld attr v, - val_casted v (Tstruct id fld attr) - | val_casted_union: forall id fld attr v, - val_casted v (Tunion id fld attr) + | val_casted_ptr_cptr: forall b ofs id attr, + val_casted (Vptr b ofs) (Tcomp_ptr id attr) + | val_casted_int_cptr: forall n id attr, + val_casted (Vint n) (Tcomp_ptr id attr) + | val_casted_struct: forall id fld attr b ofs, + val_casted (Vptr b ofs) (Tstruct id fld attr) + | val_casted_union: forall id fld attr b ofs, + val_casted (Vptr b ofs) (Tunion id fld attr) | val_casted_void: forall v, val_casted v Tvoid. @@ -240,12 +246,15 @@ Proof. constructor. (* int *) destruct i; destruct ty; simpl in H; try discriminate; destruct v; inv H. - constructor. apply (cast_int_int_idem I8 s). + constructor. apply (cast_int_int_idem I8 s). + constructor. apply (cast_int_int_idem I8 s). destruct (cast_float_int s f0); inv H1. constructor. apply (cast_int_int_idem I8 s). - constructor. apply (cast_int_int_idem I16 s). + constructor. apply (cast_int_int_idem I16 s). + constructor. apply (cast_int_int_idem I16 s). destruct (cast_float_int s f0); inv H1. constructor. apply (cast_int_int_idem I16 s). constructor. auto. - constructor. + constructor. + constructor. auto. destruct (cast_float_int s f0); inv H1. constructor. auto. constructor. auto. constructor. @@ -253,7 +262,10 @@ Proof. constructor. constructor; auto. constructor; auto. + constructor; auto. + constructor; auto. constructor. simpl. destruct (Int.eq i0 Int.zero); auto. + constructor. simpl. destruct (Int64.eq i Int64.zero); auto. constructor. simpl. destruct (Float.cmp Ceq f0 Float.zero); auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. constructor; auto. @@ -261,20 +273,31 @@ Proof. constructor; auto. constructor. simpl. destruct (Int.eq i Int.zero); auto. constructor; auto. + constructor. simpl. destruct (Int.eq i0 Int.zero); auto. + constructor; auto. +(* long *) + destruct ty; try discriminate. + destruct v; inv H. constructor. + destruct v; inv H. constructor. + destruct v; try discriminate. destruct (cast_float_long s f0); inv H. constructor. (* float *) destruct ty; simpl in H; try discriminate; destruct v; inv H. constructor. apply cast_float_float_idem. constructor. apply cast_float_float_idem. + constructor. apply cast_float_float_idem. (* pointer *) destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor. (* impossible cases *) discriminate. discriminate. -(* structs,unions *) - constructor. - constructor. -(* impossible cases *) - discriminate. +(* structs *) + destruct ty; try discriminate; destruct v; try discriminate. + destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor. +(* unions *) + destruct ty; try discriminate; destruct v; try discriminate. + destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor. +(* comp_ptr *) + destruct ty; simpl in H; try discriminate; destruct v; inv H; constructor. Qed. Lemma val_casted_load_result: @@ -293,6 +316,9 @@ Proof. inv H0; auto. inv H0; auto. inv H0; auto. + inv H0; auto. + discriminate. + discriminate. discriminate. discriminate. discriminate. @@ -301,24 +327,18 @@ Qed. Lemma cast_val_casted: forall v ty, val_casted v ty -> sem_cast v ty ty = Some v. Proof. - intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl. + intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto. destruct sz; congruence. congruence. - auto. - auto. - auto. unfold proj_sumbool; repeat rewrite dec_eq_true; auto. unfold proj_sumbool; repeat rewrite dec_eq_true; auto. - auto. Qed. Lemma val_casted_inject: forall f v v' ty, val_inject f v v' -> val_casted v ty -> val_casted v' ty. Proof. - intros. inv H. - auto. - auto. + intros. inv H; auto. inv H0; constructor. inv H0; constructor. Qed. @@ -356,7 +376,10 @@ Proof. destruct v1; inv H0; auto. destruct sz2; auto. destruct v1; inv H0; auto. destruct sz2; auto. destruct v1; inv H0; auto. + destruct v1; inv H0; auto. + destruct v1; try discriminate. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. + destruct v1; try discriminate. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto. inv H0; auto. Qed. @@ -1324,176 +1347,6 @@ Proof. exists (Vptr loc' ofs'); split; auto. eapply deref_loc_copy; eauto. Qed. -Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue. -Proof. unfold Vtrue; auto. Qed. - -Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse. -Proof. unfold Vfalse; auto. Qed. - -Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). -Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. -Qed. - -Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool. - -Ltac TrivialInject := - match goal with - | |- exists v', Some ?v = Some v' /\ _ => exists v; split; auto -(* - | |- exists v', _ /\ val_inject _ (Vint ?n) _ => exists (Vint n); split; auto - | |- exists v', _ /\ val_inject _ (Vfloat ?n) _ => exists (Vfloat n); split; auto - | |- exists v', _ /\ val_inject _ Vtrue _ => exists Vtrue; split; auto - | |- exists v', _ /\ val_inject _ Vfalse _ => exists Vfalse; split; auto - | |- exists v', _ /\ val_inject _ (Val.of_bool ?b) _ => exists (Val.of_bool b); split; auto -*) - | _ => idtac - end. - -Lemma sem_unary_operation_inject: - forall op v1 ty v tv1, - sem_unary_operation op v1 ty = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv. -Proof. - unfold sem_unary_operation; intros. destruct op. - (* notbool *) - unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject. - (* notint *) - unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject. - (* neg *) - unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject. -Qed. - -Lemma sem_cmp_inject: - forall cmp v1 tv1 ty1 v2 tv2 ty2 v, - sem_cmp cmp v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> - val_inject f v2 tv2 -> - exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv. -Proof. - unfold sem_cmp; intros. - assert (MM: option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some v -> - exists tv, option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some tv /\ val_inject f v tv). - intros. exists v; split; auto. - destruct cmp; simpl in H2; inv H2; auto. - - destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct (Int.eq i Int.zero); try discriminate; auto. - destruct (Int.eq i Int.zero); try discriminate; auto. - - destruct (zeq b1 b0); subst. - rewrite H0 in H2. inv H2. rewrite zeq_true. - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; try discriminate. - destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate. - simpl H3. - rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto. - rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto. - simpl. replace (Int.cmpu cmp (Int.add ofs1 (Int.repr delta)) - (Int.add ofs0 (Int.repr delta))) - with (Int.cmpu cmp ofs1 ofs0). - inv H3; TrivialInject. - symmetry. apply Int.translate_cmpu. - eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. - eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. - destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate. - destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate. - destruct (zeq b2 b3); subst. - rewrite Mem.valid_pointer_implies - by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb); eauto). - rewrite Mem.valid_pointer_implies - by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0); eauto). - simpl. - exploit Mem.different_pointers_inject; eauto. intros [[]|A]. easy. - destruct cmp; simpl in H3; inv H3. - simpl. unfold Int.eq. rewrite zeq_false; auto. - simpl. unfold Int.eq. rewrite zeq_false; auto. - rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto. - rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto. - simpl in H3 |- *. auto. -Qed. - -Lemma sem_binary_operation_inject: - forall op v1 ty1 v2 ty2 v tv1 tv2, - sem_binary_operation op v1 ty1 v2 ty2 m = Some v -> - val_inject f v1 tv1 -> val_inject f v2 tv2 -> - exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv. -Proof. - unfold sem_binary_operation; intros. destruct op. -(* add *) - unfold sem_add in *; destruct (classify_add ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. -(* sub *) - unfold sem_sub in *; destruct (classify_sub ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. - econstructor. eauto. rewrite Int.sub_add_l. auto. - destruct (zeq b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2. - rewrite zeq_true. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3. - rewrite Int.sub_shifted. TrivialInject. -(* mul *) - unfold sem_mul in *; destruct (classify_mul ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. -(* div *) - unfold sem_div in *; destruct (classify_div ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct ( Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H1; TrivialInject. - destruct (Int.eq i0 Int.zero); inv H1; TrivialInject. -(* mod *) - unfold sem_mod in *; destruct (classify_binint ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct ( Int.eq i0 Int.zero - || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H1; TrivialInject. - destruct (Int.eq i0 Int.zero); inv H1; TrivialInject. -(* and *) - unfold sem_and in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. -(* or *) - unfold sem_or in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. -(* xor *) - unfold sem_xor in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. -(* shl *) - unfold sem_shl in *; destruct (classify_shift ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject. -(* shr *) - unfold sem_shr in *; destruct (classify_shift ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject. - destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject. -(* comparisons *) - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. - eapply sem_cmp_inject; eauto. -Qed. - -Lemma sem_cast_inject: - forall v1 ty1 ty v tv1, - sem_cast v1 ty1 ty = Some v -> - val_inject f v1 tv1 -> - exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv. -Proof. - unfold sem_cast; intros. - destruct (classify_cast ty1 ty); try discriminate. - inv H0; inv H; TrivialInject. econstructor; eauto. - inv H0; inv H; TrivialInject. - inv H0; inv H; TrivialInject. - inv H0; inv H; TrivialInject. - inv H0; try discriminate. destruct (cast_float_int si2 f0); inv H. TrivialInject. - inv H0; inv H. TrivialInject. - inv H0; inv H. TrivialInject. - TrivialInject. - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. TrivialInject. - destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. TrivialInject. - inv H; TrivialInject. -Qed. - -Lemma bool_val_inject: - forall v ty b tv, - bool_val v ty = Some b -> - val_inject f v tv -> - bool_val tv ty = Some b. -Proof. - unfold bool_val; intros. - destruct (classify_bool ty); inv H0; congruence. -Qed. - Lemma eval_simpl_expr: forall a v, eval_expr ge e le m a v -> @@ -1512,6 +1365,7 @@ Proof. (* const *) exists (Vint i); split; auto. constructor. exists (Vfloat f0); split; auto. constructor. + exists (Vlong i); split; auto. constructor. (* tempvar *) exploit me_temps; eauto. intros [[tv [A B]] C]. exists tv; split; auto. constructor; auto. @@ -2184,7 +2038,7 @@ Proof. (* goto *) generalize TRF; intros TRF'. monadInv TRF'. - exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x0 (call_cont tk)). + exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x (call_cont tk)). eauto. eapply match_cont_call_cont. eauto. apply compat_cenv_for. rewrite H. intros [ts' [tk' [A [B [C D]]]]]. @@ -2197,12 +2051,10 @@ Proof. generalize EQ; intro EQ'; monadInv EQ'. assert (list_norepet (var_names (fn_params f ++ fn_vars f))). unfold var_names. rewrite map_app. auto. - assert (list_disjoint (var_names (fn_params f)) (var_names (fn_temps f))). - monadInv EQ0. auto. exploit match_envs_alloc_variables; eauto. instantiate (1 := cenv_for_gen (addr_taken_stmt f.(fn_body)) (fn_params f ++ fn_vars f)). - intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H5. - intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H4. + intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H4. + intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H3. intros [j' [te [tm0 [A [B [C [D [E F]]]]]]]]. exploit store_params_correct. eauto. @@ -2212,7 +2064,7 @@ Proof. eexact B. eexact C. intros. apply (create_undef_temps_lifted id f). auto. intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto. - exploit create_undef_temps_inv; eauto. intros [P Q]. elim (H3 id id); auto. + exploit create_undef_temps_inv; eauto. intros [P Q]. elim (l id id); auto. intros [tel [tm1 [P [Q [R [S T]]]]]]. change (cenv_for_gen (addr_taken_stmt (fn_body f)) (fn_params f ++ fn_vars f)) with (cenv_for f) in *. -- cgit