Library mcertikos.devdrivers.DIoApicCode
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 LApicGenSpec.
Require Import ObjInterruptController.
Require Import ObjInterruptDriver.
Require Import DIoApic.
Require Import DeviceStateDataType.
Require Import INVLemmaDriver.
Require Import DIoApicCSource.
Module DIOAPICCODE.
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 LAPICINIT.
Let L: compatlayer (cdata RData) :=
lapic_read ↦ gensem lapic_read_spec
⊕ lapic_write ↦ gensem lapic_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 LApicInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (blapic_read: block).
Hypothesis hlapic_read1 : Genv.find_symbol ge lapic_read = Some blapic_read.
Hypothesis hlapic_read2 : Genv.find_funct_ptr ge blapic_read =
Some (External (EF_external lapic_read
(signature_of_type (Tcons tuint Tnil)
tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (blapic_write: block).
Hypothesis hlapic_write1 : Genv.find_symbol ge lapic_write = Some blapic_write.
Hypothesis hlapic_write2 : Genv.find_funct_ptr ge blapic_write =
Some (External (EF_external lapic_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_lapic; unfold update_s; unfold update_l1;
unfold update_l2; unfold update_l3; simpl; unfold_LApicState.
Ltac solve_lapic_wr :=
unfold lapic_write_spec, lapic_trans_cpu; unfold_data.
Lemma lapic_init_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
lapic_init_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) lapic_init_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hinv Hspec.
functional inversion Hspec. clear H Hspec Hinv.
destruct d; destruct lapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold lapic_init_body.
Opaque Z.add Z.mul lapic_write_spec.
repeat vcgen.
Transparent Z.add Z.mul lapic_write_spec.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr.
unfold lapic_reg_to_enable, lapic_reg_to_spurious, lapic_reg_to_lvt_mask; simpl.
unfold_data. reflexivity.
Qed.
End LApicInitBody.
Theorem lapic_init_code_correct:
spec_le
(lapic_init ↦ lapic_init_spec_low)
(〚lapic_init ↦ f_lapic_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(lapic_init_body_correct s
(Genv.globalenv p) makeglobalenv b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_lapic_init) nil
(create_undef_temps (fn_temps f_lapic_init))
)
) H0.
Qed.
End LAPICINIT.
Section LAPICEOI.
Let L: compatlayer (cdata RData) :=
lapic_read ↦ gensem lapic_read_spec
⊕ lapic_write ↦ gensem lapic_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 LApicEoiBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (blapic_read: block).
Hypothesis hlapic_read1 : Genv.find_symbol ge lapic_read = Some blapic_read.
Hypothesis hlapic_read2 : Genv.find_funct_ptr ge blapic_read =
Some (External (EF_external lapic_read
(signature_of_type (Tcons tuint Tnil)
tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (blapic_write: block).
Hypothesis hlapic_write1 : Genv.find_symbol ge lapic_write = Some blapic_write.
Hypothesis hlapic_write2 : Genv.find_funct_ptr ge blapic_write =
Some (External (EF_external lapic_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_lapic; unfold update_s; simpl; unfold_LApicState.
Lemma lapic_eoi_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
lapic_eoi_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) lapic_eoi_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hinv Hspec.
functional inversion Hspec. clear H Hspec Hinv.
destruct d; destruct lapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold lapic_eoi_body.
Opaque Z.add Z.mul lapic_write_spec.
repeat vcgen.
Qed.
End LApicEoiBody.
Theorem lapic_eoi_code_correct:
spec_le
(lapic_eoi ↦ lapic_eoi_spec_low)
(〚lapic_eoi ↦ f_lapic_eoi 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(lapic_eoi_body_correct s
(Genv.globalenv p) makeglobalenv b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_lapic_eoi) nil
(create_undef_temps (fn_temps f_lapic_eoi))
)
) H0.
Qed.
End LAPICEOI.
End WithPrimitives.
End DIOAPICCODE.
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 LApicGenSpec.
Require Import ObjInterruptController.
Require Import ObjInterruptDriver.
Require Import DIoApic.
Require Import DeviceStateDataType.
Require Import INVLemmaDriver.
Require Import DIoApicCSource.
Module DIOAPICCODE.
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 LAPICINIT.
Let L: compatlayer (cdata RData) :=
lapic_read ↦ gensem lapic_read_spec
⊕ lapic_write ↦ gensem lapic_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 LApicInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (blapic_read: block).
Hypothesis hlapic_read1 : Genv.find_symbol ge lapic_read = Some blapic_read.
Hypothesis hlapic_read2 : Genv.find_funct_ptr ge blapic_read =
Some (External (EF_external lapic_read
(signature_of_type (Tcons tuint Tnil)
tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (blapic_write: block).
Hypothesis hlapic_write1 : Genv.find_symbol ge lapic_write = Some blapic_write.
Hypothesis hlapic_write2 : Genv.find_funct_ptr ge blapic_write =
Some (External (EF_external lapic_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_lapic; unfold update_s; unfold update_l1;
unfold update_l2; unfold update_l3; simpl; unfold_LApicState.
Ltac solve_lapic_wr :=
unfold lapic_write_spec, lapic_trans_cpu; unfold_data.
Lemma lapic_init_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
lapic_init_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) lapic_init_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hinv Hspec.
functional inversion Hspec. clear H Hspec Hinv.
destruct d; destruct lapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold lapic_init_body.
Opaque Z.add Z.mul lapic_write_spec.
repeat vcgen.
Transparent Z.add Z.mul lapic_write_spec.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr. reflexivity.
solve_lapic_wr.
unfold lapic_reg_to_enable, lapic_reg_to_spurious, lapic_reg_to_lvt_mask; simpl.
unfold_data. reflexivity.
Qed.
End LApicInitBody.
Theorem lapic_init_code_correct:
spec_le
(lapic_init ↦ lapic_init_spec_low)
(〚lapic_init ↦ f_lapic_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(lapic_init_body_correct s
(Genv.globalenv p) makeglobalenv b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_lapic_init) nil
(create_undef_temps (fn_temps f_lapic_init))
)
) H0.
Qed.
End LAPICINIT.
Section LAPICEOI.
Let L: compatlayer (cdata RData) :=
lapic_read ↦ gensem lapic_read_spec
⊕ lapic_write ↦ gensem lapic_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 LApicEoiBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variable (blapic_read: block).
Hypothesis hlapic_read1 : Genv.find_symbol ge lapic_read = Some blapic_read.
Hypothesis hlapic_read2 : Genv.find_funct_ptr ge blapic_read =
Some (External (EF_external lapic_read
(signature_of_type (Tcons tuint Tnil)
tuint
cc_default))
(Tcons tuint Tnil) tuint cc_default).
Variable (blapic_write: block).
Hypothesis hlapic_write1 : Genv.find_symbol ge lapic_write = Some blapic_write.
Hypothesis hlapic_write2 : Genv.find_funct_ptr ge blapic_write =
Some (External (EF_external lapic_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_lapic; unfold update_s; simpl; unfold_LApicState.
Lemma lapic_eoi_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
high_level_invariant d →
lapic_eoi_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) lapic_eoi_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hinv Hspec.
functional inversion Hspec. clear H Hspec Hinv.
destruct d; destruct lapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold lapic_eoi_body.
Opaque Z.add Z.mul lapic_write_spec.
repeat vcgen.
Qed.
End LApicEoiBody.
Theorem lapic_eoi_code_correct:
spec_le
(lapic_eoi ↦ lapic_eoi_spec_low)
(〚lapic_eoi ↦ f_lapic_eoi 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(lapic_eoi_body_correct s
(Genv.globalenv p) makeglobalenv b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_lapic_eoi) nil
(create_undef_temps (fn_temps f_lapic_eoi))
)
) H0.
Qed.
End LAPICEOI.
End WithPrimitives.
End DIOAPICCODE.