mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-04 04:30:23 +00:00
Code Activity

Fix static analysis findings: uninitialized vars, bitwise shift UB, garbage values

Browse source 
- 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>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-02 00:13:55 +00:00
parent 122ee94935
commit 8e94cad8ab
9 changed files with 42 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

43
src/util/bit_util.cpp
View file

@ -214,6 +214,15 @@ void shl(std::span<unsigned const> src, unsigned k, std::span<unsigned> 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<unsigned const> src, unsigned k, std::span<unsigned> 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<unsigned const> src, unsigned k, std::span<unsigned> 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;