Skip to content

Commit

Permalink
Add missing initialisation in ntdrivers/parport.i.cil-2
Browse files Browse the repository at this point in the history
Missing or non-deterministic initialisation caused several memory-safety
errors. For example, the task eventually tries to access the memory
pointed to by
`irp.Tail.Overlay.__annonCompField17.__annonCompField16.CurrentStackLocation->Parameters.FilterResourceRequirements.IoResourceRequirementList`.
This member was never initialised, and could thus point anywhere.
Equally, `devobj.DeviceExtension` is used, but was not initialised.

Fixes: sosy-lab#1269
  • Loading branch information
tautschnig committed Dec 8, 2020
1 parent efea738 commit 1f32dfd
Showing 1 changed file with 11 additions and 0 deletions.
11 changes: 11 additions & 0 deletions c/ntdrivers/parport.i.cil-2.c
Original file line number Diff line number Diff line change
Expand Up @@ -3716,6 +3716,8 @@ NTSTATUS PptDispatchInternalDeviceControl(PDEVICE_OBJECT DeviceObject , PIRP Irp
Status = -1073741789L;
} else {
{
PARALLEL_1284_COMMAND cmd;
Irp->AssociatedIrp.SystemBuffer = &cmd;
Status = PptDeselectDevice(Extension, Irp->AssociatedIrp.SystemBuffer);
}
}
Expand Down Expand Up @@ -4757,6 +4759,7 @@ BOOLEAN PptCheckIfStlProductId(PDEVICE_EXTENSION DeviceExtension , ULONG ulDaisy
}
BOOLEAN PptSend1284_3Command(PDEVICE_EXTENSION DeviceExtension , UCHAR Command )
{ UCHAR i = __VERIFIER_nondet_char() ;
__VERIFIER_assume(i < 7);
UCHAR value ;
UCHAR newvalue ;
UCHAR test ;
Expand Down Expand Up @@ -9681,8 +9684,16 @@ int main(void)
int __BLAST_NONDET = __VERIFIER_nondet_int() ;
int irp_choice = __VERIFIER_nondet_int() ;
DEVICE_OBJECT devobj ;
d.DeviceObject = &devobj;
devobj.DeviceExtension = malloc(sizeof(struct _DEVICE_EXTENSION));
s = __VERIFIER_nondet_int();
irp.Tail.Overlay.__annonCompField17.__annonCompField16.CurrentStackLocation = malloc(4 * sizeof (IO_STACK_LOCATION));
for(int i = 0; i < 4; ++i)
{
irp.Tail.Overlay.__annonCompField17.__annonCompField16.CurrentStackLocation[i].
Parameters.FilterResourceRequirements.IoResourceRequirementList =
malloc(sizeof(struct _IO_RESOURCE_REQUIREMENTS_LIST));
}
/* ensure a bounded number of subsequent decrements do not result in stack underflow */
irp.Tail.Overlay.__annonCompField17.__annonCompField16.CurrentStackLocation += 3;

Expand Down

0 comments on commit 1f32dfd

Please sign in to comment.