Library mcertikos.devdrivers.DHandlerCxtCode_serial_intr_enable
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 AbstractDataType.
Require Import HandlerOpGenSpec.
Require Import ObjInterruptController.
Require Import ObjConsole.
Require Import FutureTactic.
Require Import INVLemmaDriver.
Require Import ObjInterruptManagement.
Require Import CommonTactic.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import DHandlerCxt.
Require Import FutureTactic.
Require Import DHandlerCxtCSource.
Require Import ObjInterruptController.
Module DHANDLERCXTCODE.
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 SERIAL_INTR_ENABLE_HANDLER.
Let L: compatlayer (cdata RData) := ic_intr ↦ gensem ic_intr_spec
⊕ serial_intr_handler_asm ↦ gensem serial_intr_handler_sw_spec
⊕ iret ↦ gensem iret_spec
⊕ serial_irq_current ↦ gensem serial_irq_current_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 Serial_Intr_Enable_Body.
Notation MAX := 100%Z.
Lemma MAX_eq_INTR_DISABLE_REC_MAX:
MAX = Z.of_nat INTR_DISABLE_REC_MAX. simpl. reflexivity. Qed.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bic_intr: block).
Hypothesis hic_intr1 : Genv.find_symbol ge ic_intr = Some bic_intr.
Hypothesis hic_intr2 : Genv.find_funct_ptr ge bic_intr =
Some (External (EF_external ic_intr
(signature_of_type (Tcons tuint Tnil) tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (bserial_intr_handler_asm: block).
Hypothesis hserial_intr_handler_asm1 : Genv.find_symbol ge serial_intr_handler_asm = Some bserial_intr_handler_asm.
Hypothesis hserial_intr_handler_asm2 : Genv.find_funct_ptr ge bserial_intr_handler_asm =
Some (External (EF_external serial_intr_handler_asm
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (biret: block).
Hypothesis hiret1 : Genv.find_symbol ge iret = Some biret.
Hypothesis hiret2 : Genv.find_funct_ptr ge biret =
Some (External (EF_external iret
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (bserial_irq_current: block).
Hypothesis hserial_irq_current1 : Genv.find_symbol ge serial_irq_current = Some bserial_irq_current.
Hypothesis hserial_irq_current2 : Genv.find_funct_ptr ge bserial_irq_current =
Some (External (EF_external serial_irq_current
(signature_of_type Tnil tuint
cc_default))
Tnil tuint cc_default).
Require Import ObjInterruptDriver.
Lemma cons_intr_spec_subset:
∀ d d´ r,
lapic_eoi_spec d = Some r →
cons_intr_aux r = Some d´ →
cons_intr_spec d = Some d´.
Proof.
intros.
unfold cons_intr_spec. rewrite H, H0.
functional inversion H. rewrite H4, H3, H5, H2.
reflexivity.
Qed.
Lemma serial_irq_current_range:
∀ d x,
serial_irq_current_spec d = x →
x = 0 ∨ x = 1.
Proof.
intros.
unfold serial_irq_current_spec in H.
destruct (SerialIrq (s (com1 d))); subst.
- right. reflexivity.
- left . reflexivity.
Qed.
Lemma serial_irq_current_range_rewrite:
∀ d,
serial_irq_current_spec d = 0 ∨ serial_irq_current_spec d = 1.
Proof.
intros.
specialize (serial_irq_current_range d). intros.
destruct (serial_irq_current_spec d) eqn: Hx; try split; auto.
Qed.
Lemma serial_irq_current_bound:
∀ d,
0 ≤ serial_irq_current_spec d ≤ Int.max_unsigned.
Proof.
generalize max_unsigned_val; intro muval.
intros. generalize (serial_irq_current_range_rewrite d).
destruct 1 as [Hw | Hw]; rewrite Hw; omega.
Qed.
Lemma ioapic_trans_intr_preserves_length: ∀ d n,
Zlength (IoApicEnables (ioapic_trans_intr (IRQ n) (s (ioapic d))))
= Zlength (IoApicEnables (s (ioapic d))).
Proof.
intros.
unfold ioapic_trans_intr.
Opaque replace nth_error.
destruct (s (ioapic d)); simpl.
destruct (nth_error IoApicIrqs (Z.to_nat n)).
destruct (nth_error IoApicEnables (Z.to_nat n)).
destruct b;
reflexivity.
reflexivity.
reflexivity.
Qed.
Lemma cons_intr_preserves_iflags:
∀ d d´,
cons_intr_spec d = Some d´ →
init d´ = init d ∧ ikern d´ = ikern d ∧ ihost d´ = ihost d.
Proof.
intros.
functional inversion H; subst.
functional inversion H0; functional inversion H5; simpl in *; subst; eauto.
Qed.
Lemma cons_intr_preserves_length:
∀ d d´,
cons_intr_spec d = Some d´ →
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
intros.
functional inversion H; subst.
functional inversion H0; functional inversion H5; simpl in *; subst; eauto.
Qed.
Lemma intr_flag_eq:
∀ d, intr_flag d = true → d = d {intr_flag: true}.
Proof.
intros.
destruct d.
simpl in ×.
rewrite H.
reflexivity.
Qed.
Lemma ic_intr_spec_not_none:
∀ v d,
ic_intr_spec v d ≠ None.
Proof.
intros.
unfold ic_intr_spec.
destruct (hw_intr_trans v d).
destruct o; try case_if;
intros Hs; inversion Hs.
Qed.
Lemma neq_same:
∀ {A} (a: A),
a ≠ a → False.
Proof.
intros.
apply H. reflexivity.
Qed.
Lemma serial_intr_pending_handler_inv:
∀ d d´ b,
serial_intr_pending_handler d = Some (d´, b) ∧
ikern d = true ∧
ihost d = true ∧
init d = true →
(
(b = true ∧
SerialIrq (s (com1 d)) = true ∧
∃ d0 d1,
ic_intr_spec 4 d = Some (d0, 36) ∧
serial_intr_handler_sw_spec d0 = Some d1 ∧
iret_spec d1 = Some d´
)
∨
(b = false ∧
SerialIrq (s (com1 d)) = false
)
).
Proof.
intros d d´ b.
unfold serial_intr_pending_handler. unfold serial_intr_handler_sw_spec.
intros (H & Hflag). blast Hflag.
subdestruct; subst; inversion H.
- left.
repeat (split; [auto |]). ∃ r. ∃ (r1 { ioapic / s / IoApicEnables [Pos.to_nat 4]:true}).
split; [auto |]. rewrite Hdestruct3. rewrite Hdestruct4.
rewrite H1. split.
{
functional inversion Hdestruct0. functional inversion H4. simpl.
rewrite Hflag0, Hflag2, Hflag3. reflexivity.
}
{
unfold iret_spec. rewrite H1. reflexivity.
}
- right. repeat (split; [auto |]). reflexivity.
Qed.
Lemma ic_intr_spec_cases:
∀ n d d´ v,
init d = true →
0 ≤ n ≤ 23 →
high_level_invariant d →
ic_intr_spec n d = Some (d´, v) →
v = 0 ∨ v = n + IRQ0.
Proof.
Opaque nth_error Z.to_nat.
intros n d d´ v Hinit Hnrange Hinv H. functional inversion H.
- subst. clear H. functional inversion H2; subst. clear H2.
unfold s_ioapic´ in ×. clear s_ioapic´. unfold ioapic_trans_intr in H1.
destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
unfold update_CurrentIrq in H1; simpl in H1.
remember (Z.to_nat n) as nn.
inversion Hinv; simpl in ×.
destruct (nth_error IoApicIrqs nn) eqn: Hirq.
+ generalize (valid_ioapic_state Hinit _ _ Hirq). intros [Hz [b Henable]].
rewrite Henable in H1; simpl in H1. destruct b eqn: Hb; simpl in H1.
× inversion H1. generalize Hz. rewrite Heqnn. rewrite Z2Nat.id. clear Hz. intros Hz. clear Hinv.
subst.
unfold s_lapic´ in ×. clear s_lapic´. unfold lapic_trans_intr in H4.
destruct lapic; simpl in ×. destruct s; simpl in ×.
rewrite Hz in *; simpl in ×. unfold update_LapicEoi in H4; simpl in H4.
subdestruct.
inversion H4.
right. reflexivity.
omega. omega.
× inversion H1.
+ simpl in H1. inversion H1.
- left. reflexivity.
- left. reflexivity.
Qed.
Transparent nth_error Z.to_nat.
Lemma serial_intr_handler_body_correct_irq:
∀ m d d´ env le t b,
ikern d = true →
ihost d = true →
init d = true →
intr_flag d = true →
0 < t ≤ Z.of_nat INTR_ENABLE_REC_MAX →
env = PTree.empty _ →
SerialIrq (s (com1 d)) = true →
serial_intr_pending_handler d = Some (d´, b) →
high_level_invariant d →
le ! _t = Some (Vint (Int.repr t)) →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_enable_handler_loop_body E0 le´ (m, d´) Out_normal ∧
le´ ! _t = Some (Vint (Int.repr (t - 1))) ∧
SerialIrq (s (com1 d´)) = false ∧
le´ ! _has_irq = Some (Vint (Int.repr 0)).
Proof.
generalize max_unsigned_val; intro muval. toZ.
intros m d d´ env le t b Hk Hh Hinit Hintr_flag Htrange Henv Hirq H Hinv Ht.
assert (Hspec: serial_intr_pending_handler d = Some (d´, b) ∧ ikern d = true ∧
ihost d = true ∧ init d = true).
{
repeat (split; [auto|]); auto.
}
generalize (serial_intr_pending_handler_inv _ _ _ Hspec).
intros Hspecinv. destruct Hspecinv as [Hc | Hc]; blast Hc; subst.
-
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 AbstractDataType.
Require Import HandlerOpGenSpec.
Require Import ObjInterruptController.
Require Import ObjConsole.
Require Import FutureTactic.
Require Import INVLemmaDriver.
Require Import ObjInterruptManagement.
Require Import CommonTactic.
Require Import XOmega.
Require Import DeviceStateDataType.
Require Import DHandlerCxt.
Require Import FutureTactic.
Require Import DHandlerCxtCSource.
Require Import ObjInterruptController.
Module DHANDLERCXTCODE.
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 SERIAL_INTR_ENABLE_HANDLER.
Let L: compatlayer (cdata RData) := ic_intr ↦ gensem ic_intr_spec
⊕ serial_intr_handler_asm ↦ gensem serial_intr_handler_sw_spec
⊕ iret ↦ gensem iret_spec
⊕ serial_irq_current ↦ gensem serial_irq_current_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 Serial_Intr_Enable_Body.
Notation MAX := 100%Z.
Lemma MAX_eq_INTR_DISABLE_REC_MAX:
MAX = Z.of_nat INTR_DISABLE_REC_MAX. simpl. reflexivity. Qed.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bic_intr: block).
Hypothesis hic_intr1 : Genv.find_symbol ge ic_intr = Some bic_intr.
Hypothesis hic_intr2 : Genv.find_funct_ptr ge bic_intr =
Some (External (EF_external ic_intr
(signature_of_type (Tcons tuint Tnil) tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (bserial_intr_handler_asm: block).
Hypothesis hserial_intr_handler_asm1 : Genv.find_symbol ge serial_intr_handler_asm = Some bserial_intr_handler_asm.
Hypothesis hserial_intr_handler_asm2 : Genv.find_funct_ptr ge bserial_intr_handler_asm =
Some (External (EF_external serial_intr_handler_asm
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (biret: block).
Hypothesis hiret1 : Genv.find_symbol ge iret = Some biret.
Hypothesis hiret2 : Genv.find_funct_ptr ge biret =
Some (External (EF_external iret
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (bserial_irq_current: block).
Hypothesis hserial_irq_current1 : Genv.find_symbol ge serial_irq_current = Some bserial_irq_current.
Hypothesis hserial_irq_current2 : Genv.find_funct_ptr ge bserial_irq_current =
Some (External (EF_external serial_irq_current
(signature_of_type Tnil tuint
cc_default))
Tnil tuint cc_default).
Require Import ObjInterruptDriver.
Lemma cons_intr_spec_subset:
∀ d d´ r,
lapic_eoi_spec d = Some r →
cons_intr_aux r = Some d´ →
cons_intr_spec d = Some d´.
Proof.
intros.
unfold cons_intr_spec. rewrite H, H0.
functional inversion H. rewrite H4, H3, H5, H2.
reflexivity.
Qed.
Lemma serial_irq_current_range:
∀ d x,
serial_irq_current_spec d = x →
x = 0 ∨ x = 1.
Proof.
intros.
unfold serial_irq_current_spec in H.
destruct (SerialIrq (s (com1 d))); subst.
- right. reflexivity.
- left . reflexivity.
Qed.
Lemma serial_irq_current_range_rewrite:
∀ d,
serial_irq_current_spec d = 0 ∨ serial_irq_current_spec d = 1.
Proof.
intros.
specialize (serial_irq_current_range d). intros.
destruct (serial_irq_current_spec d) eqn: Hx; try split; auto.
Qed.
Lemma serial_irq_current_bound:
∀ d,
0 ≤ serial_irq_current_spec d ≤ Int.max_unsigned.
Proof.
generalize max_unsigned_val; intro muval.
intros. generalize (serial_irq_current_range_rewrite d).
destruct 1 as [Hw | Hw]; rewrite Hw; omega.
Qed.
Lemma ioapic_trans_intr_preserves_length: ∀ d n,
Zlength (IoApicEnables (ioapic_trans_intr (IRQ n) (s (ioapic d))))
= Zlength (IoApicEnables (s (ioapic d))).
Proof.
intros.
unfold ioapic_trans_intr.
Opaque replace nth_error.
destruct (s (ioapic d)); simpl.
destruct (nth_error IoApicIrqs (Z.to_nat n)).
destruct (nth_error IoApicEnables (Z.to_nat n)).
destruct b;
reflexivity.
reflexivity.
reflexivity.
Qed.
Lemma cons_intr_preserves_iflags:
∀ d d´,
cons_intr_spec d = Some d´ →
init d´ = init d ∧ ikern d´ = ikern d ∧ ihost d´ = ihost d.
Proof.
intros.
functional inversion H; subst.
functional inversion H0; functional inversion H5; simpl in *; subst; eauto.
Qed.
Lemma cons_intr_preserves_length:
∀ d d´,
cons_intr_spec d = Some d´ →
Zlength (IoApicEnables (s (ioapic d´))) = Zlength (IoApicEnables (s (ioapic d))).
Proof.
intros.
functional inversion H; subst.
functional inversion H0; functional inversion H5; simpl in *; subst; eauto.
Qed.
Lemma intr_flag_eq:
∀ d, intr_flag d = true → d = d {intr_flag: true}.
Proof.
intros.
destruct d.
simpl in ×.
rewrite H.
reflexivity.
Qed.
Lemma ic_intr_spec_not_none:
∀ v d,
ic_intr_spec v d ≠ None.
Proof.
intros.
unfold ic_intr_spec.
destruct (hw_intr_trans v d).
destruct o; try case_if;
intros Hs; inversion Hs.
Qed.
Lemma neq_same:
∀ {A} (a: A),
a ≠ a → False.
Proof.
intros.
apply H. reflexivity.
Qed.
Lemma serial_intr_pending_handler_inv:
∀ d d´ b,
serial_intr_pending_handler d = Some (d´, b) ∧
ikern d = true ∧
ihost d = true ∧
init d = true →
(
(b = true ∧
SerialIrq (s (com1 d)) = true ∧
∃ d0 d1,
ic_intr_spec 4 d = Some (d0, 36) ∧
serial_intr_handler_sw_spec d0 = Some d1 ∧
iret_spec d1 = Some d´
)
∨
(b = false ∧
SerialIrq (s (com1 d)) = false
)
).
Proof.
intros d d´ b.
unfold serial_intr_pending_handler. unfold serial_intr_handler_sw_spec.
intros (H & Hflag). blast Hflag.
subdestruct; subst; inversion H.
- left.
repeat (split; [auto |]). ∃ r. ∃ (r1 { ioapic / s / IoApicEnables [Pos.to_nat 4]:true}).
split; [auto |]. rewrite Hdestruct3. rewrite Hdestruct4.
rewrite H1. split.
{
functional inversion Hdestruct0. functional inversion H4. simpl.
rewrite Hflag0, Hflag2, Hflag3. reflexivity.
}
{
unfold iret_spec. rewrite H1. reflexivity.
}
- right. repeat (split; [auto |]). reflexivity.
Qed.
Lemma ic_intr_spec_cases:
∀ n d d´ v,
init d = true →
0 ≤ n ≤ 23 →
high_level_invariant d →
ic_intr_spec n d = Some (d´, v) →
v = 0 ∨ v = n + IRQ0.
Proof.
Opaque nth_error Z.to_nat.
intros n d d´ v Hinit Hnrange Hinv H. functional inversion H.
- subst. clear H. functional inversion H2; subst. clear H2.
unfold s_ioapic´ in ×. clear s_ioapic´. unfold ioapic_trans_intr in H1.
destruct d; simpl in ×. destruct ioapic; simpl in ×. destruct s; simpl in ×.
unfold update_CurrentIrq in H1; simpl in H1.
remember (Z.to_nat n) as nn.
inversion Hinv; simpl in ×.
destruct (nth_error IoApicIrqs nn) eqn: Hirq.
+ generalize (valid_ioapic_state Hinit _ _ Hirq). intros [Hz [b Henable]].
rewrite Henable in H1; simpl in H1. destruct b eqn: Hb; simpl in H1.
× inversion H1. generalize Hz. rewrite Heqnn. rewrite Z2Nat.id. clear Hz. intros Hz. clear Hinv.
subst.
unfold s_lapic´ in ×. clear s_lapic´. unfold lapic_trans_intr in H4.
destruct lapic; simpl in ×. destruct s; simpl in ×.
rewrite Hz in *; simpl in ×. unfold update_LapicEoi in H4; simpl in H4.
subdestruct.
inversion H4.
right. reflexivity.
omega. omega.
× inversion H1.
+ simpl in H1. inversion H1.
- left. reflexivity.
- left. reflexivity.
Qed.
Transparent nth_error Z.to_nat.
Lemma serial_intr_handler_body_correct_irq:
∀ m d d´ env le t b,
ikern d = true →
ihost d = true →
init d = true →
intr_flag d = true →
0 < t ≤ Z.of_nat INTR_ENABLE_REC_MAX →
env = PTree.empty _ →
SerialIrq (s (com1 d)) = true →
serial_intr_pending_handler d = Some (d´, b) →
high_level_invariant d →
le ! _t = Some (Vint (Int.repr t)) →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_enable_handler_loop_body E0 le´ (m, d´) Out_normal ∧
le´ ! _t = Some (Vint (Int.repr (t - 1))) ∧
SerialIrq (s (com1 d´)) = false ∧
le´ ! _has_irq = Some (Vint (Int.repr 0)).
Proof.
generalize max_unsigned_val; intro muval. toZ.
intros m d d´ env le t b Hk Hh Hinit Hintr_flag Htrange Henv Hirq H Hinv Ht.
assert (Hspec: serial_intr_pending_handler d = Some (d´, b) ∧ ikern d = true ∧
ihost d = true ∧ init d = true).
{
repeat (split; [auto|]); auto.
}
generalize (serial_intr_pending_handler_inv _ _ _ Hspec).
intros Hspecinv. destruct Hspecinv as [Hc | Hc]; blast Hc; subst.
-
has irq, not masked
esplit.
split. repeat vcgen.
{
f_equal. f_equal.
unfold serial_irq_current_spec.
simpl. functional inversion H2. simpl.
functional inversion H8; simpl;
(rewrite Int.unsigned_repr; [reflexivity | omega]).
}
{
split. discharge_cmp. ptreesolve.
split. simpl. functional inversion H2. functional inversion H8; simpl; reflexivity.
discharge_cmp. ptreesolve.
}
- rewrite Hirq in Hc1. inversion Hc1.
Qed.
Function serial_intr_enable_concrete_rec (n: nat) (abd: RData) {struct n} : option (RData × bool) :=
match n with
| O ⇒ Some (abd, true)
| S n´ ⇒
match serial_intr_enable_concrete_rec n´ abd with
| Some (d´, true) ⇒ match serial_intr_pending_handler d´ with
| Some (d´´, true) ⇒ Some (d´´, true)
| Some (d´´, false) ⇒ Some (d´, false)
| None ⇒ None
end
| Some (d´, false) ⇒ Some (d´, false)
| None ⇒ None
end
end.
Lemma serial_intr_pending_handler_irq_to_noirq:
∀ d d´,
SerialIrq (s (com1 d)) = true →
serial_intr_pending_handler d = Some (d´, true) →
SerialIrq (s (com1 d´)) = false.
Proof.
intros d d´ H.
unfold serial_intr_pending_handler. rewrite H. intros Hspec.
subdestruct.
inversion Hspec. simpl.
functional inversion Hdestruct3; simpl; reflexivity.
Qed.
Lemma serial_intr_pending_handler_noirq:
∀ d,
SerialIrq (s (com1 d)) = false →
serial_intr_pending_handler d = Some (d, false).
Proof.
intros d H.
unfold serial_intr_pending_handler. rewrite H. reflexivity.
Qed.
Lemma serial_intr_enable_concrete_aux_exec:
∀ d d´,
SerialIrq (s (com1 d)) = true →
serial_intr_enable_concrete_aux INTR_ENABLE_REC_MAX d = Some d´ →
serial_intr_pending_handler d = Some (d´, true).
Proof.
intros d d´ H.
destruct (serial_intr_pending_handler d) eqn: Hx. destruct p. destruct b.
- generalize (serial_intr_pending_handler_irq_to_noirq d r H Hx). intros H´.
generalize (serial_intr_pending_handler_noirq r H´). intros Hx´.
unfold serial_intr_enable_concrete_aux. rewrite Hx, Hx´. inversion 1. reflexivity.
- unfold serial_intr_pending_handler in Hx. rewrite H in Hx. subdestruct.
- unfold serial_intr_enable_concrete_aux. rewrite Hx. inversion 1.
Qed.
Lemma serial_intr_enable_concrete_aux_stop:
∀ d d´,
SerialIrq (s (com1 d)) = false →
serial_intr_enable_concrete_aux INTR_ENABLE_REC_MAX d = Some d´ →
d = d´.
Proof.
intros d d´ H Hspec.
generalize (serial_intr_pending_handler_noirq d H). intros Hpend.
unfold serial_intr_enable_concrete_aux in Hspec. rewrite Hpend in Hspec. inversion Hspec.
reflexivity.
Qed.
Lemma in_intr_same_rewrite:
∀ d b,
in_intr d = b →
d {in_intr: b} = d.
Proof.
intros.
unfold_RData.
destruct d; simpl in ×. subst. reflexivity.
Qed.
Lemma serial_intr_pending_handler_preserves_in_intr:
∀ d d´ b,
in_intr d = false →
serial_intr_pending_handler d = Some (d´, b) →
in_intr d´ = false.
Proof.
intros d d´ b H Hspec.
unfold serial_intr_pending_handler in Hspec. subdestruct.
inversion Hspec. simpl. reflexivity.
inversion Hspec. subst. assumption.
Qed.
Lemma serial_intr_enable_concrete_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
serial_intr_enable_concrete_aux_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_enable_handler_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hspec Hinv.
functional inversion Hspec.
destruct (SerialIrq (s (com1 d))) eqn: Hirq.
-
split. repeat vcgen.
{
f_equal. f_equal.
unfold serial_irq_current_spec.
simpl. functional inversion H2. simpl.
functional inversion H8; simpl;
(rewrite Int.unsigned_repr; [reflexivity | omega]).
}
{
split. discharge_cmp. ptreesolve.
split. simpl. functional inversion H2. functional inversion H8; simpl; reflexivity.
discharge_cmp. ptreesolve.
}
- rewrite Hirq in Hc1. inversion Hc1.
Qed.
Function serial_intr_enable_concrete_rec (n: nat) (abd: RData) {struct n} : option (RData × bool) :=
match n with
| O ⇒ Some (abd, true)
| S n´ ⇒
match serial_intr_enable_concrete_rec n´ abd with
| Some (d´, true) ⇒ match serial_intr_pending_handler d´ with
| Some (d´´, true) ⇒ Some (d´´, true)
| Some (d´´, false) ⇒ Some (d´, false)
| None ⇒ None
end
| Some (d´, false) ⇒ Some (d´, false)
| None ⇒ None
end
end.
Lemma serial_intr_pending_handler_irq_to_noirq:
∀ d d´,
SerialIrq (s (com1 d)) = true →
serial_intr_pending_handler d = Some (d´, true) →
SerialIrq (s (com1 d´)) = false.
Proof.
intros d d´ H.
unfold serial_intr_pending_handler. rewrite H. intros Hspec.
subdestruct.
inversion Hspec. simpl.
functional inversion Hdestruct3; simpl; reflexivity.
Qed.
Lemma serial_intr_pending_handler_noirq:
∀ d,
SerialIrq (s (com1 d)) = false →
serial_intr_pending_handler d = Some (d, false).
Proof.
intros d H.
unfold serial_intr_pending_handler. rewrite H. reflexivity.
Qed.
Lemma serial_intr_enable_concrete_aux_exec:
∀ d d´,
SerialIrq (s (com1 d)) = true →
serial_intr_enable_concrete_aux INTR_ENABLE_REC_MAX d = Some d´ →
serial_intr_pending_handler d = Some (d´, true).
Proof.
intros d d´ H.
destruct (serial_intr_pending_handler d) eqn: Hx. destruct p. destruct b.
- generalize (serial_intr_pending_handler_irq_to_noirq d r H Hx). intros H´.
generalize (serial_intr_pending_handler_noirq r H´). intros Hx´.
unfold serial_intr_enable_concrete_aux. rewrite Hx, Hx´. inversion 1. reflexivity.
- unfold serial_intr_pending_handler in Hx. rewrite H in Hx. subdestruct.
- unfold serial_intr_enable_concrete_aux. rewrite Hx. inversion 1.
Qed.
Lemma serial_intr_enable_concrete_aux_stop:
∀ d d´,
SerialIrq (s (com1 d)) = false →
serial_intr_enable_concrete_aux INTR_ENABLE_REC_MAX d = Some d´ →
d = d´.
Proof.
intros d d´ H Hspec.
generalize (serial_intr_pending_handler_noirq d H). intros Hpend.
unfold serial_intr_enable_concrete_aux in Hspec. rewrite Hpend in Hspec. inversion Hspec.
reflexivity.
Qed.
Lemma in_intr_same_rewrite:
∀ d b,
in_intr d = b →
d {in_intr: b} = d.
Proof.
intros.
unfold_RData.
destruct d; simpl in ×. subst. reflexivity.
Qed.
Lemma serial_intr_pending_handler_preserves_in_intr:
∀ d d´ b,
in_intr d = false →
serial_intr_pending_handler d = Some (d´, b) →
in_intr d´ = false.
Proof.
intros d d´ b H Hspec.
unfold serial_intr_pending_handler in Hspec. subdestruct.
inversion Hspec. simpl. reflexivity.
inversion Hspec. subst. assumption.
Qed.
Lemma serial_intr_enable_concrete_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
serial_intr_enable_concrete_aux_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_enable_handler_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hspec Hinv.
functional inversion Hspec.
destruct (SerialIrq (s (com1 d))) eqn: Hirq.
-
has irq
generalize (serial_intr_enable_concrete_aux_exec _ _ Hirq H5). intros Hhand.
exploit (serial_intr_handler_body_correct_irq
m d d0 (PTree.empty (block × type))
(PTree.set _has_irq (Vint Int.one) (PTree.set _t (Vint (Int.repr 100)) le)) 100 true);
eauto.
toZ. omega.
ptreesolve. intros (le´ & Hexec & Hle´ & Hirq´ & Hhasirq´).
esplit. subst.
unfold serial_intr_enable_handler_body.
repeat vcgen.
unfold serial_irq_current_spec. rewrite Hirq. rewrite Int.unsigned_repr. reflexivity. omega.
simpl. rewrite Int.unsigned_repr. simpl. reflexivity. omega.
discharge_cmp.
exploit (serial_intr_handler_body_correct_irq
m d d0 (PTree.empty (block × type))
(PTree.set _has_irq (Vint Int.one) (PTree.set _t (Vint (Int.repr 100)) le)) 100 true);
eauto.
toZ. omega.
ptreesolve. intros (le´ & Hexec & Hle´ & Hirq´ & Hhasirq´).
esplit. subst.
unfold serial_intr_enable_handler_body.
repeat vcgen.
unfold serial_irq_current_spec. rewrite Hirq. rewrite Int.unsigned_repr. reflexivity. omega.
simpl. rewrite Int.unsigned_repr. simpl. reflexivity. omega.
discharge_cmp.
first iteration
unfold Swhile.
change E0 with (E0 ** E0 ** E0).
eapply exec_Sloop_loop. unfold serial_intr_enable_handler_loop_condition.
vcgen.
vcgen. repeat vcgen.
eapply Hexec.
econstructor.
repeat vcgen.
change E0 with (E0 ** E0 ** E0).
eapply exec_Sloop_loop. unfold serial_intr_enable_handler_loop_condition.
vcgen.
vcgen. repeat vcgen.
eapply Hexec.
econstructor.
repeat vcgen.
second iteration
eapply exec_Sloop_stop1. unfold serial_intr_enable_handler_loop_condition.
eapply exec_Sseq_2.
repeat vcgen. simpl. rewrite in_intr_same_rewrite.
eapply exec_Sbreak.
apply (serial_intr_pending_handler_preserves_in_intr _ _ _ H0 Hhand).
intros Habsurd. inversion Habsurd.
econstructor.
-
eapply exec_Sseq_2.
repeat vcgen. simpl. rewrite in_intr_same_rewrite.
eapply exec_Sbreak.
apply (serial_intr_pending_handler_preserves_in_intr _ _ _ H0 Hhand).
intros Habsurd. inversion Habsurd.
econstructor.
-
no irq
subst.
esplit.
unfold serial_intr_enable_handler_body.
repeat vcgen. unfold serial_irq_current_spec. rewrite Hirq.
rewrite Int.unsigned_repr. reflexivity. omega.
rewrite Int.unsigned_repr. simpl. reflexivity. omega.
discharge_cmp.
generalize (serial_intr_enable_concrete_aux_stop _ _ Hirq H5). intros Hd.
rewrite <- Hd. rewrite in_intr_same_rewrite.
eapply exec_Sskip. assumption.
Qed.
End Serial_Intr_Enable_Body.
Theorem serial_intr_enable_code_correct:
spec_le (serial_intr_enable_handler ↦ serial_intr_enable_handler_spec_low)
(〚serial_intr_enable_handler ↦ f_serial_intr_enable_handler 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (serial_intr_enable_concrete_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_intr_enable_handler)
(nil)
(create_undef_temps (fn_temps f_serial_intr_enable_handler)))) H0.
Qed.
End SERIAL_INTR_ENABLE_HANDLER.
End WithPrimitives.
End DHANDLERCXTCODE.
esplit.
unfold serial_intr_enable_handler_body.
repeat vcgen. unfold serial_irq_current_spec. rewrite Hirq.
rewrite Int.unsigned_repr. reflexivity. omega.
rewrite Int.unsigned_repr. simpl. reflexivity. omega.
discharge_cmp.
generalize (serial_intr_enable_concrete_aux_stop _ _ Hirq H5). intros Hd.
rewrite <- Hd. rewrite in_intr_same_rewrite.
eapply exec_Sskip. assumption.
Qed.
End Serial_Intr_Enable_Body.
Theorem serial_intr_enable_code_correct:
spec_le (serial_intr_enable_handler ↦ serial_intr_enable_handler_spec_low)
(〚serial_intr_enable_handler ↦ f_serial_intr_enable_handler 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (serial_intr_enable_concrete_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_serial_intr_enable_handler)
(nil)
(create_undef_temps (fn_temps f_serial_intr_enable_handler)))) H0.
Qed.
End SERIAL_INTR_ENABLE_HANDLER.
End WithPrimitives.
End DHANDLERCXTCODE.