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/Mach.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/Mach.v')
| -rw-r--r-- | backend/Mach.v | 5 |
1 files changed, 4 insertions, 1 deletions
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: |