diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asm.v | 65 | ||||
-rw-r--r-- | arm/Asmgen.v | 4 | ||||
-rw-r--r-- | arm/Asmgenproof.v | 35 | ||||
-rw-r--r-- | arm/Op.v | 3 | ||||
-rw-r--r-- | arm/PrintAsm.ml | 84 | ||||
-rw-r--r-- | arm/linux/Conventions1.v (renamed from arm/linux/Conventions.v) | 218 |
6 files changed, 130 insertions, 279 deletions
@@ -24,7 +24,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Locations. Require Stacklayout. -Require Conventions. +Require Import Conventions. (** * Abstract syntax *) @@ -65,6 +65,28 @@ Inductive crbit: Type := Lemma crbit_eq: forall (x y: crbit), {x=y} + {x<>y}. Proof. decide equality. Defined. +(** We model the following registers of the ARM architecture. *) + +Inductive preg: Type := + | IR: ireg -> preg (**r integer registers *) + | FR: freg -> preg (**r float registers *) + | CR: crbit -> preg (**r bits in the condition register *) + | PC: preg. (**r program counter *) + +Coercion IR: ireg >-> preg. +Coercion FR: freg >-> preg. +Coercion CR: crbit >-> preg. + +Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. +Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined. + +Module PregEq. + Definition t := preg. + Definition eq := preg_eq. +End PregEq. + +Module Pregmap := EMap(PregEq). + (** The instruction set. Most instructions correspond exactly to actual instructions of the PowerPC processor. See the PowerPC reference manuals for more details. Some instructions, @@ -149,7 +171,8 @@ Inductive instruction : Type := | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) - | Pbtbl: ireg -> list label -> instruction. (**r N-way branch through a jump table *) + | Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *) + | Pbuiltin: external_function -> list preg -> preg -> instruction. (**r built-in *) (** The pseudo-instructions are the following: @@ -204,28 +227,6 @@ Definition program := AST.program fundef unit. (** * Operational semantics *) -(** We model the following registers of the ARM architecture. *) - -Inductive preg: Type := - | IR: ireg -> preg (**r integer registers *) - | FR: freg -> preg (**r float registers *) - | CR: crbit -> preg (**r bits in the condition register *) - | PC: preg. (**r program counter *) - -Coercion IR: ireg >-> preg. -Coercion FR: freg >-> preg. -Coercion CR: crbit >-> preg. - -Lemma preg_eq: forall (x y: preg), {x=y} + {x<>y}. -Proof. decide equality. apply ireg_eq. apply freg_eq. apply crbit_eq. Defined. - -Module PregEq. - Definition t := preg. - Definition eq := preg_eq. -End PregEq. - -Module Pregmap := EMap(PregEq). - (** The semantics operates over a single mapping from registers (type [preg]) to values. We maintain (but do not enforce) the convention that integer registers are mapped to values of @@ -532,6 +533,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome else Error | _ => Error end + | Pbuiltin ef args res => Error (**r treated specially below *) end. (** Translation of the LTL/Linear/Mach view of machine registers @@ -594,10 +596,10 @@ Inductive extcall_args (rs: regset) (m: mem): list loc -> list val -> Prop := Definition extcall_arguments (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := - extcall_args rs m (Conventions.loc_arguments sg) args. + extcall_args rs m (loc_arguments sg) args. Definition loc_external_result (sg: signature) : preg := - preg_of (Conventions.loc_result sg). + preg_of (loc_result sg). (** Execution of the instruction at [rs#PC]. *) @@ -612,13 +614,20 @@ Inductive step: state -> trace -> state -> Prop := find_instr (Int.unsigned ofs) c = Some i -> exec_instr c i rs m = OK rs' m' -> step (State rs m) E0 (State rs' m') + | exec_step_builtin: + forall b ofs c ef args res rs m t v m', + rs PC = Vptr b ofs -> + Genv.find_funct_ptr ge b = Some (Internal c) -> + find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) -> + external_call ef ge (map rs args) m t v m' -> + step (State rs m) t (State (nextinstr(rs # res <- v)) m') | exec_step_external: forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> - extcall_arguments rs m ef.(ef_sig) args -> - rs' = (rs#(loc_external_result ef.(ef_sig)) <- res + extcall_arguments rs m (ef_sig ef) args -> + rs' = (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs IR14)) -> step (State rs m) t (State rs' m'). diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 2a3b3f36..775bb37f 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -55,7 +55,7 @@ Definition is_immed_mem_float (x: int) : bool := Int.eq (Int.and x (Int.repr 3)) Int.zero && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x. -(** Smart constructor for integer immediate arguments. *) +(** Smart constructors for integer immediate arguments. *) Definition loadimm (r: ireg) (n: int) (k: code) := if is_immed_arith n then @@ -479,6 +479,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := loadind_int IR13 f.(fn_retaddr_ofs) IR14 (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb :: k) + | Mbuiltin ef args res => + Pbuiltin ef (map preg_of args) (preg_of res) :: k | Mlabel lbl => Plabel lbl :: k | Mgoto lbl => diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 99759720..cc4d7ac5 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -25,6 +25,7 @@ Require Import Globalenvs. Require Import Smallstep. Require Import Op. Require Import Locations. +Require Import Conventions. Require Import Mach. Require Import Machconcr. Require Import Machtyping. @@ -896,6 +897,37 @@ Lemma exec_Mtailcall_prop:
forall (s : list stackframe) (fb stk : block) (soff intros. rewrite Pregmap.gso; auto. Qed. +Lemma exec_Mbuiltin_prop: + forall (s : list stackframe) (f : block) (sp : val) + (ms : Mach.regset) (m : mem) (ef : external_function) + (args : list mreg) (res : mreg) (b : list Mach.instruction) + (t : trace) (v : val) (m' : mem), + external_call ef ge ms ## args m t v m' -> + exec_instr_prop (Machconcr.State s f sp (Mbuiltin ef args res :: b) ms m) t + (Machconcr.State s f sp b (Regmap.set res v ms) m'). +Proof. + intros; red; intros; inv MS. + generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). + intro WTI. inv WTI. + inv AT. simpl in H3. + generalize (functions_transl _ _ FIND); intro FN. + generalize (functions_transl_no_overflow _ _ FIND); intro NOOV. + left. econstructor; split. apply plus_one. + eapply exec_step_builtin. eauto. eauto. + eapply find_instr_tail; eauto. + replace (rs##(preg_of##args)) with (ms##args). + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact varinfo_preserved. + rewrite list_map_compose. apply list_map_exten. intros. + symmetry. eapply preg_val; eauto. + econstructor; eauto with coqlib. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. + rewrite <- H0. simpl. constructor; auto. + eapply code_tail_next_int; eauto. + apply sym_not_equal. auto with ppcgen. + auto with ppcgen. +Qed. + Lemma exec_Mgoto_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) @@ -1145,7 +1177,7 @@ Lemma exec_function_external_prop: Genv.find_funct_ptr ge fb = Some (External ef) -> external_call ef ge args m t0 res m' -> Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> - ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> + ms' = Regmap.set (loc_result (ef_sig ef)) res ms -> exec_instr_prop (Machconcr.Callstate s fb ms m) t0 (Machconcr.Returnstate s ms' m'). Proof. @@ -1187,6 +1219,7 @@ Proof exec_Mstore_prop exec_Mcall_prop exec_Mtailcall_prop + exec_Mbuiltin_prop exec_Mgoto_prop exec_Mcond_true_prop exec_Mcond_false_prop @@ -24,6 +24,7 @@ syntax and dynamic semantics of the Cminor language. *) +Require Import Axioms. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -132,7 +133,7 @@ Proof. generalize Int.eq_dec; intro. assert (forall (x y: shift_amount), {x=y}+{x<>y}). destruct x as [x Px]. destruct y as [y Py]. destruct (H x y). - subst x. rewrite (proof_irrelevance _ Px Py). left; auto. + subst x. rewrite (proof_irr Px Py). left; auto. right. red; intro. elim n. inversion H0. auto. decide equality. Qed. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 3184d92f..b3f49cd6 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -188,7 +188,53 @@ let call_helper oc fn dst arg1 arg2 = (* ... for a total of at most 7 instructions *) 7 -(* Built-in functions *) +(* Built-ins. They come in two flavors: + - inlined by the compiler: take their arguments in arbitrary + registers; preserve all registers except IR14 + - inlined while printing asm code; take their arguments in + locations dictated by the calling conventions; preserve + callee-save regs only. *) + +let print_builtin_inlined oc name args res = + fprintf oc "%s begin %s\n" comment name; + let n = match name, args, res with + (* Volatile reads *) + | "__builtin_volatile_read_int8unsigned", [IR addr], IR res -> + fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1 + | "__builtin_volatile_read_int8signed", [IR addr], IR res -> + fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1 + | "__builtin_volatile_read_int16unsigned", [IR addr], IR res -> + fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1 + | "__builtin_volatile_read_int16signed", [IR addr], IR res -> + fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1 + | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res -> + fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1 + | "__builtin_volatile_read_float32", [IR addr], FR res -> + fprintf oc " ldfs %a, [%a, #0]\n" freg res ireg addr; + fprintf oc " mvfd %a, %a\n" freg res freg res; 2 + | "__builtin_volatile_read_float64", [IR addr], FR res -> + fprintf oc " ldfd %a, [%a, #0]\n" freg res ireg addr; 1 + (* Volatile writes *) + | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ -> + fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1 + | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ -> + fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1 + | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ -> + fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1 + | "__builtin_volatile_write_float32", [IR addr; FR src], _ -> + fprintf oc " mvfs %a, %a\n" freg FR2 freg src; + fprintf oc " stfs %a, [%a, #0]\n" freg FR2 ireg addr; 2 + | "__builtin_volatile_write_float64", [IR addr; FR src], _ -> + fprintf oc " stfd %a, [%a, #0]\n" freg src ireg addr; 1 + (* Float arithmetic *) + | "__builtin_fabs", [FR a1], FR res -> + fprintf oc " absd %a, %a\n" freg res freg a1; 1 + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + in + fprintf oc "%s end %s\n" comment name; + n let re_builtin_function = Str.regexp "__builtin_" @@ -200,38 +246,6 @@ let print_builtin_function oc s = (* int args: IR0-IR3 float args: FR0, FR1 int res: IR0 float res: FR0 *) let n = match extern_atom s with - (* Volatile reads *) - | "__builtin_volatile_read_int8unsigned" -> - fprintf oc " ldrb %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_int8signed" -> - fprintf oc " ldrsb %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_int16unsigned" -> - fprintf oc " ldrh %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_int16signed" -> - fprintf oc " ldrsh %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_int32" - | "__builtin_volatile_read_pointer" -> - fprintf oc " ldr %a, [%a, #0]\n" ireg IR0 ireg IR0; 1 - | "__builtin_volatile_read_float32" -> - fprintf oc " ldfs %a, [%a, #0]\n" freg FR0 ireg IR0; - fprintf oc " mvfd %a, %a\n" freg FR0 freg FR0; 2 - | "__builtin_volatile_read_float64" -> - fprintf oc " ldfd %a, [%a, #0]\n" freg FR0 ireg IR0; 1 - (* Volatile writes *) - | "__builtin_volatile_write_int8unsigned" - | "__builtin_volatile_write_int8signed" -> - fprintf oc " strb %a, [%a, #0]\n" ireg IR1 ireg IR0; 1 - | "__builtin_volatile_write_int16unsigned" - | "__builtin_volatile_write_int16signed" -> - fprintf oc " strh %a, [%a, #0]\n" ireg IR1 ireg IR0; 1 - | "__builtin_volatile_write_int32" - | "__builtin_volatile_write_pointer" -> - fprintf oc " str %a, [%a, #0]\n" ireg IR1 ireg IR0; 1 - | "__builtin_volatile_write_float32" -> - fprintf oc " mvfs %a, %a\n" freg FR0 freg FR0; - fprintf oc " stfs %a, [%a, #0]\n" freg FR0 ireg IR0; 2 - | "__builtin_volatile_write_float64" -> - fprintf oc " stfd %a, [%a, #0]\n" freg FR0 ireg IR0; 1 (* Block copy *) | "__builtin_memcpy" -> let lbl1 = new_label() in @@ -252,7 +266,7 @@ let print_builtin_function oc s = fprintf oc " subnes %a, %a, #1\n" ireg IR2 ireg IR2; fprintf oc " bne %a\n" label lbl *) - | "__builtin_memcpy_word" -> + | "__builtin_memcpy_words" -> let lbl1 = new_label() in let lbl2 = new_label() in fprintf oc " movs %a, %a, lsr #2\n" ireg IR2 ireg IR2; @@ -467,6 +481,8 @@ let print_instruction oc labels = function (fun l -> fprintf oc " .word %a\n" print_label l) tbl; 2 + List.length tbl + | Pbuiltin(ef, args, res) -> + print_builtin_inlined oc (extern_atom ef.ef_id) args res let no_fallthrough = function | Pb _ -> true diff --git a/arm/linux/Conventions.v b/arm/linux/Conventions1.v index a35162c2..703dc12d 100644 --- a/arm/linux/Conventions.v +++ b/arm/linux/Conventions1.v @@ -222,65 +222,6 @@ Proof. unfold float_callee_save_regs; NoRepet. Qed. -(** * Acceptable locations for register allocation *) - -(** The following predicate describes the locations that can be assigned - to an RTL pseudo-register during register allocation: a non-temporary - machine register or a [Local] stack slot are acceptable. *) - -Definition loc_acceptable (l: loc) : Prop := - match l with - | R r => ~(In l temporaries) - | S (Local ofs ty) => ofs >= 0 - | S (Incoming _ _) => False - | S (Outgoing _ _) => False - end. - -Definition locs_acceptable (ll: list loc) : Prop := - forall l, In l ll -> loc_acceptable l. - -Lemma temporaries_not_acceptable: - forall l, loc_acceptable l -> Loc.notin l temporaries. -Proof. - unfold loc_acceptable; destruct l. - simpl. intuition congruence. - destruct s; try contradiction. - intro. simpl. tauto. -Qed. -Hint Resolve temporaries_not_acceptable: locs. - -Lemma locs_acceptable_disj_temporaries: - forall ll, locs_acceptable ll -> Loc.disjoint ll temporaries. -Proof. - intros. apply Loc.notin_disjoint. intros. - apply temporaries_not_acceptable. auto. -Qed. - -Lemma loc_acceptable_noteq_diff: - forall l1 l2, - loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2. -Proof. - unfold loc_acceptable, Loc.diff; destruct l1; destruct l2; - try (destruct s); try (destruct s0); intros; auto; try congruence. - case (zeq z z0); intro. - compare t t0; intro. - subst z0; subst t0; tauto. - tauto. tauto. - contradiction. contradiction. -Qed. - -Lemma loc_acceptable_notin_notin: - forall r ll, - loc_acceptable r -> - ~(In r ll) -> Loc.notin r ll. -Proof. - induction ll; simpl; intros. - auto. - split. apply loc_acceptable_noteq_diff. assumption. - apply sym_not_equal. tauto. - apply IHll. assumption. tauto. -Qed. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -326,40 +267,18 @@ Proof. reflexivity. Qed. -(** The result location is acceptable. *) - -Lemma loc_result_acceptable: - forall sig, loc_acceptable (R (loc_result sig)). -Proof. - intros. unfold loc_acceptable. red. - unfold loc_result. destruct (sig_res sig). - destruct t; simpl; NotOrEq. - simpl; NotOrEq. -Qed. - -(** The result location is a caller-save register. *) +(** The result location is a caller-save register or a temporary *) Lemma loc_result_caller_save: - forall (s: signature), In (R (loc_result s)) destroyed_at_call. + forall (s: signature), + In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries. Proof. - intros; unfold loc_result. + intros; unfold loc_result. left; destruct (sig_res s). destruct t; simpl; OrEq. simpl; OrEq. Qed. -(** The result location is not a callee-save register. *) - -Lemma loc_result_not_callee_save: - forall (s: signature), - ~(In (loc_result s) int_callee_save_regs \/ In (loc_result s) float_callee_save_regs). -Proof. - intros. generalize (loc_result_caller_save s). - generalize (int_callee_save_not_destroyed (loc_result s)). - generalize (float_callee_save_not_destroyed (loc_result s)). - tauto. -Qed. - (** ** Location of function arguments *) (** We use the following calling conventions, adapted from the ARM ABI: @@ -449,13 +368,6 @@ Fixpoint size_arguments_rec Definition size_arguments (s: signature) : Z := size_arguments_rec s.(sig_args) int_param_regs float_param_regs 0. -(** A tail-call is possible for a signature if the corresponding - arguments are all passed in registers. *) - -Definition tailcall_possible (s: signature) : Prop := - forall l, In l (loc_arguments s) -> - match l with R _ => True | S _ => False end. - (** Argument locations are either non-temporary registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -685,24 +597,6 @@ Proof. ElimOrEq; intuition. Qed. -(** Callee-save registers do not overlap with argument locations. *) - -Lemma arguments_not_preserved: - forall sig l, - Loc.notin l destroyed_at_call -> loc_acceptable l -> - Loc.notin l (loc_arguments sig). -Proof. - intros. unfold loc_arguments. destruct l. - apply loc_arguments_rec_notin_reg. - generalize (Loc.notin_not_in _ _ H). intro; red; intro. - apply H1. generalize H2. simpl. ElimOrEq; OrEq. - generalize (Loc.notin_not_in _ _ H). intro; red; intro. - apply H1. generalize H2. simpl. ElimOrEq; OrEq. - destruct s; simpl in H0; try contradiction. - apply loc_arguments_rec_notin_local. -Qed. -Hint Resolve arguments_not_preserved: locs. - (** Argument locations agree in number with the function signature. *) Lemma loc_arguments_length: @@ -748,107 +642,3 @@ Proof. intro; simpl. ElimOrEq; reflexivity. Qed. -(** There is no partial overlap between an argument location and an - acceptable location: they are either identical or disjoint. *) - -Lemma no_overlap_arguments: - forall args sg, - locs_acceptable args -> - Loc.no_overlap args (loc_arguments sg). -Proof. - unfold Loc.no_overlap; intros. - generalize (H r H0). - generalize (loc_arguments_acceptable _ _ H1). - destruct s; destruct r; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; auto. - intros. right. auto. - destruct s; try tauto. destruct s0; tauto. -Qed. - -(** Decide whether a tailcall is possible. *) - -Definition tailcall_is_possible (sg: signature) : bool := - let fix tcisp (l: list loc) := - match l with - | nil => true - | R _ :: l' => tcisp l' - | S _ :: l' => false - end - in tcisp (loc_arguments sg). - -Lemma tailcall_is_possible_correct: - forall s, tailcall_is_possible s = true -> tailcall_possible s. -Proof. - intro s. unfold tailcall_is_possible, tailcall_possible. - generalize (loc_arguments s). induction l; simpl; intros. - elim H0. - destruct a. - destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate. -Qed. - -(** ** Location of function parameters *) - -(** A function finds the values of its parameter in the same locations - where its caller stored them, except that the stack-allocated arguments, - viewed as [Outgoing] slots by the caller, are accessed via [Incoming] - slots (at the same offsets and types) in the callee. *) - -Definition parameter_of_argument (l: loc) : loc := - match l with - | S (Outgoing n ty) => S (Incoming n ty) - | _ => l - end. - -Definition loc_parameters (s: signature) := - List.map parameter_of_argument (loc_arguments s). - -Lemma loc_parameters_type: - forall sig, List.map Loc.type (loc_parameters sig) = sig.(sig_args). -Proof. - intros. unfold loc_parameters. - rewrite list_map_compose. - rewrite <- loc_arguments_type. - apply list_map_exten. - intros. destruct x; simpl. auto. - destruct s; reflexivity. -Qed. - -Lemma loc_parameters_length: - forall sg, List.length (loc_parameters sg) = List.length sg.(sig_args). -Proof. - intros. unfold loc_parameters. rewrite list_length_map. - apply loc_arguments_length. -Qed. - -Lemma loc_parameters_not_temporaries: - forall sig, Loc.disjoint (loc_parameters sig) temporaries. -Proof. - intro; red; intros. - unfold loc_parameters in H. - elim (list_in_map_inv _ _ _ H). intros y [EQ IN]. - generalize (loc_arguments_not_temporaries sig y x2 IN H0). - subst x1. destruct x2. - destruct y; simpl. auto. destruct s; auto. - byContradiction. generalize H0. simpl. NotOrEq. -Qed. - -Lemma no_overlap_parameters: - forall params sg, - locs_acceptable params -> - Loc.no_overlap (loc_parameters sg) params. -Proof. - unfold Loc.no_overlap; intros. - unfold loc_parameters in H0. - elim (list_in_map_inv _ _ _ H0). intros t [EQ IN]. - rewrite EQ. - generalize (loc_arguments_acceptable _ _ IN). - generalize (H s H1). - destruct s; destruct t; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; simpl; auto. - intros; right; auto. - destruct s; try tauto. destruct s0; try tauto. - intros; simpl. tauto. -Qed. - |