diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-21 11:16:42 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-21 11:16:42 +0100 |
commit | b873e06abcee1c7f6a51aaabb973b550a52a5b61 (patch) | |
tree | 70ccd9c7cbba08e20b782217b1a2268b1afce3e9 /backend/Stackingproof.v | |
parent | 65db9a4a02c30d8dd5ca89b6fe3e4524cd4c29a5 (diff) | |
parent | eb7bd26e2b9eeed21d204bad26fa56c8a7937ffb (diff) | |
download | compcert-kvx-b873e06abcee1c7f6a51aaabb973b550a52a5b61.tar.gz compcert-kvx-b873e06abcee1c7f6a51aaabb973b550a52a5b61.zip |
Merge tag 'v3.4' into mppa_k1c
Conflicts:
.gitignore
Diffstat (limited to 'backend/Stackingproof.v')
-rw-r--r-- | backend/Stackingproof.v | 92 |
1 files changed, 32 insertions, 60 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 6d46d04d..c9b07427 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -294,12 +294,13 @@ Qed. Lemma contains_locations_exten: forall ls ls' j sp pos bound sl, - (forall ofs ty, ls' (S sl ofs ty) = ls (S sl ofs ty)) -> + (forall ofs ty, Val.lessdef (ls' (S sl ofs ty)) (ls (S sl ofs ty))) -> massert_imp (contains_locations j sp pos bound sl ls) (contains_locations j sp pos bound sl ls'). Proof. intros; split; simpl; intros; auto. - intuition auto. rewrite H. eauto. + intuition auto. exploit H5; eauto. intros (v & A & B). exists v; split; auto. + specialize (H ofs ty). inv H. congruence. auto. Qed. Lemma contains_locations_incr: @@ -481,7 +482,8 @@ Qed. Lemma frame_contents_exten: forall ls ls0 ls' ls0' j sp parent retaddr P m, - (forall sl ofs ty, ls' (S sl ofs ty) = ls (S sl ofs ty)) -> + (forall ofs ty, Val.lessdef (ls' (S Local ofs ty)) (ls (S Local ofs ty))) -> + (forall ofs ty, Val.lessdef (ls' (S Outgoing ofs ty)) (ls (S Outgoing ofs ty))) -> (forall r, In r b.(used_callee_save) -> ls0' (R r) = ls0 (R r)) -> m |= frame_contents j sp ls ls0 parent retaddr ** P -> m |= frame_contents j sp ls' ls0' parent retaddr ** P. @@ -573,16 +575,6 @@ Record agree_locs (ls ls0: locset) : Prop := ls (S Incoming ofs ty) = ls0 (S Outgoing ofs ty) }. -(** Auxiliary predicate used at call points *) - -Definition agree_callee_save (ls ls0: locset) : Prop := - forall l, - match l with - | R r => is_callee_save r = true - | S _ _ _ => True - end -> - ls l = ls0 l. - (** ** Properties of [agree_regs]. *) (** Values of registers *) @@ -666,6 +658,16 @@ Proof. apply agree_regs_set_reg; auto. Qed. +Lemma agree_regs_undef_caller_save_regs: + forall j ls rs, + agree_regs j ls rs -> + agree_regs j (LTL.undef_caller_save_regs ls) (Mach.undef_caller_save_regs rs). +Proof. + intros; red; intros. + unfold LTL.undef_caller_save_regs, Mach.undef_caller_save_regs. + destruct (is_callee_save r); auto. +Qed. + (** Preservation under assignment of stack slot *) Lemma agree_regs_set_slot: @@ -800,41 +802,7 @@ Lemma agree_locs_return: Proof. intros. red in H0. inv H; constructor; auto; intros. - rewrite H0; auto. unfold mreg_within_bounds in H. tauto. -- rewrite H0; auto. -Qed. - -(** Preservation at tailcalls (when [ls0] is changed but not [ls]). *) - -Lemma agree_locs_tailcall: - forall ls ls0 ls0', - agree_locs ls ls0 -> - agree_callee_save ls0 ls0' -> - agree_locs ls ls0'. -Proof. - intros. red in H0. inv H; constructor; auto; intros. -- rewrite <- H0; auto. unfold mreg_within_bounds in H. tauto. -- rewrite <- H0; auto. -Qed. - -(** ** Properties of [agree_callee_save]. *) - -Lemma agree_callee_save_return_regs: - forall ls1 ls2, - agree_callee_save (return_regs ls1 ls2) ls1. -Proof. - intros; red; intros. - unfold return_regs. destruct l; auto. rewrite H; auto. -Qed. - -Lemma agree_callee_save_set_result: - forall sg v ls1 ls2, - agree_callee_save ls1 ls2 -> - agree_callee_save (Locmap.setpair (loc_result sg) v ls1) ls2. -Proof. - intros; red; intros. rewrite Locmap.gpo. apply H; auto. - assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). - { intros. destruct l; auto. simpl; congruence. } - generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto. +- rewrite <- agree_incoming0 by auto. apply H0. congruence. Qed. (** ** Properties of destroyed registers. *) @@ -1071,6 +1039,7 @@ Lemma function_prologue_correct: forall j ls ls0 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k P, agree_regs j ls rs -> agree_callee_save ls ls0 -> + agree_outgoing_arguments (Linear.fn_sig f) ls ls0 -> (forall r, Val.has_type (ls (R r)) (mreg_type r)) -> ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) -> rs1 = undef_regs destroyed_at_function_entry rs -> @@ -1090,7 +1059,7 @@ Lemma function_prologue_correct: /\ j' sp = Some(sp', fe.(fe_stack_data)) /\ inject_incr j j'. Proof. - intros until P; intros AGREGS AGCS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP. + intros until P; intros AGREGS AGCS AGARGS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP. rewrite unfold_transf_function. unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs. (* Stack layout info *) @@ -1174,7 +1143,7 @@ Local Opaque b fe. split. rewrite LS1. apply agree_locs_undef_locs; [|reflexivity]. constructor; intros. unfold call_regs. apply AGCS. unfold mreg_within_bounds in H; tauto. - unfold call_regs. apply AGCS. auto. + unfold call_regs. apply AGARGS. apply incoming_slot_in_parameters; auto. split. exact SEPFINAL. split. exact SAME. exact INCR. Qed. @@ -1325,7 +1294,7 @@ Proof. apply CS; auto. rewrite NCS by auto. apply AGR. split. red; unfold return_regs; intros. - destruct l; auto. rewrite H; auto. + destruct l. rewrite H; auto. destruct sl; auto; contradiction. assumption. Qed. @@ -1619,6 +1588,7 @@ Variable ls: locset. Variable rs: regset. Hypothesis AGR: agree_regs j ls rs. Hypothesis AGCS: agree_callee_save ls (parent_locset cs). +Hypothesis AGARGS: agree_outgoing_arguments sg ls (parent_locset cs). Variable m': mem. Hypothesis SEP: m' |= stack_contents j cs cs'. @@ -1641,7 +1611,7 @@ Proof. assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto. exploit frame_get_outgoing; eauto. intros (v & A & B). exists v; split. - constructor. exact A. red in AGCS. rewrite AGCS; auto. + constructor. exact A. rewrite AGARGS by auto. exact B. Qed. Lemma transl_external_argument_2: @@ -1816,7 +1786,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := (TRANSL: transf_fundef f = OK tf) (FIND: Genv.find_funct_ptr tge fb = Some tf) (AGREGS: agree_regs j ls rs) - (AGLOCS: agree_callee_save ls (parent_locset cs)) (SEP: m' |= stack_contents j cs cs' ** minjection j m ** globalenv_inject ge j), @@ -1826,7 +1795,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := forall cs ls m cs' rs m' j sg (STACKS: match_stacks j cs cs' sg) (AGREGS: agree_regs j ls rs) - (AGLOCS: agree_callee_save ls (parent_locset cs)) (SEP: m' |= stack_contents j cs cs' ** minjection j m ** globalenv_inject ge j), @@ -1989,9 +1957,8 @@ Proof. econstructor; eauto with coqlib. apply Val.Vptr_has_type. intros; red. - apply Z.le_trans with (size_arguments (Linear.funsig f')); auto. + apply Z.le_trans with (size_arguments (Linear.funsig f')); auto. apply loc_arguments_bounded; auto. - simpl; red; auto. simpl. rewrite sep_assoc. exact SEP. - (* Ltailcall *) @@ -2091,6 +2058,7 @@ Proof. destruct (transf_function f) as [tfn|] eqn:TRANSL; simpl; try congruence. intros EQ; inversion EQ; clear EQ; subst tf. rewrite sep_comm, sep_assoc in SEP. + exploit wt_callstate_agree; eauto. intros [AGCS AGARGS]. exploit function_prologue_correct; eauto. red; intros; eapply wt_callstate_wt_regs; eauto. eapply match_stacks_type_sp; eauto. @@ -2109,6 +2077,7 @@ Proof. - (* external function *) simpl in TRANSL. inversion TRANSL; subst tf. + exploit wt_callstate_agree; eauto. intros [AGCS AGARGS]. exploit transl_external_arguments; eauto. apply sep_proj1 in SEP; eauto. intros [vl [ARGS VINJ]]. rewrite sep_comm, sep_assoc in SEP. exploit external_call_parallel_rule; eauto. @@ -2118,18 +2087,22 @@ Proof. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_states_return with (j := j'). eapply match_stacks_change_meminj; eauto. - apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto. - apply agree_callee_save_set_result; auto. + apply agree_regs_set_pair. apply agree_regs_undef_caller_save_regs. + apply agree_regs_inject_incr with j; auto. + auto. apply stack_contents_change_meminj with j; auto. rewrite sep_comm, sep_assoc; auto. - (* return *) - inv STACKS. simpl in AGLOCS. simpl in SEP. rewrite sep_assoc in SEP. + inv STACKS. exploit wt_returnstate_agree; eauto. intros [AGCS OUTU]. + simpl in AGCS. simpl in SEP. rewrite sep_assoc in SEP. econstructor; split. apply plus_one. apply exec_return. econstructor; eauto. apply agree_locs_return with rs0; auto. apply frame_contents_exten with rs0 (parent_locset s); auto. + intros; apply Val.lessdef_same; apply AGCS; red; congruence. + intros; rewrite (OUTU ty ofs); auto. Qed. Lemma transf_initial_states: @@ -2147,7 +2120,6 @@ Proof. eapply match_states_call with (j := j); eauto. constructor. red; intros. rewrite H3, loc_arguments_main in H. contradiction. red; simpl; auto. - red; simpl; auto. simpl. rewrite sep_pure. split; auto. split;[|split]. eapply Genv.initmem_inject; eauto. simpl. exists (Mem.nextblock m0); split. apply Ple_refl. |