/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    MemAfterReqCompletedReadA

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

    After a Request is completed, the associated WDFMEMORY object
    cannot be accessed (inside Read callback only).
    WDFMEMORY object was retrieved by calling WdfRequestRetrieveOutputMemory.

    Within Read Io queue event callback, the Request associated WDFMEMORY object retrieved by calling
    WdfRequestRetrieveOutputMemory cannot be accessed after WdfRequestComplete/WithInformation/WithPriorityBoost 
    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=507106

--*/



#include "slic_base.h"

state{
     enum {INIT2, MEMRETR, REQCOMPL} t = INIT2;
     int *cur_memory = 0;
}
watch fun_WDF_IO_QUEUE_IO_READ.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_WdfRequestRetrieveOutputMemory.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.";
   }
} 

