Library mcertikos.trap.TTrapArgCode5
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 SYSSETTSCOFFSET.
Let L: compatlayer (cdata RData) :=
vmx_set_tsc_offset ↦ gensem thread_vmx_set_tsc_offset_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_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 SysSetTscOffsetBody.
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 SYSSETTSCOFFSET.
Let L: compatlayer (cdata RData) :=
vmx_set_tsc_offset ↦ gensem thread_vmx_set_tsc_offset_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_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 SysSetTscOffsetBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_set_tsc_offset
Variable bvmx_set_tsc_offset: block.
Hypothesis hvmx_set_tsc_offset1 : Genv.find_symbol ge vmx_set_tsc_offset = Some bvmx_set_tsc_offset.
Hypothesis hvmx_set_tsc_offset2 : Genv.find_funct_ptr ge bvmx_set_tsc_offset =
let arg_type := Tcons tulong Tnil in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_tsc_offset in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_set_tsc_offset1 : Genv.find_symbol ge vmx_set_tsc_offset = Some bvmx_set_tsc_offset.
Hypothesis hvmx_set_tsc_offset2 : Genv.find_funct_ptr ge bvmx_set_tsc_offset =
let arg_type := Tcons tulong Tnil in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_tsc_offset in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
uctx_arg2
Variable buctx_arg2: block.
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
uctx_arg3
Variable buctx_arg3: block.
Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
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_set_tsc_offset_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_set_tsc_offset_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_tsc_offset_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.
functional inversion H1.
functional inversion H2.
unfold sys_set_tsc_offset_body.
generalize (Int.unsigned_range_2 n); intro.
generalize (Int.unsigned_range_2 n0); intro.
rewrite <- H4 in ×.
rewrite <- H12 in ×.
unfold ofs in ×.
esplit.
repeat vcgen.
unfold Int64.add.
rewrite <- H12 in H3.
rewrite <- H4 in H3.
assumption.
Qed.
End SysSetTscOffsetBody.
Theorem sys_set_tsc_offset_body_code_correct:
spec_le
(sys_set_tsc_offset ↦ trap_set_tsc_offset_spec_low)
(〚sys_set_tsc_offset ↦ f_sys_set_tsc_offset 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_set_tsc_offset_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_set_tsc_offset)
nil
(create_undef_temps (fn_temps f_sys_set_tsc_offset)))) H.
Qed.
End SYSSETTSCOFFSET.
Section SYSGETTSCOFFSET.
Let L: compatlayer (cdata RData) :=
vmx_get_tsc_offset ↦ gensem thread_vmx_get_tsc_offset_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ uctx_set_retval2 ↦ gensem uctx_set_retval2_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 SysGetTscOffsetBody.
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_set_tsc_offset_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_set_tsc_offset_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_tsc_offset_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.
functional inversion H1.
functional inversion H2.
unfold sys_set_tsc_offset_body.
generalize (Int.unsigned_range_2 n); intro.
generalize (Int.unsigned_range_2 n0); intro.
rewrite <- H4 in ×.
rewrite <- H12 in ×.
unfold ofs in ×.
esplit.
repeat vcgen.
unfold Int64.add.
rewrite <- H12 in H3.
rewrite <- H4 in H3.
assumption.
Qed.
End SysSetTscOffsetBody.
Theorem sys_set_tsc_offset_body_code_correct:
spec_le
(sys_set_tsc_offset ↦ trap_set_tsc_offset_spec_low)
(〚sys_set_tsc_offset ↦ f_sys_set_tsc_offset 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_set_tsc_offset_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_set_tsc_offset)
nil
(create_undef_temps (fn_temps f_sys_set_tsc_offset)))) H.
Qed.
End SYSSETTSCOFFSET.
Section SYSGETTSCOFFSET.
Let L: compatlayer (cdata RData) :=
vmx_get_tsc_offset ↦ gensem thread_vmx_get_tsc_offset_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ uctx_set_retval2 ↦ gensem uctx_set_retval2_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 SysGetTscOffsetBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_get_tsc_offset
Variable bvmx_get_tsc_offset: block.
Hypothesis hvmx_get_tsc_offset1 : Genv.find_symbol ge vmx_get_tsc_offset = Some bvmx_get_tsc_offset.
Hypothesis hvmx_get_tsc_offset2 : Genv.find_funct_ptr ge bvmx_get_tsc_offset =
let arg_type := Tnil in
let ret_type := tulong in
let cal_conv := cc_default in
let prim := vmx_get_tsc_offset in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_tsc_offset1 : Genv.find_symbol ge vmx_get_tsc_offset = Some bvmx_get_tsc_offset.
Hypothesis hvmx_get_tsc_offset2 : Genv.find_funct_ptr ge bvmx_get_tsc_offset =
let arg_type := Tnil in
let ret_type := tulong in
let cal_conv := cc_default in
let prim := vmx_get_tsc_offset in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
uctx_set_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
uctx_set_retval2
Variable buctx_set_retval2: block.
Hypothesis huctx_set_retval21 : Genv.find_symbol ge uctx_set_retval2 = Some buctx_set_retval2.
Hypothesis huctx_set_retval22 : Genv.find_funct_ptr ge buctx_set_retval2 =
Some (External (EF_external uctx_set_retval2
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval21 : Genv.find_symbol ge uctx_set_retval2 = Some buctx_set_retval2.
Hypothesis huctx_set_retval22 : Genv.find_funct_ptr ge buctx_set_retval2 =
Some (External (EF_external uctx_set_retval2
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
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_get_tsc_offset_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_get_tsc_offset_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_get_tsc_offset_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 ofs1, ofs2 in ×.
unfold sys_get_tsc_offset_body.
assert(ofsrange: 0 ≤ ofs ≤ Int64.max_unsigned).
{
functional inversion H1; subst.
functional inversion H4; subst.
unfold Z64Lemma.Z64ofwords.
apply Z64_lor_range.
apply Z_shiftl_32_range.
apply Int.unsigned_range_2.
split.
discharge_unsigned_range.
apply Z.le_trans with (m:=Int.max_unsigned).
apply Int.unsigned_range_2.
omega.
}
assert(ofsmodrange: 0 ≤ ofs mod 4294967296 ≤ Int.max_unsigned).
{
apply Z_mod_range.
omega.
}
esplit.
d3 vcgen.
repeat vcgen.
instantiate (1:= (Int64.repr ofs)).
rewrite Int64.unsigned_repr.
reflexivity.
omega.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold Int64.divu.
repeat vcgen.
xomega.
xomega.
xomega.
xomega.
xomega.
repeat vcgen.
unfold Int64.modu.
repeat vcgen.
Qed.
End SysGetTscOffsetBody.
Theorem sys_get_tsc_offset_body_code_correct:
spec_le
(sys_get_tsc_offset ↦ trap_get_tsc_offset_spec_low)
(〚sys_get_tsc_offset ↦ f_sys_get_tsc_offset 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_get_tsc_offset_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_get_tsc_offset)
nil
(create_undef_temps (fn_temps f_sys_get_tsc_offset)))) H.
Qed.
End SYSGETTSCOFFSET.
Section SYSINJECTEVENT.
Let L: compatlayer (cdata RData) :=
uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
⊕ vmx_inject_event ↦ gensem thread_vmx_inject_event_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 SysInjectEventBody.
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_get_tsc_offset_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_get_tsc_offset_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_get_tsc_offset_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 ofs1, ofs2 in ×.
unfold sys_get_tsc_offset_body.
assert(ofsrange: 0 ≤ ofs ≤ Int64.max_unsigned).
{
functional inversion H1; subst.
functional inversion H4; subst.
unfold Z64Lemma.Z64ofwords.
apply Z64_lor_range.
apply Z_shiftl_32_range.
apply Int.unsigned_range_2.
split.
discharge_unsigned_range.
apply Z.le_trans with (m:=Int.max_unsigned).
apply Int.unsigned_range_2.
omega.
}
assert(ofsmodrange: 0 ≤ ofs mod 4294967296 ≤ Int.max_unsigned).
{
apply Z_mod_range.
omega.
}
esplit.
d3 vcgen.
repeat vcgen.
instantiate (1:= (Int64.repr ofs)).
rewrite Int64.unsigned_repr.
reflexivity.
omega.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold Int64.divu.
repeat vcgen.
xomega.
xomega.
xomega.
xomega.
xomega.
repeat vcgen.
unfold Int64.modu.
repeat vcgen.
Qed.
End SysGetTscOffsetBody.
Theorem sys_get_tsc_offset_body_code_correct:
spec_le
(sys_get_tsc_offset ↦ trap_get_tsc_offset_spec_low)
(〚sys_get_tsc_offset ↦ f_sys_get_tsc_offset 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_get_tsc_offset_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_get_tsc_offset)
nil
(create_undef_temps (fn_temps f_sys_get_tsc_offset)))) H.
Qed.
End SYSGETTSCOFFSET.
Section SYSINJECTEVENT.
Let L: compatlayer (cdata RData) :=
uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
⊕ vmx_inject_event ↦ gensem thread_vmx_inject_event_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 SysInjectEventBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
uctx_arg2
Variable buctx_arg2: block.
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
uctx_arg3
Variable buctx_arg3: block.
Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
uctx_arg4
Variable buctx_arg4: block.
Hypothesis huctx_arg41 : Genv.find_symbol ge uctx_arg4 = Some buctx_arg4.
Hypothesis huctx_arg42 : Genv.find_funct_ptr ge buctx_arg4 =
Some (External (EF_external uctx_arg4 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg41 : Genv.find_symbol ge uctx_arg4 = Some buctx_arg4.
Hypothesis huctx_arg42 : Genv.find_funct_ptr ge buctx_arg4 =
Some (External (EF_external uctx_arg4 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
vmx_inject_event
Variable bvmx_inject_event: block.
Hypothesis hvmx_inject_event1 : Genv.find_symbol ge vmx_inject_event = Some bvmx_inject_event.
Hypothesis hvmx_inject_event2 : Genv.find_funct_ptr ge bvmx_inject_event =
let arg_type := (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tuint Tnil)))) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_inject_event in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_inject_event1 : Genv.find_symbol ge vmx_inject_event = Some bvmx_inject_event.
Hypothesis hvmx_inject_event2 : Genv.find_funct_ptr ge bvmx_inject_event =
let arg_type := (Tcons tuint (Tcons tuint (Tcons tuint (Tcons tuint Tnil)))) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_inject_event 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_inject_event_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_inject_event_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_inject_event_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst.
functional inversion H2; subst.
functional inversion H3; subst.
unfold sys_inject_event_body.
assert(0 ≤ Int.unsigned n1 mod 256 ≤ Int.max_unsigned).
{
assert (0 ≤ Int.unsigned n1 mod 256 < 256).
{
eapply Z_mod_lt; omega.
}
omega.
}
esplit.
repeat vcgen.
discharge_cmp.
generalize (Int.unsigned_range n1); unfold Int.modulus, two_power_nat, shift_nat; simpl; intro.
xomega.
Qed.
End SysInjectEventBody.
Theorem sys_inject_event_code_correct:
spec_le
(sys_inject_event ↦ trap_inject_event_spec_low)
(〚sys_inject_event ↦ f_sys_inject_event 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_inject_event_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_inject_event)
nil
(create_undef_temps (fn_temps f_sys_inject_event)))) H.
Qed.
End SYSINJECTEVENT.
Section SYSSETREG.
Let L: compatlayer (cdata RData) :=
vmx_set_reg ↦ gensem thread_vmx_set_reg_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_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 SysSetRegBody.
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_inject_event_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_inject_event_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_inject_event_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst.
functional inversion H2; subst.
functional inversion H3; subst.
unfold sys_inject_event_body.
assert(0 ≤ Int.unsigned n1 mod 256 ≤ Int.max_unsigned).
{
assert (0 ≤ Int.unsigned n1 mod 256 < 256).
{
eapply Z_mod_lt; omega.
}
omega.
}
esplit.
repeat vcgen.
discharge_cmp.
generalize (Int.unsigned_range n1); unfold Int.modulus, two_power_nat, shift_nat; simpl; intro.
xomega.
Qed.
End SysInjectEventBody.
Theorem sys_inject_event_code_correct:
spec_le
(sys_inject_event ↦ trap_inject_event_spec_low)
(〚sys_inject_event ↦ f_sys_inject_event 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_inject_event_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_inject_event)
nil
(create_undef_temps (fn_temps f_sys_inject_event)))) H.
Qed.
End SYSINJECTEVENT.
Section SYSSETREG.
Let L: compatlayer (cdata RData) :=
vmx_set_reg ↦ gensem thread_vmx_set_reg_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_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 SysSetRegBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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).
uctx_arg2
Variable buctx_arg2: block.
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
uctx_arg3
Variable buctx_arg3: block.
Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
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_set_reg_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_set_reg_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_reg_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst;
functional inversion H2; subst;
functional inversion H4; subst;
functional inversion H5; subst;
rewrite Int.repr_unsigned in H, H4;
unfold sys_set_reg_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
functional inversion H1; subst;
functional inversion H2; subst.
destruct _x;
unfold sys_set_reg_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
Qed.
End SysSetRegBody.
Theorem sys_set_reg_body_code_correct:
spec_le
(sys_set_reg ↦ trap_set_reg_spec_low)
(〚sys_set_reg ↦ f_sys_set_reg 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_set_reg_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_set_reg)
nil
(create_undef_temps (fn_temps f_sys_set_reg)))) H.
Qed.
End SYSSETREG.
Section SYSGETREG.
Let L: compatlayer (cdata RData) :=
vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_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 SysGetRegBody.
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_set_reg_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_set_reg_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_reg_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst;
functional inversion H2; subst;
functional inversion H4; subst;
functional inversion H5; subst;
rewrite Int.repr_unsigned in H, H4;
unfold sys_set_reg_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
functional inversion H1; subst;
functional inversion H2; subst.
destruct _x;
unfold sys_set_reg_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
Qed.
End SysSetRegBody.
Theorem sys_set_reg_body_code_correct:
spec_le
(sys_set_reg ↦ trap_set_reg_spec_low)
(〚sys_set_reg ↦ f_sys_set_reg 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_set_reg_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_set_reg)
nil
(create_undef_temps (fn_temps f_sys_set_reg)))) H.
Qed.
End SYSSETREG.
Section SYSGETREG.
Let L: compatlayer (cdata RData) :=
vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_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 SysGetRegBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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).
uctx_arg2
Variable buctx_arg2: block.
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
uctx_set_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
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_get_reg_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_get_reg_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_get_reg_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst.
functional inversion H3; subst.
functional inversion H5; subst.
unfold sys_get_reg_body.
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
unfold sys_get_reg_body.
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
unfold sys_get_reg_body.
functional inversion H1; subst.
destruct _x.
esplit;
repeat vcgen.
esplit; repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
Qed.
End SysGetRegBody.
Theorem sys_get_reg_body_code_correct:
spec_le
(sys_get_reg ↦ trap_get_reg_spec_low)
(〚sys_get_reg ↦ f_sys_get_reg 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_get_reg_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_get_reg)
nil
(create_undef_temps (fn_temps f_sys_get_reg)))) H.
Qed.
End SYSGETREG.
Section SYSGETNEXTEIP.
Let L: compatlayer (cdata RData) :=
vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_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 SysGetNextEipBody.
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_get_reg_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_get_reg_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_get_reg_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst.
functional inversion H3; subst.
functional inversion H5; subst.
unfold sys_get_reg_body.
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
unfold sys_get_reg_body.
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
unfold sys_get_reg_body.
functional inversion H1; subst.
destruct _x.
esplit;
repeat vcgen.
esplit; repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
Qed.
End SysGetRegBody.
Theorem sys_get_reg_body_code_correct:
spec_le
(sys_get_reg ↦ trap_get_reg_spec_low)
(〚sys_get_reg ↦ f_sys_get_reg 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_get_reg_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_get_reg)
nil
(create_undef_temps (fn_temps f_sys_get_reg)))) H.
Qed.
End SYSGETREG.
Section SYSGETNEXTEIP.
Let L: compatlayer (cdata RData) :=
vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_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 SysGetNextEipBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
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_get_next_eip_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_get_next_eip_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_get_next_eip_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst.
functional inversion H4; subst.
unfold sys_get_next_eip_body.
esplit;
repeat vcgen.
instantiate (1:= (Int.repr (Int.unsigned v1 + Int.unsigned v2))).
rewrite Int.unsigned_repr; try omega.
reflexivity.
rewrite Int.unsigned_repr; try omega.
eassumption.
Qed.
End SysGetNextEipBody.
Theorem sys_get_next_eip_code_correct:
spec_le
(sys_get_next_eip ↦ trap_get_next_eip_spec_low)
(〚sys_get_next_eip ↦ f_sys_get_next_eip 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_get_next_eip_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_get_next_eip)
nil
(create_undef_temps (fn_temps f_sys_get_next_eip)))) H.
Qed.
End SYSGETNEXTEIP.
Section SYSINTERCEPTINTWINDOW.
Let L: compatlayer (cdata RData) :=
vmx_set_intercept_intwin ↦ gensem thread_vmx_set_intercept_intwin_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_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 SysInterceptIntWindowBody.
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_get_next_eip_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_get_next_eip_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_get_next_eip_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst.
functional inversion H4; subst.
unfold sys_get_next_eip_body.
esplit;
repeat vcgen.
instantiate (1:= (Int.repr (Int.unsigned v1 + Int.unsigned v2))).
rewrite Int.unsigned_repr; try omega.
reflexivity.
rewrite Int.unsigned_repr; try omega.
eassumption.
Qed.
End SysGetNextEipBody.
Theorem sys_get_next_eip_code_correct:
spec_le
(sys_get_next_eip ↦ trap_get_next_eip_spec_low)
(〚sys_get_next_eip ↦ f_sys_get_next_eip 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_get_next_eip_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_get_next_eip)
nil
(create_undef_temps (fn_temps f_sys_get_next_eip)))) H.
Qed.
End SYSGETNEXTEIP.
Section SYSINTERCEPTINTWINDOW.
Let L: compatlayer (cdata RData) :=
vmx_set_intercept_intwin ↦ gensem thread_vmx_set_intercept_intwin_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_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 SysInterceptIntWindowBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_set_intercept_intwin
Variable bvmx_set_intercept_intwin: block.
Hypothesis hvmx_set_intercept_intwin1 : Genv.find_symbol ge vmx_set_intercept_intwin = Some bvmx_set_intercept_intwin.
Hypothesis hvmx_set_intercept_intwin2 : Genv.find_funct_ptr ge bvmx_set_intercept_intwin =
let arg_type := Tcons tint Tnil in
let ret_type := Tvoid in
let cal_conv := cc_default in
let prim := vmx_set_intercept_intwin in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_set_intercept_intwin1 : Genv.find_symbol ge vmx_set_intercept_intwin = Some bvmx_set_intercept_intwin.
Hypothesis hvmx_set_intercept_intwin2 : Genv.find_funct_ptr ge bvmx_set_intercept_intwin =
let arg_type := Tcons tint Tnil in
let ret_type := Tvoid in
let cal_conv := cc_default in
let prim := vmx_set_intercept_intwin in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
uctx_arg2
Variable buctx_arg2: block.
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
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_intercept_int_window_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_intercept_int_window_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_intercept_intwin_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst.
functional inversion H2; subst;
functional inversion H3; subst;
unfold sys_set_intercept_intwin_body;
esplit;
repeat vcgen.
Qed.
End SysInterceptIntWindowBody.
Theorem sys_intercept_int_window_code_correct:
spec_le
(sys_intercept_int_window ↦ trap_intercept_int_window_spec_low)
(〚sys_intercept_int_window ↦ f_sys_set_intercept_intwin 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_intercept_int_window_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_set_intercept_intwin)
nil
(create_undef_temps (fn_temps f_sys_set_intercept_intwin)))) H.
Qed.
End SYSINTERCEPTINTWINDOW.
Section SYSCHECKPENDINGEVENT.
Let L: compatlayer (cdata RData) :=
vmx_check_pending_event ↦ gensem thread_vmx_check_pending_event_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_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 SysCheckPendingEventBody.
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_intercept_int_window_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_intercept_int_window_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_intercept_intwin_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst.
functional inversion H2; subst;
functional inversion H3; subst;
unfold sys_set_intercept_intwin_body;
esplit;
repeat vcgen.
Qed.
End SysInterceptIntWindowBody.
Theorem sys_intercept_int_window_code_correct:
spec_le
(sys_intercept_int_window ↦ trap_intercept_int_window_spec_low)
(〚sys_intercept_int_window ↦ f_sys_set_intercept_intwin 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_intercept_int_window_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_set_intercept_intwin)
nil
(create_undef_temps (fn_temps f_sys_set_intercept_intwin)))) H.
Qed.
End SYSINTERCEPTINTWINDOW.
Section SYSCHECKPENDINGEVENT.
Let L: compatlayer (cdata RData) :=
vmx_check_pending_event ↦ gensem thread_vmx_check_pending_event_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_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 SysCheckPendingEventBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_check_int_shadow
Variable bvmx_check_pending_event: block.
Hypothesis hvmx_check_pending_event1 : Genv.find_symbol ge vmx_check_pending_event = Some bvmx_check_pending_event.
Hypothesis hvmx_check_pending_event2 : Genv.find_funct_ptr ge bvmx_check_pending_event =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_check_pending_event in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_check_pending_event1 : Genv.find_symbol ge vmx_check_pending_event = Some bvmx_check_pending_event.
Hypothesis hvmx_check_pending_event2 : Genv.find_funct_ptr ge bvmx_check_pending_event =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_check_pending_event in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
uctx_set_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
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_check_pending_event_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_check_pending_event_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_check_pending_event_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst;
functional inversion H3; subst;
rewrite <- Int.unsigned_repr in H1 at 1;
try omega;
unfold sys_check_pending_event_body;
esplit;
repeat vcgen.
Qed.
End SysCheckPendingEventBody.
Theorem sys_check_pending_event_code_correct:
spec_le
(sys_check_pending_event ↦ trap_check_pending_event_spec_low)
(〚sys_check_pending_event ↦ f_sys_check_pending_event 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_check_pending_event_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_check_pending_event)
nil
(create_undef_temps (fn_temps f_sys_check_pending_event)))) H.
Qed.
End SYSCHECKPENDINGEVENT.
Section SYSCHECKINTSHADOW.
Let L: compatlayer (cdata RData) :=
uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ vmx_check_int_shadow ↦ gensem thread_vmx_check_int_shadow_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 SysCheckIntShadowBody.
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_check_pending_event_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_check_pending_event_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_check_pending_event_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst;
functional inversion H3; subst;
rewrite <- Int.unsigned_repr in H1 at 1;
try omega;
unfold sys_check_pending_event_body;
esplit;
repeat vcgen.
Qed.
End SysCheckPendingEventBody.
Theorem sys_check_pending_event_code_correct:
spec_le
(sys_check_pending_event ↦ trap_check_pending_event_spec_low)
(〚sys_check_pending_event ↦ f_sys_check_pending_event 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_check_pending_event_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_check_pending_event)
nil
(create_undef_temps (fn_temps f_sys_check_pending_event)))) H.
Qed.
End SYSCHECKPENDINGEVENT.
Section SYSCHECKINTSHADOW.
Let L: compatlayer (cdata RData) :=
uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ vmx_check_int_shadow ↦ gensem thread_vmx_check_int_shadow_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 SysCheckIntShadowBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_check_int_shadow
Variable bvmx_check_int_shadow: block.
Hypothesis hvmx_check_int_shadow1 : Genv.find_symbol ge vmx_check_int_shadow = Some bvmx_check_int_shadow.
Hypothesis hvmx_check_int_shadow2 : Genv.find_funct_ptr ge bvmx_check_int_shadow =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_check_int_shadow in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_check_int_shadow1 : Genv.find_symbol ge vmx_check_int_shadow = Some bvmx_check_int_shadow.
Hypothesis hvmx_check_int_shadow2 : Genv.find_funct_ptr ge bvmx_check_int_shadow =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_check_int_shadow in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
uctx_set_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
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_check_int_shadow_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_check_int_shadow_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_check_int_shadow_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst;
functional inversion H3; subst;
rewrite <- Int.unsigned_repr in H1 at 1;
try omega;
unfold sys_check_int_shadow_body;
esplit;
repeat vcgen.
Qed.
End SysCheckIntShadowBody.
Theorem sys_check_int_shadow_code_correct:
spec_le
(sys_check_int_shadow ↦ trap_check_int_shadow_spec_low)
(〚sys_check_int_shadow ↦ f_sys_check_int_shadow 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_check_int_shadow_body_correct
s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
b2 Hb2fs Hb2fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_check_int_shadow)
nil
(create_undef_temps (fn_temps f_sys_check_int_shadow)))) H.
Qed.
End SYSCHECKINTSHADOW.
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_check_int_shadow_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_check_int_shadow_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_check_int_shadow_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; subst;
functional inversion H3; subst;
rewrite <- Int.unsigned_repr in H1 at 1;
try omega;
unfold sys_check_int_shadow_body;
esplit;
repeat vcgen.
Qed.
End SysCheckIntShadowBody.
Theorem sys_check_int_shadow_code_correct:
spec_le
(sys_check_int_shadow ↦ trap_check_int_shadow_spec_low)
(〚sys_check_int_shadow ↦ f_sys_check_int_shadow 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_check_int_shadow_body_correct
s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp
b0 Hb0fs Hb0fp
b2 Hb2fs Hb2fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_check_int_shadow)
nil
(create_undef_temps (fn_temps f_sys_check_int_shadow)))) H.
Qed.
End SYSCHECKINTSHADOW.
End WithPrimitives.
End TTRAPARGCODE.