Library mcertikos.driver.CertiKOS

Dependencies for extraction
Require Import Coqlib.
Require Wfsimpl.
Require AST.
Require Iteration.
Require Floats.
Require SelectLong.
Require RTLgen.
Require Inlining.
Require ValueDomain.
Require Tailcall.
Require Allocation.
Require Ctypes.
Require Csyntax.
Require Int31.
CompCertX:test-compcert-param-memory instantiations of extractees with concrete memory model
Require InitializersImpl.
Require Import mcertikos.driver.CertiKOSImpl.

Require Import liblayers.compcertx.ErrorMonad.
Require Import liblayers.logic.Modules.
Require Import liblayers.logic.Layers.
Require Import String.

Require Import mcertikos.clib.CDataTypes.

Require Import mcertikos.ticketlog.CurIDGenLinkSource.
Require Import mcertikos.ticketlog.TicketLockIntroGenLinkSource.
Require Import mcertikos.ticketlog.TicketLockOpGenLinkSource.
Require Import mcertikos.ticketlog.QTicketLockOpGenLinkSource.
Require Import mcertikos.ticketlog.HTicketLockOpGenLinkSource.
Require Import mcertikos.ticketlog.QTicketLockGenLinkSource.

Require Import mcertikos.devdrivers.ConsoleBuffIntroGenLinkSource.
Require Import mcertikos.devdrivers.AbsConsoleBuffIntroGenLinkSource.
Require Import mcertikos.devdrivers.SerialIntroGenLinkSource.
Require Import mcertikos.devdrivers.SerialGenLinkSource.
Require Import mcertikos.devdrivers.IoApicGenLinkSource.
Require Import mcertikos.devdrivers.LApicGenLinkSource.
Require Import mcertikos.devdrivers.ConsoleGenLinkSource.
Require Import mcertikos.devdrivers.HandlerIntroGenLinkSource.
Require Import mcertikos.devdrivers.HandlerSwGenLinkSource.
Require Import mcertikos.devdrivers.HandlerAsmGenLinkSource.
Require Import mcertikos.devdrivers.HandlerCxtGenLinkSource.
Require Import mcertikos.devdrivers.HandlerOpGenLinkSource.
Require Import mcertikos.devdrivers.HandlerGenLinkSource.
Require Import mcertikos.devdrivers.AbsHandlerGenLinkSource.

Require Import mcertikos.mm.ContainerIntroGenLinkSource.
Require Import mcertikos.mm.ContainerGenLinkSource.
Require Import mcertikos.mm.ALInitGenLinkSource.
Require Import mcertikos.mm.ALOpGenLinkSource.
Require Import mcertikos.mm.ALGenLinkSource.
Require Import mcertikos.mm.ALHGenLinkSource.
Require Import mcertikos.mm.PTIntroGenLinkSource.
Require Import mcertikos.mm.PTOpGenLinkSource.
Require Import mcertikos.mm.PTCommGenLinkSource.
Require Import mcertikos.mm.PTKernGenLinkSource.
Require Import mcertikos.mm.PTInitGenLinkSource.
Require Import mcertikos.mm.PTNewGenLinkSource.
Require Import mcertikos.mm.ShareIntroGenLinkSource.
Require Import mcertikos.mm.ShareOpGenLinkSource.
Require Import mcertikos.mm.ShareGenLinkSource.

Require Import mcertikos.proc.KContextGenLinkSource.
Require Import mcertikos.proc.KContextNewGenLinkSource.
Require Import mcertikos.proc.SleeperGenLinkSource.
Require Import mcertikos.proc.QueueIntroGenLinkSource.
Require Import mcertikos.proc.QueueInitGenLinkSource.
Require Import mcertikos.proc.AbQueueAtomicGenLinkSource.
Require Import mcertikos.proc.CVIntroGenLinkSource.
Require Import mcertikos.proc.CVOpGenLinkSource.
Require Import mcertikos.proc.ThreadSchedGenLinkSource.
Require Import mcertikos.proc.ThreadGenLinkSource.
Require Import mcertikos.proc.QThreadGenLinkSource.

Require Import mcertikos.proc.UCtxtIntroGenLinkSource.
Require Import mcertikos.proc.ProcGenLinkSource.

Require Import mcertikos.proc.EPTIntroGenLinkSource.
Require Import mcertikos.proc.EPTOpGenLinkSource.
Require Import mcertikos.proc.EPTInitGenLinkSource.
Require Import mcertikos.proc.VMCSIntroGenLinkSource.
Require Import mcertikos.proc.VMCSInitGenLinkSource.
Require Import mcertikos.proc.VMXIntroGenLinkSource.
Require Import mcertikos.proc.VMXInitGenLinkSource.

Require Import mcertikos.proc.BThreadGenLinkSource.

Require Import mcertikos.ipc.IPCIntroGenLinkSource.
Require Import mcertikos.ipc.IPCGenLinkSource.

Require Import mcertikos.trap.TrapArgGenLinkSource.
Require Import mcertikos.trap.TrapGenLinkSource.
Require Import mcertikos.trap.DispatchGenLinkSource.
Require Import mcertikos.trap.SysCallGenLinkSource.

Require Import GlobalOracleProp.
Require Import CompCertiKOSproofImpl.
Require Import RealParamsImpl.

Require Import AlgebraicMemImpl.
Require Import SingleOracle.
Require Import SingleConfiguration.
Require Import SingleOracleImpl.

Section WITHCOMPCERTIKOS.

  Context `{multi_oracle_prop : MultiOracleProp}.
  Context `{s_oracle_ops : SingleOracleOps}.
  Context `{s_threads_ops: ThreadsConfigurationOps}.

  Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
  Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
                                      (s_threads_ops := s_threads_ops)}.

  Existing Instance SingleOracleImpl.s_oracle_prf.
  Existing Instance SingleOracleImpl.s_oracle_prop_prf.
  Existing Instance SingleOracleImpl.s_config.

Can be useful for debugging: < Definition add_loc {A} s (r: res A): res A := match r with | OK a => OK a | Error e => Error (MSG (append s ": ") :: e) end. >

  Definition add_loc {A} (s: string) (r: res A) := r.

  Local Notation "M ⊗ Mrest" := (Mrest ⊕ M)
    (right associativity, at level 35, only parsing).

  Definition certikos_plus_ctxt CTXT: res LAsm.module :=
    

    M0010 <- add_loc "MCurID" MCurID_impl;
    M0020 <- add_loc "MTicketLockIntro" MTicketLockIntro_impl;
    M0030 <- add_loc "MTicketLockOp" MTicketLockOp_impl;
    M0040 <- add_loc "MQTicketLockOp" MQTicketLockOp_impl;
    M0050 <- add_loc "MHTicketLockOp" MHTicketLockOp_impl;
    M0060 <- add_loc "MQTicketLock" MQTicketLock_impl;

    M1010 <- add_loc "DConsolebuffintro" DConsoleBuffIntro_impl;
    M1020 <- add_loc "DAbsConsoleBuffIntro" DAbsConsoleBuffIntro_impl;
    M1030 <- add_loc "DSerialIntro" DSerialIntro_impl;
    M1040 <- add_loc "DSerial" DSerial_impl;
    M1050 <- add_loc "DIoApic" DIoApic_impl;
    M1060 <- add_loc "DLApic" DLApic_impl;
    M1070 <- add_loc "DConsole" DConsole_impl;
    M1080 <- add_loc "DHandlerIntro" DHandlerIntro_impl;
    M1090 <- add_loc "DHandlerSw" DHandlerSw_impl;
    M1100 <- add_loc "DHandlerAsm" DHandlerAsm_impl;
    M1110 <- add_loc "DHandlerCxt" DHandlerCxt_impl;
    M1120 <- add_loc "DHandlerOp" DHandlerOp_impl;
    M1130 <- add_loc "DHandler" DHandler_impl;
    M1140 <- add_loc "DAbsHandler" DAbsHandler_impl;


    M2010 <- add_loc "MContainerIntro" MContainerIntro_impl;
    M2020 <- add_loc "MContainer" MContainer_impl;
    M2030 <- add_loc "MALInit" MALInit_impl;
    M2040 <- add_loc "MALOp" MALOp_impl;
    M2050 <- add_loc "MALT" MALT_impl;
    M2060 <- add_loc "MALH" MALH_impl;
    M2070 <- add_loc "MPTIntro" MPTIntro_impl;
    M2080 <- add_loc "MPTOp" MPTOp_impl;
    M2090 <- add_loc "MPTCommon" MPTCommon_impl;
    M2100 <- add_loc "MPTKern" MPTKern_impl;
    M2110 <- add_loc "MPTInit" MPTInit_impl;
    M2120 <- add_loc "MPTNew" MPTNew_impl;
    M2130 <- add_loc "MShareIntro" MShareIntro_impl;
    M2140 <- add_loc "MShareOp" MShareOp_impl;
    M2150 <- add_loc "MShare" MShare_impl;

    M3010 <- add_loc "PKContext" PKContext_impl;
    M3020 <- add_loc "PKContextNew" PKContextNew_impl;
    M3030 <- add_loc "PSleeper" PSleeper_impl;
    M3040 <- add_loc "PQueueIntro" PQueueIntro_impl;
    M3050 <- add_loc "PQueueInit" PQueueInit_impl;
    
    M3060 <- add_loc "PAbQueueAtomic" PAbQueueAtomic_impl;
    M3070 <- add_loc "PCVIntro" PCVIntro_impl;
    M3080 <- add_loc "PCVOp" PCVOp_impl;
    M3090 <- add_loc "PThreadsched" PThreadSched_impl;
    M3100 <- add_loc "PThread" PThread_impl;
    M3110 <- add_loc "PQThread" PQThread_impl;

    M3120 <- add_loc "PUCtxtIntro" PUCtxtIntro_impl;
    M3130 <- add_loc "PProc" PProc_impl;

    M3140 <- add_loc "VEPTIntro" VEPTIntro_impl;
    M3150 <- add_loc "VEPTOp" VEPTOp_impl;
    M3160 <- add_loc "VEPTInit" VEPTInit_impl;
    M3170 <- add_loc "VVMCSIntro" VVMCSIntro_impl;
    M3180 <- add_loc "VVMCSInit" VVMCSInit_impl;
    M3190 <- add_loc "VVMXIntro" VVMXIntro_impl;
    M3200 <- add_loc "VVMXInit" VVMXInit_impl;

    M3210 <- add_loc "PBThread" PBThread_impl;


    M4010 <- add_loc "PIPCIntro" PIPCIntro_impl;
    M4020 <- add_loc "PIPC" PIPC_impl;

    M5010 <- add_loc "TTrapArg" TTrapArg_impl;
    M5020 <- add_loc "TTrap" TTrap_impl;
    M5030 <- add_loc "TDispatch" TDispatch_impl;
    M5040 <- add_loc "TSysCall" TSysCall_impl;

    ret (M0010 ⊗ M0020 ⊗ M0030 ⊗ M0040 ⊗ M0050 ⊗ M0060 ⊗

               M1010 ⊗ M1020 ⊗ M1030 ⊗ M1040 ⊗ M1050 ⊗
               M1060 ⊗ M1070 ⊗ M1080 ⊗ M1090 ⊗ M1100 ⊗
               M1110 ⊗ M1120 ⊗ M1130 ⊗ M1140 ⊗

               M2010 ⊗ M2020 ⊗ M2030 ⊗ M2040 ⊗ M2050 ⊗
               M2060 ⊗ M2070 ⊗ M2080 ⊗ M2090 ⊗ M2100 ⊗
               M2110 ⊗ M2120 ⊗ M2130 ⊗ M2140 ⊗ M2150 ⊗

               M3010 ⊗ M3020 ⊗ M3030 ⊗ M3040 ⊗ M3050 ⊗ ∅ ⊗
               M3060 ⊗ M3070 ⊗ M3080 ⊗ M3090 ⊗ M3100 ⊗
               M3110 ⊗ M3120 ⊗ M3130 ⊗ M3140 ⊗ M3150 ⊗
               M3160 ⊗ M3170 ⊗ M3180 ⊗ M3190 ⊗ M3200 ⊗
               M3210 ⊗

               M4010 ⊗ M4020 ⊗

               M5010 ⊗ M5020 ⊗ M5030 ⊗ M5040 ⊗

               CTXT).

  Definition certikos := certikos_plus_ctxt ∅.

  Definition per_cpu_certikos_plus_ctxt CTXT: res LAsm.module :=
    
    M0010 <- add_loc "MCurID" MCurID_impl;
    M0020 <- add_loc "MTicketLockIntro" MTicketLockIntro_impl;
    M0030 <- add_loc "MTicketLockOp" MTicketLockOp_impl;
    M0040 <- add_loc "MQTicketLockOp" MQTicketLockOp_impl;
    M0050 <- add_loc "MHTicketLockOp" MHTicketLockOp_impl;
    M0060 <- add_loc "MQTicketLock" MQTicketLock_impl;

    M1010 <- add_loc "DConsolebuffintro" DConsoleBuffIntro_impl;
    M1020 <- add_loc "DAbsConsoleBuffIntro" DAbsConsoleBuffIntro_impl;
    M1030 <- add_loc "DSerialIntro" DSerialIntro_impl;
    M1040 <- add_loc "DSerial" DSerial_impl;
    M1050 <- add_loc "DIoApic" DIoApic_impl;
    M1060 <- add_loc "DLApic" DLApic_impl;
    M1070 <- add_loc "DConsole" DConsole_impl;
    M1080 <- add_loc "DHandlerIntro" DHandlerIntro_impl;
    M1090 <- add_loc "DHandlerSw" DHandlerSw_impl;
    M1100 <- add_loc "DHandlerAsm" DHandlerAsm_impl;
    M1110 <- add_loc "DHandlerCxt" DHandlerCxt_impl;
    M1120 <- add_loc "DHandlerOp" DHandlerOp_impl;
    M1130 <- add_loc "DHandler" DHandler_impl;
    M1140 <- add_loc "DAbsHandler" DAbsHandler_impl;


    M2010 <- add_loc "MContainerIntro" MContainerIntro_impl;
    M2020 <- add_loc "MContainer" MContainer_impl;
    M2030 <- add_loc "MALInit" MALInit_impl;
    M2040 <- add_loc "MALOp" MALOp_impl;
    M2050 <- add_loc "MALT" MALT_impl;
    M2060 <- add_loc "MALH" MALH_impl;
    M2070 <- add_loc "MPTIntro" MPTIntro_impl;
    M2080 <- add_loc "MPTOp" MPTOp_impl;
    M2090 <- add_loc "MPTCommon" MPTCommon_impl;
    M2100 <- add_loc "MPTKern" MPTKern_impl;
    M2110 <- add_loc "MPTInit" MPTInit_impl;
    M2120 <- add_loc "MPTNew" MPTNew_impl;
    M2130 <- add_loc "MShareIntro" MShareIntro_impl;
    M2140 <- add_loc "MShareOp" MShareOp_impl;
    M2150 <- add_loc "MShare" MShare_impl;

    M3010 <- add_loc "PKContext" PKContext_impl;
    M3020 <- add_loc "PKContextNew" PKContextNew_impl;
    M3030 <- add_loc "PSleeper" PSleeper_impl;
    M3040 <- add_loc "PQueueIntro" PQueueIntro_impl;
    M3050 <- add_loc "PQueueInit" PQueueInit_impl;
    
    M3060 <- add_loc "PAbQueueAtomic" PAbQueueAtomic_impl;
    M3070 <- add_loc "PCVIntro" PCVIntro_impl;
    M3080 <- add_loc "PCVOp" PCVOp_impl;
    M3090 <- add_loc "PThreadsched" PThreadSched_impl;
    M3100 <- add_loc "PThread" PThread_impl;
    M3110 <- add_loc "PQThread" PQThread_impl;

    M3120 <- add_loc "PUCtxtIntro" PUCtxtIntro_impl;
    M3130 <- add_loc "PProc" PProc_impl;

    M3140 <- add_loc "VEPTIntro" VEPTIntro_impl;
    M3150 <- add_loc "VEPTOp" VEPTOp_impl;
    M3160 <- add_loc "VEPTInit" VEPTInit_impl;
    M3170 <- add_loc "VVMCSIntro" VVMCSIntro_impl;
    M3180 <- add_loc "VVMCSInit" VVMCSInit_impl;
    M3190 <- add_loc "VVMXIntro" VVMXIntro_impl;
    M3200 <- add_loc "VVMXInit" VVMXInit_impl;

    M3210 <- add_loc "PBThread" PBThread_impl;

    ret (M0010 ⊗ M0020 ⊗ M0030 ⊗ M0040 ⊗ M0050 ⊗ M0060 ⊗

               M1010 ⊗ M1020 ⊗ M1030 ⊗ M1040 ⊗ M1050 ⊗
               M1060 ⊗ M1070 ⊗ M1080 ⊗ M1090 ⊗ M1100 ⊗
               M1110 ⊗ M1120 ⊗ M1130 ⊗ M1140 ⊗

               M2010 ⊗ M2020 ⊗ M2030 ⊗ M2040 ⊗ M2050 ⊗
               M2060 ⊗ M2070 ⊗ M2080 ⊗ M2090 ⊗ M2100 ⊗
               M2110 ⊗ M2120 ⊗ M2130 ⊗ M2140 ⊗ M2150 ⊗

               M3010 ⊗ M3020 ⊗ M3030 ⊗ M3040 ⊗ M3050 ⊗ ∅ ⊗
               M3060 ⊗ M3070 ⊗ M3080 ⊗ M3090 ⊗ M3100 ⊗
               M3110 ⊗ M3120 ⊗ M3130 ⊗ M3140 ⊗ M3150 ⊗
               M3160 ⊗ M3170 ⊗ M3180 ⊗ M3190 ⊗ M3200 ⊗
               M3210 ⊗

               CTXT).

  Definition per_cpu_certikos := per_cpu_certikos_plus_ctxt ∅.

  Definition per_thread_certikos_plus_ctxt CTXT: res LAsm.module :=
    

    M4010 <- add_loc "PIPCIntro" PIPCIntro_impl;
    M4020 <- add_loc "PIPC" PIPC_impl;

    M5010 <- add_loc "TTrapArg" TTrapArg_impl;
    M5020 <- add_loc "TTrap" TTrap_impl;
    M5030 <- add_loc "TDispatch" TDispatch_impl;
    M5040 <- add_loc "TSysCall" TSysCall_impl;

    ret (M4010 ⊗ M4020 ⊗
                
               M5010 ⊗ M5020 ⊗ M5030 ⊗ M5040 ⊗
                
               CTXT).

  Definition per_thread_certikos := per_thread_certikos_plus_ctxt ∅.

End WITHCOMPCERTIKOS.

Require Import OracleInstances.
Extract Constant LEnv ⇒ "fun _ -> failwith ""LEnv cannot be utilized in the code.""".