Resources to help you annotate code for static analysis
What are annotations?
} Essentially comments in the code that can be understood by static analysis tools (PREfast for Drivers, /analyze option in Visual Studio)
Why are annotations needed?
} Because they find bugs!
} Annotations describe the contract between the calling function and the called function
} The static tools use the annotations to verify the contract specifications (initialization, return values, and so on.)
} They improve the results of static analysis tools (for example, the signal-to-noise ratio)
If you have looked at the header files in the Windows Driver Kit (WDK), or looked at the source code for some of the sample drivers in the WDK, you might have noticed modifiers that are associated with function parameters. The modifiers, such as __in, __out, __ecount(size), and __bcount(size), are called annotations, and they describe how a function operates and interacts with its parameters or return values. Annotations are ignored by the compiler, but are understood by static analysis tools, such as PREfast for Drivers or by the code analysis option in Visual Studio (/analyze).
Annotations can provide additional information about a parameter that is not otherwise expressible. By adding annotations to your driver code, you can improve the accuracy of results from the static analysis tools. And in turn, by adding annotations, you gain a better understanding how your code is supposed to work. Because annotations and static tools can help you catch bugs earlier in the development process (during compilation), you can improve the effectiveness of the time you spend testing and debugging.
You add annotations on the driver-supplied function prototypes and function definitions in your driver source code. You can use as many or as few annotations as you need. The payback for all this work is that you benefit from the annotations every time you call those functions and run the static analysis tools. Additionally, you benefit from the annotations that Microsoft has added to the system-supplied functions.
Example of an annotated driver-supplied function
The following is a function declaration from the Toaster sample function driver in the WDK (WDKroot\version\src\general\toaster\func\). This function uses some simple annotations that enable PREfast for Drivers to report errors if it finds that uninitialized values are used incorrectly when this function is called.
NTSTATUS
ToasterQueryWmiDataBlock(
__in PDEVICE_OBJECT DeviceObject,
__in PIRP Irp,
__in ULONG GuidIndex,
__in ULONG InstanceIndex,
__in ULONG InstanceCount,
__inout PULONG InstanceLengthArray,
__in ULONG BufferAvail,
__out_bcount(BufferAvail) PUCHAR Buffer
);
Annotations to indicate Input and output parameters
In the ToasterQueryWmiDataBlock function, the __in annotation indicates the parameter is an input to a function. That is, the parameter must be valid (initialized) before the function call. Conversely, an __out annotation indicates that the parameter is initialized after the function call and thus is safe to use as an __in parameter to a subsequent function. The annotations can be combined. If a parameter is marked __inout, the parameter is initialized before the call and thus it is assumed to be safe to use as an __in parameter to a subsequent function. These annotations are particularly useful for pointer parameters. In the C language, a parameter is passed by value, which makes it impossible to tell from the function prototype whether the pointer is intended as input to the function, output from the function, or both. Use the __in, __out, and __inout annotations to direct the static analysis tools to check parameters that have these annotations and report any errors if it finds that uninitialized values are used incorrectly.
Annotations to indicate buffer parameters
Functions that read or write to buffers are a potential source of bugs and can represent a real security concern. When you add annotations for buffer parameters, you can enable the static tools to find buffer overflow and buffer underflow conditions. In the ToasterQueryWmiDataBlock example, the __out_bcount(BufferAvail) annotation indicates that the parameter is a buffer that is initialized after the function call and that the size of the buffer is specified by the BufferAvail parameter. The byte-count and element -count buffer annotations __bcount(size), and __ecount(size) provide information that ensures that neither the calling function nor the called function can access data outside the bounds of the buffer (the size of the buffer). The annotations can also express the difference between available memory and initialized memory, so that access to uninitialized memory can be detected. For an excellent discussion about how annotations can help catch buffer problems, see Michael Howard's blog A Brief Introduction to the Standard Annotation Language.
Example of an annotated system-supplied function
You can benefit from annotations simply by using the static analysis tools on your driver code. To save you trouble and to catch problems in Windows code, some system-supplied functions are annotated. These annotations include driver-specific annotations (using the prefix __drv) that ensure proper usage of the DDI. For example, there are driver annotations that specify the proper IRQL at which a function can be called, and annotations that describe the correct use of memory, spin locks, and other resources .
For example, WdfSpinLockAcquire method is a KMDF system-supplied function that is declared in Wdfsync.h.
__drv_maxIRQL(DISPATCH_LEVEL)
VOID
FORCEINLINE
WdfSpinLockAcquire(
__in
__drv_savesIRQL
__drv_neverHold(SpinLock)
__drv_acquiresResource(SpinLock)
WDFSPINLOCK SpinLock
)
{ ((PFN_WDFSPINLOCKACQUIRE) WdfFunctions[WdfSpinLockAcquireTableIndex])(WdfDriverGlobals, SpinLock);
}
There is a lot going on here. But to be brief, the annotation __drv_maxIRQL(DISPATCH_LEVEL) applies to the whole function and specifies that the WdfSpinLockAcquire method must be called only when IRQL <= DISPATCH_LEVEL. The annotations __drv_neverHold(SpinLock) and __drv_acquiresResource(SpinLock) prevent a double-taking of the spinlock (that is, the WdfSpinLockAcquire method must not be called again while the method is holding the spinlock). For more information about the driver specific annotations, see Driver Annotations in the WDK and take a look at the KMDF sample code and KMDF header files in the WDK.
Call to action!
· Use the static analysis tools. Use them early and use them often!
· Learn more about annotations, and add them to your function prototypes.
Resources
} PREfast for Drivers in the WDK
} PREfast for Drivers Annotations in the WDK
} Michael Howard's blog A Brief Introduction to the Standard Annotation Language
} Header Annotations in the SDK
} The driver sample and header files in the WDK
Dave Hagen [MSFT], WDK Technical Writer
http://blogs.msdn.com/wdkdocs
This posting is provided "AS IS" with no warranties, and confers no rights.
