/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    MemAfterReqCompletedWrite

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

    This rule verifies that after a request is completed, the associated WDFMEMORY object
    cannot be accessed (inside EvtIoWrite callback only).
    The WDFMEMORY object was retrieved by calling WdfRequestRetrieveInputMemory or WdfRequestRetrieveOutputMemory.

    Within the EvtIoWrite callback function, the WDFMEMORY object associated with the
    request by calling WdfRequestRetrieveInputMemory or WdfRequestRetrieveOutputMemory
    cannot be accessed after calling the WdfRequestComplete, WdfRequestCompleteWithInformation, 
    or WdfRequestCompleteWithPriorityBoost methods on the request.
    The following possible WDFMEMORY object access functions are considered:
    WdfRequestRetrieveInputMemory, WdfRequestRetrieveOutputMemory.


Help Link:

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

--*/



#include "slic_base.h"

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

fun_WDF_IO_QUEUE_IO_WRITE.entry[guard $2]
{
   s = WRITE;
}
fun_WDF_IO_QUEUE_IO_WRITE.exit[guard $2]
{
	halt;
}
[sdv_WdfRequestComplete
,sdv_WdfRequestCompleteWithInformation
,sdv_WdfRequestCompleteWithPriorityBoost 
].entry[guard $1]
{    
     if (s == WRITE){
           t = REQCOMPL;                      
   }
}
[sdv_WdfRequestRetrieveInputMemory
,sdv_WdfRequestRetrieveOutputMemory
].entry[guard $1]
{
   if ((s == WRITE) && (t == REQCOMPL)) 
   {
          abort "Request's memory object cannot be accessed after the Request had been completed.";
   }
   
}
