diff options
Diffstat (limited to 'backend/CastOptimproof.v')
| -rw-r--r-- | backend/CastOptimproof.v | 577 |
1 files changed, 577 insertions, 0 deletions
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v new file mode 100644 index 0000000..60b10c2 --- /dev/null +++ b/backend/CastOptimproof.v @@ -0,0 +1,577 @@ +(* *********************************************************************) +(* *) +(* 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.gmap. 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 v, + regs_match_approx app rs -> + eval_operation ge sp op rs##args = 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; 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 v, + regs_match_approx app rs -> + eval_operation ge sp op rs##args = Some v -> + eval_operation ge sp (transf_operation op (approx_regs app args)) rs##args = 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; eauto. + rewrite <- H0. apply eval_addressing_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_of_chunk_correct; eauto. + + (* Istore *) + econstructor; split. + TransfInstr; intro. eapply exec_Istore; eauto. + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + 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, using the generic preservation theorem + [Smallstep.simulation_step_preservation]. *) + +Theorem transf_program_correct: + forall (beh: program_behavior), not_wrong beh -> + exec_program prog beh -> exec_program tprog beh. +Proof. + unfold exec_program; intros. + eapply simulation_step_preservation; eauto. + eexact transf_initial_states. + eexact transf_final_states. + exact transf_step_correct. +Qed. + +End PRESERVATION. + + |