diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocproof.v | 11 | ||||
| -rw-r--r-- | backend/RTLgen.v | 21 | ||||
| -rw-r--r-- | backend/Regalloc.ml | 12 |
3 files changed, 23 insertions, 21 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 154c1e2e..47dac12f 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1890,7 +1890,8 @@ Proof. { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. eapply reg_unconstrained_satisf. eauto. eapply add_equations_satisf; eauto. assumption. - rewrite Regmap.gss. apply Val.lessdef_trans with v1'; auto. + rewrite Regmap.gss. + apply Val.lessdef_trans with v1'; unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. assert (LD3: Val.lessdef_list rs##args (reglist ls3 args2')). @@ -1906,7 +1907,8 @@ Proof. assert (SAT4: satisf (rs#dst <- v) ls4 e0). { eapply loc_unconstrained_satisf. eapply can_undef_satisf; eauto. eapply add_equations_satisf; eauto. assumption. - rewrite Regmap.gss. apply Val.lessdef_trans with v2'; auto. + rewrite Regmap.gss. + apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. } exploit (exec_moves mv3); eauto. intros [ls5 [A5 B5]]. econstructor; split. @@ -1938,7 +1940,8 @@ Proof. set (ls2 := Locmap.set (R dst') v1'' (undef_regs (destroyed_by_load Mint32 addr) ls1)). assert (SAT2: satisf (rs#dst <- v) ls2 e0). { eapply parallel_assignment_satisf; eauto. - apply Val.lessdef_trans with v1'; auto. + apply Val.lessdef_trans with v1'; + unfold sel_val; unfold kind_first_word; unfold v1'; destruct Archi.big_endian; auto. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. @@ -1968,7 +1971,7 @@ Proof. set (ls2 := Locmap.set (R dst') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls1)). assert (SAT2: satisf (rs#dst <- v) ls2 e0). { eapply parallel_assignment_satisf; eauto. - apply Val.lessdef_trans with v2'; auto. + apply Val.lessdef_trans with v2'; unfold sel_val; unfold kind_second_word; unfold v2'; destruct Archi.big_endian; auto. eapply can_undef_satisf. eauto. eapply add_equations_satisf; eauto. } exploit (exec_moves mv2); eauto. intros [ls3 [A3 B3]]. diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 49d79fb2..11da630b 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -23,7 +23,7 @@ Require Import Registers. Require Import CminorSel. Require Import RTL. -Open Local Scope string_scope. +Local Open Scope string_scope. (** * Translation environments and state *) @@ -112,16 +112,13 @@ Implicit Arguments Error [A s]. Definition mon (A: Type) : Type := forall (s: state), res A s. -Definition ret (A: Type) (x: A) : mon A := +Definition ret {A: Type} (x: A) : mon A := fun (s: state) => OK x s (state_incr_refl s). -Implicit Arguments ret [A]. -Definition error (A: Type) (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. +Definition error {A: Type} (msg: Errors.errmsg) : mon A := fun (s: state) => Error msg. -Implicit Arguments error [A]. - -Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B := +Definition bind {A B: Type} (f: mon A) (g: A -> mon B) : mon B := fun (s: state) => match f s with | Error msg => Error msg @@ -132,27 +129,21 @@ Definition bind (A B: Type) (f: mon A) (g: A -> mon B) : mon B := end end. -Implicit Arguments bind [A B]. - -Definition bind2 (A B C: Type) (f: mon (A * B)) (g: A -> B -> mon C) : mon C := +Definition bind2 {A B C: Type} (f: mon (A * B)) (g: A -> B -> mon C) : mon C := bind f (fun xy => g (fst xy) (snd xy)). -Implicit Arguments bind2 [A B C]. - Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) (at level 200, X ident, Y ident, A at level 100, B at level 200). -Definition handle_error (A: Type) (f g: mon A) : mon A := +Definition handle_error {A: Type} (f g: mon A) : mon A := fun (s: state) => match f s with | OK a s' i => OK a s' i | Error _ => g s end. -Implicit Arguments handle_error [A]. - (** ** Operations on state *) (** The initial state (empty CFG). *) diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index e6e07339..b91bad27 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -657,9 +657,12 @@ let add_interfs_instr g instr live = | Xstore(chunk, addr, args, src) -> add_interfs_destroyed g live (destroyed_by_store chunk addr) | Xcall(sg, vos, args, res) -> + begin match vos with + | Coq_inl v -> List.iter (fun r -> IRC.add_interf g (vmreg r) v) destroyed_at_indirect_call + | _ -> () end; add_interfs_destroyed g (vset_removelist res live) destroyed_at_call | Xtailcall(sg, Coq_inl v, args) -> - List.iter (fun r -> IRC.add_interf g (vmreg r) v) int_callee_save_regs + List.iter (fun r -> IRC.add_interf g (vmreg r) v) (int_callee_save_regs @ destroyed_at_indirect_call) | Xtailcall(sg, Coq_inr id, args) -> () | Xbuiltin(ef, args, res) -> @@ -915,7 +918,12 @@ let spill_instr tospill eqs instr = | false, true -> let eqs1 = add arg1 res (kill res eqs) in let (argl', c1, eqs2) = reload_vars tospill eqs1 argl in - (Xreload(arg1, res) :: c1 @ [Xop(op, res :: argl', res)], + (* PR#113, PR#122: [Xreload] here causes [res] to become + unspillable in the future. This is too strong, hence + the [Xmove]. Alternatively, this [false, true] + case could be removed and the [true, true] case + below used instead. *) + (Xmove(arg1, res) :: c1 @ [Xop(op, res :: argl', res)], kill res eqs2) | true, true -> let tmp = new_temp (typeof res) in |