Module CompCertLib

From Velus Require Import Common.

From compcert Require Import lib.Coqlib.
From compcert Require Import lib.Maps.
From compcert Require Import cfrontend.Clight.
From compcert Require Import cfrontend.Ctypes.
From compcert Require Import lib.Integers.
From compcert Require Import common.Values.
From compcert Require Import common.Errors.
From compcert Require Import common.Memory.

From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

From Coq Require Import Classes.RelationClasses.

Open Scope error_monad_scope.



Lemma NoDup_norepet:
  forall {A} (l: list A),
    NoDup l <-> list_norepet l.

Lemma NoDupMembers_disjoint:
  forall l1 l2,
    NoDupMembers (l1 ++ l2) ->
    list_disjoint (var_names l1) (var_names l2).

Lemma list_drop_skipn:
  forall {A} (xs: list A) n,
    Coqlib.list_drop n xs = skipn n xs.

Lemma list_forall2_Forall2:
  forall {A B} P (xs: list A) (ys: list B),
    Coqlib.list_forall2 P xs ys <-> Forall2 P xs ys.


Section Mmaps.

  Context {A B S: Type}.

  Definition mmaps (f: S -> A -> res (S * B)) : S -> list A -> res (S * list B) :=
    fix mmaps (s: S) (xs: list A) {struct xs} : res (S * list B) :=
      match xs with
      | nil => OK (s, nil)
      | x :: xs' => do (s', y) <- f s x;
                    do (s'', ys) <- mmaps s' xs';
                    OK (s'', y :: ys)
      end.

  Lemma mmaps_spec:
    forall (P: S -> S -> B -> Prop) (R: S -> S -> Prop)
           (I: list B -> Prop) (IS: S -> Prop)
           (f: S -> A -> res (S * B)) xs ys s s',
      mmaps f s xs = OK (s', ys) ->
      Reflexive R ->
      Transitive R ->
      I [] ->
      IS s ->
      (forall s s' y, P s s' y ->
                         (forall r, R r s -> P r s' y)
                      /\ (forall t', R s' t' -> P s t' y)) ->
      (forall x y s s',
          In x xs ->
          IS s ->
          f s x = OK (s', y) ->
          P s s' y /\ R s s' /\ IS s') ->
      (forall y ys s s' s'',
          P s s' y ->
          Forall (P s' s'') ys ->
          R s s' ->
          R s' s'' ->
          I ys ->
          I (y :: ys)) ->
      Forall (P s s') ys /\ R s s' /\ I ys /\ IS s'.

  Lemma mmaps_weak_spec:
    forall (I: S -> Prop) (R: B -> Prop)
           (f: S -> A -> res (S * B)) xs s ys s',
      mmaps f s xs = OK (s', ys) ->
      I s ->
      (forall x s y s',
          I s ->
          In x xs ->
          f s x = OK (s', y) ->
          I s' /\ R y) ->
      I s' /\ Forall R ys.

  Lemma mmaps_weak_spec':
  forall (R: B -> Prop)
         (f: S -> A -> res (S * B)) xs s ys s',
    mmaps f s xs = OK (s', ys) ->
    (forall x s y s',
        In x xs ->
        f s x = OK (s', y) ->
        R y) ->
    Forall R ys.

End Mmaps.

Definition mfoldl {A B: Type} (f: A -> B -> res A) : A -> list B -> res A :=
  fix mfoldl s xs {struct xs} :=
    match xs with
    | nil => OK s
    | x :: xs' => do s' <- f s x;
                    mfoldl s' xs'
    end.

Lemma OK_OK:
  forall {A} (x: A) y,
    OK x = OK y <-> x = y.

Definition mmapacc {A S T: Type} (acc: S -> T -> S) (f: A -> res T)
  : S -> list A -> res S :=
  fix mmapacc (s: S) (xs: list A) {struct xs} : res S :=
    match xs with
    | nil => OK s
    | x :: xs' => do r <- f x;
                    mmapacc (acc s r) xs'
    end.

Lemma mmap_skipn:
  forall {A B} (f: A -> res B) xs ys n,
    mmap f xs = OK ys ->
    mmap f (skipn n xs) = OK (skipn n ys).

Open Scope nat.

Lemma mmapacc_plus_shift:
  forall {A} f (xs: list A) m1 m2 n,
    mmapacc plus f (m1 + m2) xs = OK n ->
    mmapacc plus f m1 xs = OK (n - m2) /\ m2 <= n.


Definition bind22 {A B C D: Type} (f: res (A * (B * C))) (g: A -> B -> C -> res D) : res D :=
  match f with
  | OK (x, (y, z)) => g x y z
  | Error msg => Error msg
  end.

Module DoNotation.

  Notation "'do' ( X , ( Y , Z ) ) <- A ; B" :=
    (bind22 A (fun X Y Z => B))
      (at level 200, X ident, Y ident, Z ident, A at level 100, B at level 200)
    : error_monad_scope.

End DoNotation.

Remark bind22_inversion:
  forall {A B C D: Type} (f: res (A*(B*C))) (g: A -> B -> C -> res D) {z: D},
    bind22 f g = OK z ->
    exists w, exists x, exists y, f = OK (w, (x, y)) /\ g w x y = OK z.

Ltac monadInv2 H :=
  match type of H with
  | (OK _ = OK _) =>
    inversion H; clear H; try subst
  | (Error _ = OK _) =>
    discriminate
  | (bind ?F ?G = OK ?X) =>
    let x := fresh "x" in (
      let EQ1 := fresh "EQ" in (
        let EQ2 := fresh "EQ" in (
          destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
          clear H;
          try (monadInv2 EQ2))))
  | (bind2 ?F ?G = OK ?X) =>
    let x1 := fresh "x" in (
      let x2 := fresh "x" in (
        let EQ1 := fresh "EQ" in (
          let EQ2 := fresh "EQ" in (
            destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
            clear H;
            try (monadInv2 EQ2)))))
  | (bind22 ?F ?G = OK ?X) =>
    let x1 := fresh "x" in (
      let x2 := fresh "x" in (
        let x3 := fresh "x" in (
          let EQ1 := fresh "EQ" in (
            let EQ2 := fresh "EQ" in (
              destruct (bind22_inversion F G H) as [x1 [x2 [x3 [EQ1 EQ2]]]];
              clear H;
              try (monadInv2 EQ2))))))
  | (match ?X with left _ => _ | right _ => assertion_failed end = OK _) =>
    destruct X; [try (monadInv2 H) | discriminate]
  | (match (negb ?X) with true => _ | false => assertion_failed end = OK _) =>
    destruct X as [] eqn:?; [discriminate | try (monadInv2 H)]
  | (match ?X with true => _ | false => assertion_failed end = OK _) =>
    destruct X as [] eqn:?; [try (monadInv2 H) | discriminate]
  | (mmap ?F ?L = OK ?M) =>
    generalize (mmap_inversion F L H); intro
  end.

Close Scope nat.
Close Scope error_monad_scope.

Lemma Int_Ptrofs_max_unsigned:
  Int.max_unsigned <= Ptrofs.max_unsigned.

Lemma type_eq_refl:
  forall {A} t (T F: A),
    (if type_eq t t then T else F) = T.

Remark field_offset_rec_in_range':
  forall gcenv flds x ofs pos,
    field_offset_rec gcenv x flds pos = Errors.OK ofs ->
    pos <= ofs.

Corollary field_offset_in_range':
  forall gcenv flds x ofs,
    field_offset gcenv x flds = Errors.OK ofs ->
    0 <= ofs.

Lemma two_power_nat_le_divides:
  forall m n,
    two_power_nat m <= two_power_nat n ->
    (two_power_nat m | two_power_nat n).

Lemma two_power_nat_max:
  forall m n,
    (two_power_nat m | Z.max (two_power_nat m) (two_power_nat n)).

Lemma co_members_alignof:
  forall env co,
    composite_consistent env co ->
    attr_alignas (co_attr co) = None ->
    Forall (fun x => (alignof env (snd x) | co_alignof co)) (co_members co).

Lemma align_noattr:
  forall a, align_attr noattr a = a.

Lemma in_field_type:
  forall xs x ty,
    NoDupMembers xs ->
    In (x, ty) xs ->
    field_type x xs = Errors.OK ty.

Lemma field_offset_type:
  forall ge id flds d,
    field_offset ge id flds = Errors.OK d ->
    exists ty, field_type id flds = Errors.OK ty.

Lemma field_type_skip_app:
  forall x ws xs,
    ~InMembers x ws ->
    field_type x (ws ++ xs) = field_type x xs.

Lemma sizeof_by_value:
  forall ge ty chunk,
    access_mode ty = By_value chunk ->
    sizeof ge ty = Memdata.size_chunk chunk.
Hint Resolve sizeof_by_value.

Lemma set_comm:
  forall {A} x x' (v v': A) m,
    x <> x' ->
    PTree.set x v (PTree.set x' v' m) = PTree.set x' v' (PTree.set x v m).


Remark bind_parameter_temps_comm:
  forall xs vs s ts o to vself vout x t v le le',
    x <> o ->
    x <> s ->
    (bind_parameter_temps ((s, ts) :: (o, to) :: (x, t) :: xs) (vself :: vout :: v :: vs) le = Some le' <->
     bind_parameter_temps ((x, t) :: (s, ts) :: (o, to) :: xs) (v :: vself :: vout :: vs) le = Some le').

Remark bind_parameter_temps_comm_noout:
  forall xs vs s ts vself x t v le le',
    x <> s ->
    (bind_parameter_temps ((s, ts) :: (x, t) :: xs) (vself :: v :: vs) le = Some le' <->
     bind_parameter_temps ((x, t) :: (s, ts) :: xs) (v :: vself :: vs) le = Some le').

Remark bind_parameter_temps_conservation:
  forall xs vs x v le le',
    ~ InMembers x xs ->
    le ! x = v ->
    bind_parameter_temps xs vs le = Some le' ->
    le' ! x = v.

Remark bind_parameter_temps_cons:
  forall xs vs x ty v le le',
    ~ InMembers x xs ->
    bind_parameter_temps xs vs le = Some le' ->
    bind_parameter_temps ((x, ty) :: xs) (v :: vs) le = Some (PTree.set x v le').

Remark bind_parameter_temps_implies_two:
  forall xs vs s ts vself o to vout le le',
    s <> o ->
    ~ InMembers s xs ->
    ~ InMembers o xs ->
    bind_parameter_temps ((s, ts) :: (o, to) :: xs)
                         (vself :: vout :: vs) le = Some le' ->
    le' ! s = Some vself /\ le' ! o = Some vout.

Remark bind_parameter_temps_implies:
  forall xs vs s ts vself le le',
    ~ InMembers s xs ->
    bind_parameter_temps ((s, ts) :: xs)
                         (vself :: vs) le = Some le' ->
    le' ! s = Some vself.


Remark alloc_implies:
  forall tge vars x b t e m e' m',
    ~ InMembers x vars ->
    alloc_variables tge (PTree.set x (b, t) e) m vars e' m' ->
    e' ! x = Some (b, t).

Definition drop_block '((x, (_, t)): ident * (block * Ctypes.type)) : (ident * Ctypes.type) :=
  (x, t).

Remark In_drop_block:
  forall elts x t,
    In (x, t) (map drop_block elts) ->
    exists b, In (x, (b, t)) elts.

Remark drop_block_In:
  forall elts x b t,
    In (x, (b, t)) elts ->
    In (x, t) (map drop_block elts).

Remark alloc_In:
  forall tge vars e m e' m',
    alloc_variables tge e m vars e' m' ->
    NoDupMembers vars ->
    (forall x t,
        In (x, t) (map drop_block (PTree.elements e')) <->
        (In (x, t) (map drop_block (PTree.elements e)) /\ (forall t', In (x, t') vars -> t = t'))
        \/ In (x, t) vars).

Remark alloc_permutation:
  forall tge vars m e' m',
    alloc_variables tge empty_env m vars e' m' ->
    NoDupMembers vars ->
    Permutation.Permutation vars (map drop_block (PTree.elements e')).

Lemma Permutation_set:
  forall {A B} x (a:A) (b:B) e,
    ~InMembers x (PTree.elements e) ->
    Permutation.Permutation (PTree.elements (PTree.set x (a, b) e))
                            ((x, (a, b)) :: PTree.elements e).

Lemma set_nodupmembers:
  forall x (e: Clight.env) b1 t,
    NoDupMembers (map snd (PTree.elements e)) ->
    ~InMembers x (PTree.elements e) ->
    ~InMembers b1 (map snd (PTree.elements e)) ->
    NoDupMembers (map snd (PTree.elements (PTree.set x (b1, t) e))).

Remark alloc_nodupmembers:
  forall tge vars e m e' m',
    alloc_variables tge e m vars e' m' ->
    NoDupMembers vars ->
    NoDupMembers (map snd (PTree.elements e)) ->
    Forall (fun xv => ~InMembers (fst xv) (PTree.elements e)) vars ->
    (forall b, InMembers b (map snd (PTree.elements e)) -> Mem.valid_block m b) ->
    NoDupMembers (map snd (PTree.elements e')).

Remark alloc_exists:
  forall tge vars e m,
    NoDupMembers vars ->
    exists e' m',
      alloc_variables tge e m vars e' m'.

Remark Permutation_fst:
  forall vars elems,
    Permutation.Permutation vars elems ->
    Permutation.Permutation (var_names vars) (map fst elems).

Remark map_fst_drop_block:
  forall elems,
    map fst (map drop_block elems) = map fst elems.

Program Definition empty_co: composite :=
  {|
    co_su := Struct;
    co_members := [];
    co_attr := noattr;
    co_sizeof := 0;
    co_alignof := 1;
    co_rank := 0
  |}.