From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Complements.v | 651 --------------------------------------------------- common/Main.v | 305 ------------------------ 2 files changed, 956 deletions(-) delete mode 100644 common/Complements.v delete mode 100644 common/Main.v (limited to 'common') diff --git a/common/Complements.v b/common/Complements.v deleted file mode 100644 index 6df488fc..00000000 --- a/common/Complements.v +++ /dev/null @@ -1,651 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Corollaries of the main semantic preservation theorem. *) - -Require Import Classical. -Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Csyntax. -Require Import Csem. -Require Import PPC. -Require Import Main. -Require Import Errors. - -(** * Determinism of PPC semantics *) - -(** In this section, we show that the semantics for the PPC language - are deterministic, in a sense to be made precise later. - There are two sources of apparent non-determinism: -- The semantics leaves unspecified the results of calls to external - functions. Different results to e.g. a "read" operation can of - course lead to different behaviors for the program. - We address this issue by modeling a notion of deterministic - external world that uniquely determines the results of external calls. -- For diverging executions, the trace of I/O events is not uniquely - determined: it can contain events that will never be performed - because the program diverges earlier. We address this issue - by showing the existence of a minimal trace for diverging executions. - -*) - -(** ** Deterministic worlds *) - -(** An external world is a function that, given the name of an - external call and its arguments, returns either [None], meaning - that this external call gets stuck, or [Some(r,w)], meaning - that this external call succeeds, has result [r], and changes - the world to [w]. *) - -Inductive world: Set := - World: (ident -> list eventval -> option (eventval * world)) -> world. - -Definition nextworld (w: world) (evname: ident) (evargs: list eventval) : - option (eventval * world) := - match w with World f => f evname evargs end. - -(** A trace is possible in a given world if all events correspond - to non-stuck external calls according to the given world. - Two predicates are defined, for finite and infinite traces respectively: -- [possible_trace w t w'], where [w] is the initial state of the - world, [t] the finite trace of interest, and [w'] the state of the - world after performing trace [t]. -- [possible_traceinf w T], where [w] is the initial state of the - world and [T] the possibly infinite trace of interest. -*) - -Inductive possible_trace: world -> trace -> world -> Prop := - | possible_trace_nil: forall w, - possible_trace w E0 w - | possible_trace_cons: forall w0 evname evargs evres w1 t w2, - nextworld w0 evname evargs = Some (evres, w1) -> - possible_trace w1 t w2 -> - possible_trace w0 (mkevent evname evargs evres :: t) w2. - -Lemma possible_trace_app: - forall t2 w2 w0 t1 w1, - possible_trace w0 t1 w1 -> possible_trace w1 t2 w2 -> - possible_trace w0 (t1 ** t2) w2. -Proof. - induction 1; simpl; intros. - auto. - econstructor; eauto. -Qed. - -Lemma possible_trace_app_inv: - forall t2 w2 t1 w0, - possible_trace w0 (t1 ** t2) w2 -> - exists w1, possible_trace w0 t1 w1 /\ possible_trace w1 t2 w2. -Proof. - induction t1; simpl; intros. - exists w0; split. constructor. auto. - inv H. exploit IHt1; eauto. intros [w1 [A B]]. - exists w1; split. econstructor; eauto. auto. -Qed. - -CoInductive possible_traceinf: world -> traceinf -> Prop := - | possible_traceinf_nil: forall w0, - possible_traceinf w0 Enilinf - | possible_traceinf_cons: forall w0 evname evargs evres w1 T, - nextworld w0 evname evargs = Some (evres, w1) -> - possible_traceinf w1 T -> - possible_traceinf w0 (Econsinf (mkevent evname evargs evres) T). - -Lemma possible_traceinf_app: - forall t2 w0 t1 w1, - possible_trace w0 t1 w1 -> possible_traceinf w1 t2 -> - possible_traceinf w0 (t1 *** t2). -Proof. - induction 1; simpl; intros. - auto. - econstructor; eauto. -Qed. - -Lemma possible_traceinf_app_inv: - forall t2 t1 w0, - possible_traceinf w0 (t1 *** t2) -> - exists w1, possible_trace w0 t1 w1 /\ possible_traceinf w1 t2. -Proof. - induction t1; simpl; intros. - exists w0; split. constructor. auto. - inv H. exploit IHt1; eauto. intros [w1 [A B]]. - exists w1; split. econstructor; eauto. auto. -Qed. - -Ltac possibleTraceInv := - match goal with - | [H: possible_trace _ (_ ** _) _ |- _] => - let P1 := fresh "P" in - let w := fresh "w" in - let P2 := fresh "P" in - elim (possible_trace_app_inv _ _ _ _ H); clear H; - intros w [P1 P2]; - possibleTraceInv - | [H: possible_traceinf _ (_ *** _) |- _] => - let P1 := fresh "P" in - let w := fresh "w" in - let P2 := fresh "P" in - elim (possible_traceinf_app_inv _ _ _ H); clear H; - intros w [P1 P2]; - possibleTraceInv - | _ => idtac - end. - -(** Determinism properties of [event_match]. *) - -Remark eventval_match_deterministic: - forall ev1 ev2 ty v1 v2, - eventval_match ev1 ty v1 -> eventval_match ev2 ty v2 -> - (ev1 = ev2 <-> v1 = v2). -Proof. - intros. inv H; inv H0; intuition congruence. -Qed. - -Remark eventval_list_match_deterministic: - forall ev1 ty v, eventval_list_match ev1 ty v -> - forall ev2, eventval_list_match ev2 ty v -> ev1 = ev2. -Proof. - induction 1; intros. - inv H. auto. - inv H1. decEq. - rewrite (eventval_match_deterministic _ _ _ _ _ H H6). auto. - eauto. -Qed. - -Lemma event_match_deterministic: - forall w0 t1 w1 t2 w2 ef vargs vres1 vres2, - possible_trace w0 t1 w1 -> - possible_trace w0 t2 w2 -> - event_match ef vargs t1 vres1 -> - event_match ef vargs t2 vres2 -> - vres1 = vres2 /\ t1 = t2 /\ w1 = w2. -Proof. - intros. inv H1. inv H2. - assert (eargs = eargs0). eapply eventval_list_match_deterministic; eauto. subst eargs0. - inv H. inv H12. inv H0. inv H12. - rewrite H11 in H10. inv H10. intuition. - rewrite <- (eventval_match_deterministic _ _ _ _ _ H4 H5). auto. -Qed. - -(** ** Determinism of PPC transitions. *) - -Remark extcall_arguments_deterministic: - forall rs m sg args args', - extcall_arguments rs m sg args -> - extcall_arguments rs m sg args' -> args = args'. -Proof. - assert ( - forall rs m tyl iregl fregl ofs args, - extcall_args rs m tyl iregl fregl ofs args -> - forall args', extcall_args rs m tyl iregl fregl ofs args' -> args = args'). - induction 1; intros. - inv H. auto. - inv H1. decEq; eauto. - inv H1. decEq. congruence. eauto. - inv H1. decEq; eauto. - inv H1. decEq. congruence. eauto. - - unfold extcall_arguments; intros; eauto. -Qed. - -Lemma step_deterministic: - forall ge s0 t1 s1 t2 s2 w0 w1 w2, - step ge s0 t1 s1 -> step ge s0 t2 s2 -> - possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 -> - s1 = s2 /\ t1 = t2 /\ w1 = w2. -Proof. - intros. inv H; inv H0. - assert (c0 = c) by congruence. subst c0. - assert (i0 = i) by congruence. subst i0. - split. congruence. split. auto. inv H1; inv H2; auto. - congruence. - congruence. - assert (ef0 = ef) by congruence. subst ef0. - assert (args0 = args). eapply extcall_arguments_deterministic; eauto. subst args0. - exploit event_match_deterministic. eexact H1. eexact H2. eauto. eauto. - intros [A [B C]]. intuition congruence. -Qed. - -Lemma initial_state_deterministic: - forall p s1 s2, - initial_state p s1 -> initial_state p s2 -> s1 = s2. -Proof. - intros. inv H; inv H0. reflexivity. -Qed. - -Lemma final_state_not_step: - forall ge st r t st', final_state st r -> step ge st t st' -> False. -Proof. - intros. inv H. inv H0. - unfold Vzero in H1. congruence. - unfold Vzero in H1. congruence. -Qed. - -Lemma final_state_deterministic: - forall st r1 r2, final_state st r1 -> final_state st r2 -> r1 = r2. -Proof. - intros. inv H; inv H0. congruence. -Qed. - -(** ** Determinism for terminating executions. *) - -(* -Lemma star_star_inv: - forall ge s t1 s1, star step ge s t1 s1 -> - forall t2 s2 w w1 w2, star step ge s t2 s2 -> - possible_trace w t1 w1 -> possible_trace w t2 w2 -> - exists t, (star step ge s1 t s2 /\ t2 = t1 ** t) - \/ (star step ge s2 t s1 /\ t1 = t2 ** t). -Proof. - induction 1; intros. - exists t2; left; split; auto. - inv H2. exists (t1 ** t2); right; split. econstructor; eauto. auto. - possibleTraceInv. - exploit step_deterministic. eexact H. eexact H5. eauto. eauto. - intros [U [V W]]. subst s5 t3 w3. - exploit IHstar; eauto. intros [t [ [Q R] | [Q R] ]]. - subst t4. exists t; left; split. auto. traceEq. - subst t2. exists t; right; split. auto. traceEq. -Qed. -*) - -Lemma steps_deterministic: - forall ge s0 t1 s1, star step ge s0 t1 s1 -> - forall r1 r2 t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> - final_state s1 r1 -> final_state s2 r2 -> - possible_trace w0 t1 w1 -> possible_trace w0 t2 w2 -> - t1 = t2 /\ r1 = r2. -Proof. - induction 1; intros. - inv H. split. auto. eapply final_state_deterministic; eauto. - byContradiction. eapply final_state_not_step with (st := s); eauto. - inv H2. byContradiction. eapply final_state_not_step with (st := s0); eauto. - possibleTraceInv. - exploit step_deterministic. eexact H. eexact H7. eauto. eauto. - intros [A [B C]]. subst s5 t3 w3. - exploit IHstar. eexact H8. eauto. eauto. eauto. eauto. - intros [A B]. subst t4 r2. - auto. -Qed. - -(** ** Determinism for infinite transition sequences. *) - -Lemma forever_star_inv: - forall ge s t s', star step ge s t s' -> - forall T w w', forever step ge s T -> - possible_trace w t w' -> possible_traceinf w T -> - exists T', - forever step ge s' T' /\ possible_traceinf w' T' /\ T = t *** T'. -Proof. - induction 1; intros. - inv H0. exists T; auto. - subst t. possibleTraceInv. - inv H2. possibleTraceInv. - exploit step_deterministic. - eexact H. eexact H1. eauto. eauto. intros [A [B C]]; subst s4 t1 w1. - exploit IHstar; eauto. intros [T' [A [B C]]]. - exists T'; split. auto. - split. auto. - rewrite C. rewrite Eappinf_assoc; auto. -Qed. - -Lemma star_final_not_forever: - forall ge s1 t s2 r T w1 w2, - star step ge s1 t s2 -> - final_state s2 r -> forever step ge s1 T -> - possible_trace w1 t w2 -> possible_traceinf w1 T -> - False. -Proof. - intros. exploit forever_star_inv; eauto. intros [T' [A [B C]]]. - inv A. eapply final_state_not_step; eauto. -Qed. - -(** ** Minimal traces for divergence. *) - -(** There are two mutually exclusive way in which a program can diverge. - It can diverge in a reactive fashion: it performs infinitely many - external calls, and the internal computations between two external - calls are always finite. Or it can diverge silently: after a finite - number of external calls, it enters an infinite sequence of internal - computations. *) - -Definition reactive (ge: genv) (s: state) (w: world) := - forall t s1 w1, - star step ge s t s1 -> possible_trace w t w1 -> - exists s2, exists t', exists s3, exists w2, - star step ge s1 E0 s2 - /\ step ge s2 t' s3 - /\ possible_trace w1 t' w2 - /\ t' <> E0. - -Definition diverges_silently (ge: genv) (s: state) := - forall s2, star step ge s E0 s2 -> exists s3, step ge s2 E0 s3. - -Definition diverges_eventually (ge: genv) (s: state) (w: world) := - exists t, exists s1, exists w1, - star step ge s t s1 /\ possible_trace w t w1 /\ diverges_silently ge s1. - -(** Using classical logic, we show that any infinite sequence of transitions - that is possible in a deterministic world is of one of the two forms - described above. *) - -Lemma reactive_or_diverges: - forall ge s T w, - forever step ge s T -> possible_traceinf w T -> - reactive ge s w \/ diverges_eventually ge s w. -Proof. - intros. elim (classic (diverges_eventually ge s w)); intro. - right; auto. - left. red; intros. - generalize (not_ex_all_not trace _ H1 t). - intro. clear H1. - generalize (not_ex_all_not state _ H4 s1). - intro. clear H4. - generalize (not_ex_all_not world _ H1 w1). - intro. clear H1. - elim (not_and_or _ _ H4); clear H4; intro. - contradiction. - elim (not_and_or _ _ H1); clear H1; intro. - contradiction. - generalize (not_all_ex_not state _ H1). intros [s2 A]. clear H1. - destruct (imply_to_and _ _ A). clear A. - exploit forever_star_inv. - eapply star_trans. eexact H2. eexact H1. reflexivity. - eauto. rewrite E0_right. eauto. eauto. - intros [T' [A [B C]]]. - inv A. possibleTraceInv. - exists s2; exists t0; exists s3; exists w4. intuition. - subst t0. apply H4. exists s3; auto. -Qed. - -(** Moreover, a program cannot be both reactive and silently diverging. *) - -Lemma reactive_not_diverges: - forall ge s w, - reactive ge s w -> diverges_eventually ge s w -> False. -Proof. - intros. destruct H0 as [t [s1 [w1 [A [B C]]]]]. - destruct (H _ _ _ A B) as [s2 [t' [s3 [w2 [P [Q [R S]]]]]]]. - destruct (C _ P) as [s4 T]. - assert (s3 = s4 /\ t' = E0 /\ w2 = w1). - eapply step_deterministic; eauto. constructor. - intuition congruence. -Qed. - -(** A program that silently diverges can be given any finite or - infinite trace of events. In particular, taking [T' = Enilinf], - it can be given the empty trace of events. *) - -Lemma diverges_forever: - forall ge s1 T w T', - diverges_silently ge s1 -> - forever step ge s1 T -> - possible_traceinf w T -> - forever step ge s1 T'. -Proof. - cofix COINDHYP; intros. inv H0. possibleTraceInv. - assert (exists s3, step ge s1 E0 s3). apply H. constructor. - destruct H0 as [s3 C]. - assert (s2 = s3 /\ t = E0 /\ w0 = w). eapply step_deterministic; eauto. constructor. - destruct H0 as [Q [R S]]. subst s3 t w0. - change T' with (E0 *** T'). econstructor. eassumption. - eapply COINDHYP; eauto. - red; intros. apply H. eapply star_left; eauto. -Qed. - -(** The trace of I/O events generated by a reactive diverging program - is uniquely determined up to bisimilarity. *) - -Lemma reactive_sim: - forall ge s w T1 T2, - reactive ge s w -> - forever step ge s T1 -> - forever step ge s T2 -> - possible_traceinf w T1 -> - possible_traceinf w T2 -> - traceinf_sim T1 T2. -Proof. - cofix COINDHYP; intros. - elim (H E0 s w); try constructor. - intros s2 [t' [s3 [w2 [A [B [C D]]]]]]. - assert (star step ge s t' s3). eapply star_right; eauto. - destruct (forever_star_inv _ _ _ _ H4 _ _ _ H0 C H2) - as [T1' [P [Q R]]]. - destruct (forever_star_inv _ _ _ _ H4 _ _ _ H1 C H3) - as [T2' [S [T U]]]. - destruct t'. unfold E0 in D. congruence. - assert (t' = nil). inversion B. inversion H7. auto. subst t'. - subst T1 T2. simpl. constructor. - apply COINDHYP with ge s3 w2; auto. - red; intros. eapply H. eapply star_trans; eauto. - eapply possible_trace_app; eauto. -Qed. - -(** A trace is minimal for a program if it is a prefix of all possible - traces. *) - -Definition minimal_trace (ge: genv) (s: state) (w: world) (T: traceinf) := - forall T', - forever step ge s T' -> possible_traceinf w T' -> - traceinf_prefix T T'. - -(** For any program that diverges with some possible trace [T1], - the set of possible traces admits a minimal element [T]. - If the program is reactive, this trace is [T1]. - If the program silently diverges, this trace is the finite trace - of events performed prior to silent divergence. *) - -Lemma forever_minimal_trace: - forall ge s T1 w, - forever step ge s T1 -> possible_traceinf w T1 -> - exists T, - forever step ge s T - /\ possible_traceinf w T - /\ minimal_trace ge s w T. -Proof. - intros. - destruct (reactive_or_diverges _ _ _ _ H H0). - (* reactive *) - exists T1; split. auto. split. auto. red; intros. - elim (reactive_or_diverges _ _ _ _ H2 H3); intro. - apply traceinf_sim_prefix. eapply reactive_sim; eauto. - elimtype False. eapply reactive_not_diverges; eauto. - (* diverges *) - elim H1. intros t [s1 [w1 [A [B C]]]]. - exists (t *** Enilinf); split. - exploit forever_star_inv; eauto. intros [T' [P [Q R]]]. - eapply star_forever. eauto. - eapply diverges_forever; eauto. - split. eapply possible_traceinf_app. eauto. constructor. - red; intros. exploit forever_star_inv. eauto. eexact H2. eauto. eauto. - intros [T2 [P [Q R]]]. - subst T'. apply traceinf_prefix_app. constructor. -Qed. - -(** ** Refined semantics for program executions. *) - -(** We now define the following variant [exec_program'] of the - [exec_program] predicate defined in module [Smallstep]. - In the diverging case [Diverges T], the new predicate imposes that the - finite or infinite trace [T] is minimal. *) - -Inductive exec_program' (p: program) (w: world): program_behavior -> Prop := - | program_terminates': forall s t s' w' r, - initial_state p s -> - star step (Genv.globalenv p) s t s' -> - possible_trace w t w' -> - final_state s' r -> - exec_program' p w (Terminates t r) - | program_diverges': forall s T, - initial_state p s -> - forever step (Genv.globalenv p) s T -> - possible_traceinf w T -> - minimal_trace (Genv.globalenv p) s w T -> - exec_program' p w (Diverges T). - -(** We show that any [exec_program] execution corresponds to - an [exec_program'] execution. *) - -Definition possible_behavior (w: world) (b: program_behavior) : Prop := - match b with - | Terminates t r => exists w', possible_trace w t w' - | Diverges T => possible_traceinf w T - end. - -Inductive matching_behaviors: program_behavior -> program_behavior -> Prop := - | matching_behaviors_terminates: forall t r, - matching_behaviors (Terminates t r) (Terminates t r) - | matching_behaviors_diverges: forall T1 T2, - traceinf_prefix T2 T1 -> - matching_behaviors (Diverges T1) (Diverges T2). - -Theorem exec_program_program': - forall p b w, - exec_program p b -> possible_behavior w b -> - exists b', exec_program' p w b' /\ matching_behaviors b b'. -Proof. - intros. inv H; simpl in H0. - (* termination *) - destruct H0 as [w' A]. - exists (Terminates t r). - split. econstructor; eauto. constructor. - (* divergence *) - exploit forever_minimal_trace; eauto. intros [T0 [A [B C]]]. - exists (Diverges T0); split. - econstructor; eauto. - constructor. apply C; auto. -Qed. - -(** Moreover, [exec_program'] is deterministic, in that the behavior - associated with a given program and external world is uniquely - defined up to bisimilarity between infinite traces. *) - -Inductive same_behaviors: program_behavior -> program_behavior -> Prop := - | same_behaviors_terminates: forall t r, - same_behaviors (Terminates t r) (Terminates t r) - | same_behaviors_diverges: forall T1 T2, - traceinf_sim T2 T1 -> - same_behaviors (Diverges T1) (Diverges T2). - -Theorem exec_program'_deterministic: - forall p b1 b2 w, - exec_program' p w b1 -> exec_program' p w b2 -> - same_behaviors b1 b2. -Proof. - intros. inv H; inv H0; - assert (s0 = s) by (eapply initial_state_deterministic; eauto); subst s0. - (* terminates, terminates *) - exploit steps_deterministic. eexact H2. eexact H5. eauto. eauto. eauto. eauto. - intros [A B]. subst. constructor. - (* terminates, diverges *) - byContradiction. eapply star_final_not_forever; eauto. - (* diverges, terminates *) - byContradiction. eapply star_final_not_forever; eauto. - (* diverges, diverges *) - constructor. apply traceinf_prefix_2_sim; auto. -Qed. - -Lemma matching_behaviors_same: - forall b b1' b2', - matching_behaviors b b1' -> same_behaviors b1' b2' -> - matching_behaviors b b2'. -Proof. - intros. inv H; inv H0. - constructor. - constructor. apply traceinf_prefix_compat with T2 T1. - auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl. -Qed. - -(** * Additional semantic preservation property *) - -(** Combining the semantic preservation theorem from module [Main] - with the determinism of PPC executions, we easily obtain - additional, stronger semantic preservation properties. - The first property states that, when compiling a Clight - program that has well-defined semantics, all possible executions - of the resulting PPC code correspond to an execution of - the source Clight program, in the sense of the [matching_behaviors] - predicate. *) - -Theorem transf_c_program_correct_strong: - forall p tp b w, - transf_c_program p = OK tp -> - Csem.exec_program p b -> - possible_behavior w b -> - (exists b', exec_program' tp w b') -/\(forall b', exec_program' tp w b' -> - exists b0, Csem.exec_program p b0 /\ matching_behaviors b0 b'). -Proof. - intros. - assert (PPC.exec_program tp b). - eapply transf_c_program_correct; eauto. - exploit exec_program_program'; eauto. - intros [b' [A B]]. - split. exists b'; auto. - intros. exists b. split. auto. - apply matching_behaviors_same with b'. auto. - eapply exec_program'_deterministic; eauto. -Qed. - -Section SPECS_PRESERVED. - -(** The second additional results shows that if one execution - of the source Clight program satisfies a given specification - (a predicate on the observable behavior of the program), - then all executions of the produced PPC program satisfy - this specification as well. *) - -Variable spec: program_behavior -> Prop. - -(* Since the execution trace for a diverging Clight program - is not uniquely defined (the trace can contain events that - the program will never perform because it loops earlier), - this result holds only if the specification is closed under - prefixes in the case of diverging executions. This is the - case for all safety properties (some undesirable event never - occurs), but not for liveness properties (some desirable event - always occurs). *) - -Hypothesis spec_safety: - forall T T', traceinf_prefix T T' -> spec (Diverges T') -> spec (Diverges T). - -Theorem transf_c_program_preserves_spec: - forall p tp b w, - transf_c_program p = OK tp -> - Csem.exec_program p b -> - possible_behavior w b -> - spec b -> - (exists b', exec_program' tp w b') -/\(forall b', exec_program' tp w b' -> spec b'). -Proof. - intros. - assert (PPC.exec_program tp b). - eapply transf_c_program_correct; eauto. - exploit exec_program_program'; eauto. - intros [b' [A B]]. - split. exists b'; auto. - intros b'' EX. - assert (same_behaviors b' b''). eapply exec_program'_deterministic; eauto. - inv B; inv H4. - auto. - apply spec_safety with T1. - eapply traceinf_prefix_compat with T2 T1. - auto. apply traceinf_sim_sym; auto. apply traceinf_sim_refl. - auto. -Qed. - -End SPECS_PRESERVED. diff --git a/common/Main.v b/common/Main.v deleted file mode 100644 index f50640ae..00000000 --- a/common/Main.v +++ /dev/null @@ -1,305 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** The whole compiler and its proof of semantic preservation *) - -(** Libraries. *) -Require Import Coqlib. -Require Import Maps. -Require Import Errors. -Require Import AST. -Require Import Values. -Require Import Smallstep. -(** Languages (syntax and semantics). *) -Require Csyntax. -Require Csem. -Require Csharpminor. -Require Cminor. -Require CminorSel. -Require RTL. -Require LTL. -Require LTLin. -Require Linear. -Require Mach. -Require PPC. -(** Translation passes. *) -Require Cshmgen. -Require Cminorgen. -Require Selection. -Require RTLgen. -Require Constprop. -Require CSE. -Require Allocation. -Require Tunneling. -Require Linearize. -Require Reload. -Require Stacking. -Require PPCgen. -(** Type systems. *) -Require Ctyping. -Require RTLtyping. -Require LTLtyping. -Require LTLintyping. -Require Lineartyping. -Require Machtyping. -(** Proofs of semantic preservation and typing preservation. *) -Require Cshmgenproof3. -Require Cminorgenproof. -Require Selectionproof. -Require RTLgenproof. -Require Constpropproof. -Require CSEproof. -Require Allocproof. -Require Alloctyping. -Require Tunnelingproof. -Require Tunnelingtyping. -Require Linearizeproof. -Require Linearizetyping. -Require Reloadproof. -Require Reloadtyping. -Require Stackingproof. -Require Stackingtyping. -Require Machabstr2concr. -Require PPCgenproof. - -Open Local Scope string_scope. - -(** * Composing the translation passes *) - -(** We first define useful monadic composition operators, - along with funny (but convenient) notations. *) - -Definition apply_total (A B: Set) (x: res A) (f: A -> B) : res B := - match x with Error msg => Error msg | OK x1 => OK (f x1) end. - -Definition apply_partial (A B: Set) - (x: res A) (f: A -> res B) : res B := - match x with Error msg => Error msg | OK x1 => f x1 end. - -Notation "a @@@ b" := - (apply_partial _ _ a b) (at level 50, left associativity). -Notation "a @@ b" := - (apply_total _ _ a b) (at level 50, left associativity). - -(** We define three translation functions for whole programs: one - starting with a C program, one with a Cminor program, one with an - RTL program. The three translations produce PPC programs ready for - pretty-printing and assembling. - - There are two ways to compose the compiler passes. The first - translates every function from the Cminor program from Cminor to - RTL, then to LTL, etc, all the way to PPC, and iterates this - transformation for every function. The second translates the whole - Cminor program to a RTL program, then to an LTL program, etc. - Between Cminor and PPC, we follow the first approach because it has - lower memory requirements. The translation from Clight to PPC - follows the second approach. - - The translation of an RTL function to a PPC function is as follows. *) - -Definition transf_rtl_fundef (f: RTL.fundef) : res PPC.fundef := - OK f - @@ Constprop.transf_fundef - @@ CSE.transf_fundef - @@@ Allocation.transf_fundef - @@ Tunneling.tunnel_fundef - @@@ Linearize.transf_fundef - @@ Reload.transf_fundef - @@@ Stacking.transf_fundef - @@@ PPCgen.transf_fundef. - -(* Here is the translation of a Cminor function to a PPC function. *) - -Definition transf_cminor_fundef (f: Cminor.fundef) : res PPC.fundef := - OK f - @@ Selection.sel_fundef - @@@ RTLgen.transl_fundef - @@@ transf_rtl_fundef. - -(** The corresponding translations for whole program follow. *) - -Definition transf_rtl_program (p: RTL.program) : res PPC.program := - transform_partial_program transf_rtl_fundef p. - -Definition transf_cminor_program (p: Cminor.program) : res PPC.program := - transform_partial_program transf_cminor_fundef p. - -Definition transf_c_program (p: Csyntax.program) : res PPC.program := - match Ctyping.typecheck_program p with - | false => - Error (msg "Ctyping: type error") - | true => - OK p - @@@ Cshmgen.transl_program - @@@ Cminorgen.transl_program - @@@ transf_cminor_program - end. - -(** The following lemmas help reason over compositions of passes. *) - -Lemma map_partial_compose: - forall (X A B C: Set) - (ctx: X -> errmsg) - (f1: A -> res B) (f2: B -> res C) - (pa: list (X * A)) (pc: list (X * C)), - map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc -> - exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc. -Proof. - induction pa; simpl. - intros. inv H. econstructor; eauto. - intro pc. destruct a as [x a]. - caseEq (f1 a); simpl; try congruence. intros b F1. - caseEq (f2 b); simpl; try congruence. intros c F2 EQ. - monadInv EQ. exploit IHpa; eauto. intros [pb [P Q]]. - rewrite P; simpl. - exists ((x, b) :: pb); split. auto. simpl. rewrite F2. rewrite Q. auto. -Qed. - -Lemma transform_partial_program_compose: - forall (A B C V: Set) - (f1: A -> res B) (f2: B -> res C) - (pa: program A V) (pc: program C V), - transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc -> - exists pb, transform_partial_program f1 pa = OK pb /\ - transform_partial_program f2 pb = OK pc. -Proof. - intros. monadInv H. - exploit map_partial_compose; eauto. intros [xb [P Q]]. - exists (mkprogram xb (prog_main pa) (prog_vars pa)); split. - unfold transform_partial_program. rewrite P; auto. - unfold transform_partial_program. simpl. rewrite Q; auto. -Qed. - -Lemma transform_program_partial_program: - forall (A B V: Set) (f: A -> B) (p: program A V) (tp: program B V), - transform_partial_program (fun x => OK (f x)) p = OK tp -> - transform_program f p = tp. -Proof. - intros until tp. unfold transform_partial_program. - rewrite map_partial_total. simpl. intros. inv H. auto. -Qed. - -Lemma transform_program_compose: - forall (A B C V: Set) - (f1: A -> res B) (f2: B -> C) - (pa: program A V) (pc: program C V), - transform_partial_program (fun f => f1 f @@ f2) pa = OK pc -> - exists pb, transform_partial_program f1 pa = OK pb /\ - transform_program f2 pb = pc. -Proof. - intros. - replace (fun f : A => f1 f @@ f2) - with (fun f : A => f1 f @@@ (fun x => OK (f2 x))) in H. - exploit transform_partial_program_compose; eauto. - intros [pb [X Y]]. exists pb; split. auto. - apply transform_program_partial_program. auto. - apply extensionality; intro. destruct(f1 x); auto. -Qed. - -Lemma transform_partial_program_identity: - forall (A V: Set) (pa pb: program A V), - transform_partial_program (@OK A) pa = OK pb -> - pa = pb. -Proof. - intros until pb. unfold transform_partial_program. - replace (@OK A) with (fun b => @OK A b). - rewrite map_partial_identity. simpl. destruct pa; simpl; congruence. - apply extensionality; auto. -Qed. - -(** * Semantic preservation *) - -(** We prove that the [transf_program] translations preserve semantics. - The proof composes the semantic preservation results for each pass. - This establishes the correctness of the whole compiler! *) - -Theorem transf_rtl_program_correct: - forall p tp beh, - transf_rtl_program p = OK tp -> - RTL.exec_program p beh -> - PPC.exec_program tp beh. -Proof. - intros. unfold transf_rtl_program, transf_rtl_fundef in H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p7 [H7 P7]]. - clear H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H7) as [p6 [H6 P6]]. - clear H7. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]]. - clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]]. - clear H5. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]]. - clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. - clear H3. - destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. - clear H2. - destruct (transform_program_compose _ _ _ _ _ _ _ _ H1) as [p0 [H00 P0]]. - clear H1. - generalize (transform_partial_program_identity _ _ _ _ H00). clear H00. intro. subst p0. - - assert (WT3 : LTLtyping.wt_program p3). - apply Alloctyping.program_typing_preserved with p2. auto. - assert (WT4 : LTLtyping.wt_program p4). - subst p4. apply Tunnelingtyping.program_typing_preserved. auto. - assert (WT5 : LTLintyping.wt_program p5). - apply Linearizetyping.program_typing_preserved with p4. auto. auto. - assert (WT6 : Lineartyping.wt_program p6). - subst p6. apply Reloadtyping.program_typing_preserved. auto. - assert (WT7: Machtyping.wt_program p7). - apply Stackingtyping.program_typing_preserved with p6. auto. auto. - - apply PPCgenproof.transf_program_correct with p7; auto. - apply Machabstr2concr.exec_program_equiv; auto. - apply Stackingproof.transf_program_correct with p6; auto. - subst p6; apply Reloadproof.transf_program_correct; auto. - apply Linearizeproof.transf_program_correct with p4; auto. - subst p4; apply Tunnelingproof.transf_program_correct. - apply Allocproof.transf_program_correct with p2; auto. - subst p2; apply CSEproof.transf_program_correct. - subst p1; apply Constpropproof.transf_program_correct. auto. -Qed. - -Theorem transf_cminor_program_correct: - forall p tp beh, - transf_cminor_program p = OK tp -> - Cminor.exec_program p beh -> - PPC.exec_program tp beh. -Proof. - intros. unfold transf_cminor_program, transf_cminor_fundef in H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H) as [p3 [H3 P3]]. - clear H. - destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. - clear H3. - destruct (transform_program_compose _ _ _ _ _ _ _ _ H2) as [p1 [H1 P1]]. - generalize (transform_partial_program_identity _ _ _ _ H1). clear H1. intro. subst p1. - apply transf_rtl_program_correct with p3. auto. - apply RTLgenproof.transf_program_correct with p2; auto. - rewrite <- P1. apply Selectionproof.transf_program_correct; auto. -Qed. - -Theorem transf_c_program_correct: - forall p tp beh, - transf_c_program p = OK tp -> - Csem.exec_program p beh -> - PPC.exec_program tp beh. -Proof. - intros until beh; unfold transf_c_program; simpl. - caseEq (Ctyping.typecheck_program p); try congruence; intro. - caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. - caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. - intros EQ3 SEM. - eapply transf_cminor_program_correct; eauto. - eapply Cminorgenproof.transl_program_correct; eauto. - eapply Cshmgenproof3.transl_program_correct; eauto. - apply Ctyping.typecheck_program_correct; auto. -Qed. -- cgit