Library mcertikos.trap.TTrapArgCode4
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 SYSGETEXITINFO.
Let L: compatlayer (cdata RData) :=
vmx_get_exit_reason ↦ gensem thread_vmx_get_exit_reason_spec
⊕ vmx_get_exit_io_port ↦ gensem thread_vmx_get_exit_io_port_spec
⊕ vmx_get_io_width ↦ gensem thread_vmx_get_io_width_spec
⊕ vmx_get_io_write ↦ gensem thread_vmx_get_io_write_spec
⊕ vmx_get_exit_io_rep ↦ gensem thread_vmx_get_exit_io_rep_spec
⊕ vmx_get_exit_io_str ↦ gensem thread_vmx_get_exit_io_str_spec
⊕ vmx_get_exit_fault_addr ↦ gensem thread_vmx_get_exit_fault_addr_spec
⊕ vmx_get_exit_qualification ↦ gensem thread_vmx_get_exit_qualification_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ uctx_set_retval2 ↦ gensem uctx_set_retval2_spec
⊕ uctx_set_retval3 ↦ gensem uctx_set_retval3_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 SysGetExitinfoBody.
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 SYSGETEXITINFO.
Let L: compatlayer (cdata RData) :=
vmx_get_exit_reason ↦ gensem thread_vmx_get_exit_reason_spec
⊕ vmx_get_exit_io_port ↦ gensem thread_vmx_get_exit_io_port_spec
⊕ vmx_get_io_width ↦ gensem thread_vmx_get_io_width_spec
⊕ vmx_get_io_write ↦ gensem thread_vmx_get_io_write_spec
⊕ vmx_get_exit_io_rep ↦ gensem thread_vmx_get_exit_io_rep_spec
⊕ vmx_get_exit_io_str ↦ gensem thread_vmx_get_exit_io_str_spec
⊕ vmx_get_exit_fault_addr ↦ gensem thread_vmx_get_exit_fault_addr_spec
⊕ vmx_get_exit_qualification ↦ gensem thread_vmx_get_exit_qualification_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ uctx_set_retval2 ↦ gensem uctx_set_retval2_spec
⊕ uctx_set_retval3 ↦ gensem uctx_set_retval3_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 SysGetExitinfoBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_get_exit_reason
Variable bvmx_get_exit_reason: block.
Hypothesis hvmx_get_exit_reason1 : Genv.find_symbol ge vmx_get_exit_reason = Some bvmx_get_exit_reason.
Hypothesis hvmx_get_exit_reason2 : Genv.find_funct_ptr ge bvmx_get_exit_reason =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_reason in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_exit_reason1 : Genv.find_symbol ge vmx_get_exit_reason = Some bvmx_get_exit_reason.
Hypothesis hvmx_get_exit_reason2 : Genv.find_funct_ptr ge bvmx_get_exit_reason =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_reason in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_exit_io_port
Variable bvmx_get_exit_io_port: block.
Hypothesis hvmx_get_exit_io_port1 : Genv.find_symbol ge vmx_get_exit_io_port = Some bvmx_get_exit_io_port.
Hypothesis hvmx_get_exit_io_port2 : Genv.find_funct_ptr ge bvmx_get_exit_io_port =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_io_port in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_exit_io_port1 : Genv.find_symbol ge vmx_get_exit_io_port = Some bvmx_get_exit_io_port.
Hypothesis hvmx_get_exit_io_port2 : Genv.find_funct_ptr ge bvmx_get_exit_io_port =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_io_port in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_io_width
Variable bvmx_get_io_width: block.
Hypothesis hvmx_get_io_width1 : Genv.find_symbol ge vmx_get_io_width = Some bvmx_get_io_width.
Hypothesis hvmx_get_io_width2 : Genv.find_funct_ptr ge bvmx_get_io_width =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_io_width in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_io_width1 : Genv.find_symbol ge vmx_get_io_width = Some bvmx_get_io_width.
Hypothesis hvmx_get_io_width2 : Genv.find_funct_ptr ge bvmx_get_io_width =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_io_width in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_io_write
Variable bvmx_get_io_write: block.
Hypothesis hvmx_get_io_write1 : Genv.find_symbol ge vmx_get_io_write = Some bvmx_get_io_write.
Hypothesis hvmx_get_io_write2 : Genv.find_funct_ptr ge bvmx_get_io_write =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_io_write in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_io_write1 : Genv.find_symbol ge vmx_get_io_write = Some bvmx_get_io_write.
Hypothesis hvmx_get_io_write2 : Genv.find_funct_ptr ge bvmx_get_io_write =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_io_write in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_exit_io_rep
Variable bvmx_get_exit_io_rep: block.
Hypothesis hvmx_get_exit_io_rep1 : Genv.find_symbol ge vmx_get_exit_io_rep = Some bvmx_get_exit_io_rep.
Hypothesis hvmx_get_exit_io_rep2 : Genv.find_funct_ptr ge bvmx_get_exit_io_rep =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_io_rep in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_exit_io_rep1 : Genv.find_symbol ge vmx_get_exit_io_rep = Some bvmx_get_exit_io_rep.
Hypothesis hvmx_get_exit_io_rep2 : Genv.find_funct_ptr ge bvmx_get_exit_io_rep =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_io_rep in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_exit_io_str
Variable bvmx_get_exit_io_str: block.
Hypothesis hvmx_get_exit_io_str1 : Genv.find_symbol ge vmx_get_exit_io_str = Some bvmx_get_exit_io_str.
Hypothesis hvmx_get_exit_io_str2 : Genv.find_funct_ptr ge bvmx_get_exit_io_str =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_io_str in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_exit_io_str1 : Genv.find_symbol ge vmx_get_exit_io_str = Some bvmx_get_exit_io_str.
Hypothesis hvmx_get_exit_io_str2 : Genv.find_funct_ptr ge bvmx_get_exit_io_str =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_io_str in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_exit_fault_addr
Variable bvmx_get_exit_fault_addr: block.
Hypothesis hvmx_get_exit_fault_addr1 : Genv.find_symbol ge vmx_get_exit_fault_addr = Some bvmx_get_exit_fault_addr.
Hypothesis hvmx_get_exit_fault_addr2 : Genv.find_funct_ptr ge bvmx_get_exit_fault_addr =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_fault_addr in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_exit_fault_addr1 : Genv.find_symbol ge vmx_get_exit_fault_addr = Some bvmx_get_exit_fault_addr.
Hypothesis hvmx_get_exit_fault_addr2 : Genv.find_funct_ptr ge bvmx_get_exit_fault_addr =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_fault_addr in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
vmx_get_exit_qualification
Variable bvmx_get_exit_qualification: block.
Hypothesis hvmx_get_exit_qualification1 : Genv.find_symbol ge vmx_get_exit_qualification = Some bvmx_get_exit_qualification.
Hypothesis hvmx_get_exit_qualification2 : Genv.find_funct_ptr ge bvmx_get_exit_qualification =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_qualification in
Some (External (EF_external prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_get_exit_qualification1 : Genv.find_symbol ge vmx_get_exit_qualification = Some bvmx_get_exit_qualification.
Hypothesis hvmx_get_exit_qualification2 : Genv.find_funct_ptr ge bvmx_get_exit_qualification =
let arg_type := Tnil in
let ret_type := tuint in
let cal_conv := cc_default in
let prim := vmx_get_exit_qualification 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_retval3
Variable buctx_set_retval3: block.
Hypothesis huctx_set_retval31 : Genv.find_symbol ge uctx_set_retval3 = Some buctx_set_retval3.
Hypothesis huctx_set_retval32 : Genv.find_funct_ptr ge buctx_set_retval3 =
Some (External (EF_external uctx_set_retval3
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval31 : Genv.find_symbol ge uctx_set_retval3 = Some buctx_set_retval3.
Hypothesis huctx_set_retval32 : Genv.find_funct_ptr ge buctx_set_retval3 =
Some (External (EF_external uctx_set_retval3
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
uctx_set_retval4
Variable buctx_set_retval4: block.
Hypothesis huctx_set_retval41 : Genv.find_symbol ge uctx_set_retval4 = Some buctx_set_retval4.
Hypothesis huctx_set_retval42 : Genv.find_funct_ptr ge buctx_set_retval4 =
Some (External (EF_external uctx_set_retval4
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval41 : Genv.find_symbol ge uctx_set_retval4 = Some buctx_set_retval4.
Hypothesis huctx_set_retval42 : Genv.find_funct_ptr ge buctx_set_retval4 =
Some (External (EF_external uctx_set_retval4
(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_exitinfo_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_get_exitinfo_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_get_exitinfo_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
assert(0 ≤ port ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H13.
repeat discharge_unsigned_range.
}
assert(0 ≤ width ≤ 3).
{
functional inversion H3;
functional inversion H14;
intomega.
}
assert(0 ≤ write ≤ 1).
{
functional inversion H4;
functional inversion H15;
intomega.
}
assert(0 ≤ rep ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H16; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 5) with 32.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ str ≤ Int.max_unsigned).
{
functional inversion H6; subst.
functional inversion H17; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 4) with 16.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ fault_addr ≤ Int.max_unsigned).
{
functional inversion H7; subst.
functional inversion H18; subst.
repeat discharge_unsigned_range.
}
assert(0 ≤ addr ≤ Int.max_unsigned).
{
functional inversion H8; subst.
functional inversion H19; subst.
repeat discharge_unsigned_range.
}
rewrite <- Int.unsigned_repr in H2 at 1; try omega.
rewrite <- Int.unsigned_repr in H3 at 1; try omega.
rewrite <- Int.unsigned_repr in H4 at 1; try omega.
rewrite <- Int.unsigned_repr in H5 at 1; try omega.
rewrite <- Int.unsigned_repr in H6 at 1; try omega.
rewrite <- Int.unsigned_repr in H7 at 1; try omega.
rewrite <- Int.unsigned_repr in H8 at 1; try omega.
unfold flags in ×.
unfold get_flags in H12.
subdestruct; subst.
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 0 1) with 1 in H12.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 0 2) with 2 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 1 2) with 3 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 0 4) with 4 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 1 4) with 5 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor (Z.lor 0 2) 4) with 6 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor (Z.lor 1 2) 4) with 7 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
assert(0 ≤ port ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H13.
repeat discharge_unsigned_range.
}
assert(0 ≤ width ≤ 3).
{
functional inversion H3;
functional inversion H14;
intomega.
}
assert(0 ≤ write ≤ 1).
{
functional inversion H4;
functional inversion H15;
intomega.
}
assert(0 ≤ rep ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H16; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 5) with 32.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ str ≤ Int.max_unsigned).
{
functional inversion H6; subst.
functional inversion H17; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 4) with 16.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ fault_addr ≤ Int.max_unsigned).
{
functional inversion H7; subst.
functional inversion H18; subst.
repeat discharge_unsigned_range.
}
assert(0 ≤ addr ≤ Int.max_unsigned).
{
functional inversion H8; subst.
functional inversion H19; subst.
repeat discharge_unsigned_range.
}
rewrite <- Int.unsigned_repr in H2 at 1; try omega.
rewrite <- Int.unsigned_repr in H3 at 1; try omega.
rewrite <- Int.unsigned_repr in H4 at 1; try omega.
rewrite <- Int.unsigned_repr in H5 at 1; try omega.
rewrite <- Int.unsigned_repr in H6 at 1; try omega.
rewrite <- Int.unsigned_repr in H7 at 1; try omega.
rewrite <- Int.unsigned_repr in H8 at 1; try omega.
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 48)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
}
{
assert(0 ≤ port ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H14.
repeat discharge_unsigned_range.
}
assert(0 ≤ width ≤ 3).
{
functional inversion H3;
functional inversion H15;
intomega.
}
assert(0 ≤ write ≤ 1).
{
functional inversion H4;
functional inversion H16;
intomega.
}
assert(0 ≤ rep ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H17; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 5) with 32.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ str ≤ Int.max_unsigned).
{
functional inversion H6; subst.
functional inversion H18; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 4) with 16.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ fault_addr ≤ Int.max_unsigned).
{
functional inversion H7; subst.
functional inversion H19; subst.
repeat discharge_unsigned_range.
}
assert(0 ≤ addr ≤ Int.max_unsigned).
{
functional inversion H8; subst.
functional inversion H20; subst.
repeat discharge_unsigned_range.
}
rewrite <- Int.unsigned_repr in H2 at 1; try omega.
rewrite <- Int.unsigned_repr in H3 at 1; try omega.
rewrite <- Int.unsigned_repr in H4 at 1; try omega.
rewrite <- Int.unsigned_repr in H5 at 1; try omega.
rewrite <- Int.unsigned_repr in H6 at 1; try omega.
rewrite <- Int.unsigned_repr in H7 at 1; try omega.
rewrite <- Int.unsigned_repr in H8 at 1; try omega.
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 28)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
}
{
assert(0 ≤ reason ≤ Int.max_unsigned).
{
functional inversion H1; subst.
functional inversion H13; subst.
apply Z_land_range.
repeat discharge_unsigned_range.
omega.
}
assert(0 ≤ port ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H14.
repeat discharge_unsigned_range.
}
assert(0 ≤ width ≤ Int.max_unsigned).
{
functional inversion H3;
functional inversion H15;
intomega.
}
assert(0 ≤ write ≤ Int.max_unsigned).
{
functional inversion H4;
functional inversion H16;
intomega.
}
assert(0 ≤ rep ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H17; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 5) with 32.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ str ≤ Int.max_unsigned).
{
functional inversion H6; subst.
functional inversion H18; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 4) with 16.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ fault_addr ≤ Int.max_unsigned).
{
functional inversion H7; subst.
functional inversion H19; subst.
repeat discharge_unsigned_range.
}
assert(0 ≤ addr ≤ Int.max_unsigned).
{
functional inversion H8; subst.
functional inversion H20; subst.
repeat discharge_unsigned_range.
}
rewrite <- Int.unsigned_repr in H1 at 1; try omega.
rewrite <- Int.unsigned_repr in H2 at 1; try omega.
rewrite <- Int.unsigned_repr in H3 at 1; try omega.
rewrite <- Int.unsigned_repr in H4 at 1; try omega.
rewrite <- Int.unsigned_repr in H5 at 1; try omega.
rewrite <- Int.unsigned_repr in H6 at 1; try omega.
rewrite <- Int.unsigned_repr in H7 at 1; try omega.
rewrite <- Int.unsigned_repr in H8 at 1; try omega.
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
}
Qed.
End SysGetExitinfoBody.
Theorem sys_get_exitinfo_body_code_correct:
spec_le
(sys_get_exitinfo ↦ trap_get_exitinfo_spec_low)
(〚sys_get_exitinfo ↦ f_sys_get_exitinfo 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_get_exitinfo_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
b5 Hb5fs Hb5fp
b6 Hb6fs Hb6fp
b7 Hb7fs Hb7fp
b8 Hb8fs Hb8fp
b9 Hb9fs Hb9fp
b10 Hb10fs Hb10fp
b11 Hb11fs Hb11fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_get_exitinfo)
nil
(create_undef_temps (fn_temps f_sys_get_exitinfo)))) H.
Qed.
End SYSGETEXITINFO.
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_get_exitinfo_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_get_exitinfo_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_get_exitinfo_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
assert(0 ≤ port ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H13.
repeat discharge_unsigned_range.
}
assert(0 ≤ width ≤ 3).
{
functional inversion H3;
functional inversion H14;
intomega.
}
assert(0 ≤ write ≤ 1).
{
functional inversion H4;
functional inversion H15;
intomega.
}
assert(0 ≤ rep ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H16; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 5) with 32.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ str ≤ Int.max_unsigned).
{
functional inversion H6; subst.
functional inversion H17; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 4) with 16.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ fault_addr ≤ Int.max_unsigned).
{
functional inversion H7; subst.
functional inversion H18; subst.
repeat discharge_unsigned_range.
}
assert(0 ≤ addr ≤ Int.max_unsigned).
{
functional inversion H8; subst.
functional inversion H19; subst.
repeat discharge_unsigned_range.
}
rewrite <- Int.unsigned_repr in H2 at 1; try omega.
rewrite <- Int.unsigned_repr in H3 at 1; try omega.
rewrite <- Int.unsigned_repr in H4 at 1; try omega.
rewrite <- Int.unsigned_repr in H5 at 1; try omega.
rewrite <- Int.unsigned_repr in H6 at 1; try omega.
rewrite <- Int.unsigned_repr in H7 at 1; try omega.
rewrite <- Int.unsigned_repr in H8 at 1; try omega.
unfold flags in ×.
unfold get_flags in H12.
subdestruct; subst.
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 0 1) with 1 in H12.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 0 2) with 2 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 1 2) with 3 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 0 4) with 4 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor 1 4) with 5 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor (Z.lor 0 2) 4) with 6 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 30)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
discharge_cmp.
discharge_cmp.
repeat vcgen.
ptreesolve.
ptreesolve.
discharge_cmp.
discharge_cmp.
discharge_cmp.
change (Z.lor (Z.lor 1 2) 4) with 7 in ×.
rewrite Int.unsigned_repr.
assumption.
apply Z_lor_range.
omega.
omega.
}
{
assert(0 ≤ port ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H13.
repeat discharge_unsigned_range.
}
assert(0 ≤ width ≤ 3).
{
functional inversion H3;
functional inversion H14;
intomega.
}
assert(0 ≤ write ≤ 1).
{
functional inversion H4;
functional inversion H15;
intomega.
}
assert(0 ≤ rep ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H16; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 5) with 32.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ str ≤ Int.max_unsigned).
{
functional inversion H6; subst.
functional inversion H17; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 4) with 16.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ fault_addr ≤ Int.max_unsigned).
{
functional inversion H7; subst.
functional inversion H18; subst.
repeat discharge_unsigned_range.
}
assert(0 ≤ addr ≤ Int.max_unsigned).
{
functional inversion H8; subst.
functional inversion H19; subst.
repeat discharge_unsigned_range.
}
rewrite <- Int.unsigned_repr in H2 at 1; try omega.
rewrite <- Int.unsigned_repr in H3 at 1; try omega.
rewrite <- Int.unsigned_repr in H4 at 1; try omega.
rewrite <- Int.unsigned_repr in H5 at 1; try omega.
rewrite <- Int.unsigned_repr in H6 at 1; try omega.
rewrite <- Int.unsigned_repr in H7 at 1; try omega.
rewrite <- Int.unsigned_repr in H8 at 1; try omega.
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 48)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
}
{
assert(0 ≤ port ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H14.
repeat discharge_unsigned_range.
}
assert(0 ≤ width ≤ 3).
{
functional inversion H3;
functional inversion H15;
intomega.
}
assert(0 ≤ write ≤ 1).
{
functional inversion H4;
functional inversion H16;
intomega.
}
assert(0 ≤ rep ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H17; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 5) with 32.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ str ≤ Int.max_unsigned).
{
functional inversion H6; subst.
functional inversion H18; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 4) with 16.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ fault_addr ≤ Int.max_unsigned).
{
functional inversion H7; subst.
functional inversion H19; subst.
repeat discharge_unsigned_range.
}
assert(0 ≤ addr ≤ Int.max_unsigned).
{
functional inversion H8; subst.
functional inversion H20; subst.
repeat discharge_unsigned_range.
}
rewrite <- Int.unsigned_repr in H2 at 1; try omega.
rewrite <- Int.unsigned_repr in H3 at 1; try omega.
rewrite <- Int.unsigned_repr in H4 at 1; try omega.
rewrite <- Int.unsigned_repr in H5 at 1; try omega.
rewrite <- Int.unsigned_repr in H6 at 1; try omega.
rewrite <- Int.unsigned_repr in H7 at 1; try omega.
rewrite <- Int.unsigned_repr in H8 at 1; try omega.
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
instantiate (1:= (Int.repr 28)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat vcgen.
repeat vcgen.
}
{
assert(0 ≤ reason ≤ Int.max_unsigned).
{
functional inversion H1; subst.
functional inversion H13; subst.
apply Z_land_range.
repeat discharge_unsigned_range.
omega.
}
assert(0 ≤ port ≤ Int.max_unsigned).
{
functional inversion H2.
functional inversion H14.
repeat discharge_unsigned_range.
}
assert(0 ≤ width ≤ Int.max_unsigned).
{
functional inversion H3;
functional inversion H15;
intomega.
}
assert(0 ≤ write ≤ Int.max_unsigned).
{
functional inversion H4;
functional inversion H16;
intomega.
}
assert(0 ≤ rep ≤ Int.max_unsigned).
{
functional inversion H5; subst.
functional inversion H17; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 5) with 32.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ str ≤ Int.max_unsigned).
{
functional inversion H6; subst.
functional inversion H18; subst.
apply Z_land_range.
split.
apply Z.shiftr_nonneg.
discharge_unsigned_range.
rewrite Z.shiftr_div_pow2.
change (2 ^ 4) with 16.
generalize (Int.unsigned_range_2 v); intro.
xomega.
omega.
omega.
}
assert(0 ≤ fault_addr ≤ Int.max_unsigned).
{
functional inversion H7; subst.
functional inversion H19; subst.
repeat discharge_unsigned_range.
}
assert(0 ≤ addr ≤ Int.max_unsigned).
{
functional inversion H8; subst.
functional inversion H20; subst.
repeat discharge_unsigned_range.
}
rewrite <- Int.unsigned_repr in H1 at 1; try omega.
rewrite <- Int.unsigned_repr in H2 at 1; try omega.
rewrite <- Int.unsigned_repr in H3 at 1; try omega.
rewrite <- Int.unsigned_repr in H4 at 1; try omega.
rewrite <- Int.unsigned_repr in H5 at 1; try omega.
rewrite <- Int.unsigned_repr in H6 at 1; try omega.
rewrite <- Int.unsigned_repr in H7 at 1; try omega.
rewrite <- Int.unsigned_repr in H8 at 1; try omega.
unfold sys_get_exitinfo_body.
esplit.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
}
Qed.
End SysGetExitinfoBody.
Theorem sys_get_exitinfo_body_code_correct:
spec_le
(sys_get_exitinfo ↦ trap_get_exitinfo_spec_low)
(〚sys_get_exitinfo ↦ f_sys_get_exitinfo 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_get_exitinfo_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
b5 Hb5fs Hb5fp
b6 Hb6fs Hb6fp
b7 Hb7fs Hb7fp
b8 Hb8fs Hb8fp
b9 Hb9fs Hb9fp
b10 Hb10fs Hb10fp
b11 Hb11fs Hb11fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_get_exitinfo)
nil
(create_undef_temps (fn_temps f_sys_get_exitinfo)))) H.
Qed.
End SYSGETEXITINFO.
End WithPrimitives.
End TTRAPARGCODE.