From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constpropproof.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 1dad5187..d534c756 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -283,13 +283,13 @@ Proof. exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args); intros op' args' OSR. - assert (eval_operation tge sp op' rs##args' = Some v). + assert (eval_operation tge sp op' rs##args' m = Some v). rewrite (eval_operation_preserved _ _ symbols_preserved). - generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs + generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs m MATCH op args v). rewrite OSR; simpl. auto. generalize (eval_static_operation_correct ge op sp - (approx_regs (analyze f)!!pc args) rs##args v + (approx_regs (analyze f)!!pc args) rs##args m v (approx_regs_val_list _ _ _ args MATCH) H0). case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros; simpl in H2; @@ -370,14 +370,14 @@ Proof. exists (State s' (transf_function f) sp ifso rs m); split. caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); intros cond' args' CSR. - assert (eval_condition cond' rs##args' = Some true). + assert (eval_condition cond' rs##args' m = Some true). generalize (cond_strength_reduction_correct - ge (approx_reg (analyze f)!!pc) rs MATCH cond args). + ge (approx_reg (analyze f)!!pc) rs m MATCH cond args). rewrite CSR. intro. congruence. TransfInstr. rewrite CSR. caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ _ + generalize (eval_static_condition_correct ge cond _ _ m _ (approx_regs_val_list _ _ _ args MATCH) ESC); intro. replace b with true. intro; eapply exec_Inop; eauto. congruence. intros. eapply exec_Icond_true; eauto. @@ -390,14 +390,14 @@ Proof. exists (State s' (transf_function f) sp ifnot rs m); split. caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); intros cond' args' CSR. - assert (eval_condition cond' rs##args' = Some false). + assert (eval_condition cond' rs##args' m = Some false). generalize (cond_strength_reduction_correct - ge (approx_reg (analyze f)!!pc) rs MATCH cond args). + ge (approx_reg (analyze f)!!pc) rs m MATCH cond args). rewrite CSR. intro. congruence. TransfInstr. rewrite CSR. caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). intros b ESC. - generalize (eval_static_condition_correct ge cond _ _ _ + generalize (eval_static_condition_correct ge cond _ _ m _ (approx_regs_val_list _ _ _ args MATCH) ESC); intro. replace b with false. intro; eapply exec_Inop; eauto. congruence. intros. eapply exec_Icond_false; eauto. -- cgit