Using PREfast for Static Code Analysis

Introduction

If you are a Windows developer, you must have noticed strange annotations in Windows SDK headers. Something like this:

DWORD WINAPI WaitForMultipleObjects(
    __in DWORD nCount,
    __in_ecount(nCount) CONST HANDLE *lpHandles,
    __in BOOL bWaitAll,
    __in DWORD dwMilliseconds
    ); 

This article will describe what it is and how it may be useful for you. Also, it will reveal basics of static code analysis with PREfast in Visual Studio.

What is PREfast?

PREfast is a utility for static code analysis (it means that analysis is done at compile time). It can find defects in C/C++ code such as buffer overruns, null pointer dereferencing, forgetting to check function return value and so on. Especially it is good in checking kernel-mode code due to a larger set of rules which the code has to follow. You can treat PREfast as a tool for an automatic code review.

To make its job better, PREfast has to know additional information about the code. That’s where annotations come into the action.

Annotations

Annotations are special macros. It is safe to use them in any context because these macros are expanded to nothing when the code is compiled normally. Only when PREfast runs, these macros are expanded into meaningful definitions. You can find general-purpose annotations defined in specstrings.h and the driver-specific annotations defined in driverspecs.h. System headers include the headers for annotations, so in most cases, you don't have to include them separately.

Annotations extend function prototype and describe the contract between the function and its caller. This makes it possible for PREfast to analyze code more accurately, with significantly fewer false positives and false negatives.

The other major benefit of using annotations is documentation. PREfast annotations are very easy to read and they form a documentation that doesn’t drift apart the code. Programmers don’t have to search external documentation or guess and experiment.

The set of source code annotations forms the Standard Annotation Language (SAL).

Annotation Modifiers

For various reasons related to implementation, many annotations that must be applied to a function parameter must be represented as a single macro, rather than as a series of adjacent macros. This is accomplished by adding modifiers to the annotation to compose a more complete annotation.

For example, __in annotation may be appended with _opt modifier and resulting annotation will be __in_opt.

Where to Place Annotations in Code

Annotations can be applied to a function as a whole, to an individual function parameter, and to the typedef declaration, including declaration of function types.

General-purpose Annotations

This section describes most commonly used annotations. You can use them in both driver and non-driver code. General-purpose annotations are defined in specstrings.h and described with extensive comments in specstrings_strict.h.

Direction of Data Flow

The most basic annotations are listed below, they should be used everywhere:

• __in
• __out
• __inout

These annotations help to identify that uninitialized values are used incorrectly. Formally, __in means that the value that is being passed as an argument must be valid before the function call and the function does not change it. __out means that the function returns a valid value and that PREfast can ignore the value before the function call. __inout means that the parameter must be valid before and after the function call and the function changes the value.

The valid value of pointers with these annotations cannot be NULL.

Examples

__out HANDLE WINAPI FindFirstFileW(
    __in  LPCWSTR            lpFileName,
    __out LPWIN32_FIND_DATAW lpFindFileData
    );

LONG __cdecl InterlockedDecrement (
    __inout LONG volatile *lpAddend
    );

Optionality

The _opt modifier indicates that the parameter is optional and thus a value of pointer can be NULL.

• __in_opt
• __out_opt
• __inout_opt

Examples

__out_opt HANDLE WINAPI CreateThread(
    __in_opt  LPSECURITY_ATTRIBUTES lpThreadAttributes,
    __in      SIZE_T dwStackSize,
    __in      LPTHREAD_START_ROUTINE lpStartAddress,
    __in_opt  LPVOID lpParameter,
    __in      DWORD dwCreationFlags,
    __out_opt LPDWORD lpThreadId
    );

WINBASEAPI BOOL WINAPI CreateProcessW(
    __in_opt    LPCWSTR lpApplicationName,
    __inout_opt LPWSTR lpCommandLine,
    __in_opt    LPSECURITY_ATTRIBUTES lpProcessAttributes,
    __in_opt    LPSECURITY_ATTRIBUTES lpThreadAttributes,
    __in        BOOL bInheritHandles,
    __in        DWORD dwCreationFlags,
    __in_opt    LPVOID lpEnvironment,
    __in_opt    LPCWSTR lpCurrentDirectory,
    __in        LPSTARTUPINFOW lpStartupInfo,
    __out       LPPROCESS_INFORMATION lpProcessInformation
    );

Dereference

The __deref modifier indicates that an annotation should be applied to the dereferenced value of a parameter, and not the parameter itself:

• __deref_in
• __deref_out
• __deref_inout

To make things clear, the following table shows how __deref and _opt modifiers can be combined together and what rules correspond to each combination.

Table 1 - __deref and _opt combinations

Examples

BOOL WINAPI OpenProcessToken (
    __in        HANDLE ProcessHandle,
    __in        DWORD DesiredAccess,
    __deref_out PHANDLE TokenHandle
    );

Zero-termination

The _z modifier indicates that the buffer is zero-terminated:

• __in_z
• __out_z
• __inout_z

Examples

struct hostent FAR * PASCAL FAR gethostbyname(__in_z const char FAR * name);

WINOLEAUTAPI_(BSTR) SysAllocString(__in_z_opt const OLECHAR * psz);

Strings

There are special annotations for strings:

• __nullterminated
• __nullnullterminated
• __possibly_notnullterminated

They are useful when applied to typedef declarations. These annotations enable PREfast to check that the type is used correctly in a function without requiring the programmer to annotate every function parameter that uses the type. Note the difference between PWCHAR and PWSTR:

typedef WCHAR *PWCHAR, *LPWCH, *PWCH;
typedef __nullterminated WCHAR *LPWSTR, *PWSTR;

The __nullnullterminated annotation is meant for “string of strings” that is terminated by a double null, such as a registry value whose type is REG_MULTI_SZ.

Several older functions usually return null-terminated strings but occasionally do not. The classic examples are snprintf and strncpy, where the function omits the null terminator if the buffer is exactly full. The __possibly_notnullterminated annotation describes such behavior.

Examples

WINOLEAPI StgIsStorageFile(
__in __nullterminated const WCHAR* pwcsName);

__out __nullnullterminated LPCH WINAPI
GetEnvironmentStrings(VOID);

int _snprintf(
   __out_ecount(count) __possibly_notnullterminated LPSTR buffer,
   __in size_t count,
   __in LPCSTR *format,
   ...
);

Buffer Size Annotations

Many bugs in code, particularly security bugs, are caused by buffer overflows in which a variable-sized object is being passed. The following annotations can be used to describe the contract between the caller and the callee about the size of buffers:

• _ecount(size)
• _bcount(size)
• _xcount(expr)
• _full(size)
• _part(size, length)

Use _ecount(size) to express the size of a buffer as a number of elements. Use _bcount(size) to express the size of a buffer as a number of bytes. The size parameter can be any general expression that makes sense at compile time. It can be a number, but it is usually the name of some parameter in the function that is being annotated (to refer to the function return value use return in the size specification). The _xcount(expr) is designed for complicated cases when the buffer size cannot be expressed as a simple byte or element count. For example, the count might be in a global variable or implied by an enumeration. PREfast treats expr as a comment and does not use it to check buffer size. expr can be anything that is meaningful to the reader.

The _full modifier indicates that the entire buffer is initialized (this is redundant with other annotations). The _part modifier indicates that the part of the buffer is initialized and explicitly indicates how much.

The following table summarizes the annotations that can be combined to describe a buffer.

Table 2 – Summary of buffer annotations

Examples

DWORD WINAPI WaitForMultipleObjects(
    __in DWORD nCount,
    __in_ecount(nCount) CONST HANDLE *lpHandles,
    __in BOOL bWaitAll,
    __in DWORD dwMilliseconds
    );

DWORD WINAPI GetLogicalDriveStringsW(
    __in DWORD nBufferLength,
    __out_ecount_part_opt(nBufferLength, return + 1) LPWSTR lpBuffer
    );

__bcount_opt(dwSize) LPVOID WINAPI VirtualAlloc(
    __in_opt LPVOID lpAddress,
    __in     SIZE_T dwSize,
    __in     DWORD flAllocationType,
    __in     DWORD flProtect
    );

BOOL APIENTRY VerQueryValueW(
    __in LPCVOID pBlock,
    __in LPCWSTR lpSubBlock,
    __deref_out_xcount("buffer can be PWSTR or DWORD*") LPVOID * lplpBuffer,
    __out PUINT puLen
    );

BOOL WINAPI ReadFile(
    __in        HANDLE hFile,
    __out_bcount_part_opt(nNumberOfBytesToRead, *lpNumberOfBytesRead) LPVOID lpBuffer,
    __in        DWORD   nNumberOfBytesToRead,
    __out_opt   LPDWORD lpNumberOfBytesRead,
    __inout_opt LPOVERLAPPED lpOverlapped
    );

Reserved Parameters

The __reserved annotation ensures that in future versions, old callers to a function can be reliably detected. This annotation insists that the provided parameter is 0 or NULL, as appropriate to the type.

Examples

WINAPI CreateDesktopW(
    __in LPCWSTR lpszDesktop,
    __reserved LPCWSTR lpszDevice,
    __reserved LPDEVMODEW pDevmode,
    __in DWORD dwFlags,
    __in ACCESS_MASK dwDesiredAccess,
    __in_opt LPSECURITY_ATTRIBUTES lpsa);

BOOLAPI InternetTimeToSystemTimeW(
    __in LPCWSTR lpszTime,
    __out SYSTEMTIME *pst,
    __reserved DWORD dwReserved
    );

Function Return Value

It is common to find code that assumes that a function call is always successful and that does not check the return value. The __checkReturn annotation indicates that the function return value should be checked.

Examples

__checkReturn DWORD WINAPI GetLastError(
    VOID
    );

__checkReturn SOCKET WSAAPI socket(
    __in int af,
    __in int type,
    __in int protocol
    );

Kernel-mode Annotations

There are a lot of annotations specially designed for kernel-mode code. They are defined in driverspecs.h and begin with the prefix __drv.

Here is a list of some of them:

• __drv_isObjectPointer
• __drv_inTry
• __drv_allocatesMem(type)
• __drv_freesMem(type)
• __drv_acquiresResource(kind)
• __drv_releasesResource(kind)
• __drv_acquiresCriticalRegion
• __drv_releasesCriticalRegion
• __drv_acquiresCancelSpinLock
• __drv_releasesCancelSpinLock
• __drv_mustHold(kind)
• __drv_neverHold(kind)
• __drv_mustHoldCriticalRegion
• __drv_neverHoldCriticalRegion
• __drv_mustHoldCancelSpinLock
• __drv_neverHoldCancelSpinLock
• __drv_acquiresExclusiveResource(kind)
• __drv_releasesExclusiveResource(kind)
• __drv_maxIRQL(value)
• __drv_minIRQL(value)
• __drv_floatUsed
• __drv_floatSaved
• __drv_floatRestored
• __drv_strictTypeMatch(mode)
• __drv_strictType(typename, mode)
• __drv_when(cond, anno_list)
• __drv_valueIs(list)
• __drv_clearDoInit(yes|no)
• __drv_dispatchType(type)

Using PREfast for drivers deserves a separate article and is not covered by this one.

False Positives

If you determine that a PREfast warning is a false positive or simply noise that does not need to be fixed, you can use a #pragma warning directive to suppress the warning.

In the #pragma warning directive, use the PREfast warning number to identify the warning to suppress. You can use the (push) and (pop) statements to confine the effect of the directive to the line of code that is producing the false positive:

#pragma warning(push)
#pragma warning(disable: XXXX)
// the following code will not produce specified warning
…
#pragma warning(pop)

As an alternative to push and pop, you can use the suppress statement to suppress the warning only for the next line of code:

#pragma warning(suppress : XXXX)
… // this line will not produce specified warning

Also, you can provide some assumptions about your code with __analysis_assume (expr) source code annotation, where expr is any expression that is assumed to evaluate to true. The following example eliminates null pointer dereference warning:

__analysis_assume(foo != NULL);
*foo = 0;

Running Code Analysis in Visual Studio

PREfast is integrated to Visual Studio 2010 Ultimate and Premium Editions, Visual Studio 2008 Development Edition and Team Suite. It is also available in Windows SDK compiler and as a separate tool in Windows DDK.

In Visual Studio, you can launch code analysis for a specific project using Analyze->Run Code Analysis on Only menu:

Also you can control code analysis via project properties or with command-line switch /analyze:

Analysis Examples

This section shows some functions with defects and what PREfast warnings they produce.

Uninitialized memory

Warning C6001: Using uninitialized memory 'b': Lines: 16, 18, 23

Memory leak

Warning C6211: Leaking memory 'p1' due to an exception. Consider using a local catch block to clean up memory: Lines: 21, 23, 25

Passing NULL handle

Warning C6387: 'argument 1' might be '0': this does not adhere to the specification for the function 'CloseHandle': Lines: 16, 20

Number of characters/number of bytes mismatch

Warning C6057: Buffer overrun due to number of characters/number of bytes mismatch in call to 'GetWindowsDirectoryW'
Warning C6031: Return value ignored: 'GetWindowsDirectoryW'
Warning C6386: Buffer overrun: accessing 'argument 1', the writable size is '200' bytes, but '400' bytes might be written: Lines: 16, 18

Conclusion

Don’t expect PREfast to find all defects in your code. The main benefit of SAL and PREfast is that you can find more bugs with just a little bit of upfront work and make your code more understandable to other programmers.

References

• Experiences with SAL/PREfast
• PREfast Annotations
• PREfast Step-by-Step
• About PREfast for Drivers
• PREfast: Less Bugs, More Reliability
• Prefast And SAL Annotations

History

• 11^th March, 2011: Initial post