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/CSEproof.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/CSEproof.v')
-rw-r--r-- | backend/CSEproof.v | 49 |
1 files changed, 19 insertions, 30 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 275b9fd2..53576adb 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -208,9 +208,10 @@ Lemma kill_load_eqs_incl: Proof. induction eqs; simpl; intros. apply incl_refl. - destruct a. destruct r. apply incl_same_head; auto. - auto. - apply incl_tl. auto. + destruct a. destruct r. + destruct (op_depends_on_memory o). auto with coqlib. + apply incl_same_head; auto. + auto with coqlib. Qed. Lemma wf_kill_loads: @@ -400,7 +401,7 @@ Definition rhs_evals_to (valu: valnum -> val) (rh: rhs) (v: val) : Prop := match rh with | Op op vl => - eval_operation ge sp op (List.map valu vl) = Some v + eval_operation ge sp op (List.map valu vl) m = Some v | Load chunk addr vl => exists a, eval_addressing ge sp addr (List.map valu vl) = Some a /\ @@ -481,7 +482,7 @@ Lemma add_op_satisfiable: forall n rs op args dst v, wf_numbering n -> numbering_satisfiable ge sp rs m n -> - eval_operation ge sp op rs##args = Some v -> + eval_operation ge sp op rs##args m = Some v -> numbering_satisfiable ge sp (rs#dst <- v) m (add_op n dst op args). Proof. intros. inversion H0. @@ -547,36 +548,22 @@ Proof. eauto. Qed. -(** Allocation of a fresh memory block preserves satisfiability. *) - -Lemma alloc_satisfiable: - forall lo hi b m' rs n, - Mem.alloc m lo hi = (m', b) -> - numbering_satisfiable ge sp rs m n -> - numbering_satisfiable ge sp rs m' n. -Proof. - intros. destruct H0 as [valu [A B]]. - exists valu; split; intros. - generalize (A _ _ H0). destruct rh; simpl. - auto. - intros [addr [C D]]. exists addr; split. auto. - destruct addr; simpl in *; try discriminate. - eapply Mem.load_alloc_other; eauto. - eauto. -Qed. - (** [kill_load] preserves satisfiability. Moreover, the resulting numbering is satisfiable in any concrete memory state. *) Lemma kill_load_eqs_ops: forall v rhs eqs, In (v, rhs) (kill_load_eqs eqs) -> - match rhs with Op _ _ => True | Load _ _ _ => False end. + match rhs with + | Op op _ => op_depends_on_memory op = false + | Load _ _ _ => False + end. Proof. induction eqs; simpl; intros. elim H. - destruct a. destruct r. - elim H; intros. inversion H0; subst v0; subst rhs. auto. + destruct a. destruct r. destruct (op_depends_on_memory o) as [] _eqn. + apply IHeqs; auto. + simpl in H; destruct H. inv H. auto. apply IHeqs. auto. apply IHeqs. auto. Qed. @@ -590,7 +577,9 @@ Proof. exists x. split; intros. generalize (H _ _ (H1 _ H2)). generalize (kill_load_eqs_ops _ _ _ H2). - destruct rh; simpl; tauto. + destruct rh; simpl. + intros. rewrite <- H4. apply op_depends_on_memory_correct; auto. + tauto. apply H0. auto. Qed. @@ -645,7 +634,7 @@ Lemma find_op_correct: wf_numbering n -> numbering_satisfiable ge sp rs m n -> find_op n op args = Some r -> - eval_operation ge sp op rs##args = Some rs#r. + eval_operation ge sp op rs##args m = Some rs#r. Proof. intros until r. intros WF [valu NH]. unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND. @@ -834,14 +823,14 @@ Proof. (* Iop *) exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. - assert (eval_operation tge sp op rs##args = Some v). + assert (eval_operation tge sp op rs##args m = Some v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. generalize C; clear C. case (is_trivial_op op). intro. eapply exec_Iop'; eauto. caseEq (find_op (analyze f)!!pc op args). intros r FIND CODE. eapply exec_Iop'; eauto. simpl. - assert (eval_operation ge sp op rs##args = Some rs#r). + assert (eval_operation ge sp op rs##args m = Some rs#r). eapply find_op_correct; eauto. eapply wf_analyze; eauto. congruence. |