diff options
| -rw-r--r-- | arm/Asm.v | 11 | ||||
| -rw-r--r-- | arm/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | backend/Allocproof.v | 3 | ||||
| -rw-r--r-- | backend/Asmgenproof0.v | 17 | ||||
| -rw-r--r-- | backend/LTL.v | 13 | ||||
| -rw-r--r-- | backend/Linear.v | 2 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 11 | ||||
| -rw-r--r-- | backend/Mach.v | 5 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 26 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 10 | ||||
| -rw-r--r-- | powerpc/Asm.v | 11 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | riscV/Asm.v | 11 | ||||
| -rw-r--r-- | riscV/Asmgenproof.v | 4 | ||||
| -rw-r--r-- | x86/Asm.v | 11 | ||||
| -rw-r--r-- | x86/Asmgenproof.v | 4 |
16 files changed, 127 insertions, 20 deletions
@@ -852,6 +852,15 @@ Definition preg_of (r: mreg) : preg := | F12 => FR12 | F13 => FR13 | F14 => FR14 | F15 => FR15 end. +(** Undefine all registers except SP and callee-save registers *) + +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => + if preg_eq r SP + || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) + then rs r + else Vundef. + (** Extract the values of the arguments of an external call. We exploit the calling conventions from module [Conventions], except that we use ARM registers instead of locations. *) @@ -911,7 +920,7 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> extcall_arguments rs m (ef_sig ef) args -> - rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs IR14) -> + rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs rs))#PC <- (rs IR14) -> step (State rs m) t (State rs' m'). End RELSEM. diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index abec6815..2c001f45 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -926,8 +926,8 @@ Opaque loadind. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - apply agree_set_other; auto with asmgen. - eapply agree_set_pair; eauto. + unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. + apply agree_undef_caller_save_regs; auto. - (* return *) inv STACKS. simpl in *. diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 585fb0da..068e0de0 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2476,7 +2476,8 @@ Proof. rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. rewrite val_longofwords_eq_1 by auto. auto. red; intros. rewrite (AG l H0). - symmetry; apply Locmap.gpo. + rewrite Locmap.gpo. + unfold undef_caller_save_regs. destruct l; auto. simpl in H0; rewrite H0; auto. assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). { intros. destruct l; simpl in *. congruence. auto. } generalize (loc_result_caller_save (ef_sig ef)). destruct (loc_result (ef_sig ef)); simpl; intuition auto. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index f6f03868..70c4323c 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -316,6 +316,23 @@ Proof. intros. rewrite Pregmap.gso; auto. Qed. +Lemma agree_undef_caller_save_regs: + forall ms sp rs, + agree ms sp rs -> + agree (Mach.undef_caller_save_regs ms) sp (Asm.undef_caller_save_regs rs). +Proof. + intros. destruct H. unfold Mach.undef_caller_save_regs, Asm.undef_caller_save_regs; split. +- unfold proj_sumbool; rewrite dec_eq_true. auto. +- auto. +- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). + destruct (in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. ++ apply list_in_map_inv in i. destruct i as (mr & A & B). + assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. + apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. ++ destruct (is_callee_save r) eqn:CS; auto. + elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. +Qed. + Lemma agree_change_sp: forall ms sp rs sp', agree ms sp rs -> sp' <> Vundef -> diff --git a/backend/LTL.v b/backend/LTL.v index 8567a891..6dd1abd6 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -106,6 +106,17 @@ Definition return_regs (caller callee: locset) : locset := | S sl ofs ty => caller (S sl ofs ty) end. +(** [undef_caller_save_regs ls] models the effect of calling + an external function: caller-save registers can change unpredictably, + hence we set them to [Vundef]. *) + +Definition undef_caller_save_regs (ls: locset) : locset := + fun (l: loc) => + match l with + | R r => if is_callee_save r then ls (R r) else Vundef + | S sl ofs ty => ls (S sl ofs ty) + end. + (** LTL execution states. *) Inductive stackframe : Type := @@ -259,7 +270,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s ef t args res rs m rs' m', args = map (fun p => Locmap.getpair p rs) (loc_arguments (ef_sig ef)) -> external_call ef ge args m t res m' -> - rs' = Locmap.setpair (loc_result (ef_sig ef)) res rs -> + rs' = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) -> step (Callstate s (External ef) rs m) t (Returnstate s rs' m') | exec_return: forall f sp rs1 bb s rs m, diff --git a/backend/Linear.v b/backend/Linear.v index 55f92d16..447c6ba6 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -239,7 +239,7 @@ Inductive step: state -> trace -> state -> Prop := forall s ef args res rs1 rs2 m t m', args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) -> external_call ef ge args m t res m' -> - rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1 -> + rs2 = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs1) -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m') | exec_return: diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 30cc0d91..fd252dc6 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -149,6 +149,14 @@ Proof. unfold return_regs. destruct l; auto. destruct (is_callee_save r); auto. Qed. +Lemma wt_undef_caller_save_regs: + forall ls, wt_locset ls -> wt_locset (undef_caller_save_regs ls). +Proof. + intros; red; intros. unfold undef_caller_save_regs. + destruct l; auto. + destruct (is_callee_save r); auto; simpl; auto. +Qed. + Lemma wt_init: wt_locset (Locmap.init Vundef). Proof. @@ -339,8 +347,9 @@ Local Opaque mreg_type. econstructor. eauto. eauto. eauto. apply wt_undef_regs. apply wt_call_regs. auto. - (* external function *) - econstructor. auto. apply wt_setpair; auto. + econstructor. auto. apply wt_setpair. eapply external_call_well_typed; eauto. + apply wt_undef_caller_save_regs; auto. - (* return *) inv WTSTK. econstructor; eauto. Qed. diff --git a/backend/Mach.v b/backend/Mach.v index 839a25bd..9fdee9eb 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -156,6 +156,9 @@ Proof. unfold Regmap.set. destruct (RegEq.eq r a); auto. Qed. +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => if is_callee_save r then rs r else Vundef. + Definition set_pair (p: rpair mreg) (v: val) (rs: regset) : regset := match p with | One r => rs#r <- v @@ -407,7 +410,7 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge fb = Some (External ef) -> extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> external_call ef ge args m t res m' -> - rs' = set_pair (loc_result (ef_sig ef)) res rs -> + rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) -> step (Callstate s fb rs m) t (Returnstate s rs' m') | exec_return: diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index f7570f57..5dbc4532 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -666,6 +666,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: @@ -826,6 +836,16 @@ Proof. unfold return_regs. destruct l; auto. rewrite H; auto. Qed. +Lemma agree_callee_save_undef_caller_save_regs: + forall ls1 ls2, + agree_callee_save ls1 ls2 -> + agree_callee_save (LTL.undef_caller_save_regs ls1) ls2. +Proof. + intros; red; intros. unfold LTL.undef_caller_save_regs. + destruct l; auto. + rewrite H0; auto. +Qed. + Lemma agree_callee_save_set_result: forall sg v ls1 ls2, agree_callee_save ls1 ls2 -> @@ -2113,8 +2133,10 @@ 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 agree_callee_save_set_result. apply agree_callee_save_undef_caller_save_regs. auto. apply stack_contents_change_meminj with j; auto. rewrite sep_comm, sep_assoc; auto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index c6644ceb..fd97ce33 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -334,6 +334,14 @@ Proof. induction res; intros; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef. Qed. +Lemma locmap_undef_caller_save_regs_lessdef: + forall ls1 ls2, + locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_caller_save_regs ls1) (undef_caller_save_regs ls2). +Proof. + intros; red; intros. unfold undef_caller_save_regs. + destruct l; auto. destruct (Conventions1.is_callee_save r); auto. +Qed. + Lemma find_function_translated: forall ros ls tls fd, locmap_lessdef ls tls -> @@ -516,7 +524,7 @@ Proof. left; simpl; econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. - simpl. econstructor; eauto using locmap_setpair_lessdef. + simpl. econstructor; eauto using locmap_setpair_lessdef, locmap_undef_caller_save_regs_lessdef. - (* return *) inv STK. inv H1. left; econstructor; split. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index ff580f01..aa15547b 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -1130,6 +1130,15 @@ Definition preg_of (r: mreg) : preg := | F28 => FPR28 | F29 => FPR29 | F30 => FPR30 | F31 => FPR31 end. +(** Undefine all registers except SP and callee-save registers *) + +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => + if preg_eq r SP + || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) + then rs r + else Vundef. + (** Extract the values of the arguments of an external call. We exploit the calling conventions from module [Conventions], except that we use PPC registers instead of locations. *) @@ -1189,7 +1198,7 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> extcall_arguments rs m (ef_sig ef) args -> - rs' = (set_pair (loc_external_result (ef_sig ef)) res rs) #PC <- (rs RA) -> + rs' = (set_pair (loc_external_result (ef_sig ef)) res (undef_caller_save_regs rs)) #PC <- (rs RA) -> step (State rs m) t (State rs' m'). End RELSEM. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 9f258e3d..8ad28aea 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -918,8 +918,8 @@ Local Transparent destroyed_by_jumptable. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - unfold loc_external_result. - apply agree_set_other; auto. apply agree_set_pair; auto. + unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. + apply agree_undef_caller_save_regs; auto. - (* return *) inv STACKS. simpl in *. diff --git a/riscV/Asm.v b/riscV/Asm.v index 4cd3b1fd..6d223c1d 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -1013,6 +1013,15 @@ Definition preg_of (r: mreg) : preg := | Machregs.F28 => F28 | Machregs.F29 => F29 | Machregs.F30 => F30 | Machregs.F31 => F31 end. +(** Undefine all registers except SP and callee-save registers *) + +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => + if preg_eq r SP + || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) + then rs r + else Vundef. + (** Extract the values of the arguments of an external call. We exploit the calling conventions from module [Conventions], except that we use RISC-V registers instead of locations. *) @@ -1073,7 +1082,7 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> extcall_arguments rs m (ef_sig ef) args -> - rs' = (set_pair (loc_external_result (ef_sig ef) ) res rs)#PC <- (rs RA) -> + rs' = (set_pair (loc_external_result (ef_sig ef) ) res (undef_caller_save_regs rs))#PC <- (rs RA) -> step (State rs m) t (State rs' m'). End RELSEM. diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index cc45a8de..5ec57886 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -975,8 +975,8 @@ Local Transparent destroyed_at_function_entry. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - unfold loc_external_result. - apply agree_set_other; auto. apply agree_set_pair; auto. + unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. + apply agree_undef_caller_save_regs; auto. - (* return *) inv STACKS. simpl in *. @@ -1047,6 +1047,15 @@ Definition preg_of (r: mreg) : preg := | FP0 => ST0 end. +(** Undefine all registers except SP and callee-save registers *) + +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => + if preg_eq r SP + || In_dec preg_eq r (List.map preg_of (List.filter is_callee_save all_mregs)) + then rs r + else Vundef. + (** Extract the values of the arguments of an external call. We exploit the calling conventions from module [Conventions], except that we use machine registers instead of locations. *) @@ -1106,7 +1115,7 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge b = Some (External ef) -> extcall_arguments rs m (ef_sig ef) args -> external_call ef ge args m t res m' -> - rs' = (set_pair (loc_external_result (ef_sig ef)) res rs) #PC <- (rs RA) -> + rs' = (set_pair (loc_external_result (ef_sig ef)) res (undef_caller_save_regs rs)) #PC <- (rs RA) -> step (State rs m) t (State rs' m'). End RELSEM. diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index 38816fd2..3aa87a4c 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -861,8 +861,8 @@ Transparent destroyed_at_function_entry. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - unfold loc_external_result. - apply agree_set_other; auto. apply agree_set_pair; auto. + unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. + apply agree_undef_caller_save_regs; auto. - (* return *) inv STACKS. simpl in *. |