Home

POPL 2012 submission: Theorem 4

Constructed scalar fields

Section ScalarFields.

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

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

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

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

Definition scalar_fields_some_constructed (s : _ _ nativeop) :=
forall obj ar i h p hp, valid_pointer hier (Globals.heap (State.global s)) (Value.subobject obj ar i h p hp) ->
forall cn, last p = Some cn ->
forall c, hier ! cn = Some c ->
forall fs, In fs (Class.fields c) ->
forall ty, FieldSignature.type fs = FieldSignature.Scalar ty ->
forall v, Globals.get_field (Globals.field_values (State.global s)) (obj, ar, i, (h, p), fs) = Some v ->
assoc (@aux_constr_state_key_eq_dec _) (obj, ar, i, (h, p), fs) (State.field_construction_states s) = Some Constructed
.

Definition scalar_fields_some_constructed_recip (s : _ _ nativeop) :=
enable_uninitialized_scalar_fields cppsem = false ->
forall obj ar i h p hp, valid_pointer hier (Globals.heap (State.global s)) (Value.subobject obj ar i h p hp) ->
forall cn, last p = Some cn ->
forall c, hier ! cn = Some c ->
forall fs, In fs (Class.fields c) ->
forall ty, FieldSignature.type fs = FieldSignature.Scalar ty ->
assoc (@aux_constr_state_key_eq_dec _) (obj, ar, i, (h, p), fs) (State.field_construction_states s) = Some Constructed ->
exists v, Globals.get_field (Globals.field_values (State.global s)) (obj, ar, i, (h, p), fs) = Some v
.

Variables s1 : State.t A nativeop.

Lemma init_scalar_fields_some_constructed :
initial_state prog s1 ->
scalar_fields_some_constructed s1.
Proof.
inversion 1; subst.
unfold scalar_fields_some_constructed.
simpl.
inversion 1; subst.
rewrite PTree.gempty in H3.
discriminate.
Qed.

Lemma init_scalar_fields_some_constructed_recip :
initial_state prog s1 ->
scalar_fields_some_constructed_recip s1.
Proof.
inversion 1; subst.
unfold scalar_fields_some_constructed_recip.
simpl.
inversion 2; subst.
rewrite PTree.gempty in H4.
discriminate.
Qed.

Hypothesis Hs1 : invariant prog s1.

Variable s2 : State.t A nativeop.
Variable t : trace (evtr sem).

Hypothesis step : step prog cppsem s1 t s2.

Section Straight.

Hypothesis Hs1fields : scalar_fields_some_constructed s1.

Lemma preservation_scalar_fields_some_constructed :
scalar_fields_some_constructed s2.
Proof.
unfold scalar_fields_some_constructed in *.
Opaque Globals.get_field Globals.put_field.
inversion step; subst; simpl in *; try assumption.

intros.
destruct (aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs) (obj0, ar0, i0, (h0, p0), fs0)).
injection e; intros; subst; assumption.
unfold_ident_in_all.
rewrite (Globals.get_put_field_other H2 n) in H8.
eauto.

intros until 1.
destruct (peq obj obj0).
subst.
injection H1; intros until 2; subst; simpl in *.
generalize (Globals.valid_none (valid_global Hs1) (Ple_refl _)).
intros.
rewrite (unconstructed_scalar_fields Hs1 H3 H7) in H8.
discriminate.
injection H1; intros until 2; subst; simpl in *.
inversion H2; subst.
rewrite PTree.gso in H5; eauto.
eapply Hs1fields with (hp := hp2).
econstructor; eauto.

intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, hp, fs)
(obj0, ar0, i0, (h, p), fs0)
); eauto.
unfold_ident_in_all; abstract congruence.

intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, (h0, p0), fs0)
); eauto.

intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, (h0, p0), fs0)
); eauto.
unfold_ident_in_all.
rewrite (Globals.get_put_field_other H3 n) in H9.
eauto.

intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj', ar', i', (h, p), fs)
(obj0, ar0, i, (h0, p0), fs0)
); eauto.

intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, (h0, p0), fs0)
); eauto.
injection e; intros; subst.
Transparent Globals.get_field. simpl in *.
rewrite H in H5.
rewrite find_remove_field_same in H5.
discriminate.
assert (
Globals.get_field
(remove_field (obj, ar, i, (h, p), fs) (Globals.field_values gl))
(obj0, ar0, i0, (h0, p0), fs0) = Globals.get_field
( (Globals.field_values gl))
(obj0, ar0, i0, (h0, p0), fs0)
).
simpl.
rewrite H4.
rewrite (find_remove_field_other n).
reflexivity.
rewrite H6 in H5.
eauto.

intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, (h0, p0), fs0)
); eauto.
unfold_ident_in_all; abstract congruence.

intros.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj', ar', i', hp', fs)
(obj0, ar0, i, (h, p), fs0)
); eauto.
generalize (kind Hs1).
intro.
unfold state_kind_inv in *; simpl in *; destruct hp'; invall; subst.
rewrite (last_complete) in H8.
invall; subst.
unfold_ident_in_all; abstract congruence.

Qed.

End Straight.

Section Recip.

Hypothesis Hs1fields : scalar_fields_some_constructed_recip s1.

Lemma preservation_scalar_fields_some_constructed_recip :
scalar_fields_some_constructed_recip s2.
Proof.
unfold scalar_fields_some_constructed_recip in *.
Opaque Globals.get_field Globals.put_field.
inversion step; subst; simpl in *; try assumption.

intros.
destruct (aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs) (obj0, ar0, i0, (h0, p0), fs0)).
injection e; intros; subst.
erewrite Globals.get_put_field_same.
2 : eassumption.
eauto.
erewrite Globals.get_put_field_other.
2 : eassumption.
eauto.
assumption.

intros until 2.
destruct (peq obj obj0).
subst.
injection H1; intros until 2; subst; simpl in *.
generalize (Globals.valid_none (valid_global Hs1) (Ple_refl _)).
intros.
rewrite (construction_states_fields_none Hs1 H4) in H9.
discriminate.
injection H1; intros until 2; subst; simpl in *.
inversion H3; subst.
rewrite PTree.gso in H6; eauto.
eapply Hs1fields with (hp := hp2).
assumption.
econstructor; eauto.

intros until 6.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, hp, fs)
(obj0, ar0, i0, (h, p), fs0)
); eauto.
intro; discriminate.

intro.
congruence.

intros until 6.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, (h0, p0), fs0)
).
injection e; intros; subst.
erewrite Globals.get_put_field_same.
2 : eassumption.
eauto.
erewrite Globals.get_put_field_other.
2 : eassumption.
eauto.
assumption.

intros until 6.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj', ar', i', (h, p), fs)
(obj0, ar0, i, (h0, p0), fs0)
); eauto.
generalize (kind Hs1).
unfold state_kind_inv; simpl.
intro; invall; subst.
rewrite last_complete in H8.
invall; subst.
congruence.

intros until 6.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, (h0, p0), fs0)
).
intro; discriminate.
assert (
Globals.get_field
(remove_field (obj, ar, i, (h, p), fs) (Globals.field_values gl))
(obj0, ar0, i0, (h0, p0), fs0) = Globals.get_field
( (Globals.field_values gl))
(obj0, ar0, i0, (h0, p0), fs0)
).
Transparent Globals.get_field.
simpl.
rewrite H5.
rewrite (find_remove_field_other n).
reflexivity.
unfold_ident_in_all.
rewrite H6.
eauto.

intros until 6.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj, ar, i, (h, p), fs)
(obj0, ar0, i0, (h0, p0), fs0)
); eauto.
unfold_ident_in_all; abstract congruence.

intros until 6.
sdestruct (
Cppsem.aux_constr_state_key_eq_dec (obj', ar', i', hp', fs)
(obj0, ar0, i, (h, p), fs0)
); eauto.
intro; discriminate.

Qed.

End Recip.

End ScalarFields.

End Preservation.