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/Linear.v | |
| parent | 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 (diff) | |
| download | compcert-c58b421571b0354eea602adbdae674bd1f4847e3.tar.gz compcert-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/Linear.v')
| -rw-r--r-- | backend/Linear.v | 2 |
1 files changed, 1 insertions, 1 deletions
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: |