From 8e94cad8abe3c31f7554def389b1660e5237ddb5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 2 Mar 2026 00:13:55 +0000 Subject: [PATCH] Fix static analysis findings: uninitialized vars, bitwise shift UB, garbage values - nla_core.cpp: Initialize j = null_lpvar in is_octagon_term - bit2int.cpp: Initialize sign_p, sign_n, sz_p, sz_n - act_cache.cpp: Initialize debug vars to nullptr - enum2bv_rewriter.cpp: Use unsigned literal in 1u << idx - bit_matrix.cpp: Use unsigned literal in 1u << (n-1) - bit_util.cpp: Guard against bit_shift == 0 in shl/shr - mpff.cpp: Cast exp to unsigned before shifting - sorting_network.h: Guard against bits == 0 - dl_sparse_table.h: Use >= 64 instead of == 64 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/act_cache.cpp | 4 +-- src/ast/rewriter/bit2int.cpp | 4 +-- src/ast/rewriter/enum2bv_rewriter.cpp | 2 +- src/math/lp/nla_core.cpp | 1 + src/math/simplex/bit_matrix.cpp | 2 +- src/muz/rel/dl_sparse_table.h | 2 +- src/util/bit_util.cpp | 43 +++++++++++++++++++-------- src/util/mpff.cpp | 4 +-- src/util/sorting_network.h | 2 +- 9 files changed, 42 insertions(+), 22 deletions(-) diff --git a/src/ast/act_cache.cpp b/src/ast/act_cache.cpp index 223ad2406..dbebb9ee1 100644 --- a/src/ast/act_cache.cpp +++ b/src/ast/act_cache.cpp @@ -173,7 +173,7 @@ void act_cache::insert(expr * k, unsigned offset, expr * v) { DEBUG_CODE(expected_tag = 0;); } DEBUG_CODE({ - expr * v2; + expr * v2 = nullptr; SASSERT(m_table.find(e, v2)); SASSERT(v == UNTAG(expr*, v2)); SASSERT(expected_tag == GET_TAG(v2)); @@ -195,7 +195,7 @@ expr * act_cache::find(expr * k, unsigned offset) { SASSERT(m_unused > 0); m_unused--; DEBUG_CODE({ - expr * v; + expr * v = nullptr; SASSERT(m_table.find(e, v)); SASSERT(GET_TAG(v) == 1); }); diff --git a/src/ast/rewriter/bit2int.cpp b/src/ast/rewriter/bit2int.cpp index 3bf921fae..71e126c48 100644 --- a/src/ast/rewriter/bit2int.cpp +++ b/src/ast/rewriter/bit2int.cpp @@ -354,8 +354,8 @@ void bit2int::visit(app* n) { // // (pos1 - neg1) mod e2 = (pos1 + (e2 - (neg1 mod e2))) mod e2 // - unsigned sz_p, sz_n, sz; - bool sign_p, sign_n; + unsigned sz_p = 0, sz_n = 0, sz; + bool sign_p = false, sign_n = false; expr_ref tmp_p(m), tmp_n(m); VERIFY(extract_bv(pos1, sz_p, sign_p, tmp_p)); VERIFY(extract_bv(neg1, sz_n, sign_n, tmp_n)); diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index a8171c230..d2c5fd122 100644 --- a/src/ast/rewriter/enum2bv_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -64,7 +64,7 @@ struct enum2bv_rewriter::imp { unsigned bv_size = get_bv_size(s); sort_ref bv_sort(m_bv.mk_sort(bv_size), m); if (is_unate(s)) - return m_bv.mk_numeral(rational((1 << idx) - 1), bv_sort.get()); + return m_bv.mk_numeral(rational((1u << idx) - 1), bv_sort.get()); else return m_bv.mk_numeral(rational(idx), bv_sort.get()); } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 34f2f0a1b..c7a29e9a7 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -539,6 +539,7 @@ bool core::is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar & bool seen_minus = false; bool seen_plus = false; i = null_lpvar; + j = null_lpvar; for(lp::lar_term::ival p : t) { const auto & c = p.coeff(); if (c == 1) { diff --git a/src/math/simplex/bit_matrix.cpp b/src/math/simplex/bit_matrix.cpp index 097dd4396..401b941fb 100644 --- a/src/math/simplex/bit_matrix.cpp +++ b/src/math/simplex/bit_matrix.cpp @@ -125,7 +125,7 @@ unsigned_vector bit_matrix::gray(unsigned n) { auto v = gray(n-1); auto w = v; w.reverse(); - for (auto & u : v) u |= (1 << (n-1)); + for (auto & u : v) u |= (1u << (n-1)); v.append(w); return v; } diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h index 330e4d440..c548e3ff0 100644 --- a/src/muz/rel/dl_sparse_table.h +++ b/src/muz/rel/dl_sparse_table.h @@ -328,7 +328,7 @@ namespace datalog { column_info(unsigned offset, unsigned length) : m_big_offset(offset / 8), m_small_offset(offset % 8), - m_mask( length == 64 ? ULLONG_MAX : (static_cast(1)<= 64 ? ULLONG_MAX : (static_cast(1)< src, unsigned k, std::span dst) { } } else { + if (bit_shift == 0) { + if (src_sz > dst_sz) + src_sz = dst_sz; + for (size_t i = 0; i < src_sz; ++i) + dst[i] = src[i]; + for (size_t i = src_sz; i < dst_sz; ++i) + dst[i] = 0; + return; + } unsigned comp_shift = (8 * sizeof(unsigned)) - bit_shift; unsigned prev = 0; if (src_sz > dst_sz) @@ -278,7 +287,11 @@ void shr(std::span src, unsigned k, std::span dst) { } else { SASSERT(new_sz == sz); - SASSERT(bit_shift != 0); + if (bit_shift == 0) { + for (size_t i = 0; i < sz; ++i) + dst[i] = src[i]; + return; + } unsigned i = 0; for (; i < new_sz - 1; ++i) { dst[i] = src[i]; @@ -327,20 +340,26 @@ void shr(std::span src, unsigned k, std::span dst) { } else { SASSERT(new_sz == src_sz); - SASSERT(bit_shift != 0); - auto sz = new_sz; - if (new_sz > dst_sz) - sz = dst_sz; - unsigned i = 0; - for (; i < sz - 1; ++i) { + if (bit_shift == 0) { + auto sz = std::min(new_sz, dst_sz); + for (size_t i = 0; i < sz; ++i) + dst[i] = src[i]; + } + else { + auto sz = new_sz; + if (new_sz > dst_sz) + sz = dst_sz; + unsigned i = 0; + for (; i < sz - 1; ++i) { + dst[i] = src[i]; + dst[i] >>= bit_shift; + dst[i] |= (src[i+1] << comp_shift); + } dst[i] = src[i]; dst[i] >>= bit_shift; - dst[i] |= (src[i+1] << comp_shift); + if (new_sz > dst_sz) + dst[i] |= (src[i+1] << comp_shift); } - dst[i] = src[i]; - dst[i] >>= bit_shift; - if (new_sz > dst_sz) - dst[i] |= (src[i+1] << comp_shift); } for (auto i = new_sz; i < dst_sz; ++i) dst[i] = 0; diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index a0851bad6..c2c058696 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -161,7 +161,7 @@ uint64_t mpff_manager::get_uint64(mpff const & a) const { int exp = -a.m_exponent - sizeof(unsigned) * 8 * (m_precision - 2); SASSERT(exp >= 0); uint64_t * s = reinterpret_cast(sig(a) + (m_precision - 2)); - return *s >> exp; + return *s >> static_cast(exp); } int64_t mpff_manager::get_int64(mpff const & a) const { @@ -175,7 +175,7 @@ int64_t mpff_manager::get_int64(mpff const & a) const { return INT64_MIN; } else { - int64_t r = *s >> exp; + int64_t r = *s >> static_cast(exp); if (is_neg(a)) r = -r; return r; diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index e77757aea..0a91f7a85 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -412,7 +412,7 @@ Notes: bits++; w_max >>= 1; } - unsigned pow = (1ul << (bits-1)); + unsigned pow = bits > 0 ? (1u << (bits-1)) : 0; unsigned a = (k + pow - 1) / pow; // a*pow >= k SASSERT(a*pow >= k); SASSERT((a-1)*pow < k);