Require Import Coqlib Values Memory.
injection from Vundef to pointer values are undesirable for footprint preservation,
because cmpu on pointer values generates cmp footprint, while cmpu on Vundefs
has no footprint.
specific requirements on Vundef injected values
Definition not_ptr (
v:
val) :
Prop :=
match v with
|
Vptr _ _ =>
False
|
_ =>
True
end.
Definition local_ptr (
Local:
block ->
Prop) (
v:
val) :
Prop :=
match v with
|
Vptr b _ =>
Local b
|
_ =>
True
end.
Lemma not_ptr_implies_local:
forall v Local,
not_ptr v ->
local_ptr Local v.
Proof.
destruct v; simpl; intros; tauto. Qed.
restricting Val.inject
Definition val_inj_undef_spec (
v v':
val) (
spec:
val ->
Prop) :
Prop :=
match v with
|
Vundef =>
spec v'
|
_ =>
True
end.
Definition val_inj_undef_spec' (
v v':
val) (
spec:
val ->
Prop) :
Prop :=
v =
Vundef ->
spec v'.
Lemma val_inj_undef_spec_eq:
forall v v'
spec,
val_inj_undef_spec v v'
spec <->
val_inj_undef_spec'
v v'
spec.
Proof.
destruct v; simpl; cbv; intros; firstorder; discriminate. Qed.
Lemma val_inj_undef_spec_implies:
forall v v' (
spec1 spec2:
val ->
Prop),
(
spec1 v' ->
spec2 v') ->
val_inj_undef_spec v v'
spec1 ->
val_inj_undef_spec v v'
spec2.
Proof.
Inductive vl_inj_undef_spec :
list val ->
list val -> (
val ->
Prop) ->
Prop :=
|
inject_undef_nil:
forall spec,
vl_inj_undef_spec nil nil spec
|
inject_undef_cons:
forall v v'
spec vl vl',
val_inj_undef_spec v v'
spec ->
vl_inj_undef_spec vl vl'
spec ->
vl_inj_undef_spec (
v::
vl) (
v'::
vl')
spec.
Lemma vl_inj_undef_spec_implies:
forall (
spec1 spec2:
val ->
Prop),
(
forall v,
spec1 v ->
spec2 v) ->
forall vl vl',
vl_inj_undef_spec vl vl'
spec1 ->
vl_inj_undef_spec vl vl'
spec2.
Proof.
induction vl.
intros;
inv H0.
constructor.
intros.
inv H0.
constructor;
auto.
eapply val_inj_undef_spec_implies;
try eassumption;
auto.
Qed.
Definition val_inj_undef_not_ptr (
v v':
val) :=
val_inj_undef_spec v v'
not_ptr.
Definition val_inj_undef_local_ptr (
Local:
block ->
Prop) (
v v':
val) :=
val_inj_undef_spec v v' (
local_ptr Local).
Definition vl_inj_undef_not_ptr (
vl vl':
list val) :=
vl_inj_undef_spec vl vl'
not_ptr.
Definition vl_inj_undef_local_ptr (
Local:
block ->
Prop) (
vl vl':
list val) :=
vl_inj_undef_spec vl vl' (
local_ptr Local).
Lemma Vundef_inj_not_ptr_implies_local:
forall Local v v',
val_inj_undef_not_ptr v v' ->
val_inj_undef_local_ptr Local v v'.
Proof.
Lemma Vundef_inj_list_not_ptr_implies_local:
forall Local vl vl',
vl_inj_undef_not_ptr vl vl' ->
vl_inj_undef_local_ptr Local vl vl'.
Proof.
restricting memval_inject
Definition memval_inject_undef_spec (
mv mv':
memval) (
spec:
val ->
Prop) :
Prop :=
match mv,
mv'
with
|
Undef,
Fragment v _ _ =>
spec v
|
Fragment Vundef _ _,
Fragment v _ _ =>
spec v
|
_,
_ =>
True
end.
Lemma memval_inject_undef_spec_implies:
forall (
spec1 spec2:
val ->
Prop),
(
forall v,
spec1 v ->
spec2 v) ->
forall mv mv',
memval_inject_undef_spec mv mv'
spec1 ->
memval_inject_undef_spec mv mv'
spec2.
Proof.
Definition memval_inject_undef_not_ptr (
mv mv':
memval) :
Prop :=
memval_inject_undef_spec mv mv' (
not_ptr).
Definition memval_inject_undef_local (
Local:
block ->
Prop) (
mv mv':
memval) :
Prop :=
memval_inject_undef_spec mv mv' (
local_ptr Local).
Lemma Undef_inj_not_ptr_implies_local:
forall mv mv',
memval_inject_undef_not_ptr mv mv' ->
forall Local,
memval_inject_undef_local Local mv mv'.
Proof.
TODO: properties about memval_inject?
Lemma memval_inject_undef_not_ptr_bytes:
forall n,
memval_inject_undef_not_ptr (
Byte n) (
Byte n).
Proof.
cbn; auto. Qed.
Lemma memval_inject_undef_not_ptr_frag:
forall v1 v2 q n,
val_inj_undef_not_ptr v1 v2 ->
memval_inject_undef_not_ptr (
Fragment v1 q n) (
Fragment v2 q n).
Proof.
cbn; auto. Qed.
Lemma memval_inject_undef_local_ptr_frag:
forall Local v1 v2 q n,
val_inj_undef_local_ptr Local v1 v2 ->
memval_inject_undef_local Local (
Fragment v1 q n) (
Fragment v2 q n).
Proof.
cbn; auto. Qed.
restricting Mem.mem_inj