Skip to content

[Draft PR] Added comments where code changes may be needed - #1238 #1252

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

[Draft PR] Added comments where code changes may be needed - #1238 #1252

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0d3676c
Added comments where code changes may be needed
IamYJLee Oct 27, 2025
0bd72f5
Extend addFnCall to return FnCallResult and handle allocsize
IamYJLee Nov 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 19 additions & 4 deletions ir/instr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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);

Expand Down
1 change: 1 addition & 0 deletions ir/memory.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1717,6 +1717,7 @@ 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?

}

void Memory::markByVal(unsigned bid, bool is_const) {
Expand Down
30 changes: 24 additions & 6 deletions ir/state.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1081,7 +1081,7 @@ expr State::FnCallOutput::refines(const FnCallOutput &rhs,
return ret;
}

StateValue
State::FnCallResult
State::addFnCall(const string &name, vector<StateValue> &&inputs,
vector<PtrInput> &&ptr_inputs,
const Type &out_type, StateValue &&ret_arg,
Expand All @@ -1090,7 +1090,8 @@ State::addFnCall(const string &name, vector<StateValue> &&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;
Expand Down Expand Up @@ -1278,8 +1279,17 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
addUB(I->second.ub);
addNoReturn(I->second.noreturns);
retval = I->second.retval;

optional<expr> 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,
Copy link
Contributor Author

@IamYJLee IamYJLee Nov 3, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would it be okay to skip this part when addFnCall is executed before m.alloc?

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
Expand Down Expand Up @@ -1336,15 +1346,23 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
fn_call_pre &= pre;
if (qvar.isValid())
fn_call_qvars.emplace(std::move(qvar));

// Extract allocation size for noalias functions returning pointers
optional<expr> 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<expr> e,
Expand Down
10 changes: 9 additions & 1 deletion ir/state.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -240,6 +240,14 @@ class State {
smt::expr refines(const FnCallOutput &rhs, const Type &retval_ty) const;
auto operator<=>(const FnCallOutput &rhs) const = default;
};

struct FnCallResult {
StateValue retval;
std::optional<smt::expr> alloc_size;
};

// Add non-deterministic local_blk_size variable member and pending variable to access it

std::map<std::string, std::map<FnCallInput, FnCallOutput>> fn_call_data;
smt::expr fn_call_pre = true;
std::set<smt::expr> fn_call_qvars;
Expand Down Expand Up @@ -308,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<StateValue> &&inputs,
std::vector<PtrInput> &&ptr_inputs,
const Type &out_type,
Expand Down
Loading