From ed6844a0df0e3f5609a1715a87d3f922d99d641c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 22 Dec 2024 12:35:54 +0000 Subject: [PATCH] don't emit the poison axiom for the null block --- ir/memory.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/ir/memory.cpp b/ir/memory.cpp index 5de63d342..1b55bd63b 100644 --- a/ir/memory.cpp +++ b/ir/memory.cpp @@ -40,6 +40,10 @@ using namespace util; //--- Functions for non-local block analysis based on bid ---// +static bool skip_null() { + return has_null_block && !null_is_dereferenceable; +} + // If include_tgt is true, return true if bid is a global var existing in target // only as well static bool is_globalvar(unsigned bid, bool include_tgt) { @@ -1511,12 +1515,11 @@ Memory::Memory(State &state) next_nonlocal_bid = has_null_block + num_globals_src + num_ptrinputs + has_fncall; - bool skip_null = has_null_block && !null_is_dereferenceable; - if (skip_null) + if (skip_null()) non_local_block_val.emplace_back(); // TODO: should skip initialization of fully initialized constants - for (unsigned bid = skip_null, e = numNonlocals(); bid != e; ++bid) { + for (unsigned bid = skip_null(), e = numNonlocals(); bid != e; ++bid) { non_local_block_val.emplace_back(mk_block_val_array(bid)); } @@ -1543,7 +1546,7 @@ Memory::Memory(State &state) stored_pointers.resize(numNonlocals()); // Initialize a memory block for null pointer. - if (skip_null) { + if (skip_null()) { auto zero = expr::mkUInt(0, bits_size_t); alloc(&zero, bits_byte / 8, GLOBAL, false, false, 0); } @@ -1569,7 +1572,7 @@ void Memory::mkAxioms(const Memory &tgt) const { for (auto m_ptr : { this, &tgt }) { auto &m = const_cast(*m_ptr); auto old_vals = m.non_local_block_val; - for (unsigned i = 0, e = old_vals.size(); i != e; ++i) { + for (unsigned i = skip_null(), e = old_vals.size(); i != e; ++i) { m.non_local_block_val.at(i).val = m.mk_block_val_array(i); } m.mkNonlocalValAxioms(false);