Library mcertikos.devdrivers.DHandlerIntroCode
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 DeviceStateDataType.
Require Import HandlerSwGenSpec.
Require Import FutureTactic.
Require Import INVLemmaDriver.
Require Import CommonTactic.
Require Import FutureTactic.
Require Import XOmega.
Require Import DHandlerIntroCSource.
Require Import DHandlerIntro.
Module DHANDLERINTROCODE.
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_HANDLER_SW.
Let L: compatlayer (cdata RData) := cons_intr ↦ gensem cons_intr_spec
⊕ sti ↦ gensem sti_spec
⊕ ioapic_mask ↦ gensem ioapic_mask_spec
⊕ ioapic_unmask ↦ gensem ioapic_unmask_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_Handler_Sw_Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bcons_intr: block).
Hypothesis hcons_intr1 : Genv.find_symbol ge cons_intr = Some bcons_intr.
Hypothesis hcons_intr2 : Genv.find_funct_ptr ge bcons_intr =
Some (External (EF_external cons_intr
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (bsti: block).
Hypothesis hsti1 : Genv.find_symbol ge sti = Some bsti.
Hypothesis hsti2 : Genv.find_funct_ptr ge bsti =
Some (External (EF_external sti
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (bioapic_mask: block).
Hypothesis hioapic_mask1 : Genv.find_symbol ge ioapic_mask = Some bioapic_mask.
Hypothesis hioapic_mask2 : Genv.find_funct_ptr ge bioapic_mask =
Some (External (EF_external ioapic_mask
(signature_of_type (Tcons tuint Tnil) tvoid
cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Variable (bioapic_unmask: block).
Hypothesis hioapic_unmask1 : Genv.find_symbol ge ioapic_unmask = Some bioapic_unmask.
Hypothesis hioapic_unmask2 : Genv.find_funct_ptr ge bioapic_unmask =
Some (External (EF_external ioapic_unmask
(signature_of_type (Tcons tuint Tnil) tvoid
cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Lemma serial_intr_handler_sw_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
serial_intr_handler_sw_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_handler_sw_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. subst.
esplit.
unfold serial_intr_handler_sw_body.
change (Z.to_nat 4) with 4%nat in ×. change (Pos.to_nat 4) with 4%nat in ×.
repeat vcgen.
{
unfold ioapic_mask_spec. rewrite H1, H3, H2.
inversion Hinv.
if_true. reflexivity.
}
{
unfold cons_intr_spec. simpl. rewrite H3, H2, H1, H0.
change (Z.to_nat 4) with 4%nat in ×. change (Pos.to_nat 4) with 4%nat in ×.
rewrite H4. eassumption.
}
{
unfold ioapic_unmask_spec. if_true. if_true. if_true. if_true.
change (Z.to_nat 4) with 4%nat in ×. change (Pos.to_nat 4) with 4%nat in ×.
reflexivity.
- functional inversion H5; functional inversion H4;
inversion Hinv; simpl; change (Z.to_nat 4) with 4%nat in *;
change (Pos.to_nat 4) with 4%nat in *; rewrite replace_preserves_Zlength; omega.
- functional inversion H5; functional inversion H4;
inversion Hinv; simpl; change (Z.to_nat 4) with 4%nat in *;
change (Pos.to_nat 4) with 4%nat in *; rewrite replace_preserves_Zlength; omega.
- functional inversion H5; simpl; functional inversion H4; simpl; assumption.
- functional inversion H5; simpl; functional inversion H4; simpl; assumption.
- functional inversion H5; simpl; functional inversion H4; simpl; assumption.
}
Qed.
End Serial_Intr_Handler_Sw_Body.
Theorem serial_intr_handler_sw_code_correct:
spec_le (serial_intr_handler_sw ↦ serial_intr_handler_sw_spec_low)
(〚serial_intr_handler_sw ↦ f_serial_intr_handler_sw 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (serial_intr_handler_sw_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_handler_sw)
(nil)
(create_undef_temps (fn_temps f_serial_intr_handler_sw)))) H0.
Qed.
End SERIAL_INTR_HANDLER_SW.
End WithPrimitives.
End DHANDLERINTROCODE.
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 DeviceStateDataType.
Require Import HandlerSwGenSpec.
Require Import FutureTactic.
Require Import INVLemmaDriver.
Require Import CommonTactic.
Require Import FutureTactic.
Require Import XOmega.
Require Import DHandlerIntroCSource.
Require Import DHandlerIntro.
Module DHANDLERINTROCODE.
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_HANDLER_SW.
Let L: compatlayer (cdata RData) := cons_intr ↦ gensem cons_intr_spec
⊕ sti ↦ gensem sti_spec
⊕ ioapic_mask ↦ gensem ioapic_mask_spec
⊕ ioapic_unmask ↦ gensem ioapic_unmask_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_Handler_Sw_Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (bcons_intr: block).
Hypothesis hcons_intr1 : Genv.find_symbol ge cons_intr = Some bcons_intr.
Hypothesis hcons_intr2 : Genv.find_funct_ptr ge bcons_intr =
Some (External (EF_external cons_intr
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (bsti: block).
Hypothesis hsti1 : Genv.find_symbol ge sti = Some bsti.
Hypothesis hsti2 : Genv.find_funct_ptr ge bsti =
Some (External (EF_external sti
(signature_of_type Tnil tvoid
cc_default))
Tnil tvoid cc_default).
Variable (bioapic_mask: block).
Hypothesis hioapic_mask1 : Genv.find_symbol ge ioapic_mask = Some bioapic_mask.
Hypothesis hioapic_mask2 : Genv.find_funct_ptr ge bioapic_mask =
Some (External (EF_external ioapic_mask
(signature_of_type (Tcons tuint Tnil) tvoid
cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Variable (bioapic_unmask: block).
Hypothesis hioapic_unmask1 : Genv.find_symbol ge ioapic_unmask = Some bioapic_unmask.
Hypothesis hioapic_unmask2 : Genv.find_funct_ptr ge bioapic_unmask =
Some (External (EF_external ioapic_unmask
(signature_of_type (Tcons tuint Tnil) tvoid
cc_default))
(Tcons tuint Tnil) tvoid cc_default).
Lemma serial_intr_handler_sw_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
serial_intr_handler_sw_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) serial_intr_handler_sw_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. subst.
esplit.
unfold serial_intr_handler_sw_body.
change (Z.to_nat 4) with 4%nat in ×. change (Pos.to_nat 4) with 4%nat in ×.
repeat vcgen.
{
unfold ioapic_mask_spec. rewrite H1, H3, H2.
inversion Hinv.
if_true. reflexivity.
}
{
unfold cons_intr_spec. simpl. rewrite H3, H2, H1, H0.
change (Z.to_nat 4) with 4%nat in ×. change (Pos.to_nat 4) with 4%nat in ×.
rewrite H4. eassumption.
}
{
unfold ioapic_unmask_spec. if_true. if_true. if_true. if_true.
change (Z.to_nat 4) with 4%nat in ×. change (Pos.to_nat 4) with 4%nat in ×.
reflexivity.
- functional inversion H5; functional inversion H4;
inversion Hinv; simpl; change (Z.to_nat 4) with 4%nat in *;
change (Pos.to_nat 4) with 4%nat in *; rewrite replace_preserves_Zlength; omega.
- functional inversion H5; functional inversion H4;
inversion Hinv; simpl; change (Z.to_nat 4) with 4%nat in *;
change (Pos.to_nat 4) with 4%nat in *; rewrite replace_preserves_Zlength; omega.
- functional inversion H5; simpl; functional inversion H4; simpl; assumption.
- functional inversion H5; simpl; functional inversion H4; simpl; assumption.
- functional inversion H5; simpl; functional inversion H4; simpl; assumption.
}
Qed.
End Serial_Intr_Handler_Sw_Body.
Theorem serial_intr_handler_sw_code_correct:
spec_le (serial_intr_handler_sw ↦ serial_intr_handler_sw_spec_low)
(〚serial_intr_handler_sw ↦ f_serial_intr_handler_sw 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (serial_intr_handler_sw_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_handler_sw)
(nil)
(create_undef_temps (fn_temps f_serial_intr_handler_sw)))) H0.
Qed.
End SERIAL_INTR_HANDLER_SW.
End WithPrimitives.
End DHANDLERINTROCODE.