Library link_ext
Require Import compcert.AST.
Require Import veric.base.
Require Import veric.sim.
Require Import List.
Section MODULAR_PROGRAMS.
Inductive globdef (F V: Type) : Type :=
| Gfun (f: F)
| Gvar (v: globvar V).
Record Module (F V:Type) := mkmodule {
id_defs: list (ident * globdef F V);
id_def_unique: forall f gdef1 gdef2,
In (f,gdef1) id_defs -> In (f,gdef2) id_defs -> gdef1=gdef2
}.
Record Module'(F V:Type) := mkmodule' {
extern_defs: list (ident * globdef F V);
exported_ids: list ident;
intern_defs: list (ident * globdef F V);
mod_defs_unique: forall f gdef1 gdef2,
In (f,gdef1) (extern_defs ++ intern_defs) ->
In (f,gdef2) (extern_defs ++ intern_defs) -> gdef1=gdef2;
exporteds_are_extern: forall f, In f exported_ids -> exists d, In (f,d) extern_defs;
interns_not_extern: forall f d, In (f,d) intern_defs -> ~ In (f,d) extern_defs
}.
Fixpoint walkFuns {F V} (l: list (ident * globdef F V)) : list (ident * F) :=
match l with nil => nil
| (id,d)::t => match d with Gfun f => (id,f) :: (walkFuns t) | Gvar _ => walkFuns t end
end.
Fixpoint walkVars {F V} (l: list (ident * globdef F V)) : list (ident * globvar V) :=
match l with nil => nil
| (id,d)::t => match d with Gfun _ => (walkVars t) | Gvar v => (id,v) :: (walkVars t) end
end.
Definition mod_funs {F V} (M : Module F V): list (ident * F) := walkFuns (id_defs _ _ M).
Definition mod_vars {F V} (M : Module F V): list (ident * globvar V) := walkVars (id_defs _ _ M).
Definition mod_funct_names {F V} (M : Module F V): list ident:= List.map fst (mod_funs M).
Definition mod_var_names {F V} (M : Module F V): list ident:= List.map fst (mod_vars M).
Fixpoint lookup_ {F V} (l:list (ident * globdef F V)) f :=
match l with nil => None
| cons HD TL => match HD with (ff,dd) => if peq ff f then Some dd else lookup_ TL f end
end.
Lemma lookup_In_funs: forall {F V} (MOD : Module F V) id f,
lookup_ (id_defs F V MOD) id = Some (Gfun F V f)->
In (id,f) (mod_funs MOD).
Proof. intros.
unfold mod_funs. remember (id_defs F V MOD) as vl. clear Heqvl MOD.
induction vl; simpl in *. inv H.
destruct a. destruct (peq i id); subst. inv H. left; trivial.
apply IHvl in H. destruct g. right. apply H. apply H.
Qed.
Lemma lookup_In_vars: forall {F V} (MOD : Module F V) id v,
lookup_ (id_defs F V MOD) id = Some (Gvar F V v)->
In (id,v) (mod_vars MOD).
Proof. intros.
unfold mod_vars. remember (id_defs F V MOD) as vl. clear Heqvl MOD.
induction vl; simpl in *. inv H.
destruct a. destruct (peq i id); subst. inv H. left; trivial.
apply IHvl in H. destruct g. apply H. right. apply H.
Qed.
Definition M_defines' {F V} (M:Module' F V) (f:ident): Prop := In f M.(exported_ids _ _ ).
Definition M_lookup' {F V} (M:Module' F V) (f:ident) : option (globdef F V) :=
lookup_ ((extern_defs _ _ M) ++ (intern_defs _ _ M)) f.
Definition M_defines {F V} (M:Module F V) (f:ident): Prop :=
exists gdef, In (f,gdef) M.(id_defs _ _ ).
Definition M_lookup {F V} (M:Module F V) (f:ident) : option (globdef F V) :=
lookup_ (id_defs _ _ M) f.
Lemma M_defines_iff_M_lookup: forall F V (M:Module F V) f,
M_defines M f <-> exists d, M_lookup M f = Some d.
Proof. intros. unfold M_defines. unfold M_lookup. destruct M as [l U]. simpl in *. clear U.
induction l; simpl; split; intros.
destruct H. contradiction.
destruct H. inv H.
destruct H.
destruct H; subst.
exists x. apply peq_true.
destruct a as [ff dd]. destruct IHl as [? _]. destruct H0. exists x; assumption.
remember (peq ff f ) as b. destruct b. exists dd; trivial.
exists x0. trivial.
destruct H. destruct a as [ff dd].
remember (peq ff f ) as b. destruct b. inv H. exists x; left; trivial.
destruct IHl as [_ ?]. destruct H0. exists x; assumption.
exists x0. right. trivial.
Qed.
Record PreProgram := mkPreProgram {
FParams: nat -> Type;
VParams: nat -> Type;
NumModules : nat;
Modules: forall i, (Module (FParams i) (VParams i));
PP_find: ident -> option nat;
PP_find_None: forall f, PP_find f = None <-> (forall n, (n < NumModules)%nat -> ~M_defines (Modules n) f);
PP_find_Some: forall f n, PP_find f = Some n <-> ((n < NumModules)%nat /\ M_defines (Modules n) f)
}.
Lemma PP_find_LT: forall (PP:PreProgram) f n, PP_find PP f = Some n ->
nat_compare n (NumModules PP) = Lt.
Proof. intros. apply nat_compare_lt. apply PP_find_Some in H. apply H. Qed.
Lemma PP_no_duplicates: forall (PP:PreProgram) (f:ident) n1 n2,
M_defines (Modules PP n1) f -> (n1 < NumModules PP)%nat ->
M_defines (Modules PP n2) f -> (n2 < NumModules PP)%nat -> n1=n2.
Proof.
intros.
assert (N1: PP_find PP f = Some n1). apply (PP_find_Some PP). split; assumption.
assert (N2: PP_find PP f = Some n2). apply (PP_find_Some PP). split; assumption.
rewrite N1 in N2. congruence.
Qed.
Definition PP_getFParam (PP:PreProgram) f: Type :=
match PP_find PP f with
None => False
| Some n => match nat_compare n (NumModules PP) with
Lt => FParams PP n
| _ => False
end
end.
Definition PP_getVParam (PP:PreProgram) f: Type :=
match PP_find PP f with
None => False
| Some n => match nat_compare n (NumModules PP) with
Lt => VParams PP n
| _ => False
end
end.
Definition PP_lookup (PP:PreProgram) f n: option (globdef (FParams PP n) (VParams PP n)) :=
match nat_compare n (NumModules PP) with
Lt => M_lookup (Modules PP n) f
| _ => None
end.
Lemma PP_lookup_inv: forall PP f n d, PP_lookup PP f n = Some d -> (n < NumModules PP)%nat /\ M_lookup (Modules PP n) f = Some d.
Proof. intros. unfold PP_lookup in H.
remember (nat_compare n (NumModules PP)) as b.
destruct b; try inv H.
split; trivial.
apply nat_compare_lt. rewrite Heqb. trivial.
Qed.
Lemma PP_lookup_intro: forall PP f n, (n < NumModules PP)%nat -> PP_lookup PP f n = M_lookup (Modules PP n) f.
Proof. intros. unfold PP_lookup. apply nat_compare_lt in H. rewrite H. trivial. Qed.
Lemma PP_find_PP_lookup1: forall PP f n, PP_find PP f = Some n -> exists d, PP_lookup PP f n = Some d.
Proof. intros. apply (PP_find_Some PP f n) in H. destruct H.
apply M_defines_iff_M_lookup in H0. destruct H0. exists x.
apply nat_compare_lt in H. unfold PP_lookup. rewrite H. assumption.
Qed.
Lemma PP_find_PP_lookup2: forall PP f, PP_find PP f = None-> forall n, (n < NumModules PP)%nat -> PP_lookup PP f n = None.
Proof. intros. destruct (PP_find_None PP f) as [Z1 _].
assert (Z2 := Z1 H _ H0).
unfold PP_lookup. apply nat_compare_lt in H0. rewrite H0.
remember (M_lookup (Modules PP n) f) as b.
destruct b; trivial.
exfalso. apply Z2. apply M_defines_iff_M_lookup. exists g. rewrite Heqb. trivial.
Qed.
Record LinkedProgram:= {
PreProg: PreProgram;
main : ident;
main_defined: exists n, PP_find PreProg main = Some n
}.
End MODULAR_PROGRAMS.
Section LINKED_SEMANTICS.
Definition get_ident (ef:external_function * signature * list val): option ident :=
match ef with ((f,_),_) =>
match f with
EF_external id _ => Some id
| _ => None
end
end.
Variable M:Type. Record RecSem (F V:Type) := mkRecSem {
coreTP :Type;
dataTP: Type;
ssem: @CoreSemantics (Genv.t F V) coreTP M dataTP
}.
Variable mkSem: forall {F V} (Mod: Module F V), RecSem F V.
Definition SemTable (PP:PreProgram) (n:nat) : option (RecSem (FParams PP n) (VParams PP n)) :=
match nat_compare n (NumModules PP) with
Lt => Some (mkSem _ _ (Modules PP n))
| _ => None
end.
Variable Genvs: forall {F V} (Mod: Module F V), Genv.t F V.
Definition GenvsDom (PP:PreProgram): Prop := forall n f d,
(n < NumModules PP)%nat -> (M_lookup (Modules PP n) f = Some d-> exists b, Genv.find_symbol (Genvs _ _ (Modules PP n)) f = Some b).
Definition Genvs_wellshared (PP:PreProgram): Prop := forall n1 f1 d1 n2 f2 d2,
(n1 < NumModules PP)%nat -> (M_lookup (Modules PP n1) f1 = Some d1) ->
(n2 < NumModules PP)%nat -> (M_lookup (Modules PP n2) f2 = Some d2) ->
((Genv.find_symbol (Genvs _ _ (Modules PP n1)) f1 = Genv.find_symbol (Genvs _ _ (Modules PP n2)) f2) <-> (f1=f2)).
Inductive RunningCore:=
runCore: forall {G C D}, @CoreSemantics G C M D -> G -> C -> RunningCore.
Definition getCore (PP:PreProgram) (ef: external_function * signature * list val): option RunningCore :=
match ef with (_,args) =>
match (get_ident ef) with None => None
| Some f =>
match PP_find PP f with None => None
| Some n => match SemTable PP n with
None => None
| Some CR => let g := Genvs _ _ (Modules PP n)
in match Genv.find_symbol g f with None => None
| Some b => match make_initial_core (ssem _ _ CR) g (Vptr b Int.zero) args with
None => None
| Some c => Some (runCore (ssem _ _ CR) g c)
end
end
end
end
end
end.
Definition args_ok (PP:PreProgram) f args :=
forall n b, Genv.find_symbol (Genvs _ _ (Modules PP n)) f = Some b ->
exists c,
make_initial_core
(ssem (FParams PP n) (VParams PP n) (mkSem _ _ (Modules PP n)))
(Genvs _ _ (Modules PP n)) (Vptr b Int.zero) args = Some c.
Lemma getCore_succeeds: forall PP (PP_H1: GenvsDom PP) (PP_H2: Genvs_wellshared PP)
f sig args n, PP_find PP f = Some n -> args_ok PP f args ->
exists RC, getCore PP (EF_external f sig, sig, args) = Some RC.
Proof. intros.
unfold getCore. simpl. rewrite H. unfold SemTable.
assert (X:= PP_find_LT _ _ _ H).
rewrite X.
apply PP_find_PP_lookup1 in H. destruct H as [d XX].
destruct (PP_lookup_inv _ _ _ _ XX) as [XX1 XX2].
destruct (PP_H1 _ _ _ XX1 XX2) as [b Hb]. rewrite Hb.
apply H0 in Hb. destruct Hb as [c Hc]. rewrite Hc. eexists. reflexivity.
Qed.
Definition LinkCore:Type := list RunningCore.
Variable PP:PreProgram.
Inductive LinkCoreStep: unit -> LinkCore -> M -> LinkCore -> M -> Prop :=
link_step: forall {G C D} (Sem:@CoreSemantics G C M D) q m q' m' stack c c' ge,
q = runCore Sem ge c ->
corestep Sem ge c m c' m' ->
q' = runCore Sem ge c' ->
LinkCoreStep tt (q::stack) m (q'::stack) m'
| link_call: forall {G C D} (Sem:@CoreSemantics G C M D) q m q' m' stack c f sig args ge,
q = runCore Sem ge c ->
at_external Sem c = Some(f,sig,args) ->
getCore PP (f, sig, args) = Some q' ->
LinkCoreStep tt (q::stack) m (q'::q::stack) m'
| link_ret: forall {G' C' D'} (Sem':@CoreSemantics G' C' M D') {G C D} (Sem:@CoreSemantics G C M D)
q m q' m' stack c f sig args g g' c' cc qq v,
q' = runCore Sem' g' c' ->
safely_halted Sem' g' c' = Some v ->
q = runCore Sem g c ->
at_external Sem c = Some(f,sig,args) ->
after_external Sem (Some v) c = Some cc ->
qq = runCore Sem g cc ->
LinkCoreStep tt (q'::q::stack) m (qq::stack) m'.
Definition Link_at_external (stack:LinkCore): option (external_function * signature * list val) :=
match stack with nil => None
| (runCore G C D Sem ge c) :: _ => match at_external Sem c with
None => None
| Some(f,sig,args) => match getCore PP (f, sig, args) with
None => Some (f, sig, args)
| Some q => None
end
end
end.
Lemma Link_corestep_not_at_external: forall g m q m' q',
LinkCoreStep g q m q' m' -> Link_at_external q = None.
Proof. intros.
inversion H; subst; simpl in *.
apply corestep_not_at_external in H1. rewrite H1. trivial.
rewrite H1. rewrite H2. trivial.
assert (Z1:= at_external_halted_excl Sem' g' c').
destruct Z1.
rewrite H0. trivial.
rewrite H1 in H0. inv H0.
Qed.
Definition Link_safely_halted (_:unit) (stack:LinkCore): option val :=
match stack with nil => None
| (runCore _ _ _ Sem ge c) :: nil => safely_halted Sem ge c
| _ => None
end.
Lemma Link_corestep_not_halted: forall g m q m' q',
LinkCoreStep g q m q' m' -> Link_safely_halted g q = None.
Proof. intros.
inversion H; subst; simpl in *.
apply corestep_not_halted in H1. rewrite H1. destruct stack; trivial.
assert (Z1:= at_external_halted_excl Sem ge c).
destruct Z1. rewrite H1 in H0. inv H0.
rewrite H0. destruct stack; trivial.
trivial.
Qed.
Lemma Link_at_external_halted_excl: forall g q,
Link_at_external q = None \/ Link_safely_halted g q = None.
Proof. intros.
destruct q; simpl.
left; trivial.
destruct r; simpl. rename c into Sem. rename c0 into c.
destruct (at_external_halted_excl Sem g0 c); rewrite H.
left; trivial.
right. destruct q; trivial.
Qed.
Definition Link_after_external (rv:option val) (stack: LinkCore) : option LinkCore :=
match stack with nil => None
| (runCore _ _ _ Sem ge c) :: stk => match after_external Sem rv c with
None => None
| Some cc => Some ((runCore Sem ge cc) :: stk)
end
end.
Variable D_values: forall i, dataTP _ _ (mkSem _ _ (Modules PP i)).
Definition Link_initial_mem (D:Type) (_:unit) (m: M) (d: D) : Prop :=
forall i, (i < NumModules PP)%nat -> initial_mem (ssem _ _ (mkSem _ _ (Modules PP i))) (Genvs _ _ (Modules PP i)) m (D_values i).
Variable Link_make_initial_core: unit -> val -> list val -> option LinkCore.
Definition LinkSem (D:Type) : CoreSemantics unit LinkCore M D.
eapply Build_CoreSemantics with (at_external := Link_at_external)(safely_halted := Link_safely_halted)(corestep:=LinkCoreStep).
apply Link_initial_mem.
apply Link_make_initial_core.
apply Link_after_external.
apply Link_corestep_not_at_external.
apply Link_corestep_not_halted.
apply Link_at_external_halted_excl.
Defined.
Parameter PP_H1: GenvsDom PP.
Parameter PP_H2: Genvs_wellshared PP.
End LINKED_SEMANTICS.
Check LinkSem.
Require Import veric.base.
Require Import veric.sim.
Require Import List.
Section MODULAR_PROGRAMS.
Inductive globdef (F V: Type) : Type :=
| Gfun (f: F)
| Gvar (v: globvar V).
Record Module (F V:Type) := mkmodule {
id_defs: list (ident * globdef F V);
id_def_unique: forall f gdef1 gdef2,
In (f,gdef1) id_defs -> In (f,gdef2) id_defs -> gdef1=gdef2
}.
Record Module'(F V:Type) := mkmodule' {
extern_defs: list (ident * globdef F V);
exported_ids: list ident;
intern_defs: list (ident * globdef F V);
mod_defs_unique: forall f gdef1 gdef2,
In (f,gdef1) (extern_defs ++ intern_defs) ->
In (f,gdef2) (extern_defs ++ intern_defs) -> gdef1=gdef2;
exporteds_are_extern: forall f, In f exported_ids -> exists d, In (f,d) extern_defs;
interns_not_extern: forall f d, In (f,d) intern_defs -> ~ In (f,d) extern_defs
}.
Fixpoint walkFuns {F V} (l: list (ident * globdef F V)) : list (ident * F) :=
match l with nil => nil
| (id,d)::t => match d with Gfun f => (id,f) :: (walkFuns t) | Gvar _ => walkFuns t end
end.
Fixpoint walkVars {F V} (l: list (ident * globdef F V)) : list (ident * globvar V) :=
match l with nil => nil
| (id,d)::t => match d with Gfun _ => (walkVars t) | Gvar v => (id,v) :: (walkVars t) end
end.
Definition mod_funs {F V} (M : Module F V): list (ident * F) := walkFuns (id_defs _ _ M).
Definition mod_vars {F V} (M : Module F V): list (ident * globvar V) := walkVars (id_defs _ _ M).
Definition mod_funct_names {F V} (M : Module F V): list ident:= List.map fst (mod_funs M).
Definition mod_var_names {F V} (M : Module F V): list ident:= List.map fst (mod_vars M).
Fixpoint lookup_ {F V} (l:list (ident * globdef F V)) f :=
match l with nil => None
| cons HD TL => match HD with (ff,dd) => if peq ff f then Some dd else lookup_ TL f end
end.
Lemma lookup_In_funs: forall {F V} (MOD : Module F V) id f,
lookup_ (id_defs F V MOD) id = Some (Gfun F V f)->
In (id,f) (mod_funs MOD).
Proof. intros.
unfold mod_funs. remember (id_defs F V MOD) as vl. clear Heqvl MOD.
induction vl; simpl in *. inv H.
destruct a. destruct (peq i id); subst. inv H. left; trivial.
apply IHvl in H. destruct g. right. apply H. apply H.
Qed.
Lemma lookup_In_vars: forall {F V} (MOD : Module F V) id v,
lookup_ (id_defs F V MOD) id = Some (Gvar F V v)->
In (id,v) (mod_vars MOD).
Proof. intros.
unfold mod_vars. remember (id_defs F V MOD) as vl. clear Heqvl MOD.
induction vl; simpl in *. inv H.
destruct a. destruct (peq i id); subst. inv H. left; trivial.
apply IHvl in H. destruct g. apply H. right. apply H.
Qed.
Definition M_defines' {F V} (M:Module' F V) (f:ident): Prop := In f M.(exported_ids _ _ ).
Definition M_lookup' {F V} (M:Module' F V) (f:ident) : option (globdef F V) :=
lookup_ ((extern_defs _ _ M) ++ (intern_defs _ _ M)) f.
Definition M_defines {F V} (M:Module F V) (f:ident): Prop :=
exists gdef, In (f,gdef) M.(id_defs _ _ ).
Definition M_lookup {F V} (M:Module F V) (f:ident) : option (globdef F V) :=
lookup_ (id_defs _ _ M) f.
Lemma M_defines_iff_M_lookup: forall F V (M:Module F V) f,
M_defines M f <-> exists d, M_lookup M f = Some d.
Proof. intros. unfold M_defines. unfold M_lookup. destruct M as [l U]. simpl in *. clear U.
induction l; simpl; split; intros.
destruct H. contradiction.
destruct H. inv H.
destruct H.
destruct H; subst.
exists x. apply peq_true.
destruct a as [ff dd]. destruct IHl as [? _]. destruct H0. exists x; assumption.
remember (peq ff f ) as b. destruct b. exists dd; trivial.
exists x0. trivial.
destruct H. destruct a as [ff dd].
remember (peq ff f ) as b. destruct b. inv H. exists x; left; trivial.
destruct IHl as [_ ?]. destruct H0. exists x; assumption.
exists x0. right. trivial.
Qed.
Record PreProgram := mkPreProgram {
FParams: nat -> Type;
VParams: nat -> Type;
NumModules : nat;
Modules: forall i, (Module (FParams i) (VParams i));
PP_find: ident -> option nat;
PP_find_None: forall f, PP_find f = None <-> (forall n, (n < NumModules)%nat -> ~M_defines (Modules n) f);
PP_find_Some: forall f n, PP_find f = Some n <-> ((n < NumModules)%nat /\ M_defines (Modules n) f)
}.
Lemma PP_find_LT: forall (PP:PreProgram) f n, PP_find PP f = Some n ->
nat_compare n (NumModules PP) = Lt.
Proof. intros. apply nat_compare_lt. apply PP_find_Some in H. apply H. Qed.
Lemma PP_no_duplicates: forall (PP:PreProgram) (f:ident) n1 n2,
M_defines (Modules PP n1) f -> (n1 < NumModules PP)%nat ->
M_defines (Modules PP n2) f -> (n2 < NumModules PP)%nat -> n1=n2.
Proof.
intros.
assert (N1: PP_find PP f = Some n1). apply (PP_find_Some PP). split; assumption.
assert (N2: PP_find PP f = Some n2). apply (PP_find_Some PP). split; assumption.
rewrite N1 in N2. congruence.
Qed.
Definition PP_getFParam (PP:PreProgram) f: Type :=
match PP_find PP f with
None => False
| Some n => match nat_compare n (NumModules PP) with
Lt => FParams PP n
| _ => False
end
end.
Definition PP_getVParam (PP:PreProgram) f: Type :=
match PP_find PP f with
None => False
| Some n => match nat_compare n (NumModules PP) with
Lt => VParams PP n
| _ => False
end
end.
Definition PP_lookup (PP:PreProgram) f n: option (globdef (FParams PP n) (VParams PP n)) :=
match nat_compare n (NumModules PP) with
Lt => M_lookup (Modules PP n) f
| _ => None
end.
Lemma PP_lookup_inv: forall PP f n d, PP_lookup PP f n = Some d -> (n < NumModules PP)%nat /\ M_lookup (Modules PP n) f = Some d.
Proof. intros. unfold PP_lookup in H.
remember (nat_compare n (NumModules PP)) as b.
destruct b; try inv H.
split; trivial.
apply nat_compare_lt. rewrite Heqb. trivial.
Qed.
Lemma PP_lookup_intro: forall PP f n, (n < NumModules PP)%nat -> PP_lookup PP f n = M_lookup (Modules PP n) f.
Proof. intros. unfold PP_lookup. apply nat_compare_lt in H. rewrite H. trivial. Qed.
Lemma PP_find_PP_lookup1: forall PP f n, PP_find PP f = Some n -> exists d, PP_lookup PP f n = Some d.
Proof. intros. apply (PP_find_Some PP f n) in H. destruct H.
apply M_defines_iff_M_lookup in H0. destruct H0. exists x.
apply nat_compare_lt in H. unfold PP_lookup. rewrite H. assumption.
Qed.
Lemma PP_find_PP_lookup2: forall PP f, PP_find PP f = None-> forall n, (n < NumModules PP)%nat -> PP_lookup PP f n = None.
Proof. intros. destruct (PP_find_None PP f) as [Z1 _].
assert (Z2 := Z1 H _ H0).
unfold PP_lookup. apply nat_compare_lt in H0. rewrite H0.
remember (M_lookup (Modules PP n) f) as b.
destruct b; trivial.
exfalso. apply Z2. apply M_defines_iff_M_lookup. exists g. rewrite Heqb. trivial.
Qed.
Record LinkedProgram:= {
PreProg: PreProgram;
main : ident;
main_defined: exists n, PP_find PreProg main = Some n
}.
End MODULAR_PROGRAMS.
Section LINKED_SEMANTICS.
Definition get_ident (ef:external_function * signature * list val): option ident :=
match ef with ((f,_),_) =>
match f with
EF_external id _ => Some id
| _ => None
end
end.
Variable M:Type. Record RecSem (F V:Type) := mkRecSem {
coreTP :Type;
dataTP: Type;
ssem: @CoreSemantics (Genv.t F V) coreTP M dataTP
}.
Variable mkSem: forall {F V} (Mod: Module F V), RecSem F V.
Definition SemTable (PP:PreProgram) (n:nat) : option (RecSem (FParams PP n) (VParams PP n)) :=
match nat_compare n (NumModules PP) with
Lt => Some (mkSem _ _ (Modules PP n))
| _ => None
end.
Variable Genvs: forall {F V} (Mod: Module F V), Genv.t F V.
Definition GenvsDom (PP:PreProgram): Prop := forall n f d,
(n < NumModules PP)%nat -> (M_lookup (Modules PP n) f = Some d-> exists b, Genv.find_symbol (Genvs _ _ (Modules PP n)) f = Some b).
Definition Genvs_wellshared (PP:PreProgram): Prop := forall n1 f1 d1 n2 f2 d2,
(n1 < NumModules PP)%nat -> (M_lookup (Modules PP n1) f1 = Some d1) ->
(n2 < NumModules PP)%nat -> (M_lookup (Modules PP n2) f2 = Some d2) ->
((Genv.find_symbol (Genvs _ _ (Modules PP n1)) f1 = Genv.find_symbol (Genvs _ _ (Modules PP n2)) f2) <-> (f1=f2)).
Inductive RunningCore:=
runCore: forall {G C D}, @CoreSemantics G C M D -> G -> C -> RunningCore.
Definition getCore (PP:PreProgram) (ef: external_function * signature * list val): option RunningCore :=
match ef with (_,args) =>
match (get_ident ef) with None => None
| Some f =>
match PP_find PP f with None => None
| Some n => match SemTable PP n with
None => None
| Some CR => let g := Genvs _ _ (Modules PP n)
in match Genv.find_symbol g f with None => None
| Some b => match make_initial_core (ssem _ _ CR) g (Vptr b Int.zero) args with
None => None
| Some c => Some (runCore (ssem _ _ CR) g c)
end
end
end
end
end
end.
Definition args_ok (PP:PreProgram) f args :=
forall n b, Genv.find_symbol (Genvs _ _ (Modules PP n)) f = Some b ->
exists c,
make_initial_core
(ssem (FParams PP n) (VParams PP n) (mkSem _ _ (Modules PP n)))
(Genvs _ _ (Modules PP n)) (Vptr b Int.zero) args = Some c.
Lemma getCore_succeeds: forall PP (PP_H1: GenvsDom PP) (PP_H2: Genvs_wellshared PP)
f sig args n, PP_find PP f = Some n -> args_ok PP f args ->
exists RC, getCore PP (EF_external f sig, sig, args) = Some RC.
Proof. intros.
unfold getCore. simpl. rewrite H. unfold SemTable.
assert (X:= PP_find_LT _ _ _ H).
rewrite X.
apply PP_find_PP_lookup1 in H. destruct H as [d XX].
destruct (PP_lookup_inv _ _ _ _ XX) as [XX1 XX2].
destruct (PP_H1 _ _ _ XX1 XX2) as [b Hb]. rewrite Hb.
apply H0 in Hb. destruct Hb as [c Hc]. rewrite Hc. eexists. reflexivity.
Qed.
Definition LinkCore:Type := list RunningCore.
Variable PP:PreProgram.
Inductive LinkCoreStep: unit -> LinkCore -> M -> LinkCore -> M -> Prop :=
link_step: forall {G C D} (Sem:@CoreSemantics G C M D) q m q' m' stack c c' ge,
q = runCore Sem ge c ->
corestep Sem ge c m c' m' ->
q' = runCore Sem ge c' ->
LinkCoreStep tt (q::stack) m (q'::stack) m'
| link_call: forall {G C D} (Sem:@CoreSemantics G C M D) q m q' m' stack c f sig args ge,
q = runCore Sem ge c ->
at_external Sem c = Some(f,sig,args) ->
getCore PP (f, sig, args) = Some q' ->
LinkCoreStep tt (q::stack) m (q'::q::stack) m'
| link_ret: forall {G' C' D'} (Sem':@CoreSemantics G' C' M D') {G C D} (Sem:@CoreSemantics G C M D)
q m q' m' stack c f sig args g g' c' cc qq v,
q' = runCore Sem' g' c' ->
safely_halted Sem' g' c' = Some v ->
q = runCore Sem g c ->
at_external Sem c = Some(f,sig,args) ->
after_external Sem (Some v) c = Some cc ->
qq = runCore Sem g cc ->
LinkCoreStep tt (q'::q::stack) m (qq::stack) m'.
Definition Link_at_external (stack:LinkCore): option (external_function * signature * list val) :=
match stack with nil => None
| (runCore G C D Sem ge c) :: _ => match at_external Sem c with
None => None
| Some(f,sig,args) => match getCore PP (f, sig, args) with
None => Some (f, sig, args)
| Some q => None
end
end
end.
Lemma Link_corestep_not_at_external: forall g m q m' q',
LinkCoreStep g q m q' m' -> Link_at_external q = None.
Proof. intros.
inversion H; subst; simpl in *.
apply corestep_not_at_external in H1. rewrite H1. trivial.
rewrite H1. rewrite H2. trivial.
assert (Z1:= at_external_halted_excl Sem' g' c').
destruct Z1.
rewrite H0. trivial.
rewrite H1 in H0. inv H0.
Qed.
Definition Link_safely_halted (_:unit) (stack:LinkCore): option val :=
match stack with nil => None
| (runCore _ _ _ Sem ge c) :: nil => safely_halted Sem ge c
| _ => None
end.
Lemma Link_corestep_not_halted: forall g m q m' q',
LinkCoreStep g q m q' m' -> Link_safely_halted g q = None.
Proof. intros.
inversion H; subst; simpl in *.
apply corestep_not_halted in H1. rewrite H1. destruct stack; trivial.
assert (Z1:= at_external_halted_excl Sem ge c).
destruct Z1. rewrite H1 in H0. inv H0.
rewrite H0. destruct stack; trivial.
trivial.
Qed.
Lemma Link_at_external_halted_excl: forall g q,
Link_at_external q = None \/ Link_safely_halted g q = None.
Proof. intros.
destruct q; simpl.
left; trivial.
destruct r; simpl. rename c into Sem. rename c0 into c.
destruct (at_external_halted_excl Sem g0 c); rewrite H.
left; trivial.
right. destruct q; trivial.
Qed.
Definition Link_after_external (rv:option val) (stack: LinkCore) : option LinkCore :=
match stack with nil => None
| (runCore _ _ _ Sem ge c) :: stk => match after_external Sem rv c with
None => None
| Some cc => Some ((runCore Sem ge cc) :: stk)
end
end.
Variable D_values: forall i, dataTP _ _ (mkSem _ _ (Modules PP i)).
Definition Link_initial_mem (D:Type) (_:unit) (m: M) (d: D) : Prop :=
forall i, (i < NumModules PP)%nat -> initial_mem (ssem _ _ (mkSem _ _ (Modules PP i))) (Genvs _ _ (Modules PP i)) m (D_values i).
Variable Link_make_initial_core: unit -> val -> list val -> option LinkCore.
Definition LinkSem (D:Type) : CoreSemantics unit LinkCore M D.
eapply Build_CoreSemantics with (at_external := Link_at_external)(safely_halted := Link_safely_halted)(corestep:=LinkCoreStep).
apply Link_initial_mem.
apply Link_make_initial_core.
apply Link_after_external.
apply Link_corestep_not_at_external.
apply Link_corestep_not_halted.
apply Link_at_external_halted_excl.
Defined.
Parameter PP_H1: GenvsDom PP.
Parameter PP_H2: Genvs_wellshared PP.
End LINKED_SEMANTICS.
Check LinkSem.