Library mcertikos.devdrivers.DSerialCode_ioapic_init
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 ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
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 Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import FutureTactic.
Require Import List.
Require Import AbstractDataType.
Require Import IoApicGenSpec.
Require Import ObjInterruptDriver.
Require Import DSerial.
Require Import DeviceStateDataType.
Require Import INVLemmaDriver.
Require Import DSerialCSource.
Module DSERIALCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
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}.
Local Open Scope Z_scope.
Section IOAPICINIT.
Let L: compatlayer (cdata RData) :=
ioapic_read ↦ gensem ioapic_read_spec
⊕ ioapic_write ↦ gensem ioapic_write_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section IoApicInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bioapic_read: block).
Hypothesis hioapic_read1 : Genv.find_symbol ge ioapic_read = Some bioapic_read.
Hypothesis hioapic_read2 : Genv.find_funct_ptr ge bioapic_read =
Some (External (EF_external ioapic_read
(signature_of_type (Tcons tuint Tnil)
tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (bioapic_write: block).
Hypothesis hioapic_write1 : Genv.find_symbol ge ioapic_write = Some bioapic_write.
Hypothesis hioapic_write2 : Genv.find_funct_ptr ge bioapic_write =
Some (External (EF_external ioapic_write
(signature_of_type (Tcons tuint (Tcons tuint Tnil))
tvoid
cc_default))
(Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).
Ltac unfold_data :=
unfold update_ioapic; unfold update_s; simpl; unfold_IoApicState.
Ltac unfold_read_spec :=
unfold ioapic_read_spec;
unfold ioapic_valid_read_range; simpl;
unfold ioapic_read_1; simpl.
Ltac unfold_write_spec :=
unfold ioapic_write_spec;
unfold ioapic_valid_write_range; simpl;
unfold low32_to_irq; simpl;
unfold low32_to_enable; simpl.
Section ioapic_init_loop_proof.
Variable m_init: memb.
Variable abd: RData.
Notation n := (IoApicMaxIntr (s (ioapic abd))).
Notation irqs := (IoApicIrqs (s (ioapic abd))).
Notation enables := (IoApicEnables (s (ioapic abd))).
Hypothesis Hnrange: 0 ≤ n < 32.
Hypothesis Hirqlen: Zlength irqs = n + 1.
Hypothesis Henblen: Zlength enables = n + 1.
Hypothesis Hinv: high_level_invariant abd.
Hypothesis Hkern: ikern abd = true.
Hypothesis Hhost: ihost abd = true.
Definition ioapic_init_loop_body_P (le: temp_env) (m: mem): Prop :=
le ! _maxintr = Some (Vint (Int.repr n)) ∧
le ! _j = Some (Vint (Int.zero)) ∧
m = (m_init, abd).
Function d_mid (j: Z) :=
if zeq j 0 then abd
else
(abd {ioapic / s: ioapic_init_aux (s (ioapic abd)) (Z.to_nat (j - 1))}).
Definition ioapic_init_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (m_init, d_mid (n + 1)).
Lemma ioapic_trans_step:
∀ j,
0 ≤ j ≤ (n - 1) →
ioapic_trans_cpu (OpOutput (16 + 2 × (j + 1) + 1) 0)
(ioapic_trans_cpu (OpOutput (16 + 2 × (j + 1)) (65536 + 32 + (j + 1)))
(ioapic_init_aux (s (ioapic abd)) (Z.to_nat j)))
= (ioapic_init_aux (s (ioapic abd)) (Z.to_nat (j + 1))).
Proof.
intros. remember (s (ioapic abd)) as d.
replace (16 + 2 × (j + 1)) with (2 × j + 18) by omega.
remember (Z.to_nat j) as nj.
assert (HeqSnj: Z.to_nat (j + 1) = S nj).
{
repeat toNat. rewrite Heqnj. reflexivity.
}
assert (Heven: (2 × j + 18) mod 2 = 0).
{
replace (2 × j + 18) with ((j + 9) × 2) by omega.
rewrite Z_even_mod. trivial.
}
assert (Hodd: (2 × j + 18 + 1) mod 2 = 1).
{
rewrite Z.add_mod. rewrite Heven. calc. reflexivity.
omega.
}
assert (Hirq: (65536 + 32 + j + 1) mod 256 = j + 33).
{
replace (65536 + 32 + j + 1) with (65536 + (32 + j + 1)) by omega.
rewrite Z.add_mod. replace (65536 mod 256) with 0. calc. reflexivity.
vm_compute. reflexivity. omega.
}
assert (Honce: (((65536 + 32 + j + 1) / 65536) mod 2 =? 0) = false).
{
replace (65536 + 32 + j + 1) with (1 × 65536 + (33 + j)) by omega.
rewrite Z.div_add_l. rewrite Z.div_small. calc. reflexivity.
omega. omega.
}
assert (Hsj: 32 + Z.of_nat (S nj) = j + 33).
{
rewrite Heqnj. toZ. omega. omega.
}
rewrite HeqSnj.
Opaque Z.add Z.mul.
pose proof (init_does_not_change_max_intr nj d) as Hmaxinv.
remember (ioapic_init_aux d nj) as d´.
remember (ioapic_init_aux d (S nj)) as d´´.
unfold ioapic_trans_cpu at 2.
unfold_data.
destruct d´; simpl.
if_false.
case_cmp_step.
- unfold addr_to_idx. rewrite Heven. if_true.
unfold ioapic_trans_cpu.
if_false.
case_cmp_step.
+ unfold addr_to_idx. rewrite Hodd. if_false.
rewrite Heqd´´. rewrite <- disable_irq_init_step. rewrite <- Heqd´.
unfold disable_irq. rewrite Hsj.
simpl. unfold_data. calc. rewrite HeqSnj.
f_equal. f_equal.
unfold low32_to_irq. rewrite Hirq. reflexivity.
f_equal.
unfold low32_to_enable. rewrite Honce. reflexivity.
omega.
+ rewrite Heqd´´. rewrite <- disable_irq_init_step. rewrite <- Heqd´.
unfold disable_irq. rewrite Hsj.
simpl. calc. rewrite HeqSnj. unfold_data.
f_equal. f_equal.
unfold low32_to_irq. rewrite Hirq. reflexivity.
f_equal.
unfold low32_to_enable. rewrite Honce. reflexivity.
omega.
- destruct o. omega.
assert (2 × j > IoApicMaxIntr × 2 - 1) by omega.
assert ((DeviceStateDataType.IoApicMaxIntr d) = IoApicMaxIntr).
{
rewrite <- Hmaxinv. simpl. reflexivity.
}
rewrite H2 in H. omega.
Qed.
Ltac rewrite_intr := rewrite init_does_not_change_max_intr; simpl; omega.
Lemma ioapic_init_loop_correct_aux:
LoopProofSimpleWhile.t
ioapic_init_loop_condition
ioapic_init_loop_body
ge (PTree.empty _)
ioapic_init_loop_body_P
ioapic_init_loop_body_Q.
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ j,
le ! _maxintr = Some (Vint (Int.repr n)) ∧
le ! _j = Some (Vint (Int.repr j)) ∧
w = n + 1 - j ∧
0 ≤ j ≤ n + 1 ∧
m = (m_init, d_mid j)
).
apply Zwf_well_founded.
intros le m Hp.
destruct Hp as (Hlemax & Hlej & Hm).
∃ (n + 1), (0).
repeat constructor; discharge_cmp.
unfold ioapic_init_loop_body_Q. unfold d_mid.
unfold_data.
intros le m w Hi.
Locate ioapic_trans_step.
destruct Hi as (j & Hlemax & Hlej & Hw & Hjrange & Hm).
pose proof (@ioapic_trans_step (j - 1)) as Htrans.
replace (j - 1 + 1) with j in Htrans by omega.
Opaque Z.add Z.mul.
destruct abd; destruct ioapic; destruct s; simpl in ×.
Transparent Z.add Z.mul.
assert (Hcase: j = 0 ∨ 0 < j < IoApicMaxIntr + 1 ∨ j = IoApicMaxIntr + 1) by omega.
destruct Hcase as [Hcase | [Hcase | Hcase]];
subst; simpl.
- Case ("first iteration").
esplit. esplit.
split; [| split; [| split]].
+ SCase ("loop condition").
unfold ioapic_init_loop_condition.
repeat vcgen.
+ SCase ("bool val = true").
simpl. discharge_cmp.
+ SCase ("not done").
inversion 1.
+ SCase ("will continue").
intros H; clear H.
esplit. esplit.
split.
× unfold ioapic_init_loop_body. repeat vcgen.
unfold_write_spec. unfold_data. repeat if_true; reflexivity.
unfold_write_spec. unfold_data. repeat if_true; reflexivity.
× ∃ (IoApicMaxIntr).
split. omega.
∃ (1).
split. repeat vcgen.
split. repeat vcgen.
split. omega.
split. omega.
if_false. calc. f_equal.
- Case ("loop").
assert (Htransp: 0 ≤ j - 1 ≤ IoApicMaxIntr - 1) by omega.
generalize (Htrans Htransp). clear Htrans Htransp. intros Htrans.
esplit. esplit.
split; [| split; [| split]].
+ SCase ("loop condition").
unfold ioapic_init_loop_condition.
repeat vcgen.
+ SCase ("bool val = true").
simpl. discharge_cmp.
+ SCase ("not done").
inversion 1.
+ SCase ("will continue").
intros H; clear H.
esplit. esplit.
split.
× if_false.
Opaque Z.add Z.mul.
unfold ioapic_init_loop_body.
repeat vcgen.
unfold_write_spec. unfold_data. if_false. if_true. reflexivity.
rewrite_intr.
unfold_write_spec. unfold_data. if_false. if_true. replace (-1 + j) with (j - 1) by omega.
rewrite Htrans.
reflexivity.
rewrite ioapic_trans_cpu_does_not_change_maxintr. rewrite_intr.
× ∃ (IoApicMaxIntr - j).
split. omega.
∃ (j + 1).
split. repeat vcgen.
split. repeat vcgen.
split. omega.
split. omega.
if_false.
calc. f_equal.
- Case ("break").
esplit. esplit.
split; [| split; [| split]].
+ SCase ("loop condition").
unfold ioapic_init_loop_condition.
repeat vcgen.
+ SCase ("bool val = false").
simpl. discharge_cmp.
+ SCase ("done").
intros H; clear H.
if_false. reflexivity.
+ SCase ("will break").
inversion 1.
Qed.
End ioapic_init_loop_proof.
Section ioapic_init_loop_correct_proof.
Variable m: memb.
Variable d: RData.
Variable le: temp_env.
Notation n := (IoApicMaxIntr (s (ioapic d))).
Notation irqs := (IoApicIrqs (s (ioapic d))).
Notation enables := (IoApicEnables (s (ioapic d))).
Hypothesis Hnrange: 0 ≤ n < 32.
Hypothesis Hirqlen: Zlength irqs = n + 1.
Hypothesis Henblen: Zlength enables = n + 1.
Hypothesis Hinv: high_level_invariant d.
Hypothesis Hkern: ikern d = true.
Hypothesis Hhost: ihost d = true.
Hypothesis Hlemax: le ! _maxintr = Some (Vint (Int.repr n)).
Hypothesis Hlej: le ! _j = Some (Vint (Int.zero)).
Lemma ioapic_init_loop_correct:
∃ le´, exec_stmt ge (PTree.empty _) le ((m, d): mem)
(Swhile ioapic_init_loop_condition ioapic_init_loop_body)
E0 le´ (m, (d_mid d (n + 1))) Out_normal.
Proof.
generalize (ioapic_init_loop_correct_aux m d Hnrange Hirqlen Henblen Hinv Hkern Hhost).
unfold ioapic_init_loop_body_P, ioapic_init_loop_body_Q.
intro Hlp.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ Hlp le (m, d) _)).
intro pre.
destruct pre as (le´ & m´ & Hexec & Hd_end).
∃ le´. subst. assumption.
repeat split; try assumption.
Qed.
End ioapic_init_loop_correct_proof.
Lemma ioapic_init_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
ioapic_init_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) ioapic_init_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hinv Hspec.
inversion Hinv.
functional inversion Hspec; subst; clear Hspec.
destruct d; destruct ioapic; subst; simpl in ×.
unfold_data.
destruct s; simpl in ×.
remember ({|
MM := MM;
MMSize := MMSize;
vmxinfo := vmxinfo;
CR3 := CR3;
ti := ti;
pg := pg;
ikern := ikern;
ihost := ihost;
HP := HP;
AC := AC;
AT := AT;
nps := nps;
init := init;
pperm := pperm;
PT := PT;
ptpool := ptpool;
idpde := idpde;
ipt := ipt;
LAT := LAT;
smspool := smspool;
kctxt := kctxt;
tcb := tcb;
tdq := tdq;
abtcb := abtcb;
abq := abq;
cid := cid;
syncchpool := syncchpool;
uctxt := uctxt;
ept := ept;
vmcs := vmcs;
vmx := vmx;
ts := ts;
com1 := com1;
drv_serial := drv_serial;
console_concrete := console_concrete;
console := console;
ioapic := {|
s := {|
CurrentIrq := CurrentIrq;
IoApicBase := IoApicBase;
IoApicId := IoApicId;
IoApicMaxIntr := IoApicMaxIntr;
IoApicIrqs := IoApicIrqs;
IoApicEnables := IoApicEnables |};
l1 := l1;
l2 := l2;
l3 := l3 |};
lapic := lapic;
tf := tf;
curr_intr_num := curr_intr_num;
intr_flag := intr_flag |}) as d1.
remember (PTree.set _j (Vint (Int.repr 0))
(PTree.set _maxintr (Vint (Int.repr IoApicMaxIntr))
(PTree.set 39
(Vint (Int.repr (IoApicMaxIntr × 65536))) le)))
as le1.
exploit (ioapic_init_loop_correct m d1 le1);
try rewrite Heqd1; try rewrite Heqle1; simpl;
try repeat vcgen.
inversion Hinv; constructor; eauto.
destruct H as (le_after_loop & Hloopexec).
generalize Hloopexec; clear Hloopexec.
unfold d_mid; unfold_data; simpl. calc.
if_false.
rewrite <- Heqd1. rewrite <- Heqle1. unfold update_s; simpl. calc.
intros Hloopexec.
unfold ioapic_init_body.
esplit. repeat vcgen.
unfold_read_spec. rewrite Heqd1; simpl. rewrite <- Heqd1.
rewrite Int.unsigned_repr. reflexivity. omega.
replace (Int.modu (Int.divu (Int.repr (IoApicMaxIntr × 65536))
(Int.repr 65536))
(Int.repr (255 + 1))) with (Int.repr IoApicMaxIntr).
replace (set_opttemp (Some 39%positive)
(Vint (Int.repr (IoApicMaxIntr × 65536))) le) with
(PTree.set 39 (Vint (Int.repr (IoApicMaxIntr × 65536))) le).
rewrite <- Heqle1.
eapply Hloopexec.
discharge_cmp.
{
repeat vcgen. f_equal. rewrite Z_div_mult. rewrite Z.mod_small. reflexivity.
omega. omega.
}
Qed.
End IoApicInitBody.
Theorem ioapic_init_code_correct:
spec_le
(ioapic_init ↦ ioapic_init_spec_low)
(〚ioapic_init ↦ f_ioapic_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(ioapic_init_body_correct
s
(Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ioapic_init) (nil)
(create_undef_temps (fn_temps f_ioapic_init))
)
) H0.
Qed.
End IOAPICINIT.
End WithPrimitives.
End DSERIALCODE.
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 ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
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 Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import FutureTactic.
Require Import List.
Require Import AbstractDataType.
Require Import IoApicGenSpec.
Require Import ObjInterruptDriver.
Require Import DSerial.
Require Import DeviceStateDataType.
Require Import INVLemmaDriver.
Require Import DSerialCSource.
Module DSERIALCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
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}.
Local Open Scope Z_scope.
Section IOAPICINIT.
Let L: compatlayer (cdata RData) :=
ioapic_read ↦ gensem ioapic_read_spec
⊕ ioapic_write ↦ gensem ioapic_write_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section IoApicInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bioapic_read: block).
Hypothesis hioapic_read1 : Genv.find_symbol ge ioapic_read = Some bioapic_read.
Hypothesis hioapic_read2 : Genv.find_funct_ptr ge bioapic_read =
Some (External (EF_external ioapic_read
(signature_of_type (Tcons tuint Tnil)
tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (bioapic_write: block).
Hypothesis hioapic_write1 : Genv.find_symbol ge ioapic_write = Some bioapic_write.
Hypothesis hioapic_write2 : Genv.find_funct_ptr ge bioapic_write =
Some (External (EF_external ioapic_write
(signature_of_type (Tcons tuint (Tcons tuint Tnil))
tvoid
cc_default))
(Tcons tuint (Tcons tuint Tnil)) tvoid cc_default).
Ltac unfold_data :=
unfold update_ioapic; unfold update_s; simpl; unfold_IoApicState.
Ltac unfold_read_spec :=
unfold ioapic_read_spec;
unfold ioapic_valid_read_range; simpl;
unfold ioapic_read_1; simpl.
Ltac unfold_write_spec :=
unfold ioapic_write_spec;
unfold ioapic_valid_write_range; simpl;
unfold low32_to_irq; simpl;
unfold low32_to_enable; simpl.
Section ioapic_init_loop_proof.
Variable m_init: memb.
Variable abd: RData.
Notation n := (IoApicMaxIntr (s (ioapic abd))).
Notation irqs := (IoApicIrqs (s (ioapic abd))).
Notation enables := (IoApicEnables (s (ioapic abd))).
Hypothesis Hnrange: 0 ≤ n < 32.
Hypothesis Hirqlen: Zlength irqs = n + 1.
Hypothesis Henblen: Zlength enables = n + 1.
Hypothesis Hinv: high_level_invariant abd.
Hypothesis Hkern: ikern abd = true.
Hypothesis Hhost: ihost abd = true.
Definition ioapic_init_loop_body_P (le: temp_env) (m: mem): Prop :=
le ! _maxintr = Some (Vint (Int.repr n)) ∧
le ! _j = Some (Vint (Int.zero)) ∧
m = (m_init, abd).
Function d_mid (j: Z) :=
if zeq j 0 then abd
else
(abd {ioapic / s: ioapic_init_aux (s (ioapic abd)) (Z.to_nat (j - 1))}).
Definition ioapic_init_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (m_init, d_mid (n + 1)).
Lemma ioapic_trans_step:
∀ j,
0 ≤ j ≤ (n - 1) →
ioapic_trans_cpu (OpOutput (16 + 2 × (j + 1) + 1) 0)
(ioapic_trans_cpu (OpOutput (16 + 2 × (j + 1)) (65536 + 32 + (j + 1)))
(ioapic_init_aux (s (ioapic abd)) (Z.to_nat j)))
= (ioapic_init_aux (s (ioapic abd)) (Z.to_nat (j + 1))).
Proof.
intros. remember (s (ioapic abd)) as d.
replace (16 + 2 × (j + 1)) with (2 × j + 18) by omega.
remember (Z.to_nat j) as nj.
assert (HeqSnj: Z.to_nat (j + 1) = S nj).
{
repeat toNat. rewrite Heqnj. reflexivity.
}
assert (Heven: (2 × j + 18) mod 2 = 0).
{
replace (2 × j + 18) with ((j + 9) × 2) by omega.
rewrite Z_even_mod. trivial.
}
assert (Hodd: (2 × j + 18 + 1) mod 2 = 1).
{
rewrite Z.add_mod. rewrite Heven. calc. reflexivity.
omega.
}
assert (Hirq: (65536 + 32 + j + 1) mod 256 = j + 33).
{
replace (65536 + 32 + j + 1) with (65536 + (32 + j + 1)) by omega.
rewrite Z.add_mod. replace (65536 mod 256) with 0. calc. reflexivity.
vm_compute. reflexivity. omega.
}
assert (Honce: (((65536 + 32 + j + 1) / 65536) mod 2 =? 0) = false).
{
replace (65536 + 32 + j + 1) with (1 × 65536 + (33 + j)) by omega.
rewrite Z.div_add_l. rewrite Z.div_small. calc. reflexivity.
omega. omega.
}
assert (Hsj: 32 + Z.of_nat (S nj) = j + 33).
{
rewrite Heqnj. toZ. omega. omega.
}
rewrite HeqSnj.
Opaque Z.add Z.mul.
pose proof (init_does_not_change_max_intr nj d) as Hmaxinv.
remember (ioapic_init_aux d nj) as d´.
remember (ioapic_init_aux d (S nj)) as d´´.
unfold ioapic_trans_cpu at 2.
unfold_data.
destruct d´; simpl.
if_false.
case_cmp_step.
- unfold addr_to_idx. rewrite Heven. if_true.
unfold ioapic_trans_cpu.
if_false.
case_cmp_step.
+ unfold addr_to_idx. rewrite Hodd. if_false.
rewrite Heqd´´. rewrite <- disable_irq_init_step. rewrite <- Heqd´.
unfold disable_irq. rewrite Hsj.
simpl. unfold_data. calc. rewrite HeqSnj.
f_equal. f_equal.
unfold low32_to_irq. rewrite Hirq. reflexivity.
f_equal.
unfold low32_to_enable. rewrite Honce. reflexivity.
omega.
+ rewrite Heqd´´. rewrite <- disable_irq_init_step. rewrite <- Heqd´.
unfold disable_irq. rewrite Hsj.
simpl. calc. rewrite HeqSnj. unfold_data.
f_equal. f_equal.
unfold low32_to_irq. rewrite Hirq. reflexivity.
f_equal.
unfold low32_to_enable. rewrite Honce. reflexivity.
omega.
- destruct o. omega.
assert (2 × j > IoApicMaxIntr × 2 - 1) by omega.
assert ((DeviceStateDataType.IoApicMaxIntr d) = IoApicMaxIntr).
{
rewrite <- Hmaxinv. simpl. reflexivity.
}
rewrite H2 in H. omega.
Qed.
Ltac rewrite_intr := rewrite init_does_not_change_max_intr; simpl; omega.
Lemma ioapic_init_loop_correct_aux:
LoopProofSimpleWhile.t
ioapic_init_loop_condition
ioapic_init_loop_body
ge (PTree.empty _)
ioapic_init_loop_body_P
ioapic_init_loop_body_Q.
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ j,
le ! _maxintr = Some (Vint (Int.repr n)) ∧
le ! _j = Some (Vint (Int.repr j)) ∧
w = n + 1 - j ∧
0 ≤ j ≤ n + 1 ∧
m = (m_init, d_mid j)
).
apply Zwf_well_founded.
intros le m Hp.
destruct Hp as (Hlemax & Hlej & Hm).
∃ (n + 1), (0).
repeat constructor; discharge_cmp.
unfold ioapic_init_loop_body_Q. unfold d_mid.
unfold_data.
intros le m w Hi.
Locate ioapic_trans_step.
destruct Hi as (j & Hlemax & Hlej & Hw & Hjrange & Hm).
pose proof (@ioapic_trans_step (j - 1)) as Htrans.
replace (j - 1 + 1) with j in Htrans by omega.
Opaque Z.add Z.mul.
destruct abd; destruct ioapic; destruct s; simpl in ×.
Transparent Z.add Z.mul.
assert (Hcase: j = 0 ∨ 0 < j < IoApicMaxIntr + 1 ∨ j = IoApicMaxIntr + 1) by omega.
destruct Hcase as [Hcase | [Hcase | Hcase]];
subst; simpl.
- Case ("first iteration").
esplit. esplit.
split; [| split; [| split]].
+ SCase ("loop condition").
unfold ioapic_init_loop_condition.
repeat vcgen.
+ SCase ("bool val = true").
simpl. discharge_cmp.
+ SCase ("not done").
inversion 1.
+ SCase ("will continue").
intros H; clear H.
esplit. esplit.
split.
× unfold ioapic_init_loop_body. repeat vcgen.
unfold_write_spec. unfold_data. repeat if_true; reflexivity.
unfold_write_spec. unfold_data. repeat if_true; reflexivity.
× ∃ (IoApicMaxIntr).
split. omega.
∃ (1).
split. repeat vcgen.
split. repeat vcgen.
split. omega.
split. omega.
if_false. calc. f_equal.
- Case ("loop").
assert (Htransp: 0 ≤ j - 1 ≤ IoApicMaxIntr - 1) by omega.
generalize (Htrans Htransp). clear Htrans Htransp. intros Htrans.
esplit. esplit.
split; [| split; [| split]].
+ SCase ("loop condition").
unfold ioapic_init_loop_condition.
repeat vcgen.
+ SCase ("bool val = true").
simpl. discharge_cmp.
+ SCase ("not done").
inversion 1.
+ SCase ("will continue").
intros H; clear H.
esplit. esplit.
split.
× if_false.
Opaque Z.add Z.mul.
unfold ioapic_init_loop_body.
repeat vcgen.
unfold_write_spec. unfold_data. if_false. if_true. reflexivity.
rewrite_intr.
unfold_write_spec. unfold_data. if_false. if_true. replace (-1 + j) with (j - 1) by omega.
rewrite Htrans.
reflexivity.
rewrite ioapic_trans_cpu_does_not_change_maxintr. rewrite_intr.
× ∃ (IoApicMaxIntr - j).
split. omega.
∃ (j + 1).
split. repeat vcgen.
split. repeat vcgen.
split. omega.
split. omega.
if_false.
calc. f_equal.
- Case ("break").
esplit. esplit.
split; [| split; [| split]].
+ SCase ("loop condition").
unfold ioapic_init_loop_condition.
repeat vcgen.
+ SCase ("bool val = false").
simpl. discharge_cmp.
+ SCase ("done").
intros H; clear H.
if_false. reflexivity.
+ SCase ("will break").
inversion 1.
Qed.
End ioapic_init_loop_proof.
Section ioapic_init_loop_correct_proof.
Variable m: memb.
Variable d: RData.
Variable le: temp_env.
Notation n := (IoApicMaxIntr (s (ioapic d))).
Notation irqs := (IoApicIrqs (s (ioapic d))).
Notation enables := (IoApicEnables (s (ioapic d))).
Hypothesis Hnrange: 0 ≤ n < 32.
Hypothesis Hirqlen: Zlength irqs = n + 1.
Hypothesis Henblen: Zlength enables = n + 1.
Hypothesis Hinv: high_level_invariant d.
Hypothesis Hkern: ikern d = true.
Hypothesis Hhost: ihost d = true.
Hypothesis Hlemax: le ! _maxintr = Some (Vint (Int.repr n)).
Hypothesis Hlej: le ! _j = Some (Vint (Int.zero)).
Lemma ioapic_init_loop_correct:
∃ le´, exec_stmt ge (PTree.empty _) le ((m, d): mem)
(Swhile ioapic_init_loop_condition ioapic_init_loop_body)
E0 le´ (m, (d_mid d (n + 1))) Out_normal.
Proof.
generalize (ioapic_init_loop_correct_aux m d Hnrange Hirqlen Henblen Hinv Hkern Hhost).
unfold ioapic_init_loop_body_P, ioapic_init_loop_body_Q.
intro Hlp.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ Hlp le (m, d) _)).
intro pre.
destruct pre as (le´ & m´ & Hexec & Hd_end).
∃ le´. subst. assumption.
repeat split; try assumption.
Qed.
End ioapic_init_loop_correct_proof.
Lemma ioapic_init_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
ioapic_init_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) ioapic_init_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hinv Hspec.
inversion Hinv.
functional inversion Hspec; subst; clear Hspec.
destruct d; destruct ioapic; subst; simpl in ×.
unfold_data.
destruct s; simpl in ×.
remember ({|
MM := MM;
MMSize := MMSize;
vmxinfo := vmxinfo;
CR3 := CR3;
ti := ti;
pg := pg;
ikern := ikern;
ihost := ihost;
HP := HP;
AC := AC;
AT := AT;
nps := nps;
init := init;
pperm := pperm;
PT := PT;
ptpool := ptpool;
idpde := idpde;
ipt := ipt;
LAT := LAT;
smspool := smspool;
kctxt := kctxt;
tcb := tcb;
tdq := tdq;
abtcb := abtcb;
abq := abq;
cid := cid;
syncchpool := syncchpool;
uctxt := uctxt;
ept := ept;
vmcs := vmcs;
vmx := vmx;
ts := ts;
com1 := com1;
drv_serial := drv_serial;
console_concrete := console_concrete;
console := console;
ioapic := {|
s := {|
CurrentIrq := CurrentIrq;
IoApicBase := IoApicBase;
IoApicId := IoApicId;
IoApicMaxIntr := IoApicMaxIntr;
IoApicIrqs := IoApicIrqs;
IoApicEnables := IoApicEnables |};
l1 := l1;
l2 := l2;
l3 := l3 |};
lapic := lapic;
tf := tf;
curr_intr_num := curr_intr_num;
intr_flag := intr_flag |}) as d1.
remember (PTree.set _j (Vint (Int.repr 0))
(PTree.set _maxintr (Vint (Int.repr IoApicMaxIntr))
(PTree.set 39
(Vint (Int.repr (IoApicMaxIntr × 65536))) le)))
as le1.
exploit (ioapic_init_loop_correct m d1 le1);
try rewrite Heqd1; try rewrite Heqle1; simpl;
try repeat vcgen.
inversion Hinv; constructor; eauto.
destruct H as (le_after_loop & Hloopexec).
generalize Hloopexec; clear Hloopexec.
unfold d_mid; unfold_data; simpl. calc.
if_false.
rewrite <- Heqd1. rewrite <- Heqle1. unfold update_s; simpl. calc.
intros Hloopexec.
unfold ioapic_init_body.
esplit. repeat vcgen.
unfold_read_spec. rewrite Heqd1; simpl. rewrite <- Heqd1.
rewrite Int.unsigned_repr. reflexivity. omega.
replace (Int.modu (Int.divu (Int.repr (IoApicMaxIntr × 65536))
(Int.repr 65536))
(Int.repr (255 + 1))) with (Int.repr IoApicMaxIntr).
replace (set_opttemp (Some 39%positive)
(Vint (Int.repr (IoApicMaxIntr × 65536))) le) with
(PTree.set 39 (Vint (Int.repr (IoApicMaxIntr × 65536))) le).
rewrite <- Heqle1.
eapply Hloopexec.
discharge_cmp.
{
repeat vcgen. f_equal. rewrite Z_div_mult. rewrite Z.mod_small. reflexivity.
omega. omega.
}
Qed.
End IoApicInitBody.
Theorem ioapic_init_code_correct:
spec_le
(ioapic_init ↦ ioapic_init_spec_low)
(〚ioapic_init ↦ f_ioapic_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(ioapic_init_body_correct
s
(Genv.globalenv p)
makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ioapic_init) (nil)
(create_undef_temps (fn_temps f_ioapic_init))
)
) H0.
Qed.
End IOAPICINIT.
End WithPrimitives.
End DSERIALCODE.