diff options
Diffstat (limited to 'backend/Conventions.v')
-rw-r--r-- | backend/Conventions.v | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/backend/Conventions.v b/backend/Conventions.v index bdc4c8b6..989bfa05 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -103,3 +103,56 @@ Proof. generalize (loc_arguments_bounded _ _ _ H0). generalize (typesize_pos ty). omega. Qed. + + +(** * Callee-save locations *) + +(** We classify locations as either +- callee-save, i.e. preserved across function calls: + callee-save registers, [Local] and [Incoming] stack slots; +- caller-save, i.e. possibly modified by a function call: + non-callee-save registers, [Outgoing] stack slots. + +Concerning [Outgoing] stack slots: several ABIs allow a function to modify +the stack slots used for passing parameters to this function. +The code currently generated by CompCert never does so, but the code +generated by other compilers often does so (e.g. GCC for x86-32). +Hence, CompCert-generated code must not assume that [Outgoing] stack slots +are preserved across function calls, because they might not be preserved +if the called function was compiled by another compiler. +*) + +Definition callee_save_loc (l: loc) := + match l with + | R r => is_callee_save r = true + | S sl ofs ty => sl <> Outgoing + end. + +Hint Unfold callee_save_loc. + +Definition agree_callee_save (ls1 ls2: Locmap.t) : Prop := + forall l, callee_save_loc l -> ls1 l = ls2 l. + +(** * Assigning result locations *) + +(** Useful lemmas to reason about the result of an external call. *) + +Lemma locmap_get_set_loc_result: + forall sg v rs l, + match l with R r => is_callee_save r = true | S _ _ _ => True end -> + Locmap.setpair (loc_result sg) v rs l = rs l. +Proof. + intros. apply Locmap.gpo. + assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). + { intros. destruct l; simpl. congruence. auto. } + generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto. +Qed. + +Lemma locmap_get_set_loc_result_callee_save: + forall sg v rs l, + callee_save_loc l -> + Locmap.setpair (loc_result sg) v rs l = rs l. +Proof. + intros. apply locmap_get_set_loc_result. + red in H; destruct l; auto. +Qed. |