diff options
| -rw-r--r-- | backend/Allocation.v | 10 | ||||
| -rw-r--r-- | backend/Allocproof.v | 6 | ||||
| -rw-r--r-- | backend/Alloctyping.v | 6 | ||||
| -rw-r--r-- | backend/Conventions.v | 23 | ||||
| -rw-r--r-- | backend/LTLtyping.v | 1 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 1 | ||||
| -rw-r--r-- | backend/Mach.v | 22 | ||||
| -rw-r--r-- | backend/Machabstr.v | 24 | ||||
| -rw-r--r-- | backend/Machabstr2mach.v | 27 | ||||
| -rw-r--r-- | backend/Machtyping.v | 1 | ||||
| -rw-r--r-- | backend/PPC.v | 56 | ||||
| -rw-r--r-- | backend/PPCgenproof.v | 8 | ||||
| -rw-r--r-- | backend/PPCgenproof1.v | 97 | ||||
| -rw-r--r-- | backend/RTLtyping.v | 19 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 47 | ||||
| -rw-r--r-- | backend/Stackingtyping.v | 2 | ||||
| -rw-r--r-- | caml/Cil2Csyntax.ml | 15 | ||||
| -rw-r--r-- | extraction/.depend | 25 | ||||
| -rw-r--r-- | lib/Coqlib.v | 44 |
19 files changed, 267 insertions, 167 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 66c7a3c1..c66d6b08 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -412,15 +412,7 @@ Definition transf_function (f: RTL.function) : option LTL.function := end. Definition transf_fundef (fd: RTL.fundef) : option LTL.fundef := - match fd with - | External ef => - if type_external_function ef then Some (External ef) else None - | Internal f => - match transf_function f with - | None => None - | Some tf => Some (Internal tf) - end - end. + transf_partial_fundef transf_function fd. Definition transf_program (p: RTL.program) : option LTL.program := transform_partial_program transf_fundef p. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 07c0f58b..0b252d56 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1231,9 +1231,7 @@ Proof. destruct (regalloc f t). intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; simpl; auto. congruence. congruence. congruence. - destruct (type_external_function e). intro EQ; inversion EQ; subst tf. reflexivity. - congruence. Qed. Lemma entrypoint_function_translated: @@ -1780,7 +1778,7 @@ Lemma transl_function_correct: exec_function_prop (Internal f) args m t vres (free m2 stk). Proof. intros; red; intros until tf. - unfold transf_fundef, transf_function. + unfold transf_fundef, transf_partial_fundef, transf_function. caseEq (type_function f). intros env TRF. caseEq (analyze f). @@ -1856,7 +1854,7 @@ Lemma transl_external_function_correct: Proof. intros; red; intros. simpl in H0. - destruct (type_external_function ef); simplify_eq H0; intro. + simplify_eq H0; intro. exists (Locmap.set (R (loc_result (funsig tf))) res ls); split. subst tf. eapply exec_funct_external; eauto. apply Locmap.gss. diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index e4f9f964..4c4c4f76 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -420,7 +420,7 @@ Proof. assert (sig = tf.(fn_sig)). unfold sig. assert (transf_fundef (Internal f) = Some (Internal tf)). - unfold transf_fundef; rewrite TRANSL; auto. + unfold transf_fundef, transf_partial_fundef. rewrite TRANSL; auto. generalize (Allocproof.sig_function_translated _ _ H). simpl; auto. assert (locs_read_ok (loc_parameters sig)). red; unfold loc_parameters. intros. @@ -542,9 +542,7 @@ Proof. caseEq (transf_function f). intros g TF EQ. inversion EQ. constructor. eapply wt_transf_function; eauto. congruence. - caseEq (type_external_function e); intros. - inversion H0. constructor. apply type_external_function_correct. auto. - congruence. + intros. inversion H. constructor. Qed. Lemma program_typing_preserved: diff --git a/backend/Conventions.v b/backend/Conventions.v index 5b4222df..d621e7c0 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -676,29 +676,6 @@ Proof. intros; simpl. tauto. Qed. -(** ** Location of arguments to external functions *) - -Definition loc_external_arguments (s: signature) : list mreg := - List.map - (fun l => match l with R r => r | S _ => IT1 end) - (loc_arguments s). - -Definition sig_external_ok (s: signature) : Prop := - forall sl, ~In (S sl) (loc_arguments s). - -Lemma loc_external_arguments_loc_arguments: - forall s, - sig_external_ok s -> - loc_arguments s = List.map R (loc_external_arguments s). -Proof. - intros. unfold loc_external_arguments. - rewrite list_map_compose. - transitivity (List.map (fun x => x) (loc_arguments s)). - symmetry; apply list_map_identity. - apply list_map_exten; intros. - destruct x. auto. elim (H _ H0). -Qed. - (** ** Location of argument and result of dynamic allocation *) Definition loc_alloc_argument := R3. diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 34508140..187c5cb8 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -94,7 +94,6 @@ Definition wt_function (f: function) : Prop := Inductive wt_fundef: fundef -> Prop := | wt_fundef_external: forall ef, - Conventions.sig_external_ok ef.(ef_sig) -> wt_fundef (External ef) | wt_function_internal: forall f, wt_function f -> diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 3a0ee131..cbe18311 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -254,7 +254,6 @@ Definition wt_function (f: function) : Prop := Inductive wt_fundef: fundef -> Prop := | wt_fundef_external: forall ef, - Conventions.sig_external_ok ef.(ef_sig) -> wt_fundef (External ef) | wt_function_internal: forall f, wt_function f -> diff --git a/backend/Mach.v b/backend/Mach.v index b8bf1e36..f61620d1 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -143,6 +143,26 @@ Definition find_function (ros: mreg + ident) (rs: regset) : option fundef := end end. +(** Extract the values of the arguments of an external call. *) + +Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := + | extcall_arg_reg: forall rs m sp r, + extcall_arg rs m sp (R r) (rs r) + | extcall_arg_stack: forall rs m sp ofs ty v, + load_stack m sp ty (Int.repr (4 * ofs)) = Some v -> + extcall_arg rs m sp (S (Outgoing ofs ty)) v. + +Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := + | extcall_args_nil: forall rs m sp, + extcall_args rs m sp nil nil + | extcall_args_cons: forall rs m sp l1 ll v1 vl, + extcall_arg rs m sp l1 v1 -> extcall_args rs m sp ll vl -> + extcall_args rs m sp (l1 :: ll) (v1 :: vl). + +Definition extcall_arguments + (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop := + extcall_args rs m sp (Conventions.loc_arguments sg) args. + (** [exec_instr ge f sp c rs m c' rs' m'] reflects the execution of the first instruction in the current instruction sequence [c]. [c'] is the current instruction sequence after this execution. @@ -299,7 +319,7 @@ with exec_function: | exec_funct_external: forall ef parent args res rs1 rs2 m t, event_match ef args t res -> - args = rs1##(Conventions.loc_external_arguments ef.(ef_sig)) -> + extcall_arguments rs1 m parent ef.(ef_sig) args -> rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> exec_function (External ef) parent rs1 m t rs2 m. diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 33ed93ca..d83ffa51 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -88,6 +88,26 @@ Inductive set_slot: frame -> typ -> Z -> val -> frame -> Prop := Definition init_frame (f: function) := empty_block (- f.(fn_framesize)) 0. +(** Extract the values of the arguments of an external call. *) + +Inductive extcall_arg: regset -> frame -> loc -> val -> Prop := + | extcall_arg_reg: forall rs fr r, + extcall_arg rs fr (R r) (rs r) + | extcall_arg_stack: forall rs fr ofs ty v, + get_slot fr ty (Int.signed (Int.repr (4 * ofs))) v -> + extcall_arg rs fr (S (Outgoing ofs ty)) v. + +Inductive extcall_args: regset -> frame -> list loc -> list val -> Prop := + | extcall_args_nil: forall rs fr, + extcall_args rs fr nil nil + | extcall_args_cons: forall rs fr l1 ll v1 vl, + extcall_arg rs fr l1 v1 -> extcall_args rs fr ll vl -> + extcall_args rs fr (l1 :: ll) (v1 :: vl). + +Definition extcall_arguments + (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop := + extcall_args rs fr (Conventions.loc_arguments sg) args. + Section RELSEM. Variable ge: genv. @@ -223,7 +243,7 @@ with exec_function: | exec_funct_external: forall ef parent args res rs1 rs2 m t, event_match ef args t res -> - args = rs1##(Conventions.loc_external_arguments ef.(ef_sig)) -> + extcall_arguments rs1 parent ef.(ef_sig) args -> rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> exec_function (External ef) parent rs1 m t rs2 m. @@ -367,7 +387,7 @@ Lemma exec_mutual_induction: (res : val) (rs1 : mreg -> val) (rs2 : RegEq.t -> val) (m : mem) (t0 : trace), event_match ef args t0 res -> - args = rs1 ## (Conventions.loc_external_arguments (ef_sig ef)) -> + extcall_arguments rs1 parent ef.(ef_sig) args -> rs2 = rs1 # (Conventions.loc_result (ef_sig ef)) <- res -> P2 (External ef) parent rs1 m t0 rs2 m) -> (forall (f16 : function) (v : val) (f17 : frame) (c : code) diff --git a/backend/Machabstr2mach.v b/backend/Machabstr2mach.v index a07f64af..8a2b01dd 100644 --- a/backend/Machabstr2mach.v +++ b/backend/Machabstr2mach.v @@ -906,6 +906,29 @@ Proof. constructor. exact A. constructor. Qed. +(** Preservation of arguments to external functions. *) + +Lemma transl_extcall_arguments: + forall rs fr sg args stk base cs m ms, + Machabstr.extcall_arguments rs fr sg args -> + callstack_invariant ((fr, stk, base) :: cs) m ms -> + wt_frame fr -> + extcall_arguments rs ms (Vptr stk base) sg args. +Proof. + unfold Machabstr.extcall_arguments, extcall_arguments; intros. + assert (forall locs vals, + Machabstr.extcall_args rs fr locs vals -> + extcall_args rs ms (Vptr stk base) locs vals). + induction locs; intros; inversion H2; subst; clear H2. + constructor. + constructor; auto. + inversion H7; subst; clear H7. + constructor. + constructor. eapply callstack_get_slot; eauto. + eapply wt_get_slot; eauto. + auto. +Qed. + (** * The proof of simulation *) Section SIMULATION. @@ -1132,7 +1155,9 @@ Proof. auto. (* external function *) - exists ms; split. econstructor; eauto. auto. + exists ms; split. econstructor; eauto. + eapply transl_extcall_arguments; eauto. + auto. Qed. End SIMULATION. diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 24f0ddb6..ad3ee886 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -83,7 +83,6 @@ Record wt_function (f: function) : Prop := mk_wt_function { Inductive wt_fundef: fundef -> Prop := | wt_fundef_external: forall ef, - Conventions.sig_external_ok ef.(ef_sig) -> wt_fundef (External ef) | wt_function_internal: forall f, wt_function f -> diff --git a/backend/PPC.v b/backend/PPC.v index 3aa4ec4f..ba645d02 100644 --- a/backend/PPC.v +++ b/backend/PPC.v @@ -756,32 +756,34 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome the calling conventions in module [Conventions], except that we use PPC registers instead of locations. *) -Fixpoint loc_external_arguments_rec - (tyl: list typ) (iregl: list ireg) (fregl: list freg) - {struct tyl} : list preg := - match tyl with - | nil => nil - | Tint :: tys => - match iregl with - | nil => IR GPR11 (* should not happen *) - | ireg :: _ => IR ireg - end :: - loc_external_arguments_rec tys (list_drop1 iregl) fregl - | Tfloat :: tys => - match fregl with - | nil => IR GPR11 (* should not happen *) - | freg :: _ => FR freg - end :: - loc_external_arguments_rec tys (list_drop2 iregl) (list_drop1 fregl) - end. - -Definition int_param_regs := - GPR3 :: GPR4 :: GPR5 :: GPR6 :: GPR7 :: GPR8 :: GPR9 :: GPR10 :: nil. -Definition float_param_regs := - FPR1 :: FPR2 :: FPR3 :: FPR4 :: FPR5 :: FPR6 :: FPR7 :: FPR8 :: FPR9 :: FPR10 :: nil. - -Definition loc_external_arguments (s: signature) : list preg := - loc_external_arguments_rec s.(sig_args) int_param_regs float_param_regs. +Inductive extcall_args (rs: regset) (m: mem): + list typ -> list ireg -> list freg -> Z -> list val -> Prop := + | extcall_args_nil: forall irl frl ofs, + extcall_args rs m nil irl frl ofs nil + | extcall_args_int_reg: forall tyl ir1 irl frl ofs v1 vl, + v1 = rs (IR ir1) -> + extcall_args rs m tyl irl frl (ofs + 4) vl -> + extcall_args rs m (Tint :: tyl) (ir1 :: irl) frl ofs (v1 :: vl) + | extcall_args_int_stack: forall tyl frl ofs v1 vl, + Mem.loadv Mint32 m (Val.add (rs (IR GPR1)) (Vint (Int.repr ofs))) = Some v1 -> + extcall_args rs m tyl nil frl (ofs + 4) vl -> + extcall_args rs m (Tint :: tyl) nil frl ofs (v1 :: vl) + | extcall_args_float_reg: forall tyl irl fr1 frl ofs v1 vl, + v1 = rs (FR fr1) -> + extcall_args rs m tyl (list_drop2 irl) frl (ofs + 8) vl -> + extcall_args rs m (Tfloat :: tyl) irl (fr1 :: frl) ofs (v1 :: vl) + | extcall_args_float_stack: forall tyl irl ofs v1 vl, + Mem.loadv Mfloat64 m (Val.add (rs (IR GPR1)) (Vint (Int.repr ofs))) = Some v1 -> + extcall_args rs m tyl (list_drop2 irl) nil (ofs + 8) vl -> + extcall_args rs m (Tfloat :: tyl) irl nil ofs (v1 :: vl). + +Definition extcall_arguments + (rs: regset) (m: mem) (sg: signature) (args: list val) : Prop := + extcall_args rs m + sg.(sig_args) + (GPR3 :: GPR4 :: GPR5 :: GPR6 :: GPR7 :: GPR8 :: GPR9 :: GPR10 :: nil) + (FPR1 :: FPR2 :: FPR3 :: FPR4 :: FPR5 :: FPR6 :: FPR7 :: FPR8 :: FPR9 :: FPR10 :: nil) + 24 args. Definition loc_external_result (s: signature) : preg := match s.(sig_res) with @@ -805,7 +807,7 @@ Inductive exec_step: regset -> mem -> trace -> regset -> mem -> Prop := rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> event_match ef args t res -> - args = List.map (fun r => rs#r) (loc_external_arguments ef.(ef_sig)) -> + extcall_arguments rs m ef.(ef_sig) args -> rs' = (rs#(loc_external_result ef.(ef_sig)) <- res #PC <- (rs LR)) -> exec_step rs m t rs' m. diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v index 9cbbc659..f1ee9f22 100644 --- a/backend/PPCgenproof.v +++ b/backend/PPCgenproof.v @@ -1185,7 +1185,7 @@ Lemma exec_function_external_prop: (res : val) (ms1 ms2: Mach.regset) (m : mem) (t : trace), event_match ef args t res -> - args = ms1 ## (Conventions.loc_external_arguments (ef_sig ef)) -> + Mach.extcall_arguments ms1 m parent ef.(ef_sig) args -> ms2 = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms1 -> exec_function_prop (External ef) parent ms1 m t ms2 m. Proof. @@ -1197,10 +1197,8 @@ Proof. split. apply exec_one. eapply exec_step_external; eauto. destruct (functions_translated _ _ AT) as [tf [A B]]. simpl in B. congruence. - rewrite H0. rewrite loc_external_arguments_match. - rewrite list_map_compose. apply list_map_exten; intros. - symmetry; eapply preg_val; eauto. - reflexivity. + eapply extcall_arguments_match; eauto. + reflexivity. Qed. (** We then conclude by induction on the structure of the Mach diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v index 4a9ac948..f9af3c30 100644 --- a/backend/PPCgenproof1.v +++ b/backend/PPCgenproof1.v @@ -442,40 +442,54 @@ Proof. destruct sres. destruct t; reflexivity. reflexivity. Qed. -Remark list_map_drop1: - forall (A B: Set) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l). -Proof. - intros; destruct l; reflexivity. -Qed. - -Remark list_map_drop2: - forall (A B: Set) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l). -Proof. - intros; destruct l. reflexivity. destruct l; reflexivity. -Qed. - -Lemma loc_external_arguments_rec_match: - forall tyl iregl fregl ofs, +Lemma extcall_args_match: + forall ms m sp rs, + agree ms sp rs -> + forall tyl iregl fregl ofs args, (forall r, In r iregl -> mreg_type r = Tint) -> (forall r, In r fregl -> mreg_type r = Tfloat) -> - PPC.loc_external_arguments_rec tyl (map ireg_of iregl) (map freg_of fregl) = - List.map - (fun l => preg_of (match l with R r => r | S _ => IT1 end)) - (Conventions.loc_arguments_rec tyl iregl fregl ofs). -Proof. - induction tyl; intros; simpl. - auto. - destruct a; simpl; apply (f_equal2 (@cons preg)). - destruct iregl; simpl. - reflexivity. unfold preg_of; rewrite (H m); auto with coqlib. - rewrite list_map_drop1. apply IHtyl. - intros; apply H; apply list_drop1_incl; auto. - assumption. - destruct fregl; simpl. - reflexivity. unfold preg_of; rewrite (H0 m); auto with coqlib. - rewrite list_map_drop1. rewrite list_map_drop2. apply IHtyl. - intros; apply H; apply list_drop2_incl; auto. - intros; apply H0; apply list_drop1_incl; auto. + Mach.extcall_args ms m sp (Conventions.loc_arguments_rec tyl iregl fregl ofs) args -> + PPC.extcall_args rs m tyl (List.map ireg_of iregl) (List.map freg_of fregl) (4 * ofs) args. +Proof. + induction tyl; intros. + inversion H2; constructor. + destruct a. + (* integer case *) + destruct iregl as [ | ir1 irl]. + (* stack *) + inversion H2; subst; clear H2. inversion H8; subst; clear H8. + constructor. replace (rs GPR1) with sp. assumption. + eapply sp_val; eauto. + change (@nil ireg) with (ireg_of ## nil). + replace (4 * ofs + 4) with (4 * (ofs + 1)) by omega. + apply IHtyl; auto. + (* register *) + inversion H2; subst; clear H2. inversion H8; subst; clear H8. + simpl map. econstructor. eapply ireg_val; eauto. + apply H0; simpl; auto. + replace (4 * ofs + 4) with (4 * (ofs + 1)) by omega. + apply IHtyl; auto. + intros; apply H0; simpl; auto. + (* float case *) + destruct fregl as [ | fr1 frl]. + (* stack *) + inversion H2; subst; clear H2. inversion H8; subst; clear H8. + constructor. replace (rs GPR1) with sp. assumption. + eapply sp_val; eauto. + change (@nil freg) with (freg_of ## nil). + replace (4 * ofs + 8) with (4 * (ofs + 2)) by omega. + rewrite list_map_drop2. + apply IHtyl; auto. + intros. apply H0. apply list_drop2_incl. auto. + (* register *) + inversion H2; subst; clear H2. inversion H8; subst; clear H8. + simpl map. econstructor. eapply freg_val; eauto. + apply H1; simpl; auto. + replace (4 * ofs + 8) with (4 * (ofs + 2)) by omega. + rewrite list_map_drop2. + apply IHtyl; auto. + intros; apply H0. apply list_drop2_incl. auto. + intros; apply H1; simpl; auto. Qed. Ltac ElimOrEq := @@ -488,14 +502,17 @@ Ltac ElimOrEq := let H := fresh in (intro H; contradiction) end. -Lemma loc_external_arguments_match: - forall sg, - PPC.loc_external_arguments sg = List.map preg_of (Conventions.loc_external_arguments sg). -Proof. - intros. destruct sg as [sgargs sgres]; unfold loc_external_arguments, Conventions.loc_external_arguments. - rewrite list_map_compose. unfold Conventions.loc_arguments. - rewrite <- loc_external_arguments_rec_match. - reflexivity. +Lemma extcall_arguments_match: + forall ms m sp rs sg args, + agree ms sp rs -> + Mach.extcall_arguments ms m sp sg args -> + PPC.extcall_arguments rs m sg args. +Proof. + unfold Mach.extcall_arguments, PPC.extcall_arguments; intros. + change (extcall_args rs m sg.(sig_args) + (List.map ireg_of Conventions.int_param_regs) + (List.map freg_of Conventions.float_param_regs) (4 * 6) args). + eapply extcall_args_match; eauto. intro; simpl; ElimOrEq; reflexivity. intro; simpl; ElimOrEq; reflexivity. Qed. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 449e837a..97d063ac 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -105,7 +105,6 @@ Record wt_function (f: function) (env: regenv): Prop := Inductive wt_fundef: fundef -> Prop := | wt_fundef_external: forall ef, - Conventions.sig_external_ok ef.(ef_sig) -> wt_fundef (External ef) | wt_function_internal: forall f env, wt_function f env -> @@ -300,11 +299,6 @@ Definition type_function (f: function): option regenv := then Some env else None end. -Definition type_external_function (ef: external_function): bool := - List.fold_right - (fun l b => match l with Locations.S _ => false | Locations.R _ => b end) - true (Conventions.loc_arguments ef.(ef_sig)). - Lemma type_function_correct: forall f env, type_function f = Some env -> @@ -327,19 +321,6 @@ Proof. congruence. Qed. -Lemma type_external_function_correct: - forall ef, - type_external_function ef = true -> - Conventions.sig_external_ok ef.(ef_sig). -Proof. - intro ef. unfold type_external_function, Conventions.sig_external_ok. - generalize (Conventions.loc_arguments (ef_sig ef)). - induction l; simpl. - tauto. - destruct a. intros. firstorder congruence. - congruence. -Qed. - (** * Type preservation during evaluation *) (** The type system for RTL is not sound in that it does not guarantee diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 69a7e99f..3bc4339b 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1272,6 +1272,50 @@ Proof. apply shift_offset_sp; auto. Qed. +(** Preservation of the arguments to an external call. *) + +Section EXTERNAL_ARGUMENTS. + +Variable ls: locset. +Variable fr: frame. +Variable rs: regset. +Variable sg: signature. +Hypothesis AG1: forall r, rs r = ls (R r). +Hypothesis AG2: forall (ofs : Z) (ty : typ), + 6 <= ofs -> + ofs + typesize ty <= size_arguments sg -> + get_slot fr ty (Int.signed (Int.repr (4 * ofs))) + (ls (S (Outgoing ofs ty))). + +Lemma transl_external_arguments_rec: + forall locs, + (forall l, In l locs -> loc_argument_acceptable l) -> + (forall ofs ty, In (S (Outgoing ofs ty)) locs -> + ofs + typesize ty <= size_arguments sg) -> + extcall_args rs fr locs ls##locs. +Proof. + induction locs; simpl; intros. + constructor. + constructor. + assert (loc_argument_acceptable a). apply H; auto. + destruct a; red in H1. + rewrite <- AG1. constructor. + destruct s; try contradiction. + constructor. apply AG2. omega. apply H0. auto. + apply IHlocs; auto. +Qed. + +Lemma transl_external_arguments: + extcall_arguments rs fr sg (ls ## (loc_arguments sg)). +Proof. + unfold extcall_arguments. + apply transl_external_arguments_rec. + exact (Conventions.loc_arguments_acceptable sg). + exact (Conventions.loc_arguments_bounded sg). +Qed. + +End EXTERNAL_ARGUMENTS. + (** The proof of semantic preservation relies on simulation diagrams of the following form: << @@ -1594,8 +1638,7 @@ Proof. inversion WTF. subst ef0. set (sg := ef_sig ef) in *. exists (rs#(loc_result sg) <- res). split. econstructor. eauto. - fold sg. rewrite H0. rewrite Conventions.loc_external_arguments_loc_arguments; auto. - rewrite list_map_compose. apply list_map_exten; intros. auto. + fold sg. rewrite H0. apply transl_external_arguments; assumption. reflexivity. split; intros. rewrite H1. unfold Regmap.set. case (RegEq.eq r (loc_result sg)); intro. diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v index 996ada4c..beb28e29 100644 --- a/backend/Stackingtyping.v +++ b/backend/Stackingtyping.v @@ -217,7 +217,7 @@ Lemma wt_transf_fundef: wt_fundef tf. Proof. intros f tf WT. inversion WT; subst. - simpl; intros; inversion H0. constructor; auto. + simpl; intros; inversion H. constructor. unfold transf_fundef, transf_partial_fundef. caseEq (transf_function f0); try congruence. intros tfn TRANSF EQ. inversion EQ; subst tf. diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml index 4012cd15..c41ddeb9 100644 --- a/caml/Cil2Csyntax.ml +++ b/caml/Cil2Csyntax.ml @@ -160,17 +160,6 @@ let globals_for_strings globs = (fun s id l -> CList.Coq_cons(global_for_string s id, l)) stringTable globs -(** Checking restrictions on external functions *) - -let acceptableExtFun targs = - let rec acceptable nint nfloat = function - | Tnil -> true - | Tcons(Tfloat _, rem) -> - nfloat > 0 && acceptable (nint - 2) (nfloat - 1) rem - | Tcons(_, rem) -> - nint > 0 && acceptable (nint - 1) nfloat rem - in acceptable 8 10 targs - (** ** Handling of stubs for variadic functions *) let stub_function_table = Hashtbl.create 47 @@ -185,8 +174,6 @@ let register_stub_function name tres targs = try (stub_name, Hashtbl.find stub_function_table stub_name) with Not_found -> - if not (acceptableExtFun targs) then - warning (name ^ ": too many parameters for a variadic function, will fail during Cminor -> PPC translation"); let rec types_of_types = function | Tnil -> Tnil | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl) @@ -864,8 +851,6 @@ let convertExtFun v = updateLoc(v.vdecl); match convertTyp v.vtype with | Tfunction(args, res) -> - if not (acceptableExtFun args) then - warning (v.vname ^ ": too many parameters for an external function, will fail during Cminor -> PPC translation"); let id = intern_string v.vname in Datatypes.Coq_pair (id, External(id, args, res)) | _ -> diff --git a/extraction/.depend b/extraction/.depend index 9e201baf..f320d0dd 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -40,10 +40,6 @@ ../caml/Main2.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \ Datatypes.cmx Csyntax.cmx ../caml/Cil2Csyntax.cmx ../caml/CMtypecheck.cmx \ ../caml/CMparser.cmx ../caml/CMlexer.cmx -../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \ - ../caml/Camlcoq.cmo CList.cmi AST.cmi -../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \ - ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ CList.cmi AST.cmi ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ @@ -99,6 +95,7 @@ Ctyping.cmi: Specif.cmi Maps.cmi Datatypes.cmi Csyntax.cmi Coqlib.cmi \ Floats.cmi: Specif.cmi Integers.cmi Datatypes.cmi FSetAVL.cmi: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi \ Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi +FSetBridge.cmi: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi FSetFacts.cmi: Specif.cmi setoid.cmi FSetInterface.cmi Datatypes.cmi FSetInterface.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi FSetList.cmi: Specif.cmi OrderedType.cmi Datatypes.cmi CList.cmi @@ -154,8 +151,8 @@ RTLgen.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Integers.cmi \ Datatypes.cmi Coqlib.cmi Cminor.cmi CList.cmi BinPos.cmi AST.cmi RTL.cmi: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi -RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Locations.cmi \ - Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi AST.cmi +RTLtyping.cmi: Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \ + Coqlib.cmi CList.cmi AST.cmi setoid.cmi: Datatypes.cmi Sets.cmi: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi Specif.cmi: Datatypes.cmi @@ -164,6 +161,7 @@ Stacking.cmi: Specif.cmi Op.cmi Mach.cmi Locations.cmi Lineartyping.cmi \ CList.cmi BinPos.cmi BinInt.cmi AST.cmi Sumbool.cmi: Specif.cmi Datatypes.cmi Tunneling.cmi: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi +union_find.cmi: Wf.cmi Specif.cmi Datatypes.cmi Values.cmi: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi BinInt.cmi AST.cmi ZArith_dec.cmi: Sumbool.cmi Specif.cmi Datatypes.cmi BinInt.cmi @@ -173,6 +171,7 @@ Zdiv.cmi: Zbool.cmi ZArith_dec.cmi Specif.cmi Datatypes.cmi BinPos.cmi \ BinInt.cmi Zeven.cmi: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zmax.cmi: Datatypes.cmi BinInt.cmi +Zmin.cmi: Datatypes.cmi BinInt.cmi Zmisc.cmi: Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Allocation.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi \ @@ -267,6 +266,10 @@ FSetAVL.cmo: Wf.cmi Specif.cmi Peano.cmi OrderedType.cmi Int.cmi FSetList.cmi \ Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi FSetAVL.cmi FSetAVL.cmx: Wf.cmx Specif.cmx Peano.cmx OrderedType.cmx Int.cmx FSetList.cmx \ Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx FSetAVL.cmi +FSetBridge.cmo: Specif.cmi FSetInterface.cmi Datatypes.cmi CList.cmi \ + FSetBridge.cmi +FSetBridge.cmx: Specif.cmx FSetInterface.cmx Datatypes.cmx CList.cmx \ + FSetBridge.cmi FSetFacts.cmo: Specif.cmi setoid.cmi OrderedType.cmi FSetInterface.cmi \ Datatypes.cmi FSetFacts.cmi FSetFacts.cmx: Specif.cmx setoid.cmx OrderedType.cmx FSetInterface.cmx \ @@ -400,11 +403,9 @@ RTL.cmo: Values.cmi Registers.cmi Op.cmi Maps.cmi Integers.cmi Globalenvs.cmi \ RTL.cmx: Values.cmx Registers.cmx Op.cmx Maps.cmx Integers.cmx Globalenvs.cmx \ Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx RTL.cmi RTLtyping.cmo: Specif.cmi Registers.cmi ../caml/RTLtypingaux.cmo RTL.cmi \ - Op.cmi Maps.cmi Locations.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ - CList.cmi AST.cmi RTLtyping.cmi + Op.cmi Maps.cmi Datatypes.cmi Coqlib.cmi CList.cmi AST.cmi RTLtyping.cmi RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \ - Op.cmx Maps.cmx Locations.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \ - CList.cmx AST.cmx RTLtyping.cmi + Op.cmx Maps.cmx Datatypes.cmx Coqlib.cmx CList.cmx AST.cmx RTLtyping.cmi setoid.cmo: Datatypes.cmi setoid.cmi setoid.cmx: Datatypes.cmx setoid.cmi Sets.cmo: Specif.cmi Maps.cmi Datatypes.cmi CList.cmi Sets.cmi @@ -421,6 +422,8 @@ Sumbool.cmo: Specif.cmi Datatypes.cmi Sumbool.cmi Sumbool.cmx: Specif.cmx Datatypes.cmx Sumbool.cmi Tunneling.cmo: Maps.cmi LTL.cmi Datatypes.cmi AST.cmi Tunneling.cmi Tunneling.cmx: Maps.cmx LTL.cmx Datatypes.cmx AST.cmx Tunneling.cmi +union_find.cmo: Wf.cmi Specif.cmi Datatypes.cmi union_find.cmi +union_find.cmx: Wf.cmx Specif.cmx Datatypes.cmx union_find.cmi Values.cmo: Specif.cmi Integers.cmi Floats.cmi Datatypes.cmi Coqlib.cmi \ BinPos.cmi BinInt.cmi AST.cmi Values.cmi Values.cmx: Specif.cmx Integers.cmx Floats.cmx Datatypes.cmx Coqlib.cmx \ @@ -443,6 +446,8 @@ Zeven.cmo: Specif.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zeven.cmi Zeven.cmx: Specif.cmx Datatypes.cmx BinPos.cmx BinInt.cmx Zeven.cmi Zmax.cmo: Datatypes.cmi BinInt.cmi Zmax.cmi Zmax.cmx: Datatypes.cmx BinInt.cmx Zmax.cmi +Zmin.cmo: Datatypes.cmi BinInt.cmi Zmin.cmi +Zmin.cmx: Datatypes.cmx BinInt.cmx Zmin.cmi Zmisc.cmo: Datatypes.cmi BinPos.cmi BinInt.cmi Zmisc.cmi Zmisc.cmx: Datatypes.cmx BinPos.cmx BinInt.cmx Zmisc.cmi Zpower.cmo: Zmisc.cmi Datatypes.cmi BinPos.cmi BinInt.cmi Zpower.cmi diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 3bcc8a69..b5d59b86 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -637,6 +637,21 @@ Proof. apply sym_not_equal. apply H; auto. Qed. +Lemma list_disjoint_dec: + forall (A: Set) (eqA_dec: forall (x y: A), {x=y} + {x<>y}) (l1 l2: list A), + {list_disjoint l1 l2} + {~list_disjoint l1 l2}. +Proof. + induction l1; intros. + left; red; intros. elim H. + case (In_dec eqA_dec a l2); intro. + right; red; intro. apply (H a a); auto with coqlib. + case (IHl1 l2); intro. + left; red; intros. elim H; intro. + red; intro; subst a y. contradiction. + apply l; auto. + right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto. +Defined. + (** [list_norepet l] holds iff the list [l] contains no repetitions, i.e. no element occurs twice. *) @@ -658,7 +673,7 @@ Proof. right. red; intro. inversion H. contradiction. left. constructor; auto. right. red; intro. inversion H. contradiction. -Qed. +Defined. Lemma list_map_norepet: forall (A B: Set) (f: A -> B) (l: list A), @@ -803,3 +818,30 @@ Proof. destruct l; simpl. constructor. inversion H. inversion H3. auto. Qed. +Lemma list_map_drop1: + forall (A B: Set) (f: A -> B) (l: list A), list_drop1 (map f l) = map f (list_drop1 l). +Proof. + intros; destruct l; reflexivity. +Qed. + +Lemma list_map_drop2: + forall (A B: Set) (f: A -> B) (l: list A), list_drop2 (map f l) = map f (list_drop2 l). +Proof. + intros; destruct l. reflexivity. destruct l; reflexivity. +Qed. + +(** * Definitions and theorems over boolean types *) + +Definition proj_sumbool (P Q: Prop) (a: {P} + {Q}) : bool := + if a then true else false. + +Implicit Arguments proj_sumbool [P Q]. + +Coercion proj_sumbool: sumbool >-> bool. + +Lemma proj_sumbool_true: + forall (P Q: Prop) (a: {P}+{Q}), proj_sumbool a = true -> P. +Proof. + intros P Q a. destruct a; simpl. auto. congruence. +Qed. + |