Module MoreAxioms

Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Events.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.


Axiom external_functions_mem_inject_gen':
    forall name sg (ge1 ge2 : Senv.t)
      (vargs : list val) (m1 : mem) (t : trace)
      (vres : val) (m2 : mem) (f : block -> option (block * Z))
      (m1' : mem) (vargs' : list val),
      symbols_inject f ge1 ge2 ->
      external_call (EF_external name sg) ge1 vargs m1 t vres m2 ->
      Mem.inject f m1 m1' ->
      Val.inject_list f vargs vargs' ->
      (forall b b' delta, f b = Some (b', delta) -> delta = 0) ->
      (forall b b1 b2, f b1 = Some (b, 0) -> f b2 = Some (b, 0) -> b1 = b2) ->
      (forall b b' o k p, f b = Some (b', 0) -> (Mem.perm m1 b o k p <-> Mem.perm m1' b' o k p)) ->
      exists (f' : meminj) (vres' : val) (m2' : mem),
        external_call (EF_external name sg) ge2 vargs' m1' t vres' m2' /\
        Val.inject f' vres vres' /\
        Mem.inject f' m2 m2' /\
        Mem.unchanged_on (loc_unmapped f) m1 m2 /\
        Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' /\
        inject_incr f f' /\
        inject_separated f f' m1 m1' /\
        (forall b b' delta, f' b = Some (b', delta) -> delta = 0) /\
        (forall b b1 b2, f' b1 = Some (b, 0) -> f' b2 = Some (b, 0) -> b1 = b2) /\
        (forall b b' o k p, f' b = Some (b', 0) -> (Mem.perm m2 b o k p <-> Mem.perm m2' b' o k p)).

  Axiom inline_asm_mem_inject_gen':
    forall txt sg clb (ge1 ge2 : Senv.t)
      (vargs : list val) (m1 : mem) (t : trace)
      (vres : val) (m2 : mem) (f : block -> option (block * Z))
      (m1' : mem) (vargs' : list val),
      symbols_inject f ge1 ge2 ->
      external_call (EF_inline_asm txt sg clb) ge1 vargs m1 t vres m2 ->
      Mem.inject f m1 m1' ->
      Val.inject_list f vargs vargs' ->
      (forall b b' delta, f b = Some (b', delta) -> delta = 0) ->
      (forall b b1 b2, f b1 = Some (b, 0) -> f b2 = Some (b, 0) -> b1 = b2) ->
      (forall b b' o k p, f b = Some (b', 0) -> (Mem.perm m1 b o k p <-> Mem.perm m1' b' o k p)) ->
      exists (f' : meminj) (vres' : val) (m2' : mem),
        external_call (EF_inline_asm txt sg clb) ge2 vargs' m1' t vres' m2' /\
        Val.inject f' vres vres' /\
        Mem.inject f' m2 m2' /\
        Mem.unchanged_on (loc_unmapped f) m1 m2 /\
        Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' /\
        inject_incr f f' /\
        inject_separated f f' m1 m1' /\
        (forall b b' delta, f' b = Some (b', delta) -> delta = 0) /\
        (forall b b1 b2, f' b1 = Some (b, 0) -> f' b2 = Some (b, 0) -> b1 = b2) /\
        (forall b b' o k p, f' b = Some (b', 0) -> (Mem.perm m2 b o k p <-> Mem.perm m2' b' o k p)).

  Lemma external_call_mem_inject_gen':
    forall (ef : external_function) (ge1 ge2 : Senv.t)
      (vargs : list val) (m1 : mem) (t : trace)
      (vres : val) (m2 : mem) (f : block -> option (block * Z))
      (m1' : mem) (vargs' : list val),
      symbols_inject f ge1 ge2 ->
      external_call ef ge1 vargs m1 t vres m2 ->
      Mem.inject f m1 m1' ->
      Val.inject_list f vargs vargs' ->
      (forall b b' delta, f b = Some (b', delta) -> delta = 0) ->
      (forall b b1 b2, f b1 = Some (b, 0) -> f b2 = Some (b, 0) -> b1 = b2) ->
      (forall b b' o k p, f b = Some (b', 0) -> (Mem.perm m1 b o k p <-> Mem.perm m1' b' o k p)) ->
      exists (f' : meminj) (vres' : val) (m2' : mem),
        external_call ef ge2 vargs' m1' t vres' m2' /\
        Val.inject f' vres vres' /\
        Mem.inject f' m2 m2' /\
        Mem.unchanged_on (loc_unmapped f) m1 m2 /\
        Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' /\
        inject_incr f f' /\
        inject_separated f f' m1 m1' /\
        (forall b b' delta, f' b = Some (b', delta) -> delta = 0) /\
        (forall b b1 b2, f' b1 = Some (b, 0) -> f' b2 = Some (b, 0) -> b1 = b2) /\
        (forall b b' o k p, f' b = Some (b', 0) -> (Mem.perm m2 b o k p <-> Mem.perm m2' b' o k p)).
Proof.
    intros; destruct ef; simpl in H0.
    - eapply external_functions_mem_inject_gen'; eauto.
    - eapply external_functions_mem_inject_gen'; eauto.
    - inv H0; inv H2. inv H8. exploit volatile_load_inject; eauto.
      intros [v' [A B]]. exists f. exists v'. exists m1'. intuition.
      + simpl. inv H10. constructor. auto.
      + red; intros. congruence.
    - inv H0. inv H2. inv H10. inv H11. inv H6.
      + inv H8. inv H. destruct H8 as [Q [R S]].
        exploit Q; eauto. intros [A B]. subst delta.
        rewrite Int.add_zero. exists f. exists Vundef. exists m1'. split.
        constructor; auto. constructor; auto.
        erewrite S; eauto.
        eapply eventval_match_inject; eauto. econstructor; eauto.
        apply Val.load_result_inject; auto.
        intuition auto with mem. congruence.
      + exists f. exists Vundef. inv H8. inv H; destruct H8 as [Q [R S]].
        assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2) by (simpl; eauto).
        exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]].
        exists m2'; intuition auto.
        * econstructor. econstructor; auto. erewrite S; eauto.
        * eapply Mem.store_unchanged_on; eauto.
          unfold loc_unmapped; intros. congruence.
        * eapply Mem.store_unchanged_on; eauto.
          unfold loc_out_of_reach; intros. red; intros. simpl in A.
          assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta)
            by (eapply Mem.address_inject; eauto with mem).
          rewrite EQ in *.
          eelim H9; eauto.
          exploit Mem.store_valid_access_3. eexact H2. intros [X Y].
          apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
          apply X. Psatz.lia.
        * congruence.
        * eapply Mem.perm_store_1; eauto.
          eapply H5; eauto. eapply Mem.perm_store_2; eauto.
        * eapply Mem.perm_store_1; eauto.
          eapply H5; eauto. eapply Mem.perm_store_2; eauto.
    - assert (UNCHANGED:
                forall (P: block -> Z -> Prop) m n m' b m'',
                  Mem.alloc m (-4) (Int.unsigned n) = (m', b) ->
                  Mem.store Mint32 m' b (-4) (Vint n) = Some m'' ->
                  Mem.unchanged_on P m m'').
      {
        intros; constructor; intros.
        - split; intros; eauto with mem.
        - assert (b0 <> b) by (eapply Mem.valid_not_valid_diff; eauto with mem).
          erewrite Mem.store_mem_contents; eauto. rewrite Maps.PMap.gso by auto.
          Local Transparent Mem.alloc. unfold Mem.alloc in H6. injection H6; intros A B.
          rewrite <- B; simpl. rewrite A. rewrite Maps.PMap.gso by auto. auto.
      }
      inv H0. inv H2. inv H9. inv H11.
      exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl.
      intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]].
      exploit Mem.store_mapped_inject. eexact A. eauto. eauto.
      instantiate (1 := Vint n). auto.
      intros [m2' [E G]].
      exists f'; exists (Vptr b' Int.zero); exists m2'; intuition.
      + econstructor; eauto.
      + econstructor. eauto. auto.
      + eapply UNCHANGED; eauto.
      + eapply UNCHANGED; eauto.
      + red; intros. destruct (eq_block b1 b).
        * subst b1. rewrite C in H2. inv H2. eauto with mem.
        * rewrite D in H2 by auto. congruence.
      + destruct (eq_block b0 b).
        * subst b0. rewrite C in H0; inv H0. auto.
        * rewrite D in H0; eauto.
      + destruct (peq b1 b).
        * destruct (peq b2 b).
          { subst b1; subst b2; eauto. }
          { subst b1. generalize (Mem.alloc_result _ _ _ _ _ H6).
            intros; subst b. rewrite C in H0; inv H0.
            generalize (Mem.alloc_result _ _ _ _ _ ALLOC). intros; subst b0.
            inv H1. rewrite D in H2; auto. eapply mi_mappedblocks in H2. unfold Mem.valid_block in H2. xomega. }
        * destruct (peq b2 b).
          { subst b2. generalize (Mem.alloc_result _ _ _ _ _ H6).
            intros; subst b. inv H1. rewrite C in H2; inv H2.
            generalize (Mem.alloc_result _ _ _ _ _ ALLOC). intros; subst b0.
            rewrite D in H0; auto. eapply mi_mappedblocks in H0. unfold Mem.valid_block in H0. xomega. }
          { rewrite D in H0; rewrite D in H2; eauto. }
      + eapply Mem.perm_store_1; eauto. generalize (Mem.perm_store_2 _ _ _ _ _ _ H7 _ _ _ _ H2). intros.
        destruct (peq b0 b).
        * subst b0. rewrite H0 in C; inv C. eapply Mem.perm_alloc_inv in H8; eauto.
          destruct (eq_block b b); try congruence. clear e.
          eapply Mem.perm_implies. eapply Mem.perm_alloc_2; eauto. constructor.
        * rewrite D in H0; eauto.
          eapply Mem.perm_alloc_1; eauto. eapply H5; eauto.
          eapply Mem.perm_alloc_4; eauto.
      + eapply Mem.perm_store_1; eauto. generalize (Mem.perm_store_2 _ _ _ _ _ _ E _ _ _ _ H2). intros.
        destruct (peq b0 b).
        * subst b0. rewrite H0 in C. inv C. eapply Mem.perm_alloc_inv in H8; eauto.
          destruct (eq_block b' b'); try congruence; clear e.
          eapply Mem.perm_implies. eapply Mem.perm_alloc_2; eauto. constructor.
        * rewrite D in H0; eauto.
          eapply Mem.perm_alloc_1; eauto. eapply H5; eauto.
          eapply Mem.perm_alloc_4; eauto. unfold not; intros.
          subst b'0. inv H1. eapply mi_mappedblocks in H0.
          exploit Mem.alloc_result; eauto. intros; subst b'. unfold Mem.valid_block in H0. xomega.
    - inv H0. inv H2. inv H10. inv H12.
      exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B.
      assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable).
      eapply Mem.free_range_perm; eauto.
      exploit Mem.address_inject; eauto.
      apply Mem.perm_implies with Freeable; auto with mem.
      apply H0. instantiate (1 := lo). Psatz.lia.
      intro EQ.
      exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D).
      exists f, Vundef, m2'; split.
      apply extcall_free_sem_intro with (sz := sz) (m' := m2').
      rewrite EQ. rewrite <- A. f_equal. Psatz.lia.
      auto.
      rewrite ! EQ. rewrite <- C. f_equal; Psatz.lia.
      split. auto.
      split. auto.
      split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence.
      split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach.
      intros. red; intros. eelim H10; eauto.
      apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem.
      apply H0. Psatz.lia.
      split. auto.
      split. red; intros. congruence.
      repeat split; try eauto.
      + intros. generalize (Mem.perm_free_3 _ _ _ _ _ H8 _ _ _ _ H10). intros.
        eapply Mem.perm_free_1; eauto.
        * destruct (peq b' b2); eauto. right.
          destruct (zlt o (Int.unsigned lo - 4 + delta)); auto.
          right. destruct (zle (Int.unsigned lo + Int.unsigned sz + delta) o); auto.
          exfalso. eapply Mem.perm_free_2. eapply H8. instantiate (1 := o).
          eapply H3 in H9. subst delta. Psatz.lia.
          subst b2. generalize (H3 _ _ _ H9); intros; subst delta. generalize (H4 _ _ _ H2 H9).
          intros; subst b0. eauto.
        * eapply H5; eauto.
      + intros. generalize (Mem.perm_free_3 _ _ _ _ _ C _ _ _ _ H10). intros.
        eapply Mem.perm_free_1; eauto.
        * destruct (peq b0 b); eauto.
          subst b0; right. destruct (zlt o (Int.unsigned lo - 4)); auto.
          right. destruct (zle (Int.unsigned lo + Int.unsigned sz) o); auto.
          exfalso. eapply Mem.perm_free_2. eapply C. instantiate (1 := o).
          eapply H3 in H9. subst delta. Psatz.lia.
          rewrite H2 in H9; inv H9. eauto.
        * eapply H5; eauto.
    - inv H0. inv H2. inv H15. inv H17. inv H15. inv H18.
      destruct (zeq sz 0).
      + (* special case sz = 0 *)
        assert (bytes = nil).
        { exploit (Mem.loadbytes_empty m1 bsrc (Int.unsigned osrc) sz). omega. congruence. }
        subst.
        destruct (Mem.range_perm_storebytes m1' b2 (Int.unsigned (Int.add odst (Int.repr delta))) nil)
          as [m2' SB].
        simpl. red; intros; omegaContradiction.
        exists f, Vundef, m2'.
        split. econstructor; eauto.
        intros; omegaContradiction.
        intros; omegaContradiction.
        right; omega.
        apply Mem.loadbytes_empty. omega.
        split. auto.
        split. eapply Mem.storebytes_empty_inject; eauto.
        split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros.
        congruence.
        split. eapply Mem.storebytes_unchanged_on; eauto.
        simpl; intros; omegaContradiction.
        split. apply inject_incr_refl.
        split. red; intros; congruence.
        repeat split; auto.
        * intros. eapply Mem.perm_storebytes_1; eauto.
          eapply H5; eauto. eapply Mem.perm_storebytes_2; eauto.
        * intros. eapply Mem.perm_storebytes_1; eauto.
          eapply H5; eauto. eapply Mem.perm_storebytes_2; eauto.
      + (* general case sz > 0 *)
        exploit Mem.loadbytes_length; eauto. intros LEN.
        assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Cur Nonempty).
        eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
        assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Cur Nonempty).
        replace sz with (Z_of_nat (length bytes)).
        eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
        rewrite LEN. apply nat_of_Z_eq. omega.
        assert (PSRC: Mem.perm m1 bsrc (Int.unsigned osrc) Cur Nonempty).
        apply RPSRC. omega.
        assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Cur Nonempty).
        apply RPDST. omega.
        exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1.
        exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2.
        exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]].
        exploit Mem.storebytes_mapped_inject; eauto. intros [m2' [C D]].
        exists f; exists Vundef; exists m2'.
        split. econstructor; try rewrite EQ1; try rewrite EQ2; eauto.
        intros; eapply Mem.aligned_area_inject with (m := m1); eauto.
        intros; eapply Mem.aligned_area_inject with (m := m1); eauto.
        eapply Mem.disjoint_or_equal_inject with (m := m1); eauto.
        apply Mem.range_perm_max with Cur; auto.
        apply Mem.range_perm_max with Cur; auto. omega.
        split. constructor.
        split. auto.
        split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros.
        congruence.
        split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros.
        eelim H2; eauto.
        apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem.
        eapply Mem.storebytes_range_perm; eauto.
        erewrite list_forall2_length; eauto.
        Psatz.lia.
        split. apply inject_incr_refl.
        split. red; intros; congruence.
        repeat split; auto.
        * intros. eapply Mem.perm_storebytes_1; eauto.
          eapply H5; eauto. eapply Mem.perm_storebytes_2; eauto.
        * intros. eapply Mem.perm_storebytes_1; eauto.
          eapply H5; eauto. eapply Mem.perm_storebytes_2; eauto.
    - inv H0.
      exists f; exists Vundef; exists m1'; intuition.
      econstructor; eauto.
      eapply eventval_list_match_inject; eauto.
      red; intros; congruence.
    - inv H0. inv H2. inv H10.
      exists f; exists v'; exists m1'; intuition.
      econstructor; eauto.
      eapply eventval_match_inject; eauto.
      red; intros; congruence.
    - eapply inline_asm_mem_inject_gen'; eauto.
    - inv H0.
      exists f; exists Vundef; exists m1'; intuition.
      econstructor; eauto.
      red; intros; congruence.
  Qed.
Generated by coq2html