diff options
Diffstat (limited to 'backend/CastOptimproof.v')
| -rw-r--r-- | backend/CastOptimproof.v | 577 |
1 files changed, 0 insertions, 577 deletions
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v deleted file mode 100644 index 0afc208c..00000000 --- a/backend/CastOptimproof.v +++ /dev/null @@ -1,577 +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. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for cast optimization. *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Events. -Require Import Memory. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import Lattice. -Require Import Kildall. -Require Import CastOptim. - -(** * Correctness of the static analysis *) - -Section ANALYSIS. - -Definition val_match_approx (a: approx) (v: val) : Prop := - match a with - | Novalue => False - | Int7 => v = Val.zero_ext 8 v /\ v = Val.sign_ext 8 v - | Int8u => v = Val.zero_ext 8 v - | Int8s => v = Val.sign_ext 8 v - | Int15 => v = Val.zero_ext 16 v /\ v = Val.sign_ext 16 v - | Int16u => v = Val.zero_ext 16 v - | Int16s => v = Val.sign_ext 16 v - | Single => v = Val.singleoffloat v - | Unknown => True - end. - -Definition regs_match_approx (a: D.t) (rs: regset) : Prop := - forall r, val_match_approx (D.get r a) rs#r. - -Lemma regs_match_approx_top: - forall rs, regs_match_approx D.top rs. -Proof. - intros. red; intros. simpl. rewrite PTree.gempty. - unfold Approx.top, val_match_approx. auto. -Qed. - -Lemma val_match_approx_increasing: - forall a1 a2 v, - Approx.ge a1 a2 -> val_match_approx a2 v -> val_match_approx a1 v. -Proof. - assert (A: forall v, v = Val.zero_ext 8 v -> v = Val.zero_ext 16 v). - intros. rewrite H. - destruct v; simpl; auto. decEq. symmetry. - apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto. - assert (B: forall v, v = Val.sign_ext 8 v -> v = Val.sign_ext 16 v). - intros. rewrite H. - destruct v; simpl; auto. decEq. symmetry. - apply Int.sign_ext_widen. compute; auto. split. omega. compute; auto. - assert (C: forall v, v = Val.zero_ext 8 v -> v = Val.sign_ext 16 v). - intros. rewrite H. - destruct v; simpl; auto. decEq. symmetry. - apply Int.sign_zero_ext_widen. compute; auto. split. omega. compute; auto. - intros. destruct a1; destruct a2; simpl in *; intuition; auto. -Qed. - -Lemma regs_match_approx_increasing: - forall a1 a2 rs, - D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs. -Proof. - unfold D.ge, regs_match_approx. intros. - apply val_match_approx_increasing with (D.get r a2); auto. -Qed. - -Lemma regs_match_approx_update: - forall ra rs a v r, - val_match_approx a v -> - regs_match_approx ra rs -> - regs_match_approx (D.set r a ra) (rs#r <- v). -Proof. - intros; red; intros. rewrite Regmap.gsspec. - case (peq r0 r); intro. - subst r0. rewrite D.gss. auto. - rewrite D.gso; auto. -Qed. - -Lemma approx_regs_val_list: - forall ra rs rl, - regs_match_approx ra rs -> - list_forall2 val_match_approx (approx_regs ra rl) rs##rl. -Proof. - induction rl; simpl; intros. - constructor. - constructor. apply H. auto. -Qed. - -Lemma analyze_correct: - forall f pc rs pc' i, - f.(fn_code)!pc = Some i -> - In pc' (successors_instr i) -> - regs_match_approx (transfer f pc (analyze f)!!pc) rs -> - regs_match_approx (analyze f)!!pc' rs. -Proof. - intros until i. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with (transfer f pc approxs!!pc). - eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto. - auto. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - -Lemma analyze_correct_start: - forall f rs, - regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs. -Proof. - intros. unfold analyze. - caseEq (DS.fixpoint (successors f) (transfer f) - ((fn_entrypoint f, D.top) :: nil)). - intros approxs; intros. - apply regs_match_approx_increasing with D.top. - eapply DS.fixpoint_entry; eauto. auto with coqlib. - apply regs_match_approx_top. - intros. rewrite PMap.gi. apply regs_match_approx_top. -Qed. - -Lemma approx_bitwise_correct: - forall (sem_op: int -> int -> int) a1 n1 a2 n2, - (forall a b c, sem_op (Int.and a c) (Int.and b c) = Int.and (sem_op a b) c) -> - val_match_approx a1 (Vint n1) -> val_match_approx a2 (Vint n2) -> - val_match_approx (approx_bitwise_op a1 a2) (Vint (sem_op n1 n2)). -Proof. - intros. - assert (forall N, 0 < N < Z_of_nat Int.wordsize -> - sem_op (Int.zero_ext N n1) (Int.zero_ext N n2) = - Int.zero_ext N (sem_op (Int.zero_ext N n1) (Int.zero_ext N n2))). - intros. repeat rewrite Int.zero_ext_and; auto. rewrite H. - rewrite Int.and_assoc. rewrite Int.and_idem. auto. - unfold approx_bitwise_op. - caseEq (Approx.bge Int8u a1 && Approx.bge Int8u a2); intro EQ1. - destruct (andb_prop _ _ EQ1). - assert (V1: val_match_approx Int8u (Vint n1)). - eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto. - assert (V2: val_match_approx Int8u (Vint n2)). - eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto. - simpl in *. inversion V1; inversion V2; decEq. apply H2. compute; auto. - caseEq (Approx.bge Int16u a1 && Approx.bge Int16u a2); intro EQ2. - destruct (andb_prop _ _ EQ2). - assert (V1: val_match_approx Int16u (Vint n1)). - eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto. - assert (V2: val_match_approx Int16u (Vint n2)). - eapply val_match_approx_increasing; eauto. apply Approx.bge_correct; eauto. - simpl in *. inversion V1; inversion V2; decEq. apply H2. compute; auto. - exact I. -Qed. - -Lemma approx_operation_correct: - forall app rs (ge: genv) sp op args m v, - regs_match_approx app rs -> - eval_operation ge sp op rs##args m = Some v -> - val_match_approx (approx_operation op (approx_regs app args)) v. -Proof. - intros. destruct op; simpl; try (exact I). -(* move *) - destruct args; try (exact I). destruct args; try (exact I). - simpl. simpl in H0. inv H0. apply H. -(* const int *) - destruct args; simpl in H0; inv H0. - destruct (Int.eq_dec i (Int.zero_ext 7 i)). red; simpl. - split. - decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto. - decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. - destruct (Int.eq_dec i (Int.zero_ext 8 i)). red; simpl; congruence. - destruct (Int.eq_dec i (Int.sign_ext 8 i)). red; simpl; congruence. - destruct (Int.eq_dec i (Int.zero_ext 15 i)). red; simpl. - split. - decEq. rewrite e. symmetry. apply Int.zero_ext_widen. compute; auto. split. omega. compute; auto. - decEq. rewrite e. symmetry. apply Int.sign_zero_ext_widen. compute; auto. compute; auto. - destruct (Int.eq_dec i (Int.zero_ext 16 i)). red; simpl; congruence. - destruct (Int.eq_dec i (Int.sign_ext 16 i)). red; simpl; congruence. - exact I. -(* const float *) - destruct args; simpl in H0; inv H0. - destruct (Float.eq_dec f (Float.singleoffloat f)). red; simpl; congruence. - exact I. -(* cast8signed *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. symmetry. apply Int.sign_ext_idem. compute; auto. -(* cast8unsigned *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. symmetry. apply Int.zero_ext_idem. compute; auto. -(* cast16signed *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. symmetry. apply Int.sign_ext_idem. compute; auto. -(* cast16unsigned *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. symmetry. apply Int.zero_ext_idem. compute; auto. -(* and *) - destruct args; try (exact I). - destruct args; try (exact I). - destruct args; try (exact I). - generalize (H p) (H p0). simpl in *. FuncInv. subst. - apply approx_bitwise_correct; auto. - intros. repeat rewrite Int.and_assoc. decEq. - rewrite (Int.and_commut b c). rewrite <- Int.and_assoc. rewrite Int.and_idem. auto. -(* or *) - destruct args; try (exact I). - destruct args; try (exact I). - destruct args; try (exact I). - generalize (H p) (H p0). simpl in *. FuncInv. subst. - apply approx_bitwise_correct; auto. - intros. rewrite (Int.and_commut a c); rewrite (Int.and_commut b c). - rewrite <- Int.and_or_distrib. apply Int.and_commut. -(* xor *) - destruct args; try (exact I). - destruct args; try (exact I). - destruct args; try (exact I). - generalize (H p) (H p0). simpl in *. FuncInv. subst. - apply approx_bitwise_correct; auto. - intros. rewrite (Int.and_commut a c); rewrite (Int.and_commut b c). - rewrite <- Int.and_xor_distrib. apply Int.and_commut. -(* singleoffloat *) - destruct args; simpl in H0; try congruence. - destruct args; simpl in H0; try congruence. - inv H0. destruct (rs#p); simpl; auto. - decEq. rewrite Float.singleoffloat_idem; auto. -(* comparison *) - simpl in H0. destruct (eval_condition c rs##args); try discriminate. - destruct b; inv H0; compute; auto. -Qed. - -Lemma approx_of_chunk_correct: - forall chunk m a v, - Mem.loadv chunk m a = Some v -> - val_match_approx (approx_of_chunk chunk) v. -Proof. - intros. destruct a; simpl in H; try discriminate. - exploit Mem.load_cast; eauto. - destruct chunk; intros; simpl; auto. -Qed. - -End ANALYSIS. - -(** * Correctness of the code transformation *) - -Section PRESERVATION. - -Variable prog: program. -Let tprog := transf_program prog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - -Lemma symbols_preserved: - forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_symbol_transf. -Qed. - -Lemma varinfo_preserved: - forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. -Proof. - intros; unfold ge, tge, tprog, transf_program. - apply Genv.find_var_info_transf. -Qed. - -Lemma functions_translated: - forall (v: val) (f: fundef), - Genv.find_funct ge v = Some f -> - Genv.find_funct tge v = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_transf transf_fundef _ _ H). -Qed. - -Lemma function_ptr_translated: - forall (b: block) (f: fundef), - Genv.find_funct_ptr ge b = Some f -> - Genv.find_funct_ptr tge b = Some (transf_fundef f). -Proof. - intros. - exact (Genv.find_funct_ptr_transf transf_fundef _ _ H). -Qed. - -Lemma sig_function_translated: - forall f, - funsig (transf_fundef f) = funsig f. -Proof. - intros. destruct f; reflexivity. -Qed. - -Lemma find_function_translated: - forall ros rs fd, - find_function ge ros rs = Some fd -> - find_function tge ros rs = Some (transf_fundef fd). -Proof. - intros. destruct ros; simpl in *. - apply functions_translated; auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try congruence. - apply function_ptr_translated; auto. -Qed. - -(** Correctness of [transf_operation]. *) - -Lemma transf_operation_correct: - forall (ge: genv) app rs sp op args m v, - regs_match_approx app rs -> - eval_operation ge sp op rs##args m = Some v -> - eval_operation ge sp (transf_operation op (approx_regs app args)) rs##args m = Some v. -Proof. - intros until v. intro RMA. - assert (A: forall a r, Approx.bge a (approx_reg app r) = true -> val_match_approx a rs#r). - intros. eapply val_match_approx_increasing. apply Approx.bge_correct; eauto. apply RMA. -Opaque Approx.bge. - destruct op; simpl; auto. -(* cast8signed *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Int8s (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -(* cast8unsigned *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Int8u (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -(* cast8signed *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Int16s (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -(* cast8unsigned *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Int16u (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -(* singleoffloat *) - destruct args; simpl; try congruence. destruct args; simpl; try congruence. - intros EQ; inv EQ. - caseEq (Approx.bge Single (approx_reg app p)); intros. - exploit A; eauto. unfold val_match_approx. simpl. congruence. - auto. -Qed. - -(** Matching between states. *) - -Inductive match_stackframes: stackframe -> stackframe -> Prop := - match_stackframe_intro: - forall res sp pc rs f, - (forall v, regs_match_approx (analyze f)!!pc (rs#res <- v)) -> - match_stackframes - (Stackframe res f sp pc rs) - (Stackframe res (transf_function f) sp pc rs). - -Inductive match_states: state -> state -> Prop := - | match_states_intro: - forall s sp pc rs m f s' - (MATCH: regs_match_approx (analyze f)!!pc rs) - (STACKS: list_forall2 match_stackframes s s'), - match_states (State s f sp pc rs m) - (State s' (transf_function f) sp pc rs m) - | match_states_call: - forall s f args m s', - list_forall2 match_stackframes s s' -> - match_states (Callstate s f args m) - (Callstate s' (transf_fundef f) args m) - | match_states_return: - forall s s' v m, - list_forall2 match_stackframes s s' -> - match_states (Returnstate s v m) - (Returnstate s' v m). - -Ltac TransfInstr := - match goal with - | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => - cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr)); - [ simpl transf_instr - | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; - unfold option_map; rewrite H1; reflexivity ] - end. - -(** The proof of semantic preservation follows from the lock-step simulation lemma below. *) - -Lemma transf_step_correct: - forall s1 t s2, - step ge s1 t s2 -> - forall s1' (MS: match_states s1 s1'), - exists s2', step tge s1' t s2' /\ match_states s2 s2'. -Proof. - induction 1; intros; inv MS. - - (* Inop *) - econstructor; split. - TransfInstr; intro. eapply exec_Inop; eauto. - econstructor; eauto. - eapply analyze_correct with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. auto. - - (* Iop *) - exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. - TransfInstr; intro. eapply exec_Iop; eauto. - apply transf_operation_correct; auto. - rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. - econstructor; eauto. - eapply analyze_correct with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. apply regs_match_approx_update; auto. - eapply approx_operation_correct; eauto. - - (* Iload *) - econstructor; split. - TransfInstr; intro. eapply exec_Iload with (a := a). eauto. - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eauto. - econstructor; eauto. - eapply analyze_correct with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. apply regs_match_approx_update; auto. - eapply approx_of_chunk_correct; eauto. - - (* Istore *) - econstructor; split. - TransfInstr; intro. eapply exec_Istore with (a := a). eauto. - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eauto. - econstructor; eauto. - eapply analyze_correct with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. auto. - - (* Icall *) - TransfInstr; intro. - econstructor; split. - eapply exec_Icall. eauto. apply find_function_translated; eauto. - apply sig_function_translated; auto. - constructor; auto. constructor; auto. - econstructor; eauto. - intros. eapply analyze_correct; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. exact I. - - (* Itailcall *) - TransfInstr; intro. - econstructor; split. - eapply exec_Itailcall. eauto. apply find_function_translated; eauto. - apply sig_function_translated; auto. - simpl; eauto. - constructor; auto. - - (* Ibuiltin *) - TransfInstr. intro. - exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split. - eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. - econstructor; eauto. - eapply analyze_correct; eauto. simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. exact I. - - (* Icond, true *) - exists (State s' (transf_function f) sp ifso rs m); split. - TransfInstr. intro. - eapply exec_Icond_true; eauto. - econstructor; eauto. - eapply analyze_correct; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Icond, false *) - exists (State s' (transf_function f) sp ifnot rs m); split. - TransfInstr. intro. - eapply exec_Icond_false; eauto. - econstructor; eauto. - eapply analyze_correct; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Ijumptable *) - exists (State s' (transf_function f) sp pc' rs m); split. - TransfInstr. intro. - eapply exec_Ijumptable; eauto. - constructor; auto. - eapply analyze_correct; eauto. - simpl. eapply list_nth_z_in; eauto. - unfold transfer; rewrite H; auto. - - (* Ireturn *) - exists (Returnstate s' (regmap_optget or Vundef rs) m'); split. - eapply exec_Ireturn; eauto. TransfInstr; auto. - constructor; auto. - - (* internal function *) - simpl. unfold transf_function. - econstructor; split. - eapply exec_function_internal; simpl; eauto. - simpl. econstructor; eauto. - apply analyze_correct_start; auto. - - (* external function *) - simpl. econstructor; split. - eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. - constructor; auto. - - (* return *) - inv H3. inv H1. - econstructor; split. - eapply exec_return; eauto. - econstructor; eauto. -Qed. - -Lemma transf_initial_states: - forall st1, initial_state prog st1 -> - exists st2, initial_state tprog st2 /\ match_states st1 st2. -Proof. - intros. inversion H. - exploit function_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil m0); split. - econstructor; eauto. - apply Genv.init_mem_transf; auto. - replace (prog_main tprog) with (prog_main prog). - rewrite symbols_preserved. eauto. - reflexivity. - rewrite <- H3. apply sig_function_translated. - constructor. constructor. -Qed. - -Lemma transf_final_states: - forall st1 st2 r, - match_states st1 st2 -> final_state st1 r -> final_state st2 r. -Proof. - intros. inv H0. inv H. inv H4. constructor. -Qed. - -(** The preservation of the observable behavior of the program then - follows. *) - -Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (RTL.semantics tprog). -Proof. - eapply forward_simulation_step. - eexact symbols_preserved. - eexact transf_initial_states. - eexact transf_final_states. - exact transf_step_correct. -Qed. - -End PRESERVATION. - - |