From compcert Require Import cfrontend.ClightBigstep.
From compcert Require Import cfrontend.Clight.
From compcert Require Import cfrontend.Ctypes.
From compcert Require Import lib.Integers.
From compcert Require Import lib.Maps.
From compcert Require Import lib.Coqlib.
From compcert Require Errors.
From compcert Require Import common.Separation.
From compcert Require Import common.Values.
From compcert Require Import common.Memory.
From compcert Require Import common.Events.
From compcert Require Import common.Globalenvs.
From compcert Require Import common.Smallstep.
From compcert Require Import common.Behaviors.
From Velus Require Import Common.
From Velus Require Import Environment.
From Velus Require Import VelusMemory.
From Velus Require Import Ident.
From Velus Require Import Traces.
From Velus Require Import Common.CompCertLib.
From Velus Require Import ObcToClight.MoreSeparation.
From Velus Require Import ObcToClight.SepInvariant.
From Velus Require Import ObcToClight.Generation.
From Velus Require Import ObcToClight.GenerationProperties.
From Velus Require Import ObcToClight.Interface.
From Coq Require Import Program.Tactics.
From Coq Require Import List.
Import List.ListNotations.
From Coq Require Import ZArith.BinInt.
From Coq Require Import Omega.
From Coq Require Import Sorting.Permutation.
Import Obc.Typ.
Import Obc.Syn.
Import Obc.Sem.
Import Obc.Inv.
Import OpAux.
Open Scope list_scope.
Open Scope sep_scope.
Open Scope Z.
Hint Constructors Clight.eval_lvalue Clight.eval_expr.
Hint Resolve Clight.assign_loc_value.
Hint Resolve Z.divide_refl.
simple occurence predicate *
(to ensure that a statement occurs in the caller body) *
Inductive occurs_in:
stmt ->
stmt ->
Prop :=
|
occurs_refl:
forall s,
occurs_in s s
|
occurs_ite:
forall s e s1 s2,
occurs_in s s1 \/
occurs_in s s2 ->
occurs_in s (
Ifte e s1 s2)
|
occurs_comp:
forall s s1 s2,
occurs_in s s1 \/
occurs_in s s2 ->
occurs_in s (
Comp s1 s2).
Hint Resolve occurs_refl.
Remark occurs_in_ite:
forall e s1 s2 s,
occurs_in (
Ifte e s1 s2)
s ->
occurs_in s1 s /\
occurs_in s2 s.
Proof.
intros * Occurs.
induction s; inversion_clear Occurs as [|? ? ? ? [Hs1|Hs2]|? ? ? [Hs1|Hs2]];
split; constructor; ((left; now apply IHs1) || (right; now apply IHs2) || idtac).
- left; auto.
- right; auto.
Qed.
Remark occurs_in_comp:
forall s1 s2 s,
occurs_in (
Comp s1 s2)
s ->
occurs_in s1 s /\
occurs_in s2 s.
Proof.
intros * Occurs.
induction s; inversion_clear Occurs as [|? ? ? ? [Hs1|Hs2]|? ? ? [Hs1|Hs2]];
split; constructor; ((left; now apply IHs1) || (right; now apply IHs2) || idtac).
- left; auto.
- right; auto.
Qed.
Hint Resolve occurs_in_ite occurs_in_comp.
Lemma occurs_in_wt:
forall s s'
p insts mems vars,
wt_stmt p insts mems vars s ->
occurs_in s'
s ->
wt_stmt p insts mems vars s'.
Proof.
induction s; intros * Wt Occ;
inv Wt; inversion_clear Occ as [|? ? ? ? [?|?]|? ? ? [?|?]];
try econstructor; eauto.
Qed.
Lemma occurs_in_No_Naked_Vars:
forall s2 s1,
No_Naked_Vars s2 ->
occurs_in s1 s2 ->
No_Naked_Vars s1.
Proof.
induction s2;
inversion_clear 1;
inversion_clear 1;
eauto using No_Naked_Vars;
take (
_ \/
_)
and destruct it;
auto.
Qed.
Lemma occurs_in_instance_methods:
forall ys clsid o fid es f p insts mems,
wt_method p insts mems f ->
NoDupMembers insts ->
occurs_in (
Call ys clsid o fid es) (
m_body f) ->
(1 <
length ys)%
nat ->
M.MapsTo (
o,
fid)
clsid (
instance_methods f).
Proof.
Section PRESERVATION.
we work in a well-typed translated program *
Variable (
main_node :
ident)
(
prog :
program)
(
tprog :
Clight.program)
(
do_sync :
bool)
(
all_public :
bool).
Let tge :=
Clight.globalenv tprog.
Let gcenv :=
Clight.genv_cenv tge.
Hypothesis (
TRANSL :
translate do_sync all_public main_node prog =
Errors.OK tprog)
(
WT :
wt_program prog).
Opaque sepconj.
Hint Resolve wt_val_load_result.
Hint Constructors wt_stmt.
Section MatchStates.
we work under a caller method of an owner class, *
we state various results of semantics preservation using *
the memory predicate match_states *
Variable
Obc class
(
ownerid :
ident) (
owner :
class) (
prog' :
program)
Obc method
(
callerid :
ident) (
caller :
method)
Obc state
(
me :
menv) (
ve :
venv)
Clight state
(
m :
Mem.mem) (
e :
Clight.env) (
le :
temp_env)
Clight self structure
(
sb :
block) (
sofs :
ptrofs)
Clight output structure
(
outb_co :
option (
block *
composite))
frame
(
P :
massert).
Hypothesis (
Findowner :
find_class ownerid prog =
Some (
owner,
prog'))
(
Findcaller :
find_method callerid owner.(
c_methods) =
Some caller)
(
Hmem :
m |=
match_states gcenv prog owner caller (
me,
ve) (
e,
le)
sb sofs outb_co
**
P).
Section ExprCorrectness.
correctness of expressions *
out->x
Section OutField.
Variable (
x :
ident)
(
ty :
type).
Let out_ind_field :=
deref_field (
prefix obc2c out) (
prefix_fun (
m_name caller) (
c_name owner))
x (
cltype ty).
Hypothesis (
Hin :
In (
x,
ty)
caller.(
m_out))
(
Length : (1 <
length caller.(
m_out))%
nat).
Lemma evall_out_field:
forall ve1 le1 m1 P1,
m1 |=
outputrep gcenv owner caller ve1 le1 outb_co **
P1 ->
exists outb outco d,
eval_lvalue tge e le1 m1 out_ind_field outb (
Ptrofs.repr d)
/\
outb_co =
Some (
outb,
outco)
/\
field_offset gcenv x (
co_members outco) =
Errors.OK d.
Proof.
Corollary eval_out_field:
forall v,
Env.find x ve =
Some v ->
eval_expr tge e le m out_ind_field v.
Proof.
End OutField.
̄x
Lemma eval_temp_var:
forall x ty v,
In (
x,
ty) (
meth_vars caller) ->
~
InMembers x caller.(
m_out) ->
Env.find x ve =
Some v ->
eval_expr tge e le m (
Etempvar x (
cltype ty))
v.
Proof.
x
Corollary eval_var:
forall x ty v,
Env.find x ve =
Some v ->
In (
x,
ty) (
meth_vars caller) ->
eval_expr tge e le m (
translate_var owner caller x ty)
v.
Proof.
self->x and &self->o
Section SelfField.
Variable (
x :
ident)
(
ty :
type).
Let self_ind_field :=
deref_field (
prefix obc2c self) (
c_name owner)
x (
cltype ty).
Hypothesis (
Hmems :
In (
x,
ty)
owner.(
c_mems)).
Lemma evall_self_field:
exists d,
eval_lvalue tge e le m self_ind_field sb (
Ptrofs.add sofs (
Ptrofs.repr d))
/\
field_offset gcenv x (
make_members owner) =
Errors.OK d
/\ 0 <=
d <=
Ptrofs.max_unsigned.
Proof.
Corollary eval_self_field:
forall v,
find_val x me =
Some v ->
eval_expr tge e le m self_ind_field v.
Proof.
&self->o : appears only as an additional parameter of funcalls
Lemma eval_self_inst:
forall o c',
In (
o,
c') (
c_objs owner) ->
exists d,
eval_expr tge e le m (
ptr_obj owner c'
o) (
Vptr sb (
Ptrofs.add sofs (
Ptrofs.repr d)))
/\
field_offset gcenv o (
make_members owner) =
Errors.OK d
/\ 0 <=
Ptrofs.unsigned sofs +
d <=
Ptrofs.max_unsigned.
Proof.
End SelfField.
Theorem expr_correct:
forall ex v,
wt_exp owner.(
c_mems) (
meth_vars caller)
ex ->
exp_eval me ve ex (
Some v) ->
eval_expr tge e le m (
translate_exp owner caller ex)
v.
Proof.
Corollary exprs_correct:
forall es vs,
let es' :=
map (
translate_exp owner caller)
es in
Forall (
wt_exp owner.(
c_mems) (
meth_vars caller))
es ->
Forall2 (
fun e v =>
exp_eval me ve e (
Some v))
es vs ->
Clight.eval_exprlist tge e le m es'
(
list_type_to_typelist (
map Clight.typeof es'))
vs.
Proof.
End ExprCorrectness.
Hint Resolve exprs_correct.
Section AssignCorrectness.
'Hoare triple' for assignments, the leaves of the program *
Variable (
x :
ident) (
ty :
type) (
v :
val)
(
ae :
expr).
Hypothesis (
WTv :
wt_val v ty)
(
Teq :
Clight.typeof ae =
cltype ty)
(
Hin :
In (
x,
ty) (
meth_vars caller)).
x = ae : x can be a temp or an indirect access field (output variable)
Lemma exec_assign:
forall m1 le1 ve1 P1,
m1 |=
outputrep gcenv owner caller ve1 le1 outb_co
**
varsrep caller ve1 le1
**
P1 ->
eval_expr tge e le1 m1 ae v ->
exists m'
le',
exec_stmt_fe function_entry2 tge e le1 m1
(
assign owner caller x (
cltype ty)
ae)
E0 le'
m'
Out_normal
/\
m' |=
outputrep gcenv owner caller (
Env.add x v ve1)
le'
outb_co
**
varsrep caller (
Env.add x v ve1)
le'
**
P1
/\
forall v,
le1 ! (
prefix obc2c self) =
Some v ->
le' ! (
prefix obc2c self) =
Some v.
Proof.
clear Hmem;
intros *
Hmem Ev.
assert (
x <>
prefix obc2c self).
{
intro;
subst.
eapply In_InMembers,
m_AtomOrGensym,
AtomOrGensym_inv in Hin;
eauto. }
destruct (
mem_assoc_ident x caller.(
m_out))
eqn:
E.
-
assert (
In (
x,
ty)
caller.(
m_out))
as Hin'.
{
apply mem_assoc_ident_true in E as (
t &?).
assert (
In (
x,
t) (
meth_vars caller))
by (
do 2
setoid_rewrite in_app;
auto).
pose proof (
m_nodupvars caller);
app_NoDupMembers_det;
auto.
}
unfold assign.
destruct_list caller.(
m_out)
as (
x',
t') (
x'',
t'')
outs :
Houts;
try contradiction.
+
inversion_clear Hin'
as [
Eq|
Eq];
inv Eq.
exists m1, (
PTree.set x v le1);
rewrite PTree.gso;
intuition;
unfold exec_stmt_fe;
eauto using exec_stmt.
eapply sep_imp;
eauto.
*
eapply outputrep_assign_singleton_mem;
eauto.
*
rewrite varsrep_add;
eauto.
+
assert (1 <
Datatypes.length (
m_out caller))%
nat by (
rewrite Houts;
simpl;
omega).
assert (
In (
x,
ty)
caller.(
m_out))
by now rewrite Houts.
rewrite E.
edestruct outputrep_assign_gt1_mem as (
m' & ?&?&?&
Hco &
Hofs &?&?);
eauto using output_match.
exists m',
le1;
intuition;
auto.
*
edestruct evall_out_field with (
m1 :=
m1)
as (?&?&?&?&
Hco' &
Hofs');
eauto.
rewrite Hco in Hco';
inv Hco'.
simpl in Hofs.
change (
prog_comp_env tprog)
with gcenv in Hofs;
rewrite Hofs in Hofs';
inv Hofs'.
econstructor;
eauto;
simpl.
rewrite Teq;
eauto.
*
eapply sep_imp;
eauto.
rewrite varsrep_corres_out;
eauto.
-
assert (~
InMembers x caller.(
m_out))
by
(
apply NotIn_NotInMembers;
intro;
apply mem_assoc_ident_false;
auto).
exists m1, (
PTree.set x v le1);
rewrite PTree.gso;
intuition;
auto.
+
unfold assign.
destruct_list caller.(
m_out) :
Houts;
try rewrite E;
unfold exec_stmt_fe;
eauto using exec_stmt.
+
rewrite varsrep_add in Hmem.
eapply outputrep_assign_var_mem;
eauto using output_match.
Qed.
Corollary exec_assign_match_states:
eval_expr tge e le m ae v ->
exists m'
le',
exec_stmt_fe function_entry2 tge e le m
(
assign owner caller x (
cltype ty)
ae)
E0 le'
m'
Out_normal
/\
m' |=
match_states gcenv prog owner caller (
me,
Env.add x v ve) (
e,
le')
sb sofs outb_co
**
P .
Proof.
End AssignCorrectness.
Section FuncallAssignCorrectness.
assignments after a funcall are particular as they do not *
correspond to source statements *
we assume that the callee exists in a child class, with *
more at least two outputs, meaning that a local output *
structure is declared in the caller *
Variable
Child class
(
cid :
ident) (
c :
class) (
prog'' :
program)
Callee
(
fid :
ident) (
callee :
method)
the callee environment
(
ve_callee :
venv)
the local output structure
(
o :
ident) (
instco :
composite) (
instb :
block).
Hypothesis (
Findchild :
find_class cid prog =
Some (
c,
prog''))
(
Findcallee :
find_method fid c.(
c_methods) =
Some callee)
(
Len : (1 <
Datatypes.length (
m_out callee))%
nat)
(
Ho :
e !
o =
Some (
instb,
type_of_inst (
prefix_fun fid cid)))
(
Hinstco :
gcenv ! (
prefix_fun fid cid) =
Some instco).
o.x : a local output structure field is evaluated to the value found in the callee env
Lemma eval_inst_field:
forall x ty v le2 m1 P1,
let inst_field :=
Efield (
Evar o (
type_of_inst (
prefix_fun fid cid)))
x (
cltype ty)
in
m1 |=
fieldsrep gcenv ve_callee (
co_members instco)
instb **
P1 ->
In (
x,
ty)
callee.(
m_out) ->
Env.find x ve_callee =
Some v ->
eval_expr tge e le2 m1 inst_field v.
Proof.
after a call, we are not in match_states: the according *
structure is 'filled' with return values *
the variables to be assigned are again temporaries or *
indirect field accesses *
Variables
the memory just after the call
(
m1 :
Mem.mem)
frame
(
P1 :
massert).
Hypothesis (
Hmem1 :
m1 |=
fieldsrep gcenv ve_callee (
co_members instco)
instb
**
outputrep gcenv owner caller ve le outb_co
**
varsrep caller ve le
**
P1).
Lemma exec_funcall_assign_outs:
forall outs xs vs,
let tyo :=
type_of_inst (
prefix_fun fid cid)
in
incl outs callee.(
m_out) ->
Forall2 (
fun y xt =>
In (
y,
snd xt) (
meth_vars caller))
xs outs ->
wt_vals vs outs ->
Forall2 (
fun xt v =>
Env.find (
fst xt)
ve_callee =
Some v)
outs vs ->
exists m'
le',
exec_stmt_fe function_entry2 tge e le m1
(
funcall_assign owner caller xs o tyo outs)
E0 le'
m'
Out_normal
/\
m' |=
fieldsrep gcenv ve_callee (
co_members instco)
instb
**
outputrep gcenv owner caller (
Env.adds xs vs ve)
le'
outb_co
**
varsrep caller (
Env.adds xs vs ve)
le'
**
P1
/\
forall v,
le ! (
prefix obc2c self) =
Some v ->
le' ! (
prefix obc2c self) =
Some v.
Proof.
Corollary exec_funcall_assign:
forall xs vs,
let tyo :=
type_of_inst (
prefix_fun fid cid)
in
Forall2 (
fun y xt =>
In (
y,
snd xt) (
meth_vars caller))
xs callee.(
m_out) ->
wt_vals vs callee.(
m_out) ->
Forall2 (
fun xt v =>
Env.find (
fst xt)
ve_callee =
Some v)
callee.(
m_out)
vs ->
exists m'
le',
exec_stmt_fe function_entry2 tge e le m1
(
funcall_assign owner caller xs o tyo callee.(
m_out))
E0 le'
m'
Out_normal
/\
m' |=
fieldsrep gcenv ve_callee (
co_members instco)
instb
**
outputrep gcenv owner caller (
Env.adds xs vs ve)
le'
outb_co
**
varsrep caller (
Env.adds xs vs ve)
le'
**
P1
/\
forall v,
le ! (
prefix obc2c self) =
Some v ->
le' ! (
prefix obc2c self) =
Some v.
Proof.
End FuncallAssignCorrectness.
the expected execution and memory state after a funcall, *
depending on the numbers of outputs: *
0: no 'out' pointer parameter, we only need staterep for *
the sub-state, and we get an updated staterep after *
the call, with no return value *
1: no 'out' pointer parameter, we only need staterep for *
the sub-state, and we get an updated staterep after *
the call, with only one return value *
n: 'out' pointer parameter, we need both staterep for *
the sub-state and fieldsrep for the output structure, *
we get an updated staterep and a the output structure *
filled with the return values *
Definition call_spec (
c:
class) (
f:
method) (
vs rvs:
list val) (
me me':
menv) :
Prop :=
forall sb sofs m P,
bounded_struct_of_class tge c sofs ->
case_out f
(
m |=
staterep gcenv prog c.(
c_name)
me sb (
Ptrofs.unsigned sofs) **
P ->
exists m'
fd,
method_spec c f prog fd
/\
eval_funcall_fe function_entry2 tge m (
Internal fd)
(
Vptr sb sofs ::
vs)
E0 m'
Vundef
/\
m' |=
staterep gcenv prog c.(
c_name)
me'
sb (
Ptrofs.unsigned sofs) **
P
)
(
fun _ _ =>
m |=
staterep gcenv prog c.(
c_name)
me sb (
Ptrofs.unsigned sofs) **
P ->
exists m'
fd rv,
method_spec c f prog fd
/\
eval_funcall_fe function_entry2 tge m (
Internal fd)
(
Vptr sb sofs ::
vs)
E0 m'
rv
/\
rvs = [
rv]
/\
m' |=
staterep gcenv prog c.(
c_name)
me'
sb (
Ptrofs.unsigned sofs) **
P
)
(
fun outs =>
forall instb instco,
gcenv ! (
prefix_fun f.(
m_name)
c.(
c_name)) =
Some instco ->
m |=
staterep gcenv prog c.(
c_name)
me sb (
Ptrofs.unsigned sofs)
**
fieldsrep gcenv vempty instco.(
co_members)
instb
**
P ->
exists ve_f m'
fd,
method_spec c f prog fd
/\
eval_funcall_fe function_entry2 tge m (
Internal fd)
(
Vptr sb sofs ::
var_ptr instb ::
vs)
E0 m'
Vundef
/\
Forall2 (
fun xt v =>
Env.find (
fst xt)
ve_f =
Some v)
outs rvs
/\
m' |=
staterep gcenv prog c.(
c_name)
me'
sb (
Ptrofs.unsigned sofs)
**
fieldsrep gcenv ve_f instco.(
co_members)
instb
**
P
).
'Hoare triple' for funcalls, assuming call_spec for the *
callee as a mutual induction hypothesis *
Lemma exec_binded_funcall:
forall ys o es me_o'
vs rvs cid c prog''
fid callee,
find_class cid prog' =
Some (
c,
prog'') ->
find_method fid c.(
c_methods) =
Some callee ->
call_spec c callee vs rvs (
instance_match o me)
me_o' ->
Forall2 (
fun y xt =>
In (
y,
snd xt) (
meth_vars caller))
ys callee.(
m_out) ->
wt_vals rvs callee.(
m_out) ->
((1 <
Datatypes.length callee.(
m_out))%
nat ->
M.MapsTo (
o,
fid)
cid (
instance_methods caller)) ->
NoDup ys ->
In (
o,
cid) (
c_objs owner) ->
Forall2 (
fun e xt =>
Clight.typeof e =
cltype (
snd xt))
es callee.(
m_in) ->
eval_exprlist tge e le m es (
list_type_to_typelist (
map Clight.typeof es))
vs ->
wt_mem me_o'
prog''
c ->
exists m'
le',
exec_stmt_fe function_entry2 tge e le m
(
binded_funcall (
rev prog)
owner caller ys cid o fid es)
E0 le'
m'
Out_normal /\
m' |=
match_states gcenv prog owner caller
(
add_inst o me_o'
me,
Env.adds_opt ys (
map Some rvs)
ve)
(
e,
le')
sb sofs outb_co
**
P.
Proof.
intros *
Findchild Findcallee CallSpec Hins WTrvs Hinstmth Nodup Hin Hts Evs WTme_o.
assert (
find_class cid prog =
Some (
c,
prog''))
as Findchild'
by (
eapply find_class_chained;
eauto);
edestruct methods_corres with (3 :=
Findchild')
as (
loc_f &
fun_f &
Gf &
Gptrf &
Spec_f);
eauto.
assert (
forall targs tres cc,
eval_expr tge e le m (
Evar (
prefix_fun fid cid) (
Tfunction targs tres cc))
(
Vptr loc_f Ptrofs.zero)).
{
intros;
eapply eval_Elvalue.
-
apply eval_Evar_global;
eauto.
rewrite <-
not_Some_is_None.
intros (?, ?)
Hget.
apply match_states_conj in Hmem as (?&?&?&?&
He).
apply He in Hget;
destruct Hget as (? & ? &
Eqpref).
apply prefix_injective in Eqpref as (
Heq1&
_).
apply fun_not_out in Heq1;
auto.
-
apply deref_loc_reference;
auto.
}
assert (
Genv.find_funct (
Genv.globalenv tprog) (
Vptr loc_f Ptrofs.zero)
=
Some (
Internal fun_f))
by auto.
assert (
type_of_fundef (
Internal fun_f)
=
Tfunction
(
case_out callee
(
Tcons (
type_of_inst_p cid) (
list_type_to_typelist (
map Clight.typeof es)))
(
fun _ _ =>
Tcons (
type_of_inst_p cid) (
list_type_to_typelist (
map Clight.typeof es)))
(
fun _ =>
Tcons (
type_of_inst_p cid)
(
Tcons (
type_of_inst_p (
prefix_fun fid cid))
(
list_type_to_typelist (
map Clight.typeof es)))))
(
case_out callee Tvoid (
fun _ t =>
cltype t) (
fun _ =>
Tvoid))
AST.cc_default)
as Type_f.
{
simpl;
unfold type_of_function.
destruct Spec_f as (
Params_f &
Return_f &
CC_f &?).
rewrite Params_f,
Return_f,
CC_f;
simpl;
f_equal.
erewrite find_class_name,
find_method_name;
eauto.
unfold case_out;
destruct_list (
m_out callee)
as (?,?) (?,?) ?;
simpl;
erewrite types_pres';
eauto.
}
edestruct eval_self_inst as (
d & ?&
Hofs &?);
eauto.
assert (
Cop.sem_cast (
Vptr sb (
Ptrofs.add sofs (
Ptrofs.repr d)))
(
type_of_inst_p cid) (
type_of_inst_p cid)
m
=
Some (
Vptr sb (
Ptrofs.add sofs (
Ptrofs.repr d))))
by auto.
apply match_states_conj in Hmem as (
Hmem & ?&?&?&?).
assert (
bounded_struct_of_class tge c (
Ptrofs.repr (
Ptrofs.unsigned sofs +
d))).
{
unfold bounded_struct_of_class.
edestruct make_members_co as (?&?&?& <- &?);
eauto.
rewrite Ptrofs.unsigned_repr;
auto.
eapply struct_in_struct_in_bounds;
eauto.
-
eapply Consistent;
eauto.
-
eapply field_translate_obj_type;
eauto.
}
erewrite find_class_name in Hmem;
eauto.
pose proof (
conj Hin Hmem)
as Hmem';
eapply staterep_extract in Hmem'
as (
objs &
objs' & ? &
E &
Hofs' &
Hmem');
eauto.
clear Hmem;
rename Hmem'
into Hmem.
erewrite <-(
find_class_name cid)
in Hmem;
eauto.
rewrite Hofs'
in Hofs;
inv Hofs.
rewrite <- (
Ptrofs.unsigned_repr (
Ptrofs.unsigned sofs +
d))
in Hmem;
auto.
assert (0 <=
d <=
Ptrofs.max_unsigned).
{
assert (0 <=
Ptrofs.unsigned sofs)
by eauto.
split;
try omega.
edestruct field_offset_type;
eauto.
eapply field_offset_rec_in_range;
eauto.
}
assert (~
InMembers o (
objs ++
objs'))
by (
eapply NoDupMembers_app_cons;
setoid_rewrite <-
E;
apply c_nodupobjs).
unfold binded_funcall.
pose proof Findchild';
apply find_class_rev in Findchild'
as (
cls &
Findchild');
auto.
rewrite Findchild',
Findcallee.
unfold call_spec in CallSpec.
unfold case_out in Type_f,
CallSpec.
destruct_list callee.(
m_out)
as (
a,
ta) (
b,
tb) ? :
Hout;
inversion Hins as [|
x ????
Hins'];
try inv Hins';
inversion WTrvs as [|?????
WTrvs'];
try inv WTrvs'.
-
edestruct CallSpec as (
m' & ? &
Spec_f' &
EvalF &
Hmem');
eauto.
clear Hmem.
erewrite find_class_name in Hmem';
eauto.
eapply method_spec_eq with (2 :=
Spec_f)
in Spec_f';
eauto;
subst.
rewrite <- (
Ptrofs.unsigned_repr d), <-
Ptrofs.add_unsigned in EvalF;
eauto.
exists m',
le;
split.
+
unfold funcall.
change le with (
set_opttemp None Vundef le).
econstructor;
simpl;
eauto using eval_exprlist.
+
rewrite Env.adds_opt_nil_l.
apply match_states_conj;
intuition;
eauto.
erewrite find_class_name;
eauto.
eapply staterep_extract;
eauto.
exists objs,
objs',
d;
intuition;
eauto.
eapply sep_imp;
eauto.
*
unfold instance_match;
rewrite find_inst_gss.
rewrite Ptrofs.unsigned_repr;
auto.
*
repeat apply sep_imp';
auto.
apply staterep_objs_not_in;
auto.
-
edestruct CallSpec as (
m' & ? &
rv &
Spec_f' &
EvalF &
Erv &
Hmem');
eauto.
clear Hmem.
erewrite find_class_name in Hmem';
eauto.
inv Erv.
eapply method_spec_eq with (2 :=
Spec_f)
in Spec_f';
eauto;
subst.
rewrite <- (
Ptrofs.unsigned_repr d), <-
Ptrofs.add_unsigned in EvalF;
eauto.
rewrite sep_swap34,
sep_swap23,
sep_swap,
sep_swap67,
sep_swap56,
sep_swap45,
sep_swap34,
sep_swap23 in Hmem'.
edestruct exec_assign with (
x :=
x) (
ty :=
ta)
(
ae :=
Etempvar (
prefix_temp fid a) (
cltype ta))
(
le1 :=
PTree.set (
prefix_temp fid a)
rv le)
as (
m'' &
le' & ? &
Hmem'' &
Hself);
eauto using eval_expr,
PTree.gss.
{
eapply find_method_name in Findcallee;
subst.
specialize (
m_good callee)
as (
_&
Hat).
eapply sep_imp;
eauto.
-
apply outputrep_add_prefix;
auto.
-
repeat apply sep_imp';
auto.
apply varsrep_add'''.
intro contra.
eapply InMembers_In in contra as (?&
Hin').
specialize (
m_good caller)
as (
Hvars&
_).
rewrite Forall_map in Hvars.
repeat rewrite Forall_app in Hvars.
destruct Hvars as (?&?&?).
eapply Forall_forall in Hin'. 2:
rewrite Forall_app in *;
eauto.
eapply AtomOrGensym_inv in Hin';
eauto.
}
clear Hmem'.
exists m'',
le';
split.
+
change E0 with (
Eapp E0 (
Eapp E0 E0)).
unfold funcall.
eapply exec_Sseq_1;
eauto.
change (
PTree.set (
prefix_temp fid a)
rv le)
with (
set_opttemp (
Some (
prefix_temp fid a))
rv le).
econstructor;
simpl;
eauto using eval_exprlist.
+
simpl map;
rewrite Env.adds_opt_cons_cons,
Env.adds_opt_nil_l.
apply match_states_conj;
intuition;
eauto using m_nodupvars.
*
erewrite find_class_name;
eauto.
eapply staterep_extract;
eauto.
exists objs,
objs',
d;
intuition;
eauto.
rewrite sep_swap34,
sep_swap23,
sep_swap,
sep_swap67,
sep_swap56,
sep_swap45,
sep_swap34,
sep_swap23.
eapply sep_imp;
eauto.
repeat apply sep_imp';
auto.
--
unfold instance_match;
rewrite find_inst_gss.
rewrite Ptrofs.unsigned_repr;
auto.
--
apply staterep_objs_not_in;
auto.
*
apply Hself.
rewrite PTree.gso;
auto.
eapply prefix_injective'.
left.
prove_str_to_pos_neq.
-
assert (
M.MapsTo (
o,
fid)
cid (
instance_methods caller))
by (
apply Hinstmth;
simpl;
omega).
rewrite sep_swap45,
sep_swap34,
sep_swap23,
sep_swap in Hmem.
eapply subrep_extract in Hmem as (
instb &
instco &
xs &
xs' &?&
Hinstco &?&
Hmem);
eauto.
pose proof Hinstco;
erewrite <-(
find_class_name cid), <-(
find_method_name fid)
in Hinstco;
eauto.
assert (
eval_expr tge e le m (
Eaddrof (
Evar (
prefix_out fid o) (
type_of_inst (
prefix_fun fid cid)))
(
pointer_of (
type_of_inst (
prefix_fun fid cid))))
(
Vptr instb Ptrofs.zero))
by (
constructor;
constructor;
auto).
assert (
Cop.sem_cast (
Vptr instb Ptrofs.zero)
(
Clight.typeof
(
Eaddrof (
Evar (
prefix_out o fid) (
type_of_inst (
prefix_fun fid cid)))
(
pointer_of (
type_of_inst (
prefix_fun fid cid)))))
(
pointer_of (
type_of_inst (
prefix_fun fid cid)))
m
=
Some (
Vptr instb Ptrofs.zero))
by auto.
rewrite sep_swap23,
sep_swap in Hmem.
edestruct CallSpec as (
ve_f &
m' & ? &
Spec_f' &
EvalF & ? &
Hmem');
eauto.
erewrite find_class_name in Hmem';
eauto.
clear Hmem.
eapply method_spec_eq with (2 :=
Spec_f)
in Spec_f';
eauto;
subst.
rewrite <- (
Ptrofs.unsigned_repr d), <-
Ptrofs.add_unsigned in EvalF;
eauto.
assert (1 <
Datatypes.length (
m_out callee))%
nat by (
rewrite Hout;
simpl;
omega).
rewrite sep_swap,
sep_swap56,
sep_swap45,
sep_swap34,
sep_swap23,
sep_swap78,
sep_swap67,
sep_swap56,
sep_swap45,
sep_swap34 in Hmem'.
edestruct exec_funcall_assign as (
m'' &
le' & ? &
Hmem'' &
Hself);
eauto;
try rewrite Hout;
eauto.
clear Hmem'.
exists m'',
le';
split.
+
change E0 with (
Eapp E0 (
Eapp E0 E0)).
unfold funcall.
rewrite <-
Hout.
eapply exec_Sseq_1;
eauto.
change le with (
set_opttemp None Vundef le).
econstructor;
simpl;
eauto using eval_exprlist.
+
apply match_states_conj;
intuition;
eauto using m_nodupvars.
erewrite find_class_name;
eauto.
eapply staterep_extract;
eauto.
exists objs,
objs',
d;
intuition;
eauto.
rewrite sep_swap45,
sep_swap34,
sep_swap23,
sep_swap.
eapply subrep_extract;
eauto.
exists instb,
instco,
xs,
xs';
intuition.
rewrite Env.adds_opt_is_adds;
auto.
rewrite sep_swap56,
sep_swap45,
sep_swap34,
sep_swap23,
sep_swap78,
sep_swap67,
sep_swap56,
sep_swap45,
sep_swap34,
sep_swap45.
eapply sep_imp;
eauto using fieldsrep_any_empty.
repeat apply sep_imp';
eauto.
*
unfold instance_match;
rewrite find_inst_gss.
rewrite Ptrofs.unsigned_repr;
auto.
*
apply staterep_objs_not_in;
auto.
Qed.
End MatchStates.
The main correctness result, shown by mutual induction: *
the usual scheme with induction on the program is not *
adapted because the generation function is monadic, and not *
recursive *
we have to perform the mutual induction on suffixes though, *
to be able to use the previous results *
Hypothesis SpecIO :
forall ome ome'
clsid f vos rvos,
Forall (
fun vo =>
vo <>
None)
vos ->
stmt_call_eval prog ome clsid f vos ome'
rvos ->
Forall (
fun x =>
x <>
None)
rvos.
Hypothesis NO_NAKED_VARS:
Forall_methods (
fun m =>
No_Naked_Vars m.(
m_body))
prog.
Theorem mutual_correctness:
(
forall p me ve s me'
ve'
ownerid owner prog'
callerid caller m e le outb_co sb sofs P,
suffix p prog ->
stmt_eval p me ve s (
me',
ve') ->
find_class ownerid prog =
Some (
owner,
prog') ->
find_method callerid owner.(
c_methods) =
Some caller ->
occurs_in s caller.(
m_body) ->
m |=
match_states gcenv prog owner caller (
me,
ve) (
e,
le)
sb sofs outb_co
**
P ->
exists m'
le',
exec_stmt_fe function_entry2 tge e le m
(
translate_stmt (
rev prog)
owner caller s)
E0 le'
m'
Out_normal
/\
m' |=
match_states gcenv prog owner caller (
me',
ve') (
e,
le')
sb sofs outb_co
**
P)
/\
(
forall p me cid fid c f vs rvs prog'
me',
suffix p prog ->
stmt_call_eval p me cid fid (
map Some vs)
me' (
map Some rvs) ->
find_class cid prog =
Some (
c,
prog') ->
find_method fid c.(
c_methods) =
Some f ->
wt_vals vs f.(
m_in) ->
wt_mem me prog c ->
call_spec c f vs rvs me me').
Proof.
cut ((
forall p me ve s (
me_ve':
menv *
venv),
stmt_eval p me ve s me_ve' ->
suffix p prog ->
forall ownerid owner prog'
callerid caller m e le outb_co sb sofs P,
let (
me',
ve') :=
me_ve'
in
forall (
Findowner :
find_class ownerid prog =
Some (
owner,
prog'))
(
Findcaller :
find_method callerid owner.(
c_methods) =
Some caller)
(
Hmem :
m |=
match_states gcenv prog owner caller (
me,
ve) (
e,
le)
sb sofs outb_co **
P)
(
Occurs :
occurs_in s caller.(
m_body))
(
NoNaked :
No_Naked_Vars s)
(
WTs :
wt_stmt prog'
owner.(
c_objs)
owner.(
c_mems) (
meth_vars caller)
s),
exists m'
le',
exec_stmt_fe function_entry2 tge e le m
(
translate_stmt (
rev prog)
owner caller s)
E0 le'
m'
Out_normal
/\
m' |=
match_states gcenv prog owner caller (
me',
ve') (
e,
le')
sb sofs outb_co **
P)
/\
(
forall p me cid fid vos me'
rvos,
stmt_call_eval p me cid fid vos me'
rvos ->
suffix p prog ->
forall c f vs rvs prog',
find_class cid prog =
Some (
c,
prog') ->
find_method fid c.(
c_methods) =
Some f ->
wt_vals vs f.(
m_in) ->
wt_mem me prog'
c ->
vos =
map Some vs ->
rvos =
map Some rvs ->
call_spec c f vs rvs me me')).
{
intros (
Hstmt &
Hcall);
split;
eauto.
intros * ????
Occurs ?.
eapply (
Hstmt p me ve s (
me',
ve'));
eauto.
-
eapply occurs_in_No_Naked_Vars with (2 :=
Occurs);
eauto.
eapply Forall_methods_find with (1 :=
NO_NAKED_VARS);
eauto.
-
eapply occurs_in_wt with (2 :=
Occurs);
eauto.
eapply wt_class_find_method;
eauto.
eapply wt_program_find_class;
eauto.
}
Opaque match_states sepconj.
apply stmt_eval_call_ind; [| |
|
intros ??????????
IH1 ?
IH2
|
intros ?????????????
IH|
|
intros *
Findcl Findmth ??
IH Hrvos ? *
Findcl'
Findmth'];
intros;
try inversion_clear WTs as [| | | |?????????
Findcl Findmth|];
try inv NoNaked;
simpl.
-
eapply exec_assign_match_states;
eauto using expr_correct.
-
edestruct evall_self_field as (?&?&
Hofs' &?);
eauto.
take (
In _ (
c_mems owner))
and edestruct match_states_assign_state_mem with (4 :=
it)
as (
m' & ? &
Hofs & ? &
Hmem');
eauto.
rewrite Hofs in Hofs';
inv Hofs'.
exists m',
le;
intuition.
econstructor;
eauto using expr_correct;
simpl.
+
rewrite type_pres;
eauto.
+
rewrite Ptrofs.add_unsigned,
Ptrofs.unsigned_repr;
auto.
-
take (
stmt_call_eval _ _ _ _ _ _ _)
and rename it into Ev.
eapply stmt_call_eval_suffix in Ev;
eauto.
assert (
Forall (
fun vo =>
vo <>
None)
vos)
as HnNone
by (
eapply no_vars_in_args_spec;
eauto).
assert (
exists vs,
vos =
map Some vs)
as (
vs & ?)
by (
eapply not_None_is_Some_Forall;
auto).
assert (
exists rvs,
rvos =
map Some rvs)
as (
rvs &?)
by (
eapply not_None_is_Some_Forall;
eauto).
assert (
Forall2 (
fun vo xt =>
wt_valo vo (
snd xt))
vos (
m_in fm))
as WTvs by eauto.
subst.
rewrite Forall2_map_1 in WTvs;
simpl in WTvs.
pose proof Ev as Ev'.
pose proof Findcl;
eapply find_class_chained in Findcl;
eauto.
assert (
wt_mem (
instance_match o me)
p'
cls).
{
apply match_states_conj in Hmem as (?&?& (
WTmem & ?) &?).
inversion_clear WTmem as [????
WTinsts].
eapply Forall_forall in WTinsts;
eauto.
unfold instance_match.
inversion_clear WTinsts as [????
Find|???????
Find Findcl'];
rewrite Find;
auto.
rewrite Findcl in Findcl';
inv Findcl';
auto.
}
eapply pres_sem_stmt_call in Ev'
as (?&
WTrvos);
eauto.
rewrite Forall2_map_1 in WTrvos.
take (
Forall2 (
exp_eval _ _)
_ _)
and rewrite Forall2_map_2 in it.
inversion_clear Ev as [???????????
Findcl'
Findmth' ??
Hrvs].
rewrite Findcl in Findcl';
inv Findcl';
rewrite Findmth in Findmth';
inv Findmth'.
rewrite Forall2_map_1,
Forall2_map_2 in Hrvs.
eapply exec_binded_funcall;
eauto using exprs_correct.
+
intro;
eapply occurs_in_instance_methods;
eauto.
*
eapply wt_class_find_method;
eauto.
eapply wt_program_find_class;
eauto.
*
apply c_nodupobjs.
*
erewrite Forall2_length;
eauto.
+
rewrite Forall2_map_1.
eapply Forall2_impl_In;
eauto;
simpl.
setoid_rewrite type_pres;
congruence.
-
apply occurs_in_comp in Occurs as (?&?).
edestruct IH1 as (?&?&?&?);
eauto.
clear Hmem.
edestruct IH2 as (
m' &
le' &?&?);
eauto.
change E0 with (
Eapp E0 (
Eapp E0 E0)).
exists m',
le';
intuition;
unfold exec_stmt_fe;
eauto using exec_stmt.
-
assert (
Cop.bool_val v (
Clight.typeof (
translate_exp owner caller cond))
m =
Some b)
by (
rewrite type_pres;
take (
_ =
bool_type)
and rewrite it;
eauto).
apply occurs_in_ite in Occurs as (?&?).
destruct b.
+
edestruct IH as (
m' &
le' &?&?);
eauto.
exists m',
le';
intuition.
eapply exec_Sifthenelse with (
b :=
true);
eauto using expr_correct.
+
edestruct IH as (
m' &
le' &?&?);
eauto.
exists m',
le';
intuition.
eapply exec_Sifthenelse with (
b :=
false);
eauto using expr_correct.
-
exists m,
le;
split;
eauto;
constructor.
-
eapply find_class_sub_same in Findcl;
eauto.
rewrite Findcl'
in Findcl;
inv Findcl.
rewrite Findmth'
in Findmth;
inv Findmth.
assert (
NoDup (
map fst (
m_in fm)))
by (
apply fst_NoDupMembers,
m_nodupin).
rewrite Env.adds_opt_is_adds in IH;
auto.
assert (
wt_stmt prog' (
c_objs cls) (
c_mems cls) (
meth_vars fm) (
m_body fm))
by (
eapply wt_class_find_method;
eauto;
eapply wt_program_find_class;
eauto).
assert (
No_Naked_Vars fm.(
m_body))
by
(
eapply Forall_methods_find with (1 :=
NO_NAKED_VARS);
eauto).
assert (
wt_vals rvs fm.(
m_out))
as WTrvs.
{
assert (
Forall2 (
fun v xt =>
wt_valo v (
snd xt)) (
map Some vs) (
m_in fm))
by (
rewrite Forall2_map_1;
simpl;
auto).
assert (
Forall2 (
fun v xt =>
wt_valo v (
snd xt)) (
map Some rvs) (
m_out fm))
as WTrvs
by (
eapply pres_sem_stmt_call with (
me :=
me);
eauto using stmt_call_eval).
rewrite Forall2_map_1 in WTrvs;
simpl in WTrvs;
auto.
}
edestruct methods_corres as (
fun_b &
fd & ?&?&
Mspec);
eauto.
pose proof Mspec as Entry;
eapply function_entry_match_states with (
me :=
me)
in Entry;
eauto.
assert (
fn_body fd =
return_with (
translate_stmt (
rev prog)
cls fm (
m_body fm))
(
case_out fm
None
(
fun x t =>
Some (
make_in_arg (
x,
t)))
(
fun _ =>
None)))
as Body by (
destruct Mspec as (?&?&?&?&?&?&?&?&?);
auto).
assert (
fn_return fd =
case_out fm
Tvoid
(
fun _ t =>
cltype t)
(
fun _ =>
Tvoid))
as Return by (
destruct Mspec as (?&?&?);
auto).
unfold call_spec,
case_out in *;
intros.
assert (
suffix prog'
prog)
by (
eapply find_class_sub;
eauto).
subst gcenv;
erewrite find_class_name,
find_method_name;
eauto.
destruct_list (
m_out fm)
as (
a,
ta) (?,?) ? :
Hout;
[
intros *
Hmem|
intros *
Hmem|
intros * ?
Hmem];
edestruct Entry as (
e_f &
le_f &
m_f & ? &
Hm_f);
eauto;
clear Hmem;
edestruct IH as (
m' &
le' & ? &
Hm');
eauto;
clear Hm_f;
apply match_states_conj in Hm'
as (
Hm' &?);
rewrite sep_swap23,
sep_swap,
sep_swap34,
sep_swap23, <-
sep_assoc,
sep_unwand in Hm';
eauto using decidable_subrep;
apply free_exists in Hm'
as (
m'' & ?&
Hm'').
+
exists m'',
fd;
intuition;
eauto.
*
econstructor;
eauto.
--
rewrite Body.
change E0 with (
Eapp E0 E0).
eapply exec_Sseq_1;
eauto using exec_stmt.
--
rewrite Return;
simpl;
auto.
*
erewrite find_class_name in Hm'';
eauto.
now do 2
apply sep_drop2 in Hm''.
+
rewrite sep_swap in Hm''.
rewrite outputrep_singleton in Hm'';
eauto.
rewrite Forall2_map_1,
Forall2_map_2 in Hrvos.
inversion Hrvos as [|?
rv ??
Hrv Hrvos'];
inv Hrvos'.
inv WTrvs.
unfold match_var in Hm'';
simpl in Hrv;
rewrite Hrv in Hm''.
destruct Hm''
as (
Hm'' &
Eq).
cases_eqn E;
inv Eq.
exists m'',
fd,
rv;
intuition;
eauto.
*
econstructor;
eauto.
--
rewrite Body.
change E0 with (
Eapp E0 E0).
eapply exec_Sseq_1;
eauto using exec_stmt,
eval_expr.
--
rewrite Return;
simpl;
auto.
split;
eauto using sem_cast_same.
destruct ta;
simpl;
discriminate.
*
erewrite find_class_name in Hm'';
eauto.
now apply sep_drop2 in Hm''.
+
rewrite Forall2_map_1,
Forall2_map_2 in Hrvos.
exists ve',
m'',
fd;
intuition;
eauto.
*
econstructor;
eauto.
--
rewrite Body.
change E0 with (
Eapp E0 E0).
eapply exec_Sseq_1;
eauto using exec_stmt.
--
rewrite Return;
simpl;
auto.
*
erewrite find_class_name in Hm'';
eauto.
rewrite sep_swap in Hm''.
assert (1 <
Datatypes.length (
m_out fm))%
nat by (
rewrite Hout;
simpl;
omega).
apply outputrep_notnil in Hm''
as (?&?&
E &
Hm'' &?);
auto;
inv E.
rewrite sep_swap, <-
sep_assoc in Hm''.
apply sep_drop2 in Hm''.
now rewrite sep_assoc in Hm''.
Qed.
Corollary stmt_call_correctness:
forall me cid fid c f vs rvs prog'
me',
stmt_call_eval prog me cid fid (
map Some vs)
me' (
map Some rvs) ->
find_class cid prog =
Some (
c,
prog') ->
find_method fid c.(
c_methods) =
Some f ->
wt_vals vs f.(
m_in) ->
wt_mem me prog'
c ->
call_spec c f vs rvs me me'.
Proof.
Correctness of the whole program *
Let c_main :=
c_main _ _ _ _ _ TRANSL.
Let prog_main :=
prog_main _ _ _ _ _ TRANSL.
Let main_step :=
main_step _ _ _ _ _ TRANSL.
Let main_reset :=
main_reset _ _ _ _ _ TRANSL.
Let main_f :=
main_f _ _ _ _ _ TRANSL.
Definition find_main_class:
find_class main_node prog =
Some (
c_main,
prog_main) :=
find_main_class _ _ _ _ _ TRANSL.
Definition find_main_step:
find_method step c_main.(
c_methods) =
Some main_step :=
find_main_step _ _ _ _ _ TRANSL.
Definition find_main_reset:
find_method reset c_main.(
c_methods) =
Some main_reset :=
find_main_reset _ _ _ _ _ TRANSL.
Hint Resolve find_main_class find_main_step find_main_reset.
Lemma bounded_main_class:
bounded_struct_of_class tge c_main Ptrofs.zero.
Proof.
Hint Resolve bounded_main_class.
Lemma reset_correct:
forall me0,
stmt_call_eval prog mempty main_node reset []
me0 [] ->
call_spec c_main main_reset [] []
mempty me0.
Proof.
Lemma step_correct:
forall me me'
vs rvs,
stmt_call_eval prog me main_node step (
map Some vs)
me' (
map Some rvs) ->
wt_vals vs (
m_in main_step) ->
wt_mem me prog_main c_main ->
call_spec c_main main_step vs rvs me me'.
Proof.
Let le_main :=
create_undef_temps main_f.(
fn_temps).
Let out_step :=
prefix out step.
Let t_out_step :=
type_of_inst (
prefix_fun step main_node).
Lemma main_entry:
forall m0 P,
m0 |=
P ->
if lt_dec 1 (
length (
m_out main_step))
then
exists m1 step_b step_co,
function_entry2 tge main_f []
m0
(
PTree.set out_step (
step_b,
t_out_step)
empty_env)
le_main m1
/\
gcenv ! (
prefix_fun step main_node) =
Some step_co
/\
m1 |=
P
**
fieldsrep gcenv vempty step_co.(
co_members)
step_b
else function_entry2 tge main_f []
m0 empty_env le_main m0.
Proof.
Trace semantics of reads and writes to volatiles
Definition out_step_env (
e:
Clight.env) :
Prop :=
forall x b t,
e !
x =
Some (
b,
t) ->
x =
out_step.
Remark out_step_env_no_prefix_glob:
forall e x,
out_step_env e ->
e ! (
prefix_glob x) =
None.
Proof.
Lemma exec_read:
forall vs e le m,
out_step_env e ->
wt_vals vs main_step.(
m_in) ->
exists le',
exec_stmt_fe function_entry2 tge e le m
(
load_in main_step.(
m_in))
(
load_events vs main_step.(
m_in))
le'
m Out_normal
/\
Forall2 (
fun v xt =>
le' ! (
fst xt) =
Some v)
vs main_step.(
m_in)
/\ (
forall x, ~
InMembers x main_step.(
m_in) ->
le' !
x =
le !
x).
Proof.
Lemma exec_write_multiple:
forall outs,
incl outs main_step.(
m_out) ->
(1 <
Datatypes.length (
m_out main_step))%
nat ->
forall rvs e ve le m step_b step_co,
NoDupMembers outs ->
out_step_env e ->
wt_vals rvs outs ->
gcenv ! (
prefix_fun step main_node) =
Some step_co ->
e !
out_step =
Some (
step_b,
t_out_step) ->
Forall2 (
fun xt v =>
Env.find (
fst xt)
ve =
Some v)
outs rvs ->
m |=
fieldsrep gcenv ve (
co_members step_co)
step_b ->
exec_stmt_fe function_entry2 tge e le m
(
write_multiple_outs main_node outs)
(
store_events rvs outs)
le m Out_normal.
Proof.
Corollary exec_write:
forall rvs e le m,
out_step_env e ->
wt_vals rvs main_step.(
m_out) ->
case_out main_step
True
(
fun y t =>
exists rv,
rvs = [
rv] /\
le !
y =
Some rv)
(
fun outs =>
exists ve step_b step_co,
gcenv ! (
prefix_fun step main_node) =
Some step_co
/\
e !
out_step =
Some (
step_b,
t_out_step)
/\
Forall2 (
fun xt v =>
Env.find (
fst xt)
ve =
Some v)
outs rvs
/\
m |=
fieldsrep gcenv ve (
co_members step_co)
step_b) ->
exec_stmt_fe function_entry2 tge e le m
(
write_out main_node main_step.(
m_out))
(
store_events rvs main_step.(
m_out))
le m Out_normal.
Proof.
Clight version of dostep *
Section dostep.
Variables (
sb :
block)
(
step_f :
function).
Variables ins outs:
IStr.stream (
list val).
This coinductive predicate describes the logical behavior of
the while loop.
CoInductive dostep (
e:
Clight.env) :
nat ->
mem ->
Prop :=
DoStep :
forall n m m',
case_out main_step
(
eval_funcall_fe function_entry2 tge m (
Internal step_f)
(
var_ptr sb ::
ins n)
E0 m'
Vundef)
(
fun _ _ =>
exists v,
outs n = [
v]
/\
eval_funcall_fe function_entry2 tge m (
Internal step_f)
(
var_ptr sb ::
ins n)
E0 m'
v)
(
fun ys =>
exists ve step_b step_co,
eval_funcall_fe function_entry2 tge m (
Internal step_f)
(
var_ptr sb ::
var_ptr step_b ::
ins n)
E0 m'
Vundef
/\
gcenv ! (
prefix_fun step main_node) =
Some step_co
/\
e !
out_step =
Some (
step_b,
t_out_step)
/\
Forall2 (
fun xt v =>
Env.find (
fst xt)
ve =
Some v)
ys (
outs n)
/\
m' |=
fieldsrep gcenv ve (
co_members step_co)
step_b) ->
out_step_env e ->
dostep e (
S n)
m' ->
dostep e n m.
Section Dostep_coind.
Variable R:
nat ->
mem ->
Prop.
Variable e:
Clight.env.
Hypothesis He :
out_step_env e.
Definition dostepCase :=
forall n m,
R n m ->
exists m',
case_out main_step
(
eval_funcall_fe function_entry2 tge m (
Internal step_f)
(
var_ptr sb ::
ins n)
E0 m'
Vundef)
(
fun _ _ =>
exists v,
outs n = [
v]
/\
eval_funcall_fe function_entry2 tge m (
Internal step_f)
(
var_ptr sb ::
ins n)
E0 m'
v)
(
fun ys =>
exists ve step_b step_co,
eval_funcall_fe function_entry2 tge m (
Internal step_f)
(
var_ptr sb ::
var_ptr step_b ::
ins n)
E0 m'
Vundef
/\
gcenv ! (
prefix_fun step main_node) =
Some step_co
/\
e !
out_step =
Some (
step_b,
t_out_step)
/\
Forall2 (
fun xt v =>
Env.find (
fst xt)
ve =
Some v)
ys (
outs n)
/\
m' |=
fieldsrep gcenv ve (
co_members step_co)
step_b)
/\
R (
S n)
m'.
Lemma dostep_coind:
dostepCase ->
forall n m,
R n m ->
dostep e n m.
Proof.
intro DoStep.
cofix COINDHYP.
intros ? ? HR.
pose proof (DoStep _ _ HR) as Hstep.
simpl in *; decompose record Hstep; subst.
econstructor; eauto.
Qed.
End Dostep_coind.
dostep implies a step of the body loop *
Remark out_step_env_no_prefix_fun:
forall e x f,
out_step_env e ->
e ! (
prefix_fun f x) =
None.
Proof.
Hint Resolve out_step_env_no_prefix_fun.
Let step_name :=
Evar (
prefix_fun step main_node).
Let self_addr :=
Eaddrof (
Evar (
prefix_glob (
prefix self main_id)) (
type_of_inst main_node))
(
type_of_inst_p main_node).
Hypothesis Find_self :
Genv.find_symbol tge (
prefix_glob (
prefix self main_id)) =
Some sb.
evaluate the self parameter
Lemma eval_expr_self:
forall e le m,
out_step_env e ->
eval_expr tge e le m self_addr (
var_ptr sb).
Proof.
Hint Resolve eval_expr_self.
Hypothesis Hwt_ins :
forall n,
wt_vals (
ins n)
main_step.(
m_in).
Hypothesis Hwt_outs :
forall n,
wt_vals (
outs n)
main_step.(
m_out).
Hypothesis StepSpec :
method_spec c_main main_step prog step_f.
Lemma exec_body:
forall e n m_n le_n,
dostep e n m_n ->
exists le_Sn m_Sn,
exec_stmt_fe function_entry2 tge e le_n m_n
(
main_loop_body false main_node main_step)
(
load_events (
ins n) (
m_in main_step)
++
E0
++
store_events (
outs n) (
m_out main_step))
le_Sn m_Sn Out_normal
/\
dostep e (
S n)
m_Sn.
Proof.
intros *
Dostep.
inversion_clear Dostep as [??
m_Sn EvalStep].
edestruct exec_read with (
le :=
le_n) (
m :=
m_n)
as (
le1 & ?&?&?);
eauto.
edestruct methods_corres with (4 :=
find_main_step)
as (
ptr_step &
f &
Get_s &
Get_f & ?);
eauto.
assert (
f =
step_f)
by (
eapply method_spec_eq;
eauto);
subst f.
assert (
forall targs tres cc,
eval_expr tge e le1 m_n (
step_name (
Tfunction targs tres cc)) (
var_ptr ptr_step)).
{
intros;
eapply eval_Elvalue.
-
apply eval_Evar_global;
eauto.
-
apply deref_loc_reference;
auto.
}
assert (
forall vs,
wt_vals vs main_step.(
m_in) ->
Forall2 (
fun v xt =>
le1 ! (
fst xt) =
Some v)
vs main_step.(
m_in) ->
eval_exprlist tge e le1 m_n
(
map make_in_arg main_step.(
m_in))
(
list_type_to_typelist
(
map Clight.typeof (
map make_in_arg (
m_in main_step))))
vs).
{
clear.
induction main_step.(
m_in)
as [|(
x,
t)];
intros ?
Hvals_in;
inversion_clear Hvals_in as [|
cin ?
cins];
intro Hdef;
inversion_clear Hdef;
simpl in *;
eauto using eval_exprlist.
apply eval_Econs with (
v1 :=
cin)(
v2 :=
cin).
-
econstructor;
eauto.
-
now apply sem_cast_same.
-
apply IHl;
eauto.
}
assert (
exists le2,
exec_stmt_fe function_entry2 tge e le1 m_n
(
step_call main_node (
map make_in_arg (
m_in main_step)) (
m_out main_step))
E0 le2 m_Sn Out_normal
/\
match main_step.(
m_out),
outs n with
| [(
x,
_)], [
v] =>
le2 !
x =
Some v
|
_,
_ =>
True
end)
as (
le2 &
Hcall & ?).
{
unfold step_call.
destruct_list main_step.(
m_out)
as (?, ?) ? ? :
Out;
unfold case_out in EvalStep;
rewrite Out in EvalStep.
-
eexists;
split;
auto.
eapply exec_Scall;
simpl;
eauto;
simpl;
eauto using eval_exprlist.
unfold type_of_function.
destruct StepSpec as (
P_f &
R_f &
CC_f &?).
rewrite P_f,
R_f,
CC_f;
unfold case_out;
rewrite Out;
simpl.
rewrite type_of_params_make_in_arg;
auto.
erewrite find_class_name;
eauto.
-
destruct EvalStep as (? &
E & ?);
rewrite E.
eexists;
split.
+
eapply exec_Scall;
simpl;
eauto;
simpl;
eauto using eval_exprlist.
unfold type_of_function.
destruct StepSpec as (
P_f &
R_f &
CC_f &?).
rewrite P_f,
R_f,
CC_f;
unfold case_out;
rewrite Out;
simpl.
rewrite type_of_params_make_in_arg;
auto.
erewrite find_class_name;
eauto.
+
simpl;
apply PTree.gss.
-
destruct EvalStep as (?&?&?&?&?&?&?).
eexists;
split;
auto.
eapply exec_Scall;
simpl;
eauto;
simpl;
eauto 7
using eval_exprlist.
unfold type_of_function.
destruct StepSpec as (
P_f &
R_f &
CC_f &?).
rewrite P_f,
R_f,
CC_f;
unfold case_out;
rewrite Out;
simpl.
rewrite type_of_params_make_in_arg;
auto.
erewrite find_class_name,
find_method_name;
eauto.
unfold type_of_inst_p;
auto.
}
eexists le2,
m_Sn;
split;
auto.
repeat eapply exec_Sseq_1;
eauto.
eapply exec_write;
eauto.
unfold case_out;
destruct_list main_step.(
m_out)
as (?, ?) ? ?:
Outs;
auto;
unfold case_out in EvalStep;
rewrite Outs in EvalStep.
-
destruct EvalStep as (?&
E & ?).
rewrite E in *;
eauto.
-
destruct EvalStep as (
ve &
step_b &
step_co & ?&?&?&?).
exists ve,
step_b,
step_co;
intuition;
eauto.
Qed.
Section MainCorrectness.
Variables (
me0 :
menv)
(
reset_f :
function)
(
e :
Clight.env)
(
m_main :
mem).
Hypothesis (
ResetCall :
stmt_call_eval prog mempty main_node reset []
me0 [])
(
WTme0 :
wt_mem me0 prog_main c_main)
(
StepLoop :
loop_call prog main_node step (
fun n =>
map Some (
ins n)) (
fun n =>
map Some (
outs n)) 0
me0)
(
ResetSpec :
method_spec c_main main_reset prog reset_f)
(
He :
out_step_env e)
(
Hm_main :
if lt_dec 1 (
length (
m_out main_step))
then
exists step_b step_co,
gcenv ! (
prefix_fun step main_node) =
Some step_co
/\
e !
out_step =
Some (
step_b,
t_out_step)
/\
m_main |=
staterep gcenv prog main_node mempty sb Z0
**
fieldsrep gcenv vempty step_co.(
co_members)
step_b
else m_main |=
staterep gcenv prog main_node mempty sb Z0).
Lemma reset_no_output:
m_out main_reset = [].
Proof.
Lemma reset_no_input:
m_in main_reset = [].
Proof.
Correctness of dostep relatively to loop_call *
Lemma dostep_imp:
exists m0,
eval_funcall_fe function_entry2 tge m_main (
Internal reset_f)
[
var_ptr sb]
E0 m0 Vundef
/\
dostep e 0
m0.
Proof.
pose proof ResetCall as ResetCall'.
apply reset_correct in ResetCall'.
unfold call_spec,
case_out in ResetCall'.
rewrite reset_no_output in ResetCall'.
erewrite find_class_name in ResetCall';
eauto.
rewrite <-
Ptrofs.unsigned_zero in Hm_main.
set (
R :=
fun n m =>
case_out main_step
(
exists me,
loop_call prog main_node step
(
fun n =>
map Some (
ins n)) (
fun n =>
map Some (
outs n))
n me
/\
wt_mem me prog_main c_main
/\
m |=
staterep gcenv prog main_node me sb 0)
(
fun _ _ =>
exists me,
loop_call prog main_node step
(
fun n =>
map Some (
ins n)) (
fun n =>
map Some (
outs n))
n me
/\
wt_mem me prog_main c_main
/\
m |=
staterep gcenv prog main_node me sb 0 )
(
fun _ =>
exists me step_b step_co,
loop_call prog main_node step
(
fun n =>
map Some (
ins n)) (
fun n =>
map Some (
outs n))
n me
/\
wt_mem me prog_main c_main
/\
gcenv ! (
prefix_fun step main_node) =
Some step_co
/\
e !
out_step =
Some (
step_b,
t_out_step)
/\
m |=
staterep gcenv prog main_node me sb 0
**
fieldsrep gcenv vempty (
co_members step_co)
step_b)).
assert (
dostepCase R e).
{
unfold R;
unfold dostepCase,
case_out.
intros n m_n Spec.
destruct_list (
m_out main_step)
as (?,?) (?,?) ? :
Hout;
[
destruct Spec as (? &
Dostep &
Hwt &
Hm_n)
|
destruct Spec as (? &
Dostep &
Hwt &
Hm_n)
|
destruct Spec as (? &
step_b' &
step_co' &
Dostep &
Hwt & ? & ? &
Hm_n)];
destruct Dostep as [?
me_n me_Sn EvalStep dostep];
assert (
wt_mem me_Sn prog_main c_main)
by (
eapply pres_sem_stmt_call with (
f :=
step);
eauto;
rewrite Forall2_map_1;
simpl;
apply Hwt_ins);
eapply step_correct in EvalStep;
auto;
unfold call_spec,
case_out in EvalStep;
rewrite Hout in EvalStep;
erewrite find_class_name in EvalStep;
eauto;
rewrite sepemp_right, <-
Ptrofs.unsigned_zero in Hm_n;
try rewrite sep_assoc in Hm_n;
[
eapply EvalStep in Hm_n as (
m_Sn &
step_f' & ? & ? &
Hm_Sn)
|
eapply EvalStep in Hm_n as (
m_Sn &
step_f' & ? & ? & ? & ? &
Hm_Sn)
|
eapply EvalStep in Hm_n as (
ve_f &
m_Sn &
step_f' & ? & ? & ? &
Hm_Sn)];
auto;
try erewrite find_method_name;
eauto;
assert (
step_f =
step_f')
by (
eapply method_spec_eq;
eauto);
subst step_f'.
-
exists m_Sn;
split;
eauto.
exists me_Sn;
intuition.
now rewrite <-
sepemp_right,
Ptrofs.unsigned_zero in Hm_Sn.
-
exists m_Sn;
split;
eauto.
exists me_Sn;
intuition.
now rewrite <-
sepemp_right,
Ptrofs.unsigned_zero in Hm_Sn.
-
exists m_Sn;
split;
eauto.
+
exists ve_f,
step_b',
step_co';
intuition.
now apply sep_proj2,
sep_proj1 in Hm_Sn.
+
exists me_Sn,
step_b',
step_co';
intuition.
rewrite <-
sepemp_right,
Ptrofs.unsigned_zero in Hm_Sn.
eapply sep_imp;
eauto.
apply fieldsrep_any_empty.
}
cases;
[
destruct Hm_main as (
step_b &
step_co & ? & ? &
Hm_main');
clear Hm_main;
rename Hm_main'
into Hm_main
|
rewrite sepemp_right in Hm_main];
eapply ResetCall'
in Hm_main as (
m0 &
reset_f' & ? & ? &
Hm0);
auto;
assert (
reset_f =
reset_f')
by (
eapply method_spec_eq;
eauto);
subst reset_f';
exists m0;
split;
auto;
apply dostep_coind with (
R :=
R);
auto;
unfold R,
case_out;
destruct_list (
m_out main_step)
as (?,?) (?,?) ?;
simpl in *;
try omega.
-
exists me0,
step_b,
step_co;
intuition.
-
exists me0;
intuition.
now rewrite <-
sepemp_right,
Ptrofs.unsigned_zero in Hm0.
-
exists me0;
intuition.
now rewrite <-
sepemp_right,
Ptrofs.unsigned_zero in Hm0.
Qed.
Let reset_name :=
Evar (
prefix_fun reset main_node).
Corollary exec_reset:
exists m0,
exec_stmt_fe function_entry2 tge e
le_main m_main (
reset_call main_node)
E0
le_main m0 Out_normal
/\
dostep e 0
m0.
Proof.
Corollary of exec_body: dostep implies the infinte looping* *
execution *
We switch to the small-step semantics since the big-step *
one cannot distinguish between Reacts and Diverges *
Section TraceInf.
Hypothesis Step_in_out_spec:
main_step.(
m_in) <> [] \/
main_step.(
m_out) <> [].
Fact Len_ins:
forall n :
nat,
Datatypes.length (
ins n) =
Datatypes.length (
m_in main_step).
Proof.
Fact Len_outs:
forall n :
nat,
Datatypes.length (
outs n) =
Datatypes.length (
m_out main_step).
Proof.
Definition trace_main_step (
n:
nat):
traceinf :=
trace_step main_step ins outs Step_in_out_spec Len_ins Len_outs n.
Let main_state F :=
Clight.State F (
main_loop false main_node main_step).
Lemma reactive_loop:
forall n F e m le k,
dostep e n m ->
Forever_reactive (
semantics2 tprog) (
main_state F k e le m) (
trace_main_step n).
Proof.
We show that the whole program is reactive, with the *
correct infinite trace *
Section Behavior.
Variable (
m0 :
mem).
Hypothesis Init:
Genv.init_mem tprog =
Some m0.
Let prog_state :=
Clight.Callstate (
Internal main_f) []
Kstop m0.
Lemma initial_state_main:
Clight.initial_state tprog prog_state.
Proof.
Lemma reacts:
function_entry2 tge main_f []
m0 e le_main m_main ->
program_behaves (
semantics2 tprog) (
Reacts (
trace_main_step 0)).
Proof.
End Behavior.
End TraceInf.
End MainCorrectness.
End dostep.
Lemma out_step_env_empty:
out_step_env empty_env.
Proof.
intros ???
Hin;
rewrite PTree.gempty in Hin;
discriminate.
Qed.
Lemma out_step_env_set_out_step:
forall b t,
out_step_env (
PTree.set out_step (
b,
t)
empty_env).
Proof.
Program Theorem correctness:
forall ins outs me0
(
WTins :
forall n,
wt_vals (
ins n) (
m_in main_step))
(
WTouts :
forall n,
wt_vals (
outs n) (
m_out main_step))
(
Step_in_out_spec :
m_in main_step <> [] \/
m_out main_step <> []),
stmt_call_eval prog mempty main_node reset []
me0 [] ->
loop_call prog main_node step (
fun n =>
map Some (
ins n)) (
fun n =>
map Some (
outs n)) 0
me0 ->
wt_mem me0 prog_main c_main ->
program_behaves (
semantics2 tprog) (
Reacts (
trace_main_step ins outs _ _ _ 0)).
Proof.
End PRESERVATION.