/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    BufAfterReqCompletedIntIoctl

Domain:

    wdf

Rule ID:

    Not Applicable

Description:


    The BufAfterReqCompletedIntIoctl rule specifies that after a request is completed, its buffer cannot be accessed
    (inside EvtIoInternalDeviceControl callback function only). The buffer is retrieved by calling 
    WdfRequestRetrieveOutputBuffer or WdfRequestRetrieveUnsafeUserOutputBuffer or
    WdfRequestRetrieveInputBuffer or WdfRequestRetrieveUnsafeUserInputBuffer.
          
    
    Within the EvtIoInternalDeviceControl I/O queue event callback function, the request buffer retrieved 
    by calling WdfRequestRetrieveInputBuffer, WdfRequestRetrieveOutputBuffer, 
    WdfRequestRetrieveUnsafeUserInputBuffer, or WdfRequestRetrieveUnsafeUserOutputBuffer
    cannot be accessed after the request is completed. The request is completed by calling WdfRequestComplete,
    WdfRequestCompleteWithInformation, or WdfRequestCompleteWdfRequestCompleteWithPriorityBoost. 
    The following possible buffer access functions are considered:
    WdfRequestRetrieveOutputBuffer, WdfRequestRetrieveUnsafeUserOutputBuffer, 
        WdfRequestRetrieveInputBuffer and WdfRequestRetrieveUnsafeUserInputBuffer.
    
    Rule diagnostics: 
    "Request's Buffer cannot be accessed after the Request had been completed."      
    
    Note 1:  The following buffer access functions are considered in a separate
    rule: RtlMoveMemory (with the buffer as a 1st and 2nd parameter),
    RtlZeroMemory, RtlCompareMemory, ZwReadFile, WDF_MEMORY_DESCRIPTOR_INIT_BUFFER, 
    WdfMemoryCreatePreallocated, WdfMemoryAssignBuffer, WdfMemoryCopyFromBuffer,
    WdfMemoryCopyToBuffer.

Help Link:

    https://go.microsoft.com/fwlink/?LinkId=507041

--*/




#include "slic_base.h"

state{
     enum {INIT1, IOCTL} s = INIT1;
     enum {INIT2, REQCOMPL} t = INIT2;
} with guard (sdv_main, hrequest)

fun_WDF_IO_QUEUE_IO_INTERNAL_DEVICE_CONTROL.entry [guard $2]
{
   s = IOCTL;
}
fun_WDF_IO_QUEUE_IO_INTERNAL_DEVICE_CONTROL.exit [guard $2]
{
	halt;
}
[sdv_WdfRequestComplete
,sdv_WdfRequestCompleteWithInformation
,sdv_WdfRequestCompleteWithPriorityBoost
].exit [guard $1]
{    
    if (s == IOCTL){
       t = REQCOMPL;                      
   }
}
[ sdv_WdfRequestRetrieveOutputBuffer
, sdv_WdfRequestRetrieveUnsafeUserOutputBuffer
, sdv_WdfRequestRetrieveInputBuffer
, sdv_WdfRequestRetrieveUnsafeUserInputBuffer
].exit [guard $1]
{
     if ((s == IOCTL) && (t == REQCOMPL)) 
	 {
          abort "Request's Buffer cannot be accessed after the Request had been completed.";
     }
	 
}
