Library mcertikos.trap.SysCallGenAsm2


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 TDispatch.
Require Import TSysCall.
Require Import SysCallGenAsmSource.
Require Import SysCallGenAsmData.
Require Import SysCallGenSpec.

Require Import LRegSet.
Require Import AbstractDataType.

Require Import GlobalOracleProp.
Require Import SingleOracle.

Require Import LAsmModuleSemSpec.

Section ASM_VERIFICATION.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.

  Local Open Scope Z_scope.

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

  Notation LDATA := RData.
  Notation LDATAOps := (cdata (cdata_ops := pipcintro_data_ops) 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}.


    Lemma sys_run_vm_proof:
       ge (s: stencil) (rs: regset) m labd labd0 labd´ rs01 rs0 rs´ rs2 v0 v1 v2 v3 v5 v6
             v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 v7 vargs sg b
             (HUEIP_cond: v12 Int.repr 0),
        make_globalenv s (sys_run_vm sys_run_vm_function) tdispatch = ret ge

        trap_into_kernel_spec sys_run_vm s m rs labd labd0 vargs sg b
                              v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16

        rs01 = (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP)
        thread_vm_run_spec rs01 labd0 = Some (labd´, rs´)

        rs0 = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: RA :: nil)
                          (undef_regs (List.map preg_of destroyed_at_call) rs))

        rs2 = (rs0#EAX<- (rs´#EAX)#EBX <- (rs´#EBX)#EDX <- (rs´#EDX)
                  #ESI <- (rs´#ESI)#EDI <- (rs´#EDI)#EBP <- (rs´#EBP)
                  #PC <- (rs´#RA))

        asm_invariant (mem := mwd LDATAOps) s rs (m, labd)
        high_level_invariant labd
        low_level_invariant (Mem.nextblock m) labd

         r_: regset,
          lasm_step (sys_run_vm sys_run_vm_function) (tdispatch (Hmwd:= Hmwd) (Hmem:= Hmem))
                    sys_run_vm s rs (m, labd) r_ (m, labd´)
           ( l,
                Val.lessdef (Pregmap.get l rs2)
                            (Pregmap.get l r_)).
    Proof.
      intros. destruct H0 as [Hv [Hsg[Harg[Hsym[HPC[Hex [HESP HESP_STACK]]]]]]]. subst.
      exploit Hexit; eauto.
      intros [[b_exit [Hexit_symbol Hexit_fun]] prim_exit].
      exploit Hrun_vm; eauto.
      intros [[b_check [Hcheck_symbol Hcheck_fun]] prim_check].

      exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
      intros Hstencil_matches.

      exploit Hsys_run_vm; eauto 2. intros Hfunct.

      assert (Hblock: b0 o,
                        rs ESP = Vptr b0 oPle (Genv.genv_next ge) b0 Plt b0 (Mem.nextblock m)).
      {
        intros. exploit HESP_STACK; eauto.
        inv Hstencil_matches.
        rewrite stencil_matches_genv_next.
        trivial.
      }
      clear HESP_STACK.

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

      one_step_forward´.
      Lregset_simpl_tac.
      unfold symbol_offset. unfold fundef.
      rewrite Hexit_symbol.

      econstructor; eauto 1.
      eapply (LAsm.exec_step_prim_call _ b_exit); eauto.

      econstructor; eauto 1.
      instantiate (4:= proc_exit_user).
      change positive with ident in ×.
      rewrite prim_exit.
      refine_split´; try reflexivity.
      econstructor; eauto 1.
      refine_split´; try reflexivity; try eassumption.
      simpl. econstructor; try eassumption; try reflexivity.
      {
        intros b1 o rsESP.
        rewrite <- (stencil_matches_genv_next _ _ Hstencil_matches).
        apply Hblock with o.
        exact rsESP.
      }

      inv Harg.
      constructor; eauto 1;
      repeat match goal with
               | [H0: extcall_arg _ _ _ _ |- extcall_arg _ _ _ _] ⇒ inv H0; econstructor; [reflexivity| eassumption]
               | [H1: list_forall2 _ _ _ |- list_forall2 _ _ _] ⇒ inv H1; constructor
               | H1: list_forall2 _ _ _ |- _inv H1
             end.
      inv Hstencil_matches. erewrite <- stencil_matches_symbols; eassumption.
      Lregset_simpl_tac.

      one_step_forward´.
      Lregset_simpl_tac.
      unfold symbol_offset. unfold fundef.
      rewrite Hcheck_symbol.

      eapply star_one; eauto.
      eapply (LAsm.exec_step_prim_call _ b_check); eauto 1.
      econstructor; eauto 1.
      instantiate (4:= vmx_run_vm).
      change positive with ident in ×.
      rewrite prim_check.
      refine_split´; try reflexivity.
      econstructor; eauto 1.
      simpl.

      assert (HUCTX: r, Val.has_type (rs´ r) Tint
                                val_inject (Mem.flat_inj (Mem.nextblock m))
                                             (rs´ r) (rs´ r)).
      {
        eapply sys_run_vm_generate; eauto.
      }
      econstructor; try eassumption; try reflexivity;
      try eapply HUCTX.
      erewrite <- stencil_matches_symbols; eassumption.

      Lregset_simpl_tac.
      intros. specialize (Hblock _ _ H0).
      erewrite <- stencil_matches_genv_next; eassumption.

      reflexivity.

      Lregset_simpl_tac.
      simpl.
      Lregset_simpl_tac.
      intros reg.
      unfold Lregset_fold; simpl.
      repeat (rewrite Pregmap.gsspec).
      simpl_destruct_reg.
      exploit reg_false; try eassumption.
      intros HF. inv HF.
    Qed.

    Lemma sys_run_vm_code_correct:
      asm_spec_le (sys_run_vm sys_run_vm_spec_low)
                  (sys_run_vm sys_run_vm_function tdispatch).
    Proof.
      eapply asm_sem_intro; try reflexivity.
      intros. inv H.
      eapply make_program_make_globalenv in H0.
      exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
      intros Hstencil_matches.
      assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal sys_run_vm_function)).
      {
        assert (Hmodule: get_module_function sys_run_vm (sys_run_vm sys_run_vm_function) = OK (Some sys_run_vm_function)) by
            reflexivity.
        assert (HInternal: make_internal sys_run_vm_function = OK (AST.Internal sys_run_vm_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.
        destruct H2 as [_ [_[_[Hsym _]]]].
        rewrite Hsym in Hsymbol. inv Hsymbol.
        assumption.
      }

      exploit sys_run_vm_proof; eauto 2.
      intros HW. exploit HW; eauto 2.

      intros [r_[Hstep Hv]].
      assert (Hle: (Mem.nextblock m0 Mem.nextblock m0)%positive).
      {
        reflexivity.
      }

      refine_split´; try eassumption; try reflexivity.
      - inv H7. inv inv_inject_neutral.
        lift_unfold. split; try reflexivity.
        eapply Mem.neutral_inject. assumption.
      - esplit; reflexivity.
    Qed.






    Ltac accessors_simpl:=
      match goal with
        | |- exec_storeex _ _ _ _ _ _ _ = _
          unfold exec_storeex, LoadStoreSem3high.exec_storeex3high;
            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, LoadStoreSem3high.exec_loadex3high;
            simpl; Lregset_simpl_tac;
            match goal with
              | |- context[Asm.exec_load _ _ _ _ _ _ ] ⇒
                unfold Asm.exec_load; simpl;
                Lregset_simpl_tac; lift_trivial
            end
      end.

      Lemma pgf_handler_spec:
         ge (s: stencil) (rs: regset) m labd labd0 labd1 labd´ rs0 vadr rs´ v0 v1 v2 v3 v5 v6
               v8 v9 v10 v11 v12 v13 v14 v15 v16 v4 v7 vargs sg b
             (HUEIP_cond: v12 Int.repr 0),
          make_globalenv s (pgf_handler pgf_handler_function) tdispatch = ret ge
          

          syscall_spec pgf_handler s m rs rs´ rs0 labd labd0 labd1 labd´ vargs sg b
                       v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16

          
          
          vadr = fst (ti labd0) →
          ptfault_resv_spec (Int.unsigned vadr) labd0 = Some labd1

          asm_invariant (mem := mwd LDATAOps) s rs (m, labd)
          
          low_level_invariant (Mem.nextblock m) labd

           m0´ r_,
            lasm_step (pgf_handler pgf_handler_function) (tdispatch (Hmwd:= Hmwd) (Hmem:= Hmem))
                      pgf_handler s rs
                      (m, labd) r_ (m0´, labd´)
             inject_incr (Mem.flat_inj (Mem.nextblock m))
             Memtype.Mem.inject m m0´
             (Mem.nextblock m Mem.nextblock m0´)%positive
             ( l,
                  Val.lessdef (Pregmap.get l rs0)
                              (Pregmap.get l r_)).
      Proof.
        intros.

        caseEq(Mem.alloc m 0 12).
        intros m1 b0 HALC.
        exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
        intros Hstencil_matches.

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

        destruct H0 as [Hk[Hst [Hr _]]]. subst.
        destruct Hk as [Hv [Hsg[Harg[Hsym[HPC[Hex [HESP HESP_STACK]]]]]]]. subst.

        assert (HOS´: 0 64 Int.max_unsigned) by rewrite_omega.

        exploit Hstart; eauto.
        intros [[b_start [Hstart_symbol Hstart_fun]] prim_start].
        exploit Hexit; eauto.
        intros [[b_exit [Hexit_symbol Hexit_fun]] prim_exit].
        exploit Hget; eauto.
        intros [[b_check [Hcheck_symbol Hcheck_fun]] prim_check].
        exploit Hpgfr; eauto.
        intros [[b_pgfr [Hpgfr_symbol Hpgfr_fun]] prim_pgfr].

        specialize (Mem.valid_access_alloc_same _ _ _ _ _ HALC). intros.
        assert (HV1: Mem.valid_access m1 Mint32 b0 4 Freeable).
        {
          eapply H0; auto; simpl; try omega.
          apply Z.divide_refl.
        }
        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 b0 8 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply H0; auto; simpl; try omega.
          unfold Z.divide.
           2; omega.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV2; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ Vundef HV2) as [m3 HST2].

        assert (HV3: Mem.valid_access m3 Mint32 b0 0 Freeable).
        {
          eapply Mem.store_valid_access_1; eauto.
          eapply Mem.store_valid_access_1; eauto.
          eapply H0; auto; simpl; try omega.
          apply Zdivide_0.
        }
        eapply Mem.valid_access_implies with (p2:= Writable) in HV3; [|constructor].
        destruct (Mem.valid_access_store _ _ _ _ (Vint (fst (ti labd0))) HV3) as [m4 HST3].

        assert(Hnextblock4: Mem.nextblock m4 = Mem.nextblock m1).
        {
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST3); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST2); trivial.
          rewrite (Mem.nextblock_store _ _ _ _ _ _ HST1); trivial.
        }

        assert (HV4: Mem.range_perm m4 b0 0 12 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 _ _ _ _ HV4) as [m5 HFree].

        assert (HUCTX: ikern labd0 = true
                        ihost labd0 = true
                       /\( i, 0 i < UCTXT_SIZE
                                    let v:= (ZMap.get i rs´) in
                                    Val.has_type v Tint
                                     val_inject (Mem.flat_inj (Mem.nextblock m5)) v v)).
        {
          eapply pgf_handler_generate; eauto.
          intros. subst v.
          inv_proc; try (split; constructor).
          rewrite ZMap.gi.
          split; constructor.
        }
        destruct HUCTX as [ik[ih HUCTX]].

        exploit Hpgf_handler; eauto 2. intros Hfunct.

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

        one_step_forward´.
        Lregset_simpl_tac.
        unfold symbol_offset. unfold fundef.
        rewrite Hexit_symbol.

        econstructor; eauto 1.
        eapply (LAsm.exec_step_prim_call _ b_exit); eauto.

        econstructor; eauto 1.
        instantiate (4:= proc_exit_user).
        change positive with ident in ×.
        rewrite prim_exit.
        refine_split´; try reflexivity.
        econstructor; eauto 1.
        refine_split´; try reflexivity; try eassumption.
        simpl. econstructor; try eassumption; try reflexivity.

        inv Harg.
        constructor; eauto 1;
        repeat match goal with
                 | [H0: extcall_arg _ _ _ _ |- extcall_arg _ _ _ _] ⇒ inv H0; econstructor; [reflexivity| eassumption]
                 | [H1: list_forall2 _ _ _ |- list_forall2 _ _ _] ⇒ inv H1; constructor
                 | H1: list_forall2 _ _ _ |- _inv H1
               end.
        inv Hstencil_matches. erewrite <- stencil_matches_symbols; eassumption.
        Lregset_simpl_tac.

        one_step_forward´.
        Lregset_simpl_tac.
        lift_trivial.
        unfold set; simpl.
        rewrite HALC. simpl.
        change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
        change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
        rewrite HST1. simpl.
        rewrite HST2.
        reflexivity.
        Lregset_simpl_tac.

        one_step_forward´.
        unfold symbol_offset. unfold fundef.
        rewrite Hcheck_symbol.
        Lregset_simpl_tac.

        econstructor; eauto.
        eapply (LAsm.exec_step_prim_call _ b_check); eauto 1.
        econstructor; eauto 1.
        instantiate (4:= trap_get).
        change positive with ident in ×.
        rewrite prim_check.
        refine_split´; try reflexivity.
        econstructor; eauto. simpl.
        econstructor; eauto.
        Lregset_simpl_tac.
        unfold thread_trap_info_get_spec.
        unfold ObjCPU.trap_info_get_spec.

        one_step_forward´.
        unfold exec_storeex, LoadStoreSem3high.exec_storeex3high.
        simpl; Lregset_simpl_tac. rewrite ik, ih.
        unfold Asm.exec_store; simpl.
        Lregset_simpl_tac. lift_trivial.
        change (Int.unsigned (Int.add Int.zero (Int.add Int.zero Int.zero))) with 0.
        rewrite HST3. reflexivity.
        unfold set; simpl.

        one_step_forward´.
        unfold symbol_offset. unfold fundef.
        rewrite Hpgfr_symbol.
        Lregset_simpl_tac.

        econstructor; eauto.
        eapply (LAsm.exec_step_external _ b_pgfr); eauto 1.
        econstructor; eauto.
        econstructor; eauto. simpl; lift_trivial.
        erewrite Mem.load_store_same; eauto.
        constructor; trivial.

        econstructor; eauto 1.
        red. red. red. red. red. red.
        change positive with ident in ×.
        rewrite prim_pgfr.
        refine_split´; try reflexivity.
        econstructor; eauto 1.
        refine_split´; try reflexivity; try eassumption.
        constructor_gen_sem_intro.

        Lregset_simpl_tac.
        lift_trivial.
        intros. inv H1.
        rewrite Hnextblock4; assumption.

        discriminate.
        discriminate.

        Lregset_simpl_tac.

        one_step_forward´.
        lift_trivial.
        change (Int.unsigned (Int.add Int.zero (Int.repr 4))) with 4.
        change (Int.unsigned (Int.add Int.zero (Int.repr 8))) with 8.
        unfold set; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_same; eauto.

        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_other; eauto; simpl.
        erewrite Mem.load_store_same; eauto.
        erewrite register_type_load_result.

        rewrite HFree. reflexivity.
        inv H3.
        apply inv_reg_wt.
        right. left. omega.
        right. right. omega.
        right. right. omega.
        Lregset_simpl_tac.

        one_step_forward´.
        Lregset_simpl_tac.
        unfold symbol_offset. unfold fundef.
        rewrite Hstart_symbol.

        eapply star_one; eauto.
        eapply (LAsm.exec_step_prim_call _ b_start); eauto 1.
        econstructor; eauto 1.
        instantiate (4:= proc_start_user).
        change positive with ident in ×.
        rewrite prim_start.
        refine_split´; try reflexivity.
        econstructor; eauto 1.
        refine_split´; try reflexivity; try eassumption.
        simpl.
        econstructor; try eassumption; try reflexivity.
        eapply HUCTX.
        eapply HUCTX.

        inv Hstencil_matches. erewrite <- stencil_matches_symbols; eassumption.

        intros contra.
        erewrite <- pgf_handler_ueip_value in contra; eauto.
        rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
        rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
        rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
        rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
        rewrite ZMap.gss in contra.
        elim HUEIP_cond.
        inv contra; auto.

        intros contra.
        erewrite <- pgf_handler_ueip_value in contra; eauto.
        rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
        rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
        rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
        rewrite ZMap.gso in contra; [ | intro contra´; inv contra´].
        rewrite ZMap.gss in contra.
        inv contra.

        reflexivity.
        reflexivity.

        assert (HFB: b1 delta, Mem.flat_inj (Mem.nextblock m) b1 Some (b0, delta)).
        {
          intros. unfold Mem.flat_inj.
          red; intros.
          destruct (plt b1 (Mem.nextblock m)). inv H1.
          rewrite (Mem.alloc_result _ _ _ _ _ HALC) in p.
          xomega. inv H1.
        }
        eapply Mem.free_right_inject; eauto 1; [|intros; specialize (HFB b1 delta); apply HFB; trivial].
        repeat (eapply Mem.store_outside_inject; [ | | eassumption]
                ; [|intros b1 delta; intros; specialize (HFB b1 delta); apply HFB; trivial]).
        eapply Mem.alloc_right_inject; eauto 1.
        inv H3. inv inv_inject_neutral.
        apply Mem.neutral_inject; trivial.

        rewrite (Mem.nextblock_free _ _ _ _ _ HFree); trivial.
        rewrite Hnextblock4.
        rewrite (Mem.nextblock_alloc _ _ _ _ _ HALC); eauto.
        clear. abstract xomega.

        Lregset_simpl_tac.
        simpl.
        Lregset_simpl_tac.
        intros reg.
        unfold Lregset_fold; simpl.
        repeat (rewrite Pregmap.gsspec).
        simpl_destruct_reg.
        constructor.
      Qed.

    Lemma pgf_handler_code_correct:
      asm_spec_le (pgf_handler pagefault_handler_spec_low)
                  (pgf_handler pgf_handler_function tdispatch).
    Proof.
      eapply asm_sem_intro; try reflexivity.
      intros. inv H.
      eapply make_program_make_globalenv in H0.
      exploit (make_globalenv_stencil_matches (D:= LDATAOps)); eauto.
      intros Hstencil_matches.
      assert(Hfun: Genv.find_funct_ptr (Genv.globalenv p) b = Some (Internal pgf_handler_function)).
      {
        assert (Hmodule: get_module_function pgf_handler (pgf_handler pgf_handler_function) = OK (Some pgf_handler_function)) by
            reflexivity.
        assert (HInternal: make_internal pgf_handler_function = OK (AST.Internal pgf_handler_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.
        destruct H2 as [Hk _]. subst.
        destruct Hk as [_ [_[_[Hsym _]]]].
        rewrite Hsym in Hsymbol. inv Hsymbol.
        assumption.
      }
      
      exploit pgf_handler_spec; eauto 2. intros HW. exploit HW; eauto 2.
      intros ( & m0´ & r_ & Hstep & Hincr & Hv & Hnext & HV).
      refine_split´; try eassumption; try reflexivity.
      - lift_unfold. split; [assumption| reflexivity].
      - esplit; reflexivity.
    Qed.

  End WITHMEM.

End ASM_VERIFICATION.