From 5a4bd6f2636df432383bb3144f91816742d2fa53 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 17:16:55 +0000 Subject: Renamed Machconcr into Machsem. Removed Machabstr and Machabstr2concr, now useless following the reengineering of Stacking. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1633 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Stackingproof.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index c32886c6..d651220d 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -30,7 +30,7 @@ Require LTL. Require Import Linear. Require Import Lineartyping. Require Import Mach. -Require Import Machconcr. +Require Import Machsem. Require Import Bounds. Require Import Conventions. Require Import Stacklayout. @@ -2215,7 +2215,7 @@ End EXTERNAL_ARGUMENTS. - Well-typedness of [f]. *) -Inductive match_states: Linear.state -> Machconcr.state -> Prop := +Inductive match_states: Linear.state -> Machsem.state -> Prop := | match_states_intro: forall cs f sp c ls m cs' fb sp' rs m' j tf (MINJ: Mem.inject j m m') @@ -2227,7 +2227,7 @@ Inductive match_states: Linear.state -> Machconcr.state -> Prop := (AGFRAME: agree_frame f j ls (parent_locset cs) m sp m' sp' (parent_sp cs') (parent_ra cs')) (TAIL: is_tail c (Linear.fn_code f)), match_states (Linear.State cs f (Vptr sp Int.zero) c ls m) - (Machconcr.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') + (Machsem.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') | match_states_call: forall cs f ls m cs' fb rs m' j tf (MINJ: Mem.inject j m m') @@ -2239,7 +2239,7 @@ Inductive match_states: Linear.state -> Machconcr.state -> Prop := (AGREGS: agree_regs j ls rs) (AGLOCS: agree_callee_save ls (parent_locset cs)), match_states (Linear.Callstate cs f ls m) - (Machconcr.Callstate cs' fb rs m') + (Machsem.Callstate cs' fb rs m') | match_states_return: forall cs ls m cs' rs m' j sg (MINJ: Mem.inject j m m') @@ -2248,12 +2248,12 @@ Inductive match_states: Linear.state -> Machconcr.state -> Prop := (AGREGS: agree_regs j ls rs) (AGLOCS: agree_callee_save ls (parent_locset cs)), match_states (Linear.Returnstate cs ls m) - (Machconcr.Returnstate cs' rs m'). + (Machsem.Returnstate cs' rs m'). Theorem transf_step_correct: forall s1 t s2, Linear.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), - exists s2', plus Machconcr.step tge s1' t s2' /\ match_states s2 s2'. + exists s2', plus Machsem.step tge s1' t s2' /\ match_states s2 s2'. Proof. assert (RED: forall f i c, transl_code (make_env (function_bounds f)) (i :: c) = @@ -2586,7 +2586,7 @@ Qed. Lemma transf_initial_states: forall st1, Linear.initial_state prog st1 -> - exists st2, Machconcr.initial_state tprog st2 /\ match_states st1 st2. + exists st2, Machsem.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inv H. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. @@ -2614,7 +2614,7 @@ Qed. Lemma transf_final_states: forall st1 st2 r, - match_states st1 st2 -> Linear.final_state st1 r -> Machconcr.final_state st2 r. + match_states st1 st2 -> Linear.final_state st1 r -> Machsem.final_state st2 r. Proof. intros. inv H0. inv H. inv STACKS. constructor. @@ -2624,9 +2624,9 @@ Qed. Theorem transf_program_correct: forall (beh: program_behavior), not_wrong beh -> - Linear.exec_program prog beh -> Machconcr.exec_program tprog beh. + Linear.exec_program prog beh -> Machsem.exec_program tprog beh. Proof. - unfold Linear.exec_program, Machconcr.exec_program; intros. + unfold Linear.exec_program, Machsem.exec_program; intros. eapply simulation_plus_preservation; eauto. eexact transf_initial_states. eexact transf_final_states. -- cgit