@@ -5,6 +5,7 @@ use std::path::PathBuf;
5
5
use std:: time:: SystemTime ;
6
6
7
7
use bitflags:: bitflags;
8
+ use rand:: Rng ;
8
9
9
10
use crate :: shims:: files:: { FileDescription , FileHandle } ;
10
11
use crate :: shims:: windows:: handle:: { EvalContextExt as _, Handle } ;
@@ -462,6 +463,15 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
462
463
} ;
463
464
let io_status_info = this. project_field_named ( & io_status_block, "Information" ) ?;
464
465
466
+ // Non-deterministically decide to further reduce the count, simulating a partial write (but
467
+ // never to 0, that has different behavior).
468
+ let count =
469
+ if desc. nondet_short_accesses ( ) && count >= 2 && this. machine . rng . get_mut ( ) . random ( ) {
470
+ count / 2
471
+ } else {
472
+ count
473
+ } ;
474
+
465
475
let finish = {
466
476
let io_status = io_status. clone ( ) ;
467
477
let io_status_info = io_status_info. clone ( ) ;
@@ -491,7 +501,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
491
501
} }
492
502
)
493
503
} ;
494
-
495
504
desc. write ( this. machine . communicate ( ) , buf, count. try_into ( ) . unwrap ( ) , this, finish) ?;
496
505
497
506
// Return status is written to `dest` and `io_status_block` on callback completion.
@@ -556,6 +565,22 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
556
565
} ;
557
566
let io_status_info = this. project_field_named ( & io_status_block, "Information" ) ?;
558
567
568
+ let fd = match handle {
569
+ Handle :: File ( fd) => fd,
570
+ _ => this. invalid_handle ( "NtWriteFile" ) ?,
571
+ } ;
572
+
573
+ let Some ( desc) = this. machine . fds . get ( fd) else { this. invalid_handle ( "NtReadFile" ) ? } ;
574
+
575
+ // Non-deterministically decide to further reduce the count, simulating a partial write (but
576
+ // never to 0, that has different behavior).
577
+ let count =
578
+ if desc. nondet_short_accesses ( ) && count >= 2 && this. machine . rng . get_mut ( ) . random ( ) {
579
+ count / 2
580
+ } else {
581
+ count
582
+ } ;
583
+
559
584
let finish = {
560
585
let io_status = io_status. clone ( ) ;
561
586
let io_status_info = io_status_info. clone ( ) ;
@@ -585,14 +610,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
585
610
} }
586
611
)
587
612
} ;
588
-
589
- let fd = match handle {
590
- Handle :: File ( fd) => fd,
591
- _ => this. invalid_handle ( "NtWriteFile" ) ?,
592
- } ;
593
-
594
- let Some ( desc) = this. machine . fds . get ( fd) else { this. invalid_handle ( "NtReadFile" ) ? } ;
595
-
596
613
desc. read ( this. machine . communicate ( ) , buf, count. try_into ( ) . unwrap ( ) , this, finish) ?;
597
614
598
615
// See NtWriteFile for commentary on this
0 commit comments