Library mcertikos.conlib.conmtlib.HAsm
HAsm is a specialization for LAsm used for the layer
PHThread and above, and uses initial states that are suitable for
thread linking code: the initial value of the PC and the initial
memory's Mem.nextblock are derived from the init_log.
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 Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import Constant.
Require Import PrimSemantics.
Require Import LRegSet.
Require Import AuxStateDataType.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobalOracle.
Require Import AlgebraicMem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import SingleOracle.
Require Import AbstractDataType.
Require Export ObjMultiprocessor.
Require Import AuxFunctions.
Require Import liblayers.compat.CompatLayers.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import CompatExternalCalls.
Require Import MakeProgram.
Require Import LAsmModuleSem.
Require Import I64Layer.
Require Import Soundness.
Require Import LinkTactic.
Require Import LAsmModuleSemAux.
Require Export SingleConfiguration.
Require Import LAsm.
Require Import TAsm.
Require Import SingleConfiguration.
Require Import LAsm.
Section HASM.
Context `{Hsc: SingleConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{Hstencil: Stencil}.
Context `{Hdata: CompatData RData}.
Inductive initial_state {F V} p: state (mem := mwd (cdata RData)) → Prop :=
| initial_state_intro m0 m1 d pc:
Genv.init_mem (F:=F) (V:=V) p = Some (m0, d) →
init_mem_lift_nextblock m0 = m1 →
let ge := Genv.globalenv p in
initial_thread_pc ge current_thread init_log = Some pc →
let rs0 := (Pregmap.init Vundef) # PC <- pc # ESP <- Vzero in
initial_state p (State rs0 (m1, d)).
Global Program Instance hasm_init_state: AsmInitialState (mwd (cdata RData)) :=
{
asm_init_state F V := initial_state
}.
Next Obligation.
destruct H, H0.
subst ge ge0 rs0 rs1.
congruence.
Qed.
Definition semantics (L: compatlayer _) `{acc_def: !AccessorsDefined L} :=
LAsm.semantics (asm_init := hasm_init_state) (lcfg_ops := LC L).
End HASM.
Section HASM_SOUNDNESS.
Context `{Hsc: SingleConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{Hstencil: Stencil}.
Lemma init_mem_lift_nextblock_nextblock:
Proper
(eq @@ Mem.nextblock ++> Pos.le @@ Mem.nextblock)
init_mem_lift_nextblock.
Proof.
unfold RelCompFun.
intros m1 m2 Hm.
unfold init_mem_lift_nextblock.
destruct init_log; eauto.
- rewrite Hm; reflexivity.
- rewrite Hm.
apply Pos2Nat.inj_le.
erewrite mem_lift_nextblock_target_eq
with (m´ := mem_lift_nextblock m1 _)
by eauto.
erewrite mem_lift_nextblock_target_eq
with (m´ := mem_lift_nextblock m2 _)
by eauto.
apply plus_le_compat; eauto.
apply Pos2Nat.inj_le; eauto.
rewrite Hm; reflexivity.
Qed.
Lemma init_mem_lift_nextblock_perm m b ofs k p:
¬ Mem.perm m b ofs k p →
¬ Mem.perm (init_mem_lift_nextblock m) b ofs k p.
Proof.
unfold init_mem_lift_nextblock.
destruct init_log; eauto.
generalize (Pos.to_nat (last_nb (l :: l0)) -
Pos.to_nat (Mem.nextblock m))%nat.
intros n.
pose proof (mem_lift_nextblock_perm n m b ofs k p).
tauto.
Qed.
Lemma init_mem_lift_nextblock_le m:
(Mem.nextblock m ≤ Mem.nextblock (init_mem_lift_nextblock m))%positive.
Proof.
unfold init_mem_lift_nextblock.
destruct init_log; [reflexivity | ].
eapply mem_lift_nextblock_source_target_le; eauto.
Qed.
Lemma init_mem_lift_nextblock_inject_neutral m:
let m´ := init_mem_lift_nextblock m in
Mem.inject_neutral (Mem.nextblock m) m →
Mem.inject_neutral (Mem.nextblock m´) m´.
Proof.
unfold init_mem_lift_nextblock.
destruct init_log; eauto.
eapply mem_lift_nextblock_inject_neutral.
Qed.
Lemma init_mem_lift_nextblock_generic (P: mem → mem → Prop) m1 m2:
Mem.nextblock m1 = Mem.nextblock m2 →
P m1 m2 →
(∀ m1´ m2´ m1´´ m2´´ b1 b2,
(Mem.nextblock m1 ≤ Mem.nextblock m1´)%positive →
(Mem.nextblock m2 ≤ Mem.nextblock m2´)%positive →
Mem.alloc m1´ 0 0 = (m1´´, b1) →
Mem.alloc m2´ 0 0 = (m2´´, b2) →
P m1´ m2´ → P m1´´ m2´´) →
P (init_mem_lift_nextblock m1) (init_mem_lift_nextblock m2).
Proof.
intros Hnb HP Hstep.
unfold init_mem_lift_nextblock.
destruct init_log; eauto.
rewrite Hnb.
eapply mem_lift_nextblock_generic; eauto.
Qed.
Lemma initial_thread_pc_global {F V} (ge: Genv.t F V) tid l v:
initial_thread_pc ge tid l = Some v →
(∃ id ofs, symbol_offset ge id ofs = v).
Proof.
induction l.
- simpl.
destruct (decide _); try discriminate.
inversion 1; eauto.
- simpl.
destruct (initial_thread_pc _ _ _) eqn:Hv; eauto.
clear.
unfold thread_init_pc_of.
destruct (thread_init_pc _ _) as [[? ?] | ] eqn:Hv; try discriminate.
destruct (decide _); try discriminate.
inversion 1; subst.
unfold thread_init_pc in Hv.
destruct a; try discriminate.
destruct l; try discriminate.
subdestruct; inv Hv.
eapply prim_thread_init_pc_global; eauto.
Qed.
Lemma initial_thread_pc_symbols_preserved {F V} (ge1 ge2: Genv.t F V) tid l v:
(∀ i, Genv.find_symbol ge1 i = Genv.find_symbol ge2 i) →
initial_thread_pc ge1 tid l = Some v →
initial_thread_pc ge2 tid l = Some v.
Proof.
revert v ge1 ge2.
induction l; intros v ge1 ge2 Hge.
- simpl.
destruct (decide _); try discriminate.
intros H.
rewrite <- H.
f_equal.
apply AsmX.symbol_offset_symbols_preserved; eauto.
- simpl.
destruct (initial_thread_pc ge1 _ _) eqn:Hv1; inversion 1; subst.
+ erewrite IHl; eauto.
+ destruct (initial_thread_pc ge2 _ _) eqn:Hv2.
× assert (initial_thread_pc ge1 tid l = Some v0) by eauto.
congruence.
× rewrite H.
revert Hge H.
unfold thread_init_pc_of, thread_init_pc.
clear; intros.
destruct a;
try discriminate.
destruct l;
try discriminate.
case_eq (prim_thread_init_pc ge1 id args); intros.
{ erewrite prim_thread_init_pc_symbols_preserved; eauto.
subdestruct; inv H; inv H0; auto. }
{ rewrite H0 in H; discriminate. }
Qed.
Context `{data1_ops: !CompatDataOps RData} `{Hdata1: !CompatData RData}.
Context `{data2_ops: !CompatDataOps RData} `{Hdata2: !CompatData RData}.
Context `{crel_ops: !CompatRelOps (stencil:=stencil) (cdata (cdata_ops := data1_ops) RData) (cdata (cdata_ops := data2_ops) RData)}.
Context `{Hcrel: !CompatRel (stencil:=stencil) (cdata RData) (cdata RData)}.
Context `{Hbinr: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{mkp_ops: !MakeProgramOps LAsm.function Ctypes.type LAsm.fundef unit}.
Context `{mkp_prf: !MakeProgram LAsm.function Ctypes.type LAsm.fundef unit}.
Remove Hints asm_init_default : typeclass_instances.
Global Instance hasm_init_compat CTXT LH M LL:
AsmInitialStatesCompatible
(cdata (cdata_ops := data1_ops) _)
(cdata (cdata_ops := data2_ops) _)
(one_crel (CompatRelOps0 := crel_ops) RData RData)
CTXT LH M LL.
Proof.
constructor.
intros s ph pl s1 Hph Hpl HLOK Hgeh Hgel Hp_main Hp_defs H Hinit.
simpl.
destruct 1 as [m0h m1h dh pch Hm0h Hm1h geh Hpch rs0h].
We put together a "regular" LAsm initial state, so that we can
get most of what we need out of the default instance of
AsmInitialStatesCompatible.
pose
(rs0h´ :=
(Pregmap.init Vundef)
# PC <- (symbol_offset (Genv.globalenv ph) (prog_main ph) Int.zero)
# ESP <- Vzero).
edestruct
(asm_init_state_match
(AsmInitialStatesCompatible :=
asm_init_default_compat _ _ (one_crel RData RData) CTXT LH M LL))
as (s2´ & Hs2´ & Hs´); eauto.
{
instantiate (1 := (State rs0h´ (m0h, dh))).
econstructor; eauto.
}
(rs0h´ :=
(Pregmap.init Vundef)
# PC <- (symbol_offset (Genv.globalenv ph) (prog_main ph) Int.zero)
# ESP <- Vzero).
edestruct
(asm_init_state_match
(AsmInitialStatesCompatible :=
asm_init_default_compat _ _ (one_crel RData RData) CTXT LH M LL))
as (s2´ & Hs2´ & Hs´); eauto.
{
instantiate (1 := (State rs0h´ (m0h, dh))).
econstructor; eauto.
}
Now from the regular LAsm initial state for the low layer, we
do the inverse poeration and synthesize one of our special HAsm
initial states.
destruct Hs2´ as [[m0l dl] Hm0l rs0l´].
pose
(rs0l :=
(Pregmap.init Vundef)
# PC <- pch
# ESP <- Vzero).
pose (m1l := init_mem_lift_nextblock m0l).
∃ (State (mem := mwd (cdata (cdata_ops := data2_ops) _)) rs0l (m1l, dl)).
split.
{
econstructor; eauto.
eapply (initial_thread_pc_symbols_preserved
(Genv.globalenv ph)
(Genv.globalenv pl)); eauto.
intros i.
erewrite !stencil_matches_symbols by eauto.
reflexivity.
}
setoid_rewrite InitMem.init_mem_with_data in Hm0h.
destruct (Genv.init_mem ph) as [xm0h | ] eqn:Hm0h´; [ | discriminate].
inversion Hm0h; clear Hm0h; subst xm0h dh.
setoid_rewrite InitMem.init_mem_with_data in Hm0l.
destruct (Genv.init_mem pl) as [xm0l | ] eqn:Hm0l´; [ | discriminate].
inversion Hm0l; clear Hm0l; subst xm0l dl.
assert
(∀ f,
inject_incr (Mem.flat_inj (genv_next s)) f →
val_inject f pch pch)
as Hpch_inject.
{
intros f´ Hf.
eapply initial_thread_pc_global in Hpch.
destruct Hpch as (id & ofs & Hpch).
subst pch.
eapply stencil_symbol_offset_inject; eauto.
}
inversion Hs´; clear Hs´; subst.
subst m1l.
pattern (init_mem_lift_nextblock m0h), (init_mem_lift_nextblock m0l).
apply init_mem_lift_nextblock_generic; eauto.
pose
(rs0l :=
(Pregmap.init Vundef)
# PC <- pch
# ESP <- Vzero).
pose (m1l := init_mem_lift_nextblock m0l).
∃ (State (mem := mwd (cdata (cdata_ops := data2_ops) _)) rs0l (m1l, dl)).
split.
{
econstructor; eauto.
eapply (initial_thread_pc_symbols_preserved
(Genv.globalenv ph)
(Genv.globalenv pl)); eauto.
intros i.
erewrite !stencil_matches_symbols by eauto.
reflexivity.
}
setoid_rewrite InitMem.init_mem_with_data in Hm0h.
destruct (Genv.init_mem ph) as [xm0h | ] eqn:Hm0h´; [ | discriminate].
inversion Hm0h; clear Hm0h; subst xm0h dh.
setoid_rewrite InitMem.init_mem_with_data in Hm0l.
destruct (Genv.init_mem pl) as [xm0l | ] eqn:Hm0l´; [ | discriminate].
inversion Hm0l; clear Hm0l; subst xm0l dl.
assert
(∀ f,
inject_incr (Mem.flat_inj (genv_next s)) f →
val_inject f pch pch)
as Hpch_inject.
{
intros f´ Hf.
eapply initial_thread_pc_global in Hpch.
destruct Hpch as (id & ofs & Hpch).
subst pch.
eapply stencil_symbol_offset_inject; eauto.
}
inversion Hs´; clear Hs´; subst.
subst m1l.
pattern (init_mem_lift_nextblock m0h), (init_mem_lift_nextblock m0l).
apply init_mem_lift_nextblock_generic; eauto.
The nextblock for initial memories are identical
{
erewrite <- !Genv.init_mem_genv_next by eauto.
erewrite !stencil_matches_genv_next by eauto.
reflexivity.
}
erewrite <- !Genv.init_mem_genv_next by eauto.
erewrite !stencil_matches_genv_next by eauto.
reflexivity.
}
Show that the modified PC is still okay
{
econstructor; eauto.
- instantiate (1 := f).
destruct H7; constructor; eauto.
subst rs0h rs0l.
val_inject_simpl.
eapply Hpch_inject; eauto.
destruct match_extcall_states; eauto.
- destruct H11; constructor; eauto.
+ destruct inv_inject_neutral; constructor; eauto.
subst rs0l.
val_inject_simpl.
revert Hpch_inject inv_mem_valid; clear; intros.
lift_unfold.
eapply Hpch_inject; eauto.
eapply flat_inj_inject_incr; eauto.
+ subst rs0l.
apply AsmX.set_reg_wt.
{
constructor.
}
apply AsmX.set_reg_wt.
{
eapply initial_thread_pc_global in Hpch.
destruct Hpch as (id & ofs & Hpch).
subst pch.
unfold symbol_offset.
destruct (Genv.find_symbol _ _);
constructor.
}
intro; constructor.
}
econstructor; eauto.
- instantiate (1 := f).
destruct H7; constructor; eauto.
subst rs0h rs0l.
val_inject_simpl.
eapply Hpch_inject; eauto.
destruct match_extcall_states; eauto.
- destruct H11; constructor; eauto.
+ destruct inv_inject_neutral; constructor; eauto.
subst rs0l.
val_inject_simpl.
revert Hpch_inject inv_mem_valid; clear; intros.
lift_unfold.
eapply Hpch_inject; eauto.
eapply flat_inj_inject_incr; eauto.
+ subst rs0l.
apply AsmX.set_reg_wt.
{
constructor.
}
apply AsmX.set_reg_wt.
{
eapply initial_thread_pc_global in Hpch.
destruct Hpch as (id & ofs & Hpch).
subst pch.
unfold symbol_offset.
destruct (Genv.find_symbol _ _);
constructor.
}
intro; constructor.
}
Show that Mem.allocating and empty block preserves the relation
{
clear Hpch.
revert Hsc.
clear.
intros.
inv H3.
destruct H11.
destruct match_extcall_states.
edestruct (Mem.alloc_parallel_inject f m1´ m2´ 0 0 m1´´ b1 0 0)
as (f´ & xm2´´ & xb2 & Hx2 & Hm´´ & Hf´ & Hf´b1 & Hf´nb1);
eauto; try reflexivity.
assert (xm2´´ = m2´´) by congruence; subst xm2´´.
assert (xb2 = b2) by congruence; subst xb2.
assert (Mem.nextblock m2´ < Mem.nextblock m2´´)%positive as Hnb2.
{
erewrite (Mem.nextblock_alloc m2´ 0 0 m2´´); eauto.
xomega.
}
econstructor; eauto.
- instantiate (1 := f´).
constructor; eauto.
constructor; eauto.
+ eapply relate_incr; eauto.
+ eapply alloc_match_correct; eauto.
rewrite (Mem.alloc_result m1´ 0 0 m1´´ b1); eauto.
intros i b Hing Hb.
specialize (match_newglob_nextblock i b Hing Hb).
revert match_newglob_nextblock.
generalize (Mem.nextblock m1´); clear; intro.
destruct (decide (b = b0)); eauto; omega.
+ transitivity f; eauto.
+ intros b b´ delta Hb´.
destruct (decide (b = b1)).
× subst b.
rewrite Hf´b1 in Hb´.
inv Hb´.
rewrite (Mem.alloc_result m1´ 0 0 m1´´ b1); eauto.
rewrite (Mem.alloc_result m2´ 0 0 m2´´ b´); eauto.
× eapply match_inject_forward; eauto.
rewrite Hf´nb1 in Hb´; eauto.
+ erewrite (Mem.nextblock_alloc m1´ 0 0 m1´´); eauto.
erewrite (Mem.nextblock_alloc m2´ 0 0 m2´´); eauto.
rewrite <- Pos.succ_le_mono; eauto.
+ intros i b ofs k p Hi Hb Hp.
eapply match_newglob_noperm; eauto.
eapply (Mem.perm_alloc_inv m1´ 0 0 m1´´ b1) in Hp; eauto.
destruct (eq_block _ _); try omega.
eassumption.
+ intros.
transitivity (Mem.nextblock m1´); eauto.
erewrite (Mem.nextblock_alloc m1´ 0 0 m1´´); eauto.
xomega.
- eapply CompatData.low_level_invariant_incr; eauto.
xomega.
- destruct H15; constructor; eauto.
destruct inv_inject_neutral; constructor; eauto.
+ etransitivity; eauto.
lift_unfold.
xomega.
+ lift_unfold.
eapply Mem.alloc_inject_neutral; eauto.
eapply Mem.inject_neutral_incr; eauto.
xomega.
+ intros.
eapply val_inject_incr; [ | apply inv_reg_inject_neutral; eauto ].
eapply flat_inj_inject_incr; eauto.
lift_unfold.
xomega.
}
Qed.
clear Hpch.
revert Hsc.
clear.
intros.
inv H3.
destruct H11.
destruct match_extcall_states.
edestruct (Mem.alloc_parallel_inject f m1´ m2´ 0 0 m1´´ b1 0 0)
as (f´ & xm2´´ & xb2 & Hx2 & Hm´´ & Hf´ & Hf´b1 & Hf´nb1);
eauto; try reflexivity.
assert (xm2´´ = m2´´) by congruence; subst xm2´´.
assert (xb2 = b2) by congruence; subst xb2.
assert (Mem.nextblock m2´ < Mem.nextblock m2´´)%positive as Hnb2.
{
erewrite (Mem.nextblock_alloc m2´ 0 0 m2´´); eauto.
xomega.
}
econstructor; eauto.
- instantiate (1 := f´).
constructor; eauto.
constructor; eauto.
+ eapply relate_incr; eauto.
+ eapply alloc_match_correct; eauto.
rewrite (Mem.alloc_result m1´ 0 0 m1´´ b1); eauto.
intros i b Hing Hb.
specialize (match_newglob_nextblock i b Hing Hb).
revert match_newglob_nextblock.
generalize (Mem.nextblock m1´); clear; intro.
destruct (decide (b = b0)); eauto; omega.
+ transitivity f; eauto.
+ intros b b´ delta Hb´.
destruct (decide (b = b1)).
× subst b.
rewrite Hf´b1 in Hb´.
inv Hb´.
rewrite (Mem.alloc_result m1´ 0 0 m1´´ b1); eauto.
rewrite (Mem.alloc_result m2´ 0 0 m2´´ b´); eauto.
× eapply match_inject_forward; eauto.
rewrite Hf´nb1 in Hb´; eauto.
+ erewrite (Mem.nextblock_alloc m1´ 0 0 m1´´); eauto.
erewrite (Mem.nextblock_alloc m2´ 0 0 m2´´); eauto.
rewrite <- Pos.succ_le_mono; eauto.
+ intros i b ofs k p Hi Hb Hp.
eapply match_newglob_noperm; eauto.
eapply (Mem.perm_alloc_inv m1´ 0 0 m1´´ b1) in Hp; eauto.
destruct (eq_block _ _); try omega.
eassumption.
+ intros.
transitivity (Mem.nextblock m1´); eauto.
erewrite (Mem.nextblock_alloc m1´ 0 0 m1´´); eauto.
xomega.
- eapply CompatData.low_level_invariant_incr; eauto.
xomega.
- destruct H15; constructor; eauto.
destruct inv_inject_neutral; constructor; eauto.
+ etransitivity; eauto.
lift_unfold.
xomega.
+ lift_unfold.
eapply Mem.alloc_inject_neutral; eauto.
eapply Mem.inject_neutral_incr; eauto.
xomega.
+ intros.
eapply val_inject_incr; [ | apply inv_reg_inject_neutral; eauto ].
eapply flat_inj_inject_incr; eauto.
lift_unfold.
xomega.
}
Qed.
Theorem hasm_soundness:
let DH := cdata (cdata_ops := data1_ops) _ in
let DL := cdata (cdata_ops := data2_ops) _ in
let R := crel (CompatRelOps0 := crel_ops) RData RData in
∀ (LH: compatlayer DH)
(LL: compatlayer DL)
(LH_ACC_DEF: LAsm.AccessorsDefined LH)
(LL_ACC_DEF: LAsm.AccessorsDefined LL)
(LH_RECEPT: ExternalCallsXDefined (LH))
(LL_DETERM: ExternalCallsXDefined (LL))
(LL_DETERM´: PrimitiveCallsXDefined LL)
(LH_INV: ExtcallInvariantsDefined LH)
(LL_INV: ExtcallInvariantsDefined LL)
(LH_PRIM_INV: PrimcallInvariantsDefined LH)
(LL_PRIM_INV: PrimcallInvariantsDefined LL)
(LH_NAMES: LayerNamesMatch DH LH)
(LL_NAMSE: LayerNamesMatch DL LL)
(M: LAsm.module)
(builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet)
(REFINE: cl_sim _ _ R LH (〚 M 〛 LL ⊕ LL))
(INIT_SIM: cl_init_sim _ _ R LH M LL)
(CTXT: LAsm.module) s pl
(PL: make_program s (CTXT ⊕ M) LL = OK pl)
(prim_valid: get_layer_prim_valid LL s)
ph
(PH: make_program s CTXT LH = OK ph)
(HLayerOK´: LayerOK (〚 M 〛 LL ⊕ LL)),
backward_simulation
(semantics LH ph)
(semantics LL pl).
Proof.
intros.
eapply soundness_generic; eauto.
apply hasm_init_compat.
Qed.
End HASM_SOUNDNESS.