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.
inversion 2;
subst;
intros;
try (
simpl in *;
congruence);
simpl in Hdiff;
revert Hdiff.
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
i, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst.
exact (
stack_objects_in_construction Hinv (
l1 :=
nil) (
refl_equal _) (
refl_equal _)).
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
i, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst.
exact (
stack_objects_in_construction Hinv (
l1 :=
nil) (
refl_equal _) (
refl_equal _)).
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj,
(
ar,
i,
(
match k2 with
|
Constructor.direct_non_virtual =>
h
|
Constructor.virtual =>
Class.Inheritance.Shared
end,
match k2 with
|
Constructor.direct_non_virtual =>
p ++
b ::
nil
|
Constructor.virtual =>
b ::
nil
end))) (
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst.
exact (
stack_objects_in_construction Hinv (
l1 :=
nil) (
refl_equal _) (
refl_equal _)).
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj,
(
ar,
i,
(
match k2 with
|
Constructor.direct_non_virtual =>
h
|
Constructor.virtual =>
Class.Inheritance.Shared
end,
match k2 with
|
Constructor.direct_non_virtual =>
p ++
b ::
nil
|
Constructor.virtual =>
b ::
nil
end))) (
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst.
exact (
stack_objects_in_construction Hinv (
l1 :=
nil) (
refl_equal _) (
refl_equal _)).
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p))) (
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst.
eauto using kind_object_in_construction.
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
j, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst.
eauto using kind_object_in_construction.
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p))) (
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst.
eauto using kind_object_in_construction.
sdestruct(
pointer_eq_dec (
A:=
A)
(
obj,
(
ar,
i,
(
match beta with
|
Constructor.direct_non_virtual =>
h
|
Constructor.virtual =>
Class.Inheritance.Shared
end,
match beta with
|
Constructor.direct_non_virtual =>
p ++
b ::
nil
|
Constructor.virtual =>
b ::
nil
end))) (
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst;
eauto using kind_object_in_construction.
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i,
hp)) (
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst;
eauto using kind_object_in_construction.
sdestruct(
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p))) (
obj0,
arihp)
);
try congruence.
injection e;
intros;
subst;
eauto using kind_object_in_construction.
Qed.
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.