Library mcertikos.trap.TTrapCodeLemma26

Require Import TacticsForTesting.
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 Clight.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Ctypes.
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 DispatchGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import XOmega.
Require Import TTrapCSource.
Require Import AbstractDataType.
Require Import ObjArg.
Require Import ObjTrap.
Require Import ObjSyncIPC.
Require Export TrapPrimSemantics.
Require Import CommonTactic.
Require Import GlobalOracleProp.
Require Import ObjTMINTELVIRT.
Require Import ObjTMIPCDEVPRIM.
Require Import ObjTMVMM.
Require Import ObjTMSCHED.
Require Import SingleOracle.

Module TTRAPCODE.

  Section WithPrimitives.

    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.
    Context `{single_oracle_prop: SingleOracleProp}.
    Context `{real_params : RealParams}.
    Context `{multi_oracle_prop: MultiOracleProp}.

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

    Section SYSCALLDISPATCHC.

      Let L: compatlayer (cdata RData) := sys_proc_create ↦ trap_proccreate_compatsem trap_proc_create_spec
                                                           ⊕ sys_get_quota ↦ gensem trap_get_quota_spec
                                                           ⊕ sys_inject_event ↦ gensem trap_inject_event_spec
                                                           ⊕ sys_check_int_shadow ↦ gensem trap_check_int_shadow_spec
                                                           ⊕ sys_check_pending_event ↦ gensem trap_check_pending_event_spec
                                                           ⊕ sys_intercept_int_window ↦ gensem trap_intercept_int_window_spec
                                                           ⊕ sys_get_next_eip ↦ gensem trap_get_next_eip_spec
                                                           ⊕ sys_get_reg ↦ gensem trap_get_reg_spec
                                                           ⊕ sys_set_reg ↦ gensem trap_set_reg_spec
                                                           ⊕ sys_set_seg1 ↦ gensem trap_set_seg1_spec
                                                           ⊕ sys_set_seg2 ↦ gensem trap_set_seg2_spec
                                                           ⊕ sys_get_tsc_offset ↦ gensem trap_get_tsc_offset_spec
                                                           ⊕ sys_set_tsc_offset ↦ gensem trap_set_tsc_offset_spec
                                                           ⊕ sys_get_exitinfo ↦ gensem trap_get_exitinfo_spec
                                                           ⊕ sys_handle_rdmsr ↦ gensem trap_handle_rdmsr_spec
                                                           ⊕ sys_handle_wrmsr ↦ gensem trap_handle_wrmsr_spec
                                                           ⊕ sys_mmap ↦ gensem trap_mmap_spec
                                                           ⊕ sys_receive_chan ↦ gensem trap_receivechan_spec
                                                           ⊕ sys_sendto_chan ↦ gensem trap_sendtochan_spec
                                                           ⊕ thread_yield ↦ gensem big2_thread_yield_spec
                                                           ⊕ sys_getc ↦ gensem sys_getc_spec
                                                           ⊕ sys_putc ↦ gensem sys_putc_spec
                                                           ⊕ uctx_arg1 ↦ gensem uctx_arg1_spec
                                                           ⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec.

      Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.

      Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

      Section SyscallDispatchCBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bsys_proc_create: block.

        Hypothesis hsys_proc_create1 : Genv.find_symbol ge sys_proc_create = Some bsys_proc_create.

        Hypothesis hsys_proc_create2 : Genv.find_funct_ptr ge bsys_proc_create = Some (External (EF_external sys_proc_create (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_quota: block.

        Hypothesis hsys_get_quota1 : Genv.find_symbol ge sys_get_quota = Some bsys_get_quota.

        Hypothesis hsys_get_quota2 : Genv.find_funct_ptr ge bsys_get_quota = Some (External (EF_external sys_get_quota (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_inject_event: block.

        Hypothesis hsys_inject_event1 : Genv.find_symbol ge sys_inject_event = Some bsys_inject_event.

        Hypothesis hsys_inject_event2 : Genv.find_funct_ptr ge bsys_inject_event = Some (External (EF_external sys_inject_event (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_check_int_shadow: block.

        Hypothesis hsys_check_int_shadow1 : Genv.find_symbol ge sys_check_int_shadow = Some bsys_check_int_shadow.

        Hypothesis hsys_check_int_shadow2 : Genv.find_funct_ptr ge bsys_check_int_shadow = Some (External (EF_external sys_check_int_shadow (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_check_pending_event: block.

        Hypothesis hsys_check_pending_event1 : Genv.find_symbol ge sys_check_pending_event = Some bsys_check_pending_event.

        Hypothesis hsys_check_pending_event2 : Genv.find_funct_ptr ge bsys_check_pending_event = Some (External (EF_external sys_check_pending_event (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_intercept_int_window: block.

        Hypothesis hsys_intercept_int_window1 : Genv.find_symbol ge sys_intercept_int_window = Some bsys_intercept_int_window.

        Hypothesis hsys_intercept_int_window2 : Genv.find_funct_ptr ge bsys_intercept_int_window = Some (External (EF_external sys_intercept_int_window (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_next_eip: block.

        Hypothesis hsys_get_next_eip1 : Genv.find_symbol ge sys_get_next_eip = Some bsys_get_next_eip.

        Hypothesis hsys_get_next_eip2 : Genv.find_funct_ptr ge bsys_get_next_eip = Some (External (EF_external sys_get_next_eip (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_reg: block.

        Hypothesis hsys_get_reg1 : Genv.find_symbol ge sys_get_reg = Some bsys_get_reg.

        Hypothesis hsys_get_reg2 : Genv.find_funct_ptr ge bsys_get_reg = Some (External (EF_external sys_get_reg (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_set_reg: block.

        Hypothesis hsys_set_reg1 : Genv.find_symbol ge sys_set_reg = Some bsys_set_reg.

        Hypothesis hsys_set_reg2 : Genv.find_funct_ptr ge bsys_set_reg = Some (External (EF_external sys_set_reg (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_set_seg1: block.

        Hypothesis hsys_set_seg11 : Genv.find_symbol ge sys_set_seg1 = Some bsys_set_seg1.

        Hypothesis hsys_set_seg12 : Genv.find_funct_ptr ge bsys_set_seg1 = Some (External (EF_external sys_set_seg1 (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_set_seg2: block.

        Hypothesis hsys_set_seg21 : Genv.find_symbol ge sys_set_seg2 = Some bsys_set_seg2.

        Hypothesis hsys_set_seg22 : Genv.find_funct_ptr ge bsys_set_seg2 = Some (External (EF_external sys_set_seg2 (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_tsc_offset: block.

        Hypothesis hsys_get_tsc_offset1 : Genv.find_symbol ge sys_get_tsc_offset = Some bsys_get_tsc_offset.

        Hypothesis hsys_get_tsc_offset2 : Genv.find_funct_ptr ge bsys_get_tsc_offset = Some (External (EF_external sys_get_tsc_offset (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_set_tsc_offset: block.

        Hypothesis hsys_set_tsc_offset1 : Genv.find_symbol ge sys_set_tsc_offset = Some bsys_set_tsc_offset.

        Hypothesis hsys_set_tsc_offset2 : Genv.find_funct_ptr ge bsys_set_tsc_offset = Some (External (EF_external sys_set_tsc_offset (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_get_exitinfo: block.

        Hypothesis hsys_get_exitinfo1 : Genv.find_symbol ge sys_get_exitinfo = Some bsys_get_exitinfo.

        Hypothesis hsys_get_exitinfo2 : Genv.find_funct_ptr ge bsys_get_exitinfo = Some (External (EF_external sys_get_exitinfo (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_handle_rdmsr: block.

        Hypothesis hsys_handle_rdmsr1 : Genv.find_symbol ge sys_handle_rdmsr = Some bsys_handle_rdmsr.

        Hypothesis hsys_handle_rdmsr2 : Genv.find_funct_ptr ge bsys_handle_rdmsr = Some (External (EF_external sys_handle_rdmsr (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_handle_wrmsr: block.

        Hypothesis hsys_handle_wrmsr1 : Genv.find_symbol ge sys_handle_wrmsr = Some bsys_handle_wrmsr.

        Hypothesis hsys_handle_wrmsr2 : Genv.find_funct_ptr ge bsys_handle_wrmsr = Some (External (EF_external sys_handle_wrmsr (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_mmap: block.

        Hypothesis hsys_mmap1 : Genv.find_symbol ge sys_mmap = Some bsys_mmap.

        Hypothesis hsys_mmap2 : Genv.find_funct_ptr ge bsys_mmap = Some (External (EF_external sys_mmap (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_receive_chan: block.

        Hypothesis hsys_receive_chan1 : Genv.find_symbol ge sys_receive_chan = Some bsys_receive_chan.

        Hypothesis hsys_receive_chan2 : Genv.find_funct_ptr ge bsys_receive_chan = Some (External (EF_external sys_receive_chan (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_sendto_chan: block.

        Hypothesis hsys_sendto_chan1 : Genv.find_symbol ge sys_sendto_chan = Some bsys_sendto_chan.

        Hypothesis hsys_sendto_chan2 : Genv.find_funct_ptr ge bsys_sendto_chan = Some (External (EF_external sys_sendto_chan (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bthread_yield: block.

        Hypothesis hthread_yield1 : Genv.find_symbol ge thread_yield = Some bthread_yield.

        Hypothesis hthread_yield2 : Genv.find_funct_ptr ge bthread_yield = Some (External (EF_external thread_yield (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_getc: block.

        Hypothesis hsys_getc1 : Genv.find_symbol ge sys_getc = Some bsys_getc.

        Hypothesis hsys_getc2 : Genv.find_funct_ptr ge bsys_getc = Some (External (EF_external sys_getc (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable bsys_putc: block.

        Hypothesis hsys_putc1 : Genv.find_symbol ge sys_putc = Some bsys_putc.

        Hypothesis hsys_putc2 : Genv.find_funct_ptr ge bsys_putc = Some (External (EF_external sys_putc (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).

        Variable buctx_arg1: block.

        Hypothesis huctx_arg11 : Genv.find_symbol ge uctx_arg1 = Some buctx_arg1.

        Hypothesis huctx_arg12 : Genv.find_funct_ptr ge buctx_arg1 = Some (External (EF_external uctx_arg1 (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_set_errno: block.

        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.

        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno = Some (External (EF_external uctx_set_errno (signature_of_type (Tcons tint Tnil) tvoid cc_default)) (Tcons tint Tnil) tvoid cc_default).

        Lemma NSYS_HANDLE_RDMSR_correct: ∀ m d d´ le z,
            trap_handle_rdmsr_spec d = Some d´ →
            uctx_arg1_spec d = Some z →
            Syscall_Z2Num z = NSYS_HANDLE_RDMSR →
            ∃ le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

      End SyscallDispatchCBody.

    End SYSCALLDISPATCHC.

  End WithPrimitives.

End TTRAPCODE.