In-memory representation of values.
Require Import Coqlib.
Require Import Axioms.
Require Archi.
Require Import AST.
Require Import Integers.
Require Import Maps.
Require Import Floats.
Require Import Values.
Require Import Psatz.
Require Import Values_symbolictype.
Require Import Values_symbolic.
Require Import Normalise.
Require Import NormaliseSpec.
Require Import IntFacts.
Require Import ExprEval.
Properties of memory chunks
Memory reads and writes are performed by quantities called memory chunks,
encoding the type, size and signedness of the chunk being addressed.
The following functions extract the size information from a chunk.
Definition big_endian :
bool :=
Archi.big_endian.
Lemma be_arch:
big_endian =
Archi.big_endian.
Proof.
reflexivity. Qed.
Global Opaque big_endian.
Lemma be_rew:
big_endian =
Archi.big_endian.
Proof.
Definition size_chunk (
chunk:
memory_chunk) :
Z :=
match chunk with
|
Mint8signed => 1
|
Mint8unsigned => 1
|
Mint16signed => 2
|
Mint16unsigned => 2
|
Mint32 => 4
|
Mint64 => 8
|
Mfloat32 => 4
|
Mfloat64 => 8
|
Many32 => 4
|
Many64 => 8
end.
Lemma size_chunk_pos:
forall chunk,
size_chunk chunk > 0.
Proof.
intros. destruct chunk; simpl; omega.
Qed.
Definition size_chunk_nat (
chunk:
memory_chunk) :
nat :=
nat_of_Z(
size_chunk chunk).
Lemma size_chunk_nat_sup_0:
forall chunk, (
size_chunk_nat chunk > 0)%
nat.
Proof.
Lemma size_chunk_conv:
forall chunk,
size_chunk chunk =
Z_of_nat (
size_chunk_nat chunk).
Proof.
intros. destruct chunk; reflexivity.
Qed.
Lemma size_chunk_nat_pos:
forall chunk,
exists n,
size_chunk_nat chunk =
S n.
Proof.
Memory reads and writes must respect alignment constraints:
the byte offset of the location being addressed should be an exact
multiple of the natural alignment for the chunk being addressed.
This natural alignment is defined by the following
align_chunk function. Some target architectures
(e.g. PowerPC and x86) have no alignment constraints, which we could
reflect by taking align_chunk chunk = 1. However, other architectures
have stronger alignment requirements. The following definition is
appropriate for PowerPC, ARM and x86.
Definition align_chunk (
chunk:
memory_chunk) :
Z :=
match chunk with
|
Mint8signed => 1
|
Mint8unsigned => 1
|
Mint16signed => 2
|
Mint16unsigned => 2
|
Mint32 => 4
|
Mint64 => 8
|
Mfloat32 => 4
|
Mfloat64 => 4
|
Many32 => 4
|
Many64 => 4
end.
Lemma align_chunk_pos:
forall chunk,
align_chunk chunk > 0.
Proof.
intro. destruct chunk; simpl; omega.
Qed.
Lemma align_size_chunk_divides:
forall chunk, (
align_chunk chunk |
size_chunk chunk).
Proof.
intros.
destruct chunk;
simpl;
try apply Zdivide_refl;
exists 2;
auto.
Qed.
Lemma align_le_divides:
forall chunk1 chunk2,
align_chunk chunk1 <=
align_chunk chunk2 -> (
align_chunk chunk1 |
align_chunk chunk2).
Proof.
intros.
destruct chunk1;
destruct chunk2;
simpl in *;
solve [
omegaContradiction
|
apply Zdivide_refl
|
exists 2;
reflexivity
|
exists 4;
reflexivity
|
exists 8;
reflexivity ].
Qed.
Inductive quantity :
Type :=
Q32 |
Q64.
Definition quantity_eq (
q1 q2:
quantity) : {
q1 =
q2} + {
q1 <>
q2}.
Proof.
decide equality. Defined.
Global Opaque quantity_eq.
Definition size_quantity_nat (
q:
quantity) :=
match q with Q32 => 4%
nat |
Q64 => 8%
nat end.
Lemma size_quantity_nat_pos:
forall q,
exists n,
size_quantity_nat q =
S n.
Proof.
intros. destruct q; [exists 3%nat | exists 7%nat]; auto.
Qed.
Memory values
A ``memory value'' is a byte-sized quantity that describes the current
content of a memory cell. With our new model, a memval can only be a
byte-sized fragment of an opaque symbolic expression;
Values stored in memory cells.
Inductive memval:
Type :=
|
Symbolic :
expr_sym ->
option styp ->
nat ->
memval.
We lift this equivalence to memvals.
Encoding and decoding integers
We define functions to convert between integers and lists of bytes
of a given length
Fixpoint bytes_of_int (
n:
nat) (
x:
Z) {
struct n}:
list byte :=
match n with
|
O =>
nil
|
S m =>
Byte.repr x ::
bytes_of_int m (
x / 256)
end.
Fixpoint int_of_bytes (
l:
list byte):
Z :=
match l with
|
nil => 0
|
b ::
l' =>
Byte.unsigned b +
int_of_bytes l' * 256
end.
Definition rev_if_be {
A:
Type} (
l:
list A) :
list A :=
if big_endian then List.rev l else l.
Lemma rev_if_be_nil:
forall A,
rev_if_be (
nil (
A:=
A)) = (
nil (
A:=
A)).
Proof.
Lemma rev_if_be_one:
forall {
A} (
a:
A),
rev_if_be (
a::
nil) =
a::
nil.
Proof.
Lemma in_rib:
forall {
A} (
a:
A)
l,
In a l ->
In a (
rev_if_be l).
Proof.
Lemma rev_rev_if_be_involutive:
forall {
A} (
l:
list A),
rev (
rev_if_be (
rev (
rev_if_be l))) =
l.
Proof.
Lemma revi_rev_revi:
forall A (
l:
list A),
rev_if_be (
rev (
rev_if_be l)) =
rev l.
Proof.
Lemma list_forall2_rib:
forall {
A} (
P:
A ->
A ->
Prop) (
l l':
list A),
list_forall2 P l l' ->
list_forall2 P (
rev_if_be l) (
rev_if_be l').
Proof.
Lemma list_forall2_rib_inv:
forall {
A} (
P:
A ->
A ->
Prop) (
l l':
list A),
list_forall2 P (
rev_if_be l) (
rev_if_be l') ->
list_forall2 P l l'.
Proof.
Lemma Exists_rev:
forall {
A} (
P:
A->
Prop) (
l:
list A),
Exists P l ->
Exists P (
rev l).
Proof.
Lemma Exists_rib:
forall {
A} (
P:
A->
Prop) (
l:
list A),
Exists P l ->
Exists P (
rev_if_be l).
Proof.
Lemma Exists_rib_inv:
forall {
A} (
P:
A->
Prop) (
l:
list A),
Exists P (
rev_if_be l) ->
Exists P l.
Proof.
Lemma Forall_rib:
forall {
A} (
P:
A ->
Prop) (
l:
list A),
Forall P l ->
Forall P (
rev_if_be l).
Proof.
Lemma map_rev_if_be:
forall {
A B} (
f:
A ->
B) (
l:
list A),
map f (
rev_if_be l) =
rev_if_be (
map f l).
Proof.
induction l;
simpl;
unfold rev_if_be in *;
destr.
rewrite map_app.
simpl.
rewrite IHl;
reflexivity.
Qed.
Lemma rev_rev_if_be:
forall {
A} (
l:
list A),
rev (
rev_if_be l) =
rev_if_be (
rev l).
Proof.
induction l;
simpl in *;
unfold rev_if_be in *;
destr.
Qed.
Definition encode_int (
sz:
nat) (
x:
Z) :
list byte :=
rev_if_be (
bytes_of_int sz x).
Definition decode_int (
b:
list byte) :
Z :=
int_of_bytes (
rev_if_be b).
Length properties
Lemma length_bytes_of_int:
forall n x,
length (
bytes_of_int n x) =
n.
Proof.
induction n; simpl; intros. auto. decEq. auto.
Qed.
Lemma rev_if_be_length:
forall (
A:
Type) (
l:
list A),
length (
rev_if_be l) =
length l.
Proof.
Lemma rev_if_be_involutive:
forall A (
l:
list A),
rev_if_be (
rev_if_be l) =
l.
Proof.
A length-n encoding depends only on the low 8*n bits of the integer.
Lemma bytes_of_int_mod:
forall n x y,
Int.eqmod (
two_p (
Z_of_nat n * 8))
x y ->
bytes_of_int n x =
bytes_of_int n y.
Proof.
Lemma encode_int_8_mod:
forall x y,
Int.eqmod (
two_p 8)
x y ->
encode_int 1%
nat x =
encode_int 1%
nat y.
Proof.
Lemma encode_int_16_mod:
forall x y,
Int.eqmod (
two_p 16)
x y ->
encode_int 2%
nat x =
encode_int 2%
nat y.
Proof.
Encoding and decoding values
Fixpoint inj_symbolic' (
n:
nat) (
e:
expr_sym)
t {
struct n}:
list memval :=
match n with
|
O =>
nil
|
S m =>
Symbolic e t m ::
inj_symbolic'
m e t
end.
Definition get_type (
e:
expr_sym) :
styp :=
if wt_expr_dec e Tint
then Tint
else if wt_expr_dec e Tfloat
then Tfloat
else if wt_expr_dec e Tsingle
then Tsingle
else if wt_expr_dec e Tlong
then Tlong
else Tint.
Lemma get_type_correct:
forall e,
wt_expr e (
get_type e) \/ ~
exists t,
wt_expr e t.
Proof.
unfold get_type;
repeat destr.
right;
intro;
dex.
des t.
Qed.
Definition inj_symbolic (
n:
nat) (
e:
expr_sym) (
t:
option styp) :
list memval :=
rev (
rev_if_be (
inj_symbolic'
n e t)).
Lemma inj_symbolic_length:
forall e t n,
length (
inj_symbolic n e t) =
n.
Proof.
Definition to_bits (
c:
memory_chunk) (
v:
expr_sym) :
expr_sym :=
match c with
|
Mfloat32 =>
Eunop (
OpConvert SEUnsigned (
Tlong,
SEUnsigned))
Tint
(
Eunop OpBitsofsingle Tsingle v)
|
Mfloat64 =>
Eunop OpBitsofdouble Tfloat v
|
Mint8signed
|
Mint8unsigned
|
Mint16signed
|
Mint16unsigned
|
Mint32 =>
Eunop (
OpConvert SEUnsigned (
Tlong,
SEUnsigned))
Tint v
|
Mint64 =>
v
|
Many32 =>
match get_type v with
Tsingle =>
Eunop (
OpConvert SEUnsigned (
Tlong,
SEUnsigned))
Tint (
Eunop OpBitsofsingle Tsingle v)
|
Tint =>
Eunop (
OpConvert SEUnsigned (
Tlong,
SEUnsigned))
Tint v
|
_ =>
Eval Vundef
end
|
Many64 =>
match get_type v with
Tfloat =>
Eunop OpBitsofdouble Tfloat v
|
Tsingle =>
Eunop (
OpConvert SEUnsigned (
Tlong,
SEUnsigned))
Tint (
Eunop OpBitsofsingle Tsingle v)
|
Tint =>
Eunop (
OpConvert SEUnsigned (
Tlong,
SEUnsigned))
Tint v
|
Tlong =>
v
end
end.
Lemma same_eval_nwt_vundef:
forall v1 v2 t
(
WT:
wt_expr v1 t)
(
NWT: ~
wt_expr v2 t)
(
SE:
same_eval v1 v2)
alloc em,
eSexpr alloc em v1 =
Vundef /\
eSexpr alloc em v2 =
Vundef.
Proof.
intros.
cut (
eSexpr alloc em v2 =
Vundef).
split;
auto.
rewrite SE;
auto.
eapply expr_type';
eauto.
rewrite <-
SE.
apply expr_type;
auto.
Qed.
Lemma get_type_correct_not_int:
forall e,
get_type e <>
Tint ->
wt_expr e Tint ->
False.
Proof.
intros.
unfold get_type in *;
repeat (
revert H;
destr).
Qed.
Lemma to_bits_same_eval:
forall v v'
chunk,
same_eval v v' ->
same_eval (
to_bits chunk v) (
to_bits chunk v').
Proof.
Definition encode_val (
chunk:
memory_chunk) (
v:
expr_sym) :
list memval :=
inj_symbolic (
size_chunk_nat chunk) (
to_bits chunk v)
(
match chunk with Many32|
Many64 =>
Some (
get_type v)
|
_ =>
None end).
Lemma encode_val_length:
forall chunk v ,
length (
encode_val chunk v) =
size_chunk_nat chunk.
Proof.
get_nth_part e n t extracts the nth byte of expression e of type t
Fixpoint get_nth_part (
e:
expr_sym) (
n:
nat) :=
match n with
O =>
Ebinop OpAnd Tlong Tlong e (
Eval (
Vlong (
Int64.repr 255)))
|
S m =>
get_nth_part (
Ebinop (
OpShr SEUnsigned)
Tlong Tint e (
Eval (
Vint (
Int.repr 8))))
m
end.
Lemma gnp_eSexpr:
forall n e f,
same_eval e f ->
same_eval (
get_nth_part e n) (
get_nth_part f n).
Proof.
induction n; red; simpl; intros.
rewrite H; auto.
apply IHn; auto.
red; simpl; intros.
rewrite H; auto.
Qed.
Fixpoint get_nth_part_val (
v:
val) (
n:
nat) :
val :=
match v with
Vlong i =>
match n with
O =>
Vlong (
Int64.and i (
Int64.repr 255))
|
S m =>
get_nth_part_val (
Vlong (
Int64.shru i (
Int64.repr 8)))
m
end
|
_ =>
Vundef
end.
Lemma gnp_rew:
forall alloc em n e,
eSexpr alloc em (
get_nth_part e n) =
get_nth_part_val (
eSexpr alloc em e)
n.
Proof.
induction n; simpl; intros.
- destr.
- rewrite IHn; simpl; auto. destr; des n.
Qed.
Lemma get_nth_part_bnds:
forall n i j l,
j >= 8 ->
get_nth_part_val i n =
Vlong l ->
Int64.testbit l j =
false.
Proof.
Lemma get_nth_part_val_le:
forall n i l,
get_nth_part_val i n =
Vlong l ->
0 <=
Int64.unsigned l <= 255.
Proof.
expr_of_memval transforms a memval into the corresponding expr_sym.
Definition expr_of_memval (
m:
memval) :
expr_sym :=
match m with
|
Symbolic e t n =>
get_nth_part e n
end.
Lemma expr_of_memval_bound:
forall alloc em mv l,
eSexpr alloc em (
expr_of_memval mv) =
Vlong l ->
Int64.unsigned l < 256.
Proof.
Lemma nth_error_property:
forall {
A:
Type} {
P:
A ->
A ->
Prop}
l l'
(
LF:
list_forall2 P l l')
n a b,
nth_error l n =
Some a ->
nth_error l'
n =
Some b ->
P a b.
Proof.
induction 1; simpl; intros.
destruct n; simpl in H; discriminate.
destruct n; simpl in *.
- inv H0; inv H1; auto.
- apply IHLF with (n:=n); auto.
Qed.
proj_symbolic_aux_le transforms a list of memval into the
corresponding symbolic expression, interpreting vl as a little-endian sorted
list.
Fixpoint proj_symbolic_aux_le (
vl:
list memval) :
expr_sym :=
match vl with
nil =>
Eval (
Vlong Int64.zero)
|
a ::
r =>
Ebinop OpAdd Tlong Tlong
(
expr_of_memval a)
(
Ebinop OpShl Tlong Tint
(
proj_symbolic_aux_le r)
(
Eval (
Vint (
Int.repr 8))))
end.
Lemma psa_wt_expr:
forall alloc em l,
wt_val (
eSexpr alloc em (
proj_symbolic_aux_le l))
Tlong.
Proof.
induction l; simpl; intros; auto.
seval.
Qed.
Lemma psa_le_app_rew:
forall l1 l2,
same_eval (
proj_symbolic_aux_le (
l1 ++
l2))
(
Val.addl
(
proj_symbolic_aux_le l1)
(
Val.mull
(
proj_symbolic_aux_le l2)
(
Eval (
Vlong (
Int64.repr (256^
Z.of_nat (
length l1))))))).
Proof.
Lemma psa_le_n_bnds:
forall l n,
(
length l <=
n)%
nat ->
forall alloc em i,
eSexpr alloc em (
proj_symbolic_aux_le l) =
Vlong i ->
Int64.unsigned i < 256 ^ (
Z.of_nat n).
Proof.
Lemma psa_le_app:
forall l1 l2,
length l1 = 4%
nat ->
length l2 = 4%
nat ->
same_eval (
proj_symbolic_aux_le (
l1 ++
l2))
(
Val.longofwords
(
Val.loword (
proj_symbolic_aux_le l2))
(
Val.loword (
proj_symbolic_aux_le l1))).
Proof.
proj_symbolic_le transforms a list of memval vl into the corresponding
symbolic expression, reversing the list if we are on big-endian architecture.
Definition proj_symbolic_le (
vl:
list memval) :
expr_sym :=
proj_symbolic_aux_le (
rev_if_be vl).
Definition type_of_list_memval (
vl:
list memval) :
option styp :=
match vl with
| (
Symbolic e (
Some t)
n)::
r =>
Some t
|
_ =>
None
end.
decode_val adds a cast around the result of proj_symbolic_le, and
finalizes the decoding of a list of memval.
Definition from_bits chunk e vl :=
match chunk with
|
Mint8signed =>
Eunop (
OpSignext 8)
Tint (
Val.loword e)
|
Mint8unsigned =>
Eunop (
OpZeroext 8)
Tint (
Val.loword e)
|
Mint16signed =>
Eunop (
OpSignext 16)
Tint (
Val.loword e)
|
Mint16unsigned =>
Eunop (
OpZeroext 16)
Tint (
Val.loword e)
|
Mint32 => (
Val.loword e)
|
Mint64 =>
Eunop (
OpSignext 64)
Tlong e
|
Mfloat32 =>
Eunop OpSingleofbits Tint (
Val.loword e)
|
Mfloat64 =>
Eunop OpDoubleofbits Tlong e
|
Many64 =>
match type_of_list_memval vl with
Some Tint =>
Eunop (
OpConvert SEUnsigned (
Tint,
SEUnsigned))
Tlong e
|
Some Tfloat =>
Eunop OpDoubleofbits Tlong e
|
Some Tsingle =>
Eunop OpSingleofbits Tint
(
Eunop (
OpConvert SEUnsigned (
Tint,
SEUnsigned))
Tlong e)
|
Some Tlong =>
e
|
None =>
Eval Vundef
end
|
Many32 =>
match type_of_list_memval vl with
Some Tint =>
Eunop (
OpConvert SEUnsigned (
Tint,
SEUnsigned))
Tlong e
|
Some Tsingle =>
Eunop OpSingleofbits Tint
(
Eunop (
OpConvert SEUnsigned (
Tint,
SEUnsigned))
Tlong e)
|
_ =>
Eval Vundef
end
end.
Definition decode_val (
chunk:
memory_chunk) (
vl:
list memval) :
expr_sym :=
from_bits chunk (
proj_symbolic_le vl)
vl.
Lemma gnp_wt:
forall n e,
weak_wt (
get_nth_part e n)
Tlong.
Proof.
induction n;
simpl;
intros;
auto.
destruct (
wt_expr_dec e Tlong);
simpl;
auto.
left;
repeat split;
auto;
constructor.
right.
intro.
destruct H as [
t [
A B]].
congruence.
Qed.
Lemma eom_wt:
forall l,
weak_wt (
expr_of_memval l)
Tlong.
Proof.
Lemma psa_wt:
forall l,
weak_wt (
proj_symbolic_aux_le l)
Tlong.
Proof.
induction l;
simpl;
intros;
auto.
red;
simpl;
auto.
destruct (
eom_wt a).
-
destruct IHl.
+
left;
repeat split;
auto;
constructor.
+
right;
intro A;
destruct A as [
t [
A [[
B D]
C]]].
elim H0;
exists Tlong;
auto.
-
right;
intro A;
destruct A as [
t [
A [[
B D]
C]]].
elim H;
exists Tlong;
auto.
Qed.
Lemma ps_wt:
forall l,
weak_wt (
proj_symbolic_le l)
Tlong.
Proof.
Definition wt e t := (
exists t',
wt_expr e (
styp_of_ast t') /\
subtype t'
t =
true)
\/ ~
exists t,
wt_expr e t.
Lemma subtype_refl:
forall t,
subtype t t =
true.
Proof.
intros. des t.
Qed.
Lemma weak_wt_wt':
forall e t,
weak_wt e (
styp_of_ast t) ->
wt e t.
Proof.
intros e t [
A|
A].
left;
eexists;
split;
eauto;
try apply subtype_refl.
red;
auto.
Qed.
Lemma gnp_wt':
forall n e,
wt (
get_nth_part e n)
AST.Tlong.
Proof.
intros.
apply weak_wt_wt'.
apply gnp_wt.
Qed.
Lemma eom_wt':
forall l,
wt (
expr_of_memval l)
AST.Tlong.
Proof.
intros.
apply weak_wt_wt'.
apply eom_wt.
Qed.
Lemma psa_wt':
forall l,
wt (
proj_symbolic_aux_le l)
AST.Tlong.
Proof.
intros.
apply weak_wt_wt'.
apply psa_wt.
Qed.
Lemma ps_wt':
forall l,
wt (
proj_symbolic_le l)
AST.Tlong.
Proof.
intros.
apply weak_wt_wt'.
apply ps_wt.
Qed.
Lemma decode_val_type:
forall l chunk,
wt (
decode_val chunk l) (
type_of_chunk chunk).
Proof.
intros.
destruct (
ps_wt'
l)
as [[
t [
A B]]|
A].
-
des t.
des chunk;
try (
red;
left;
eexists;
split;
try apply subtype_refl;
simpl;
destr;
try constructor;
fail).
+
destr.
*
red;
simpl;
left.
destr.
exists AST.Tint;
destr.
exists AST.Tint;
destr.
exists AST.Tint;
destr.
exists AST.Tsingle;
destr.
*
red;
left;
eexists;
split;
eauto;
try apply subtype_refl;
simpl;
auto.
+
destr.
2:
red;
left;
eexists;
split;
eauto;
try apply subtype_refl;
destr.
red;
simpl;
left.
destr.
exists AST.Tint;
destr.
exists AST.Tlong;
destr.
exists AST.Tfloat;
destr.
exists AST.Tsingle;
destr.
-
des chunk;
repeat destr;
try (
right;
intro;
dex;
destr;
apply A;
eexists;
eauto;
fail);
left;
eexists;
split;
eauto;
try apply subtype_refl;
simpl;
auto.
Qed.
Definition is_se_or_ld R :=
R =
same_eval \/
R =
Val.lessdef.
Record wf_mr (
mr:
expr_sym ->
expr_sym ->
Prop) :=
{
mr_refl:
forall x,
mr x x;
mr_unop:
forall u t a b
(
MR:
mr a b),
mr (
Eunop u t a) (
Eunop u t b);
mr_binop:
forall bi t t'
a b c d
(
MR1:
mr a b)
(
MR2:
mr c d),
mr (
Ebinop bi t t'
a c) (
Ebinop bi t t'
b d);
mr_val_refl:
forall v1 v2
(
REL:
mr (
Eval v1) (
Eval v2))
(
NU:
v1 <>
Vundef),
v1 =
v2;
mr_same_eval:
forall v1 v2,
same_eval v1 v2 ->
mr v1 v2;
mr_closed_se:
forall v1 v2 v3 v4,
same_eval v1 v2 ->
same_eval v3 v4 ->
mr v1 v3 ->
mr v2 v4;
mr_se_or_ld:
is_se_or_ld mr
}.
Lemma add_one_zero_diff:
forall i i0,
i =
Int.add Int.one i0 ->
i =
Int.add Int.zero i0 ->
False.
Proof.
Lemma wf_mr_se:
wf_mr same_eval.
Proof.
Lemma wf_mr_ld:
wf_mr Val.lessdef.
Proof.
Section MemvalRel.
Variable mr:
expr_sym ->
expr_sym ->
Prop.
Hypothesis WF:
wf_mr mr.
Definition same_type_memval m1 m2 :=
match m1,
m2 with
Symbolic e t n,
Symbolic e'
t'
n' =>
t =
t'
end.
Definition memval_rel :
memval ->
memval ->
Prop :=
fun m1 m2 =>
mr (
expr_of_memval m1) (
expr_of_memval m2)
/\ (
same_type_memval m1 m2
\/
same_eval (
Eval Vundef) (
expr_of_memval m1))
.
Lemma memval_equiv_expr_of_memval:
forall a b,
memval_rel a b ->
mr (
expr_of_memval a) (
expr_of_memval b).
Proof.
intros.
apply H.
Qed.
Lemma psa_eSexpr:
forall v v',
list_forall2 memval_rel v v' ->
mr (
proj_symbolic_aux_le v)
(
proj_symbolic_aux_le v').
Proof.
inv WF.
induction 1;
simpl;
intros;
auto.
destruct H;
auto.
Qed.
Lemma psa_le_spec:
forall l l',
list_forall2 memval_rel l l' ->
mr (
proj_symbolic_aux_le l)
(
proj_symbolic_aux_le l').
Proof.
inv WF.
induction 1;
simpl;
intros;
auto.
destruct H;
auto.
Qed.
Lemma ps_eSexpr:
forall v v',
list_forall2 memval_rel v v' ->
mr (
proj_symbolic_le v) (
proj_symbolic_le v').
Proof.
Lemma memval_rel_type_of_ml:
forall v v',
list_forall2 memval_rel v v' ->
type_of_list_memval v =
type_of_list_memval v'
\/
(
exists h,
Some h =
head v /\
same_eval (
Eval Vundef) (
expr_of_memval h)
).
Proof.
induction 1.
-
destr.
-
destr;
dex;
destr.
+
des H.
repeat destr.
right;
exists (
Symbolic e o n);
destr.
+
subst.
inv H.
des H4.
repeat destr.
right;
exists (
Symbolic e o n);
destr.
Qed.
Lemma in_same_undef_psa_undef:
forall vl m,
In m vl ->
same_eval (
Eval Vundef) (
expr_of_memval m) ->
same_eval (
Eval Vundef) (
proj_symbolic_aux_le vl).
Proof.
induction vl; simpl; intros. easy.
red; intros; destr. subst. rewrite <- H0. destr.
rewrite <- (IHvl _ H1 H0). destr. seval.
Qed.
Lemma hd_error_in:
forall A l (
x:
A),
hd_error l =
Some x ->
In x l.
Proof.
induction l; simpl; intros; inv H; auto.
Qed.
Lemma lessdef_vundef:
forall v,
Val.lessdef (
Eval Vundef)
v.
Proof.
red; intros; auto.
Qed.
Lemma decode_val_spec:
forall l l',
list_forall2 memval_rel l l' ->
forall c,
mr (
decode_val c l) (
decode_val c l').
Proof.
Lemma decode_val_eSexpr:
forall chunk v v',
list_forall2 memval_rel v v' ->
mr (
decode_val chunk v) (
decode_val chunk v').
Proof.
End MemvalRel.
Definition decode_encode_expr_sym (
v1:
expr_sym) (
chunk1 chunk2:
memory_chunk) (
v2:
expr_sym) :
Prop :=
match chunk1,
chunk2 with
| (
Mint8signed|
Mint8unsigned),
Mint8signed =>
same_eval v2 (
Eunop (
OpSignext 8)
Tint v1)
| (
Mint8signed|
Mint8unsigned),
Mint8unsigned =>
same_eval v2 (
Eunop (
OpZeroext 8)
Tint v1)
| (
Mint16signed|
Mint16unsigned),
Mint16signed =>
same_eval v2 (
Eunop (
OpSignext 16)
Tint v1)
| (
Mint16signed|
Mint16unsigned),
Mint16unsigned =>
same_eval v2 (
Eunop (
OpZeroext 16)
Tint v1)
|
Mint32,
Mint32 =>
same_eval v2 (
Eunop (
OpSignext 32)
Tint v1)
|
Mint32,
Mfloat32 =>
same_eval v2 (
Eunop OpSingleofbits Tint v1)
|
Mfloat32,
Mint32 =>
same_eval v2 (
Eunop OpBitsofsingle Tsingle v1)
|
Mfloat32,
Mfloat32 =>
same_eval v2 (
Eunop (
OpConvert SESigned (
Tsingle,
SESigned))
Tsingle v1)
|
Mint64,
Mint64 =>
same_eval v2 (
Eunop (
OpSignext 64)
Tlong v1)
|
Mint64,
Mfloat64 =>
same_eval v2 (
Eunop OpDoubleofbits Tlong v1)
|
Mfloat64,
Mint64 =>
same_eval v2 (
Eunop OpBitsofdouble Tfloat v1)
|
Mfloat64,
Mfloat64 =>
same_eval v2 (
Eunop (
OpConvert SESigned (
Tfloat,
SESigned))
Tfloat v1)
|
Many32,
Many32 =>
match get_type v1 with
Tint =>
same_eval v2 v1
|
Tsingle =>
same_eval v2 v1
|
_ =>
same_eval v2 (
Eval Vundef)
end
|
Many32,
Mint32 =>
match get_type v1 with
|
Tint =>
same_eval v2 (
Eunop (
OpSignext 32)
Tint v1)
|
_ =>
True
end
|
Many64,
Many64 =>
same_eval v2 v1
|
_,
_ =>
True
end.
Ltac simpl_int :=
match goal with
| |-
context [
Int.eq ?
a ?
a] =>
rewrite Int.eq_true;
simpl;
simpl_int
| |-
context [
Int.eq ?
a ?
b] =>
replace (
Int.eq a b)
with false by reflexivity;
simpl;
simpl_int
| |-
context [
Int.ltu ?
a ?
b] =>
try replace (
Int.ltu a b)
with true by reflexivity;
simpl;
simpl_int
|
_ =>
progress simpl;
simpl_int
|
_ =>
idtac
end.
Ltac rew_shru_64:=
repeat match goal with
|-
context[
Int64.shru
(
Int64.shru ?
a ?
i) (
Int64.repr ?
i')] =>
rewrite Int64.shru_shru;
auto
end.
Lemma decode_encode_val_general:
forall v chunk1 chunk2,
decode_encode_expr_sym v chunk1 chunk2 (
decode_val chunk2 (
encode_val chunk1 v)).
Proof.
Lemma encode_val_int8_signed_unsigned:
forall v,
encode_val Mint8signed v =
encode_val Mint8unsigned v.
Proof.
intros.
destruct v; simpl; auto.
Qed.
Lemma encode_val_int16_signed_unsigned:
forall v,
encode_val Mint16signed v =
encode_val Mint16unsigned v.
Proof.
intros. destruct v; simpl; auto.
Qed.
Definition memval_equiv :=
memval_rel same_eval.
Lemma encode_val_int8_zero_ext:
forall mr (
wf:
wf_mr mr)
n,
list_forall2
(
memval_rel mr)
(
encode_val Mint8unsigned (
Eval (
Vint (
Int.zero_ext 8
n))))
(
encode_val Mint8unsigned (
Eval (
Vint n))).
Proof.
Lemma encode_val_int8_sign_ext:
forall mr (
wf:
wf_mr mr)
n,
list_forall2
(
memval_rel mr)
(
encode_val Mint8unsigned (
Eval (
Vint (
Int.sign_ext 8
n))))
(
encode_val Mint8unsigned (
Eval (
Vint n))).
Proof.
Lemma encode_val_int16_zero_ext:
forall mr (
wf:
wf_mr mr)
n,
list_forall2
(
memval_rel mr)
(
encode_val Mint16unsigned (
Eval (
Vint (
Int.zero_ext 16
n))))
(
encode_val Mint16unsigned (
Eval (
Vint n))).
Proof.
Lemma encode_val_int16_sign_ext:
forall mr (
wf:
wf_mr mr)
n,
list_forall2
(
memval_rel mr)
(
encode_val Mint16unsigned (
Eval (
Vint (
Int.sign_ext 16
n))))
(
encode_val Mint16unsigned (
Eval (
Vint n))).
Proof.
Definition memval_lessdef :
memval ->
memval ->
Prop :=
memval_rel Val.lessdef.
Lemma decode_val_cast:
forall chunk l,
length l =
size_chunk_nat chunk ->
let v:=
decode_val chunk l in
match chunk with
|
Mint8signed =>
same_eval v (
Val.sign_ext 8
v)
|
Mint8unsigned =>
same_eval v (
Val.zero_ext 8
v)
|
Mint16signed =>
same_eval v (
Val.sign_ext 16
v)
|
Mint16unsigned =>
same_eval v (
Val.zero_ext 16
v)
|
_ =>
True
end.
Proof.
Compatibility with memory injections
Relating two memory values according to a memory injection.
Lemma decode_val_info:
forall c n,
let v2 :=
proj_symbolic_aux_le (
rev_if_be n)
in
same_eval
(
decode_val c n)
match c with
|
Mint32 =>
Val.loword v2
|
Mint64 =>
Eunop (
OpSignext 64)
Tlong v2
|
_ =>
decode_val c n
end.
Proof.
Breaking 64-bit memory accesses into two 32-bit accesses
Lemma decode_val_int64:
forall l1 l2,
length l1 = 4%
nat ->
length l2 = 4%
nat ->
same_eval (
decode_val Mint64 (
l1 ++
l2))
(
Val.longofwords
(
decode_val Mint32 (
if big_endian then l1 else l2))
(
decode_val Mint32 (
if big_endian then l2 else l1))).
Proof.
Lemma gnpv_hi:
forall n i,
get_nth_part_val (
Vlong (
Int64.repr (
Int.unsigned (
Int64.hiword i))))
n =
get_nth_part_val (
Vlong i) (
n + 4).
Proof.
Lemma gnpv_lo:
forall n i,
(
n <= 3)%
nat ->
get_nth_part_val (
Vlong (
Int64.repr (
Int.unsigned (
Int64.loword i))))
n =
get_nth_part_val (
Vlong i)
n.
Proof.
Lemma memval_equiv_hiword:
forall n v t,
memval_equiv
(
Symbolic
(
Eunop (
OpConvert SEUnsigned (
Tlong,
SEUnsigned))
Tint (
Val.hiword v))
t n) (
Symbolic v t (
plus n 4)).
Proof.
Lemma memval_equiv_loword:
forall n (
n_bounds: (
n <= 3)%
nat)
v,
memval_equiv
(
Symbolic
(
Eunop (
OpConvert SEUnsigned (
Tlong,
SEUnsigned))
Tint (
Val.loword v))
None n) (
Symbolic v None n).
Proof.
Lemma rib_app:
forall A B (
l1 l2:
A) (
f :
A ->
list B),
rev_if_be (
f (
if big_endian then l1 else l2))
++
rev_if_be (
f (
if big_endian then l2 else l1)) =
rev_if_be ((
f l2) ++ (
f l1)).
Proof.
Definition same_type a1 a2 :
Prop :=
forall t,
wt_expr a2 t ->
wt_expr a1 t.
Lemma encode_val_int64:
forall v,
same_eval (
decode_val Mint64 (
encode_val Mint64 v))
(
decode_val
Mint64
((
encode_val
Mint32
(
if big_endian then Val.hiword v else Val.loword v))
++
(
encode_val
Mint32
(
if big_endian then Val.loword v else Val.hiword v)))).
Proof.
Lemma expr_inject_unop:
forall f e e'
u t,
Val.expr_inject f e e' ->
Val.expr_inject f (
Eunop u t e) (
Eunop u t e').
Proof.
Lemma expr_inject_binop:
forall f e e'
e1 e1'
b t1 t2,
Val.expr_inject f e e' ->
Val.expr_inject f e1 e1' ->
Val.expr_inject f (
Ebinop b t1 t2 e e1) (
Ebinop b t1 t2 e'
e1').
Proof.
Definition impl_vi (
ei:
meminj ->
expr_sym ->
expr_sym ->
Prop) :=
forall f v1 v2,
ei f (
Eval v1) (
Eval v2) ->
val_inject f v1 v2.
Lemma impl_vi_ei:
impl_vi Val.expr_inject.
Proof.
red; intros.
inv H.
des v1; auto; inv inj_ok; auto.
simp H0. des p; inv H1. econstructor; eauto.
Qed.
Fixpoint block_appears (
e:
expr_sym) (
b:
block) :
Prop :=
match e with
Eval (
Vptr bb i) =>
b =
bb
|
Eval _ =>
False
|
Eundef _ _ =>
False
|
Eunop _ _ e =>
block_appears e b
|
Ebinop _ _ _ e1 e2 =>
block_appears e1 b \/
block_appears e2 b
end.
Lemma nba_se:
forall a b,
~
block_appears a b ->
forall cm cm'
em,
(
forall bb,
bb <>
b ->
cm bb =
cm'
bb) ->
eSexpr cm em a =
eSexpr cm'
em a.
Proof.
induction a; simpl; intros; eauto.
- des v.
rewrite H0; auto.
- erewrite IHa; eauto.
- erewrite IHa1; eauto.
erewrite IHa2; eauto.
Qed.
Lemma block_appears_dec:
forall b a, {
block_appears a b} + {~
block_appears a b}.
Proof.
induction a;
simpl;
intros;
eauto.
-
des v.
des (
peq b b0);
auto.
-
destruct IHa1;
destruct IHa2;
auto.
right;
auto.
intros [
A |
A ];
congruence.
Qed.
Lemma ptr_se_block_appears:
forall a b i
(
SE:
same_eval (
Eval (
Vptr b i))
a),
block_appears a b.
Proof.
Lemma apply_inj_none:
forall f a b,
block_appears a b ->
f b =
None ->
Val.apply_inj f a =
None.
Proof.
induction a;
simpl;
intros;
eauto.
-
des v.
unfold Val.inj_ptr;
rewrite H0;
auto.
-
intuition.
-
erewrite IHa;
eauto.
-
destruct H; [
erewrite IHa1|
erewrite IHa2];
eauto.
des (
Val.apply_inj f a1).
Qed.
Lemma impl_vi_ei':
impl_vi expr_inject'.
Proof.
Definition ei_ld (
ei:
meminj ->
expr_sym ->
expr_sym ->
Prop) :
Prop :=
forall f cm em e1 e1',
ei f e1 e1' ->
Values.Val.lessdef (
eSexpr (
Val.inj_alloc cm f) (
Val.inj_em em f)
e1)
(
eSexpr cm em e1').
Lemma ei_ld_ei:
ei_ld Val.expr_inject.
Proof.
Lemma ei_ld_ei':
ei_ld expr_inject'.
Proof.
Definition cm_inj (
al:
mem) (
f:
meminj) (
al':
mem) :=
forall b b'
delta
(
FB:
f b =
Some (
b',
delta)),
al'
b =
Int.add (
al b') (
Int.repr delta).
Example cm_inj_inj_alloc:
forall f al,
cm_inj al f (
Val.inj_alloc al f).
Proof.
Definition em_inj (
em:
block ->
int ->
byte) (
f:
meminj) (
em':
block ->
int ->
byte) :=
forall b b'
delta
(
FB:
f b =
Some (
b',
delta))
i,
em'
b i =
em b' (
Int.add i (
Int.repr delta)).
Example em_inj_inj_em:
forall f em,
em_inj em f (
Val.inj_em em f).
Proof.
red;
intros.
unfold Val.inj_em.
rewrite FB.
auto.
Qed.
Definition same_eval_inj (
f:
meminj) (
e1 e2:
expr_sym) :=
forall al em al'
em'
(
IA:
cm_inj al f al')
(
IE:
em_inj em f em'),
(
eSexpr al'
em'
e1) = (
eSexpr al'
em'
e2).
Definition wf_ei_typ ei :=
forall (
f:
meminj)
a b,
ei f a b ->
same_eval_inj f a (
Eval Vundef) \/ (
forall t,
wt_expr a t <->
wt_expr b t).
Definition ei_ld'
ei :=
forall f e1 e1'
(
EI:
ei f e1 e1')
cm em cm'
em'
(
ai:
cm_inj cm f cm')
(
ie:
em_inj em f em'),
Values.Val.lessdef (
eSexpr cm'
em'
e1) (
eSexpr cm em e1').
Definition wf_inj_refl ei :=
forall f sv v,
same_eval sv (
Eval v) ->
match v with
Vptr b _ =>
f b =
Some (
b,0)
|
_ =>
True
end ->
ei f sv sv.
Record wf_inj (
ei :
meminj ->
expr_sym ->
expr_sym ->
Prop) :
Prop :=
{
ei_inj_incr:
Val.inj_incr_compat ei;
ei_unop:
forall f u t a b
(
EI:
ei f a b),
ei f (
Eunop u t a) (
Eunop u t b);
ei_binop:
forall f bi t t'
a b c d
(
EI1:
ei f a b)
(
EI2:
ei f c d),
ei f (
Ebinop bi t t'
a c) (
Ebinop bi t t'
b d);
ei_val:
forall f v
(
VINJ:
val_inject f v v),
ei f (
Eval v) (
Eval v);
vi_ei:
forall f v v',
Val.apply_inj f v =
Some v' ->
ei f v v';
ei_ld'
_expr:
ei_ld'
ei;
wf_inj_undef:
forall f v v',
same_eval_inj f v (
Eval Vundef) ->
ei f v v'
;
wf_typ:
wf_ei_typ ei;
wf_ir:
wf_inj_refl ei
}.
Lemma ei_ld_expr:
forall ei (
WF:
wf_inj ei),
ei_ld ei.
Proof.
Inductive expr_inj (
f:
meminj) :
expr_sym ->
expr_sym ->
Prop :=
|
expr_inj_vundef:
forall v,
expr_inj f (
Eval Vundef)
v
|
expr_inj_val:
forall v1 v2 (
VI:
val_inject f v1 v2),
expr_inj f (
Eval v1) (
Eval v2)
|
expr_inj_undef:
forall b b0 i z (
FB:
f b =
Some (
b0,
z)),
expr_inj f (
Eundef b i) (
Eundef b0 (
Int.add i (
Int.repr z)))
|
expr_inj_unop:
forall e1 e2 u t (
EI:
expr_inj f e1 e2),
expr_inj f (
Eunop u t e1) (
Eunop u t e2)
|
expr_inj_binop:
forall e1 e2 f1 f2 b t1 t2 (
EI1:
expr_inj f e1 e2) (
EI2:
expr_inj f f1 f2),
expr_inj f (
Ebinop b t1 t2 e1 f1) (
Ebinop b t1 t2 e2 f2).
Lemma expr_inj_incr:
Val.inj_incr_compat expr_inj.
Proof.
red;
intros.
revert e1 e2 EI.
induction 1;
constructor;
auto.
eapply val_inject_incr;
eauto.
Qed.
Lemma expr_inj_ld:
forall (
f :
meminj) (
e1 e1' :
expr_sym)
(
ei:
expr_inj f e1 e1')
(
cm :
block ->
int) (
em :
block ->
int ->
byte),
Values.Val.lessdef
(
eSexpr (
Val.inj_alloc cm f) (
Val.inj_em em f)
e1)
(
eSexpr cm em e1').
Proof.
Definition binrelexpr :=
expr_sym ->
expr_sym ->
Prop.
Definition close (
R:
binrelexpr) (
P Q:
binrelexpr) :
binrelexpr :=
fun a b =>
exists a'
b',
P a a' /\
Q b b' /\
R a'
b'.
Definition expr_inj_se f :=
close (
expr_inj f) (
same_eval_inj f)
same_eval.
Lemma wf_inj_refl_expr_inj_se:
wf_inj_refl expr_inj_se.
Proof.
red;
intros.
exists (
Eval v), (
Eval v);
repSplit;
auto.
red;
intros;
rewrite H;
auto.
constructor.
des v;
econstructor;
eauto.
rewrite Int.add_zero;
auto.
Qed.
Lemma cm_inj_incr:
forall al f f'
al'
(
IA:
cm_inj al f'
al')
(
INCR:
inject_incr f f'),
cm_inj al f al'.
Proof.
red; intros.
apply IA.
apply INCR. auto.
Qed.
Lemma em_inj_incr:
forall al f f'
al'
(
EI:
em_inj al f'
al')
(
INCR:
inject_incr f f'),
em_inj al f al'.
Proof.
red; intros.
apply EI.
apply INCR. auto.
Qed.
Lemma same_eval_inj_incr:
forall f f' (
INCR:
inject_incr f f')
a b (
SEI:
same_eval_inj f a b),
same_eval_inj f'
a b.
Proof.
Lemma unop_same_eval_inj:
forall f u t e1 e2,
same_eval_inj f e1 e2 ->
same_eval_inj f (
Eunop u t e1) (
Eunop u t e2).
Proof.
red; intros.
generalize (H _ _ _ _ IA IE).
simpl.
intro A; inv A. auto.
Qed.
Lemma binop_same_eval_inj:
forall f b t1 t2 e1 e2 e3 e4,
same_eval_inj f e1 e2 ->
same_eval_inj f e3 e4 ->
same_eval_inj f (
Ebinop b t1 t2 e1 e3) (
Ebinop b t1 t2 e2 e4).
Proof.
red; intros; simpl.
f_equal.
generalize (H _ _ _ _ IA IE).
generalize (H0 _ _ _ _ IA IE).
intros A B.
inv A. inv B.
auto.
eapply H0; eauto.
Qed.
Lemma sei_sym:
forall f a b,
same_eval_inj f a b ->
same_eval_inj f b a.
Proof.
red; intros.
symmetry; eapply H; eauto.
Qed.
Instance same_eval_inj_equi :
forall f,
RelationClasses.PreOrder (
same_eval_inj f).
Proof.
constructor.
red; red; intros; auto.
red; red; intros.
erewrite H; eauto.
Qed.
Lemma expr_inj_type:
forall f a b,
expr_inj f a b ->
same_eval a (
Eval Vundef) \/ (
forall t,
wt_expr a t <->
wt_expr b t).
Proof.
induction 1;
simpl;
intros;
auto.
-
left;
reflexivity.
-
inv VI;
auto;
try (
right;
intros;
des (
t:
styp);
fail).
left;
reflexivity.
-
destr.
-
destr;
subst.
left;
red;
intros;
simpl;
rewrite H0;
destr.
rewrite fun_of_unop_undef;
auto.
right;
intros.
rewrite H0.
tauto.
-
destruct IHexpr_inj1.
left;
red;
intros;
simpl;
rewrite H1.
apply fun_of_binop_undef_l.
destruct IHexpr_inj2.
left;
red;
intros;
simpl;
rewrite H2.
apply fun_of_binop_undef_r.
right;
intros.
rewrite H1,
H2.
tauto.
Qed.
Lemma expr_inj_type':
forall f a b,
expr_inj f a b ->
same_eval_inj f a (
Eval Vundef) \/ (
forall t,
wt_expr a t <->
wt_expr b t).
Proof.
induction 1;
simpl;
intros;
auto.
-
left;
reflexivity.
-
inv VI;
auto;
try (
right;
intros;
des (
t:
styp);
fail).
left;
reflexivity.
-
destr.
-
destr;
subst.
left;
red;
intros;
simpl.
exploit H0;
eauto.
intros A;
inv A;
auto;
try rewrite H2;
rewrite fun_of_unop_undef;
auto.
right;
intros.
rewrite H0.
tauto.
-
destruct IHexpr_inj1.
left;
red;
intros;
simpl;
exploit H1;
eauto.
intros A;
inv A;
auto;
try rewrite H3;
rewrite fun_of_binop_undef_l;
auto.
destruct IHexpr_inj2.
left;
red;
intros;
simpl;
exploit H2;
eauto.
intros A;
inv A;
auto;
try rewrite H4;
rewrite fun_of_binop_undef_r;
auto.
right;
intros.
rewrite H1,
H2.
tauto.
Qed.
Lemma get_type_same_type:
forall a b,
(
forall t,
wt_expr a t <->
wt_expr b t) ->
get_type a =
get_type b.
Proof.
unfold get_type;
repeat destr_no_dep;
rewrite H in *;
destr.
Qed.
Lemma expr_inj_get_type:
forall f a b,
expr_inj f a b ->
same_eval a (
Eval Vundef) \/
get_type a =
get_type b.
Proof.
Lemma nu_se_st:
forall v v',
~
same_eval (
Eval Vundef)
v ->
same_eval v v' ->
(
forall t,
wt_expr v t <->
wt_expr v'
t).
Proof.
Lemma nu_sei_st:
forall f v v',
~
same_eval_inj f v (
Eval Vundef) ->
same_eval_inj f v v' ->
(
forall t,
wt_expr v t <->
wt_expr v'
t).
Proof.
split;
intros.
destruct (
wt_expr_dec v'
t);
auto.
exfalso;
apply H.
red;
intros.
generalize (
expr_type _ _ H1 al'
em'), (
fun pf =>
expr_type'
al'
em'
_ _ pf n).
intros A B.
rewrite <-
B.
erewrite H0;
eauto.
simpl.
seval;
auto.
erewrite <-
H0;
eauto.
destruct (
wt_expr_dec v t);
auto.
exfalso;
apply H.
red;
intros.
generalize (
expr_type _ _ H1 al'
em'), (
fun pf =>
expr_type'
al'
em'
_ _ pf n).
intros A B.
exploit H0;
eauto.
intro C;
rewrite C in *.
eauto.
Qed.
Lemma ei_vundef:
forall f a b (
EI:
expr_inj f a b)
al em (
U:
eSexpr al em b =
Vundef),
eSexpr (
Val.inj_alloc al f) (
Val.inj_em em f)
a =
Vundef.
Proof.
intros.
generalize (
expr_inj_ld _ _ _ EI al em).
intro A;
inv A;
congruence.
Qed.
Lemma expr_inj_ld':
ei_ld'
expr_inj.
Proof.
induction 1;
simpl;
intros;
auto.
-
inv VI;
simpl;
auto.
rewrite (
ai _ _ _ FB).
sint.
rewrite (
Int.add_commut ofs1);
auto.
-
rewrite (
ie _ _ _ FB).
auto.
-
apply ld_unop;
auto.
-
apply ld_binop;
auto.
Qed.
Lemma expr_inj_se_ld':
ei_ld'
expr_inj_se.
Proof.
red; intros.
destruct EI as (a & b & A & B & C).
rewrite B.
erewrite A; eauto.
eapply expr_inj_ld'; eauto.
Qed.
Lemma expr_inj_nundef:
forall f a b
(
EI:
expr_inj f a b)
(
NU: ~
same_eval_inj f a (
Eval Vundef)),
~
same_eval b (
Eval Vundef).
Proof.
intros.
cut (
exists al al'
em em',
cm_inj al f al' /\
em_inj em f em' /\
eSexpr al'
em'
a <>
Vundef).
intros (
al &
al' &
em &
em' &
CMINJ &
EMINJ &
UNDEF).
intro SEU.
generalize (
expr_inj_ld'
_ _ _ EI al em al'
em'
CMINJ EMINJ).
rewrite SEU.
simpl.
intro D;
inv D;
congruence.
repeat (
apply Classical_Pred_Type.not_all_ex_not in NU;
dex).
exists n,
n1,
n0,
n2;
repSplit;
auto.
Qed.
Lemma nse_sym:
forall a b,
~
same_eval a b -> ~
same_eval b a.
Proof.
red; intros.
symmetry in H0; apply H; auto.
Qed.
Lemma expr_inj_se_get_type:
forall f a b
(
EI:
expr_inj_se f a b),
same_eval_inj f a (
Eval Vundef) \/ (
forall t,
wt_expr a t <->
wt_expr b t).
Proof.
Lemma wf_inj_expr_inj_se:
wf_inj expr_inj_se.
Proof.
Hint Resolve wf_inj_expr_inj_se.
Section INJ.
Variable ei :
meminj ->
expr_sym ->
expr_sym ->
Prop.
Hypothesis WF:
wf_inj ei.
Inductive memval_inject (
f:
meminj) :
memval ->
memval ->
Prop :=
|
memval_inject_symb:
forall e1 e2 n m t t'
(
Hmeminj:
ei f (
get_nth_part e1 n) (
get_nth_part e2 m))
(
TYPorUNDEF:
t =
t' \/
same_eval_inj f (
get_nth_part e1 n) (
Eval Vundef)),
memval_inject f (
Symbolic e1 t n) (
Symbolic e2 t'
m).
Lemma memval_inject_incr:
forall f f'
v1 v2,
memval_inject f v1 v2 ->
inject_incr f f' ->
memval_inject f'
v1 v2.
Proof.
intros.
inv WF.
inv H.
econstructor;
eauto.
destruct TYPorUNDEF;
auto.
right;
eapply same_eval_inj_incr;
eauto.
Qed.
Theorem gnp_inject:
forall n (
f:
meminj)
vl1 vl2
(
EI:
ei f vl1 vl2),
ei f (
get_nth_part vl1 n) (
get_nth_part vl2 n).
Proof.
inv WF.
induction n;
simpl;
intros;
eauto.
Qed.
Theorem eom_inject:
forall f a b
(
MI :
memval_inject f a b),
ei f (
expr_of_memval a) (
expr_of_memval b).
Proof.
Theorem psa_inject:
forall f vl1 vl2,
list_forall2 (
memval_inject f)
vl1 vl2 ->
ei f (
proj_symbolic_aux_le vl1) (
proj_symbolic_aux_le vl2).
Proof.
inv WF.
induction 1;
simpl;
eauto.
apply ei_binop0;
auto.
apply eom_inject;
auto.
Qed.
Theorem ps_inject:
forall f vl1 vl2 ,
list_forall2 (
memval_inject f)
vl1 vl2 ->
ei f (
proj_symbolic_le vl1) (
proj_symbolic_le vl2).
Proof.
Lemma mvinj_type:
forall f vl1 vl2,
list_forall2 (
memval_inject f)
vl1 vl2 ->
type_of_list_memval vl1 =
type_of_list_memval vl2 \/
exists h,
head vl1 =
Some h /\
same_eval_inj f (
expr_of_memval h) (
Eval Vundef).
Proof.
intros.
destruct H;
simpl;
auto.
inv H.
destruct TYPorUNDEF;
subst;
auto.
right;
exists (
Symbolic e1 t n);
split;
auto.
Qed.
Lemma in_psale_undef:
forall v e,
In e v ->
forall f,
same_eval_inj f (
expr_of_memval e) (
Eval Vundef) ->
same_eval_inj f (
proj_symbolic_aux_le v) (
Eval Vundef).
Proof.
induction v; simpl; intros. destr.
destr; subst.
- red; intros; simpl. erewrite H0; eauto.
- red; intros; simpl.
erewrite IHv; eauto.
seval; auto.
Qed.
Lemma in_decode_undef:
forall v c e,
In e v ->
forall f,
same_eval_inj f (
expr_of_memval e) (
Eval Vundef) ->
same_eval_inj f (
decode_val c v) (
Eval Vundef) .
Proof.
Lemma in_psale_undef':
forall l x,
In x l ->
same_eval (
expr_of_memval x) (
Eval Vundef) ->
same_eval (
proj_symbolic_aux_le l) (
Eval Vundef).
Proof.
induction l; simpl; intros; eauto. easy.
destr; subst.
red; intros; simpl.
rewrite H0. simpl; auto.
red; intros; simpl; erewrite IHl; simpl; eauto.
seval.
Qed.
Lemma in_decode_undef':
forall chunk l x,
In x l ->
same_eval (
expr_of_memval x) (
Eval Vundef) ->
same_eval (
decode_val chunk l) (
Eval Vundef).
Proof.
Theorem decode_val_inject:
forall f vl1 vl2 chunk,
list_forall2 (
memval_inject f)
vl1 vl2 ->
ei f (
decode_val chunk vl1) (
decode_val chunk vl2).
Proof.
Lemma same_eval_inj_undef:
forall f v,
same_eval_inj f v (
Eval Vundef) <->
(
forall al em al'
em' (
IA:
cm_inj al f al') (
IE:
em_inj em f em'),
eSexpr al'
em'
v =
Vundef).
Proof.
red; split; intros; eauto.
Qed.
Lemma encode_val_inject:
forall f v1 v2 chunk
(
EI:
ei f v1 v2),
list_forall2 (
memval_inject f) (
encode_val chunk v1) (
encode_val chunk v2).
Proof.
End INJ.
Lemma encode_val_inject':
forall f v1 v2 chunk
(
EI:
expr_inj_se f v1 v2),
list_forall2 (
memval_inject expr_inj_se f) (
encode_val chunk v1) (
encode_val chunk v2).
Proof.
memval_inject and compositions
Definition expr_list_inject (
f:
meminj) (
a b:
list expr_sym) :
Prop :=
list_forall2 (
expr_inj_se f)
a b.
Inductive list_ei (
ei:
meminj ->
expr_sym ->
expr_sym ->
Prop) (
f:
meminj):
list expr_sym ->
list expr_sym ->
Prop :=
|
list_ei_nil:
list_ei ei f nil nil
|
list_ei_cons:
forall a b al bl
(
EI:
ei f a b)
(
LEI:
list_ei ei f al bl),
list_ei ei f (
a::
al) (
b::
bl).
Lemma expr_list_inject_list_ei:
forall f vl1 vl2,
expr_list_inject f vl1 vl2 ->
list_ei expr_inj_se f vl1 vl2.
Proof.
induction 1; simpl; intros.
constructor.
constructor; auto.
Qed.
Lemma list_ei_expr_list_inject:
forall f vl1 vl2,
list_ei expr_inj_se f vl1 vl2 ->
expr_list_inject f vl1 vl2.
Proof.
induction 1; simpl; intros.
constructor.
constructor; auto.
Qed.
Lemma memval_inject_undef:
forall j n a t,
memval_inject expr_inj_se j (
Symbolic (
Eval Vundef)
t n)
a.
Proof.
intros.
destruct a.
constructor.
repeat red.
exists (
Eval Vundef), (
get_nth_part e n0);
repSplit;
auto.
red;
intros;
simpl;
auto.
rewrite gnp_rew.
simpl.
des n;
auto.
reflexivity.
constructor.
right.
red;
intros.
rewrite gnp_rew.
des n;
auto.
Qed.
Lemma expr_inj_se_vundef:
forall j v,
expr_inj_se j (
Eval Vundef)
v.
Proof.
intros; repeat eexists; constructor.
Qed.
Definition decode_encode chunk v :=
decode_val chunk (
encode_val chunk v).
Definition tolm_eq:
forall chunk b,
type_of_list_memval
(
encode_val chunk b)
=
match chunk with
Many32 |
Many64 =>
Some (
get_type b)
|
_ =>
None
end.
Proof.
des chunk.
Qed.
Lemma same_eval_wt:
forall v' (
NU: ~
exists al em,
eSexpr al em v' =
Vundef)
v (
SE:
same_eval v v')
t (
WT:
wt_expr v'
t),
wt_expr v t.
Proof.
intros.
destruct (
wt_expr_dec v t);
auto.
set (
al :=
fun _:
block =>
Int.zero).
set (
em :=
fun (
_:
block) (
_:
int) =>
Byte.zero).
generalize (
expr_type _ _ WT al em).
generalize (
fun H =>
expr_type'
al em _ _ H n).
generalize (
expr_nu_type al em v t _ eq_refl).
intros A1 A2 A3.
eapply A1.
rewrite SE.
intro EU;
apply NU;
eexists;
eauto.
rewrite SE.
apply A3.
Qed.
Lemma expr_inj_wt:
forall f e1 e2,
expr_inj f e1 e2 ->
forall t,
wt_expr e2 t ->
wt_expr e1 t.
Proof.
induction 1; simpl; auto.
inv VI; intros; simpl; auto.
destr.
apply IHexpr_inj; auto.
destr.
apply IHexpr_inj1; auto.
apply IHexpr_inj2; auto.
Qed.
Lemma expr_inj_se_to_bits:
forall f v v'
chunk,
get_type v =
get_type v' ->
expr_inj_se f v v' ->
expr_inj_se f (
to_bits chunk v) (
to_bits chunk v').
Proof.
intros.
destruct wf_inj_expr_inj_se.
des chunk;
eauto;
rewrite H.
destr;
eauto.
destr;
eauto.
Qed.
Lemma decode_encode_inj:
forall f a b
(
EQT:
get_type a =
get_type b)
(
EI:
expr_inj_se f a b)
chunk,
expr_inj_se f (
decode_encode chunk a) (
decode_encode chunk b).
Proof.
clear.
intros.
destruct wf_inj_expr_inj_se.
des chunk;
repeat (
apply ei_unop0 ||
apply ei_binop0 ||
auto);
rewrite !
tolm_eq;
rewrite EQT;
destr;
repeat (
apply ei_unop0 ||
apply ei_binop0 ||
apply expr_inj_se_to_bits ||
auto);
congruence.
Qed.
Lemma expr_inj_se_se:
forall f a b c,
expr_inj_se f a b ->
same_eval b c ->
expr_inj_se f a c.
Proof.
intros.
destruct H as (x & y & A & B & C).
exists x, y; repSplit; auto. congruence.
Qed.
Lemma expr_inj_se_l:
forall f a b c,
expr_inj_se f a b ->
same_eval a c ->
expr_inj_se f c b.
Proof.
intros.
destruct H as (x & y & A & B & C).
exists x, y; repSplit; auto.
rewrite <- A.
red; intros; rewrite H0; auto.
Qed.
Lemma get_type_correct_not_int_2:
forall v t,
get_type v =
Tint ->
wt_expr v t ->
t <>
Tint ->
wt_expr v Tint.
Proof.
unfold get_type.
intros.
repeat (
revert H;
destr).
des t.
Qed.
Ltac exp_get_type H :=
match type of H with
get_type ?
v = ?
t =>
unfold get_type in H;
destruct (
wt_expr_dec v Tint);
destruct (
wt_expr_dec v Tfloat);
destruct (
wt_expr_dec v Tsingle);
destruct (
wt_expr_dec v Tlong);
destr
end.
Ltac egt :=
repeat match goal with
H:
get_type ?
v = ?
t |-
_ =>
exp_get_type H
end.
Lemma decode_encode_eSexpr :
forall v chunk,
same_eval (
decode_encode chunk v) (
Val.load_result chunk v).
Proof.
clear.
red.
intros v chunk cm em.
unfold decode_encode.
generalize (
decode_encode_val_general v chunk chunk);
intro DE.
pose (
n:=
chunk).
des chunk;
try (
specialize (
DE cm em);
simpl in *;
rewrite DE;
now auto).
rewrite tolm_eq in *.
destr;
auto.
-
destr;
try now egt.
rewrite <-
DE;
destr.
-
destr;
destr;
try now (
egt;
match goal with
H:
wt_expr ?
v ?
t,
H0:
wt_expr ?
v ?
t' |-
context [
eSexpr ?
al ?
em ?
v] =>
let x :=
fresh in
assert (
t <>
t')
as x by congruence;
rewrite (
wt_expr_2_is_undef v t t'
H H0 x);
destr
end).
setoid_rewrite (
DE cm em);
auto.
setoid_rewrite (
DE cm em);
auto.
egt.
rewrite nwt_expr_undef;
auto.
intro;
dex.
des t.
Qed.
Lemma weak_wt_wt:
forall e t t',
weak_wt e t ->
wt_expr e t' ->
e <>
Eval Vundef ->
t =
t'.
Proof.
intros e t t'
A B C.
des A.
des (
styp_eq t t').
generalize (
wt_expr_2_is_undef _ _ _ w B n).
congruence.
exfalso;
apply n.
eauto.
Qed.
Tactic Notation "
Trim"
constr(
L) "
as"
ident(
H) :=
let x :=
fresh H in
assert (
x:=
L);
trim x; [
clear x|].
Lemma ei_vi:
forall ei (
wf:
wf_inj ei)
f v1 v2
(
ptr:
match v1 with
Vptr b o =>
f b <>
None
|
_ =>
True
end)
,
ei f (
Eval v1) (
Eval v2) ->
val_inject f v1 v2.
Proof.