Function calling conventions and other conventions regarding the use of
machine registers and stack slots.
Require Import Coqlib.
Require Import AST.
Require Import Locations.
Require Export Conventions1.
Require Import sflib.
The processor-dependent and EABI-dependent definitions are in
arch/abi/Conventions1.v. This file adds various processor-independent
definitions and lemmas.
Lemma loc_arguments_acceptable_2:
forall s l,
In l (
regs_of_rpairs (
loc_arguments s)) ->
loc_argument_acceptable l.
Proof.
intros until l.
generalize (
loc_arguments_acceptable s).
generalize (
loc_arguments s).
induction l0 as [ |
p pl];
simpl;
intros.
-
contradiction.
-
rewrite in_app_iff in H0.
destruct H0.
exploit H;
eauto.
destruct p;
simpl in *;
intuition congruence.
apply IHpl;
auto.
Qed.
Location of function parameters
A function finds the values of its parameter in the same locations
where its caller stored them, except that the stack-allocated arguments,
viewed as Outgoing slots by the caller, are accessed via Incoming
slots (at the same offsets and types) in the callee.
Definition parameter_of_argument (
l:
loc) :
loc :=
match l with
|
S Outgoing n ty =>
S Incoming n ty
|
_ =>
l
end.
Definition loc_parameters (
s:
signature) :
list (
rpair loc) :=
List.map (
map_rpair parameter_of_argument) (
loc_arguments s).
Lemma incoming_slot_in_parameters:
forall ofs ty sg,
In (
S Incoming ofs ty) (
regs_of_rpairs (
loc_parameters sg)) ->
In (
S Outgoing ofs ty) (
regs_of_rpairs (
loc_arguments sg)).
Proof.
Tail calls
A tail-call is possible for a signature if the corresponding
arguments are all passed in registers.
A tail-call is possible for a signature if the corresponding
arguments are all passed in registers.
Definition tailcall_possible (
s:
signature) :
Prop :=
forall l,
In l (
regs_of_rpairs (
loc_arguments s)) ->
match l with R _ =>
True |
S _ _ _ =>
False end.
Decide whether a tailcall is possible.
Definition tailcall_is_possible (
sg:
signature) :
bool :=
List.forallb
(
fun l =>
match l with R _ =>
true |
S _ _ _ =>
false end)
(
regs_of_rpairs (
loc_arguments sg)).
Lemma tailcall_is_possible_correct:
forall s,
tailcall_is_possible s =
true ->
tailcall_possible s.
Proof.
Lemma zero_size_arguments_tailcall_possible:
forall sg,
size_arguments sg = 0 ->
tailcall_possible sg.
Proof.
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.
Definition agree_callee_save_regs (
ls1 ls2:
Locmap.t) :
Prop :=
forall r,
is_callee_save r =
true ->
ls1 (
R r) =
ls2 (
R r).
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.
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.
Local Opaque Z.add Z.mul Z.divide list_nth_z.
Lemma tailcall_size_aux
tys ir fr
(
TAIL:
forall l,
In l (
regs_of_rpairs (
loc_arguments_64 tys ir fr 0)) ->
match l with
|
R _ =>
True
|
S _ _ _ =>
False
end)
(
IRBOUND: (
ir - 1) <
list_length_z int_param_regs)
(
FRBOUND: (
fr - 1) <
list_length_z float_param_regs):
<<
SZ:
size_arguments_64 tys ir fr 0 = 0>>.
Proof.
ginduction tys;
ii;
ss.
destruct a;
des_ifs;
ss;
try (
by exploit TAIL;
eauto;
ss);
(
eapply IHtys;
eauto;
[
ii;
des_ifs; [];
exploit TAIL;
eauto
|
rewrite Z.add_simpl_r;
apply list_nth_z_range in Heq;
xomega]).
Qed.
Lemma tailcall_size
sg
(
TAIL:
tailcall_possible sg):
size_arguments sg = 0.
Proof.
Class main_args_ctx:
Type := {
main_args:
bool }.
Local Instance main_args_none:
main_args_ctx := {
main_args :=
false }.