/*++

    Copyright (c) Microsoft Corporation.  All rights reserved.

Rule Name:

    MarkingQueuedIrps

Domain:

    wdm

Rule ID:

    Not Applicable

Description:

    This is a warning rule.
    This rule verifies that driver correctly marks the IRP as
    pending when it queues it for further processing.  Drivers
    should call IoMarkIrpPending before the lock is released,
    otherwise the IRP might get completed in an arbitrary thread
    context before it is marked as pending.

Help Link:

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

--*/


#include "slic_base.h"

state{
    int locked = 0;
    int queued = 0;
    int queuedWithoutMarking = 0;
    int markedPending = 0;  
    enum {initial,skipped} stack_location = initial; 
} with guard (sdv_main,sdv_irp)


[RemoveHeadList,sdv_containing_record].entry
{
    halt;
}

[InsertHeadList
,InsertTailList
].entry{
    queued = 1;
}


[IoSkipCurrentIrpStackLocation].entry[guard $1]
{
    stack_location = skipped;
}

[IoCallDriver,PoCallDriver].entry[guard $2]
{
    if(stack_location==skipped)
    {
        halt;
    }
}




[KeInsertDeviceQueue
,KeInsertQueueDpc
,KeInsertByKeyDeviceQueue
].exit
{
    if ($return)
        queued = 1;
}

[KeAcquireSpinLock
,KeAcquireInStackQueuedSpinLock
,KfAcquireSpinLock].entry
{
    locked = 1;
}

[KeReleaseSpinLock
,KeReleaseInStackQueuedSpinLock
,KfReleaseSpinLock].entry
{
    if (locked && queued && !markedPending) 
    {
        queuedWithoutMarking = 1;
    }
    locked = 0;
}

IoMarkIrpPending.entry
{
    markedPending = 1;       
}

[SDV_RunDispatchFunction].exit
{
    if ($return == STATUS_PENDING && queuedWithoutMarking) 
    {
        abort "Warning: Driver may have queued the IRP without marking it as pending inside the locked state."; 
    }
    else
    {
        halt;
    }    
}
