diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-16 16:51:42 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-16 16:51:42 +0000 |
| commit | 707b6a1ae9660b13cf6f68c7c0ce74017f5981c5 (patch) | |
| tree | 166a21d507612d60db40737333ddec5003fc81aa /ia32/Asmgenproof.v | |
| parent | e44df4563f1cb893ab25b2a8b25d5b83095205be (diff) | |
Assorted changes to reduce stack and heap requirements when compiling very big functions.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'ia32/Asmgenproof.v')
| -rw-r--r-- | ia32/Asmgenproof.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 060d018..e43392a 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -332,7 +332,7 @@ Lemma transl_find_label: end. Proof. intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. - simpl. eapply transl_code_label; eauto. + simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ; eauto. Qed. End TRANSL_LABEL. @@ -375,6 +375,7 @@ Proof. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. destruct (zlt (list_length_z x) Int.max_unsigned); inv EQ0. + rewrite transl_code'_transl_code in EQ. exists x; exists true; split; auto. unfold fn_code. repeat constructor. - exact transf_function_no_overflow. Qed. @@ -436,7 +437,7 @@ Lemma exec_straight_steps: exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' /\ agree ms2 sp rs2 - /\ (edx_preserved ep i = true -> rs2#EDX = parent_sp s)) -> + /\ (it1_is_parent ep i = true -> rs2#EDX = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ match_states (Mach.State s fb sp c ms2 m2) st'. @@ -455,7 +456,7 @@ Lemma exec_straight_steps_goto: Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl f.(Mach.fn_code) = Some c' -> transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> - edx_preserved ep i = false -> + it1_is_parent ep i = false -> (forall k c (TR: transl_instr f i ep k = OK c), exists jmp, exists k', exists rs2, exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' @@ -868,7 +869,7 @@ Opaque loadind. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. - generalize EQ; intros EQ'. monadInv EQ'. + generalize EQ; intros EQ'. monadInv EQ'. rewrite transl_code'_transl_code in EQ0. destruct (zlt (list_length_z x0) Int.max_unsigned); inversion EQ1. clear EQ1. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. |