/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    BufAfterReqCompletedReadA

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

    
    This rule verifies that after a request is completed, its buffer cannot be accessed
    (inside EvtIoRead callback only). The buffer was retrieved by calling 
        WdfRequestRetrieveOutputBuffer or WdfRequestRetrieveUnsafeUserOutputBuffer.
    
    Within the EvtIoRead I/O queue event callback function, the request buffer retrieved by calling
    WdfRequestRetrieveOutputBuffer or WdfRequestRetrieveUnsafeUserOutputBuffer,
    cannot be accessed after the WdfRequestComplete, WdfRequestCompleteWithInformation, or WdfRequestCompleteWithPriorityBoost 
    methods have been called on the request. The following possible buffer access functions are considered:
    RtlMoveMemory (with the buffer as a 1st and 2nd parameter),
    RtlZeroMemory, RtlCompareMemory, ZwReadFile, ZwWriteFile, 
    WDF_MEMORY_DESCRIPTOR_INIT_BUFFER, 
    WdfMemoryCreatePreallocated, WdfMemoryAssignBuffer, WdfMemoryCopyFromBuffer,
    WdfMemoryCopyToBuffer.
    
    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: WdfRequestRetrieveInputBuffer, WdfRequestRetrieveUnsafeUserInputBuffer,
    WdfRequestRetrieveOutputBuffer, WdfRequestRetrieveUnsafeUserOutputBuffer.    

Help Link:

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

--*/




#include "slic_base.h"

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


sdv_main.entry
{
  cur_buffer = hbuffer;
}

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
].exit [guard $1]
{
   if (t != REQCOMPL) {
          cur_buffer = *($3);  
      }
}
[sdv_RtlMoveMemory
,RtlCompareMemory
].entry
{
     if ((t == REQCOMPL) && (($1 == cur_buffer) || ($2 == cur_buffer))) {
       abort "Request's Buffer cannot be accessed after the Request had been completed.";
   }
}     
sdv_RtlZeroMemory.entry
{
     if ((t == REQCOMPL) && ($1 == cur_buffer)) {
       abort "Request's Buffer cannot be accessed after the Request had been completed.";
   }
} 
ZwReadFile.entry
{
     if ((t == REQCOMPL) && ($6 == cur_buffer)) {
       abort "Request's Buffer cannot be accessed after the Request had been completed.";
   }
} 
[sdv_WDF_MEMORY_DESCRIPTOR_INIT_BUFFER
,sdv_WdfMemoryCreatePreallocated
,sdv_WdfMemoryAssignBuffer
].entry
{
     if ((t == REQCOMPL) && ($2 == cur_buffer)) {
       abort "Request's Buffer cannot be accessed after the Request had been completed.";
   }
}   
[sdv_WdfMemoryCopyFromBuffer
,sdv_WdfMemoryCopyToBuffer
].entry
{
     if ((t == REQCOMPL) && ($3 == cur_buffer)) {
       abort "Request's Buffer cannot be accessed after the Request had been completed.";
   }
}       
