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/Allocproof.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/Allocproof.v')
| -rw-r--r-- | backend/Allocproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 585fb0da..068e0de0 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2476,7 +2476,8 @@ Proof. rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. rewrite val_longofwords_eq_1 by auto. auto. red; intros. rewrite (AG l H0). - symmetry; apply Locmap.gpo. + rewrite Locmap.gpo. + unfold undef_caller_save_regs. destruct l; auto. simpl in H0; rewrite H0; auto. assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). { intros. destruct l; simpl in *. congruence. auto. } generalize (loc_result_caller_save (ef_sig ef)). destruct (loc_result (ef_sig ef)); simpl; intuition auto. |