Success and Failure Annotations

When a function succeeds, the contract between the function that makes the call (the caller) and the function that is called (the callee) should be met. However, some functions can fail. If a function fails, it is unreasonable to expect the contract to be met and expecting it to do so could create false analysis paths.

PFD provides a family of annotations that can be used to describe both how a function indicates success (or failure) and how to interpret the results if the function fails. The most important of these is the __success(expr) annotation. The parameter expr describes the condition under which the function is considered to have succeeded. Usually, it is something like __success(return >= 0).

When a function succeeds, its contract is assumed to be met. That is, all of the post-call condition annotations are expected to be true. When the function does not succeed, all of the post-call condition annotations are ignored, with the specific exception of the**__out** family of annotations, When PFD scans a function that calls another function, it considers valid any parameter of the called function annotated with the __out annotation (or one of the various annotations that indicate that it should now be validated). For example, any changes in the state of resources appear as if they never occurred in the case of failure, but a parameter that should now be validated will be considered valid. Be aware that a function that does not have the __success annotation can never fail in this sense. For more information about this annotation, see Function Call Semantics, and the Pre and Post Contexts.

The __success annotation can be applied to a typedef, and by default, both NTSTATUS and HRESULT have the annotation __success(return >= 0) applied to them. Thus all functions that return either NTSTATUS or HRESULT return values have this success and failure behavior.

Frequently, a function returns a particular range of values for success and a second range for failure. It is often assumed (more a matter of common sense) that no other return values are possible. Simulation tools in general, and PFD is no exception, do not have access to these assumptions, and must know when certain values are not possible (or at least when they should not be simulated). The __failure(expr) annotation describes the range of values that should be considered as failures, with the explicit implication that no other values but those appearing in __success and __failure are possible. In particular, it is often useful to annotate functions that return BOOLEAN as the result type with the following:

__success(return == 1) __failure(return==0) BOOLEAN fun(...)

These annotations help PFD interpret the assumptions for the return type. For example, a return value of 3 might otherwise be perfectly reasonable because a BOOLEAN is really a typedef for int, and a value of 3 for an int is completely valid. In the absence of an explicit __failure annotation, failure is taken to be the negation of the condition in the __success annotation.

When a function fails, there are many different conventions as to what the output values might be. The most common convention is to use unspecified: the results are whatever they might be. That is, the output values might not be updated (but they also might be). PFD also follows that convention at this time. However, certain function and certain coding conventions require more precise control of the behavior on failure.

The annotation __on_failure(annotation) indicates that that annotation applies when the function is considered to have failed. The __on_failure annotation applies to the parameter on which it is coded (or it honors __drv_at). If the function fails, the annotation in __on_failure is taken to hold. For example, a function that guarantees that a particular output parameter is null on failure, would use the annotations __on_failure(__deref __null) to indicate that.

The annotation __valueUndefined is particularly useful in this context. The annotation __on_failure(__deref __valueUndefined) indicates that any attempt to access the output parameter is considered the same as accessing an uninitialized variable. If the coding convention is, for a particular function (or when using a typedef, a particular return value), that all output values are undefined, the annotation __failureDefault(__failureUndefined) indicates that all output values are to be considered undefined values. __failureDefault(__failureUnspecified) explicitly indicates the default (of unspecified).

 

 

Send comments about this topic to Microsoft

Build date: 5/3/2011