From a82c9c0e4a0b8e37c9c3ea5ae99714982563606f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Jan 2012 14:23:26 +0000 Subject: Merge of the nonstrict-ops branch: - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constpropproof.v | 314 +++++++++++++++++++++++++++-------------------- 1 file changed, 183 insertions(+), 131 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 058d68ef..7ac43391 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -36,9 +36,10 @@ Require Import ConstpropOpproof. Section ANALYSIS. Variable ge: genv. +Variable sp: val. Definition regs_match_approx (a: D.t) (rs: regset) : Prop := - forall r, val_match_approx ge (D.get r a) rs#r. + forall r, val_match_approx ge sp (D.get r a) rs#r. Lemma regs_match_approx_top: forall rs, regs_match_approx D.top rs. @@ -49,7 +50,7 @@ Qed. Lemma val_match_approx_increasing: forall a1 a2 v, - Approx.ge a1 a2 -> val_match_approx ge a2 v -> val_match_approx ge a1 v. + Approx.ge a1 a2 -> val_match_approx ge sp a2 v -> val_match_approx ge sp a1 v. Proof. intros until v. intros [A|[B|C]]. @@ -68,7 +69,7 @@ Qed. Lemma regs_match_approx_update: forall ra rs a v r, - val_match_approx ge a v -> + val_match_approx ge sp a v -> regs_match_approx ra rs -> regs_match_approx (D.set r a ra) (rs#r <- v). Proof. @@ -81,14 +82,13 @@ Qed. Lemma approx_regs_val_list: forall ra rs rl, regs_match_approx ra rs -> - val_list_match_approx ge (approx_regs ra rl) rs##rl. + val_list_match_approx ge sp (approx_regs ra rl) rs##rl. Proof. induction rl; simpl; intros. constructor. constructor. apply H. auto. Qed. - (** The correctness of the static analysis follows from the results of module [ConstpropOpproof] and the fact that the result of the static analysis is a solution of the forward dataflow inequations. *) @@ -178,26 +178,56 @@ Proof. intros. destruct f; reflexivity. Qed. +Definition regs_lessdef (rs1 rs2: regset) : Prop := + forall r, Val.lessdef (rs1#r) (rs2#r). + +Lemma regs_lessdef_regs: + forall rs1 rs2, regs_lessdef rs1 rs2 -> + forall rl, Val.lessdef_list rs1##rl rs2##rl. +Proof. + induction rl; constructor; auto. +Qed. + +Lemma set_reg_lessdef: + forall r v1 v2 rs1 rs2, + Val.lessdef v1 v2 -> regs_lessdef rs1 rs2 -> regs_lessdef (rs1#r <- v1) (rs2#r <- v2). +Proof. + intros; red; intros. repeat rewrite Regmap.gsspec. + destruct (peq r0 r); auto. +Qed. + +Lemma init_regs_lessdef: + forall rl vl1 vl2, + Val.lessdef_list vl1 vl2 -> + regs_lessdef (init_regs vl1 rl) (init_regs vl2 rl). +Proof. + induction rl; simpl; intros. + red; intros. rewrite Regmap.gi. auto. + inv H. red; intros. rewrite Regmap.gi. auto. + apply set_reg_lessdef; auto. +Qed. + Lemma transf_ros_correct: - forall ros rs f approx, - regs_match_approx ge approx rs -> + forall sp ros rs rs' f approx, + regs_match_approx ge sp approx rs -> find_function ge ros rs = Some f -> - find_function tge (transf_ros approx ros) rs = Some (transf_fundef f). + regs_lessdef rs rs' -> + find_function tge (transf_ros approx ros) rs' = Some (transf_fundef f). Proof. - intros until approx; intro MATCH. - destruct ros; simpl. - intro. - exploit functions_translated; eauto. intro FIND. - caseEq (D.get r approx); intros; auto. - generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto. - generalize (MATCH r). rewrite H0. intros [b [A B]]. - rewrite <- symbols_preserved in A. - rewrite B in FIND. rewrite H1 in FIND. - rewrite Genv.find_funct_find_funct_ptr in FIND. - simpl. rewrite A. auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i). - intro. apply function_ptr_translated. auto. - congruence. + intros. destruct ros; simpl in *. + generalize (H r); intro MATCH. generalize (H1 r); intro LD. + destruct (rs#r); simpl in H0; try discriminate. + destruct (Int.eq_dec i Int.zero); try discriminate. + inv LD. + assert (find_function tge (inl _ r) rs' = Some (transf_fundef f)). + simpl. rewrite <- H4. simpl. rewrite dec_eq_true. apply function_ptr_translated. auto. + destruct (D.get r approx); auto. + predSpec Int.eq Int.eq_spec i0 Int.zero; intros; auto. + simpl in *. unfold symbol_address in MATCH. rewrite symbols_preserved. + destruct (Genv.find_symbol ge i); try discriminate. + inv MATCH. apply function_ptr_translated; auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i); try discriminate. + apply function_ptr_translated; auto. Qed. (** The proof of semantic preservation is a simulation argument @@ -227,29 +257,37 @@ Qed. Inductive match_stackframes: stackframe -> stackframe -> Prop := match_stackframe_intro: - forall res sp pc rs f, - (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) -> + forall res sp pc rs f rs', + regs_lessdef rs rs' -> + (forall v, regs_match_approx ge sp (analyze f)!!pc (rs#res <- v)) -> match_stackframes (Stackframe res f sp pc rs) - (Stackframe res (transf_function 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 ge (analyze f)!!pc rs) - (STACKS: list_forall2 match_stackframes s s'), + forall s sp pc rs m f s' rs' m' + (MATCH: regs_match_approx ge sp (analyze f)!!pc rs) + (STACKS: list_forall2 match_stackframes s s') + (REGS: regs_lessdef rs rs') + (MEM: Mem.extends m m'), match_states (State s f sp pc rs m) - (State s' (transf_function 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' -> + forall s f args m s' args' m' + (STACKS: list_forall2 match_stackframes s s') + (ARGS: Val.lessdef_list args args') + (MEM: Mem.extends m m'), match_states (Callstate s f args m) - (Callstate s' (transf_fundef f) args m) + (Callstate s' (transf_fundef f) args' m') | match_states_return: - forall s s' v m, + forall s v m s' v' m' + (STACKS: list_forall2 match_stackframes s s') + (RES: Val.lessdef v v') + (MEM: Mem.extends m m'), list_forall2 match_stackframes s s' -> match_states (Returnstate s v m) - (Returnstate s' v m). + (Returnstate s' v' m'). Ltac TransfInstr := match goal with @@ -272,7 +310,7 @@ Proof. induction 1; intros; inv MS. (* Inop *) - exists (State s' (transf_function f) sp pc' rs m); split. + exists (State s' (transf_function f) sp pc' rs' m'); split. TransfInstr; intro. eapply exec_Inop; eauto. econstructor; eauto. eapply analyze_correct_1 with (pc := pc); eauto. @@ -280,58 +318,78 @@ Proof. unfold transfer; rewrite H. auto. (* Iop *) - exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. - TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args); - intros op' args' OSR. - assert (eval_operation tge sp op' rs##args' m = Some v). - rewrite (eval_operation_preserved _ _ symbols_preserved). - generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs m - MATCH op args v). - rewrite OSR; simpl. auto. - generalize (eval_static_operation_correct ge op sp - (approx_regs (analyze f)!!pc args) rs##args m v - (approx_regs_val_list _ _ _ args MATCH) H0). - case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros; - simpl in H2; - eapply exec_Iop; eauto; simpl. - congruence. - congruence. - elim H2; intros b [A B]. rewrite symbols_preserved. - rewrite A; rewrite B; auto. - econstructor; eauto. - eapply analyze_correct_1 with (pc := pc); eauto. - simpl; auto. - unfold transfer; rewrite H. - apply regs_match_approx_update; auto. - eapply eval_static_operation_correct; eauto. - apply approx_regs_val_list; auto. + assert (MATCH': regs_match_approx ge sp (analyze f) # pc' rs # res <- v). + eapply analyze_correct_1 with (pc := pc); eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. + eapply eval_static_operation_correct; eauto. + apply approx_regs_val_list; auto. + TransfInstr. + exploit eval_static_operation_correct; eauto. eapply approx_regs_val_list; eauto. intros VM. + destruct (eval_static_operation op (approx_regs (analyze f) # pc args)); intros; simpl in VM. + (* Novalue *) + contradiction. + (* Unknown *) + exploit op_strength_reduction_correct. eexact MATCH. reflexivity. eauto. + destruct (op_strength_reduction op args (approx_regs (analyze f) # pc args)) as [op' args']. + intros [v' [EV' LD']]. + assert (EV'': exists v'', eval_operation ge sp op' rs'##args' m' = Some v'' /\ Val.lessdef v' v''). + eapply eval_operation_lessdef; eauto. eapply regs_lessdef_regs; eauto. + destruct EV'' as [v'' [EV'' LD'']]. + exists (State s' (transf_function f) sp pc' (rs'#res <- v'') m'); split. + econstructor. eauto. rewrite <- EV''. apply eval_operation_preserved. exact symbols_preserved. + econstructor; eauto. apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. + (* I i *) + subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vint i)) m'); split. + econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + (* F *) + subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Vfloat f0)) m'); split. + econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + (* G *) + subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (symbol_address tge i i0)) m'); split. + econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + unfold symbol_address. rewrite symbols_preserved; auto. + (* S *) + subst v. exists (State s' (transf_function f) sp pc' (rs'#res <- (Val.add sp (Vint i))) m'); split. + econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. (* Iload *) - caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); - intros addr' args' ASR. - assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved _ _ symbols_preserved). - generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs - MATCH addr args). - rewrite ASR; simpl. congruence. - TransfInstr. rewrite ASR. intro. - exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split. + TransfInstr. + generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs + MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)). + destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args']. + intros P Q. rewrite H0 in P. + assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a'). + eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto. + destruct ADDR' as [a' [A B]]. + assert (C: eval_addressing tge sp addr' rs'##args' = Some a'). + rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. + exploit Mem.loadv_extends; eauto. intros [v' [D E]]. + exists (State s' (transf_function f) sp pc' (rs'#dst <- v') m'); split. eapply exec_Iload; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. apply regs_match_approx_update; auto. simpl; auto. + apply set_reg_lessdef; auto. (* Istore *) - caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); - intros addr' args' ASR. - assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved _ _ symbols_preserved). - generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs - MATCH addr args). - rewrite ASR; simpl. congruence. - TransfInstr. rewrite ASR. intro. - exists (State s' (transf_function f) sp pc' rs m'); split. + TransfInstr. + generalize (addr_strength_reduction_correct ge sp (analyze f)!!pc rs + MATCH addr args (approx_regs (analyze f) # pc args) (refl_equal _)). + destruct (addr_strength_reduction addr args (approx_regs (analyze f) # pc args)) as [addr' args']. + intros P Q. rewrite H0 in P. + assert (ADDR': exists a', eval_addressing ge sp addr' rs'##args' = Some a' /\ Val.lessdef a a'). + eapply eval_addressing_lessdef; eauto. eapply regs_lessdef_regs; eauto. + destruct ADDR' as [a' [A B]]. + assert (C: eval_addressing tge sp addr' rs'##args' = Some a'). + rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. + exploit Mem.storev_extends; eauto. intros [m2' [D E]]. + exists (State s' (transf_function f) sp pc' rs' m2'); split. eapply exec_Istore; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. @@ -347,17 +405,22 @@ Proof. intros. eapply analyze_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. apply regs_match_approx_update; auto. simpl. auto. + apply regs_lessdef_regs; auto. (* Itailcall *) + exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. exploit transf_ros_correct; eauto. intros FIND'. TransfInstr; intro. econstructor; split. eapply exec_Itailcall; eauto. apply sig_function_translated; auto. - constructor; auto. + constructor; auto. apply regs_lessdef_regs; auto. (* Ibuiltin *) + exploit external_call_mem_extends; eauto. + instantiate (1 := rs'##args). apply regs_lessdef_regs; auto. + intros [v' [m2' [A [B [C D]]]]]. TransfInstr. intro. - exists (State s' (transf_function f) sp pc' (rs#res <- v) m'); split. + exists (State s' (transf_function f) sp pc' (rs'#res <- v') m2'); split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. @@ -365,72 +428,61 @@ Proof. eapply analyze_correct_1; eauto. simpl; auto. unfold transfer; rewrite H. apply regs_match_approx_update; auto. simpl; auto. - - (* Icond, true *) - exists (State s' (transf_function f) sp ifso rs m); split. - caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); - intros cond' args' CSR. - assert (eval_condition cond' rs##args' m = Some true). - generalize (cond_strength_reduction_correct - ge (approx_reg (analyze f)!!pc) rs m MATCH cond args). - rewrite CSR. intro. congruence. - TransfInstr. rewrite CSR. - caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). - intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ m _ - (approx_regs_val_list _ _ _ args MATCH) ESC); intro. - replace b with true. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_true; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. - - (* Icond, false *) - exists (State s' (transf_function f) sp ifnot rs m); split. - caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); - intros cond' args' CSR. - assert (eval_condition cond' rs##args' m = Some false). - generalize (cond_strength_reduction_correct - ge (approx_reg (analyze f)!!pc) rs m MATCH cond args). - rewrite CSR. intro. congruence. - TransfInstr. rewrite CSR. - caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). - intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ m _ - (approx_regs_val_list _ _ _ args MATCH) ESC); intro. - replace b with false. intro; eapply exec_Inop; eauto. congruence. - intros. eapply exec_Icond_false; eauto. - econstructor; eauto. - eapply analyze_correct_1; eauto. - simpl; auto. - unfold transfer; rewrite H; auto. + apply set_reg_lessdef; auto. + + (* Icond *) + TransfInstr. + generalize (cond_strength_reduction_correct ge sp (analyze f)#pc rs m + MATCH cond args (approx_regs (analyze f) # pc args) (refl_equal _)). + destruct (cond_strength_reduction cond args (approx_regs (analyze f) # pc args)) as [cond' args']. + intros EV1. + exists (State s' (transf_function f) sp (if b then ifso else ifnot) rs' m'); split. + destruct (eval_static_condition cond (approx_regs (analyze f) # pc args)) as []_eqn. + assert (eval_condition cond rs ## args m = Some b0). + eapply eval_static_condition_correct; eauto. eapply approx_regs_val_list; eauto. + assert (b = b0) by congruence. subst b0. + destruct b; eapply exec_Inop; eauto. + eapply exec_Icond; eauto. + eapply eval_condition_lessdef with (vl1 := rs##args'); eauto. eapply regs_lessdef_regs; eauto. congruence. + econstructor; eauto. + eapply analyze_correct_1; eauto. destruct b; simpl; auto. + unfold transfer; rewrite H. auto. (* Ijumptable *) - exists (State s' (transf_function f) sp pc' rs m); split. - caseEq (intval (approx_reg (analyze f)!!pc) arg); intros. - exploit intval_correct; eauto. eexact MATCH. intro VRS. - eapply exec_Inop; eauto. TransfInstr. rewrite H2. - replace i with n by congruence. rewrite H1. auto. - eapply exec_Ijumptable; eauto. TransfInstr. rewrite H2. auto. - constructor; auto. + assert (A: (fn_code (transf_function f))!pc = Some(Ijumptable arg tbl) + \/ (fn_code (transf_function f))!pc = Some(Inop pc')). + TransfInstr. destruct (approx_reg (analyze f) # pc arg) as []_eqn; auto. + generalize (MATCH arg). unfold approx_reg in Heqt. rewrite Heqt. rewrite H0. + simpl. intro EQ; inv EQ. rewrite H1. auto. + assert (B: rs'#arg = Vint n). + generalize (REGS arg); intro LD; inv LD; congruence. + exists (State s' (transf_function f) sp pc' rs' m'); split. + destruct A. eapply exec_Ijumptable; eauto. eapply exec_Inop; eauto. + econstructor; eauto. eapply analyze_correct_1; eauto. simpl. eapply list_nth_z_in; eauto. unfold transfer; rewrite H; auto. (* Ireturn *) - exists (Returnstate s' (regmap_optget or Vundef rs) m'); split. + exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. + exists (Returnstate s' (regmap_optget or Vundef rs') m2'); split. eapply exec_Ireturn; eauto. TransfInstr; auto. constructor; auto. + destruct or; simpl; auto. (* internal function *) + exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + intros [m2' [A B]]. simpl. unfold transf_function. econstructor; split. eapply exec_function_internal; simpl; eauto. simpl. econstructor; eauto. apply analyze_correct_3; auto. + apply init_regs_lessdef; auto. (* external function *) + exploit external_call_mem_extends; eauto. + intros [v' [m2' [A [B [C D]]]]]. simpl. econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. @@ -441,7 +493,7 @@ Proof. inv H3. inv H1. econstructor; split. eapply exec_return; eauto. - econstructor; eauto. + econstructor; eauto. apply set_reg_lessdef; auto. Qed. Lemma transf_initial_states: @@ -457,14 +509,14 @@ Proof. rewrite symbols_preserved. eauto. reflexivity. rewrite <- H3. apply sig_function_translated. - constructor. constructor. + constructor. constructor. constructor. apply Mem.extends_refl. 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. + intros. inv H0. inv H. inv STACKS. inv RES. constructor. Qed. (** The preservation of the observable behavior of the program then -- cgit