diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-28 12:13:15 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-28 12:13:15 +0000 |
commit | 04d0d602ef7245fd566debd91bcb148acd9ed067 (patch) | |
tree | 77a11f3e551303521aa72af1e63cea0285bcd1bc /powerpc/Asmgenproof.v | |
parent | b8e535ccf82385573f80f6d146c04892b25ea0a6 (diff) |
PowerPC port: refactored the expansion of built-in functions and
pseudo-instructions so that it does not need to be re-done in
cchecklink.
cchecklink: updated accordingly.
testsuite: compile with -sdump and run cchecklink if supported.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc/Asmgenproof.v')
-rw-r--r-- | powerpc/Asmgenproof.v | 24 |
1 files changed, 15 insertions, 9 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 913fb50..2b52fe0 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -918,30 +918,36 @@ Local Transparent destroyed_by_jumptable. set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)). set (rs3 := nextinstr (rs2#GPR0 <- (rs0#LR))). set (rs4 := nextinstr rs3). + set (rs5 := nextinstr rs4). assert (EXEC_PROLOGUE: exec_straight tge x x.(fn_code) rs0 m' - x1 rs4 m3'). + x1 rs5 m3'). rewrite <- H5 at 2. simpl. - apply exec_straight_three with rs2 m2' rs3 m2'. + apply exec_straight_step with rs2 m2'. unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). rewrite F. auto. - simpl. auto. + rewrite <- (sp_val _ _ _ AG). rewrite F. auto. auto. + apply exec_straight_step with rs3 m2'. + simpl. auto. auto. + apply exec_straight_two with rs4 m3'. simpl. unfold store1. rewrite gpr_or_zero_not_zero. change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. rewrite Int.add_zero_l. simpl in P. rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. congruence. auto. auto. auto. - left; exists (State rs4 m3'); split. + left; exists (State rs5 m3'); split. eapply exec_straight_steps_1; eauto. omega. constructor. econstructor; eauto. - change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone). rewrite ATPC. simpl. constructor; eauto. - subst x; simpl in g. unfold fn_code. eapply code_tail_next_int. omega. + subst x; simpl in g. unfold fn_code. eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. constructor. - unfold rs4, rs3, rs2. - apply agree_nextinstr. apply agree_set_other; auto. apply agree_set_other; auto. + unfold rs5, rs4, rs3, rs2. + apply agree_nextinstr. apply agree_nextinstr. + apply agree_set_other; auto. apply agree_set_other; auto. apply agree_nextinstr. apply agree_set_other; auto. eapply agree_change_sp; eauto. unfold sp; congruence. congruence. |