Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import AsmImplLemma.
Require Import GenSem.

Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import Conventions.
Require Import VVMXIntro.
Require Import AbstractDataType.
Require Import mCertiKOSType.

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

Section SPECIFICATION.

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

  Notation LDATA := RData.

  Notation LDATAOps := (cdata (cdata_ops := pproc_data_ops) RData).

  Inductive vmx_get_reg_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmcs_get_reg_spec_low_intro s (WB: _ → Prop) m´0 labd reg res:
      vmx_get_reg_spec (Int.unsigned reg) labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_reg_spec_low_step s WB (Vint reg :: nil) (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_set_reg_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_set_reg_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ reg v:
      vmx_set_reg_spec (Int.unsigned reg) (Int.unsigned v) labd = Some labd´ →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_set_reg_spec_low_step s WB (Vint reg :: Vint v :: nil) (m´0, labd) Vundef (m´0, labd´).

  Inductive vmx_get_next_eip_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_next_eip_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_next_eip_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_next_eip_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_get_exit_qualification_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_exit_qualification_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_exit_qualification_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_exit_qualification_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_get_io_width_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_io_width_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_io_width_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_io_width_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_get_io_write_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_io_write_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_io_write_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_io_write_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_get_exit_io_rep_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_exit_io_rep_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_exit_io_rep_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_exit_io_rep_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_get_exit_io_str_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_exit_io_str_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_exit_io_str_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_exit_io_str_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_get_exit_io_port_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_get_exit_io_port_spec_low_intro s (WB: _ → Prop) m´0 labd res:
      vmx_get_exit_io_port_spec labd = Some (Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_get_exit_io_port_spec_low_step s WB nil (m´0, labd) (Vint res) (m´0, labd).

  Inductive vmx_set_mmap_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_set_mmap_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ gpa hpa mem_type res:
      vmx_set_mmap_spec (Int.unsigned gpa) (Int.unsigned hpa) (Int.unsigned mem_type) labd = Some (labd´, Int.unsigned res) →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_set_mmap_spec_low_step s WB (Vint gpa :: Vint hpa :: Vint mem_type :: nil) (m´0, labd) (Vint res) (m´0, labd´).

  Inductive vmx_init_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sextcall_sem (mem := mwd LDATAOps):=
  | vmx_init_spec_low_intro s (WB: _ → Prop) m´0 labd labd´ pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b:
      vmx_init_spec pml4ept_b stack_b idt_b msr_bitmap_b io_bitmap_b host_rip_b labd
      = Some labd´ →
      find_symbol s EPT_LOC = Some pml4ept_b →
      find_symbol s STACK_LOC = Some stack_b →
      find_symbol s idt_LOC = Some idt_b →
      find_symbol s msr_bitmap_LOC = Some msr_bitmap_b →
      find_symbol s io_bitmap_LOC = Some io_bitmap_b →
      find_symbol s vmx_return_from_guest = Some host_rip_b →
      kernel_mode labd →
      high_level_invariant labd →
      vmx_init_spec_low_step s WB nil (m´0, labd) Vundef (m´0, labd´).


  Inductive vmx_run_vm_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
    vm_run_spec_low_intro s m0 labd labd´ b (rs rs´: regset):
      find_symbol s vmx_run_vm = Some b →
      rs PC = Vptr b Int.zero →
      let rs01 := (Pregmap.init Vundef) #EDI <- (rs EDI) #EBP <- (rs EBP) in
      vm_run_spec rs01 labd = Some (labd´, rs´) →
      asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
      low_level_invariant (Mem.nextblock m0) labd →
      high_level_invariant labd →
      rs ESP ≠ Vundef →
      (∀ b1 o,
         rs ESP = Vptr b1 o →
         Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m0)) →
      let 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)) in
      vmx_run_vm_spec_low_step s rs (m0, labd) (rs0#EAX<- (rs´#EAX)#EBX <- (rs´#EBX)#EDX <- (rs´#EDX)
                                                   #ESI <- (rs´#ESI)#EDI <- (rs´#EDI)#EBP <- (rs´#EBP)
                                                   #PC <- (rs´#RA)) (m0, labd´).



  Inductive vmx_return_from_guest_spec_low_step `{StencilOps} `{Mem.MemoryModelOps} `{UseMemWithData mem}:
    sprimcall_sem (mem := mwd LDATAOps):=
  | vmx_return_from_guest_low_intro s m0 labd labd´ rs b:
      find_symbol s vmx_return_from_guest = Some b →
      rs PC = Vptr b Int.zero →
      rs ESP ≠ Vundef →
      (∀ b1 o,
         rs ESP = Vptr b1 o →
         Ple (genv_next s) b1 ∧ Plt b1 (Mem.nextblock m0)) →
      vmx_return_from_guest_spec labd = Some labd´ →
      asm_invariant (mem := mwd LDATAOps) s rs (m0, labd) →
      low_level_invariant (Mem.nextblock m0) labd →
      high_level_invariant labd →
      let rs0 := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
                             (undef_regs (List.map preg_of destroyed_at_call) rs)) in
      vmx_return_from_guest_spec_low_step
        s rs (m0, labd) (rs0#PC <- (Vptr b (Int.repr 3))) (m0, labd´).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.

    Definition vmx_get_reg_spec_low: compatsem LDATAOps :=
      csem vmx_get_reg_spec_low_step (type_of_list_type (Tint32::nil)) Tint32.

    Definition vmx_set_reg_spec_low: compatsem LDATAOps :=
      csem vmx_set_reg_spec_low_step (type_of_list_type (Tint32::Tint32::nil)) Tvoid.

    Definition vmx_get_next_eip_spec_low: compatsem LDATAOps :=
      csem vmx_get_next_eip_spec_low_step Tnil Tint32.

    Definition vmx_get_exit_qualification_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_qualification_spec_low_step Tnil Tint32.

    Definition vmx_get_io_width_spec_low: compatsem LDATAOps :=
      csem vmx_get_io_width_spec_low_step Tnil Tint32.

    Definition vmx_get_io_write_spec_low: compatsem LDATAOps :=
      csem vmx_get_io_write_spec_low_step Tnil Tint32.

    Definition vmx_get_exit_io_rep_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_io_rep_spec_low_step Tnil Tint32.

    Definition vmx_get_exit_io_str_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_io_str_spec_low_step Tnil Tint32.

    Definition vmx_get_exit_io_port_spec_low: compatsem LDATAOps :=
      csem vmx_get_exit_io_port_spec_low_step Tnil Tint32.

    Definition vmx_set_mmap_spec_low: compatsem LDATAOps :=
      csem vmx_set_mmap_spec_low_step (type_of_list_type (Tint32::Tint32::Tint32::nil)) Tint32.

    Definition vmx_init_spec_low: compatsem LDATAOps :=
      csem vmx_init_spec_low_step Tnil Tvoid.

    Definition vmx_run_vm_spec_low: compatsem LDATAOps :=
      asmsem vmx_run_vm vmx_run_vm_spec_low_step.

    Definition vmx_return_from_guest_spec_low: compatsem LDATAOps :=
      asmsem vmx_return_from_guest vmx_return_from_guest_spec_low_step.

  End WITHMEM.

End SPECIFICATION.