/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    BufAfterReqCompletedRead

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

    After a Request is completed, its Buffer cannot be accessed
    (inside the EvtIoRead callback only). The buffer was retrieved by calling 
    WdfRequestRetrieveInputBuffer or WdfRequestRetrieveOutputBuffer or
    WdfRequestRetrieveUnsafeUserInputBuffer or WdfRequestRetrieveUnsafeUserOutputBuffer.
         
    Within EvtIoRead Io queue event callback, the Request Buffer retrieved by calling
    WdfRequestRetrieveOutputBuffer or WdfRequestRetrieveUnsafeUserOutputBuffer
    cannot be accessed after WdfRequestComplete/WithInformation/WithPriorityBoost 
    was called on the Request. The following possible buffer access functions are considered:
    WdfRequestRetrieveOutputBuffer, WdfRequestRetrieveUnsafeUserOutputBuffer,
    WdfRequestRetrieveInputBuffer, WdfRequestRetrieveUnsafeUserInputBuffer.

Help Link:

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

--*/



#include "slic_base.h"

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

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