civl error in ring allgatherv algorithm

[raffenet]

CIVL flags this OUT_OF_BOUNDS error in the allgatherv step of ring-based allreduce. Neither ASan nor valgrind report any out of bounds issue. May be a false positive.

civl verify -input_mpi_nprocs_lo=1 -input_mpi_nprocs_hi=5 -DNMAX=5 -DAR_OP=MPI_MIN ring_allreduce_driver.cvl civl_allred_ring.c civl_mpi_funcs.c
CIVL v1.22.r5959 of 2025-03-17 -- https://civl.dev
NP = 1, OPERATOR = 2
Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. NP = 2, OPERATOR = 2
Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok. Ok.
Violation 0 encountered at depth 622:
CIVL execution violation in p1 [Library: mpi.h, Function: MPI_Sendrecv] (property: OUT_OF_BOUNDS, certainty: PROVEABLE) at
$bundle_unpack(message.data, buf)
comm.cvl:87:4-36 | $bundle_unpack(message.data, buf)

Cannot unpack the bundle data into the pointed memory region.
Bundle data: $bundle_slice(((X_x_val[0][1]+(-1*X_x_val[0][0]))<0) ? X_x_val[0][1] : X_x_val[0][0], ((X_x_val[1][1]+(-1*X_x_val[1][0]))<0) ? X_x_val[1][1] : X_x_val[1][0], X_x_val[2][0],0,(((((32768/SIZEOF_REAL)-1)<=0)&&(0!=(32768/SIZEOF_REAL))) ? (32768/SIZEOF_REAL) : 2))
Bundle data size: (((((32768/SIZEOF_REAL)-1)<=0)&&(0!=(32768/SIZEOF_REAL))) ? (32768/SIZEOF_REAL) : 2)*SIZEOF_REAL
Pointer :&<d7>my_allreduce_result[0]
Memory region size: 3*SIZEOF_REAL

Input:
  _civl_argc=X__civl_argc
  _civl_argv=X__civl_argv
  N=3
  x_val=X_x_val
  _mpi_nprocs=2
  _mpi_nprocs_lo=1
  _mpi_nprocs_hi=5
Context:
  0==(((32768 div SIZEOF_REAL - 1 <= 0 && 0 != 32768 div SIZEOF_REAL) ? (32768 div SIZEOF_REAL) : 2) + ((((32768 div SIZEOF_REAL - 1 <= 0 && 0 != 32768 div SIZEOF_REAL) ? (32768 div SIZEOF_REAL) : 2) + 32768 div SIZEOF_REAL - 1 <= 0) ? (32768 div SIZEOF_REAL) : (-1*(((32768 div SIZEOF_REAL - 1 <= 0 && 0 != 32768 div SIZEOF_REAL) ? (32768 div SIZEOF_REAL) : 2) - 2))) - 2)
  0==(((32768 div SIZEOF_REAL + 1 <= 0) ? (32768 div SIZEOF_REAL) : 1) - 1)
  0==(((X_x_val[2][1] - 1*X_x_val[2][0] < 0) ? X_x_val[2][1] : X_x_val[2][0]) - 1*(((0 < X_x_val[2][1] - 1*X_x_val[2][0]) ? X_x_val[2][0] : X_x_val[2][1])))
  forall _t : dynamicType . (0 <= CIVL_SIZEOF(_t) - 1)
  ((((((((32768/SIZEOF_REAL)-1)<=0)&&(0!=(32768/SIZEOF_REAL))) ? (32768/SIZEOF_REAL) : 2)-2)*SIZEOF_REAL)+1)<=0
  0<=(((((((32768/SIZEOF_REAL)-1)<=0)&&(0!=(32768/SIZEOF_REAL))) ? (32768/SIZEOF_REAL) : 2)*SIZEOF_REAL)-1)
  0<=(SIZEOF_INT-1)
  0<=(SIZEOF_REAL-16385)
  0<=(X__civl_argc-1)
  0!=((((((32768/SIZEOF_REAL)-1)<=0)&&(0!=(32768/SIZEOF_REAL))) ? (32768/SIZEOF_REAL) : 2)-2)
  0!=(((((32768/SIZEOF_REAL)-1)<=0)&&(0!=(32768/SIZEOF_REAL))) ? (32768/SIZEOF_REAL) : 2)
  0!=(32768/SIZEOF_REAL)
Call stacks:
process 0:
  main@23
process 1:
  $message_unpack@73 comm.cvl:87:4 $bundle_unpack called from
  $mpi_sendrecv@683 civl-mpi-blocking.cvl:289:4 $message_unpack called from
  MPI_Sendrecv@257 mpi.cvl:225:2 $mpi_sendrecv called from
  MPIR_Allgatherv_intra_ring@591 mpiimpl_cvl.h:8:47 MPI_Sendrecv called from
  MPIR_Allreduce_intra_ring@367 civl_allred_ring.c:103:16 MPIR_Allgatherv_intra_ring called from
  _civl_main@395 ring_allreduce_driver.cvl:45:4 MPIR_Allreduce_intra_ring called from
  _mpi_process@230  called from
  _par_proc0@811

Logging new entry 0, writing trace to CIVLREP/ring_allreduce_driver_0.trace
Terminating search after finding 1 violation.

=== Source files ===
ring_allreduce_driver.cvl  (ring_allreduce_driver.cvl)
civl_allred_ring.c  (civl_allred_ring.c)
mpiimpl_cvl.h  (mpiimpl_cvl.h)
civl_mpi_funcs.c  (civl_mpi_funcs.c)

=== Command ===
civl verify -input_mpi_nprocs_lo=1 -input_mpi_nprocs_hi=5 -DNMAX=5 -DAR_OP=MPI_MIN ring_allreduce_driver.cvl civl_allred_ring.c civl_mpi_funcs.c

=== Stats ===
   time (s)          : 8.91          transitions  : 9256
   memory (bytes)    : 7.71751936E8  trace steps  : 5375
   max process count : 3             valid calls  : 55431
   states            : 5376          provers      : z3
   states saved      : 7801          prover calls : 294
   state matches     : 0

=== Result ===
The program MAY NOT be correct.  See CIVLREP/ring_allreduce_driver_log.txt