Skip to content

Fix verified static-analysis bugs; reject false positives #20

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
stanmoore1 wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Fix verified static-analysis bugs; reject false positives #20

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2c09b87
Fix verified static-analysis bugs; reject false positives
claude Jun 26, 2026
6df8323
Add ai_bugfixes-specific audit appendix to BUG_VERIFICATION.md
claude Jul 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
243 changes: 243 additions & 0 deletions BUG_VERIFICATION.md
View file
Open in desktop

Large diffs are not rendered by default.

6 changes: 2 additions & 4 deletions src/KOKKOS/collide_vss_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -760,7 +760,6 @@ void CollideVSSKokkos::operator()(TagCollideCollisionsOne< NEARCP, GASTALLY, ATO
else
reduce.nreact_one++;
} else {
rand_pool.free_state(rand_gen);
continue;
}

Expand Down Expand Up @@ -1170,7 +1169,6 @@ void CollideVSSKokkos::operator()(TagCollideCollisionsOneAmbipolar< GASTALLY, AT
else
reduce.nreact_one++;
} else {
rand_pool.free_state(rand_gen);
continue;
}

Expand Down Expand Up @@ -1592,7 +1590,7 @@ void CollideVSSKokkos::SCATTER_TwoBodyScattering(Particle::OnePart *ip,
vb = vr*sinX*cos(eps);
wc = vr*sinX*sin(eps);
} else {
double scale = sqrt((2.0 * postcoln.etrans) / (d_params(isp,jsp).mr * precoln.vr2));
double scale = (precoln.vr2 > 0.0) ? sqrt((2.0 * postcoln.etrans) / (d_params(isp,jsp).mr * precoln.vr2)) : 0.0;
double cosX = 2.0*pow(rand_gen.drand(),alpha_r) - 1.0;
double sinX = sqrt(1.0 - cosX*cosX);
vrc[0] = vi[0]-vj[0];
Expand Down Expand Up @@ -1799,7 +1797,7 @@ void CollideVSSKokkos::SCATTER_ThreeBodyScattering(Particle::OnePart *ip,
vb = vr*sinX*cos(eps);
wc = vr*sinX*sin(eps);
} else {
double scale = sqrt((2.0*postcoln.etrans) / (mr*precoln.vr2));
double scale = (precoln.vr2 > 0.0) ? sqrt((2.0*postcoln.etrans) / (mr*precoln.vr2)) : 0.0;
vrc[0] = vi[0]-vj[0];
vrc[1] = vi[1]-vj[1];
vrc[2] = vi[2]-vj[2];
Expand Down
14 changes: 8 additions & 6 deletions src/KOKKOS/compute_dt_grid_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -357,13 +357,15 @@ void ComputeDtGridKokkos::operator()(TagComputeDtGrid_ComputePerGrid, const int

// cell dt based on transit time using maximum most probable speed
double vrm_max = sqrt(2.0*boltz * d_temp_vector(i) / min_species_mass);
dt_candidate = transit_fraction*dx/vrm_max;
cell_dt_desired = MIN(dt_candidate,cell_dt_desired);
dt_candidate = transit_fraction*dy/vrm_max;
cell_dt_desired = MIN(dt_candidate,cell_dt_desired);
if (dimension == 3) {
dt_candidate = transit_fraction*dz/vrm_max;
if (vrm_max > 0.0) {
dt_candidate = transit_fraction*dx/vrm_max;
cell_dt_desired = MIN(dt_candidate,cell_dt_desired);
dt_candidate = transit_fraction*dy/vrm_max;
cell_dt_desired = MIN(dt_candidate,cell_dt_desired);
if (dimension == 3) {
dt_candidate = transit_fraction*dz/vrm_max;
cell_dt_desired = MIN(dt_candidate,cell_dt_desired);
}
}

d_vector_grid(i) = cell_dt_desired;
Expand Down
10 changes: 7 additions & 3 deletions src/KOKKOS/compute_eflux_grid_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,7 @@ void ComputeEFluxGridKokkos::operator()(TagComputeEFluxGrid_compute_per_grid, co

const int ispecies = d_particles[i].ispecies;
const int igroup = d_s2g(imix,ispecies);
if (igroup < 0) return;
if (igroup < 0) continue;

const double mass = d_species[ispecies].mass;
double *v = d_particles[i].v;
Expand Down Expand Up @@ -420,8 +420,12 @@ void ComputeEFluxGridKokkos::operator()(TagComputeEFluxGrid_post_process_grid, c
h2 = d_etally(icell,mvv2v2) - 2.0*d_etally(icell,mvv2)*d_etally(icell,mv2)/summass -
d_etally(icell,mv)*d_etally(icell,mv2v2)/summass +
2.0*d_etally(icell,mv)*d_etally(icell,mv2)*d_etally(icell,mv2)/summass/summass;
wt = 0.5 * fnum * d_cinfo[icell].weight / d_cinfo[icell].volume;
d_vec[icell] = wt/nsample * (h + h1 + h2);
if (d_cinfo[icell].volume > 0.0) {
wt = 0.5 * fnum * d_cinfo[icell].weight / d_cinfo[icell].volume;
d_vec[icell] = wt/nsample * (h + h1 + h2);
} else {
d_vec[icell] = 0.0;
}
}
}

Expand Down
36 changes: 28 additions & 8 deletions src/KOKKOS/compute_lambda_grid_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -315,23 +315,43 @@ void ComputeLambdaGridKokkos::compute_per_grid_kokkos()
sizeall += sizez;
sizeall /= 3.0;
}
if (l_noutputs == 1) l_vector_grid[i] = lambda / sizeall;
else l_array_grid(i,l_output_order[KNALL]) = lambda / sizeall;
if (sizeall > 0.0) {
if (l_noutputs == 1) l_vector_grid[i] = lambda / sizeall;
else l_array_grid(i,l_output_order[KNALL]) = lambda / sizeall;
} else {
if (l_noutputs == 1) l_vector_grid[i] = 0.0;
else l_array_grid(i,l_output_order[KNALL]) = 0.0;
}
}

if (l_knxflag) {
if (l_noutputs == 1) l_vector_grid[i] = lambda / sizex;
else l_array_grid(i,l_output_order[KNX]) = lambda / sizex;
if (sizex > 0.0) {
if (l_noutputs == 1) l_vector_grid[i] = lambda / sizex;
else l_array_grid(i,l_output_order[KNX]) = lambda / sizex;
} else {
if (l_noutputs == 1) l_vector_grid[i] = 0.0;
else l_array_grid(i,l_output_order[KNX]) = 0.0;
}
}

if (l_knyflag) {
if (l_noutputs == 1) l_vector_grid[i] = lambda / sizey;
l_array_grid(i,l_output_order[KNY]) = lambda / sizey;
if (sizey > 0.0) {
if (l_noutputs == 1) l_vector_grid[i] = lambda / sizey;
else l_array_grid(i,l_output_order[KNY]) = lambda / sizey;
} else {
if (l_noutputs == 1) l_vector_grid[i] = 0.0;
else l_array_grid(i,l_output_order[KNY]) = 0.0;
}
}

if (l_knzflag) {
if (l_noutputs == 1) l_vector_grid[i] = lambda / sizez;
l_array_grid(i,l_output_order[KNZ]) = lambda / sizez;
if (sizez > 0.0) {
if (l_noutputs == 1) l_vector_grid[i] = lambda / sizez;
else l_array_grid(i,l_output_order[KNZ]) = lambda / sizez;
} else {
if (l_noutputs == 1) l_vector_grid[i] = 0.0;
else l_array_grid(i,l_output_order[KNZ]) = 0.0;
}
}
});
}
Expand Down
4 changes: 2 additions & 2 deletions src/KOKKOS/compute_pflux_grid_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -354,7 +354,7 @@ KOKKOS_INLINE_FUNCTION
void ComputePFluxGridKokkos::operator()(TagComputePFluxGrid_post_process_grid_diag, const int &icell) const {
double summass, summv, wt;
summass = d_etally(icell,mass);
if (summass == 0.0) d_vec[icell] = 0.0;
if (summass == 0.0 || d_cinfo[icell].volume == 0.0) d_vec[icell] = 0.0;
else{
wt = fnum * d_cinfo[icell].weight / d_cinfo[icell].volume;
summv = d_etally(icell,mv);
Expand All @@ -368,7 +368,7 @@ KOKKOS_INLINE_FUNCTION
void ComputePFluxGridKokkos::operator()(TagComputePFluxGrid_post_process_grid_offdiag, const int &icell) const {
double summass, wt;
summass = d_etally(icell,mass);
if (summass == 0.0) d_vec[icell] = 0.0;
if (summass == 0.0 || d_cinfo[icell].volume == 0.0) d_vec[icell] = 0.0;
else{
wt = fnum * d_cinfo[icell].weight / d_cinfo[icell].volume;
d_vec[icell] = wt/nsample * (d_etally(icell,mvv) -
Expand Down
3 changes: 0 additions & 3 deletions src/KOKKOS/compute_sonine_grid_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -225,9 +225,6 @@ void ComputeSonineGridKokkos::operator()(TagComputeSonineGrid_compute_vcom, cons

KOKKOS_INLINE_FUNCTION
void ComputeSonineGridKokkos::operator()(TagComputeSonineGrid_normalize_vcom, const int &icell) const {
const int ispecies = d_particles[icell].ispecies;
const int igroup = d_s2g(imix,ispecies);

double norm;
for (int j=0; j<ngroup; j++) {
norm = d_vcom(icell,j,3);
Expand Down
6 changes: 4 additions & 2 deletions src/KOKKOS/compute_surf_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -210,9 +210,11 @@ int ComputeSurfKokkos::tallyinfo(surfint *&ptr)
int istart = 0;
int iend = nsurf-1;

if (nsurf == 0) return 0;

while (1) {
while (h_surf2tally[istart] != -1 && istart < nsurf-2) istart++;
while (h_surf2tally[iend] == -1 && iend > 0) iend--;
while (istart < nsurf-2 && h_surf2tally[istart] != -1) istart++;
while (iend > 0 && h_surf2tally[iend] == -1) iend--;
if (istart >= iend) {
ntally = istart;
break;
Expand Down
7 changes: 5 additions & 2 deletions src/KOKKOS/compute_thermal_grid_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -166,7 +166,7 @@ void ComputeThermalGridKokkos::operator()(TagComputeThermalGrid_compute_per_grid

const int ispecies = d_particles[i].ispecies;
const int igroup = d_s2g(imix,ispecies);
if (igroup < 0) return;
if (igroup < 0) continue;

const int icell = d_particles[i].icell;

Expand Down Expand Up @@ -281,7 +281,10 @@ void ComputeThermalGridKokkos::operator()(TagComputeThermalGrid_post_process_gri
d_vec[icell] = mvsq - (mvx*mvx + mvy*mvy + mvz*mvz)/mass;
d_vec[icell] *= prefactor;
if (tflag) d_vec[icell] /= ncount;
else d_vec[icell] *= d_cinfo[icell].weight / d_cinfo[icell].volume / nsample;
else {
if (d_cinfo[icell].volume > 0.0) d_vec[icell] *= d_cinfo[icell].weight / d_cinfo[icell].volume / nsample;
else d_vec[icell] = 0.0;
}
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/KOKKOS/create_particles_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -423,7 +423,7 @@ void CreateParticlesKokkos::create_local(bigint np)
// if using per-grid variables or per-grid custom attributes

if (nfix_update_custom)
modify->update_custom(particle->nlocal-1,tempscale*temp_thermal,
modify->update_custom(inew,tempscale*temp_thermal,
tempscale*temp_rot,tempscale*temp_vib,
vstream_update_custom);
}
Expand Down
4 changes: 2 additions & 2 deletions src/KOKKOS/fix_ambipolar_kokkos.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,8 @@ class FixAmbipolarKokkos : public FixAmbipolar {

rand_type rand_gen = rand_pool.get_state();

const double vn = vscale * sqrt(-log(rand_gen.drand()));
const double vr = vscale * sqrt(-log(rand_gen.drand()));
const double vn = vscale * sqrt(-log(1.0 - rand_gen.drand()));
const double vr = vscale * sqrt(-log(1.0 - rand_gen.drand()));
const double theta1 = MathConst::MY_2PI * rand_gen.drand();
const double theta2 = MathConst::MY_2PI * rand_gen.drand();

Expand Down
5 changes: 2 additions & 3 deletions src/KOKKOS/fix_ave_histo_weight_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,7 @@ void FixAveHistoWeightKokkos::calculate_weights()
if (grid->maxlocal > maxvectorwt) {
memoryKK->destroy_kokkos(k_vectorwt,vectorwt);
maxvectorwt = grid->maxlocal;
memory->create(vectorwt,maxvectorwt,"ave/histo/weight:vectorwt");
memoryKK->create_kokkos(k_vectorwt,vectorwt,maxvectorwt,"ave/histo/weight:vectorwt");
}
input->variable->compute_grid(m,vectorwt,1,0);
k_vectorwt.modify_host();
Expand All @@ -268,7 +268,6 @@ void FixAveHistoWeightKokkos::calculate_weights()
// explicit per-particle attributes
// NOTE: need to allocate local storage
} else {
printf("%d, %d\n", which[i] == VARIABLE, kind == PERGRID);
error->all(FLERR,"Fix ave/histo/weight/kokkos option not yet supported");
}
}
Expand Down Expand Up @@ -376,7 +375,7 @@ void FixAveHistoWeightKokkos::bin_particles(

KokkosBase* regionKKBase = dynamic_cast<KokkosBase*>(region);

if (k_match.extent(0) > nmax)
if (k_match.extent(0) < nmax)
MemKK::realloc_kokkos(k_match,"fix_ave_histo_weight:match",nmax);

regionKKBase->match_all_kokkos(k_match);
Expand Down
4 changes: 2 additions & 2 deletions src/KOKKOS/fix_emit_face_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -486,7 +486,7 @@ void FixEmitFaceKokkos::operator()(TagFixEmitFace_perform_task, const int &i, in
d_beta_un(cand) = beta_un;

d_theta(cand) = MY_2PI * rand_gen.drand();
d_vr(cand) = vscale_val * sqrt(-log(rand_gen.drand()));
d_vr(cand) = vscale_val * sqrt(-log(1.0 - rand_gen.drand()));
d_erot(cand) = particle_kk_copy.obj.erot(ispecies,temp_rot,rand_gen);
d_evib(cand) = particle_kk_copy.obj.evib(ispecies,temp_vib,rand_gen);
d_id(cand) = MAXSMALLINT*rand_gen.drand();
Expand Down Expand Up @@ -545,7 +545,7 @@ void FixEmitFaceKokkos::operator()(TagFixEmitFace_perform_task, const int &i, in
d_beta_un(cand) = beta_un;

d_theta(cand) = MY_2PI * rand_gen.drand();
d_vr(cand) = vscale_val * sqrt(-log(rand_gen.drand()));
d_vr(cand) = vscale_val * sqrt(-log(1.0 - rand_gen.drand()));
d_erot(cand) = particle_kk_copy.obj.erot(ispecies,temp_rot,rand_gen);
d_evib(cand) = particle_kk_copy.obj.evib(ispecies,temp_vib,rand_gen);
d_id(cand) = MAXSMALLINT*rand_gen.drand();
Expand Down
4 changes: 2 additions & 2 deletions src/KOKKOS/fix_emit_surf_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -608,7 +608,7 @@ void FixEmitSurfKokkos::operator()(TagFixEmitSurf_perform_task, const int &i, in
else vnmag = beta_un*vscale + indot;

const double theta = MY_2PI * rand_gen.drand();
const double vr = vscale * sqrt(-log(rand_gen.drand()));
const double vr = vscale * sqrt(-log(1.0 - rand_gen.drand()));

double vamag,vbmag;
if (normalflag) {
Expand Down Expand Up @@ -720,7 +720,7 @@ void FixEmitSurfKokkos::operator()(TagFixEmitSurf_perform_task, const int &i, in
else vnmag = beta_un*vscale + indot;

const double theta = MY_2PI * rand_gen.drand();
const double vr = vscale * sqrt(-log(rand_gen.drand()));
const double vr = vscale * sqrt(-log(1.0 - rand_gen.drand()));

double vamag,vbmag;
if (normalflag) {
Expand Down
17 changes: 9 additions & 8 deletions src/KOKKOS/fix_grid_check_kokkos.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,7 @@ void FixGridCheckKokkos::end_of_step()
if (icell < 0 || icell >= nglocal) {
d_particle_problems(i) |= IS_IN_INVALID_CELL;
local_nflag++;
return;
}

// does particle coord match icell bounds
Expand Down Expand Up @@ -169,7 +170,7 @@ void FixGridCheckKokkos::end_of_step()
MPI_Allreduce(&nflag,&all,1,MPI_INT,MPI_SUM,world);
if (all && comm->me == 0) {
char str[128];
sprintf(str,"%d particles were in wrong cells on timestep "
snprintf(str, 128,"%d particles were in wrong cells on timestep "
BIGINT_FORMAT,all,update->ntimestep);
error->warning(FLERR,str);
}
Expand All @@ -183,37 +184,37 @@ void FixGridCheckKokkos::end_of_step()
for (int i = 0; i < nlocal; ++i) {
auto icell = particles[i].icell;
if (h_particle_problems(i) & IS_IN_INVALID_CELL) {
sprintf(str,
"Particle %d,%d on proc %d is in invalid cell " CELLINT_FORMAT
snprintf(str, 128,
"Particle %d,%d on proc %d is in invalid cell index %d"
" on timestep " BIGINT_FORMAT,
i,particles[i].id,comm->me,cells[icell].id,update->ntimestep);
i,particles[i].id,comm->me,icell,update->ntimestep);
error->one(FLERR,str);
}
if (h_particle_problems(i) & IS_OUTSIDE_CELL) {
sprintf(str,
snprintf(str, 128,
"Particle %d,%d on proc %d is outside cell " CELLINT_FORMAT
" on timestep " BIGINT_FORMAT,
i,particles[i].id,comm->me,cells[icell].id,
update->ntimestep);
error->one(FLERR,str);
}
if (h_particle_problems(i) & IS_IN_SPLIT_CELL) {
sprintf(str,
snprintf(str, 128,
"Particle %d,%d on proc %d is in split cell " CELLINT_FORMAT
" on timestep " BIGINT_FORMAT,
i,particles[i].id,comm->me,cells[icell].id,
update->ntimestep);
error->one(FLERR,str);
}
if (h_particle_problems(i) & IS_IN_INTERIOR_CELL) {
sprintf(str,
snprintf(str, 128,
"Particle %d,%d on proc %d is in interior cell " CELLINT_FORMAT
" on timestep " BIGINT_FORMAT,
i,particles[i].id,comm->me,cells[icell].id,update->ntimestep);
error->one(FLERR,str);
}
if (h_particle_problems(i) & IS_IN_ZERO_VOLUME_CELL) {
sprintf(str,
snprintf(str, 128,
"Particle %d,%d on proc %d is in volume=0 cell " CELLINT_FORMAT
" on timestep " BIGINT_FORMAT,
i,particles[i].id,comm->me,cells[icell].id,update->ntimestep);
Expand Down
2 changes: 1 addition & 1 deletion src/KOKKOS/fix_vibmode_kokkos.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ void FixVibmodeKokkos::update_custom_kokkos(int index, double temp_thermal,
rand_type rand_gen = rand_pool.get_state();

for (int imode = 0; imode < nmode; imode++) {
const int ivib = static_cast<int> (-log(rand_gen.drand()) * temp_vib /
const int ivib = static_cast<int> (-log(1.0 - rand_gen.drand()) * temp_vib /
d_species[isp].vibtemp[imode]);
d_vibmode(index,imode) = ivib;
evib += ivib * boltz * d_species[isp].vibtemp[imode];
Expand Down
Loading
Loading