diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 16:52:02 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 16:52:02 +0200 |
| commit | c58b421571b0354eea602adbdae674bd1f4847e3 (patch) | |
| tree | 8c83d3d7428097523d8af00b9abdcf117532be30 /backend/LTL.v | |
| parent | 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 (diff) | |
| download | compcert-kvx-c58b421571b0354eea602adbdae674bd1f4847e3.tar.gz compcert-kvx-c58b421571b0354eea602adbdae674bd1f4847e3.zip | |
Model external calls as destroying all caller-save registers
The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.
Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.
Diffstat (limited to 'backend/LTL.v')
| -rw-r--r-- | backend/LTL.v | 13 |
1 files changed, 12 insertions, 1 deletions
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, |