Home

Module ConstrorderOther

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 Invariant.
Require Import Preservation.
Require Import Smallstep.
Require Import Dyntype.
Require Import SubobjectOrdering.
Require Import ConstrSubobjectOrdering.
Require Import Constrorder.
Load Param.
Open Scope Z_scope.

Section Constrorder.

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

Open Scope Z_scope.

Variable prog : Program.t A nativeop.

Hypothesis hierarchy_wf : Well_formed_hierarchy.prop (Program.hierarchy prog).

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


Lemma construction_state_modify_topmost_object : forall s1
  (Hinv : invariant prog s1)
  t s2 (Hstep : step prog cppsem (sem := sem) s1 t s2)
  obj arihp
  (Hdiff :
    assoc (@pointer_eq_dec _) (obj, arihp) (State.construction_states s1)
    <>
    assoc (@pointer_eq_dec _) (obj, arihp) (State.construction_states s2)),
  exists p, stack_objects s1 = obj :: p.
Proof.


POPL 2012 submission: Lemma 15



Theorem lower_object_construction_states_no_change : forall s1 t s2, star _ (step prog cppsem (sem := sem)) s1 t s2 ->
  invariant prog s1 -> forall obj,
  In obj (stack_objects s1) ->
  In obj (stack_objects s2) ->
  forall obj', Plt obj' obj ->
    forall arihp,
    assoc (@pointer_eq_dec _) (obj', arihp) (State.construction_states s1)
    =
    assoc (@pointer_eq_dec _) (obj', arihp) (State.construction_states s2).
Proof.

Theorem stack_storage_duration_included_in_other_lifetime :
  forall s0,
    invariant prog s0 ->
    forall t1 s1,
      step prog cppsem (sem := sem) s0 t1 s1 ->
      forall obj, stack_objects s1 = obj :: stack_objects s0 ->
        forall t2 s2, star _ (step prog cppsem (sem := sem)) s1 t2 s2 ->
          forall obj', In obj' (stack_objects s0) ->
            forall arihp,
              assoc (@pointer_eq_dec _) (obj', arihp) (State.construction_states s1) <>
              assoc (@pointer_eq_dec _) (obj', arihp) (State.construction_states s2) ->
              exists s'1, exists t'1,
                star _ (step prog cppsem (sem := sem)) s1 t'1 s'1 /\
                exists s'2,
                  step prog cppsem (sem := sem) s'1 E0 s'2 /\
                  State.deallocated_objects s'2 = obj :: State.deallocated_objects s'1 /\
                  assoc (@pointer_eq_dec _) (obj', arihp) (State.construction_states s'2) =
                  assoc (@pointer_eq_dec _) (obj', arihp) (State.construction_states s1) /\
                  exists t'2,
                    star _ (step prog cppsem (sem := sem)) s'2 t'2 s2 /\
                    t2 = t'1 ** t'2.
Proof.

End Constrorder.