Module OnMem


Require Import Utf8 Coqlib Util Maps.
Require Import AST Values Integers Memory Globalenvs Cminor Csharpminor.

Set Implicit Arguments.
Local Unset Elimination Schemes.

Lemma eval_expr_unop_ptr (ge: genv) e tmp m u q b i:
  ¬ eval_expr ge e tmp m (Eunop u q) (Vptr b i).
Proof.
  intros H.
  remember (Eunop u q) as U eqn: EQ. revert u q EQ.
  remember (Vptr b i) as v eqn: Hv. revert b i Hv.
  induction H; try congruence.
  intros b i -> u q K. inv K.
  destruct u; destruct v1; simpl in *; try congruence;
  match goal with H : context[option_map _ ?m] |- _ => destruct m; simpl in H end; congruence.
Qed.

Lemma eval_expr_binop_ptr (ge: genv) e tmp m o q1 q2 b i:
  eval_expr ge e tmp m (Ebinop o q1 q2) (Vptr b i) →
  (o = Oadd ∧ ∃ v1 v2, eval_expr ge e tmp m q1 v1 ∧ eval_expr ge e tmp m q2 v2 ∧ Val.add v1 v2 = Vptr b i)
  ∨
  (o = Osub ∧ ∃ v1 v2, eval_expr ge e tmp m q1 v1 ∧ eval_expr ge e tmp m q2 v2 ∧ Val.sub v1 v2 = Vptr b i).
Proof.
  intros H. inv H. revert H6. destruct o; simpl in *;
  try (destruct v1; destruct v2; simpl in *; try bif; discriminate);
  intro; eq_some_inv;
  try (
      unfold Val.cmp in *; unfold Val.cmpu in *;
      unfold Val.cmpf in *; unfold Val.cmpfs in *;
      unfold Val.cmpl in *; unfold Val.cmplu in *;
      match goal with
      | H : appcontext[Val.of_optbool ?b] |- _ => destruct b as [()|]; simpl in H; discriminate
      | H : appcontext[option_map ?f ?b] |- _ => destruct b as [()|]; simpl in H;
                                             eq_some_inv; discriminate
      end
    );
  intuition eauto.
Qed.

Lemma eval_expr_binop_ptr' (ge:genv) e tmp m o q1 q2 b i:
  eval_expr ge e tmp m (Ebinop o q1 q2) (Vptr b i) →
  ∃ j,
    (eval_expr ge e tmp m q1 (Vptr b j)
     ∨
     eval_expr ge e tmp m q2 (Vptr b j)).
Proof.
  intros H.
  destruct (eval_expr_binop_ptr H) as
      [(-> & v1 & v2 & H1 & H2 & K)
      |(-> & v1 & v2 & H1 & H2 & K)];
  destruct v1; simpl in K; try discriminate;
  destruct v2; simpl in K; inv K;
  intuition eauto.
  destruct eq_block; discriminate.
Qed.

Lemma inj_one_byte i :
  inj_bytes (encode_int 1 i) = Byte (Byte.repr i) :: nil.
Proof.
  unfold encode_int, rev_if_be.
  destruct (Archi.big_endian); reflexivity.
Qed.

Lemma inj_two_bytes i :
  ∃ a b,
  inj_bytes (encode_int 2 i) = Byte a :: Byte b :: nil.
Proof.
  unfold encode_int, rev_if_be.
  destruct (Archi.big_endian); eexists _, _; reflexivity.
Qed.

Lemma inj_four_bytes i :
  ∃ a b c d,
  inj_bytes (encode_int 4 i) = Byte a :: Byte b :: Byte c :: Byte d :: nil.
Proof.
  unfold encode_int, rev_if_be.
  destruct (Archi.big_endian); eexists _, _, _, _; reflexivity.
Qed.

Lemma inj_eight_bytes i :
  ∃ a b c d e f g h,
  inj_bytes (encode_int 8 i) = Byte a :: Byte b :: Byte c :: Byte d :: Byte e :: Byte f :: Byte g :: Byte h :: nil.
Proof.
  unfold encode_int, rev_if_be.
  destruct (Archi.big_endian); eexists _, _, _, _, _, _, _, _; reflexivity.
Qed.

Lemma alloc_globals_no_int_fragment F V (ge: Genv.t F V) m defs m' :
  Genv.alloc_globals ge m defs = Some m' →
  (∀ b o, match ZMap.get o (Mem.mem_contents m) !! b with Fragment (Vint _) _ _ => False | _ => True end) →
  (∀ b o, match ZMap.get o (Mem.mem_contents m') !! b with Fragment (Vint _) _ _ => False | _ => True end).
Proof.
  revert m m'.
  induction defs as [ | (? & [? | v]) defs IH ]; simpl.
  - intros m m' H; eq_some_inv; subst m'; exact id.
  - intros m m'.
    destruct (Mem.alloc _ _ _) as (m₁, b) eqn: Hm₁.
    destruct (Mem.drop_perm _ _ _ _ _) as [? | ] eqn: Hdp; intros H; eq_some_inv.
    intros X. apply (IH _ _ H). clear IH H.
    unfold Mem.drop_perm in Hdp.
    destruct Mem.range_perm_dec; eq_some_inv. subst.
    Transparent Mem.alloc. unfold Mem.alloc in Hm₁. Opaque Mem.alloc.
    eq_some_inv. subst. simpl in *.
    intros b o. rewrite PMap.gsspec. case peq.
    intros ->. rewrite ZMap.gi. exact I. intros _. apply X.
  - intros m m'.
    destruct (Mem.alloc _ _ _) as (m₁, b) eqn: Hm₁.
    destruct (store_zeros _ _ _ _) as [m₂|] eqn: Hm₂. 2: intros; eq_some_inv.
    destruct (Genv.store_init_data_list _ _ _ _ _) as [m₃|] eqn: Hm₃. 2: intros; eq_some_inv.
    destruct (Mem.drop_perm _ _ _ _ _) as [? | ] eqn: Hdp; intros H; eq_some_inv.
    intros X. apply (IH _ _ H). clear IH H.
    unfold Mem.drop_perm in Hdp.
    destruct Mem.range_perm_dec; eq_some_inv. subst. simpl.
    intros b' o. specialize (X b' o).
    assert (match ZMap.get o (Mem.mem_contents m₁) !! b' with Fragment (Vint _) _ _ => False | _ => True end) as Y.
    {
      Transparent Mem.alloc. unfold Mem.alloc in Hm₁. Opaque Mem.alloc.
      eq_some_inv. subst. simpl in *.
      rewrite PMap.gsspec. case peq.
      intros ->. rewrite ZMap.gi. exact I. intros _. apply X.
    }
    clear X Hm₁.
    assert (match ZMap.get o (Mem.mem_contents m₂) !! b' with Fragment (Vint _) _ _ => False | _ => True end) as X.
    {
      revert Hm₂. clear -Y.
      generalize (Genv.init_data_list_size (gvar_init v)).
      intros sz.
      revert m₂.
      functional induction (store_zeros m₁ b 0 sz);
        intros m₂ Hm₂; eq_some_inv.
      subst m. exact Y.
      apply IHo0; auto; clear IHo0 Hm₂ m₂.
      Transparent Mem.store. unfold Mem.store in *. Opaque Mem.store.
      destruct Mem.valid_access_dec; eq_some_inv; subst. simpl.
      rewrite PMap.gsspec. case peq; auto.
      intros ->.
      change (inj_bytes (encode_int 1 (Int.unsigned Int.zero))) with (Byte Byte.zero :: nil).
      simpl. rewrite ZMap.gsspec.
      case ZIndexed.eq; auto.
    } clear Y Hm₂.
    revert Hm₃. clear -X.
    generalize (gvar_init v), 0. intros idl.
    revert m₂ X.
    induction idl as [| idx idl IH ].
    simpl; intros; eq_some_inv; subst; exact X.
    simpl.
    intros m₂ X sz Hm₃.
    destruct (Genv.store_init_data _ _ _ _ _) as [m' | ] eqn: Hm'.
    2: eq_some_inv.
    refine (IH m' _ _ Hm₃). clear Hm₃.
    unfold Genv.store_init_data in Hm'.
    Transparent Mem.store. unfold Mem.store in *. Opaque Mem.store.
    destruct idx; eq_some_inv; subst; auto;
      try (destruct Genv.find_symbol; eq_some_inv; subst; auto);
      try (destruct Mem.valid_access_dec; eq_some_inv; subst; simpl);
      try (rewrite PMap.gsspec; case peq; auto; intros -> );
      try (
    match goal with
    | |- appcontext[ encode_int 1 ?x ] => rewrite inj_one_byte
    | |- appcontext[ encode_int 2 ?x ] =>
      let H := fresh in
      destruct (inj_two_bytes x) as (? & ? & H);
      rewrite H
    | |- appcontext[ encode_int 4 ?x ] =>
      let H := fresh in
      destruct (inj_four_bytes x) as (? & ? & ? & ? & H);
      rewrite H
    | |- appcontext[ encode_int 8 ?x ] =>
      let H := fresh in
      destruct (inj_eight_bytes x) as (? & ? & ? & ? & ? & ? & ? & ? & H);
      rewrite H
    end); simpl; rewrite ! ZMap.gsspec; repeat (case ZIndexed.eq; auto).
Qed.

Lemma init_mem_no_int_fragment F V (prog: AST.program F V) m :
  Genv.init_mem prog = Some m →
  (∀ b o, match ZMap.get o (Mem.mem_contents m) !! b with Fragment (Vint _) _ _ => False | _ => True end).
Proof.
  unfold Genv.init_mem.
  intros H. apply (alloc_globals_no_int_fragment _ _ _ H).
  intros b o. simpl. rewrite PMap.gi, ZMap.gi. exact I.
Qed.

Lemma create_undef_temps_get l x :
  match (create_undef_temps l) ! x with
  | Some v => v = Vundef ∧ In x l
  | None => ¬ In x l
  end.
Proof.
  induction l as [|y l IH]; simpl.
  rewrite PTree.gempty. exact id.
  rewrite PTree.gsspec. destruct peq. intuition.
  destruct ((create_undef_temps l) ! x). intuition.
  intuition.
Qed.

Lemma alloc_can_store m sz m' b :
  0 <= sz →
  Mem.alloc m 0 sz = (m', b) →
  ∃ m'', store_zeros m' b 0 sz = Some m''.
Proof.
  intros SZ H.
  pose proof (Mem.valid_access_alloc_same _ _ _ _ _ H Mint8unsigned) as K. clear H.
  assert (∀ o, 0 <= o → o + 1 <= sz → Mem.valid_access m' Mint8unsigned b o Writable) as H.
  intros o H H0. eapply Mem.valid_access_implies. eapply K; eauto. exists o; simpl; ring. vauto.
  clear K.
  cut (∀ p n, 0 <= p → 0 <= n → p + n <= sz → ∃ m'', store_zeros m' b p n = Some m'').
  intros K. apply (K 0 sz); intuition.
  revert m' H. clear.
  intros m' H p n.
  functional induction (store_zeros m' b p n). vauto.
  intros H0 H1 H2. eapply IHo; auto. intros o H3 H4.
  eapply Mem.store_valid_access_1; eauto. intuition. intuition. auto with zarith.
  intros H0 H1 H2. exfalso.
  edestruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & M).
  apply H; auto. intuition.
  congruence.
Qed.

Lemma init_data_list_size_pos init :
  0 <= Genv.init_data_list_size init.
Proof.
  induction init as [|i init IH]. reflexivity.
  simpl. generalize (Genv.init_data_size_pos i). intuition.
Qed.

Lemma alloc_can_drop m lo hi m' b p :
  Mem.alloc m lo hi = (m', b) →
  ∃ m'', Mem.drop_perm m' b lo hi p = Some m''.
Proof.
  intros A.
  edestruct (Mem.range_perm_drop_2 m' b lo hi p). 2: vauto.
  intros o Ho. eapply Mem.perm_alloc_2; eauto.
Qed.

Lemma misaligned_load κ ofs :
  ¬ (align_chunk κ | ofs) →
  ∀ m b,
    Mem.load κ m b ofs = None.
Proof.
  intros H m b.
  generalize (Mem.load_valid_access m κ b ofs).
  destruct Mem.load. 2: exact (λ _, eq_refl).
  intros X. specialize (X _ eq_refl). destruct X as [_ X].
  exfalso. exact (H X).
Qed.
Arguments misaligned_load [κ][ofs] _ _ _.

Lemma not_valid_block_load_None m b :
  ¬ Mem.valid_block m b →
  ∀ κ ofs, Mem.load κ m b ofs = None.
Proof.
  intros H κ ofs.
  generalize (Mem.load_valid_access m κ b ofs).
  destruct (Mem.load κ m b ofs); auto.
  intros X. specialize (X _ eq_refl).
  elim H. eapply Mem.valid_access_valid_block.
  eapply Mem.valid_access_implies. eassumption. vauto.
Qed.

Lemma nth_def_block {F V} (ge: Genv.t F V) :
  ∀ prog, ge = Genv.globalenv prog ->
          list_norepet (map fst prog.(prog_defs)) ->
  ∀ idx id gd,
    nth idx (List.map Some prog.(prog_defs)) None = Some (id, gd) ->
    match gd with
    | Gfun gf => Genv.find_funct_ptr ge (Pos.of_succ_nat idx) = Some gf
    | Gvar gv => Genv.find_var_info ge (Pos.of_succ_nat idx) = Some gv
    end /\
    Genv.find_symbol ge id = Some (Pos.of_succ_nat idx).
Proof.
  unfold Genv.globalenv. intros*.
  unfold Genv.find_funct_ptr.
  generalize ge.
  induction (prog_defs prog) using rev_ind.
  - destruct idx; discriminate.
  - intros. subst.
    rewrite Genv.add_globals_app. simpl.
    rewrite map_app in H0, H1. rewrite list_norepet_app in H0.
    destruct H0 as (? & _ & ?). simpl in H0.
    assert (~ In (fst x) (map fst l)).
    { intro. eapply H0; simpl; eauto. }
    clear H0.
    unfold Genv.add_global, Genv.find_var_info, Genv.find_symbol in *. simpl.
    assert (Pos.of_succ_nat (Datatypes.length l) =
            Genv.genv_next (Genv.add_globals (Genv.empty_genv F V (prog_public prog)) l)).
    { clear IHl H H1 H2.
      induction l using rev_ind. reflexivity.
      rewrite app_length, Genv.add_globals_app. simpl. rewrite <- IHl.
      rewrite !Pos.of_nat_succ, Pos.succ_of_nat, Pos.of_nat_succ by discriminate.
      f_equal. Psatz.lia. }
    destruct (le_lt_dec (length (map Some l)) idx).
    + rewrite app_nth2 in H1 by auto.
      destruct (idx - Datatypes.length (map Some l))%nat as [|[]] eqn:EQ; inv H1.
      replace idx with (Datatypes.length (map Some l)) in * by Psatz.lia.
      rewrite list_length_map.
      split; destruct gd; simpl; rewrite H0, PTree.gss; auto.
    + rewrite app_nth1 in H1 by auto.
      edestruct IHl; eauto.
      split.
      * destruct x as [? []]; simpl; destruct gd; auto; rewrite PTree.gso; auto;
        rewrite <- H0; intro; apply SuccNat2Pos.inj in H5;
        rewrite map_length in l0; Psatz.lia.
      * rewrite PTree.gso. auto.
        intro. subst.
        edestruct list_in_map_inv as (? & ? & ?). eapply nth_In with (d:=None). eauto.
        rewrite H1 in H5. inv H5.
        apply in_map with (f:=fst), H2 in H6. auto.
Qed.

Lemma free_list_contents {m blocks m'}:
  Mem.free_list m blocks = Some m' ->
  Mem.mem_contents m = Mem.mem_contents m'.
Proof.
  revert m.
  induction blocks as [ | ((? & ?) & ?) blocks IH ]. simpl; intros m H; eq_some_inv; apply (f_equal _ H).
  simpl. intros m.
  Transparent Mem.free. unfold Mem.free. Opaque Mem.free.
  destruct Mem.range_perm_dec. 2: intro; eq_some_inv.
  intros H. rewrite <- (IH _ H).
  reflexivity.
Qed.

Section ON_VOL.

  Local Coercion is_true : bool >-> Sortclass.
  Lemma genv_volatile_are_global (p: program) :
    list_norepet (map fst (AST.prog_defs p)) →
    ∀ b, Senv.block_is_volatile (Genv.globalenv p) b → ∃ g, Genv.invert_symbol (Genv.globalenv p) b = Some g.
Proof.
    simpl.
    intros H b H0. cut (∃ g, Genv.find_symbol (Genv.globalenv p) g = Some b ∧ In g (map fst (AST.prog_defs p))).
    intros (g & G). exists g. apply Genv.find_invert_symbol, G.
    revert H H0.
    unfold Genv.globalenv, Genv.block_is_volatile, Genv.find_var_info, AST.prog_defs_names.
    intros NR H. destruct (Maps.PTree.get b _) eqn: H1. 2: exact (Util.false_not_true H _).
    revert NR b g H1 H.
    generalize (prog_defs p). intros defs NR.
    induction defs as [ | (x, d) defs IH ] using rev_ind; intros b gv Hgv vol.
    - simpl in Hgv. rewrite Maps.PTree.gempty in Hgv. Util.eq_some_inv.
    - rewrite Genv.add_globals_app. simpl. rewrite map_app in NR.
      rewrite Genv.add_globals_app in Hgv. simpl in *.
      specialize (IH (list_norepet_append_left _ _ NR)).
      destruct d.
      + specialize (IH b gv Hgv vol).
      destruct IH as (g & IH & IN).
      exists g.
      unfold Genv.find_symbol. simpl. rewrite Maps.PTree.gso. simpl. split. exact IH.
      rewrite map_app. apply in_app; auto.
      clear -NR IN.
      intros ->.
      apply list_norepet_app in NR. destruct NR as [ _ [ _ D]]. refine (D x x IN (or_introl eq_refl) eq_refl).
      + rewrite Maps.PTree.gsspec in Hgv. destruct (peq _ _).
         * Util.eq_some_inv. subst. eexists. split. unfold Genv.find_symbol. simpl. apply Maps.PTree.gss.
            rewrite map_app. apply in_app. right. left. reflexivity.
         * specialize (IH _ _ Hgv vol).
      destruct IH as (g & IH & IN).
      exists g.
      unfold Genv.find_symbol. simpl. rewrite Maps.PTree.gso. simpl. split. exact IH.
      rewrite map_app. apply in_app; auto.
      clear -NR IN.
      intros ->.
      apply list_norepet_app in NR. destruct NR as [ _ [ _ D]]. refine (D x x IN (or_introl eq_refl) eq_refl).
  Qed.

End ON_VOL.
Generated by coq2html