/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    MdlAfterReqCompletedIoctl

Domain:

    wdf

Rule ID:

    Not Applicable

Description:

    After a Request is completed, the associated Mdl object
    cannot be accessed (inside Ioctl callback only).
    Mdl object was retrieved by calling WdfRequestRetrieveOutputWdmMdl or 
    WdfRequestRetrieveInputWdmMdl.
 
    Within Ioctl Io queue event callback, the Mdl object associated with the
    Request by calling WdfRequestRetrieveOutputWdmMdl or WdfRequestRetrieveInputWdmMdl,
    cannot be accessed after WdfRequestComplete/WithInformation/WithPriorityBoost 
    on the Request.
    The following possible Mdl object access functions are considered:
    WdfRequestRetrieveOutputWdmMdl, WdfRequestRetrieveInputWdmMdl.

Help Link:

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

--*/




#include "slic_base.h"

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

fun_WDF_IO_QUEUE_IO_DEVICE_CONTROL.entry[guard $2]
{
   s = IOCTL;
}
fun_WDF_IO_QUEUE_IO_DEVICE_CONTROL.exit[guard $2]
{
	 halt;
}
[sdv_WdfRequestComplete
,sdv_WdfRequestCompleteWithInformation
,sdv_WdfRequestCompleteWithPriorityBoost 
].entry[guard $1]
{    
     if (s == IOCTL){
           t = REQCOMPL;
   }
}
[sdv_WdfRequestRetrieveOutputWdmMdl
,sdv_WdfRequestRetrieveInputWdmMdl
].entry[guard $1]
{
   if ((s == IOCTL) && (t == REQCOMPL)) 
   {
          abort "Request's Mdl cannot be accessed after the Request had been completed.";
   }
   
}
