Module Progress

Require Import Relations.
Require Import Coqlib.
Require Import LibPos.
Require Import Maps.
Require Import LibLists.
Require Import Cppsem.
Require Import Cplusconcepts.
Require Import CplusWf.
Require Import Events.
Require Import Smallstep.
Require Import Wellfounded.
Require Import CplusWf.
Load Param.
Open Scope nat_scope.

Section Progress.

Variable A : ATOM.t.
Variable nativeop : Type.

Variable prog : Program.t A nativeop.
Notation hier := (Program.hierarchy prog).

Hypothesis hierarchy_wf : Well_formed_hierarchy.prop hier.

Inductive has_trivial_destructor : ident -> Prop :=
| has_trivial_destructor_intro : forall cn hc,
  hier ! cn = Some hc ->
  (forall b, In (Class.Inheritance.Repeated, b) (Class.super hc) -> has_trivial_destructor b) ->
  (forall b, is_virtual_base_of hier b cn -> has_trivial_destructor b) ->
  (forall fs, In fs (Class.fields hc) -> forall b n, FieldSignature.type fs = FieldSignature.Struct b n -> has_trivial_destructor b) ->
  forall lc, (Program.hierarchy prog) ! cn = Some lc ->
    forall m,
      Method.find (Program.destructor_sig prog) (Class.methods lc) = Some m ->
      forall mcode,
        Method.kind m = Method.concrete mcode ->
        forall mb,
          (Program.methods prog) ! mcode = Some mb ->
          Method_body.code mb = Sreturn None ->
          has_trivial_destructor cn.

Variable cppsem : cppsemparam.
Variable sem : semparam A nativeop.

Definition goal_destr cn := ( forall s1,
  match State.kind s1 with
    | State.destr obj ar i (h, p) k1 k2 l =>
      last p = Some cn ->
      forall c, hier ! cn = Some c ->
        (
          match k1 as k return Constructor.init_key_secondary k -> list (Constructor.init_key_item A k) -> Prop with
            | Constructor.base =>
              fun k2' l' => forall x, In x l' ->
                match k2' with
                  | Constructor.direct_non_virtual => In (Class.Inheritance.Repeated, x) (Class.super c)
                  | _ => is_virtual_base_of hier x cn
                end
            | Constructor.field => fun _ l' => forall x, In x l' -> In x (Class.fields c)
          end
        ) k2 l ->
        exists s2,
          star _ (step prog cppsem (sem := sem)) s1 E0 s2 /\
          State.kind s2 = State.destr obj ar i (h, p) k1 k2 nil /\
          State.deallocated_objects s2 = State.deallocated_objects s1 /\
          State.stack s2 = State.stack s1
    | _ => True
  end) /\ (forall s1,
  match State.kind s1 with
    | State.destr_array obj ar i cn' =>
      cn = cn' ->
      (-1 <= i)%Z ->
      exists s2,
        star _ (step prog cppsem (sem := sem)) s1 E0 s2 /\
        State.kind s2 = State.destr_array obj ar (-1) cn /\
        State.deallocated_objects s2 = State.deallocated_objects s1 /\
        State.stack s2 = State.stack s1
    | _ => True
  end).

Lemma progress'_destr : forall cn, has_trivial_destructor cn -> goal_destr cn.

Proof.

Corollary progress_destr : forall gl obj o,
    (Globals.heap gl) ! obj = Some o ->
    has_trivial_destructor (Object.class o) ->
    (0 <= Object.arraysize o)%Z ->
    forall sdestruct sdestruct',
      exit_succ sdestruct = Some sdestruct' ->
      forall vars stl0 stl bl stk cs auxcs f,
        exists gl', exists cs', exists auxcs',
          star _ (step prog cppsem (sem := sem))
          (State.make (State.codepoint vars sdestruct stl0 (BlockPoint.make stl (Some obj) :: bl)) stk gl cs auxcs f) E0
          (State.make (State.codepoint vars sdestruct' stl bl) stk gl' cs' auxcs' (obj :: f)).

Proof.

Inductive has_nearly_trivial_constructor : ident -> Prop :=
| has_nearly_trivial_constructors_intro : forall cn hc,
  hier ! cn = Some hc ->
  (forall b, In (Class.Inheritance.Repeated, b) (Class.super hc) -> has_nearly_trivial_constructor b) ->
  (forall b, is_virtual_base_of hier b cn -> has_nearly_trivial_constructor b) ->
  (forall fs, In fs (Class.fields hc) -> forall b n, FieldSignature.type fs = FieldSignature.Struct b n -> has_nearly_trivial_constructor b) ->
  forall lc, (Program.constructors prog) ! cn = Some lc ->
    forall c,
      assoc (@Program.constructor_key_eq_dec A) nil lc = Some c ->
      (forall b, In (Class.Inheritance.Repeated, b) (Class.super hc) -> assoc (@Constructor.initializer_key_eq_dec A) (existT _ Constructor.base (Constructor.direct_non_virtual, b)) (Constructor.initializers c) = Some (Sconstructor b nil)) ->
      (forall b, is_virtual_base_of hier b cn ->
        assoc (@Constructor.initializer_key_eq_dec A) (existT _ Constructor.base (Constructor.virtual, b)) (Constructor.initializers c) = Some (Sconstructor b nil)) ->
      (forall fs, In fs (Class.fields hc) ->
        forall b n, FieldSignature.type fs = FieldSignature.Struct b n ->
          assoc (@FieldSignature.eq_dec _) fs (Constructor.struct_field_initializers c) = None) ->
      (forall fs, In fs (Class.fields hc) ->
        forall ty, FieldSignature.type fs = FieldSignature.Scalar ty -> (
          (enable_uninitialized_scalar_fields cppsem = false -> assoc (@Constructor.initializer_key_eq_dec A) (existT _ Constructor.field (tt, fs)) (Constructor.initializers c) <> None) /\ forall st, assoc (@Constructor.initializer_key_eq_dec A) (existT _ Constructor.field (tt, fs)) (Constructor.initializers c) = Some st ->
            exists aty, ty = Typ.atom aty /\
              exists op, (exists tr, exists va, nativeop_sem (s := sem) op nil (Some (existT _ aty va)) tr) /\
                exists v, st = Sseq (Snative op nil (Some v)) (Sinitscalar v))) ->
      Constructor.body c = Sreturn None ->
      has_nearly_trivial_constructor cn.

Definition goal cn := ( forall s1,
  match State.kind s1 with
    | State.constr obj ar i (h, p) tinit init body vars k1 k2 l =>
      last p = Some cn ->
      forall c, hier ! cn = Some c ->
        (
          match k1 as k return Constructor.init_key_secondary k -> list (Constructor.init_key_item A k) -> Prop with
            | Constructor.base =>
              fun k2' l' => forall x, In x l' ->
                match k2' with
                  | Constructor.direct_non_virtual => In (Class.Inheritance.Repeated, x) (Class.super c)
                  | _ => is_virtual_base_of hier x cn
                end
            | Constructor.field => fun _ l' => forall x, In x l' -> In x (Class.fields c)
          end
        ) k2 l ->
        forall lc, (Program.constructors prog) ! cn = Some lc ->
          forall c, assoc (@Program.constructor_key_eq_dec A) nil lc = Some c ->
            tinit = Constructor.struct_field_initializers c ->
            init = Constructor.initializers c ->
            body = Constructor.body c ->
            exists tr, exists s2, exists vars',
              star _ (step prog cppsem (sem := sem)) s1 tr s2 /\
              (Globals.heap (State.global s2)) ! obj = (Globals.heap (State.global s1)) ! obj /\
              State.kind s2 = State.constr obj ar i (h, p) tinit init body vars' k1 k2 nil /\
              State.deallocated_objects s2 = State.deallocated_objects s1 /\
              State.stack s2 = State.stack s1
    | _ => True
  end) /\ (forall s1,
  match State.kind s1 with
    | State.constr_array obj ar n i cn' tinit vars =>
      cn = cn' ->
      tinit = (fun _ => Sconstructor cn' nil) ->
      (0 <= i <= n)%Z ->
      exists tr, exists s2,
        star _ (step prog cppsem (sem := sem)) s1 tr s2 /\
        (Globals.heap (State.global s2)) ! obj = (Globals.heap (State.global s1)) ! obj /\
        State.kind s2 = State.constr_array obj ar n n cn tinit vars /\
        State.deallocated_objects s2 = State.deallocated_objects s1 /\
              State.stack s2 = State.stack s1
    | _ => True
  end).

Lemma progress' : forall cn, has_nearly_trivial_constructor cn -> goal cn.

Proof.

Corollary progress : forall cn,
  has_nearly_trivial_constructor cn ->
  forall num, (0 < num)%Z ->
    forall vlocstruct stm vars stl bl stk gl cs auxcs f,
      exists hp, exists obj, exists gl1,
        (obj, gl1) = Globals.new gl cn num /\
        exists t, exists vars', exists gl', exists cs', exists auxcs',
          star _ (step prog cppsem (sem := sem))
          (State.make (State.codepoint vars (Sblock (Some (vlocstruct, cn, num)) (fun _ => Sconstructor cn nil) stm) stl bl) stk gl cs auxcs f) t
          (State.make (State.codepoint vars' stm nil (BlockPoint.make stl (Some obj) :: bl)) stk gl' cs' auxcs' f) /\
          vars' = PTree.set vlocstruct (Value.ptr (Value.subobject obj nil 0 Class.Inheritance.Repeated (cn :: nil) hp)) vars /\
            (Globals.heap gl') ! obj = (Globals.heap gl1) ! obj /\
            exists o, (Globals.heap gl1) ! obj = Some o /\
              Object.class o = cn /\
              Object.arraysize o = num
              .

Proof.

End Progress.