/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    MemAfterReqCompletedWriteA

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.
         
    Within the EvtIoWrite callback function, the request associated WDFMEMORY object retrieved by calling
    the WdfRequestRetrieveInputMemory method cannot be accessed after calling the WdfRequestComplete, WdfRequestCompleteWithInformation, 
    or WdfRequestCompleteWithPriorityBoost methods on the request. 
    The following possible buffer access functions are considered:
    WdfMemoryGetBuffer, WDF_MEMORY_DESCRIPTOR_INIT_HANDLE, WdfMemoryAssignBuffer, 
    WdfMemoryCopyToBuffer, WdfMemoryCopyFromBuffer, WdfObjectReference,
    WdfObjectDereference, WdfObjectDelete.


Help Link:

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

--*/



#include "slic_base.h"

state{
     enum {INIT2, MEMRETR, REQCOMPL} t = INIT2;
     int *cur_memory = 0;              
}

watch fun_WDF_IO_QUEUE_IO_WRITE.entry.$2;

sdv_main.entry
{
  cur_memory = hmemory;
}


[sdv_WdfRequestComplete
,sdv_WdfRequestCompleteWithInformation
,sdv_WdfRequestCompleteWithPriorityBoost
].exit [guard $1]
{  
    if(t == MEMRETR)
    {  
        t = REQCOMPL;
    }
    else
    {
        halt;
    }
}
sdv_WdfRequestRetrieveInputMemory.exit [guard $1]
{
   if (t != REQCOMPL) 
   {
       cur_memory = *($2);  
 	     t = MEMRETR;
   }
}
[sdv_WdfMemoryGetBuffer
, sdv_WdfMemoryAssignBuffer
, sdv_WdfMemoryCopyToBuffer
, sdv_WdfMemoryCopyFromBuffer
, sdv_WdfObjectReference
, sdv_WdfObjectDereference
, sdv_WdfObjectDelete
].entry
{
   if ((t == REQCOMPL) && ($1 == cur_memory)) {
       abort "Request's memory object cannot be accessed after the Request had been completed.";
   }
} 
sdv_WDF_MEMORY_DESCRIPTOR_INIT_HANDLE.entry
{
   if ((t == REQCOMPL) && ($2 == cur_memory)) {
       abort "Request's memory object cannot be accessed after the Request had been completed.";
   }
} 

