From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - Added alignment constraints to memory loads and stores. - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Allocproof.v | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) (limited to 'backend/Allocproof.v') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 5e38934..3971fb6 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -601,7 +601,7 @@ Proof. rewrite <- H1. eapply agree_move_live; eauto. (* Not a move *) intros INMO CORR CODE. - assert (eval_operation tge sp op (map ls (map assign args)) m = Some v). + assert (eval_operation tge sp op (map ls (map assign args)) = Some v). replace (map ls (map assign args)) with (rs##args). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. eapply agree_eval_regs; eauto. @@ -671,25 +671,15 @@ Proof. rewrite (sig_function_translated _ _ TF). eauto. rewrite H1. econstructor; eauto. - (* Ialloc *) - assert (ls (assign arg) = Vint sz). - rewrite <- H0. symmetry. eapply agree_eval_reg; eauto. - econstructor; split. - eapply exec_Lalloc; eauto. TranslInstr. - generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). - unfold correct_alloc_instr. intros [CORR1 CORR2]. - MatchStates. - eapply agree_postcall with (args := arg :: nil) (ros := inr reg 1%positive); eauto. - (* Icond, true *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some true). + assert (COND: eval_condition cond (map ls (map assign args)) = Some true). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lcond_true; eauto. TranslInstr. MatchStates. eapply agree_reg_list_live. eauto. (* Icond, false *) - assert (COND: eval_condition cond (map ls (map assign args)) m = Some false). + assert (COND: eval_condition cond (map ls (map assign args)) = Some false). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. -- cgit v1.2.3