mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-03 12:16:54 +00:00
Code Activity

Merge pull request #8825 from Z3Prover/copilot/fix-reported-issues-8822

Browse source 
Fix CSA-reported undefined behavior and uninitialized variables
This commit is contained in:
Nikolaj Bjorner 2026-03-02 10:03:16 -08:00 • committed by GitHub
commit 94809d413a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
9 changed files with 42 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/act_cache.cpp
View file

@ -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);
});

4
src/ast/rewriter/bit2int.cpp
View file

@ -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));

2
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -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());
}

1
src/math/lp/nla_core.cpp
View file

@ -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) {

2
src/math/simplex/bit_matrix.cpp
View file

@ -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;
}

2
src/muz/rel/dl_sparse_table.h
View file

@ -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<uint64_t>(1)<<length)-1 ),
m_mask( length >= 64 ? ULLONG_MAX : (static_cast<uint64_t>(1)<<length)-1 ),
m_write_mask( ~(m_mask << m_small_offset) ),
m_offset(offset),
m_length(length) {

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;

4
src/util/mpff.cpp
View file

@ -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<uint64_t*>(sig(a) + (m_precision - 2));
return *s >> exp;
return *s >> static_cast<unsigned>(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<unsigned>(exp);
if (is_neg(a))
r = -r;
return r;

2
src/util/sorting_network.h
View file

@ -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);