Library mcertikos.proc.EPTIntroGenAsm


Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.

Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.

Require Import PProc.
Require Import EPTIntroGenSpec.
Require Import EPTIntroGenAsmSource.

Require Import LAsmModuleSemSpec.
Require Import LRegSet.
Require Import AbstractDataType.

Section ASM_VERIFICATION.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.
  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Notation LDATA := RData.
  Notation LDATAOps := (cdata LDATA).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.
    Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
    Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.

    Section EPT_INVALIDATE_MAPPINGS.

      Ltac accessors_simpl:=
        match goal with
          | |- exec_storeex _ _ _ _ _ _ _ = _
            unfold exec_storeex, LoadStoreSem2.exec_storeex2;
              simpl; Lregset_simpl_tac;
              match goal with
                | |- context[Asm.exec_store _ _ _ _ _ _ _ ] ⇒
                  unfold Asm.exec_store; simpl;
                  Lregset_simpl_tac; lift_trivial
              end
          | |- exec_loadex _ _ _ _ _ _ = _
            unfold exec_loadex, LoadStoreSem2.exec_loadex2;
              simpl; Lregset_simpl_tac;
              match goal with
                | |- context[Asm.exec_load _ _ _ _ _ _ ] ⇒
                  unfold Asm.exec_load; simpl;
                  Lregset_simpl_tac; lift_trivial
              end
        end.

      Lemma Hget_CPU_ID:
         MCode_Asm s ge,
          make_globalenv s MCode_Asm pproc = ret ge
          ( b_get_CPU_ID, Genv.find_symbol ge get_CPU_ID = Some b_get_CPU_ID
                                 Genv.find_funct_ptr ge b_get_CPU_ID =
                                   Some (External (EF_external get_CPU_ID (mksignature nil (Some Tint) cc_default))))
           get_layer_primitive get_CPU_ID pproc = OK (Some (gensem get_CPU_ID_spec)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive get_CPU_ID pproc = OK (Some (gensem get_CPU_ID_spec)))
          by (unfold pproc; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

      Lemma ept_invalidate_mappings_spec:
         ge (s: stencil) (rs rs´: regset) b b0 (m0: mwd LDATAOps) (Hhigh: high_level_invariant (snd m0)) (Hsymbol: find_symbol s EPT_LOC = Some b0),
          find_symbol s ept_invalidate_mappings = Some b
          make_globalenv s (ept_invalidate_mappings ept_invalidate_mappings_function) pproc = ret ge
          rs PC = Vptr b Int.zero
          asm_invariant (mem := mwd LDATAOps) s rs m0
          kernel_mode (snd m0) →
          let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
                                     :: IR EDX :: RA :: nil)
                                 (undef_regs (List.map preg_of destroyed_at_call) rs)) in
           m0´ r_,
            lasm_step (ept_invalidate_mappings ept_invalidate_mappings_function)
                      (pproc (Hmwd:= Hmwd) (Hmem:= Hmem)) ept_invalidate_mappings s rs m0 r_ m0´
             inject_incr (Mem.flat_inj (Mem.nextblock m0))
             Memtype.Mem.inject m0 m0´
             (Mem.nextblock m0 Mem.nextblock m0´)%positive
             ( l,
                  Val.lessdef (Pregmap.get l (rs´#PC <- (rs#RA)#EAX <- Vzero))
                              (Pregmap.get l r_)).
      Proof.
        generalize max_unsigned_val; intro muval.
        intros. destruct H3 as [Hikern Hihost].
        destruct m0 as [m0 d].
        lift_unfold.

        caseEq(Mem.alloc m0 0 24).
        intros m1 b1 HALC.
        exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
        intros Hstencil_matches.

        assert (Hblock: Ple (Genv.genv_next ge) b1 Plt b1 (Mem.nextblock m1)).
        {
          erewrite Mem.nextblock_alloc; eauto.
          apply Mem.alloc_result in HALC.
          rewrite HALC. inv H2.
          inv inv_inject_neutral.
          inv Hstencil_matches.
          rewrite stencil_matches_genv_next.
          lift_unfold.
          split; xomega.
        }

        specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros HV.

        assert (HV1: Mem.valid_access m1 Mint32 b1 16 Freeable).
        {
          eapply HV; auto; simpl; try omega.
          unfold Z.divide.
           4; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV1; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (rs ESP) HV1) as [m2 HST1].
        assert (HV2: Mem.valid_access m2 Mint32 b1 20 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply HV; auto; simpl; try omega.
          unfold Z.divide.
           5; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (rs RA) HV2) as [m3 HST2].

        assert (HV3: Mem.valid_access m3 Mint32 b1 0 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply HV; auto; simpl; try omega.
           0; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (Vptr b0 (Int.repr (30 + CPU_ID d × 8413184))) HV3) as [m4 HST3].

        assert (HV4: Mem.valid_access m4 Mint32 b1 4 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply HV; auto; simpl; try omega.
           1; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV4; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ Vzero HV4) as [m5 HST4].

        assert (HV5: Mem.valid_access m5 Mint32 b1 8 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply HV; auto; simpl; try omega.
           2; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV5; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ Vzero HV5) as [m6 HST5].

        assert (HV6: Mem.valid_access m6 Mint32 b1 12 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply HV; auto; simpl; try omega.
           3; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV6; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ Vzero HV6) as [m7 HST6].

        assert (HV7: Mem.range_perm m7 b1 0 24 Cur Freeable).
        {
          unfold Mem.range_perm. intros.
          repeat (eapply Mem.perm_store_1; [eassumption|]).
          eapply Mem.perm_alloc_2; eauto.
        }
        destruct (Mem.range_perm_free _ _ _ _ HV7) as [m8 HFree].

        assert(Hfun: Genv.find_funct_ptr ge b = Some (Internal ept_invalidate_mappings_function)).
        {
          assert (Hmodule: get_module_function
                             ept_invalidate_mappings
                             (ept_invalidate_mappings ept_invalidate_mappings_function)
                           = OK (Some ept_invalidate_mappings_function)) by
              reflexivity.
          assert (HInternal: make_internal ept_invalidate_mappings_function
                             = OK (AST.Internal ept_invalidate_mappings_function)) by reflexivity.
          eapply make_globalenv_get_module_function in H0; eauto.
          destruct H0 as [?[Hsymbol´ ?]].
          inv Hstencil_matches.
          rewrite stencil_matches_symbols in Hsymbol´.
          rewrite H in Hsymbol´. inv Hsymbol´.
          assumption.
        }

        exploit Hget_CPU_ID; eauto.
        intros [[b_get_CPU_ID [HCPU_ID_symbol HCPU_ID_fun]] prim_get_CPU_ID].

        rewrite (Lregset_rewrite rs).
        refine_split´; try eassumption; try reflexivity.
        rewrite H1.
        econstructor; eauto.

        - one_step_forward´.
          {
            Lregset_simpl_tac.
            lift_trivial.
            change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
            change (Int.unsigned (Int.add Int.zero (Int.repr 20))) with 20.
            unfold set; simpl.
            rewrite HALC. simpl.
            rewrite HST1. simpl.
            rewrite HST2.
            reflexivity.
          }

          
          one_step_forward´.
          change (Int.add (Int.add Int.zero Int.one) Int.one) with (Int.repr 2).
          unfold symbol_offset. unfold fundef.
          rewrite HCPU_ID_symbol.
          Lregset_simpl_tac.

          eapply star_step; eauto.
          eapply (LAsm.exec_step_external _ b_get_CPU_ID); eauto.
          constructor_gen_sem_intro.
          simpl. econstructor; eauto.
          red. red. red. red. red. red.
          change positive with ident in ×.
          rewrite prim_get_CPU_ID.
          refine_split´; try reflexivity.
          econstructor; eauto.
          refine_split´; try reflexivity; try eassumption.
          simpl. repeat split.
          unfold get_CPU_ID_spec.
          unfold ObjMultiprocessor.get_CPU_ID_spec.
          simpl.
          subrewrite´.
          rewrite Int.unsigned_repr.
          reflexivity.
          inv Hhigh; omega.
          intros.
          unfold set; simpl.
          unfold lift; simpl.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
          inv H3; assumption.
          Lregset_simpl_tac.
          intro contra; discriminate contra.
          Lregset_simpl_tac.
          intro contra; discriminate contra.
          Lregset_simpl_tac.

          Require Import VCGen.
          one_step_forward´.
          unfold Int.mul.
          inv Hhigh.
          discharge_cmp.

          one_step_forward´.
          unfold Int.mul.
          unfold symbol_offset.
          inv Hstencil_matches.
          rewrite stencil_matches_symbols.
          rewrite Hsymbol.
          Opaque Z.mul Z.add.
          discharge_cmp.
          rewrite Z.add_0_r.
          Lregset_simpl_tac.


          Lregset_simpl_tac.
          one_step_forward´.
          {
            accessors_simpl.
            rewrite Hikern, Hihost.
            change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 0)))) with 0.
            rewrite HST3.
            reflexivity.
          }

          Lregset_simpl_tac.
          one_step_forward´.

          Lregset_simpl_tac.
          one_step_forward´.
          {
            accessors_simpl.
            rewrite Hikern, Hihost.
            change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 4)))) with 4.
            rewrite HST4.
            reflexivity.
          }

          Lregset_simpl_tac.
          one_step_forward´.
          {
            accessors_simpl.
            rewrite Hikern, Hihost.
            change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 8)))) with 8.
            rewrite HST5.
            reflexivity.
          }

          Lregset_simpl_tac.
          one_step_forward´.
          {
            accessors_simpl.
            rewrite Hikern, Hihost.
            change (Int.unsigned (Int.add Int.zero (Int.add Int.zero (Int.repr 12)))) with 12.
            rewrite HST6.
            reflexivity.
          }

          Lregset_simpl_tac.
          one_step_forward´.

          Lregset_simpl_tac.
          one_step_forward´.

          Lregset_simpl_tac.
          one_step_forward´.
          {
            lift_trivial.
            inv H2.
            change (Int.unsigned (Int.add Int.zero (Int.repr 16))) with 16.
            change (Int.unsigned (Int.add Int.zero (Int.repr 20))) with 20.
            unfold set; simpl.
            repeat(erewrite Mem.load_store_other; [|eassumption| simpl; right; right; omega]).
            erewrite Mem.load_store_same; eauto 1.
            erewrite register_type_load_result.

            repeat(erewrite Mem.load_store_other; [|eassumption | simpl; right; right; omega]).
            erewrite Mem.load_store_other; eauto 1.
            erewrite Mem.load_store_same; eauto 1.
            erewrite register_type_load_result.

            rewrite HFree. reflexivity.
            apply inv_reg_wt.
            right; left. simpl. omega.
            apply inv_reg_wt.
          }

          Lregset_simpl_tac.
          one_step_forward´.

          Lregset_simpl_tac.
          one_step_forward´.

          Lregset_simpl_tac.
          econstructor.
          reflexivity.
        - inv H2. inv inv_inject_neutral.
          eapply Mem.neutral_inject in inv_mem_inject_neutral.
          assert (HFB: b2 delta, Mem.flat_inj (Mem.nextblock m0) b2 Some (b1, delta)).
          {
            intros. unfold Mem.flat_inj.
            red; intros.
            destruct (plt b2 (Mem.nextblock m0)). inv H2.
            rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
            xomega. inv H2.
          }

          assert (HINJ: Mem.inject (mem:= mwd LDATAOps) (Mem.flat_inj (Mem.nextblock (mem:= mwd LDATAOps) (m0, d)))
                                   (m0, d) (m8, d)).
          {
            lift_unfold.
            split; trivial.
            eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b2 delta); apply HFB; trivial].
            repeat (eapply Mem.store_outside_inject; [ | | eassumption]
                    ; [|intros b2 delta; intros; specialize (HFB b2 delta); apply HFB; trivial]).
            eapply Mem.alloc_right_inject; eauto 1.
            eapply inv_mem_inject_neutral.
          }
          assumption.

        - simpl. rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST6); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST5); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST4); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
          rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC) ; eauto.
          clear. abstract xomega.
        - subst rs´0. Lregset_simpl_tac.
          unfold Lregset_fold; simpl.
          intros reg.
          repeat (rewrite Pregmap.gsspec).
          simpl_destruct_reg.
          exploit reg_false; try eassumption.
          intros HF. inv HF.
      Qed.

      Lemma ept_invalidate_mappings_code_correct:
        asm_spec_le (ept_invalidate_mappings ept_invalidate_mappings_spec_low)
                    (ept_invalidate_mappings ept_invalidate_mappings_function pproc).
      Proof.
        eapply asm_sem_intro; try reflexivity; simpl.
        intros. inv H.
        eapply make_program_make_globalenv in H0.
        exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
        intros Hstencil_matches.
        exploit ept_invalidate_mappings_spec; eauto 2.
        intros ( & m0´ & r_ & Hstep & Hincr & Hinject & Hnb & Hv).
        refine_split´; try eassumption; try reflexivity.
        esplit; reflexivity.
      Qed.

    End EPT_INVALIDATE_MAPPINGS.

  End WITHMEM.

End ASM_VERIFICATION.