diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Allocproof.v | 1 | ||||
-rw-r--r-- | backend/CSEproof.v | 1 | ||||
-rw-r--r-- | backend/Cminor.v | 4 | ||||
-rw-r--r-- | backend/CminorSel.v | 2 | ||||
-rw-r--r-- | backend/Constpropproof.v | 1 | ||||
-rw-r--r-- | backend/LTL.v | 2 | ||||
-rw-r--r-- | backend/LTLin.v | 2 | ||||
-rw-r--r-- | backend/Linear.v | 2 | ||||
-rw-r--r-- | backend/Linearizeproof.v | 1 | ||||
-rw-r--r-- | backend/Machabstr.v | 2 | ||||
-rw-r--r-- | backend/Machabstr2concr.v | 12 | ||||
-rw-r--r-- | backend/Machconcr.v | 2 | ||||
-rw-r--r-- | backend/Machtyping.v | 2 | ||||
-rw-r--r-- | backend/RTL.v | 2 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 1 | ||||
-rw-r--r-- | backend/Reloadproof.v | 1 | ||||
-rw-r--r-- | backend/Selectionproof.v | 4 | ||||
-rw-r--r-- | backend/Stackingproof.v | 1 | ||||
-rw-r--r-- | backend/Tailcallproof.v | 1 | ||||
-rw-r--r-- | backend/Tunnelingproof.v | 1 |
20 files changed, 29 insertions, 16 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 3f526aa4..b845323f 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -717,6 +717,7 @@ Proof. injection H7; intro EQ; inv EQ. econstructor; split. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. eapply match_states_return; eauto. (* return *) diff --git a/backend/CSEproof.v b/backend/CSEproof.v index fcc867af..ce577aca 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -935,6 +935,7 @@ Proof. (* external function *) simpl. econstructor; split. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. (* return *) diff --git a/backend/Cminor.v b/backend/Cminor.v index f2f03c5d..cc4afa50 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -496,7 +496,7 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') | step_external_function: forall ef vargs k m t vres m', - external_call ef vargs m t vres m' -> + external_call ef (Genv.find_symbol ge) vargs m t vres m' -> step (Callstate (External ef) vargs k m) t (Returnstate vres k m') @@ -595,7 +595,7 @@ Inductive eval_funcall: eval_funcall m (Internal f) vargs t m3 vres | eval_funcall_external: forall ef m args t res m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> eval_funcall m (External ef) args t m' res (** Execution of a statement: [exec_stmt ge f sp e m s t e' m' out] diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 231af8fb..65dd4dec 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -354,7 +354,7 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') | step_external_function: forall ef vargs k m t vres m', - external_call ef vargs m t vres m' -> + external_call ef (Genv.find_symbol ge) vargs m t vres m' -> step (Callstate (External ef) vargs k m) t (Returnstate vres k m') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 6671960c..b5c3b1e3 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -415,6 +415,7 @@ Proof. (* external function *) simpl. econstructor; split. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. constructor; auto. (* return *) diff --git a/backend/LTL.v b/backend/LTL.v index 2a1172ab..4aa8afc5 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -228,7 +228,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m') | exec_function_external: forall s ef t args res m m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: diff --git a/backend/LTLin.v b/backend/LTLin.v index c3b432ba..64017c30 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -225,7 +225,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m') | exec_function_external: forall s ef args t res m m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: diff --git a/backend/Linear.v b/backend/Linear.v index be07b827..7d21651d 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -314,7 +314,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f (Vptr stk Int.zero) f.(fn_code) (call_regs rs) m') | exec_function_external: forall s ef args res rs1 rs2 m t m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) -> rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 -> step (Callstate s (External ef) rs1 m) diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 5d670650..fcb1acfb 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -684,6 +684,7 @@ Proof. (* external function *) monadInv H6. econstructor; split. apply plus_one. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. (* return *) diff --git a/backend/Machabstr.v b/backend/Machabstr.v index ceaf9a68..bbc7e7d8 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -303,7 +303,7 @@ Inductive step: state -> trace -> state -> Prop := f.(fn_code) rs empty_frame m') | exec_function_external: forall s ef args res rs1 rs2 m t m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args -> rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> step (Callstate s (External ef) rs1 m) diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index b766ed0d..b8232971 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -407,12 +407,12 @@ Qed. (** [frame_match] is preserved by external calls. *) Lemma frame_match_external_call: - forall fr sp base mm ms mm' ms' ef vargs vres t vargs' vres', + forall symb fr sp base mm ms mm' ms' ef vargs vres t vargs' vres', frame_match fr sp base mm ms -> Mem.extends mm ms -> - external_call ef vargs mm t vres mm' -> + external_call ef symb vargs mm t vres mm' -> Mem.extends mm' ms' -> - external_call ef vargs' ms t vres' ms' -> + external_call ef symb vargs' ms t vres' ms' -> mem_unchanged_on (loc_out_of_bounds mm) ms ms' -> frame_match fr sp base mm' ms'. Proof. @@ -420,7 +420,7 @@ Proof. eapply external_call_valid_block; eauto. eapply external_call_valid_block; eauto. auto. - rewrite (external_call_bounds _ _ _ _ _ _ _ H1); auto. + rewrite (external_call_bounds _ _ _ _ _ _ _ _ H1); auto. red; intros. apply A; auto. red. omega. intros. exploit fm_contents_match0; eauto. intros [v [C D]]. exists v; split; auto. @@ -814,9 +814,9 @@ Lemma match_stacks_external_call: match_stacks s ts mm ms -> forall ef vargs t vres mm' ms' vargs' vres', Mem.extends mm ms -> - external_call ef vargs mm t vres mm' -> + external_call ef (Genv.find_symbol ge) vargs mm t vres mm' -> Mem.extends mm' ms' -> - external_call ef vargs' ms t vres' ms' -> + external_call ef (Genv.find_symbol ge) vargs' ms t vres' ms' -> mem_unchanged_on (loc_out_of_bounds mm) ms ms' -> match_stacks s ts mm' ms'. Proof. diff --git a/backend/Machconcr.v b/backend/Machconcr.v index a6be4bc2..90d08f1f 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -233,7 +233,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s fb rs m t rs' ef args res m', Genv.find_funct_ptr ge fb = Some (External ef) -> - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> extcall_arguments rs m (parent_sp s) ef.(ef_sig) args -> rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) -> step (Callstate s fb rs m) diff --git a/backend/Machtyping.v b/backend/Machtyping.v index c2e797ae..b0673ca8 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -285,7 +285,7 @@ Proof. apply wt_empty_frame. econstructor; eauto. apply wt_setreg; auto. - generalize (external_call_well_typed _ _ _ _ _ _ H). + generalize (external_call_well_typed _ _ _ _ _ _ _ H). unfold proj_sig_res, Conventions.loc_result. destruct (sig_res (ef_sig ef)). destruct t0; simpl; auto. diff --git a/backend/RTL.v b/backend/RTL.v index c5d4d7d0..c8220e5d 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -282,7 +282,7 @@ Inductive step: state -> trace -> state -> Prop := m') | exec_function_external: forall s ef args res t m m', - external_call ef args m t res m' -> + external_call ef (Genv.find_symbol ge) args m t res m' -> step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index a15095bd..92f4cc91 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1320,6 +1320,7 @@ Proof. monadInv TF. econstructor; split. left; apply plus_one. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. constructor; auto. (* return *) diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index bf728fae..1fa000c9 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -1310,6 +1310,7 @@ Proof. intros [res' [tm' [A [B [C D]]]]]. left; econstructor; split. apply plus_one. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. simpl. rewrite Locmap.gss. auto. intros. rewrite Locmap.gso. auto. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 1da7884e..0d1a1ee7 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -469,6 +469,10 @@ Proof. econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut. rewrite H. simpl. reflexivity. constructor; auto. + (* external call *) + econstructor; split. + econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. + constructor; auto. Qed. Lemma sel_initial_states: diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index f44eac2e..fbe4b68f 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1574,6 +1574,7 @@ Proof. exploit transl_external_arguments; eauto. intro EXTARGS. econstructor; split. apply plus_one. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. econstructor; eauto. intros. unfold Regmap.set. case (RegEq.eq r (loc_result (ef_sig ef))); intro. rewrite e. rewrite Locmap.gss; auto. rewrite Locmap.gso; auto. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 0ca4c028..0535cbfb 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -557,6 +557,7 @@ Proof. intros [res' [m2' [A [B [C D]]]]]. left. exists (Returnstate s' res' m2'); split. simpl. econstructor; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. constructor; auto. (* returnstate *) diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 4cbcbd4f..3f0a27d0 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -335,6 +335,7 @@ Proof. (* external function *) simpl. left; econstructor; split. eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. simpl. econstructor; eauto. (* return *) inv H3. inv H1. |