Library mcertikos.layerlib.PrimTMSemantics
This file defines the general semantics for primitives at all layers
Require Import Coqlib.
Require Import Maps.
Require Import Globalenvs.
Require Import AsmX.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import AST.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import Conventions.
Require Import LAsm.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import compcert.cfrontend.Ctypes.
Require Import compcert.cfrontend.Cop.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Export mCertiKOSType.
Section Semantics.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context {RData} `{HD: CompatData RData}.
Section TMStartUser.
Variable start_user: RData → option (RData × UContext).
Local Open Scope Z_scope.
Inductive primcall_startuser_tm_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_startuser_sem_intro:
∀ m rs rs´ adt adt´ b,
start_user adt = Some (adt´, rs´)
→ ∀ N_TYPE: (∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v AST.Tint),
∀ N_INJECT_NEUTRAL: (∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
val_inject (Mem.flat_inj (Mem.nextblock m)) v v),
∀ Hsymbol: find_symbol s proc_start_user = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HUEIP_val_cond1: ZMap.get U_EIP rs´ ≠ Vint (Int.repr 0),
∀ HUEIP_val_cond2: ZMap.get U_EIP rs´ ≠ Vundef,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs))
# EDI <- (ZMap.get U_EDI rs´)# ESI <- (ZMap.get U_ESI rs´)
# EBP <- (ZMap.get U_EBP rs´)# ESP <- (ZMap.get U_ESP rs´)
# EBX <- (ZMap.get U_EBX rs´)# EDX <- (ZMap.get U_EDX rs´)
# ECX <- (ZMap.get U_ECX rs´)# EAX <- (ZMap.get U_EAX rs´)
# PC <- (ZMap.get U_EIP rs´) in
primcall_startuser_tm_sem s rs (m, adt) rs0 (m, adt´).
Class TMStartUserInvariants :=
{
tm_start_user_low_level_invariant n rs d d´:
start_user d = Some (d´, rs) →
low_level_invariant n d →
low_level_invariant n d´;
tm_start_user_high_level_invariant rs d d´:
start_user d = Some (d´, rs) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: TMStartUserInvariants}.
Local Instance primcall_startuser_tm_sem_propertes:
PrimcallProperties primcall_startuser_tm_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
rewrite H7 in H1.
inv H1.
split; congruence.
Qed.
Local Instance primcall_startuser_tm_sem_invariants:
PrimcallInvariants primcall_startuser_tm_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto; intros.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; omega).
+
apply set_reg_wt; eauto.
eapply N_TYPE; omega.
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl;
eapply N_TYPE; omega.
-
eapply tm_start_user_low_level_invariant; eauto.
-
eapply tm_start_user_high_level_invariant; eauto.
Qed.
Definition primcall_start_user_tm_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_startuser_tm_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some proc_start_user;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End TMStartUser.
Section TMExitUser.
Variable exit_user: RData → UContext → option RData.
Local Open Scope Z_scope.
Definition exit_sig :=
mksignature (AST.Tint::AST.Tint::AST.Tint::AST.Tint::AST.Tint::AST.Tint::
AST.Tint::AST.Tint::AST.Tint::AST.Tint::AST.Tint::
AST.Tint::AST.Tint::AST.Tint::AST.Tint::AST.Tint::
AST.Tint::nil) None cc_default.
Inductive primcall_exituser_tm_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_exituser_sem_intro:
∀ m adt adt´ (rs: regset) uctx0 vargs sg v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 b,
let uctx1:= ZMap.set U_EBX (Vint v4)
(ZMap.set U_OESP (Vint v3)
(ZMap.set U_EBP (Vint v2)
(ZMap.set U_ESI (Vint v1)
(ZMap.set U_EDI (Vint v0) (ZMap.init Vundef))))) in
let uctx2:= ZMap.set U_ES (Vint v8)
(ZMap.set U_EAX (Vint v7)
(ZMap.set U_ECX (Vint v6)
(ZMap.set U_EDX (Vint v5) uctx1))) in
let uctx3:= ZMap.set U_EIP (Vint v12)
(ZMap.set U_ERR (Vint v11)
(ZMap.set U_TRAPNO (Vint v10)
(ZMap.set U_DS (Vint v9) uctx2))) in
let uctx4:= ZMap.set U_SS (Vint v16)
(ZMap.set U_ESP (Vint v15)
(ZMap.set U_EFLAGS (Vint v14)
(ZMap.set U_CS (Vint v13) uctx3))) in
exit_user adt uctx0 = Some adt´
→ uctx0 = uctx4
→ rs ESP ≠ Vundef
→ ∀ HESP_STACK:
∀ b1 o,
rs ESP = Vptr b1 o →
Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m),
vargs = (Vint v0:: Vint v1 :: Vint v2 :: Vint v3:: Vint v4 :: Vint v5 :: Vint v6
:: Vint v7 :: Vint v8 :: Vint v9:: Vint v10 :: Vint v11 :: Vint v12
:: Vint v13 :: Vint v14 :: Vint v15:: Vint v16 ::nil)
→ v12 ≠ Int.repr 0
→ sg = exit_sig
→ extcall_arguments rs m sg vargs
→ ∀ Hsymbol: find_symbol s proc_exit_user = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
primcall_exituser_tm_sem s rs (m, adt)
((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EBX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) #PC <- (rs#RA))
(m, adt´).
Class TMExitUserInvariants :=
{
tm_exit_user_low_level_invariant n d d´ v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16:
let uctx1:= ZMap.set U_EBX (Vint v4)
(ZMap.set U_OESP (Vint v3)
(ZMap.set U_EBP (Vint v2)
(ZMap.set U_ESI (Vint v1)
(ZMap.set U_EDI (Vint v0) (ZMap.init Vundef))))) in
let uctx2:= ZMap.set U_ES (Vint v8)
(ZMap.set U_EAX (Vint v7)
(ZMap.set U_ECX (Vint v6)
(ZMap.set U_EDX (Vint v5) uctx1))) in
let uctx3:= ZMap.set U_EIP (Vint v12)
(ZMap.set U_ERR (Vint v11)
(ZMap.set U_TRAPNO (Vint v10)
(ZMap.set U_DS (Vint v9) uctx2))) in
let uctx4:= ZMap.set U_SS (Vint v16)
(ZMap.set U_ESP (Vint v15)
(ZMap.set U_EFLAGS (Vint v14)
(ZMap.set U_CS (Vint v13) uctx3))) in
exit_user d uctx4 = Some d´ →
low_level_invariant n d →
low_level_invariant n d´;
tm_exit_user_high_level_invariant rs d d´:
exit_user d rs = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: TMExitUserInvariants}.
Local Instance primcall_exituser_tm_sem_propertes:
PrimcallProperties primcall_exituser_tm_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst uctx1 uctx2 uctx3 uctx4 uctx5 uctx6 uctx7 uctx8.
specialize (extcall_arguments_determ _ _ _ _ _ H7 H15).
intros HF; inv HF.
split; congruence.
Qed.
Local Instance primcall_exituser_tm_sem_invariants:
PrimcallInvariants primcall_exituser_tm_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; omega).
+
apply set_reg_wt.
simpl. apply inv_reg_wt.
repeat apply undef_regs_wt; auto.
-
eapply tm_exit_user_low_level_invariant; eauto.
-
eapply tm_exit_user_high_level_invariant; eauto.
Qed.
Definition primcall_exit_user_tm_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_exituser_tm_sem;
sprimcall_sig := exit_sig;
sprimcall_valid s := true
|};
sprimcall_name := Some proc_exit_user;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End TMExitUser.
Section TMStartUser2.
Variable start_user: RData → option (RData × UContext).
Local Open Scope Z_scope.
Inductive primcall_startuser_tm_sem2 (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_startuser_sem_intro2:
∀ m rs rs´ adt adt´ b,
start_user adt = Some (adt´, rs´)
→ ∀ N_TYPE: (∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v AST.Tint),
∀ N_INJECT_NEUTRAL: (∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
val_inject (Mem.flat_inj (Mem.nextblock m)) v v),
∀ Hsymbol: find_symbol s proc_start_user2 = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HUEIP_val_cond1: ZMap.get U_EIP rs´ ≠ Vint (Int.repr 0),
∀ HUEIP_val_cond2: ZMap.get U_EIP rs´ ≠ Vundef,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs))
# EDI <- (ZMap.get U_EDI rs´)# ESI <- (ZMap.get U_ESI rs´)
# EBP <- (ZMap.get U_EBP rs´)# ESP <- (ZMap.get U_ESP rs´)
# EBX <- (ZMap.get U_EBX rs´)# EDX <- (ZMap.get U_EDX rs´)
# ECX <- (ZMap.get U_ECX rs´)# EAX <- (ZMap.get U_EAX rs´)
# PC <- (ZMap.get U_EIP rs´) in
primcall_startuser_tm_sem2 s rs (m, adt) rs0 (m, adt´).
Class TMStartUserInvariants2 :=
{
tm_start_user_low_level_invariant2 n rs d d´:
start_user d = Some (d´, rs) →
low_level_invariant n d →
low_level_invariant n d´;
tm_start_user_high_level_invariant2 rs d d´:
start_user d = Some (d´, rs) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: TMStartUserInvariants2}.
Local Instance primcall_startuser_tm_sem_propertes2:
PrimcallProperties primcall_startuser_tm_sem2.
Proof.
constructor; intros; inv H.
-
inv H0.
rewrite H7 in H1.
inv H1.
split; congruence.
Qed.
Local Instance primcall_startuser_tm_sem_invariants2:
PrimcallInvariants primcall_startuser_tm_sem2.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto; intros.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; omega).
+
apply set_reg_wt; eauto.
eapply N_TYPE; omega.
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl;
eapply N_TYPE; omega.
-
eapply tm_start_user_low_level_invariant2; eauto.
-
eapply tm_start_user_high_level_invariant2; eauto.
Qed.
Definition primcall_start_user_tm_compatsem2 : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_startuser_tm_sem2;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some proc_start_user2;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End TMStartUser2.
Section TMExitUser2.
Variable exit_user: RData → UContext → option RData.
Local Open Scope Z_scope.
Inductive primcall_exituser_tm_sem2 (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_exituser_sem_intro2:
∀ m adt adt´ (rs: regset) uctx0 vargs sg v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 b,
let uctx1:= ZMap.set U_EBX (Vint v4)
(ZMap.set U_OESP (Vint v3)
(ZMap.set U_EBP (Vint v2)
(ZMap.set U_ESI (Vint v1)
(ZMap.set U_EDI (Vint v0) (ZMap.init Vundef))))) in
let uctx2:= ZMap.set U_ES (Vint v8)
(ZMap.set U_EAX (Vint v7)
(ZMap.set U_ECX (Vint v6)
(ZMap.set U_EDX (Vint v5) uctx1))) in
let uctx3:= ZMap.set U_EIP (Vint v12)
(ZMap.set U_ERR (Vint v11)
(ZMap.set U_TRAPNO (Vint v10)
(ZMap.set U_DS (Vint v9) uctx2))) in
let uctx4:= ZMap.set U_SS (Vint v16)
(ZMap.set U_ESP (Vint v15)
(ZMap.set U_EFLAGS (Vint v14)
(ZMap.set U_CS (Vint v13) uctx3))) in
exit_user adt uctx0 = Some adt´
→ uctx0 = uctx4
→ rs ESP ≠ Vundef
→ ∀ HESP_STACK:
∀ b1 o,
rs ESP = Vptr b1 o →
Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m),
vargs = (Vint v0:: Vint v1 :: Vint v2 :: Vint v3:: Vint v4 :: Vint v5 :: Vint v6
:: Vint v7 :: Vint v8 :: Vint v9:: Vint v10 :: Vint v11 :: Vint v12
:: Vint v13 :: Vint v14 :: Vint v15:: Vint v16 ::nil)
→ v12 ≠ Int.repr 0
→ sg = exit_sig
→ extcall_arguments rs m sg vargs
→ ∀ Hsymbol: find_symbol s proc_exit_user2 = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
primcall_exituser_tm_sem2 s rs (m, adt)
((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EBX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) #PC <- (rs#RA))
(m, adt´).
Class TMExitUserInvariants2 :=
{
tm_exit_user_low_level_invariant2 n d d´ v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16:
let uctx1:= ZMap.set U_EBX (Vint v4)
(ZMap.set U_OESP (Vint v3)
(ZMap.set U_EBP (Vint v2)
(ZMap.set U_ESI (Vint v1)
(ZMap.set U_EDI (Vint v0) (ZMap.init Vundef))))) in
let uctx2:= ZMap.set U_ES (Vint v8)
(ZMap.set U_EAX (Vint v7)
(ZMap.set U_ECX (Vint v6)
(ZMap.set U_EDX (Vint v5) uctx1))) in
let uctx3:= ZMap.set U_EIP (Vint v12)
(ZMap.set U_ERR (Vint v11)
(ZMap.set U_TRAPNO (Vint v10)
(ZMap.set U_DS (Vint v9) uctx2))) in
let uctx4:= ZMap.set U_SS (Vint v16)
(ZMap.set U_ESP (Vint v15)
(ZMap.set U_EFLAGS (Vint v14)
(ZMap.set U_CS (Vint v13) uctx3))) in
exit_user d uctx4 = Some d´ →
low_level_invariant n d →
low_level_invariant n d´;
tm_exit_user_high_level_invariant2 rs d d´:
exit_user d rs = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: TMExitUserInvariants2}.
Local Instance primcall_exituser_tm_sem_propertes2:
PrimcallProperties primcall_exituser_tm_sem2.
Proof.
constructor; intros; inv H.
-
inv H0. subst uctx1 uctx2 uctx3 uctx4 uctx5 uctx6 uctx7 uctx8.
specialize (extcall_arguments_determ _ _ _ _ _ H7 H15).
intros HF; inv HF.
split; congruence.
Qed.
Local Instance primcall_exituser_tm_sem_invariants2:
PrimcallInvariants primcall_exituser_tm_sem2.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; omega).
+
apply set_reg_wt.
simpl. apply inv_reg_wt.
repeat apply undef_regs_wt; auto.
-
eapply tm_exit_user_low_level_invariant2; eauto.
-
eapply tm_exit_user_high_level_invariant2; eauto.
Qed.
Definition primcall_exit_user_tm_compatsem2 : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_exituser_tm_sem2;
sprimcall_sig := exit_sig;
sprimcall_valid s := true
|};
sprimcall_name := Some proc_exit_user2;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End TMExitUser2.
End Semantics.
Require Import Maps.
Require Import Globalenvs.
Require Import AsmX.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import AST.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import Conventions.
Require Import LAsm.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import compcert.cfrontend.Ctypes.
Require Import compcert.cfrontend.Cop.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Export mCertiKOSType.
Section Semantics.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context {RData} `{HD: CompatData RData}.
Section TMStartUser.
Variable start_user: RData → option (RData × UContext).
Local Open Scope Z_scope.
Inductive primcall_startuser_tm_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_startuser_sem_intro:
∀ m rs rs´ adt adt´ b,
start_user adt = Some (adt´, rs´)
→ ∀ N_TYPE: (∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v AST.Tint),
∀ N_INJECT_NEUTRAL: (∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
val_inject (Mem.flat_inj (Mem.nextblock m)) v v),
∀ Hsymbol: find_symbol s proc_start_user = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HUEIP_val_cond1: ZMap.get U_EIP rs´ ≠ Vint (Int.repr 0),
∀ HUEIP_val_cond2: ZMap.get U_EIP rs´ ≠ Vundef,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs))
# EDI <- (ZMap.get U_EDI rs´)# ESI <- (ZMap.get U_ESI rs´)
# EBP <- (ZMap.get U_EBP rs´)# ESP <- (ZMap.get U_ESP rs´)
# EBX <- (ZMap.get U_EBX rs´)# EDX <- (ZMap.get U_EDX rs´)
# ECX <- (ZMap.get U_ECX rs´)# EAX <- (ZMap.get U_EAX rs´)
# PC <- (ZMap.get U_EIP rs´) in
primcall_startuser_tm_sem s rs (m, adt) rs0 (m, adt´).
Class TMStartUserInvariants :=
{
tm_start_user_low_level_invariant n rs d d´:
start_user d = Some (d´, rs) →
low_level_invariant n d →
low_level_invariant n d´;
tm_start_user_high_level_invariant rs d d´:
start_user d = Some (d´, rs) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: TMStartUserInvariants}.
Local Instance primcall_startuser_tm_sem_propertes:
PrimcallProperties primcall_startuser_tm_sem.
Proof.
constructor; intros; inv H.
-
inv H0.
rewrite H7 in H1.
inv H1.
split; congruence.
Qed.
Local Instance primcall_startuser_tm_sem_invariants:
PrimcallInvariants primcall_startuser_tm_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto; intros.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; omega).
+
apply set_reg_wt; eauto.
eapply N_TYPE; omega.
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl;
eapply N_TYPE; omega.
-
eapply tm_start_user_low_level_invariant; eauto.
-
eapply tm_start_user_high_level_invariant; eauto.
Qed.
Definition primcall_start_user_tm_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_startuser_tm_sem;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some proc_start_user;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End TMStartUser.
Section TMExitUser.
Variable exit_user: RData → UContext → option RData.
Local Open Scope Z_scope.
Definition exit_sig :=
mksignature (AST.Tint::AST.Tint::AST.Tint::AST.Tint::AST.Tint::AST.Tint::
AST.Tint::AST.Tint::AST.Tint::AST.Tint::AST.Tint::
AST.Tint::AST.Tint::AST.Tint::AST.Tint::AST.Tint::
AST.Tint::nil) None cc_default.
Inductive primcall_exituser_tm_sem (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_exituser_sem_intro:
∀ m adt adt´ (rs: regset) uctx0 vargs sg v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 b,
let uctx1:= ZMap.set U_EBX (Vint v4)
(ZMap.set U_OESP (Vint v3)
(ZMap.set U_EBP (Vint v2)
(ZMap.set U_ESI (Vint v1)
(ZMap.set U_EDI (Vint v0) (ZMap.init Vundef))))) in
let uctx2:= ZMap.set U_ES (Vint v8)
(ZMap.set U_EAX (Vint v7)
(ZMap.set U_ECX (Vint v6)
(ZMap.set U_EDX (Vint v5) uctx1))) in
let uctx3:= ZMap.set U_EIP (Vint v12)
(ZMap.set U_ERR (Vint v11)
(ZMap.set U_TRAPNO (Vint v10)
(ZMap.set U_DS (Vint v9) uctx2))) in
let uctx4:= ZMap.set U_SS (Vint v16)
(ZMap.set U_ESP (Vint v15)
(ZMap.set U_EFLAGS (Vint v14)
(ZMap.set U_CS (Vint v13) uctx3))) in
exit_user adt uctx0 = Some adt´
→ uctx0 = uctx4
→ rs ESP ≠ Vundef
→ ∀ HESP_STACK:
∀ b1 o,
rs ESP = Vptr b1 o →
Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m),
vargs = (Vint v0:: Vint v1 :: Vint v2 :: Vint v3:: Vint v4 :: Vint v5 :: Vint v6
:: Vint v7 :: Vint v8 :: Vint v9:: Vint v10 :: Vint v11 :: Vint v12
:: Vint v13 :: Vint v14 :: Vint v15:: Vint v16 ::nil)
→ v12 ≠ Int.repr 0
→ sg = exit_sig
→ extcall_arguments rs m sg vargs
→ ∀ Hsymbol: find_symbol s proc_exit_user = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
primcall_exituser_tm_sem s rs (m, adt)
((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EBX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) #PC <- (rs#RA))
(m, adt´).
Class TMExitUserInvariants :=
{
tm_exit_user_low_level_invariant n d d´ v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16:
let uctx1:= ZMap.set U_EBX (Vint v4)
(ZMap.set U_OESP (Vint v3)
(ZMap.set U_EBP (Vint v2)
(ZMap.set U_ESI (Vint v1)
(ZMap.set U_EDI (Vint v0) (ZMap.init Vundef))))) in
let uctx2:= ZMap.set U_ES (Vint v8)
(ZMap.set U_EAX (Vint v7)
(ZMap.set U_ECX (Vint v6)
(ZMap.set U_EDX (Vint v5) uctx1))) in
let uctx3:= ZMap.set U_EIP (Vint v12)
(ZMap.set U_ERR (Vint v11)
(ZMap.set U_TRAPNO (Vint v10)
(ZMap.set U_DS (Vint v9) uctx2))) in
let uctx4:= ZMap.set U_SS (Vint v16)
(ZMap.set U_ESP (Vint v15)
(ZMap.set U_EFLAGS (Vint v14)
(ZMap.set U_CS (Vint v13) uctx3))) in
exit_user d uctx4 = Some d´ →
low_level_invariant n d →
low_level_invariant n d´;
tm_exit_user_high_level_invariant rs d d´:
exit_user d rs = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: TMExitUserInvariants}.
Local Instance primcall_exituser_tm_sem_propertes:
PrimcallProperties primcall_exituser_tm_sem.
Proof.
constructor; intros; inv H.
-
inv H0. subst uctx1 uctx2 uctx3 uctx4 uctx5 uctx6 uctx7 uctx8.
specialize (extcall_arguments_determ _ _ _ _ _ H7 H15).
intros HF; inv HF.
split; congruence.
Qed.
Local Instance primcall_exituser_tm_sem_invariants:
PrimcallInvariants primcall_exituser_tm_sem.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; omega).
+
apply set_reg_wt.
simpl. apply inv_reg_wt.
repeat apply undef_regs_wt; auto.
-
eapply tm_exit_user_low_level_invariant; eauto.
-
eapply tm_exit_user_high_level_invariant; eauto.
Qed.
Definition primcall_exit_user_tm_compatsem : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_exituser_tm_sem;
sprimcall_sig := exit_sig;
sprimcall_valid s := true
|};
sprimcall_name := Some proc_exit_user;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End TMExitUser.
Section TMStartUser2.
Variable start_user: RData → option (RData × UContext).
Local Open Scope Z_scope.
Inductive primcall_startuser_tm_sem2 (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_startuser_sem_intro2:
∀ m rs rs´ adt adt´ b,
start_user adt = Some (adt´, rs´)
→ ∀ N_TYPE: (∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
Val.has_type v AST.Tint),
∀ N_INJECT_NEUTRAL: (∀ i, 0 ≤ i < UCTXT_SIZE →
let v:= (ZMap.get i rs´) in
val_inject (Mem.flat_inj (Mem.nextblock m)) v v),
∀ Hsymbol: find_symbol s proc_start_user2 = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
∀ HUEIP_val_cond1: ZMap.get U_EIP rs´ ≠ Vint (Int.repr 0),
∀ HUEIP_val_cond2: ZMap.get U_EIP rs´ ≠ Vundef,
let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs))
# EDI <- (ZMap.get U_EDI rs´)# ESI <- (ZMap.get U_ESI rs´)
# EBP <- (ZMap.get U_EBP rs´)# ESP <- (ZMap.get U_ESP rs´)
# EBX <- (ZMap.get U_EBX rs´)# EDX <- (ZMap.get U_EDX rs´)
# ECX <- (ZMap.get U_ECX rs´)# EAX <- (ZMap.get U_EAX rs´)
# PC <- (ZMap.get U_EIP rs´) in
primcall_startuser_tm_sem2 s rs (m, adt) rs0 (m, adt´).
Class TMStartUserInvariants2 :=
{
tm_start_user_low_level_invariant2 n rs d d´:
start_user d = Some (d´, rs) →
low_level_invariant n d →
low_level_invariant n d´;
tm_start_user_high_level_invariant2 rs d d´:
start_user d = Some (d´, rs) →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: TMStartUserInvariants2}.
Local Instance primcall_startuser_tm_sem_propertes2:
PrimcallProperties primcall_startuser_tm_sem2.
Proof.
constructor; intros; inv H.
-
inv H0.
rewrite H7 in H1.
inv H1.
split; congruence.
Qed.
Local Instance primcall_startuser_tm_sem_invariants2:
PrimcallInvariants primcall_startuser_tm_sem2.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto; intros.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; omega).
+
apply set_reg_wt; eauto.
eapply N_TYPE; omega.
repeat apply set_reg_wt; try eapply N_INJECT_NEUTRAL;
try constructor; try assumption; simpl;
eapply N_TYPE; omega.
-
eapply tm_start_user_low_level_invariant2; eauto.
-
eapply tm_start_user_high_level_invariant2; eauto.
Qed.
Definition primcall_start_user_tm_compatsem2 : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_startuser_tm_sem2;
sprimcall_sig := null_signature;
sprimcall_valid s := true
|};
sprimcall_name := Some proc_start_user2;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End TMStartUser2.
Section TMExitUser2.
Variable exit_user: RData → UContext → option RData.
Local Open Scope Z_scope.
Inductive primcall_exituser_tm_sem2 (s: stencil):
regset → (mwd (cdata RData)) → regset → (mwd (cdata RData)) → Prop :=
| primcall_exituser_sem_intro2:
∀ m adt adt´ (rs: regset) uctx0 vargs sg v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 b,
let uctx1:= ZMap.set U_EBX (Vint v4)
(ZMap.set U_OESP (Vint v3)
(ZMap.set U_EBP (Vint v2)
(ZMap.set U_ESI (Vint v1)
(ZMap.set U_EDI (Vint v0) (ZMap.init Vundef))))) in
let uctx2:= ZMap.set U_ES (Vint v8)
(ZMap.set U_EAX (Vint v7)
(ZMap.set U_ECX (Vint v6)
(ZMap.set U_EDX (Vint v5) uctx1))) in
let uctx3:= ZMap.set U_EIP (Vint v12)
(ZMap.set U_ERR (Vint v11)
(ZMap.set U_TRAPNO (Vint v10)
(ZMap.set U_DS (Vint v9) uctx2))) in
let uctx4:= ZMap.set U_SS (Vint v16)
(ZMap.set U_ESP (Vint v15)
(ZMap.set U_EFLAGS (Vint v14)
(ZMap.set U_CS (Vint v13) uctx3))) in
exit_user adt uctx0 = Some adt´
→ uctx0 = uctx4
→ rs ESP ≠ Vundef
→ ∀ HESP_STACK:
∀ b1 o,
rs ESP = Vptr b1 o →
Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m),
vargs = (Vint v0:: Vint v1 :: Vint v2 :: Vint v3:: Vint v4 :: Vint v5 :: Vint v6
:: Vint v7 :: Vint v8 :: Vint v9:: Vint v10 :: Vint v11 :: Vint v12
:: Vint v13 :: Vint v14 :: Vint v15:: Vint v16 ::nil)
→ v12 ≠ Int.repr 0
→ sg = exit_sig
→ extcall_arguments rs m sg vargs
→ ∀ Hsymbol: find_symbol s proc_exit_user2 = Some b,
∀ HPC: rs PC = Vptr b Int.zero,
primcall_exituser_tm_sem2 s rs (m, adt)
((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EBX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) #PC <- (rs#RA))
(m, adt´).
Class TMExitUserInvariants2 :=
{
tm_exit_user_low_level_invariant2 n d d´ v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16:
let uctx1:= ZMap.set U_EBX (Vint v4)
(ZMap.set U_OESP (Vint v3)
(ZMap.set U_EBP (Vint v2)
(ZMap.set U_ESI (Vint v1)
(ZMap.set U_EDI (Vint v0) (ZMap.init Vundef))))) in
let uctx2:= ZMap.set U_ES (Vint v8)
(ZMap.set U_EAX (Vint v7)
(ZMap.set U_ECX (Vint v6)
(ZMap.set U_EDX (Vint v5) uctx1))) in
let uctx3:= ZMap.set U_EIP (Vint v12)
(ZMap.set U_ERR (Vint v11)
(ZMap.set U_TRAPNO (Vint v10)
(ZMap.set U_DS (Vint v9) uctx2))) in
let uctx4:= ZMap.set U_SS (Vint v16)
(ZMap.set U_ESP (Vint v15)
(ZMap.set U_EFLAGS (Vint v14)
(ZMap.set U_CS (Vint v13) uctx3))) in
exit_user d uctx4 = Some d´ →
low_level_invariant n d →
low_level_invariant n d´;
tm_exit_user_high_level_invariant2 rs d d´:
exit_user d rs = Some d´ →
high_level_invariant d →
high_level_invariant d´
}.
Section WithInv.
Context`{inv_ops: TMExitUserInvariants2}.
Local Instance primcall_exituser_tm_sem_propertes2:
PrimcallProperties primcall_exituser_tm_sem2.
Proof.
constructor; intros; inv H.
-
inv H0. subst uctx1 uctx2 uctx3 uctx4 uctx5 uctx6 uctx7 uctx8.
specialize (extcall_arguments_determ _ _ _ _ _ H7 H15).
intros HF; inv HF.
split; congruence.
Qed.
Local Instance primcall_exituser_tm_sem_invariants2:
PrimcallInvariants primcall_exituser_tm_sem2.
Proof.
constructor; intros; inv H; trivial.
-
inv H0.
constructor; eauto.
+
inv inv_inject_neutral.
constructor; eauto.
val_inject_simpl;
try (eapply N_INJECT_NEUTRAL; omega).
+
apply set_reg_wt.
simpl. apply inv_reg_wt.
repeat apply undef_regs_wt; auto.
-
eapply tm_exit_user_low_level_invariant2; eauto.
-
eapply tm_exit_user_high_level_invariant2; eauto.
Qed.
Definition primcall_exit_user_tm_compatsem2 : compatsem (cdata RData) :=
compatsem_inr
{|
sprimcall_primsem_step :=
{|
sprimcall_step := primcall_exituser_tm_sem2;
sprimcall_sig := exit_sig;
sprimcall_valid s := true
|};
sprimcall_name := Some proc_exit_user2;
sprimcall_props := OK _;
sprimcall_invs := OK _
|}.
End WithInv.
End TMExitUser2.
End Semantics.