Library mcertikos.devdrivers.DSerialCode_ioapic_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 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 IOAPICENABLE.
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 IoApicEnableBody.
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.
Import DeviceStateDataType.
Lemma ioapic_enable_body_correct:
∀ m d d´ env le i l t p,
env = PTree.empty _ →
high_level_invariant d →
PTree.get _irq le = Some (Vint i) →
PTree.get _lapicid le = Some (Vint l) →
PTree.get _trigger_mode le = Some (Vint t) →
PTree.get _polarity le = Some (Vint p) →
ioapic_enable_spec (Int.unsigned i) (Int.unsigned l)
(Int.unsigned t) (Int.unsigned p) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) ioapic_enable_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le i l t p Henv Hinv Hlei Hlel Hlet Hlep Hspec.
functional inversion Hspec. clear H H3 H4 H5 H6 Hspec.
inversion Hinv. clear Hinv.
destruct d; destruct ioapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold ioapic_enable_body.
repeat vcgen;
try rewrite Z_div_mult; try rewrite Z.mod_small; try omega.
unfold_read_spec.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega.
repeat vcgen.
repeat vcgen.
discharge_cmp; [| rewrite Z_div_mult; omega].
rewrite Z_div_mult by omega.
rewrite Z.mod_small by omega.
Opaque Z.add Z.mul.
repeat vcgen.
unfold_write_spec.
unfold_data.
if_false. if_true.
{
replace (16 + 2 × (Int.unsigned i - 0)) with (16 + 2 × Int.unsigned i) by omega.
destruct (16 + 2 × Int.unsigned i) eqn: Hcase.
- omega.
- if_true. simpl. rewrite <- Hcase. unfold addr_to_idx. if_true. calc.
replace ((32768 × Int.unsigned t + 8192 × Int.unsigned p +
Int.unsigned i + 32) mod 256) with (Int.unsigned i + 32).
replace (2 × Int.unsigned i / 2) with (Int.unsigned i).
replace (((32768 × Int.unsigned t + 8192 × Int.unsigned p +
Int.unsigned i + 32) / 65536) mod 2 =? 0) with true.
reflexivity.
+ rewrite Z.div_small. calc. reflexivity. omega.
+ calc. reflexivity. omega.
+ rewrite <- Z.add_assoc. remember (Int.unsigned i + 32) as x.
rewrite Z.add_mod by omega. rewrite Z.add_mod with (a:=(32768 × Int.unsigned t)) by omega.
calc. reflexivity.
+ Transparent Z.add Z.mul. calc. reflexivity.
+ calc. auto.
- assert (Habsurd: 16 + 2 × Int.unsigned i ≥ 0) by omega. rewrite Hcase in Habsurd.
apply Z_neg_absurd in Habsurd. inversion Habsurd.
}
Opaque Z.add Z.mul.
unfold_write_spec.
unfold_data.
if_false. if_true.
{
replace (16 + 2 × (Int.unsigned i - 0) + 1) with (17 + 2 × Int.unsigned i).
destruct (17 + 2 × Int.unsigned i) eqn: Hcase.
- omega.
- simpl. if_true. unfold addr_to_idx. if_false.
unfold ret. simpl. reflexivity.
rewrite <- Hcase. remember (Int.unsigned i) as ui.
replace (17 + 2 × ui) with ((8 + ui) × 2 + 1) by omega.
rewrite Z_odd_mod. omega.
- assert (Habsurd: 17 + 2 × Int.unsigned i ≥ 0) by omega. rewrite Hcase in Habsurd.
apply Z_neg_absurd in Habsurd. inversion Habsurd.
- calc. reflexivity.
}
Qed.
End IoApicEnableBody.
Theorem ioapic_enable_code_correct:
spec_le
(ioapic_enable ↦ ioapic_enable_spec_low)
(〚ioapic_enable ↦ f_ioapic_enable 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(ioapic_enable_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_enable) (Vint i :: Vint l :: Vint p0 :: Vint t :: nil)
(create_undef_temps (fn_temps f_ioapic_enable))
)
) H0.
Qed.
End IOAPICENABLE.
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 IOAPICENABLE.
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 IoApicEnableBody.
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.
Import DeviceStateDataType.
Lemma ioapic_enable_body_correct:
∀ m d d´ env le i l t p,
env = PTree.empty _ →
high_level_invariant d →
PTree.get _irq le = Some (Vint i) →
PTree.get _lapicid le = Some (Vint l) →
PTree.get _trigger_mode le = Some (Vint t) →
PTree.get _polarity le = Some (Vint p) →
ioapic_enable_spec (Int.unsigned i) (Int.unsigned l)
(Int.unsigned t) (Int.unsigned p) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) ioapic_enable_body E0 le´ (m, d´)
Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le i l t p Henv Hinv Hlei Hlel Hlet Hlep Hspec.
functional inversion Hspec. clear H H3 H4 H5 H6 Hspec.
inversion Hinv. clear Hinv.
destruct d; destruct ioapic; destruct s; simpl in ×.
unfold_data.
subst. esplit. unfold ioapic_enable_body.
repeat vcgen;
try rewrite Z_div_mult; try rewrite Z.mod_small; try omega.
unfold_read_spec.
rewrite Int.unsigned_repr; [reflexivity | omega].
discharge_cmp.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega. omega.
omega. omega.
repeat vcgen.
repeat vcgen.
discharge_cmp; [| rewrite Z_div_mult; omega].
rewrite Z_div_mult by omega.
rewrite Z.mod_small by omega.
Opaque Z.add Z.mul.
repeat vcgen.
unfold_write_spec.
unfold_data.
if_false. if_true.
{
replace (16 + 2 × (Int.unsigned i - 0)) with (16 + 2 × Int.unsigned i) by omega.
destruct (16 + 2 × Int.unsigned i) eqn: Hcase.
- omega.
- if_true. simpl. rewrite <- Hcase. unfold addr_to_idx. if_true. calc.
replace ((32768 × Int.unsigned t + 8192 × Int.unsigned p +
Int.unsigned i + 32) mod 256) with (Int.unsigned i + 32).
replace (2 × Int.unsigned i / 2) with (Int.unsigned i).
replace (((32768 × Int.unsigned t + 8192 × Int.unsigned p +
Int.unsigned i + 32) / 65536) mod 2 =? 0) with true.
reflexivity.
+ rewrite Z.div_small. calc. reflexivity. omega.
+ calc. reflexivity. omega.
+ rewrite <- Z.add_assoc. remember (Int.unsigned i + 32) as x.
rewrite Z.add_mod by omega. rewrite Z.add_mod with (a:=(32768 × Int.unsigned t)) by omega.
calc. reflexivity.
+ Transparent Z.add Z.mul. calc. reflexivity.
+ calc. auto.
- assert (Habsurd: 16 + 2 × Int.unsigned i ≥ 0) by omega. rewrite Hcase in Habsurd.
apply Z_neg_absurd in Habsurd. inversion Habsurd.
}
Opaque Z.add Z.mul.
unfold_write_spec.
unfold_data.
if_false. if_true.
{
replace (16 + 2 × (Int.unsigned i - 0) + 1) with (17 + 2 × Int.unsigned i).
destruct (17 + 2 × Int.unsigned i) eqn: Hcase.
- omega.
- simpl. if_true. unfold addr_to_idx. if_false.
unfold ret. simpl. reflexivity.
rewrite <- Hcase. remember (Int.unsigned i) as ui.
replace (17 + 2 × ui) with ((8 + ui) × 2 + 1) by omega.
rewrite Z_odd_mod. omega.
- assert (Habsurd: 17 + 2 × Int.unsigned i ≥ 0) by omega. rewrite Hcase in Habsurd.
apply Z_neg_absurd in Habsurd. inversion Habsurd.
- calc. reflexivity.
}
Qed.
End IoApicEnableBody.
Theorem ioapic_enable_code_correct:
spec_le
(ioapic_enable ↦ ioapic_enable_spec_low)
(〚ioapic_enable ↦ f_ioapic_enable 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(ioapic_enable_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_enable) (Vint i :: Vint l :: Vint p0 :: Vint t :: nil)
(create_undef_temps (fn_temps f_ioapic_enable))
)
) H0.
Qed.
End IOAPICENABLE.
End WithPrimitives.
End DSERIALCODE.