WinDDK配置源文件，全！

/* Copyright (c) Microsoft Corporation. All rights reserved. */ /* ..\wdm\harness-copyright.c begin */ /* Copyright (c) Microsoft Corporation. All rights reserved. */ /* Module Name: SDV harness Abstract: Functions as representation of Windows OS for SDV. It boots the device driver and puts it into various states via its entry DriverEntry routine and dispatch routines, etc. Environment: Symbolic execution in Static Driver Verifier. */ /* ..\wdm\harness-copyright.c end */ /* ..\wdm\malloc.c begin */ /* Copyright (c) Microsoft Corporation. All rights reserved. */ char * malloc(int); /* ..\wdm\malloc.c end */ /* ..\wdm\harness-parts.c begin */ /* Copyright (c) Microsoft Corporation. All rights reserved. */ #include <ntifs.h> #include <ntdddisk.h> #include "sdv-map.h" #include "dispatch_routines.h" #include "sdv_stubs.h" #define SDV_IS_FLAT_HARNESS() \ ( \ SDV_HARNESS==SDV_FLAT_DISPATCH_HARNESS || \ SDV_HARNESS==SDV_FLAT_DISPATCH_STARTIO_HARNESS || \ SDV_HARNESS==SDV_FLAT_SIMPLE_HARNESS || \ SDV_HARNESS==SDV_FLAT_HARNESS \ ) #define SDV_MACRO_COPYCURRENTIRPSTACKLOCATIONTONEXT(arg1)\ if (arg1 == &sdv_harnessIrp) {\ sdv_harnessStackLocation_next.MinorFunction =\ sdv_harnessStackLocation.MinorFunction;\ sdv_harnessStackLocation_next.MajorFunction =\ sdv_harnessStackLocation.MajorFunction;\ }\ if (arg1 == &sdv_other_harnessIrp) {\ sdv_other_harnessStackLocation_next.MinorFunction =\ sdv_other_harnessStackLocation.MinorFunction;\ sdv_other_harnessStackLocation_next.MajorFunction =\ sdv_other_harnessStackLocation.MajorFunction;\ }\ #define SDV_MACRO_IOGETCURRENTIRPSTACKLOCATION(arg1)\ (arg1->Tail.Overlay.CurrentStackLocation)\ #define SDV_MACRO_STUB_CANCEL_BEGIN(arg1)\ IoAcquireCancelSpinLock(&(arg1->CancelIrql))\ #define SDV_MACRO_STUB_CANCEL_END(arg1)\ arg1->CancelRoutine=NULL\ VOID sdv_SetIrpMinorFunctionNonBusDriver( PIRP pirp ); VOID sdv_SetMajorFunction( PIRP pirp, UCHAR fun ); VOID sdv_SetPowerIrpMinorFunction( PIRP pirp ); VOID sdv_SetStatus( PIRP pirp ); NTSTATUS sdv_DoNothing( ); NTSTATUS sdv_RunDispatchFunction( PDEVICE_OBJECT po, PIRP pirp ); VOID sdv_RunCancelFunction( PDEVICE_OBJECT po, PIRP pirp ); NTSTATUS sdv_RunQueryDeviceRelations( PDEVICE_OBJECT po, PIRP pirp ); PIRP sdv_MakeAbstractIrp(PIRP pirp ); PIRP sdv_MakeStartDeviceIrp(PIRP pirp ); PIRP sdv_MakeRemoveDeviceIrp(PIRP pirp ); LONG SdvMakeChoice(); LONG SdvKeepChoice(); /*POWER_STATE sdv_Make_POWER_STATE();*/ VOID sdv_RunStartIo( PDEVICE_OBJECT po, PIRP pirp ); VOID sdv_RunIoCompletionRoutines( __in PDEVICE_OBJECT DeviceObject, __in PIRP Irp, __in_opt PVOID Context ); VOID sdv_RunISRRoutines( struct _KINTERRUPT *ki, PVOID pv1 ); VOID sdv_RunKeDpcRoutines( struct _KDPC *kdpc, PVOID pDpcContext, PVOID pv2, PVOID pv3 ); VOID sdv_RunIoDpcRoutines( IN PKDPC Dpc, IN struct _DEVICE_OBJECT *DeviceObject, IN struct _IRP *Irp, IN PVOID Context ); VOID sdv_RunUnload( PDRIVER_OBJECT pdrivo ); NTSTATUS sdv_RunAddDevice( PDRIVER_OBJECT p1, PDEVICE_OBJECT p2 ); BOOLEAN sdv_CheckDispatchRoutines( ); BOOLEAN sdv_CheckStartIoRoutines( ); BOOLEAN sdv_CheckDpcRoutines( ); BOOLEAN sdv_CheckIsrRoutines( ); BOOLEAN sdv_CheckCancelRoutines( ); BOOLEAN sdv_CheckCancelRoutines1( ); BOOLEAN sdv_CheckIoDpcRoutines( ); BOOLEAN sdv_IoCompletionRoutines( ); BOOLEAN sdv_CheckWorkerRoutines( ); BOOLEAN sdv_CheckAddDevice( ); BOOLEAN sdv_CheckIrpMjPnp( ); BOOLEAN sdv_CheckDriverUnload( ); VOID SdvExit(); VOID SdvAssume(int e); VOID SdvAssumeSoft(int e); int sdv_start_irp_already_issued = 0; int sdv_remove_irp_already_issued = 0; int sdv_compFset = 0; BOOLEAN sdv_isr_dummy ( IN struct _KINTERRUPT * Interrupt, IN PVOID ServiceContext ) { return FALSE; } PKSERVICE_ROUTINE sdv_isr_routine = sdv_isr_dummy; VOID sdv_dpc_dummy ( IN struct _KDPC * Dpc, IN PVOID DeferredContext, IN PVOID SystemArgument1, IN PVOID SystemArgument2 ) { } PKDEFERRED_ROUTINE sdv_ke_dpc=sdv_dpc_dummy; BOOLEAN sdv_dpc_ke_registered=FALSE; VOID sdv_io_dpc_dummy ( IN PKDPC Dpc, IN struct _DEVICE_OBJECT *DeviceObject, IN struct _IRP *Irp, IN PVOID Context ) { } PIO_DPC_ROUTINE sdv_io_dpc=sdv_io_dpc_dummy; BOOLEAN sdv_dpc_io_registered = FALSE; IRP sdv_harnessIrp; PIRP sdv_irp = &sdv_harnessIrp; IO_STACK_LOCATION sdv_harnessStackLocation; IO_STACK_LOCATION sdv_harnessStackLocation_next; IRP sdv_other_harnessIrp; PIRP sdv_other_irp = &sdv_other_harnessIrp; IO_STACK_LOCATION sdv_other_harnessStackLocation; IO_STACK_LOCATION sdv_other_harnessStackLocation_next; int sdv_harnessDeviceExtension_val; int sdv_harnessDeviceExtension_two_val; PVOID sdv_harnessDeviceExtension = (PVOID) &sdv_harnessDeviceExtension_val; PVOID sdv_harnessDeviceExtension_two = (PVOID) &sdv_harnessDeviceExtension_two_val; int sdv_io_create_device_called = 0; int sdv_context_val ; PVOID sdv_context = (PVOID) &sdv_context_val; int sdv_start_info_val ; ULONG_PTR sdv_start_info = (ULONG_PTR) &sdv_start_info_val; int sdv_end_info_val ; ULONG_PTR sdv_end_info = (ULONG_PTR) &sdv_end_info_val; /* SDV_DIRQL: The OS model raises IRQL to DIRQL by the use of the SDV_DIRQL macro. DIRQL is not a specific IRQL, but rather a range of possible Device IRQLs (On X86 from 3-26, on AMD64 from 3-11 and on IA64 from 4-11). The OS Model nevertheless declares SDV_DIRQL as the concrete value 4 (which is a valid DIRQL representative for all architectures). See ntddk_slic.h for details why this concretization is proper and will not result in loss of any traces. */ #define SDV_DIRQL 4 /* SDV OS Model IRQL Stack: The OS Model contains a Bounded IRQL Stack. The Bounded IRQL Stack should only be changed in OS Model DDIs and only using 1) the operation SDV_IRQL_PUSH for pushing onto the stack and 2) SDV_IRQL_POP and SDV_IRQL_POPTO for popping from the stack. The stack is used in a number of rules that specify proper stack behaviour for pairs of DDIs such as for example KeAcquireSpinLock and KeReleaseSpinLock. Pushing is used in the OS Model when a DDI sets/increases the IRQL to a new and weakly higher IRQL. An example of such a DDI is KeAcquireSpinLock. Popping is used in the OS Model when a DDI restores/lowers the IRQL to a new and weakly lower IRQL. An example of such a DDI is KeReleaseSpinLock. The stack is represented by the global variables sdv_irql_current, sdv_irql_previous, sdv_irql_previous_2 and sdv_irql_previous_3. sdv_irql_current is considered the top of the stack, sdv_irql_previous is the second element of the stack and so on. The stack is bounded. Currently to height three. This means that the OS Model will not correctly capture the meaning of more than three pushes to the stack. Certain rules that check proper stack behaviour takes this into account by counting current depth of the stack. */ /* Global IRQL stack, 4 levels high: */ KIRQL sdv_irql_current = PASSIVE_LEVEL; KIRQL sdv_irql_previous = PASSIVE_LEVEL; KIRQL sdv_irql_previous_2 = PASSIVE_LEVEL; KIRQL sdv_irql_previous_3 = PASSIVE_LEVEL; /*