Home
Module PreservationStackKconstrotherField
Load PreservationHeader.
Lemma goal :
forall obj ar i h P tinit init body vars current other sf,
sf = (
StackFrame.Kconstrother obj ar i (
h,
P)
tinit init body vars Constructor.field tt current other) ->
forall (
Hin:
In sf (
State.stack s2)),
stackframe_weak_inv prog s2 sf.
Proof.
inversion Hs1.
Opaque concat cs_le_dec Zminus.
inversion step;
intros;
subst;
unfold stackframe_weak_inv in *;
simpl in *;
unfold Globals.update in *;
simpl in *;
subst;
try exact (
stack _ Hin);
try exact (
stack _ (
or_intror _ Hin));
try (
destruct Hin as [? |
Hin2]; [
discriminate |
exact (
stack _ Hin2) ]).
symmetry in H1.
destruct Hin as [ |
Hin2].
discriminate.
generalize (
stack _ Hin2).
intro;
invall;
subst.
esplit.
split.
eassumption.
esplit.
split.
eapply Globals.valid_pointer_new;
simpl;
eauto.
eauto 8.
destruct Hin as [ |
Hin2].
discriminate.
generalize (
stack _ (
or_intror _ Hin2)).
intro.
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
i, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0, (
ar0,
i0, (
h,
P)))
).
2 :
assumption.
apply False_rect.
injection e;
intros;
invall;
subst.
revert kind.
unfold state_kind_inv.
simpl.
intros;
invall;
subst.
assert (
i0 <=
i0 <
n)
by abstract omega.
generalize (
H14 _ H8).
intro.
unfold_ident_in_all;
abstract congruence.
generalize (
stack _ (
or_intror _ Hin)).
intro.
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
i, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0, (
ar0,
i0, (
h,
P)))
).
2 :
assumption.
apply False_rect.
injection e;
intros;
invall;
subst.
destruct (
stack_wf _ nil _ (
refl_equal _)
_ Hin).
destruct (
H1 _ _ (
refl_equal _)
_ (
refl_equal _)).
destruct H2.
generalize (
refl_equal (
length ar0)).
rewrite H2 at 1.
rewrite app_length.
destruct x.
abstract congruence.
simpl;
intro;
omegaContradiction.
destruct hp.
simpl.
destruct Hin as [
Heq |
Hin].
injection Heq;
intros;
subst.
destruct (
StackFrame.Kconstrother_field_inj Heq);
subst.
cut (
exists cs0 :
construction_state,
assoc (
pointer_eq_dec (
A:=
A)) (
obj0, (
ar0,
i0, (
h,
P)))
cs =
Some cs0 /\
(
exists hp :
is_some (
last P),
valid_pointer (
Program.hierarchy prog) (
Globals.heap gl)
(
Value.subobject obj0 ar0 i0 h P hp) /\
(
exists cn :
ident,
last P =
Some cn /\
(
exists c :
Class.t A,
(
Program.hierarchy prog) !
cn =
Some c /\
cs0 =
BasesConstructed /\
(
exists l1 :
list (
FieldSignature.t A),
Class.fields c =
l1 ++
current ::
other /\
(
if Cppsem.aux_constr_state_key_eq_dec
(
obj0,
ar0,
i0, (
h,
P),
current)
(
obj0,
ar0,
i0, (
h,
P),
current)
then Some StartedConstructing
else
assoc aux_constr_state_key_eq_dec
(
obj0,
ar0,
i0, (
h,
P),
current)
auxcs) =
Some StartedConstructing))))
);
eauto.
destruct (
aux_constr_state_key_eq_dec
(
obj0,
ar0,
i0, (
h,
P),
current)
(
obj0,
ar0,
i0, (
h,
P),
current)
).
revert kind.
unfold state_kind_inv;
simpl.
intro;
invall;
eauto 16.
abstract congruence.
cut (
exists cs0 :
construction_state,
assoc (
pointer_eq_dec (
A:=
A)) (
obj0, (
ar0,
i0, (
h,
P)))
cs =
Some cs0 /\
(
exists hp :
is_some (
last P),
valid_pointer (
Program.hierarchy prog) (
Globals.heap gl)
(
Value.subobject obj0 ar0 i0 h P hp) /\
(
exists cn :
ident,
last P =
Some cn /\
(
exists c :
Class.t A,
(
Program.hierarchy prog) !
cn =
Some c /\
cs0 =
BasesConstructed /\
(
exists l1 :
list (
FieldSignature.t A),
Class.fields c =
l1 ++
current ::
other /\
(
if Cppsem.aux_constr_state_key_eq_dec
(
obj,
ar,
i, (
t,
l),
fs)
(
obj0,
ar0,
i0, (
h,
P),
current)
then Some StartedConstructing
else
assoc aux_constr_state_key_eq_dec
(
obj0,
ar0,
i0, (
h,
P),
current)
auxcs) =
Some StartedConstructing))))
).
intro;
assumption.
generalize (
stack _ Hin).
intro.
destruct (
aux_constr_state_key_eq_dec
(
obj,
ar,
i, (
t,
l),
fs)
(
obj0,
ar0,
i0, (
h,
P),
current)
).
invall;
eauto 16.
assumption.
destruct Hin as [ |
Hin2].
discriminate.
generalize (
stack _ (
or_intror _ Hin2)).
intro.
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, (
ar0,
i0, (
h0,
P)))
).
apply False_rect.
injection e;
intros;
subst.
revert kind.
unfold state_kind_inv.
simpl.
intro;
invall;
subst.
destruct k2;
invall;
subst.
generalize (
H15 _ (
or_introl _ (
refl_equal _))).
intro;
unfold_ident_in_all;
abstract congruence.
generalize (
H17 _ (
or_introl _ (
refl_equal _))).
intro;
unfold_ident_in_all;
abstract congruence.
assumption.
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, (
ar0,
i0, (
h0,
P)))
).
2 :
exact (
stack _ (
or_intror _ Hin)).
apply False_rect.
destruct (
stack_wf _ nil _ (
refl_equal _)
_ Hin).
destruct (
H _ _ _ _ (
refl_equal _)).
generalize (
stack _ (
or_introl _ (
refl_equal _))).
destruct k2;
injection e;
intros;
invall;
subst.
generalize (
H1 _ _ _ (
refl_equal _)).
inversion 1.
rewrite last_complete in H13.
injection H13;
intros;
subst.
generalize (
concat_last (
path_nonempty H16)
H17).
rewrite (
path_last H16).
rewrite H11.
injection 1;
intros;
subst.
eapply Plt_irrefl with to'.
eapply Ple_Plt_trans with cn.
eauto using Well_formed_hierarchy.path_le.
eapply Well_formed_hierarchy.well_founded.
eassumption.
eassumption.
eapply in_map_bases_elim.
rewrite H14.
eauto using in_or_app.
destruct l.
abstract congruence.
generalize (
refl_equal (
length ar0)).
rewrite H6 at 1.
rewrite app_length.
simpl;
intro;
abstract omegaContradiction.
generalize (
H1 _ _ _ (
refl_equal _)).
eapply relptr_gt_min.
generalize (
stack _ Hin).
intro.
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p)))
(
obj0, (
ar0,
i0, (
h0,
P)))
).
invall;
eauto 16.
assumption.
simpl.
sdestruct (
aux_constr_state_key_eq_dec
(
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
P),
current)
).
apply False_rect.
injection e;
intros;
subst.
destruct (
stack_state_wf _ Hin).
generalize (
H1 _ _ _ (
refl_equal _)).
eauto using relptr_gt_irrefl.
exact (
stack _ Hin).
sdestruct (
aux_constr_state_key_eq_dec
(
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
P),
current)
).
apply False_rect.
injection e;
intros;
subst.
destruct (
stack_wf _ nil _ (
refl_equal _)
_ Hin).
destruct (
H4 _ _ _ _ (
refl_equal _)).
generalize (
H6 _ _ _ (
refl_equal _)).
eauto using relptr_gt_irrefl.
generalize (
stack _ (
or_intror _ Hin)).
intro.
invall.
esplit.
split.
eassumption.
esplit.
split.
eassumption.
eauto 8.
simpl.
sdestruct (
aux_constr_state_key_eq_dec
(
obj',
ar',
i', (
h,
p),
fs)
(
obj0,
ar0,
i, (
h0,
P),
current)
).
apply False_rect.
injection e;
intros;
subst.
destruct (
stack_wf _ nil _ (
refl_equal _)
_ Hin).
destruct (
H _ _ _ _ (
refl_equal _)).
generalize (
H1 _ _ _ (
refl_equal _)).
eauto using relptr_gt_irrefl.
exact (
stack _ (
or_intror _ Hin)).
destruct Hin as [ |
Hin2] .
discriminate.
destruct Hin2 as [ |
Hin ].
discriminate.
generalize (
stack _ (
Hin)).
intro.
sdestruct (
pointer_eq_dec (
A:=
A)
(
obj, (
ar,
j, (
Class.Inheritance.Repeated,
cn ::
nil)))
(
obj0, (
ar0,
i, (
h,
P)))
).
apply False_rect.
revert kind.
unfold state_kind_inv.
simpl;
injection e;
intros;
invall;
subst.
assert (0 <=
i <=
i)
by abstract omega.
generalize (
H21 _ H5).
unfold_ident_in_all;
abstract congruence.
assumption.
sdestruct (
aux_constr_state_key_eq_dec
(
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
P),
current)
).
apply False_rect.
injection e;
intros;
subst.
destruct (
stack_state_wf _ Hin).
generalize (
H0 _ _ _ (
refl_equal _)).
eauto using relptr_gt_irrefl.
exact (
stack _ Hin).
simpl.
destruct Hin as [ |
Hin].
discriminate.
generalize (
stack _ Hin).
intro.
sdestruct (
aux_constr_state_key_eq_dec
(
obj,
ar,
i, (
h,
p),
fs)
(
obj0,
ar0,
i0, (
h0,
P),
current)
).
apply False_rect.
injection e;
intros;
subst.
revert kind.
unfold state_kind_inv;
simpl.
intros;
invall;
subst;
unfold_ident_in_all;
abstract congruence.
assumption.
destruct hp'.
simpl.
sdestruct (
aux_constr_state_key_eq_dec
(
obj',
ar',
i', (
t,
l0),
fs)
(
obj0,
ar0,
i, (
h,
P),
current)).
apply False_rect.
injection e;
intros;
subst.
destruct (
stack_wf _ nil _ (
refl_equal _)
_ Hin).
destruct (
H _ _ _ _ (
refl_equal _)).
generalize (
H1 _ _ _ (
refl_equal _)).
eauto using relptr_gt_irrefl.
exact (
stack _ (
or_intror _ Hin)).
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p)))
(
obj0, (
ar0,
i0, (
h0,
P)))
).
apply False_rect.
injection e;
intros;
subst.
destruct (
stack_state_wf _ Hin).
generalize (
H2 _ _ _ (
refl_equal _)).
apply SubobjectOrdering.relptr_gt_irrefl.
assumption.
exact (
stack _ Hin).
destruct Hin as [ |
Hin2].
discriminate.
destruct Hin2 as [ |
Hin].
discriminate.
generalize (
stack _ Hin).
intro.
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, (
ar0,
i0, (
h0,
P)))
).
2 :
assumption.
apply False_rect.
revert kind.
unfold state_kind_inv;
simpl;
intro.
destruct beta;
injection e;
intros;
invall;
subst.
generalize (
H23 _ (
or_introl _ (
refl_equal _))).
unfold_ident_in_all;
abstract congruence.
generalize (
H24 _ (
or_introl _ (
refl_equal _))).
unfold_ident_in_all;
abstract congruence.
sdestruct (
(
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i,
hp)) (
obj0, (
ar0,
i0, (
h,
P)))
)).
apply False_rect.
injection e;
intros;
subst.
destruct (
stack_wf _ nil _ (
refl_equal _)
_ Hin).
destruct (
H _ _ _ _ (
refl_equal _)).
revert kind.
unfold state_kind_inv;
simpl.
destruct hp'.
destruct beta;
intro;
invall;
subst.
generalize (
H1 _ _ _ (
refl_equal _)).
inversion 1.
subst.
rewrite last_complete in H17.
injection H17;
intro;
subst.
generalize (
concat_last (
path_nonempty H18)
H19).
rewrite (
path_last H18).
intro.
generalize (
stack _ (
or_introl _ (
refl_equal _))).
simpl.
intro;
invall;
subst.
rewrite last_complete in H6.
injection H6;
intros;
subst.
replace x5 with to'
in *
by abstract congruence.
apply (
Plt_irrefl to').
eapply Ple_Plt_trans with x1.
eauto using Well_formed_hierarchy.path_le.
eapply Well_formed_hierarchy.well_founded.
eassumption.
eassumption.
eapply in_map_bases_elim.
eapply in_rev_elim.
rewrite H23.
eauto using in_or_app.
generalize (
refl_equal (
length ar')).
rewrite H14 at 1.
rewrite app_length.
destruct l0.
congruence.
simpl;
intro;
omegaContradiction.
generalize (
H1 _ _ _ (
refl_equal _)).
inversion 1.
subst.
injection H17;
intros;
subst.
generalize (
concat_last (
path_nonempty H18)
H19).
rewrite (
path_last H18).
intro.
generalize (
stack _ (
or_introl _ (
refl_equal _))).
simpl.
intro;
invall;
subst.
injection H6;
intros;
subst.
injection H10;
intros;
subst.
apply (
Plt_irrefl to').
eapply Ple_Plt_trans with x1.
eauto using Well_formed_hierarchy.path_le.
eapply Well_formed_hierarchy.is_virtual_base_of_lt.
eassumption.
eapply vborder_list_virtual_base.
eassumption.
eassumption.
eauto using in_rev_intro,
in_or_app.
generalize (
refl_equal (
length ar')).
rewrite H14 at 1.
rewrite app_length.
destruct l0.
congruence.
simpl;
intro;
omegaContradiction.
destruct hp.
exact (
stack _ (
or_intror _ Hin)).
sdestruct (
pointer_eq_dec (
A:=
A) (
obj, (
ar,
i, (
h,
p)))
(
obj0, (
ar0,
i0, (
h0,
P)))
).
apply False_rect.
injection e;
intros;
subst.
destruct (
stack_state_wf _ Hin _ (
refl_equal _)).
invall.
destruct x.
congruence.
generalize (
refl_equal (
length ar0)).
rewrite H1 at 1.
rewrite app_length.
simpl;
intro;
omegaContradiction.
exact (
stack _ Hin).
Qed.
End Preservation.