How to Run SDV | Developing Drivers with the Windows Driver Foundation (Pro Developer)

When you use SDV in your driver development process, you must prepare the files, select the rules that you want to verify, and then run the SDV verification.

You can verify only one driver at a time. SDV runs in the directory that contains the driver's source code and make files. If a build tree includes more than one driver source code directory, you must run SDV separately in each directory.

How to Prepare Files and Select Rules for SDV

Before you can run SDV on a driver, you must prepare the files and select the rules to verify.

Tip See "Preparing to Run Static Driver Verifier" in the WDK for details-online at http://go.microsoft.com/fwlink/?LinkId=80606.

To Prepare to Run SDV

Clean the driver's sources directory.

You are not required to do this the first time you run SDV on a driver, but you must do it each time thereafter. See "How to Clean a Driver's Sources Directory" later in this chapter for details.
Process the driver's libraries.

To include libraries in the driver verification, you must process the library's source code files by running staticdv /lib in the library's sources directory.

This step is optional; however, if you do not process the driver's libraries, SDV cannot completely verify any code path that calls into the library. Processing the libraries produces more accurate verification results.
Scan the driver's source code.

You must do this the first time you run SDV on a driver and any time after you modify the driver in a way that changes its entry points.

See "How to Scan Driver Source Code to Create an Sdv-map.h File" later in this chapter for details.
Set time limits and virtual memory limits in the SDV Options file.

About the SDV Options file The SDV Options file Sdv-default.xml-stores the time limit (that is, time-out) and virtual memory limit (that is, space-out) that SDV uses for verification. The Options file also specifies how many threads SDV can use to run verifications in parallel. The default is shown as "0": it is automatically converted to the number of available logical processors. Note that SDV verification is a heavy consumer of resources, so making the number of threads larger than the number of logical processors does not improve the overall performance.

Tip The global Options file is stored at %wdk%\tools\sdv\data\<WDM | KMDF>. You can copy and edit this file for use in any driver's sources directory. See "Static Driver Verifier Options File" in the WDK for details about the Options file-online at http://go.microsoft.com/fwlink/?LinkId=80087.
Decide which SDV rules to verify.

Before running SDV, decide which rule-or rules-you want to verify on your driver. Running all rules can take several hours on a large driver.

See "KMDF Rules for SDV" later in this chapter. See "Static Driver Verifier" in the WDK for WDM rules-online at http://go.microsoft.com/fwlink/?LinkId=80084.

Tip
To run SDV on multiple drivers, create a batch file with a series of SDV commands.

How to Clean a Driver's Sources Directory

Before you can run SDV for verification and after you modify a driver, you must "clean" the driver's Sources directory to delete the SDV files that were generated in any previous verification. If you modify a library used by a driver, you must reprocess the library, as described in "How to Process Libraries Used by the Driver" later in this chapter.

To Clean the Driver's Sources Directory

In a build environment window, navigate to the driver's Sources directory.
Type the following command:
- staticdv /clean
To clean all libraries, type the following command:
- staticdv /cleanalllibs

The clean command issued for the driver does not delete the intermediate representation files that are generated for the library when you run staticdv /lib. Also, the clean command does not delete the Sdv-map.h file if the Approved flag is set to True in the file. These files are retained for subsequent verifications.

Tip See "Sdv-map.h" in the WDK for details-online at http://go.microsoft.com/fwlink/?LinkId=80083.

How to Process Libraries Used by the Driver

The inclusion of libraries in an SDV verification is essential for determining whether a driver complies with SDV rules. For example, without library code, a driver might appear to have missed a required call that is included in the library. Or, the library might include a call that the driver duplicates, causing a repeat error such as releasing a lock twice.

To include a library in the verification of a driver, SDV must first process the library to prepare the internal representation of the library for use in verifying the driver. This internal representation is stored as a file with the .li file name extension-for example, MyDrive.li.

You should process any libraries that you create for use in your drivers. You do not need to process the Windows libraries that provide DDI functions-such as Wdm.lib, Wdf.lib, Bufferoverflow.lib, Hal.lib, Ntoskernel.lib, Wmi.lib, and so on-because the SDV operating system model supplies verification stubs for DDI functions.

To Process a Library Used by a Driver

In a build environment window, select the build environment for the Windows version on which the driver runs.
Navigate to the library's sources directory.
At the command prompt, type the following:
- staticdv /clean
At the command prompt, type the following:
- staticdv /lib
If SDV detects other library dependencies but cannot find the library code, it displays a warning message: "Process <library name>."

After SDV has processed a library, it retains the intermediate representation files for that library and automatically includes the library code in verifications that you run for all drivers that require the library. You do not need to reprocess the library unless the library code changes.

Tip See "Library Processing in Static Driver Verifier" in the WDK for details-online at http://go.microsoft.com/fwlink/?LinkId=80077.

How to Scan Driver Source Code to Create an Sdv-map.h File

Before verifying a driver for the first time, you should use SDV to scan the driver's source code. During the scan step, SDV analyzes the driver source code to find the driver entry points. For a KMDF driver, these are the driver callback function role type declarations described in "How to Annotate KMDF Driver Source Code for SDV" earlier in this chapter.

About Sdv-map.h

SDV uses these declarations to produce the Sdv-map.h file in the driver's source code directory. Sdv-map.h "defines" the driver callback functions that are relevant to SDV. In fact, Sdv-map.h maps the relevant callback functions to generic callback names that are used in the SDV operating system model. For example, MyDpc might be mapped to fun_WDF_DPC_1. This is how SDV combines the driver sources with the SDV operating system model into a monolithic C program.

The optional process of scanning driver source code as a separate step is recommended, especially before running SDV on your driver for the first time. It's also a good idea to review the Sdv-map.h file to ensure that it defines all of the driver callback functions that you want to verify. If Sdv-map.h appears incomplete, you can edit it manually.

Sdv-map.h and Number of Callback Functions per Role Type

For most callback functions, SDV assumes that the driver has at most one function of a particular role type. However, a driver might have more than one callback function of some role types such as EVT_WDF_DPC. In this case, SDV appends an integer to the function type in Sdv-map.h. So, for example, if your driver has two DPC callback functions, SDV maps them to fun_WDF_DPC_1 and fun_WDF_DPC_2.

SDV supports a maximum number of callback functions for role types that can have more than one callback function. Having more than the maximum number does not make a driver incorrect, but it does complicate the use of SDV on the driver.

If a driver exceeds the maximum number of callback functions for a role type, SDV issues a message saying that the Sdv-map.h file has duplicate entry points. To solve this problem, you should manually edit Sdv-map.h to define the driver callback functions for each role type that SDV deals with. For example, if your driver has eight callback functions of the EVT_WDF_ DPC role type-for which SDV has a maximum limit of seven-you must:

Edit Sdv-map.h to undefine fun_WDF_DPC_5 through fun_WDF_DPC_8.
Run SDV on your driver.
Then edit Sdv-map.h again to define fun_WDF_DPC_5 through fun_WDF_DPC_8 and undefine fun_WDF_DPC_1 through fun_WDF_DPC_4.
Run SDV on your driver again.

See "KMDF Callback Function Role Types for SDV" later in this chapter for a list of role types that can have more than one callback function. In that section, Table 24-2 lists the maximum number of callback functions that SDV supports for certain role types.

Steps for Scanning Source Code to Create Sdv-map.h

For SDV to use the Sdv-map.h file in a verification pass, you must edit the first line in the file to appear as follows:

 //Approved=true

To Scan a Driver's Source Code to Create the Sdv-map.h File

In a build environment window, navigate to the driver's sources directory.
At the command prompt, type the following:
- staticdv /scan
The staticdv /scan command produces the Sdv-map.h file.
Review the Sdv-map.h file in the driver's sources directory to validate the entry points (that is, callback functions) that SDV found in the driver. If necessary, edit the entry point definitions.
After the Sdv-map.h file is correct, edit the first line of the file as follows:
- //Approved=true

Listing 24-3 shows the Sdv-map.h contents for the KMDF Fail_driver6 sample.

Listing 24-3: Sdv-map.h file for Fail_driver6

 //Approved=false #define fun_WDF_DRIVER_DEVICE_ADD EvtDriverDeviceAdd #define fun_WDF_DEVICE_CONTEXT_CLEANUP DeviceContextCleanUp #define fun_WDF_IO_QUEUE_IO_READ EvtIoRead #define fun_WDF_FILE_CONTEXT_CLEANUP_CALLBACK FileContextCleanup #define fun_WDF_FILE_CONTEXT_DESTROY_CALLBACK FileContextDestroy #define fun_WDF_DEVICE_CONTEXT_DESTROY DeviceContextDestroy #define fun_WDF_IO_QUEUE_CONTEXT_CLEANUP_CALLBACK QueueCleanup #define fun_WDF_IO_QUEUE_CONTEXT_DESTROY_CALLBACK QueueDestroy #define fun_WDF_IO_QUEUE_IO_WRITE EvtIoWrite #define fun_WDF_IO_QUEUE_IO_DEVICE_CONTROL EvtIoDeviceControl

Tip See "Scanning the DriverEntry Routine" in the WDK for details-online at http://go.microsoft.com/fwlink/?LinkId=80057.

How to Run a Verification

After you have prepared files, you can run a verification by specifying all rules, one rule, or a set of rules. You can also run a verification by using a predefined rule list.

See "KMDF Rules for SDV" later in this chapter for a list of the SDV rules that you can specify when verifying KMDF drivers.

Important

Never run multiple instances of SDV in parallel. SDV automatically runs verification in parallel over multiple rules by using the number of threads specified in the Options file.

To Run a Verification for All Rules

In a build environment window, navigate to the driver's sources directory.
At the command prompt, type the following:
- staticdv /rule:*

To Run a Verification for a Single Rule

In a build environment window, navigate to the driver's sources directory.
At the command prompt, enter a staticdv command to start a verification, using the following format:
- staticdv /rule:RuleName
where RuleName specifies the name of a particular SDV rule. For example, the following command runs the KMDF rule OutputBufferAPI:
- staticdv /rule:outputbufferapi

To Run a Verification for a Subset of Rules

In a build environment window, navigate to the driver's sources directory.

At the command prompt, enter a staticdv command to start a verification, using this format:
- staticdv /rule:Rule*
where Rule* specifies a set of rules based on a rule name pattern. For example, the following command runs a set of KMDF Request Buffer rules:
- staticdv /rule:bufafterreq*

In this case, SDV would verify the following rules:

BufAfterReqCompletedRead	BufAfterReqCompletedReadA
BufAfterReqCompletedWrite	BufAfterReqCompletedWriteA
BufAfterReqCompletedIoctl	BufAfterReqCompletedIoctlA
BufAfterReqCompletedIoctl	BufAfterReqCompletedIntIoctlA

Inside Out

A rule list is a simple text file that contains a list of rules and has an .sdv file extension. The WDK provides sample .sdv files with commonly used rule lists in the %wdk%\tools\sdv\samples\rule_sets subdirectory. For example, Listing 24-4 shows the sample WDM rule list called PnP.sdv.

Listing 24-4: PnP.sdv file for WDM drivers

 AddDevice PnpSameDeviceObject PnpIrpCompletion PnpSurpriseRemove TargetRelationNeedsRef

To Run a Verification by Using a Rule List

In a build environment window, navigate to the driver's sources directory.
At the command prompt, enter the following command to start a verification based on a rule list:
- staticdv /config:RuleList.sdv
where RuleList.sdv is the name of an .sdv file that contains a rule list.

Tip See "Static Driver Verifier Commands" in the WDK for a comprehensive reference for staticdv parameters-online at http://go.microsoft.com/fwlink/?LinkId=80085.

Experimenting with SDV

Inside Out

The WDK includes seven KMDF drivers named Fail_Driver1 through Fail_Driver7 in the %wdk%\tools\sdv\samples\fail_drivers\kmdf subdirectory. These drivers are specifically designed to fail SDV verification, so you can see what SDV does when it encounters rule violations. Use these KMDF drivers to experiment with SDV and the KMDF rules.

Caution

Because the \fail_drivers\kmdf samples contain deliberate errors, do not use them as the basis for any production driver code.

The example in Listing 24-5 shows command-line output for verification of the Fail_driver6 sample driver based on the staticdv /rule:bufafterreq* command.

Listing 24-5: SDV status messages for KMDF Request Buffer rules in Fail_driver6

 C:\WINDDK\6001\tools\sdv\samples\fail_drivers\kmdf\fail_driver6\driver>staticdv /rule:"bufafterreq*" --------------------------------------------------------------------- Microsoft (R) Windows (R) Static Driver Verifier Version 1.5.314.0 Copyright (C) Microsoft Corporation.  All rights reserved. --------------------------------------------------------------------- Build     'driver'  ...Done Link      'driver' for [fail_library6.lib] ...Done Scan      'driver'  ...Done Compile   'driver' for [sdv_harness_pnp_io_requests] ...Done Link      'driver' for [fail_library6.lib] ...Done Compile   'driver' for [sdv_harness_pnp_io_requests] ...Done Link      'driver' for [fail_library6.lib] ...Done Compile   'driver' for [sdv_harness_pnp_io_requests] ...Done Link      'driver' for [fail_library6.lib] ...Done Compile   'driver' for [sdv_harness_pnp_io_requests] ...Done Link      'driver' for [fail_library6.lib] ...Done Compile   'driver' for [sdv_harness_pnp_io_requests] ...Done Link      'driver' for [fail_library6.lib] ...Done Compile   'driver' for [sdv_harness_pnp_io_requests] ...Done Link      'driver' for [fail_library6.lib] ...Done Compile   'driver' for [sdv_harness_pnp_io_requests] ...Done Link      'driver' for [fail_library6.lib] ...Done Compile   'driver' for [sdv_harness_pnp_io_requests] ...Done Link      'driver' for [fail_library6.lib] ...Done Check     'driver' for 'bufafterreqcompletedwrite' ...Running Check     'driver' for 'bufafterreqcompletedwritea' ...Running Check     'driver' for 'bufafterreqcompletedwritea'  ...Done Check     'driver' for 'bufafterreqcompletedreada' ...Running Check     'driver' for 'bufafterreqcompletedreada'  ...Done Check     'driver' for 'bufafterreqcompletedread' ...Running Check     'driver' for 'bufafterreqcompletedwrite'  ...Done Check     'driver' for 'bufafterreqcompletedioctla' ...Running Check     'driver' for 'bufafterreqcompletedioctla'  ...Done Check     'driver' for 'bufafterreqcompletedioctl' ...Running Check     'driver' for 'bufafterreqcompletedread'  ...Done Check     'driver' for 'bufafterreqcompletedintioctla' ...Running Check     'driver' for 'bufafterreqcompletedioctl'  ...Done Check     'driver' for 'bufafterreqcompletedintioctl' ...Running Check     'driver' for 'bufafterreqcompletedintioctla'  ...Done Check     'driver' for 'bufafterreqcompletedintioctl'  ...Done Static Driver Verifier performed 8 check(s) with:         2 Defect(s)         2 Rule Passes         4 Not Applicable Start Time :1/25/2007 2:35:56 PM and End Time :1/25/2007 2:37:31 PM