Library mcertikos.trap.TTrapArgCode1
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import TacticsForTesting.
Require Import XOmega.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import TTrapArg.
Require Import TrapGenSpec.
Require Import TTrapArgCSource.
Require Import ObjTrap.
Require Import CommonTactic.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Lemma int_wrap:
Int.repr (-1) = Int.repr (Int.max_unsigned).
Proof.
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
reflexivity.
Qed.
Lemma unsigned_int_range:
∀ x: int,
0 ≤ Int.unsigned x ≤ Int64.max_unsigned.
Proof.
split.
apply Int.unsigned_range.
apply Z.le_trans with (m:=Int.max_unsigned);
( apply Int.unsigned_range_2 ||
unfold Int.max_unsigned, Int64.max_unsigned;
simpl; omega).
Qed.
Lemma cat_unsigned64_lor_range:
∀ lo hi,
0 ≤ Z.lor (Z.shiftl (Int.unsigned hi) 32) (Int.unsigned lo) ≤ Int64.max_unsigned.
Proof.
intros lo hi.
apply Z64_lor_range.
apply Z_shiftl_32_range.
apply Int.unsigned_range_2.
apply unsigned_int_range.
Qed.
Lemma unsigned_div_2pow32_eq_0:
∀ x, Int.unsigned x / 2 ^ 32 = 0.
Proof.
intro.
generalize (Int.unsigned_range x); intro.
repeat autounfold in H.
unfold two_power_nat, shift_nat in H.
simpl in H.
change (2 ^ 32) with 4294967296.
xomega.
Qed.
Lemma unsigned_shiftl_lor_shiftr_range:
∀ x y n,
0 ≤ n →
0 ≤ Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) n) (Int.unsigned y)) n ≤ Int.max_unsigned.
Proof.
split.
- apply Z.shiftr_nonneg.
apply Z_lor_range_lo.
+ apply Z.shiftl_nonneg.
apply Int.unsigned_range.
+ apply Int.unsigned_range.
- rewrite Z.shiftr_lor.
rewrite Z.shiftr_shiftl_r.
+ rewrite Z.sub_diag with (n:=n).
rewrite Z.shiftr_0_r.
rewrite Z.shiftr_div_pow2.
apply Z_lor_range.
apply Int.unsigned_range_2.
split.
× change 0 with (0 / 2 ^ n).
apply Z_div_le.
apply Z.lt_gt.
apply Z.pow_pos_nonneg; omega.
apply Int.unsigned_range.
× rewrite <- Z_div_mult_full with (a:=Int.max_unsigned)(b:=2^n).
{
apply Z_div_le.
- apply Z.lt_gt.
apply Z.pow_pos_nonneg; omega.
- apply Z.le_trans with (m:=Int.max_unsigned).
+ apply Int.unsigned_range_2.
+ apply Z.le_mul_diag_r with (n:=Int.max_unsigned)(m:=2^n).
× repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
omega.
× apply Zle_lt_or_eq in H.
destruct H.
{
generalize (Z.pow_gt_1 2 n).
intro Hr.
destruct Hr.
- omega.
- apply H0 in H.
omega.
}
rewrite <- H.
simpl.
omega.
}
apply Z.pow_nonzero.
omega.
assumption.
× assumption.
+ assumption.
Qed.
Lemma unsigned_shiftl_lor_shiftr_32_range:
∀ x y,
0 ≤ Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) 32) (Int.unsigned y)) 32 ≤ Int.max_unsigned.
Proof.
intros.
apply unsigned_shiftl_lor_shiftr_range with (n:=32).
omega.
Qed.
Lemma Z_mod_range:
∀ x n,
n > 0 →
0 ≤ x mod n ≤ n - 1.
Proof.
intros.
assert(0 ≤ x mod n < n).
apply Z_mod_lt.
omega.
omega.
Qed.
Ltac intomega :=
repeat autounfold; unfold two_power_nat, shift_nat; simpl; omega.
Hint Resolve Z_lor_range_lo.
Hint Resolve Z_land_range_lo.
Hint Resolve Z_shiftl_32_range.
Hint Resolve Int.unsigned_range_2.
Hint Resolve cat_unsigned64_lor_range.
Hint Resolve Z.shiftr_nonneg.
Hint Resolve unsigned_shiftl_lor_shiftr_range.
Hint Resolve unsigned_shiftl_lor_shiftr_32_range.
Module TTRAPARGCODE.
Section WithPrimitives.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Section SYSHANDLERDMSR.
Let L: compatlayer (cdata RData) :=
rdmsr ↦ gensem thread_rdmsr_spec
⊕ vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
⊕ vmx_set_reg ↦ gensem thread_vmx_set_reg_spec
⊕ vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysHandleRdmsrBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import TacticsForTesting.
Require Import XOmega.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import TTrapArg.
Require Import TrapGenSpec.
Require Import TTrapArgCSource.
Require Import ObjTrap.
Require Import CommonTactic.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Lemma int_wrap:
Int.repr (-1) = Int.repr (Int.max_unsigned).
Proof.
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
reflexivity.
Qed.
Lemma unsigned_int_range:
∀ x: int,
0 ≤ Int.unsigned x ≤ Int64.max_unsigned.
Proof.
split.
apply Int.unsigned_range.
apply Z.le_trans with (m:=Int.max_unsigned);
( apply Int.unsigned_range_2 ||
unfold Int.max_unsigned, Int64.max_unsigned;
simpl; omega).
Qed.
Lemma cat_unsigned64_lor_range:
∀ lo hi,
0 ≤ Z.lor (Z.shiftl (Int.unsigned hi) 32) (Int.unsigned lo) ≤ Int64.max_unsigned.
Proof.
intros lo hi.
apply Z64_lor_range.
apply Z_shiftl_32_range.
apply Int.unsigned_range_2.
apply unsigned_int_range.
Qed.
Lemma unsigned_div_2pow32_eq_0:
∀ x, Int.unsigned x / 2 ^ 32 = 0.
Proof.
intro.
generalize (Int.unsigned_range x); intro.
repeat autounfold in H.
unfold two_power_nat, shift_nat in H.
simpl in H.
change (2 ^ 32) with 4294967296.
xomega.
Qed.
Lemma unsigned_shiftl_lor_shiftr_range:
∀ x y n,
0 ≤ n →
0 ≤ Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) n) (Int.unsigned y)) n ≤ Int.max_unsigned.
Proof.
split.
- apply Z.shiftr_nonneg.
apply Z_lor_range_lo.
+ apply Z.shiftl_nonneg.
apply Int.unsigned_range.
+ apply Int.unsigned_range.
- rewrite Z.shiftr_lor.
rewrite Z.shiftr_shiftl_r.
+ rewrite Z.sub_diag with (n:=n).
rewrite Z.shiftr_0_r.
rewrite Z.shiftr_div_pow2.
apply Z_lor_range.
apply Int.unsigned_range_2.
split.
× change 0 with (0 / 2 ^ n).
apply Z_div_le.
apply Z.lt_gt.
apply Z.pow_pos_nonneg; omega.
apply Int.unsigned_range.
× rewrite <- Z_div_mult_full with (a:=Int.max_unsigned)(b:=2^n).
{
apply Z_div_le.
- apply Z.lt_gt.
apply Z.pow_pos_nonneg; omega.
- apply Z.le_trans with (m:=Int.max_unsigned).
+ apply Int.unsigned_range_2.
+ apply Z.le_mul_diag_r with (n:=Int.max_unsigned)(m:=2^n).
× repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
omega.
× apply Zle_lt_or_eq in H.
destruct H.
{
generalize (Z.pow_gt_1 2 n).
intro Hr.
destruct Hr.
- omega.
- apply H0 in H.
omega.
}
rewrite <- H.
simpl.
omega.
}
apply Z.pow_nonzero.
omega.
assumption.
× assumption.
+ assumption.
Qed.
Lemma unsigned_shiftl_lor_shiftr_32_range:
∀ x y,
0 ≤ Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) 32) (Int.unsigned y)) 32 ≤ Int.max_unsigned.
Proof.
intros.
apply unsigned_shiftl_lor_shiftr_range with (n:=32).
omega.
Qed.
Lemma Z_mod_range:
∀ x n,
n > 0 →
0 ≤ x mod n ≤ n - 1.
Proof.
intros.
assert(0 ≤ x mod n < n).
apply Z_mod_lt.
omega.
omega.
Qed.
Ltac intomega :=
repeat autounfold; unfold two_power_nat, shift_nat; simpl; omega.
Hint Resolve Z_lor_range_lo.
Hint Resolve Z_land_range_lo.
Hint Resolve Z_shiftl_32_range.
Hint Resolve Int.unsigned_range_2.
Hint Resolve cat_unsigned64_lor_range.
Hint Resolve Z.shiftr_nonneg.
Hint Resolve unsigned_shiftl_lor_shiftr_range.
Hint Resolve unsigned_shiftl_lor_shiftr_32_range.
Module TTRAPARGCODE.
Section WithPrimitives.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Section SYSHANDLERDMSR.
Let L: compatlayer (cdata RData) :=
rdmsr ↦ gensem thread_rdmsr_spec
⊕ vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
⊕ vmx_set_reg ↦ gensem thread_vmx_set_reg_spec
⊕ vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysHandleRdmsrBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
rdmsr
Variable brdmsr: block.
Hypothesis hrdmsr1 : Genv.find_symbol ge rdmsr = Some brdmsr.
Hypothesis hrdmsr2 : Genv.find_funct_ptr ge brdmsr =
let arg_type := (Tcons tint Tnil) in
let ret_type := tulong in
let cal_conv := cc_default in
let prim := rdmsr in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hrdmsr1 : Genv.find_symbol ge rdmsr = Some brdmsr.
Hypothesis hrdmsr2 : Genv.find_funct_ptr ge brdmsr =
let arg_type := (Tcons tint Tnil) in
let ret_type := tulong in
let cal_conv := cc_default in
let prim := rdmsr in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_reg
Variable bvmx_get_reg: block.
Hypothesis hvmx_get_reg1 : Genv.find_symbol ge vmx_get_reg = Some bvmx_get_reg.
Hypothesis hvmx_get_reg2 : Genv.find_funct_ptr ge bvmx_get_reg =
let arg_type := Tcons tuint Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_reg in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_reg1 : Genv.find_symbol ge vmx_get_reg = Some bvmx_get_reg.
Hypothesis hvmx_get_reg2 : Genv.find_funct_ptr ge bvmx_get_reg =
let arg_type := Tcons tuint Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_reg in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_set_reg
Variable bvmx_set_reg: block.
Hypothesis hvmx_set_reg1 : Genv.find_symbol ge vmx_set_reg = Some bvmx_set_reg.
Hypothesis hvmx_set_reg2 : Genv.find_funct_ptr ge bvmx_set_reg =
let arg_type := Tcons tuint (Tcons tuint Tnil) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_reg in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_set_reg1 : Genv.find_symbol ge vmx_set_reg = Some bvmx_set_reg.
Hypothesis hvmx_set_reg2 : Genv.find_funct_ptr ge bvmx_set_reg =
let arg_type := Tcons tuint (Tcons tuint Tnil) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_reg in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_next_eip
Variable bvmx_get_next_eip: block.
Hypothesis hvmx_get_next_eip1 : Genv.find_symbol ge vmx_get_next_eip = Some bvmx_get_next_eip.
Hypothesis hvmx_get_next_eip2 : Genv.find_funct_ptr ge bvmx_get_next_eip =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_next_eip in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_next_eip1 : Genv.find_symbol ge vmx_get_next_eip = Some bvmx_get_next_eip.
Hypothesis hvmx_get_next_eip2 : Genv.find_funct_ptr ge bvmx_get_next_eip =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_next_eip in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
uctx_set_errno
Variable buctx_set_errno: block.
Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
Some (External (EF_external uctx_set_errno
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Lemma sys_handle_rdmsr_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_handle_rdmsr_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_handle_rdmsr_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize max_unsigned64_val; intro muval64.
intros; subst.
functional inversion H0; subst.
unfold sys_handle_rdmsr_body.
assert(0 ≤ val ≤ Int64.max_unsigned).
{
functional inversion H2.
functional inversion H9.
omega.
}
assert(0 ≤ next_eip ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H9; subst.
assumption.
}
assert(0 ≤ msr ≤ Int.max_unsigned).
{
functional inversion H1; subst;
functional inversion H10; subst;
apply Int.unsigned_range_2.
}
unfold val_low, val_high in ×.
change (2 ^ 32) with 4294967296 in ×.
assert (Hvalmodrange: 0 ≤ val mod 4294967296 ≤ Int64.max_unsigned).
{
split.
apply Z_mod_range.
omega.
apply Z.le_trans with (m:=Int.max_unsigned).
apply Z_mod_range.
omega.
omega.
}
assert (Hvalmodrange2: 0 ≤ val mod 4294967296 ≤ Int.max_unsigned).
{
split.
apply Z_mod_range.
omega.
apply Z_mod_range.
omega.
}
assert(Hvaldivrange: 0 ≤ val / 4294967296 ≤ Int64.max_unsigned).
{
unfold Int64.max_unsigned.
simpl.
unfold Int64.max_unsigned in H7.
simpl in H7.
xomega.
}
assert(Hvaldivrange2: 0 ≤ val / 4294967296 ≤ Int.max_unsigned).
{
unfold Int.max_unsigned.
simpl.
xomega.
}
esplit.
d3 vcgen.
repeat vcgen.
instantiate (1:=Int.repr msr); rewrite Int.unsigned_repr.
reflexivity.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:=Int64.repr val).
rewrite Int64.unsigned_repr.
reflexivity.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold Int64.modu.
repeat rewrite Int64.unsigned_repr.
eassumption.
intomega.
assumption.
assumption.
intomega.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold Int64.divu.
repeat rewrite Int64.unsigned_repr.
eassumption.
intomega.
assumption.
assumption.
intomega.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:=Int.repr next_eip); rewrite Int.unsigned_repr.
reflexivity.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
Qed.
End SysHandleRdmsrBody.
Theorem sys_handle_rdmsr_body_code_correct:
spec_le
(sys_handle_rdmsr ↦ trap_handle_rdmsr_spec_low)
(〚sys_handle_rdmsr ↦ f_sys_handle_rdmsr 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_handle_rdmsr_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_handle_rdmsr)
nil
(create_undef_temps (fn_temps f_sys_handle_rdmsr)))) H.
Qed.
End SYSHANDLERDMSR.
Section SYSHANDLEWRMSR.
Let L: compatlayer (cdata RData) :=
wrmsr ↦ gensem thread_wrmsr_spec
⊕ vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
⊕ vmx_set_reg ↦ gensem thread_vmx_set_reg_spec
⊕ vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysHandleWrmsrBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
Some (External (EF_external uctx_set_errno
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Lemma sys_handle_rdmsr_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_handle_rdmsr_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_handle_rdmsr_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize max_unsigned64_val; intro muval64.
intros; subst.
functional inversion H0; subst.
unfold sys_handle_rdmsr_body.
assert(0 ≤ val ≤ Int64.max_unsigned).
{
functional inversion H2.
functional inversion H9.
omega.
}
assert(0 ≤ next_eip ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H9; subst.
assumption.
}
assert(0 ≤ msr ≤ Int.max_unsigned).
{
functional inversion H1; subst;
functional inversion H10; subst;
apply Int.unsigned_range_2.
}
unfold val_low, val_high in ×.
change (2 ^ 32) with 4294967296 in ×.
assert (Hvalmodrange: 0 ≤ val mod 4294967296 ≤ Int64.max_unsigned).
{
split.
apply Z_mod_range.
omega.
apply Z.le_trans with (m:=Int.max_unsigned).
apply Z_mod_range.
omega.
omega.
}
assert (Hvalmodrange2: 0 ≤ val mod 4294967296 ≤ Int.max_unsigned).
{
split.
apply Z_mod_range.
omega.
apply Z_mod_range.
omega.
}
assert(Hvaldivrange: 0 ≤ val / 4294967296 ≤ Int64.max_unsigned).
{
unfold Int64.max_unsigned.
simpl.
unfold Int64.max_unsigned in H7.
simpl in H7.
xomega.
}
assert(Hvaldivrange2: 0 ≤ val / 4294967296 ≤ Int.max_unsigned).
{
unfold Int.max_unsigned.
simpl.
xomega.
}
esplit.
d3 vcgen.
repeat vcgen.
instantiate (1:=Int.repr msr); rewrite Int.unsigned_repr.
reflexivity.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:=Int64.repr val).
rewrite Int64.unsigned_repr.
reflexivity.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold Int64.modu.
repeat rewrite Int64.unsigned_repr.
eassumption.
intomega.
assumption.
assumption.
intomega.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold Int64.divu.
repeat rewrite Int64.unsigned_repr.
eassumption.
intomega.
assumption.
assumption.
intomega.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:=Int.repr next_eip); rewrite Int.unsigned_repr.
reflexivity.
assumption.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
Qed.
End SysHandleRdmsrBody.
Theorem sys_handle_rdmsr_body_code_correct:
spec_le
(sys_handle_rdmsr ↦ trap_handle_rdmsr_spec_low)
(〚sys_handle_rdmsr ↦ f_sys_handle_rdmsr 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_handle_rdmsr_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_handle_rdmsr)
nil
(create_undef_temps (fn_temps f_sys_handle_rdmsr)))) H.
Qed.
End SYSHANDLERDMSR.
Section SYSHANDLEWRMSR.
Let L: compatlayer (cdata RData) :=
wrmsr ↦ gensem thread_wrmsr_spec
⊕ vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
⊕ vmx_set_reg ↦ gensem thread_vmx_set_reg_spec
⊕ vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysHandleWrmsrBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
wrmsr
Variable bwrmsr: block.
Hypothesis hwrmsr1 : Genv.find_symbol ge wrmsr = Some bwrmsr.
Hypothesis hwrmsr2 : Genv.find_funct_ptr ge bwrmsr =
let arg_type := (Tcons tuint (Tcons tulong Tnil)) in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := wrmsr in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hwrmsr1 : Genv.find_symbol ge wrmsr = Some bwrmsr.
Hypothesis hwrmsr2 : Genv.find_funct_ptr ge bwrmsr =
let arg_type := (Tcons tuint (Tcons tulong Tnil)) in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := wrmsr in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_reg
Variable bvmx_get_reg: block.
Hypothesis hvmx_get_reg1 : Genv.find_symbol ge vmx_get_reg = Some bvmx_get_reg.
Hypothesis hvmx_get_reg2 : Genv.find_funct_ptr ge bvmx_get_reg =
let arg_type := Tcons tuint Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_reg in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_reg1 : Genv.find_symbol ge vmx_get_reg = Some bvmx_get_reg.
Hypothesis hvmx_get_reg2 : Genv.find_funct_ptr ge bvmx_get_reg =
let arg_type := Tcons tuint Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_reg in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_set_reg
Variable bvmx_set_reg: block.
Hypothesis hvmx_set_reg1 : Genv.find_symbol ge vmx_set_reg = Some bvmx_set_reg.
Hypothesis hvmx_set_reg2 : Genv.find_funct_ptr ge bvmx_set_reg =
let arg_type := Tcons tuint (Tcons tuint Tnil) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_reg in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_set_reg1 : Genv.find_symbol ge vmx_set_reg = Some bvmx_set_reg.
Hypothesis hvmx_set_reg2 : Genv.find_funct_ptr ge bvmx_set_reg =
let arg_type := Tcons tuint (Tcons tuint Tnil) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_reg in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_next_eip
Variable bvmx_get_next_eip: block.
Hypothesis hvmx_get_next_eip1 : Genv.find_symbol ge vmx_get_next_eip = Some bvmx_get_next_eip.
Hypothesis hvmx_get_next_eip2 : Genv.find_funct_ptr ge bvmx_get_next_eip =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_next_eip in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_next_eip1 : Genv.find_symbol ge vmx_get_next_eip = Some bvmx_get_next_eip.
Hypothesis hvmx_get_next_eip2 : Genv.find_funct_ptr ge bvmx_get_next_eip =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_next_eip in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
uctx_set_errno
Variable buctx_set_errno: block.
Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
Some (External (EF_external uctx_set_errno
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Lemma sys_handle_wrmsr_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_handle_wrmsr_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_handle_wrmsr_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize max_unsigned64_val; intro muval64.
intros; subst.
functional inversion H0; subst.
unfold sys_handle_wrmsr_body.
assert(0 ≤ eax ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H8.
apply Int.unsigned_range_2.
apply Int.unsigned_range_2.
}
assert(0 ≤ edx ≤ Int.max_unsigned).
{
functional inversion H3.
functional inversion H9.
apply Int.unsigned_range_2.
apply Int.unsigned_range_2.
}
assert(0 ≤ msr ≤ Int.max_unsigned).
{
functional inversion H1.
functional inversion H10.
apply Int.unsigned_range_2.
apply Int.unsigned_range_2.
}
assert(0 ≤ val ≤ Int64.max_unsigned).
{
functional inversion H4.
functional inversion H12.
unfold val.
unfold Int64.max_unsigned.
change (2 ^ 32) with 4294967296.
simpl.
unfold Int.max_unsigned in ×.
simpl in ×.
omega.
}
change (2 ^ 32) with 4294967296 in ×.
assert (Hvalmodrange: 0 ≤ val mod 4294967296 ≤ Int64.max_unsigned).
{
split.
apply Z_mod_range.
omega.
apply Z.le_trans with (m:=Int.max_unsigned).
apply Z_mod_range.
omega.
omega.
}
assert (Hvalmodrange2: 0 ≤ val mod 4294967296 ≤ Int.max_unsigned).
{
split.
apply Z_mod_range.
omega.
apply Z_mod_range.
omega.
}
assert(Hvaldivrange: 0 ≤ val / 4294967296 ≤ Int64.max_unsigned).
{
unfold Int64.max_unsigned.
simpl.
unfold Int64.max_unsigned in H7.
simpl in H7.
xomega.
}
assert(Hvaldivrange2: 0 ≤ val / 4294967296 ≤ Int.max_unsigned).
{
unfold Int.max_unsigned.
simpl.
xomega.
}
unfold val in ×.
esplit.
repeat vcgen.
instantiate (1:=Int.repr msr); rewrite Int.unsigned_repr.
reflexivity.
assumption.
rewrite H2.
instantiate (1:=Int.repr eax); rewrite Int.unsigned_repr.
reflexivity.
assumption.
rewrite H3.
instantiate (1:=Int.repr edx); rewrite Int.unsigned_repr.
reflexivity.
assumption.
repeat rewrite Int.unsigned_repr.
rewrite H4.
reflexivity.
functional inversion H4.
functional inversion H13.
intomega.
assumption.
assumption.
assumption.
rewrite Int.unsigned_repr.
intomega.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
intomega.
assumption.
repeat rewrite Int.unsigned_repr.
apply H11.
assumption.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
intomega.
assumption.
repeat rewrite Int.unsigned_repr.
intomega.
assumption.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
intomega.
assumption.
rewrite H5.
instantiate (1:=Int.repr next_eip); rewrite Int.unsigned_repr.
reflexivity.
assumption.
rewrite Int.unsigned_repr.
rewrite H7.
reflexivity.
assumption.
rewrite Int.unsigned_repr.
apply Z.le_trans with (m:=Int.max_unsigned).
omega.
omega.
assumption.
Qed.
End SysHandleWrmsrBody.
Theorem sys_handle_wrmsr_body_code_correct:
spec_le
(sys_handle_wrmsr ↦ trap_handle_wrmsr_spec_low)
(〚sys_handle_wrmsr ↦ f_sys_handle_wrmsr 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_handle_wrmsr_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_handle_wrmsr)
nil
(create_undef_temps (fn_temps f_sys_handle_wrmsr)))) H.
Qed.
End SYSHANDLEWRMSR.
End WithPrimitives.
End TTRAPARGCODE.
Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno =
Some (External (EF_external uctx_set_errno
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Lemma sys_handle_wrmsr_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_handle_wrmsr_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_handle_wrmsr_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize max_unsigned64_val; intro muval64.
intros; subst.
functional inversion H0; subst.
unfold sys_handle_wrmsr_body.
assert(0 ≤ eax ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H8.
apply Int.unsigned_range_2.
apply Int.unsigned_range_2.
}
assert(0 ≤ edx ≤ Int.max_unsigned).
{
functional inversion H3.
functional inversion H9.
apply Int.unsigned_range_2.
apply Int.unsigned_range_2.
}
assert(0 ≤ msr ≤ Int.max_unsigned).
{
functional inversion H1.
functional inversion H10.
apply Int.unsigned_range_2.
apply Int.unsigned_range_2.
}
assert(0 ≤ val ≤ Int64.max_unsigned).
{
functional inversion H4.
functional inversion H12.
unfold val.
unfold Int64.max_unsigned.
change (2 ^ 32) with 4294967296.
simpl.
unfold Int.max_unsigned in ×.
simpl in ×.
omega.
}
change (2 ^ 32) with 4294967296 in ×.
assert (Hvalmodrange: 0 ≤ val mod 4294967296 ≤ Int64.max_unsigned).
{
split.
apply Z_mod_range.
omega.
apply Z.le_trans with (m:=Int.max_unsigned).
apply Z_mod_range.
omega.
omega.
}
assert (Hvalmodrange2: 0 ≤ val mod 4294967296 ≤ Int.max_unsigned).
{
split.
apply Z_mod_range.
omega.
apply Z_mod_range.
omega.
}
assert(Hvaldivrange: 0 ≤ val / 4294967296 ≤ Int64.max_unsigned).
{
unfold Int64.max_unsigned.
simpl.
unfold Int64.max_unsigned in H7.
simpl in H7.
xomega.
}
assert(Hvaldivrange2: 0 ≤ val / 4294967296 ≤ Int.max_unsigned).
{
unfold Int.max_unsigned.
simpl.
xomega.
}
unfold val in ×.
esplit.
repeat vcgen.
instantiate (1:=Int.repr msr); rewrite Int.unsigned_repr.
reflexivity.
assumption.
rewrite H2.
instantiate (1:=Int.repr eax); rewrite Int.unsigned_repr.
reflexivity.
assumption.
rewrite H3.
instantiate (1:=Int.repr edx); rewrite Int.unsigned_repr.
reflexivity.
assumption.
repeat rewrite Int.unsigned_repr.
rewrite H4.
reflexivity.
functional inversion H4.
functional inversion H13.
intomega.
assumption.
assumption.
assumption.
rewrite Int.unsigned_repr.
intomega.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
intomega.
assumption.
repeat rewrite Int.unsigned_repr.
apply H11.
assumption.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
intomega.
assumption.
repeat rewrite Int.unsigned_repr.
intomega.
assumption.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
omega.
assumption.
rewrite Int.unsigned_repr.
intomega.
assumption.
rewrite H5.
instantiate (1:=Int.repr next_eip); rewrite Int.unsigned_repr.
reflexivity.
assumption.
rewrite Int.unsigned_repr.
rewrite H7.
reflexivity.
assumption.
rewrite Int.unsigned_repr.
apply Z.le_trans with (m:=Int.max_unsigned).
omega.
omega.
assumption.
Qed.
End SysHandleWrmsrBody.
Theorem sys_handle_wrmsr_body_code_correct:
spec_le
(sys_handle_wrmsr ↦ trap_handle_wrmsr_spec_low)
(〚sys_handle_wrmsr ↦ f_sys_handle_wrmsr 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_handle_wrmsr_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_handle_wrmsr)
nil
(create_undef_temps (fn_temps f_sys_handle_wrmsr)))) H.
Qed.
End SYSHANDLEWRMSR.
End WithPrimitives.
End TTRAPARGCODE.