Require Import Smallstep.
Require Import Machregs.
Require Import Asm.
Require Import Integers.
Require Import List.
Require Import ZArith.
Require Import Memtype.
Require Import Memory.
Require Import Archi.
Require Import Coqlib.
Require Import AST.
Require Import Globalenvs.
Require Import Events.
Require Import Values.
Require Import Conventions1.
Require Import RawAsm AsmFacts AsmRegs.
Section WFASM.
Fixpoint in_builtin_arg (
b:
builtin_arg preg) (
r:
preg) :=
match b with
|
BA x =>
if preg_eq r x then True else False
|
BA_splitlong ba1 ba2 =>
in_builtin_arg ba1 r \/
in_builtin_arg ba2 r
|
_ =>
False
end.
Inductive is_alloc :
instruction ->
Prop :=
is_alloc_intro sz pub ora:
is_alloc (
Pallocframe sz pub ora).
Definition make_palloc f :
instruction :=
let sz :=
fn_stacksize f in
(
Pallocframe sz (
fn_pubrange f) (
Ptrofs.sub (
Ptrofs.repr (
align sz 8)) (
Ptrofs.repr (
size_chunk Mptr)))).
Lemma make_palloc_is_alloc:
forall f,
is_alloc (
make_palloc f).
Proof.
constructor. Qed.
Inductive is_free :
instruction ->
Prop :=
is_free_intro sz ora:
is_free (
Pfreeframe sz ora).
Lemma is_free_dec:
forall i,
{
is_free i} + {~
is_free i}.
Proof.
destruct i; try now (right; intro A; inv A).
left. econstructor; eauto.
Defined.
Inductive is_jmp:
instruction ->
Prop :=
|
is_jmp_intro:
forall ros sg,
is_jmp (
Pjmp ros sg).
Inductive intermediate_instruction :
instruction ->
Prop :=
|
ii_alloc i:
is_alloc i ->
intermediate_instruction i
|
ii_jmp i:
i =
Pret \/
is_jmp i ->
intermediate_instruction i.
Record wf_asm_function (
f:
function):
Prop :=
{
wf_asm_alloc_only_at_beginning:
forall o sz pubrange ora,
find_instr o (
fn_code f) =
Some (
Pallocframe sz pubrange ora) ->
o = 0;
wf_asm_alloc_at_beginning:
find_instr 0 (
fn_code f) =
Some (
make_palloc f);
wf_asm_after_freeframe:
forall i o,
find_instr (
Ptrofs.unsigned o) (
fn_code f) =
Some i ->
is_free i ->
exists i' ,
find_instr (
Ptrofs.unsigned (
Ptrofs.add o (
Ptrofs.repr (
instr_size i)))) (
fn_code f) =
Some i' /\
(
i' =
Pret \/
is_jmp i' );
wf_asm_ret_jmp_comes_after_freeframe:
forall i o,
find_instr (
Ptrofs.unsigned o) (
fn_code f) =
Some i ->
i =
Pret \/
is_jmp i ->
exists o'
ifree,
find_instr (
Ptrofs.unsigned o') (
fn_code f) =
Some ifree /\
is_free ifree /\
Ptrofs.unsigned o' +
instr_size ifree =
Ptrofs.unsigned o;
wf_asm_code_bounded:
0 <=
code_size (
fn_code f) <=
Ptrofs.max_unsigned;
wf_asm_builtin_not_PC:
forall o ef args res,
find_instr o (
fn_code f) =
Some (
Pbuiltin ef args res) ->
~
in_builtin_res res PC /\
~
in_builtin_res res RSP
/\
Forall (
fun arg :
builtin_arg preg => ~
in_builtin_arg arg RA)
args;
wf_asm_jmp_no_rsp:
forall o (
r:
ireg)
sg,
find_instr o (
fn_code f) =
Some (
Pjmp (
inl r)
sg) ->
r <>
RSP;
wf_asm_call_no_rsp:
forall o (
r:
ireg)
sg,
find_instr o (
fn_code f) =
Some (
Pcall (
inl r)
sg) ->
r <>
RSP;
wf_asm_free_spec:
forall o sz ora,
find_instr o (
fn_code f) =
Some (
Pfreeframe sz ora) ->
sz =
fn_stacksize f /\
ora =
Ptrofs.sub (
Ptrofs.repr (
align (
Z.max 0
sz) 8)) (
Ptrofs.repr (
size_chunk Mptr));
wf_allocframe_repr:
forall o sz pubrange ora,
find_instr o (
fn_code f) =
Some (
Pallocframe sz pubrange ora) ->
align sz 8 -
size_chunk Mptr =
Ptrofs.unsigned (
Ptrofs.sub (
Ptrofs.repr (
align sz 8)) (
Ptrofs.repr (
size_chunk Mptr)));
wf_freeframe_repr:
forall o sz ora,
find_instr o (
fn_code f) =
Some (
Pfreeframe sz ora) ->
Ptrofs.repr (
align sz 8 -
size_chunk Mptr) =
Ptrofs.sub (
Ptrofs.repr (
align (
Z.max 0
sz) 8)) (
Ptrofs.repr (
size_chunk Mptr));
}.
Definition is_make_palloc a f :=
a =
make_palloc f /\
align (
fn_stacksize f) 8 -
size_chunk Mptr =
Ptrofs.unsigned (
Ptrofs.sub (
Ptrofs.repr (
align (
fn_stacksize f) 8)) (
Ptrofs.repr (
size_chunk Mptr))).
Lemma pair_eq:
forall {
A B}
(
Adec:
forall (
a b:
A), {
a =
b} + {
a <>
b})
(
Bdec:
forall (
a b:
B), {
a =
b} + {
a <>
b}),
forall (
a b:
A *
B), {
a =
b} + {
a <>
b}.
Proof.
intros.
destruct a, b.
destruct (Adec a a0), (Bdec b b0); subst;
first [ now (right; inversion 1; congruence)
| left; reflexivity ].
Defined.
Definition pallocframe_dec s s'
pr pr'
o o': {
Pallocframe s pr o =
Pallocframe s'
pr'
o'} + {
Pallocframe s pr o <>
Pallocframe s'
pr'
o'}.
Proof.
destruct (
zeq s s');
subst. 2: (
now right;
inversion 1).
destruct (
pair_eq zeq zeq pr pr');
subst. 2: (
now right;
inversion 1).
destruct (
Ptrofs.eq_dec o o');
subst. 2: (
now right;
inversion 1).
left;
reflexivity.
Defined.
Lemma and_dec:
forall {
A B:
Prop},
{
A } + { ~
A } ->
{
B } + { ~
B } ->
{
A /\
B } + { ~ (
A /\
B) }.
Proof.
intros. destruct H, H0; [left|right|right|right]; intuition.
Qed.
Definition is_make_palloc_dec a f : {
is_make_palloc a f } + { ~
is_make_palloc a f }.
Proof.
Definition check_ret_or_jmp roj :=
match roj with
|
Pret |
Pjmp _ _ =>
true
|
_ =>
false
end.
Definition valid_ret_or_jmp roj :=
match roj with
|
Pjmp (
inl r)
_ =>
negb (
preg_eq r RSP)
|
_ =>
true
end.
Definition check_free f sz ora :=
sz =
fn_stacksize f /\
ora =
Ptrofs.sub (
Ptrofs.repr (
align (
Z.max 0
sz) 8)) (
Ptrofs.repr (
size_chunk Mptr)) /\
Ptrofs.repr (
align sz 8 -
size_chunk Mptr) =
Ptrofs.sub (
Ptrofs.repr (
align (
Z.max 0
sz) 8)) (
Ptrofs.repr (
size_chunk Mptr)).
Definition check_free_dec f sz ora : {
check_free f sz ora } + { ~
check_free f sz ora }.
Proof.
Definition check_builtin args res :=
~
in_builtin_res res PC /\
~
in_builtin_res res RSP
/\
Forall (
fun arg :
builtin_arg preg => ~
in_builtin_arg arg RA)
args.
Lemma not_in_builtin_res_dec res r:
{~
in_builtin_res res r} + {~ ~
in_builtin_res res r}.
Proof.
induction res;
simpl.
destruct (
preg_eq x r);
subst;
intuition.
left;
inversion 1.
destruct IHres1,
IHres2;
try (
right;
now intuition).
left.
intuition congruence.
Qed.
Lemma not_in_builtin_arg_dec arg r:
{~
in_builtin_arg arg r} + {~ ~
in_builtin_arg arg r}.
Proof.
induction arg; simpl; try (try destr; left; now inversion 1).
destruct IHarg1, IHarg2; try (right; now intuition). left. intuition congruence.
Qed.
Definition check_builtin_dec args res: {
check_builtin args res} + { ~
check_builtin args res}.
Proof.
Lemma find_instr_bound:
forall c o i,
find_instr o c =
Some i ->
o +
instr_size i <=
code_size c.
Proof.
induction c;
simpl;
intros;
eauto.
congruence.
destr_in H.
inv H.
generalize (
code_size_non_neg c).
omega.
apply IHc in H.
omega.
Qed.
Lemma code_bounded_repr':
forall c
(
RNG: 0 <=
code_size c <=
Ptrofs.max_unsigned)
i o
(
FI:
find_instr o c =
Some i)
sz
(
LE: 0 <=
sz <=
instr_size i),
Ptrofs.unsigned (
Ptrofs.add (
Ptrofs.repr o) (
Ptrofs.repr sz)) =
o +
sz.
Proof.
Lemma code_bounded_repr:
forall c
(
RNG: 0 <=
code_size c <=
Ptrofs.max_unsigned)
i o
(
FI:
find_instr (
Ptrofs.unsigned o)
c =
Some i)
sz
(
LE: 0 <=
sz <=
instr_size i),
Ptrofs.unsigned (
Ptrofs.add o (
Ptrofs.repr sz)) =
Ptrofs.unsigned o +
sz.
Proof.
Lemma wf_asm_pc_repr' :
forall f :
function,
wf_asm_function f ->
forall (
i :
instruction) (
o :
ptrofs),
find_instr (
Ptrofs.unsigned o) (
fn_code f) =
Some i ->
forall sz :
Z, 0 <=
sz <=
instr_size i ->
Ptrofs.unsigned (
Ptrofs.add o (
Ptrofs.repr sz)) =
Ptrofs.unsigned o +
sz.
Proof.
Fixpoint check_asm_body (
f:
function) (
next_roj:
bool) (
r:
code) :
bool :=
match r with
|
nil =>
negb next_roj
|
i ::
r =>
let roj :=
proj_sumbool (
is_free_dec i)
in
check_asm_body f roj r &&
if next_roj then check_ret_or_jmp i &&
valid_ret_or_jmp i
else
negb (
check_ret_or_jmp i) &&
match i with
|
Pfreeframe sz ora =>
check_free_dec f sz ora
|
Pallocframe _ _ _ =>
false
|
Pcall (
inl r)
sg =>
negb (
preg_eq r RSP)
|
Pbuiltin _ args res =>
check_builtin_dec args res
|
_ =>
true
end
end.
Definition wf_asm_function_check (
f:
function) :
bool :=
match fn_code f with
|
nil =>
false
|
a::
r =>
is_make_palloc_dec a f &&
check_asm_body f false r
end &&
zle (
code_size (
fn_code f))
Ptrofs.max_unsigned.
Lemma check_asm_body_no_alloc:
forall f c b i,
check_asm_body f b c =
true ->
In i c ->
~
is_alloc i.
Proof.
induction c;
simpl;
intros.
easy.
intro IA.
inv IA.
assert (
exists b,
check_asm_body f b c =
true).
{
eexists.
refine (
proj1 _);
apply andb_true_iff;
eauto.
}
destruct H1.
destruct H0.
subst.
simpl in *.
apply andb_true_iff in H.
destruct H.
destr_in H0.
eapply IHc in H0;
eauto.
apply H0;
constructor.
Qed.
Lemma find_instr_app:
forall a o b,
0 <=
o ->
find_instr (
o +
code_size a) (
a ++
b) =
find_instr o b.
Proof.
Lemma find_instr_app':
forall a o b,
code_size a <=
o ->
find_instr o (
a ++
b) =
find_instr (
o -
code_size a)
b.
Proof.
intros.
rewrite <- (
find_instr_app a _ b).
f_equal.
omega.
omega.
Qed.
Lemma find_instr_split:
forall c o i,
find_instr o c =
Some i ->
exists a b,
c =
a ++
i ::
b /\
o =
code_size a.
Proof.
induction c;
simpl;
intros;
eauto.
congruence.
destr_in H.
inv H.
eexists nil,
c;
simpl.
split;
auto.
edestruct IHc as (
aa &
b &
EQ &
SZ).
apply H.
subst.
exists (
a::
aa),
b;
simpl;
split;
auto.
omega.
Qed.
Lemma code_size_app:
forall c1 c2,
code_size (
c1 ++
c2) =
code_size c1 +
code_size c2.
Proof.
induction c1; simpl; intros; eauto. rewrite IHc1. omega.
Qed.
Lemma check_asm_body_after_free:
forall f a i b roj,
check_asm_body f roj (
a ++
i ::
b) =
true ->
is_free i ->
check_asm_body f true b =
true.
Proof.
induction a;
simpl;
intros;
eauto.
apply andb_true_iff in H.
destruct H as (
H &
_).
inv H0.
simpl in *.
auto.
apply andb_true_iff in H.
destruct H as (
H &
B).
destruct (
is_free_dec a);
simpl in *.
inv i0.
eapply IHa;
eauto.
eapply IHa;
eauto.
Qed.
Lemma check_asm_body_call:
forall f c b r sg,
check_asm_body f b c =
true ->
In (
Pcall (
inl r)
sg)
c ->
r <>
RSP.
Proof.
induction c;
simpl;
intros.
easy.
assert (
exists b,
check_asm_body f b c =
true).
{
eexists.
refine (
proj1 _);
apply andb_true_iff;
eauto.
}
apply andb_true_iff in H.
destruct H.
destruct H1.
destruct H0;
eauto.
subst.
simpl in *.
destr_in H2;
simpl in *.
unfold proj_sumbool in H2;
destr_in H2.
simpl in H2.
congruence.
Qed.
Lemma check_asm_body_free:
forall f c b sz ora,
check_asm_body f b c =
true ->
In (
Pfreeframe sz ora)
c ->
check_free f sz ora.
Proof.
Lemma check_asm_body_before_roj:
forall f a i b roj,
check_asm_body f roj (
a ++
i ::
b) =
true ->
i =
Pret \/
is_jmp i ->
(
a =
nil /\
roj =
true) \/
exists a0 i0,
a =
a0 ++
i0 ::
nil /\
is_free i0.
Proof.
induction a;
simpl;
intros;
eauto.
-
apply andb_true_iff in H.
destruct H as (
A &
B).
destruct H0 as [
ROJ|
ROJ];
inv ROJ;
simpl in *.
destr_in B.
destr_in B.
-
apply andb_true_iff in H.
destruct H as (
A &
B).
destruct (
is_free_dec a);
simpl in *.
inv i0.
+
simpl in *.
destr_in B.
right.
destruct a0.
clear IHa.
simpl in *.
eexists nil,
_.
split.
simpl.
eauto.
constructor.
edestruct IHa as [
ROJ|(
a1 &
i1 &
EQ &
IFR)];
eauto.
destruct ROJ;
congruence.
rewrite EQ.
eexists (
_ ::
a1),
i1;
split.
simpl.
reflexivity.
auto.
+
edestruct IHa as [
ROJ|(
a1 &
i1 &
EQ &
IFR)];
eauto.
destruct ROJ;
congruence.
subst.
right.
eexists (
_ ::
a1),
i1;
split.
simpl.
reflexivity.
auto.
Qed.
Lemma check_asm_body_builtin:
forall f c b ef args res,
check_asm_body f b c =
true ->
In (
Pbuiltin ef args res)
c ->
check_builtin args res.
Proof.
Lemma check_asm_body_jmp:
forall f c b r sg,
check_asm_body f b c =
true ->
In (
Pjmp (
inl r)
sg)
c ->
r <>
RSP.
Proof.
induction c;
simpl;
intros.
easy.
assert (
exists b,
check_asm_body f b c =
true).
{
eexists.
refine (
proj1 _);
apply andb_true_iff;
eauto.
}
apply andb_true_iff in H.
destruct H.
destruct H1.
destruct H0;
eauto.
subst.
simpl in *.
destr_in H2;
simpl in *.
unfold proj_sumbool in H2;
destr_in H2.
simpl in H2.
congruence.
Qed.
Lemma wf_asm_function_check_correct f:
wf_asm_function_check f =
true ->
wf_asm_function f.
Proof.
Lemma wf_asm_pc_repr:
forall f (
WF:
wf_asm_function f)
i o,
find_instr (
Ptrofs.unsigned o) (
fn_code f) =
Some i ->
Ptrofs.unsigned (
Ptrofs.add o (
Ptrofs.repr (
instr_size i))) =
Ptrofs.unsigned o +
instr_size i.
Proof.
Lemma wf_asm_wf_allocframe:
forall f (
WF:
wf_asm_function f)
o sz pubrange ora
(
FI:
find_instr o (
fn_code f) =
Some (
Pallocframe sz pubrange ora)),
make_palloc f =
Pallocframe sz pubrange ora.
Proof.
End WFASM.
Section WITHMEMORYMODEL.
Existing Instance mem_accessors_default.
Context `{
memory_model_ops:
Mem.MemoryModelOps}.
Context `{
external_calls_ops : !
ExternalCallsOps mem}.
Context `{
enable_builtins: !
EnableBuiltins mem}.
Section WITHGE.
Variable ge :
Genv.t Asm.fundef unit.
Definition exec_instr f i rs (
m:
mem) :=
let sz :=
Ptrofs.repr (
Asm.instr_size i)
in
match i with
|
Pallocframe size _ ofs_ra =>
let sp :=
Val.offset_ptr (
rs RSP) (
Ptrofs.neg (
Ptrofs.sub (
Ptrofs.repr (
align size 8)) (
Ptrofs.repr (
size_chunk Mptr))))
in
Next (
nextinstr (
rs #
RAX <- (
Val.offset_ptr (
rs RSP) (
Ptrofs.repr (
size_chunk Mptr))) #
RSP <-
sp)
sz)
m
|
Pfreeframe fsz ofs_ra =>
let sp :=
Val.offset_ptr (
rs RSP) (
Ptrofs.sub (
Ptrofs.repr (
align (
Z.max 0
fsz) 8)) (
Ptrofs.repr (
size_chunk Mptr)))
in
Next (
nextinstr (
rs#
RSP <-
sp)
sz)
m
|
Pload_parent_pointer rd z =>
let sp :=
Val.offset_ptr (
rs RSP) (
Ptrofs.repr (
align (
Z.max 0
z) 8))
in
Next (
nextinstr (
rs#
rd <-
sp)
sz)
m
|
Pcall ros sg =>
let addr :=
eval_ros ge ros rs in
let sp :=
Val.offset_ptr (
rs RSP) (
Ptrofs.neg (
Ptrofs.repr (
size_chunk Mptr)))
in
match Mem.storev Mptr m sp (
Val.offset_ptr rs#
PC sz)
with
|
None =>
Stuck
|
Some m2 =>
Next (
rs#
RA <- (
Val.offset_ptr rs#
PC sz)
#
PC <-
addr
#
RSP <-
sp)
m2
end
|
Pret =>
match Mem.loadv Mptr m rs#
RSP with
|
None =>
Stuck
|
Some ra =>
let sp :=
Val.offset_ptr (
rs RSP) (
Ptrofs.repr (
size_chunk Mptr))
in
Next (
rs #
RSP <-
sp
#
PC <-
ra
#
RA <-
Vundef)
m
end
|
_ =>
Asm.exec_instr nil ge f i rs m
end.
Inductive step :
state ->
trace ->
state ->
Prop :=
|
exec_step_internal:
forall b ofs f i rs m rs'
m',
rs PC =
Vptr b ofs ->
Genv.find_funct_ptr ge b =
Some (
Internal f) ->
find_instr (
Ptrofs.unsigned ofs) (
fn_code f) =
Some i ->
exec_instr f i rs m =
Next rs'
m' ->
step (
State rs m)
E0 (
State rs'
m')
|
exec_step_builtin:
forall b ofs f ef args res rs m vargs t vres rs'
m',
rs PC =
Vptr b ofs ->
Genv.find_funct_ptr ge b =
Some (
Internal f) ->
find_instr (
Ptrofs.unsigned ofs)
f.(
fn_code) =
Some (
Pbuiltin ef args res) ->
eval_builtin_args ge rs (
rs RSP)
m args vargs ->
external_call ef ge vargs m t vres m' ->
forall BUILTIN_ENABLED:
builtin_enabled ef,
rs' =
nextinstr_nf
(
set_res res vres
(
undef_regs (
map preg_of (
destroyed_by_builtin ef))
rs))
(
Ptrofs.repr (
Asm.instr_size (
Pbuiltin ef args res))) ->
step (
State rs m)
t (
State rs'
m')
|
exec_step_external:
forall b ef args res rs m t rs'
m',
rs PC =
Vptr b Ptrofs.zero ->
Genv.find_funct_ptr ge b =
Some (
External ef) ->
extcall_arguments (
rs #
RSP <- (
Val.offset_ptr (
rs RSP) (
Ptrofs.repr (
size_chunk Mptr))))
m (
ef_sig ef)
args ->
forall (
SP_TYPE:
Val.has_type (
rs RSP)
Tptr)
ra (
LOADRA:
Mem.loadv Mptr m (
rs RSP) =
Some ra)
(
SP_NOT_VUNDEF:
rs RSP <>
Vundef)
(
RA_NOT_VUNDEF:
ra <>
Vundef),
external_call ef ge args m t res m' ->
rs' = (
set_pair (
loc_external_result (
ef_sig ef))
res
(
undef_regs (
CR ZF ::
CR CF ::
CR PF ::
CR SF ::
CR OF ::
nil)
(
undef_regs (
map preg_of destroyed_at_call)
rs)))
#
PC <-
ra
#
RA <-
Vundef
#
RSP <- (
Val.offset_ptr (
rs RSP) (
Ptrofs.repr (
size_chunk Mptr))) ->
step (
State rs m)
t (
State rs'
m').
End WITHGE.
Inductive initial_state_gen (
prog:
Asm.program) (
rs:
regset)
m:
state ->
Prop :=
|
initial_state_gen_intro:
forall m1 bstack m2 m3 m4 bmain
(
MALLOC:
Mem.alloc (
Mem.push_new_stage m) 0 (
Mem.stack_limit +
align (
size_chunk Mptr) 8) = (
m1,
bstack))
(
MDROP:
Mem.drop_perm m1 bstack 0 (
Mem.stack_limit +
align (
size_chunk Mptr) 8)
Writable =
Some m2)
(
MRSB:
Mem.record_stack_blocks m2 (
make_singleton_frame_adt'
bstack frame_info_mono 0) =
Some m3)
(
STORE_RETADDR:
Mem.storev Mptr m3 (
Vptr bstack (
Ptrofs.repr (
Mem.stack_limit +
align (
size_chunk Mptr) 8 -
size_chunk Mptr)))
Vnullptr =
Some m4),
let ge :=
Genv.globalenv prog in
Genv.find_symbol ge prog.(
prog_main) =
Some bmain ->
let rs0 :=
rs #
PC <- (
Vptr bmain Ptrofs.zero)
#
RA <-
Vnullptr
#
RSP <- (
Val.offset_ptr (
Vptr bstack (
Ptrofs.repr (
Mem.stack_limit +
align (
size_chunk Mptr) 8))) (
Ptrofs.neg (
Ptrofs.repr (
size_chunk Mptr))))
in
initial_state_gen prog rs m (
State rs0 m4).
Inductive initial_state (
prog:
Asm.program) (
rs:
regset) (
s:
state):
Prop :=
|
initial_state_intro:
forall m,
Genv.init_mem prog =
Some m ->
initial_state_gen prog rs m s ->
initial_state prog rs s.
Definition semantics_gen prog rs m :=
Semantics step (
initial_state_gen prog rs m)
final_state (
Genv.globalenv prog).
Definition semantics prog rs :=
Semantics step (
initial_state prog rs)
final_state (
Genv.globalenv prog).
Definition rs_state s :=
let '(
State rs _) :=
s in rs.
Definition m_state s :=
let '(
State _ m) :=
s in m.
Section INVARIANT.
Context {
memory_model: @
Mem.MemoryModel mem memory_model_ops }.
Existing Instance inject_perm_upto_writable.
Existing Instance symbols_inject_instance.
Context `{
external_calls_props : !
ExternalCallsProps mem
(
memory_model_ops :=
memory_model_ops)
}.
Variable prog:
Asm.program.
Let ge :=
Genv.globalenv prog.
Definition bstack :=
Genv.genv_next ge.
Definition rsp_ptr (
s:
state) :
Prop :=
exists o,
rs_state s RSP =
Vptr bstack o /\ (
align_chunk Mptr |
Ptrofs.unsigned o).
Definition bstack_perm (
s:
state) :
Prop :=
forall o k p,
Mem.perm (
m_state s)
bstack o k p ->
Mem.perm (
m_state s)
bstack o k Writable.
Definition stack_top_state (
s:
state) :
Prop :=
is_stack_top (
Mem.stack (
m_state s))
bstack.
Inductive real_asm_inv :
state ->
Prop :=
|
real_asm_inv_intro:
forall s
(
RSPPTR:
rsp_ptr s)
(
BSTACKPERM:
bstack_perm s)
(
STOP:
stack_top_state s),
real_asm_inv s.
Lemma real_initial_inv:
forall rs0 is,
initial_state prog rs0 is ->
real_asm_inv is.
Proof.
Lemma exec_instr_invar_same:
forall f i rs1 m1,
stack_invar i =
true ->
exec_instr ge f i rs1 m1 =
RawAsm.exec_instr ge f i rs1 m1.
Proof.
intros f i rs1 m1 SI.
destruct i; simpl in SI; simpl; congruence.
Qed.
Inductive is_load_parent_pointer:
instruction ->
Prop :=
|
ilpp_intro i z:
is_load_parent_pointer (
Pload_parent_pointer i z).
Lemma is_load_parent_pointer_dec i: {
is_load_parent_pointer i } + { ~
is_load_parent_pointer i }.
Proof.
destruct i; first [ now (right; inversion 1) | left; econstructor ].
Defined.
Lemma exec_instr_invar_same':
forall f i rs1 m1 l,
stack_invar i =
true ->
~
is_load_parent_pointer i ->
Asm.exec_instr l ge f i rs1 m1 =
RawAsm.exec_instr ge f i rs1 m1.
Proof.
intros f i rs1 m1 l SI NILPP.
destruct i; simpl in SI; simpl; try congruence.
contradict NILPP. constructor.
Qed.
Lemma exec_instr_invar_inv:
forall f i rs1 m1 rs2 m2,
asm_instr_no_rsp i ->
stack_invar i =
true ->
exec_instr ge f i rs1 m1 =
Next rs2 m2 ->
real_asm_inv (
State rs1 m1) ->
real_asm_inv (
State rs2 m2).
Proof.
intros f i rs1 m1 rs2 m2 NORSP INVAR EI RAI;
inv RAI.
destruct (
is_load_parent_pointer_dec i).
-
constructor.
+
red in RSPPTR;
red.
simpl in *.
destruct RSPPTR as (
o &
EQ &
AL).
red in NORSP.
inv i0.
simpl in EI.
inv EI.
simpl_regs.
setoid_rewrite Pregmap.gsspec.
destr.
inv e.
rewrite EQ.
simpl.
eexists;
split;
eauto.
apply div_ptr_add.
auto.
apply div_unsigned_repr.
transitivity 8.
unfold Mptr.
destr;
simpl.
exists 1;
omega.
exists 2;
omega.
apply align_divides.
omega.
apply align_Mptr_modulus.
apply align_Mptr_modulus.
eauto.
+
red in BSTACKPERM;
red.
simpl in *.
intros.
inv i0;
simpl in EI;
inv EI.
eauto.
+
red in STOP;
red.
simpl in *.
inv i0;
simpl in EI;
inv EI.
eauto.
-
erewrite exec_instr_invar_same in EI;
eauto.
erewrite <-
exec_instr_invar_same'
with (
l:=
nil)
in EI;
eauto.
exploit NORSP;
eauto.
intro EQ.
generalize (
asmgen_no_change_stack i INVAR _ _ _ _ _ _ _ EI).
intros (
A &
B).
constructor.
+
red in RSPPTR;
red.
simpl in *;
rewrite EQ.
eauto.
+
red in BSTACKPERM;
red.
simpl in *.
setoid_rewrite B.
eauto.
+
red in STOP;
red;
simpl in *.
rewrite A;
eauto.
Qed.
Lemma align_Mptr_sub:
forall o,
(
align_chunk Mptr |
Ptrofs.unsigned o) ->
(
align_chunk Mptr |
Ptrofs.unsigned (
Ptrofs.add o (
Ptrofs.neg (
Ptrofs.repr (
size_chunk Mptr))))).
Proof.
Lemma align_Mptr_add:
forall o,
(
align_chunk Mptr |
Ptrofs.unsigned o) ->
(
align_chunk Mptr |
Ptrofs.unsigned (
Ptrofs.add o (
Ptrofs.repr (
size_chunk Mptr)))).
Proof.
Lemma align_Mptr_add_gen:
forall o d,
(
align_chunk Mptr |
Ptrofs.unsigned o) ->
(
align_chunk Mptr |
Ptrofs.unsigned d) ->
(
align_chunk Mptr |
Ptrofs.unsigned (
Ptrofs.add o d)).
Proof.
Definition asm_prog_no_rsp (
ge:
Genv.t Asm.fundef unit):=
forall b f,
Genv.find_funct_ptr ge b =
Some (
Internal f) ->
asm_code_no_rsp (
fn_code f).
Definition wf_asm_prog (
ge:
Genv.t Asm.fundef unit):=
forall b f,
Genv.find_funct_ptr ge b =
Some (
Internal f) ->
wf_asm_function f.
Lemma real_asm_inv_inv:
forall (
prog_no_rsp:
asm_prog_no_rsp ge) (
WF:
wf_asm_prog ge)
s1 t s2,
step ge s1 t s2 ->
real_asm_inv s1 ->
real_asm_inv s2.
Proof.
End INVARIANT.
End WITHMEMORYMODEL.
Section RECEPTIVEDET.
Context `{
memory_model:
Mem.MemoryModel }.
Existing Instance inject_perm_upto_writable.
Context `{
external_calls_ops : !
ExternalCallsOps mem }.
Context `{!
EnableBuiltins mem}.
Existing Instance mem_accessors_default.
Existing Instance symbols_inject_instance.
Context `{
external_calls_props : !
ExternalCallsProps mem
(
memory_model_ops :=
memory_model_ops)
}.
Theorem real_asm_single_events p rs:
single_events (
semantics p rs).
Proof.
Theorem real_asm_receptive p rs:
receptive (
semantics p rs).
Proof.
Theorem real_asm_determinate p rs:
determinate (
semantics p rs).
Proof.
split.
-
simpl;
intros s t1 s1 t2 s2 STEP1 STEP2.
inv STEP1.
+
inv STEP2;
rewrite_hyps.
split.
constructor.
congruence.
simpl in H2.
inv H2.
+
inv STEP2;
rewrite_hyps.
inv H11.
exploit eval_builtin_args_determ.
apply H2.
apply H9.
intro;
subst.
exploit external_call_determ.
apply H3.
apply H10.
intros (
A &
B);
split;
auto.
intro C.
destruct B;
auto.
congruence.
+
inv STEP2;
rewrite_hyps.
exploit extcall_arguments_determ.
apply H1.
apply H7.
intro;
subst.
exploit external_call_determ.
apply H2.
apply H8.
intros (
A &
B);
split;
auto.
intro C.
destruct B;
auto.
congruence.
-
apply real_asm_single_events.
-
simpl.
intros s1 s2 IS1 IS2;
inv IS1;
inv IS2.
rewrite_hyps.
inv H0;
inv H2.
rewrite_hyps.
unfold rs0,
rs1,
ge,
ge0 in *.
rewrite_hyps.
congruence.
-
simpl.
intros s r FS.
red.
intros t s'
STEP.
inv FS.
inv STEP;
rewrite_hyps.
-
simpl.
intros s r1 r2 FS1 FS2.
inv FS1;
inv FS2.
congruence.
Qed.
End RECEPTIVEDET.