Library mcertikos.devdrivers.DConsoleCode

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 DConsoleCSource.
Require Import HandlerIntroGenSpec.
Require Import ObjInterruptDriver.
Require Import ObjMultiprocessor.

Module DCONSOLECODE.

  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 INTRDEFAULTHANDLER.

      Let L: compatlayer (cdata RData) :=
        lapic_eoi ↦ gensem lapic_eoi_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 IntrDefaultHandlerBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

        Variables (ge: genv)
                  (STENCIL_MATCHES: stencil_matches sc ge).

        Variable (blapic_eoi: block).
        Hypothesis hlapic_eoi1 : Genv.find_symbol ge lapic_eoi = Some blapic_eoi.
        Hypothesis hlapic_eoi2 : Genv.find_funct_ptr ge blapic_eoi =
                                 Some (External (EF_external lapic_eoi
                                                             (signature_of_type Tnil tvoid
                                                                                cc_default))
                                                Tnil tvoid cc_default).

        Import DeviceStateDataType.
        Lemma intr_default_handler_body_correct:
          ∀ m d d´ env le,
            env = PTree.empty _ →
            high_level_invariant d →
            intr_default_handler_spec d = Some d´ →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) intr_default_handler_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; simpl in ×. destruct s; simpl in ×.
          unfold_LApicState. unfold_DeviceData. unfold_RData.
          subst. esplit. unfold intr_default_handler_body.
          repeat vcgen.
        Qed.
      End IntrDefaultHandlerBody.

      Theorem intr_default_handler_code_correct:
        spec_le
          (intr_default_handler ↦ intr_default_handler_spec_low)
          (〚intr_default_handler ↦ f_intr_default_handler 〛L).
      Proof.
        fbigstep_pre L.
        fbigstep
          (intr_default_handler_body_correct s
                                        (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp m´0 labd labd´ (PTree.empty _)
                                        (bind_parameter_temps´ (fn_params f_intr_default_handler) nil
                                                         (create_undef_temps (fn_temps f_intr_default_handler))
                                  )
          ) H0.
      Qed.

    End INTRDEFAULTHANDLER.

    Section GETCURRINTRNUM.

      Let L: compatlayer (cdata RData) := curr_intr_num_LOC ↦ v_curr_intr_num.

      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 GetCurrIntrNumBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

        Variables (ge: genv)
                  (STENCIL_MATCHES: stencil_matches sc ge).

        Variable (bcurr_intr_num: block).

        Hypothesis hcurr_intr_num_loc :
          Genv.find_symbol ge curr_intr_num_LOC = Some bcurr_intr_num.

        Lemma get_curr_intr_num_body_correct:
          ∀ m d env le v,
            env = PTree.empty _ →
            Mem.loadv Mint32 (m, d) (Vptr bcurr_intr_num Int.zero) = Some (Vint v) →
            exec_stmt ge env le ((m, d): mem) get_curr_intr_num_body E0 le (m, d)
                      (Out_return (Some (Vint v, tint))).
        Proof.
          intros m d env le z Henv Hmem. subst.
          unfold get_curr_intr_num_body.
          repeat vcgen.
        Qed.

      End GetCurrIntrNumBody.

      Theorem get_curr_intr_num_code_correct:
        spec_le
          (get_curr_intr_num ↦ get_curr_intr_num_spec_low)
          (〚get_curr_intr_num ↦ f_get_curr_intr_num 〛L).
      Proof.
        fbigstep_pre L.
        fbigstep
          (get_curr_intr_num_body_correct
             (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_get_curr_intr_num) nil
                                    (create_undef_temps (fn_temps f_get_curr_intr_num))
             )
          ) m´.
      Qed.
    End GETCURRINTRNUM.

  End WithPrimitives.

End DCONSOLECODE.