From 231899605cb48c695d898ebc68eef03bd27cd870 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 29 May 2018 16:23:01 +0200 Subject: Simplify module Complements and add separate compilation (#121) * Simplify the theorems about preservation of specifications (section 2) There were three theorems, transf_c_program_preserves_spec, _safety_spec, and _liveness_spec) with the first being needlessly general and the last being hard to understand. Plus, the "liveness" and "safety" terminology wasn't very good. Replaced by two theorems: - transf_c_program_preserves_spec, which is the theorem previously named _safety_spec and talks about specifications that exclude going-wrong behaviors; - transf_c_program_preserves_initial_trace, which is an instance of the theorem previously named _liveness_spec, and now talks about a single initial trace of interest rather than a set of such traces. Added named definitions for properties of interest. Added more explanations. * Added theorems that talk about separate compilation (section 3) These are the theorems from section 1 and 2 but reformulated in terms of multiple C source compilation units being separately compiled to Asm units then linked together. --- driver/Complements.v | 246 +++++++++++++++++++++++++++++++++++---------------- 1 file changed, 172 insertions(+), 74 deletions(-) (limited to 'driver/Complements.v') diff --git a/driver/Complements.v b/driver/Complements.v index d1bea1b3..3660fff0 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -13,30 +13,20 @@ (** 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 Behaviors. -Require Import Csyntax. -Require Import Csem. -Require Import Cstrategy. -Require Import Clight. -Require Import Cminor. -Require Import RTL. -Require Import Asm. +Require Import Coqlib Errors. +Require Import AST Linking Events Smallstep Behaviors. +Require Import Csyntax Csem Cstrategy Asm. Require Import Compiler. -Require Import Errors. (** * Preservation of whole-program behaviors *) (** From the simulation diagrams proved in file [Compiler]. it follows that whole-program observable behaviors are preserved in the following sense. First, every behavior of the generated assembly code is matched by - a behavior of the source C code. *) + a behavior of the source C code. The behavior [beh] of the assembly + code is either identical to the behavior [beh'] of the source C code + or ``improves upon'' [beh'] by replacing a ``going wrong'' behavior + with a more defined behavior. *) Theorem transf_c_program_preservation: forall p tp beh, @@ -48,8 +38,9 @@ Proof. apply transf_c_program_correct; auto. Qed. -(** As a corollary, if the source C code cannot go wrong, the behavior of the - generated assembly code is one of the possible behaviors of the source C code. *) +(** As a corollary, if the source C code cannot go wrong, i.e. is free of + undefined behaviors, the behavior of the generated assembly code is + one of the possible behaviors of the source C code. *) Theorem transf_c_program_is_refinement: forall p tp, @@ -124,83 +115,190 @@ Qed. (** * Satisfaction of specifications *) (** The second additional results shows that if all executions - of the source C program satisfies a given specification - (a predicate on the observable behavior of the program), + of the source C program satisfies a given specification, then all executions of the produced Asm program satisfy - this specification as well. - - We first show this result for specifications that are stable - under the [behavior_improves] relation. *) - -Section SPECS_PRESERVED. - -Variable spec: program_behavior -> Prop. + this specification as well. *) + +(** The specifications we consider here are sets of observable + behaviors, representing the good behaviors a program is expected + to have. A specification can be as simple as + ``the program does not go wrong'' or as precise as + ``the program prints a prime number then terminates with code 0''. + As usual in Coq, sets of behaviors are represented as predicates + [program_behavior -> Prop]. *) + +Definition specification := program_behavior -> Prop. + +(** A program satisfies a specification if all its observable behaviors + are in the specification. *) + +Definition c_program_satisfies_spec (p: Csyntax.program) (spec: specification): Prop := + forall beh, program_behaves (Csem.semantics p) beh -> spec beh. +Definition asm_program_satisfies_spec (p: Asm.program) (spec: specification): Prop := + forall beh, program_behaves (Asm.semantics p) beh -> spec beh. + +(** It is not always the case that if the source program satisfies a + specification, then the generated assembly code satisfies it as + well. For example, if the specification is ``the program goes wrong + on an undefined behavior'', a C source that goes wrong satisfies + this specification but can be compiled into Asm code that does not + go wrong and therefore does not satisfy the specification. + + For this reason, we restrict ourselves to safety-enforcing specifications: + specifications that exclude ``going wrong'' behaviors and are satisfied + only by programs that execute safely. *) + +Definition safety_enforcing_specification (spec: specification): Prop := + forall beh, spec beh -> not_wrong beh. -Hypothesis spec_stable: - forall beh1 beh2, behavior_improves beh1 beh2 -> spec beh1 -> spec beh2. +(** As the main result of this section, we show that CompCert + compilation preserves safety-enforcing specifications: + any such specification that is satisfied by the source C program is + always satisfied by the generated assembly code. *) Theorem transf_c_program_preserves_spec: - forall p tp, + forall p tp spec, transf_c_program p = OK tp -> - (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) -> - (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh). + safety_enforcing_specification spec -> + c_program_satisfies_spec p spec -> + asm_program_satisfies_spec tp spec. Proof. - intros. - exploit transf_c_program_preservation; eauto. intros [beh' [A B]]. - apply spec_stable with beh'; auto. + intros p tp spec TRANSF SES CSAT; red; intros beh AEXEC. + exploit transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR). + apply CSAT in CEXEC. destruct IMPR as [EQ | [t [A B]]]. +- congruence. +- subst beh'. apply SES in CEXEC. contradiction. Qed. -End SPECS_PRESERVED. +(** Safety-enforcing specifications are not the only good properties + of source programs that are preserved by compilation. Another example + of a property that is preserved is the ``initial trace'' property: + all executions of the program start by producing an expected trace + of I/O actions, representing the good behavior expected from the program. + After that, the program may terminate, or continue running, or go wrong + on an undefined behavior. What matters is that the program produced + the expected trace at the beginning of its execution. This is a typical + liveness property, and it is preserved by compilation. *) + +Definition c_program_has_initial_trace (p: Csyntax.program) (t: trace): Prop := + forall beh, program_behaves (Csem.semantics p) beh -> behavior_prefix t beh. +Definition asm_program_has_initial_trace (p: Asm.program) (t: trace): Prop := + forall beh, program_behaves (Asm.semantics p) beh -> behavior_prefix t beh. + +Theorem transf_c_program_preserves_initial_trace: + forall p tp t, + transf_c_program p = OK tp -> + c_program_has_initial_trace p t -> + asm_program_has_initial_trace tp t. +Proof. + intros p tp t TRANSF CTRACE; red; intros beh AEXEC. + exploit transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR). + apply CTRACE in CEXEC. destruct IMPR as [EQ | [t' [A B]]]. +- congruence. +- destruct CEXEC as (beh1' & EQ'). + destruct B as (beh1 & EQ). + subst beh'. destruct beh1'; simpl in A; inv A. + exists (behavior_app t0 beh1). apply behavior_app_assoc. +Qed. -(** As a corollary, we obtain preservation of safety specifications: - specifications that exclude "going wrong" behaviors. *) +(** * Extension to separate compilation *) -Section SAFETY_PRESERVED. +(** The results above were given in terms of whole-program compilation. + They also extend to separate compilation followed by linking. *) -Variable spec: program_behavior -> Prop. +Section SEPARATE_COMPILATION. -Hypothesis spec_safety: - forall beh, spec beh -> not_wrong beh. +(** The source: a list of C compilation units *) +Variable c_units: nlist Csyntax.program. -Theorem transf_c_program_preserves_safety_spec: - forall p tp, - transf_c_program p = OK tp -> - (forall beh, program_behaves (Csem.semantics p) beh -> spec beh) -> - (forall beh, program_behaves (Asm.semantics tp) beh -> spec beh). +(** The compiled code: a list of Asm compilation units, obtained by separate compilation *) +Variable asm_units: nlist Asm.program. +Hypothesis separate_compilation_succeeds: + nlist_forall2 (fun cu tcu => transf_c_program cu = OK tcu) c_units asm_units. + +(** We assume that the source C compilation units can be linked together + to obtain a monolithic C program [c_program]. *) +Variable c_program: Csyntax.program. +Hypothesis source_linking: link_list c_units = Some c_program. + +(** Then, linking the Asm units obtained by separate compilation succeeds. *) +Lemma compiled_linking_succeeds: + { asm_program | link_list asm_units = Some asm_program }. Proof. - intros. eapply transf_c_program_preserves_spec; eauto. - intros. destruct H2. congruence. destruct H2 as [t [EQ1 EQ2]]. - subst beh1. elim (spec_safety _ H3). + destruct (link_list asm_units) eqn:E. +- exists p; auto. +- exfalso. + exploit separate_transf_c_program_correct; eauto. intros (a & P & Q). + congruence. Qed. -End SAFETY_PRESERVED. +(** Let asm_program be the result of linking the Asm units. *) +Let asm_program: Asm.program := proj1_sig compiled_linking_succeeds. +Let compiled_linking: link_list asm_units = Some asm_program := proj2_sig compiled_linking_succeeds. + +(** Then, [asm_program] preserves the semantics and the specifications of + [c_program], in the following sense. + First, every behavior of [asm_program] improves upon one of the possible + behaviors of [c_program]. *) -(** We also have preservation of liveness specifications: - specifications that assert the existence of a prefix of the observable - trace satisfying some conditions. *) +Theorem separate_transf_c_program_preservation: + forall beh, + program_behaves (Asm.semantics asm_program) beh -> + exists beh', program_behaves (Csem.semantics c_program) beh' /\ behavior_improves beh' beh. +Proof. + intros. exploit separate_transf_c_program_correct; eauto. intros (a & P & Q). + assert (a = asm_program) by congruence. subst a. + eapply backward_simulation_behavior_improves; eauto. +Qed. -Section LIVENESS_PRESERVED. +(** As a corollary, if [c_program] is free of undefined behaviors, + the behavior of [asm_program] is one of the possible behaviors of [c_program]. *) -Variable spec: trace -> Prop. +Theorem separate_transf_c_program_is_refinement: + (forall beh, program_behaves (Csem.semantics c_program) beh -> not_wrong beh) -> + (forall beh, program_behaves (Asm.semantics asm_program) beh -> program_behaves (Csem.semantics c_program) beh). +Proof. + intros. exploit separate_transf_c_program_preservation; eauto. intros (beh' & P & Q). + assert (not_wrong beh') by auto. + inv Q. +- auto. +- destruct H2 as (t & U & V). subst beh'. elim H1. +Qed. -Definition liveness_spec_satisfied (b: program_behavior) : Prop := - exists t, behavior_prefix t b /\ spec t. +(** We now show that if all executions of [c_program] satisfy a specification, + then all executions of [asm_program] also satisfy the specification, provided + the specification is of the safety-enforcing kind. *) -Theorem transf_c_program_preserves_liveness_spec: - forall p tp, - transf_c_program p = OK tp -> - (forall beh, program_behaves (Csem.semantics p) beh -> liveness_spec_satisfied beh) -> - (forall beh, program_behaves (Asm.semantics tp) beh -> liveness_spec_satisfied beh). +Theorem separate_transf_c_program_preserves_spec: + forall spec, + safety_enforcing_specification spec -> + c_program_satisfies_spec c_program spec -> + asm_program_satisfies_spec asm_program spec. Proof. - intros. eapply transf_c_program_preserves_spec; eauto. - intros. destruct H3 as [t1 [A B]]. destruct H2. - subst. exists t1; auto. - destruct H2 as [t [C D]]. subst. - destruct A as [b1 E]. destruct D as [b2 F]. - destruct b1; simpl in E; inv E. - exists t1; split; auto. - exists (behavior_app t0 b2); apply behavior_app_assoc. + intros spec SES CSAT; red; intros beh AEXEC. + exploit separate_transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR). + apply CSAT in CEXEC. destruct IMPR as [EQ | [t [A B]]]. +- congruence. +- subst beh'. apply SES in CEXEC. contradiction. Qed. -End LIVENESS_PRESERVED. +(** As another corollary of [separate_transf_c_program_preservation], + if all executions of [c_program] have a trace [t] as initial trace, + so do all executions of [asm_program]. *) + +Theorem separate_transf_c_program_preserves_initial_trace: + forall t, + c_program_has_initial_trace c_program t -> + asm_program_has_initial_trace asm_program t. +Proof. + intros t CTRACE; red; intros beh AEXEC. + exploit separate_transf_c_program_preservation; eauto. intros (beh' & CEXEC & IMPR). + apply CTRACE in CEXEC. destruct IMPR as [EQ | [t' [A B]]]. +- congruence. +- destruct CEXEC as (beh1' & EQ'). + destruct B as (beh1 & EQ). + subst beh'. destruct beh1'; simpl in A; inv A. + exists (behavior_app t0 beh1). apply behavior_app_assoc. +Qed. +End SEPARATE_COMPILATION. -- cgit