Library mcertikos.multithread.flatmem.PageFaultPHB

Require Import Coqlib.
Require Import Maps.
Require Import Globalenvs.
Require Import ASTExtra.
Require Import AsmX.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import LAsm.
Require Import AuxStateDataType.
Require Import Constant.
Require Import FlatMemory.
Require Import GlobIdent.
Require Import Integers.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import AsmImplLemma.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.ClightModules.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatClightSem.
Require Import liblayers.compcertx.MemWithData.

Require Import GlobalOracleProp.
Require Import AuxSingleAbstractDataType.
Require Import SingleAbstractDataType.
Require Import LoadStoreDefPHB.

Section PAGE_FAULT.

  Context `{Hmem: Mem.MemoryModel}.
  Context `{Hmwd: UseMemWithData mem}.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Context `{HD: CompatData PData}.

  Notation HDATAOps := (cdata (cdata_ops := data_ops) PData).

  Section GE.

    Context {F V} (ge: Genv.t F V).

    Definition single_exec_pagefault (m: mwd HDATAOps) (adr: int) (rs: regset): Asm.outcome (mem:= mwd HDATAOps)
      
      := let abd := (snd m) in
         let abd´ := single_trapinfo_set abd adr (rs RA) in
         match Genv.find_symbol ge pgf_handler with
           | Some b ⇒ Next (rs#RA <- (rs#PC)#PC <- (Vptr b Int.zero)) (fst m, abd´)
           | _ ⇒ Stuck
         end.

    Lemma single_exec_pagefault_fst_mem:
      ∀ m adr rs rs´ m´,
        single_exec_pagefault m adr rs = Next rs´ m´ →
        fst m´ = fst m.
    Proof.
      unfold single_exec_pagefault.
      destruct (Genv.find_symbol ge pgf_handler); try discriminate.
      injection 1; intros; subst; reflexivity.
    Qed.

    Lemma single_exec_pagefault_asm_invariant:
      ∀ m adr rs rs´ m´,
        single_exec_pagefault m adr rs = Next rs´ m´ →
        AsmX.asm_invariant ge rs m →
        AsmX.asm_invariant ge rs´ m´.
    Proof.
      unfold single_exec_pagefault.
      intros.
      destruct (Genv.find_symbol ge pgf_handler) eqn:?; try discriminate.
      inv H.
      inversion H0; subst.
      inversion inv_inject_neutral; subst.
      constructor.
      - constructor; auto.
        apply set_reg_inject; auto.
        + lift_unfold.
          econstructor.
          × unfold Mem.flat_inj.
            destruct (plt b (Mem.nextblock (fst m))) eqn:HLT; simpl in *; rewrite HLT.
            { reflexivity. }
            { exploit Genv.genv_symb_range; eauto.
              xomega. }
          × reflexivity.
        + apply set_reg_inject; auto.
      - apply set_reg_wt; auto.
        + constructor.
        + apply set_reg_wt; auto.
          change (typ_of_preg RA) with (typ_of_preg PC); auto.
    Qed.

    Lemma single_exec_pagefault_low_level_invariant `{Single_TrapinfoSetInvariant}:
      ∀ m adr rs rs´ m´,
        single_exec_pagefault m adr rs = Next rs´ m´ →
        AsmX.asm_invariant ge rs m →
        CompatData.low_level_invariant (Mem.nextblock m) (snd m) →
        CompatData.low_level_invariant (Mem.nextblock m´) (snd m´).
    Proof.
      unfold single_exec_pagefault.
      destruct (Genv.find_symbol ge pgf_handler); try discriminate.
      injection 1; intros; subst; simpl.
      inv H3.
      inv inv_inject_neutral.
      eapply single_trapinfo_set_low_level_invariant in H4; eauto.
      apply inv_reg_wt.
    Qed.

    Lemma single_exec_pagefault_high_level_invariant `{Single_TrapinfoSetInvariant}:
      ∀ m adr rs rs´ m´,
        single_exec_pagefault m adr rs = Next rs´ m´ →
        high_level_invariant (snd m) →
        high_level_invariant (snd m´).
    Proof.
      unfold single_exec_pagefault.
      destruct (Genv.find_symbol ge pgf_handler); try discriminate.
      injection 1; intros; subst; simpl.
      eapply single_trapinfo_set_high_level_invariant in H3; eauto.
    Qed.

  End GE.

End PAGE_FAULT.