Module ClightEquivalences

Require Import Coqlib.
Require Import Maps.
Require Import Values.
Require Import Globalenvs.
Require Import Events.
Require Import Ctypes.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import NormaliseSpec.
Require Import Memory.
Require Import Memdata.
Require Import Cop.
Require Import Integers.
Require Import Clight.
Require Import Equivalences.

This modules defines useful lemmas about equivalences of symbolic expressions and memories, and in particular in relation with Clight semantics.


We lift the notion of equivalence on temporary environments.
Definition temp_env_equiv (le le': temp_env) : Prop :=
  forall i,
    match PTree.get i le, PTree.get i le' with
        Some a, Some b => same_eval a b
      | None, None => True
      | _, _ => False
    end.

Lemma temp_env_equiv_set:
  forall le le',
    temp_env_equiv le le' ->
    forall id v v',
      same_eval v v' ->
      temp_env_equiv (PTree.set id v le) (PTree.set id v' le').
Proof.
  red; intros.
  rewrite ! PTree.gsspec.
  destruct (peq i id); subst; auto.
  apply H.
Qed.

Lemma bind_parameter_temps_equiv:
  forall args args',
          list_forall2 same_eval args args' ->
          forall par tmp tmp' le,
            temp_env_equiv tmp tmp' ->
            bind_parameter_temps par args tmp = Some le ->
            exists le',
              bind_parameter_temps par args' tmp' = Some le' /\ temp_env_equiv le le'.
Proof.
  induction 1; simpl; intros.
  - destruct par; simpl in *.
    + inv H0. eexists; split; eauto.
    + destruct p; congruence.
  - destruct par; simpl in H2. congruence.
    destruct p.
    eapply IHlist_forall2 in H2; eauto.
    apply temp_env_equiv_set; auto.
Qed.

Lemma temp_equiv_refl:
  forall t,
    temp_env_equiv t t.
Proof.
  red; intros; destr_cond_match; auto; reflexivity.
Qed.

Lemma deref_loc_same_eval:
  forall t m a a' v,
    deref_loc t m a v ->
    same_eval a a' ->
    exists v',
      deref_loc t m a' v' /\ same_eval v v'.
Proof.
  intros t m a a' v DL SE; inv DL.
  - unfold Mem.loadv in H0; revert H0; destr_cond_match; try discriminate.
    intro.
    rewrite (same_eval_eqm _ _ _ _ SE) in Heqv0.
    eexists; split; eauto.
    econstructor; eauto.
    unfold Mem.loadv. rewrite Heqv0; eauto.
    reflexivity.
  - eexists; split; eauto.
    eapply deref_loc_reference; eauto.
  - eexists; split; eauto.
    eapply deref_loc_copy; eauto.
Qed.


Lemma temp_equiv_clight_eval_expr_lvalue:
  forall ge m e le le',
    temp_env_equiv le le' ->
    (forall a v,
       Clight.eval_expr ge e le m a v ->
       exists v',
         Clight.eval_expr ge e le' m a v' /\
         same_eval v v')
    /\(forall a ptr,
         Clight.eval_lvalue ge e le m a ptr ->
         exists ptr',
           Clight.eval_lvalue ge e le' m a ptr' /\
           same_eval ptr ptr').
Proof.
  intros ge m e le le' ME.
  apply eval_expr_lvalue_ind; intros;
  try (eexists; split; eauto; econstructor; eauto; reflexivity).
  -
     specialize (ME id).
     rewrite H in ME.
     revert ME; destr_cond_match; try intuition congruence.
     intros; eexists; split; eauto.
     constructor; eauto.
  -
    destruct H0 as [v' [A B]].
    eexists; split; eauto.
    econstructor; simpl; eauto.
  -
    destruct (H0) as [v' [A B]].
    eexists; split; eauto.
    econstructor; simpl; eauto.
    subst.
    apply sem_unary_operation_expr_se; auto.
  -
    destruct (H0) as [v' [A B]].
    destruct (H2) as [v'' [C D]].
    generalize (sem_binary_operation_expr_se m op (typeof a1) (typeof a2) _ _ _ _
                                             B D).
    rewrite H3.
    destr_cond_match; intros; try intuition congruence.
    eexists; split; eauto.
    econstructor; simpl; eauto.
  -
    destruct (H0) as [v' [A B]].
    generalize (sem_cast_expr_se (typeof a) ty _ _ B).
    rewrite H1.
    destr_cond_match; intros; try intuition congruence.
    eexists; split; eauto.
    econstructor; simpl; eauto.
  -
    destruct H0 as [v' [A B]].
    apply (deref_loc_same_eval) with (a':=v') in H1; auto.
    destruct H1 as [v2 [C D]].
    eexists; split; eauto. econstructor; eauto.
  -
    eexists; split. apply eval_Evar_global; eauto.
    reflexivity.
  -
    destruct H0 as [v' [A B]].
    eexists; split; eauto. econstructor; eauto.
  -
    destruct (H0) as [v' [A B]].
    eexists; split; eauto. econstructor; eauto.
    se_rew.
  -
    destruct (H0) as [v' [A B]].
    eexists; split; eauto. econstructor; eauto.
Qed.


Lemma temp_equiv_clight_eval_expr:
  forall ge e le le' m,
    temp_env_equiv le le' ->
    forall a v,
       Clight.eval_expr ge e le m a v ->
       exists v',
         Clight.eval_expr ge e le' m a v' /\
         same_eval v v'.
Proof.
  intros ge e le le' m' TE.
  apply (proj1 (temp_equiv_clight_eval_expr_lvalue ge m' e le le' TE)).
Qed.

Lemma temp_equiv_clight_eval_exprlist:
  forall ge e le le' m,
    temp_env_equiv le le' ->
    forall al tl vl,
       Clight.eval_exprlist ge e le m al tl vl ->
       exists vl',
         Clight.eval_exprlist ge e le' m al tl vl' /\
         list_forall2 same_eval vl vl'.
Proof.
  induction al; simpl; intros.
  - inv H0. (exists nil; split; auto); constructor.
  - inv H0.
    apply IHal in H7.
    destruct H7 as [vl' [A B]].
    eapply temp_equiv_clight_eval_expr in H3; eauto.
    destruct H3 as [v' [C D]].
    generalize (sem_cast_expr_se (typeof a) ty _ _ D); rewrite H4.
    destr_cond_match; try intuition congruence.
    intro.
    exists ( e0 :: vl'); split.
    econstructor; eauto.
    constructor; auto.
Qed.

Lemma temp_equiv_clight_eval_lvalue:
  forall ge e le le' m,
    temp_env_equiv le le' ->
    forall a ptr,
      Clight.eval_lvalue ge e le m a ptr ->
      exists ptr',
        Clight.eval_lvalue ge e le' m a ptr' /\
        same_eval ptr ptr'.
Proof.
  intros ge e le le' m' TE.
  apply (proj2 (temp_equiv_clight_eval_expr_lvalue ge m' e le le' TE)).
Qed.

Lemma mem_equiv_deref_loc:
  forall t m locofs v m',
    mem_equiv m m' ->
    deref_loc t m locofs v ->
    exists v',
      deref_loc t m' locofs v' /\ same_eval v v'.
Proof.
  intros t m locofs v m' ME DL; inv DL.
  - apply (loadv_mem_equiv _ m') in H0; auto.
    destruct H0 as [v' [LV B]].
    eexists; split; eauto.
    econstructor; eauto.
  - eexists; split; eauto.
    eapply deref_loc_reference; eauto. reflexivity.
  - eexists; split; eauto.
    eapply deref_loc_copy; eauto. reflexivity.
Qed.

Lemma mem_equiv_clight_eval_expr_lvalue:
  forall ge e le m m',
    mem_equiv m m' ->
    (forall a v,
       Clight.eval_expr ge e le m a v ->
       exists v',
         Clight.eval_expr ge e le m' a v' /\
         same_eval v v')
    /\(forall a v,
         Clight.eval_lvalue ge e le m a v ->
         exists v',
           Clight.eval_lvalue ge e le m' a v' /\
           same_eval v v').
Proof.
  intros ge e le m m' ME.
  apply eval_expr_lvalue_ind; intros.
-
  eexists; split; eauto.
  econstructor; eauto.
  reflexivity.
-
  eexists; split; eauto.
  econstructor; eauto.
  reflexivity.
-
    eexists; split; eauto.
  econstructor; eauto.
  reflexivity.
-
    eexists; split; eauto.
  econstructor; eauto.
  reflexivity.
-
  eexists; split; eauto.
  constructor; eauto. reflexivity.
-
  destruct H0 as [v' [A B]].
  eexists; split; eauto.
  econstructor; simpl; eauto.
-
  destruct (H0) as [v' [A B]].
  eexists; split; eauto.
  econstructor; simpl; eauto.
  subst.
  apply sem_unary_operation_expr_se; auto.
-
  destruct (H0) as [v' [A B]].
  destruct (H2) as [v'' [C D]].
  generalize (sem_binary_operation_expr_se m op (typeof a1) (typeof a2) _ _ _ _
                                           B D).
  rewrite H3.
  destr_cond_match; intros; try intuition congruence.
  eexists; split; eauto.
  econstructor; simpl; eauto.
-
  destruct (H0) as [v' [A B]].
  generalize (sem_cast_expr_se (typeof a) ty _ _ B).
  rewrite H1.
  destr_cond_match; intros; try intuition congruence.
  eexists; split; eauto.
  econstructor; simpl; eauto.
-
  destruct H0 as [v' [A B]].
  apply (mem_equiv_deref_loc) with (m':=m') in H1; auto.
  destruct H1 as [v'' [C D]].
  apply deref_loc_same_eval with (a':=v') in C; auto.
  destruct C as [v3 [E F]].
  eexists; split.
  econstructor; eauto.
  rewrite D; auto.
-
  eexists; split. econstructor; eauto.
  reflexivity.
-
  eexists; split. apply eval_Evar_global; eauto.
  reflexivity.
-
  destruct H0 as [v' [A B]].
  eexists; split; eauto.
  econstructor; eauto.
-
  destruct (H0) as [v' [A B]].
  eexists; split.
  econstructor; eauto.
  apply binop_same_eval; auto.
  reflexivity.
-
  destruct (H0) as [v' [A B]].
  eexists; split; eauto.
  eapply eval_Efield_union; eauto.
Qed.

Lemma mem_equiv_clight_eval_expr:
  forall ge e le m m',
    mem_equiv m m' ->
    forall a sv,
    Clight.eval_expr ge e le m a sv ->
    exists sv',
      Clight.eval_expr ge e le m' a sv' /\
      same_eval sv sv'.
Proof.
  intros ge e le m m' ME.
  exact (proj1 (mem_equiv_clight_eval_expr_lvalue ge e le _ _ ME)).
Qed.

Lemma mem_equiv_clight_eval_exprlist:
  forall ge e le m m',
    mem_equiv m m' ->
    forall al tl sv,
    Clight.eval_exprlist ge e le m al tl sv ->
    exists sv',
      Clight.eval_exprlist ge e le m' al tl sv' /\
      list_forall2 same_eval sv sv'.
Proof.
  induction al; simpl; intros.
  - inv H0. eexists; split; eauto; constructor.
  - inv H0. apply IHal in H7.
    destruct H7 as [sv' [A B]].
    eapply mem_equiv_clight_eval_expr in H3; eauto.
    destruct H3 as [sv'0 [C D]].
    generalize (sem_cast_expr_se (typeof a) ty _ _ D); rewrite H4.
    destr_cond_match; try intuition congruence.
    intro.
    exists (e0 :: sv'); split; eauto.
    econstructor; eauto.
    constructor; auto.
Qed.

Lemma mem_equiv_clight_eval_lvalue:
  forall ge e le m m',
    mem_equiv m m' ->
    forall a ptr,
      Clight.eval_lvalue ge e le m a ptr ->
      exists ptr',
        Clight.eval_lvalue ge e le m' a ptr' /\
        same_eval ptr ptr'.
Proof.
  intros ge e le m m' ME.
  exact (proj2 (mem_equiv_clight_eval_expr_lvalue ge e le _ _ ME)).
Qed.

Lemma mem_equiv_assign_loc:
  forall t m addr v m' m2,
    mem_equiv m m' ->
    assign_loc t m addr v m2 ->
    exists m2',
      assign_loc t m' addr v m2' /\
      mem_equiv m2 m2'.
Proof.
  intros t m addr v m' m2 ME AL; inv AL.
  - eapply storev_mem_equiv in H0; eauto.
    destruct H0 as [v' [ST B]].
    eexists; split; eauto.
    econstructor; eauto.
  -
    eapply mem_equiv_loadbytes in H3; eauto.
    eapply storebytes_mem_equiv in H4; eauto.
    destruct H3 as [v' [A B]].
    destruct H4 as [m0 [C D]].
    eapply (storebytes_val_equiv) in C; eauto.
    destruct C as [m1 [E F]].
    exists m1; split; auto.
    eapply assign_loc_copy with (ofs':=ofs') (ofs:=ofs); eauto.
    rewrite <- H5.
    apply mem_equiv_norm; symmetry; eauto.
    rewrite <- H6.
    apply mem_equiv_norm; symmetry; eauto.
    rewrite D; rewrite F; reflexivity.
Qed.

Lemma val_equiv_assign_loc:
  forall t m addr v v' m2,
    assign_loc t m addr v m2 ->
    same_eval v v' ->
    exists m2',
      assign_loc t m addr v' m2' /\
      mem_equiv m2 m2'.
Proof.
  intros t m addr v v' m2 AL SE; inv AL.
  - eapply storev_val_equiv in H0; eauto.
    destruct H0 as [m2' [ST B]].
    eexists; split; eauto.
    econstructor; eauto.
  - eexists; split.
    eapply (assign_loc_copy t m addr _ _ _ ofs' bytes m2); eauto.
    rewrite <- H5.
    apply same_eval_eqm; symmetry; auto.
    reflexivity.
Qed.


Lemma addr_equiv_assign_loc:
  forall t m addr addr' v m2,
    assign_loc t m addr v m2 ->
    same_eval addr addr' ->
    assign_loc t m addr' v m2.
Proof.
  intros t m addr addr' v m2 AL SE; inv AL.
  - eapply assign_loc_value; eauto.
    revert H0; unfold Mem.storev.
    rewrite (same_eval_eqm _ _ _ _ SE).
    auto.
  -
    eapply (assign_loc_copy t m addr' _ _ _ ofs' bytes m2); eauto.
    rewrite <- H6.
    apply same_eval_eqm; symmetry; auto.
Qed.





Generated by coq2html