Library mcertikos.multithread.lowrefins.E2PBThreadComposeData
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import I64Layer.
Require Import GlobalOracleProp.
Require Import DeviceStateDataType.
Require Import AuxSingleAbstractDataType.
Require Import SingleAbstractDataType.
Require Import SingleOracleDef.
Require Import SingleConfiguration.
Require Import ObjPHBThreadReplayFunction.
Require Import SoundnessAux.
Require Import BigLogThreadConfigFunction.
Require Import CalRealProcModule.
Require Import SingleOracleImpl.
Section SINGLECOMPOSEDATA.
Context `{real_params_ops : RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Local Instance s_oracle_prf : SingleOracle := s_oracle_prf.
Section MATCH.
Definition pperm_inject (ha_ppermtable : PPermT) (la_ppermtable : PPermT) : Prop :=
∀ i,
match ZMap.get i ha_ppermtable, ZMap.get i la_ppermtable with
| PGUndef, _ ⇒ True
| PGAlloc, PGAlloc ⇒ True
| PGHide ho, PGHide lo ⇒ ho = lo
| _, _ ⇒ False
end.
Definition B_GetContainerUsed´ (tid: Z) (cid : Z) (big_log: BigLogType) : bool :=
match big_log with
| BigUndef ⇒ false
| BigDef l ⇒ B_GetContainerUsed tid cid l
end.
Definition relate_AC_per_pd (id : Z) (sd : sharedData) (pd: privData) (ladt : AbstractDataType.RData) :=
if init sd then if B_GetContainerUsed´ id (CPU_ID sd) (big_log sd) then
if zeq id main_thread
then AC pd = ZMap.get id (AbstractDataType.AC ladt)
else if zlt_lt TOTAL_CPU id num_proc then AC pd = ZMap.get id (AbstractDataType.AC ladt)
else True
else if zlt_lt TOTAL_CPU id num_proc then AC pd = AC (thread_init_dproc id) else True
else if zeq id main_thread
then (AC pd) = ZMap.get id (AbstractDataType.AC ladt)
else if zlt_lt TOTAL_CPU id num_proc then AC pd = AC (thread_init_dproc id) else True.
Definition uctxt_bieq (huctx : UContext) (luctx: UContext) :=
match ZMap.get U_EIP huctx with
| Vint i ⇒ if Int.eq i (Int.repr 0) then
(∀ i, 0 ≤ i < UCTXT_SIZE →
i ≠ U_EIP →
ZMap.get i huctx = ZMap.get i luctx) ∧
(∃ v, ZMap.get U_EIP luctx = v)
else huctx = luctx
| Vundef ⇒ (∀ i, 0 ≤ i < UCTXT_SIZE →
i ≠ U_EIP →
ZMap.get i huctx = ZMap.get i luctx) ∧
(∃ v, ZMap.get U_EIP luctx = v)
| _ ⇒ False
end.
Definition relate_uctxt_per_pd (id : Z) (sd : sharedData) (pd: privData) (ladt : AbstractDataType.RData) :=
if init sd then if B_GetContainerUsed´ id (CPU_ID sd) (big_log sd) then
if zeq id main_thread
then uctxt_bieq (uctxt pd) (ZMap.get id (AbstractDataType.uctxt ladt))
else if zlt_lt TOTAL_CPU id num_proc then uctxt_bieq (uctxt pd)
(ZMap.get id (AbstractDataType.uctxt ladt))
else True
else if zlt_lt TOTAL_CPU id num_proc then uctxt pd = uctxt (thread_init_dproc id) else True
else if zeq id main_thread
then uctxt pd = ZMap.get id (AbstractDataType.uctxt ladt)
else if zlt_lt TOTAL_CPU id num_proc then uctxt pd = uctxt (thread_init_dproc id) else True.
Definition relate_SyncChanPool_per_pd (id : Z) (sd : sharedData) (pd: privData) (ladt : AbstractDataType.RData) :=
if (init sd) then
if B_inLock (CPU_ID sd) (big_log sd) then
if zeq id (proc_id sd)
then syncchpool pd = AbstractDataType.syncchpool ladt
else True
else match (big_log sd) with
| BigDef nil ⇒
syncchpool pd = real_syncchpool (ZMap.init SyncChanUndef)
| BigDef _ ⇒ True
| _ ⇒ False
end
else if zeq id main_thread
then syncchpool pd = (ZMap.init SyncChanUndef)
else syncchpool pd = real_syncchpool (ZMap.init SyncChanUndef).
Record E2PBThreadGenPerDInv (id : Z) (kctxt_val : KContext) (sd : sharedData) (pd : privData)
(ladt : AbstractDataType.RData) :=
mkE2PBThreadGenPerDInv {
dirty_page_per_thread_inv:
∀ res i, ZMap.get i (pperm pd) = PGUndef → ZMap.get res (HP pd) = ZMap.get res (FlatMem.free_page i (HP pd))
}.
Record relate_RData_per_pd (id : Z) (kctxt_val : KContext) (sd : sharedData) (pd : privData)
(ladt : AbstractDataType.RData) :=
mkrelate_RData_per_pd {
vmxinfo_re: vmxinfo sd = AbstractDataType.vmxinfo ladt;
CR3_re: CR3 sd = AbstractDataType.CR3 ladt;
pg_re: pg sd = AbstractDataType.pg ladt;
nps_re: nps sd = AbstractDataType.nps ladt;
init_re: init sd = AbstractDataType.init ladt;
lock_re: lock sd = AbstractDataType.lock ladt;
CPU_ID_re: CPU_ID sd = AbstractDataType.CPU_ID ladt;
cid_re: if init sd
then (ZMap.get (CPU_ID sd) (cid sd)) = (ZMap.get (AbstractDataType.CPU_ID ladt) (AbstractDataType.cid ladt))
else (ZMap.get (AbstractDataType.CPU_ID ladt) (AbstractDataType.cid ladt)) = 0 ∧
(if zle_lt 0 (CPU_ID sd) TOTAL_CPU
then (ZMap.get (CPU_ID sd) (cid sd)) = ((CPU_ID sd) + 1)
else (ZMap.get (CPU_ID sd) (cid sd)) = 0);
idpde_re: idpde sd = AbstractDataType.idpde ladt;
kctxt_re: kctxt_val= ZMap.get id (AbstractDataType.kctxt ladt);
big_log_re: big_log sd = AbstractDataType.big_log ladt;
big_oracle_re: big_oracle sd = AbstractDataType.big_oracle ladt;
flatmem_re: ∀ v ofs TY,
ZMap.get ((v × PgSize + ofs mod PgSize) / PgSize) (pperm pd) = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod PgSize) →
FlatMem.load TY (HP pd) (v × PgSize + ofs mod PgSize) =
FlatMem.load TY (AbstractDataType.HP ladt) (v × PgSize + ofs mod PgSize);
ikern_re: if zeq id (proc_id sd) then ikern pd = AbstractDataType.ikern ladt else ikern pd = true;
ihost_re: if zeq id (proc_id sd) then ihost pd = AbstractDataType.ihost ladt else ihost pd = true;
AC_re: relate_AC_per_pd id sd pd ladt;
ti_re: if zeq id (proc_id sd) then ti pd = AbstractDataType.ti ladt else ti pd = init_trap_info;
pperm_re: pperm_inject (pperm pd) (AbstractDataType.pperm ladt);
PT_re: if init sd
then if zeq id (proc_id sd) then PT pd = AbstractDataType.PT ladt else PT pd = 0
else if zeq id main_thread then PT pd = -1 else PT pd = 0;
ptp_re: if init sd
then ZMap.get id (ptpool pd) = ZMap.get id (AbstractDataType.ptpool ladt)
else if zeq id main_thread then ptpool pd = (AbstractDataType.ptpool ladt)
else ptpool pd = CalRealPT.real_pt (AbstractDataType.ptpool ladt);
ipt_re: if zeq id (proc_id sd) then ipt pd = AbstractDataType.ipt ladt else ipt pd = true;
intr_flag_re: if zeq id (proc_id sd) then intr_flag pd = AbstractDataType.intr_flag ladt else intr_flag pd = true;
in_intr_re: if zeq id (proc_id sd) then in_intr pd = AbstractDataType.in_intr ladt else in_intr pd = false;
com1_re: if zeq id dev_handling_cid then com1 pd = AbstractDataType.com1 ladt else True;
console_re: if zeq id dev_handling_cid then console pd = AbstractDataType.console ladt else True;
console_concrete_re: if zeq id dev_handling_cid
then console_concrete pd = AbstractDataType.console_concrete ladt else True;
ioapic_re: if zeq id dev_handling_cid
then ioapic pd = AbstractDataType.ioapic ladt else True;
lapic_re: if zeq id dev_handling_cid
then lapic pd = AbstractDataType.lapic ladt else True;
curr_intr_num_re: if zeq id dev_handling_cid
then curr_intr_num pd = AbstractDataType.curr_intr_num ladt else True;
drv_serial_re: if zeq id dev_handling_cid
then drv_serial pd = AbstractDataType.drv_serial ladt else True;
syncchpool_re: relate_SyncChanPool_per_pd id sd pd ladt;
uctxt_re: relate_uctxt_per_pd id sd pd ladt;
ept_re: if zeq id vm_handling_cid
then ept pd = ZMap.get (AbstractDataType.CPU_ID ladt) (AbstractDataType.ept ladt)
else True;
vmcs_re: if zeq id vm_handling_cid
then vmcs pd = ZMap.get (AbstractDataType.CPU_ID ladt) (AbstractDataType.vmcs ladt)
else True;
vmx_re: if zeq id vm_handling_cid
then vmx pd = ZMap.get (AbstractDataType.CPU_ID ladt) (AbstractDataType.vmx ladt)
else True;
inv_re: E2PBThreadGenPerDInv id kctxt_val sd pd ladt
}.
Record E2PBThreadGenEmptyPerDInv (id : Z) (kctxt_val : KContext) (sd : sharedData) (ladt : AbstractDataType.RData) :=
mkE2PBThreadGenEmptyPerDInv {
}.
Record E2PBThreadGenSharedDInv (kctxt_pool : KContextPool) (sd : sharedData) (ladt : AbstractDataType.RData) :=
mkE2PBThreadGenSharedDInv {
dirty_page_shared_inv:
∀ res i, ZMap.get i (AbstractDataType.pperm ladt) = PGUndef →
ZMap.get res (AbstractDataType.HP ladt) = ZMap.get res (FlatMem.free_page i (AbstractDataType.HP ladt));
init_big_log_inv: init sd = false → big_log sd = BigUndef;
init_pperm_inv: init sd = false → AbstractDataType.pperm ladt = ZMap.init PGUndef;
init_uctxt_inv: init sd = false → AbstractDataType.uctxt ladt = ZMap.init (ZMap.init Vundef);
syncchpool_inv:
BigLogThreadConfigFunction.B_inLock (CPU_ID sd) (big_log sd) = false →
BigLogThreadConfigFunction.B_GetlastPush (CPU_ID sd) (big_log sd)
= AbstractDataType.syncchpool ladt;
container_used_inv :
∀ tid, In tid full_thread_list → B_GetContainerUsed´ tid (CPU_ID sd) (big_log sd)
= cused (ZMap.get tid (AbstractDataType.AC ladt));
uctxt_used_inv :
∀ tid, B_GetContainerUsed´ tid (CPU_ID sd) (big_log sd) = false →
ZMap.get tid (AbstractDataType.uctxt ladt) = ZMap.init Vundef;
valid_AT_log_inv: valid_AT_log_type_B (big_log sd);
valid_TCB_log_inv: valid_TCB_log_type_B (big_log sd);
big_oracle_inv: valid_big_oracle (big_oracle sd);
valid_B_Cal_AT_log_inv: ∀ i l atable,
ZMap.get i (AbstractDataType.pperm ladt) ≠ PGUndef →
(AbstractDataType.big_log ladt) = BigDef l →
B_CalAT_log_real l = Some atable →
ZMap.get i atable = ATValid true ATNorm
}.
Record E2PBThreadGenSharedMemInv (pdpool: ZMap.t (option privData)) :=
mkE2PBThreadGenSharedMemInv {
pperm_disjoint:
∀ i j pd pd´,
i ≠ j →
ZMap.get i pdpool = Some pd →
ZMap.get j pdpool = Some pd´ →
(∀ j, ZMap.get j (pperm pd) ≠ PGUndef →
ZMap.get j (pperm pd´)= PGUndef)
}.
Record relate_RData (kctxt_pool : KContextPool) (sd : sharedData) (pdpool: ZMap.t (option privData))
(ladt : AbstractDataType.RData) :=
mkrelate_RData {
sh_vmxinfo_re: vmxinfo sd = AbstractDataType.vmxinfo ladt;
sh_CR3_re: CR3 sd= AbstractDataType.CR3 ladt;
sh_pg_re: pg sd = AbstractDataType.pg ladt;
sh_nps_re: nps sd = AbstractDataType.nps ladt;
sh_init_re: init sd = AbstractDataType.init ladt;
sh_lock_re: lock sd = AbstractDataType.lock ladt;
sh_CPU_ID_re: CPU_ID sd = AbstractDataType.CPU_ID ladt;
sh_cid_re: if init sd
then (ZMap.get (CPU_ID sd) (cid sd)) = (ZMap.get (AbstractDataType.CPU_ID ladt) (AbstractDataType.cid ladt))
else (ZMap.get (AbstractDataType.CPU_ID ladt) (AbstractDataType.cid ladt)) = 0 ∧
(if zle_lt 0 (CPU_ID sd) TOTAL_CPU
then (ZMap.get (CPU_ID sd) (cid sd)) = ((CPU_ID sd) + 1)
else (ZMap.get (CPU_ID sd) (cid sd)) = 0);
sh_idpde_re: idpde sd = AbstractDataType.idpde ladt;
sh_kctxt_re: kctxt_pool = (AbstractDataType.kctxt ladt);
sh_big_log_re: big_log sd = AbstractDataType.big_log ladt;
sh_big_oracle_re: big_oracle sd = AbstractDataType.big_oracle ladt;
per_data_re: ∀ i,
match ZMap.get i pdpool with
| Some pd ⇒ relate_RData_per_pd i (ZMap.get i kctxt_pool) sd pd ladt
| _ ⇒ E2PBThreadGenEmptyPerDInv i (ZMap.get i kctxt_pool) sd ladt
end;
sh_shared_inv_re: E2PBThreadGenSharedDInv kctxt_pool sd ladt;
sh_mem_inv_re: E2PBThreadGenSharedMemInv pdpool
}.
End MATCH.
Lemma zmap_set_eq :
∀ {A} (j i : Z) (m : ZMap.t A),
ZMap.get i (ZMap.set j (ZMap.get j m) m) = ZMap.get i m.
Proof.
intros ? j i m.
destruct (zeq j i); subst; [rewrite ZMap.gss | rewrite ZMap.gso]; auto.
Qed.
Lemma ef_cases:
∀ ef,
match ef with
| EF_external _ _ ⇒ True
| _ ⇒ False
end ∨
match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end.
Proof.
destruct ef; auto.
Qed.
Opaque proc_id.
Lemma relate_RData_gss:
∀ i kctxt_pool pdpool pd sd rd,
ZMap.get i pdpool = pd→
relate_RData kctxt_pool sd pdpool rd →
relate_RData kctxt_pool sd (ZMap.set i pd pdpool) rd.
Proof.
intros until rd; intros ? Hrel; subst.
inv Hrel.
constructor; auto.
intros.
generalize (per_data_re0 i0); intros.
case_eq (zeq i0 i); intros; subst.
- rewrite ZMap.gss; auto.
- rewrite ZMap.gso; auto.
- constructor.
intros; simpl.
case_eq (zeq i0 i); intros; subst.
+ rewrite ZMap.gss in ×.
rewrite ZMap.gso in H1; auto.
inv sh_mem_inv_re0; eauto.
+ rewrite ZMap.gso in H0; auto.
case_eq (zeq j i); intros; subst.
× rewrite ZMap.gss in H1.
inv sh_mem_inv_re0; eauto.
× rewrite ZMap.gso in H1; auto.
inv sh_mem_inv_re0; eauto.
Qed.
End SINGLECOMPOSEDATA.
Ltac inv_rel :=
match goal with
| [ H: relate_RData _ _ |- _ ] ⇒ inv H
end.
Ltac rewritesf :=
repeat match goal with
| H: ?a = _ |- appcontext [?a] ⇒ rewrite H
end.
Ltac rewritesb :=
repeat match goal with
| H: _ = ?a |- appcontext [?a] ⇒ rewrite <- H
end.
Ltac inv_layer Hl :=
match type of Hl with
| get_layer_primitive ?name _ = OK (Some ?σ)
⇒ let Hl´ := fresh in
repeat (apply SoundnessAux.get_layer_primitive_oplus_either in Hl; destruct Hl as [Hl|Hl]);
try (match goal with
| [ H : get_layer_primitive _ (?id ↦ _) = _ |- _ ] ⇒ destruct (Pos.eq_dec name id); subst
end;
[rewrite get_layer_primitive_mapsto in Hl; inv Hl |
rewrite get_layer_primitive_mapsto_other_primitive in Hl; auto; inv Hl]); simpl in *;
try solve [assert (Hl´:= SoundnessAux.get_layer_primitive_oplus_either name ∅ ∅ σ Hl);
destruct Hl´ as [Hl´|Hl´]; rewrite get_layer_primitive_empty in Hl´; inv Hl´]
end.
Ltac no_event_remove Hname:=
try (match goal with
| [Hname : context[has_event ?id] |- _] ⇒
assert (event_check: has_event id = false) by (unfold has_event; auto);
rewrite event_check in Hname; intuition
end).
Ltac has_event_remove Hname:=
try (match goal with
| [Hname : context[has_event ?id] |- _] ⇒
assert (event_check: has_event id = true) by (unfold has_event; auto);
rewrite event_check in Hname; intuition
end; fail).