From 0d3676cbf5dd7db8172d554c8faac34425667c3c Mon Sep 17 00:00:00 2001 From: LeeYoungJoon Date: Mon, 27 Oct 2025 15:10:04 +0900 Subject: [PATCH 1/2] Added comments where code changes may be needed --- ir/memory.cpp | 4 ++++ ir/state.h | 5 +++++ 2 files changed, 9 insertions(+) diff --git a/ir/memory.cpp b/ir/memory.cpp index 96b213baa..2e34671ee 100644 --- a/ir/memory.cpp +++ b/ir/memory.cpp @@ -1717,6 +1717,8 @@ void Memory::syncWithSrc(const Memory &src) { next_nonlocal_bid = src.next_nonlocal_bid; ptr_alias = src.ptr_alias; // TODO: copy alias info for fn return ptrs from src? + + // Add synchronizing non-deterministic variables for local_blk_size } void Memory::markByVal(unsigned bid, bool is_const) { @@ -2261,6 +2263,8 @@ Memory::alloc(const expr *size, uint64_t align, BlockKind blockKind, if (size) (is_local ? local_blk_size : non_local_blk_size) .replace(short_bid, std::move(size_zext)); + // If size is unknown in the above condition, add a non-det variable for size + // and add it as a member of the FnCallOutput structure with the key being the function name and bid (is_local ? local_blk_align : non_local_blk_align) .add(short_bid, std::move(align_expr)); (is_local ? local_blk_kind : non_local_blk_kind) diff --git a/ir/state.h b/ir/state.h index 1cfd6a906..957d0b8b6 100644 --- a/ir/state.h +++ b/ir/state.h @@ -233,6 +233,8 @@ class State { Memory::CallState callstate; std::vector ret_data; + // Add non-deterministic local_blk_size variable member + FnCallOutput replace(const StateValue &retval) const; static FnCallOutput mkIf(const smt::expr &cond, const FnCallOutput &then, @@ -240,6 +242,9 @@ class State { smt::expr refines(const FnCallOutput &rhs, const Type &retval_ty) const; auto operator<=>(const FnCallOutput &rhs) const = default; }; + + // Add non-deterministic local_blk_size variable member and pending variable to access it + std::map> fn_call_data; smt::expr fn_call_pre = true; std::set fn_call_qvars; From 0bd72f5c2ea1ee1c4ceacdcc51487fe7987a70ad Mon Sep 17 00:00:00 2001 From: LeeYoungJoon Date: Mon, 3 Nov 2025 14:45:37 +0900 Subject: [PATCH 2/2] Extend addFnCall to return FnCallResult and handle allocsize - Changed addFnCall return type from StateValue to FnCallResult (retval + optional alloc_size) - For allocators without allocsize, call addFnCall to obtain allocation size before memory setup --- ir/instr.cpp | 23 +++++++++++++++++++---- ir/memory.cpp | 3 --- ir/state.cpp | 30 ++++++++++++++++++++++++------ ir/state.h | 9 ++++++--- 4 files changed, 49 insertions(+), 16 deletions(-) diff --git a/ir/instr.cpp b/ir/instr.cpp index 806666725..7d4841ac2 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -2682,9 +2682,24 @@ StateValue FnCall::toSMT(State &s) const { }; if (attrs.has(AllocKind::Alloc) || - attrs.has(AllocKind::Realloc) || - attrs.has(FnAttrs::AllocSize)) { - auto [size, np_size] = attrs.computeAllocSize(s, args); + attrs.has(AllocKind::Realloc)) { + + smt::expr size; + smt::expr np_size; + + if (!attrs.has(FnAttrs::AllocSize)) { + auto result = s.addFnCall(std::move(fnName_mangled).str(), std::move(inputs), + std::move(ptr_inputs), getType(), std::move(ret_val), + ret_arg_ty, std::move(ret_vals), attrs, indirect_hash); + auto retval =std::move(result.retval); + size = std::move(result.alloc_size.value()); + np_size = expr(true); + } else { + auto result = attrs.computeAllocSize(s, args); + size = std::move(result.first); + np_size = std::move(result.second); + } + expr nonnull = attrs.isNonNull() ? expr(true) : expr::mkBoolVar("malloc_never_fails"); // FIXME: alloc-family below @@ -2755,7 +2770,7 @@ StateValue FnCall::toSMT(State &s) const { return {}; } - auto ret = s.addFnCall(std::move(fnName_mangled).str(), std::move(inputs), + auto [ret, alloc_size] = s.addFnCall(std::move(fnName_mangled).str(), std::move(inputs), std::move(ptr_inputs), getType(), std::move(ret_val), ret_arg_ty, std::move(ret_vals), attrs, indirect_hash); diff --git a/ir/memory.cpp b/ir/memory.cpp index 2e34671ee..96d046cab 100644 --- a/ir/memory.cpp +++ b/ir/memory.cpp @@ -1718,7 +1718,6 @@ void Memory::syncWithSrc(const Memory &src) { ptr_alias = src.ptr_alias; // TODO: copy alias info for fn return ptrs from src? - // Add synchronizing non-deterministic variables for local_blk_size } void Memory::markByVal(unsigned bid, bool is_const) { @@ -2263,8 +2262,6 @@ Memory::alloc(const expr *size, uint64_t align, BlockKind blockKind, if (size) (is_local ? local_blk_size : non_local_blk_size) .replace(short_bid, std::move(size_zext)); - // If size is unknown in the above condition, add a non-det variable for size - // and add it as a member of the FnCallOutput structure with the key being the function name and bid (is_local ? local_blk_align : non_local_blk_align) .add(short_bid, std::move(align_expr)); (is_local ? local_blk_kind : non_local_blk_kind) diff --git a/ir/state.cpp b/ir/state.cpp index 8f863a2cc..3015a72ce 100644 --- a/ir/state.cpp +++ b/ir/state.cpp @@ -1081,7 +1081,7 @@ expr State::FnCallOutput::refines(const FnCallOutput &rhs, return ret; } -StateValue +State::FnCallResult State::addFnCall(const string &name, vector &&inputs, vector &&ptr_inputs, const Type &out_type, StateValue &&ret_arg, @@ -1090,7 +1090,8 @@ State::addFnCall(const string &name, vector &&inputs, bool noret = attrs.has(FnAttrs::NoReturn); bool willret = attrs.has(FnAttrs::WillReturn); bool noundef = attrs.has(FnAttrs::NoUndef); - bool noalias = attrs.has(FnAttrs::NoAlias); + bool noalias = (attrs.has(FnAttrs::NoAlias)) || + (attrs.has(AllocKind::Alloc) && !attrs.has(FnAttrs::AllocSize)); bool is_indirect = name.starts_with("#indirect_call"); expr fn_ptr_bid; @@ -1278,8 +1279,17 @@ State::addFnCall(const string &name, vector &&inputs, addUB(I->second.ub); addNoReturn(I->second.noreturns); retval = I->second.retval; + + optional alloc_size; + if (noalias && out_type.isPtrType() && !I->second.ret_data.empty()) { + alloc_size = I->second.ret_data[0].size; + } + memory.setState(I->second.callstate, memaccess, I->first.args_ptr, inaccessible_bid); + + + return { std::move(retval), std::move(alloc_size) }; } else { // target: this fn call must match one from the source, otherwise it's UB @@ -1336,15 +1346,23 @@ State::addFnCall(const string &name, vector &&inputs, fn_call_pre &= pre; if (qvar.isValid()) fn_call_qvars.emplace(std::move(qvar)); + + // Extract allocation size for noalias functions returning pointers + optional alloc_size; + if (noalias && out_type.isPtrType() && !d.ret_data.empty()) { + alloc_size = d.ret_data[0].size; + } + + analysis.ranges_fn_calls.inc(name, memaccess); + return { std::move(retval), std::move(alloc_size) }; } else { addUB(expr(false)); retval = out_type.getDummyValue(false); + + analysis.ranges_fn_calls.inc(name, memaccess); + return { std::move(retval), std::nullopt }; } } - - analysis.ranges_fn_calls.inc(name, memaccess); - - return retval; } void State::doesApproximation(string &&name, optional e, diff --git a/ir/state.h b/ir/state.h index 957d0b8b6..7b0ddbdad 100644 --- a/ir/state.h +++ b/ir/state.h @@ -233,8 +233,6 @@ class State { Memory::CallState callstate; std::vector ret_data; - // Add non-deterministic local_blk_size variable member - FnCallOutput replace(const StateValue &retval) const; static FnCallOutput mkIf(const smt::expr &cond, const FnCallOutput &then, @@ -243,6 +241,11 @@ class State { auto operator<=>(const FnCallOutput &rhs) const = default; }; + struct FnCallResult { + StateValue retval; + std::optional alloc_size; + }; + // Add non-deterministic local_blk_size variable member and pending variable to access it std::map> fn_call_data; @@ -313,7 +316,7 @@ class State { void addNoReturn(const smt::expr &cond); bool isViablePath() const { return domain.UB; } - StateValue + FnCallResult addFnCall(const std::string &name, std::vector &&inputs, std::vector &&ptr_inputs, const Type &out_type,