diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-04-09 16:59:13 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-04-09 16:59:13 +0000 |
commit | abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 (patch) | |
tree | ae109a136508da283a9e2be5f039c5f9cca4f95c /backend/Constpropproof.v | |
parent | ffd6080f9e1e742c73ac38354b31c6fc4e3963ba (diff) | |
download | compcert-abe2bb5c40260a31ce5ee27b841bcbd647ff8b88.tar.gz compcert-abe2bb5c40260a31ce5ee27b841bcbd647ff8b88.zip |
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
Diffstat (limited to 'backend/Constpropproof.v')
-rw-r--r-- | backend/Constpropproof.v | 18 |
1 files changed, 9 insertions, 9 deletions
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. |