diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocproof.v | 11 | ||||
| -rw-r--r-- | backend/Regalloc.ml | 7 |
2 files changed, 13 insertions, 5 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/Regalloc.ml b/backend/Regalloc.ml index e6e07339..0013d91a 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -915,7 +915,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 |