diff options
Diffstat (limited to 'ia32')
| -rw-r--r-- | ia32/Asmgenproof1.v | 2 | ||||
| -rw-r--r-- | ia32/Conventions1.v | 177 | ||||
| -rw-r--r-- | ia32/Machregs.v | 22 | ||||
| -rw-r--r-- | ia32/Machregsaux.ml | 5 | ||||
| -rw-r--r-- | ia32/Stacklayout.v | 174 |
5 files changed, 134 insertions, 246 deletions
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index d2a8206e..60cc266e 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -38,7 +38,7 @@ Lemma agree_nextinstr_nf: Proof. intros. unfold nextinstr_nf. apply agree_nextinstr. apply agree_undef_nondata_regs. auto. - intro. simpl. ElimOrEq; auto. + simpl; intros. intuition (subst r; auto). Qed. (** Useful properties of the PC register. *) diff --git a/ia32/Conventions1.v b/ia32/Conventions1.v index 11420d48..e9969ab8 100644 --- a/ia32/Conventions1.v +++ b/ia32/Conventions1.v @@ -14,6 +14,7 @@ machine registers and stack slots. *) Require Import Coqlib. +Require Import Decidableplus. Require Import AST. Require Import Events. Require Import Locations. @@ -29,6 +30,14 @@ Require Import Locations. of callee- and caller-save registers. *) +Definition is_callee_save (r: mreg) : bool := + match r with + | AX | CX | DX => false + | BX | SI | DI | BP => true + | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => false + | FP0 => false + end. + Definition int_caller_save_regs := AX :: CX :: DX :: nil. Definition float_caller_save_regs := X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. @@ -38,161 +47,11 @@ Definition int_callee_save_regs := BX :: SI :: DI :: BP :: nil. Definition float_callee_save_regs : list mreg := nil. Definition destroyed_at_call := - FP0 :: int_caller_save_regs ++ float_caller_save_regs. + List.filter (fun r => negb (is_callee_save r)) all_mregs. Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) Definition dummy_float_reg := X0. (**r Used in [Regalloc]. *) -(** The [index_int_callee_save] and [index_float_callee_save] associate - a unique positive integer to callee-save registers. This integer is - used in [Stacking] to determine where to save these registers in - the activation record if they are used by the current function. *) - -Definition index_int_callee_save (r: mreg) := - match r with - | BX => 0 | SI => 1 | DI => 2 | BP => 3 | _ => -1 - end. - -Definition index_float_callee_save (r: mreg) := -1. - -Ltac ElimOrEq := - match goal with - | |- (?x = ?y) \/ _ -> _ => - let H := fresh in - (intro H; elim H; clear H; - [intro H; rewrite <- H; clear H | ElimOrEq]) - | |- False -> _ => - let H := fresh in (intro H; contradiction) - end. - -Ltac OrEq := - match goal with - | |- (?x = ?x) \/ _ => left; reflexivity - | |- (?x = ?y) \/ _ => right; OrEq - | |- False => fail - end. - -Ltac NotOrEq := - match goal with - | |- (?x = ?y) \/ _ -> False => - let H := fresh in ( - intro H; elim H; clear H; [intro; discriminate | NotOrEq]) - | |- False -> False => - contradiction - end. - -Lemma index_int_callee_save_pos: - forall r, In r int_callee_save_regs -> index_int_callee_save r >= 0. -Proof. - intro r. simpl; ElimOrEq; unfold index_int_callee_save; omega. -Qed. - -Lemma index_float_callee_save_pos: - forall r, In r float_callee_save_regs -> index_float_callee_save r >= 0. -Proof. - intro r. simpl; ElimOrEq; unfold index_float_callee_save; omega. -Qed. - -Lemma index_int_callee_save_pos2: - forall r, index_int_callee_save r >= 0 -> In r int_callee_save_regs. -Proof. - destruct r; simpl; intro; omegaContradiction || OrEq. -Qed. - -Lemma index_float_callee_save_pos2: - forall r, index_float_callee_save r >= 0 -> In r float_callee_save_regs. -Proof. - unfold index_float_callee_save; intros. omegaContradiction. -Qed. - -Lemma index_int_callee_save_inj: - forall r1 r2, - In r1 int_callee_save_regs -> - In r2 int_callee_save_regs -> - r1 <> r2 -> - index_int_callee_save r1 <> index_int_callee_save r2. -Proof. - intros r1 r2. - simpl; ElimOrEq; ElimOrEq; unfold index_int_callee_save; - intros; congruence. -Qed. - -Lemma index_float_callee_save_inj: - forall r1 r2, - In r1 float_callee_save_regs -> - In r2 float_callee_save_regs -> - r1 <> r2 -> - index_float_callee_save r1 <> index_float_callee_save r2. -Proof. - simpl; intros. contradiction. -Qed. - -(** The following lemmas show that - (destroyed at call, integer callee-save, float callee-save) - is a partition of the set of machine registers. *) - -Lemma int_float_callee_save_disjoint: - list_disjoint int_callee_save_regs float_callee_save_regs. -Proof. - red; intros r1 r2. simpl; ElimOrEq; ElimOrEq; discriminate. -Qed. - -Lemma register_classification: - forall r, - In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs. -Proof. - destruct r; - try (left; simpl; OrEq); - try (right; left; simpl; OrEq); - try (right; right; simpl; OrEq). -Qed. - -Lemma int_callee_save_not_destroyed: - forall r, - In r destroyed_at_call -> In r int_callee_save_regs -> False. -Proof. - intros. revert H0 H. simpl. ElimOrEq; NotOrEq. -Qed. - -Lemma float_callee_save_not_destroyed: - forall r, - In r destroyed_at_call -> In r float_callee_save_regs -> False. -Proof. - intros. revert H0 H. simpl. ElimOrEq; NotOrEq. -Qed. - -Lemma int_callee_save_type: - forall r, In r int_callee_save_regs -> mreg_type r = Tany32. -Proof. - intro. simpl; ElimOrEq; reflexivity. -Qed. - -Lemma float_callee_save_type: - forall r, In r float_callee_save_regs -> mreg_type r = Tany64. -Proof. - intro. simpl; ElimOrEq; reflexivity. -Qed. - -Ltac NoRepet := - match goal with - | |- list_norepet nil => - apply list_norepet_nil - | |- list_norepet (?a :: ?b) => - apply list_norepet_cons; [simpl; intuition discriminate | NoRepet] - end. - -Lemma int_callee_save_norepet: - list_norepet int_callee_save_regs. -Proof. - unfold int_callee_save_regs; NoRepet. -Qed. - -Lemma float_callee_save_norepet: - list_norepet float_callee_save_regs. -Proof. - unfold float_callee_save_regs; NoRepet. -Qed. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -239,12 +98,12 @@ Qed. Lemma loc_result_caller_save: forall (s: signature) (r: mreg), - In r (loc_result s) -> In r destroyed_at_call. + In r (loc_result s) -> is_callee_save r = false. Proof. intros. assert (r = AX \/ r = DX \/ r = FP0 \/ r = X0). unfold loc_result in H. destruct (sig_res s) as [[]|]; simpl in H; intuition. - destruct H0 as [A | [A | [A | A]]]; subst r; simpl; OrEq. + destruct H0 as [A | [A | [A | A]]]; subst r; reflexivity. Qed. (** ** Location of function arguments *) @@ -287,8 +146,8 @@ Definition size_arguments (s: signature) : Z := Definition loc_argument_acceptable (l: loc) : Prop := match l with - | R r => In r destroyed_at_call - | S Outgoing ofs ty => ofs >= 0 /\ ty <> Tlong + | R r => is_callee_save r = false + | S Outgoing ofs ty => ofs >= 0 /\ (typealign ty | ofs) | _ => False end. @@ -296,7 +155,7 @@ Remark loc_arguments_rec_charact: forall tyl ofs l, In l (loc_arguments_rec tyl ofs) -> match l with - | S Outgoing ofs' ty => ofs' >= ofs /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1 | _ => False end. Proof. @@ -307,12 +166,12 @@ Proof. | R _ => False | S Local _ _ => False | S Incoming _ _ => False - | S Outgoing ofs' ty => ofs' >= ofs /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1 end). { intros. exploit IHtyl; eauto. destruct l; auto. destruct sl; intuition omega . } destruct a; simpl in H; repeat (destruct H); - ((eapply REC; eauto; omega) || (split; [omega|congruence])). + ((eapply REC; eauto; omega) || (split; [omega|reflexivity])). Qed. Lemma loc_arguments_acceptable: @@ -322,7 +181,7 @@ Proof. unfold loc_arguments; intros. exploit loc_arguments_rec_charact; eauto. unfold loc_argument_acceptable. - destruct l; tauto. + destruct l as [r | [] ofs ty]; intuition auto. rewrite H2; apply Z.divide_1_l. Qed. Hint Resolve loc_arguments_acceptable: locs. diff --git a/ia32/Machregs.v b/ia32/Machregs.v index 34eb0ac8..fb80a1fd 100644 --- a/ia32/Machregs.v +++ b/ia32/Machregs.v @@ -12,6 +12,7 @@ Require Import String. Require Import Coqlib. +Require Import Decidableplus. Require Import Maps. Require Import AST. Require Import Integers. @@ -41,6 +42,25 @@ Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. Proof. decide equality. Defined. Global Opaque mreg_eq. +Definition all_mregs := + AX :: BX :: CX :: DX :: SI :: DI :: BP + :: X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 + :: FP0 :: nil. + +Lemma all_mregs_complete: + forall (r: mreg), In r all_mregs. +Proof. + assert (forall r, proj_sumbool (In_dec mreg_eq r all_mregs) = true) by (destruct r; reflexivity). + intros. specialize (H r). InvBooleans. auto. +Qed. + +Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. + +Instance Finite_mreg : Finite mreg := { + Finite_elements := all_mregs; + Finite_elements_spec := all_mregs_complete +}. + Definition mreg_type (r: mreg): typ := match r with | AX | BX | CX | DX | SI | DI | BP => Tany32 @@ -62,7 +82,7 @@ Module IndexedMreg <: INDEXED_TYPE. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. Proof. - destruct r1; destruct r2; simpl; intro; discriminate || reflexivity. + decide_goal. Qed. End IndexedMreg. diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml index 6485e752..3ec9596a 100644 --- a/ia32/Machregsaux.ml +++ b/ia32/Machregsaux.ml @@ -30,7 +30,4 @@ let name_of_register r = let register_by_name s = Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s)) -let can_reserve_register r = - List.mem r Conventions1.int_callee_save_regs - || List.mem r Conventions1.float_callee_save_regs - +let can_reserve_register r = Conventions1.is_callee_save r diff --git a/ia32/Stacklayout.v b/ia32/Stacklayout.v index f9d1dafe..f19f036c 100644 --- a/ia32/Stacklayout.v +++ b/ia32/Stacklayout.v @@ -13,6 +13,7 @@ (** Machine- and ABI-dependent layout information for activation records. *) Require Import Coqlib. +Require Import Memory Separation. Require Import Bounds. (** The general shape of activation records is as follows, @@ -24,107 +25,118 @@ Require Import Bounds. - Local stack slots. - Space for the stack-allocated data declared in Cminor - Return address. - -The [frame_env] compilation environment records the positions of -the boundaries between these areas of the activation record. *) Definition fe_ofs_arg := 0. -Record frame_env : Type := mk_frame_env { - fe_size: Z; - fe_ofs_link: Z; - fe_ofs_retaddr: Z; - fe_ofs_local: Z; - fe_ofs_int_callee_save: Z; - fe_num_int_callee_save: Z; - fe_ofs_float_callee_save: Z; - fe_num_float_callee_save: Z; - fe_stack_data: Z -}. - (** Computation of the frame environment from the bounds of the current function. *) -Definition make_env (b: bounds) := +Definition make_env (b: bounds) : frame_env := let olink := 4 * b.(bound_outgoing) in (* back link *) - let oics := olink + 4 in (* integer callee-saves *) - let ofcs := align (oics + 4 * b.(bound_int_callee_save)) 8 in (* float callee-saves *) - let ol := ofcs + 8 * b.(bound_float_callee_save) in (* locals *) + let ocs := olink + 4 in (* callee-saves *) + let ol := align (size_callee_save_area b ocs) 8 in (* locals *) let ostkdata := align (ol + 4 * b.(bound_local)) 8 in (* stack data *) let oretaddr := align (ostkdata + b.(bound_stack_data)) 4 in (* return address *) let sz := oretaddr + 4 in (* total size *) - mk_frame_env sz olink oretaddr - ol - oics b.(bound_int_callee_save) - ofcs b.(bound_float_callee_save) - ostkdata. + {| fe_size := sz; + fe_ofs_link := olink; + fe_ofs_retaddr := oretaddr; + fe_ofs_local := ol; + fe_ofs_callee_save := ocs; + fe_stack_data := ostkdata; + fe_used_callee_save := b.(used_callee_save) |}. (** Separation property *) -Remark frame_env_separated: - forall b, +Local Open Scope sep_scope. + +Lemma frame_env_separated: + forall b sp m P, let fe := make_env b in - 0 <= fe_ofs_arg - /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_link) - /\ fe.(fe_ofs_link) + 4 <= fe.(fe_ofs_int_callee_save) - /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_callee_save) - /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_ofs_local) - /\ fe.(fe_ofs_local) + 4 * b.(bound_local) <= fe.(fe_stack_data) - /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_ofs_retaddr) - /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_size). + m |= range sp 0 (fe_stack_data fe) ** range sp (fe_stack_data fe + bound_stack_data b) (fe_size fe) ** P -> + m |= range sp (fe_ofs_local fe) (fe_ofs_local fe + 4 * bound_local b) + ** range sp fe_ofs_arg (fe_ofs_arg + 4 * bound_outgoing b) + ** range sp (fe_ofs_link fe) (fe_ofs_link fe + 4) + ** range sp (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) + ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) + ** P. Proof. - intros. - generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)). - generalize (align_le (fe.(fe_ofs_local) + 4 * b.(bound_local)) 8 (refl_equal _)). - generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 4 (refl_equal _)). - unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, - fe_ofs_local, fe_ofs_int_callee_save, fe_num_int_callee_save, - fe_ofs_float_callee_save, fe_num_float_callee_save, - fe_stack_data, fe_ofs_arg. - intros. - generalize (bound_local_pos b); intro; - generalize (bound_int_callee_save_pos b); intro; - generalize (bound_float_callee_save_pos b); intro; - generalize (bound_outgoing_pos b); intro; - generalize (bound_stack_data_pos b); intro. - omega. +Local Opaque Z.add Z.mul sepconj range. + intros; simpl. + set (olink := 4 * b.(bound_outgoing)). + set (ocs := olink + 4). + set (ol := align (size_callee_save_area b ocs) 8). + set (ostkdata := align (ol + 4 * b.(bound_local)) 8). + set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4). + generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + assert (0 <= olink) by (unfold olink; omega). + assert (olink + 4 <= ocs) by (unfold ocs; omega). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). + assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega). +(* Reorder as: + outgoing + back link + callee-save + local + retaddr *) + rewrite sep_swap12. + rewrite sep_swap23. + rewrite sep_swap45. + rewrite sep_swap34. +(* Apply range_split and range_split2 repeatedly *) + unfold fe_ofs_arg. + apply range_split. omega. + apply range_split. omega. + apply range_split_2. fold ol. omega. omega. + apply range_drop_right with ostkdata. omega. + rewrite sep_swap. + apply range_drop_left with (ostkdata + bound_stack_data b). omega. + rewrite sep_swap. + exact H. Qed. -(** Alignment property *) - -Remark frame_env_aligned: +Lemma frame_env_range: forall b, let fe := make_env b in - (4 | fe.(fe_ofs_link)) - /\ (4 | fe.(fe_ofs_int_callee_save)) - /\ (8 | fe.(fe_ofs_float_callee_save)) - /\ (8 | fe.(fe_ofs_local)) - /\ (8 | fe.(fe_stack_data)) - /\ (4 | fe.(fe_ofs_retaddr)) - /\ (4 | fe.(fe_size)). + 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe. Proof. - intros. - unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, - fe_ofs_local, fe_ofs_int_callee_save, - fe_num_int_callee_save, - fe_ofs_float_callee_save, fe_num_float_callee_save, - fe_stack_data. - set (x1 := 4 * bound_outgoing b). - assert (4 | x1). unfold x1; exists (bound_outgoing b); ring. - set (x2 := x1 + 4). - assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists 1; auto. - set (x3 := x2 + 4 * bound_int_callee_save b). - set (x4 := align x3 8). - assert (8 | x4). unfold x4. apply align_divides. omega. - set (x5 := x4 + 8 * bound_float_callee_save b). - assert (8 | x5). unfold x5; apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. - set (x6 := align (x5 + 4 * bound_local b) 8). - assert (8 | x6). unfold x6; apply align_divides; omega. - set (x7 := align (x6 + bound_stack_data b) 4). - assert (4 | x7). unfold x7; apply align_divides; omega. - set (x8 := x7 + 4). - assert (4 | x8). unfold x8; apply Zdivide_plus_r; auto. exists 1; auto. - tauto. + intros; simpl. + set (olink := 4 * b.(bound_outgoing)). + set (ocs := olink + 4). + set (ol := align (size_callee_save_area b ocs) 8). + set (ostkdata := align (ol + 4 * b.(bound_local)) 8). + set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4). + generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + assert (0 <= olink) by (unfold olink; omega). + assert (olink + 4 <= ocs) by (unfold ocs; omega). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). + assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega). + split. omega. omega. Qed. +Lemma frame_env_aligned: + forall b, + let fe := make_env b in + (8 | fe_ofs_arg) + /\ (8 | fe_ofs_local fe) + /\ (8 | fe_stack_data fe) + /\ (4 | fe_ofs_link fe) + /\ (4 | fe_ofs_retaddr fe). +Proof. + intros; simpl. + set (olink := 4 * b.(bound_outgoing)). + set (ocs := olink + 4). + set (ol := align (size_callee_save_area b ocs) 8). + set (ostkdata := align (ol + 4 * b.(bound_local)) 8). + set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4). + split. apply Zdivide_0. + split. apply align_divides; omega. + split. apply align_divides; omega. + split. apply Z.divide_factor_l. + apply align_divides; omega. +Qed. |