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 1 commit
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
4 changes: 4 additions & 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,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) {
Expand Down Expand Up @@ -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)
Expand Down
5 changes: 5 additions & 0 deletions ir/state.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,13 +233,18 @@ class State {
Memory::CallState callstate;
std::vector<Memory::FnRetData> ret_data;

// Add non-deterministic local_blk_size variable member

Copy link
Member

@nunoplopes nunoplopes Oct 27, 2025

Choose a reason for hiding this comment

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

yes, it goes here

Copy link
Contributor Author

@IamYJLee IamYJLee Oct 28, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

Thank you for your feedback, Nuno.
When managing the non-deterministic variable for local_blk_size in the FnCallOutput structure, should the condition inside FnCall::toSMT be modified to perform both m.alloc and addFnCall?
Or would it be better to handle this by adding a new function to the State class that accesses FnCallOutput after performing m.alloc?

Copy link
Member

@nunoplopes nunoplopes Oct 28, 2025

Choose a reason for hiding this comment

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

Uhm, maybe we can change addFnCall to return the size, and then pass that size to alloc() in FnCall::toSMT.
Actually, that way we don't even need to add another field to FnCallOutput, since the output of the function is the size. We won't store the pointer, since that's local.

Copy link
Contributor Author

@IamYJLee IamYJLee Oct 29, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

I don’t fully understand your comment yet.
In this case, the @myalloc function is processed through FnCall::toSMT.
To explain in more detail — inside FnCall::toSMT, m.alloc is called first, but addFnCall is not called.
Meanwhile, the @llvm.objectsize function is processed through Ternary::toSMT.

@myalloc 
    ⇒ FnCall::toSMT → m.alloc (does not call addFnCall)
@llvm.objectsize 
    ⇒ Ternary::toSMT

So I’m wondering how the return value from addFnCall should be passed in this situation.
By the way, when I tried calling addFnCall before m.alloc during the processing of @myalloc, I got the following error message:

Assertion failed: (has_write_fncall || num_inaccessiblememonly_fns > 0),
function get_fncallmem_bid, file memory.cpp, line 73.

Actually, I don’t think this error is particularly meaningful.

Copy link
Member

@nunoplopes nunoplopes Oct 29, 2025

Choose a reason for hiding this comment

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

we need to call addFnCall, but change the return type to be the size of the allocation. Then take that variable and pass it to m.alloc.

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.

I added the addFnCall function before calling m.alloc(). (0bd72f5)
However, I encountered the following assertion in get_fncallmem_bid() (memory.cpp):

Assertion failed: (has_write_fncall || num_inaccessiblememonly_fns > 0), function get_fncallmem_bid, file memory.cpp, line 75.
Stack dump without symbol names (ensure you have llvm-symbolizer in your PATH or set the environment var `LLVM_SYMBOLIZER_PATH` to point to it):
0  libLLVMSupport.dylib     0x000000010affae8c llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) + 56
1  libLLVMSupport.dylib     0x000000010aff8470 llvm::sys::RunSignalHandlers() + 64
2  libLLVMSupport.dylib     0x000000010affb984 SignalHandler(int, __siginfo*, void*) + 360
3  libsystem_platform.dylib 0x000000019de54624 _sigtramp + 56
4  libsystem_pthread.dylib  0x000000019de1a88c pthread_kill + 296
5  libsystem_c.dylib        0x000000019dd23c60 abort + 124
6  libsystem_c.dylib        0x000000019dd22eec err + 0
7  alive-tv                 0x00000001025303a0 IR::Memory::setState(IR::Memory::CallState const&, IR::SMTMemoryAccess const&, std::__1::vector<IR::PtrInput, std::__1::allocator<IR::PtrInput>> const&, unsigned int) + 3208
8  alive-tv                 0x0000000102552ff0 IR::State::addFnCall(std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>> const&, std::__1::vector<IR::StateValue, std::__1::allocator<IR::StateValue>>&&, std::__1::vector<IR::PtrInput, std::__1::allocator<IR::PtrInput>>&&, IR::Type const&, IR::StateValue&&, IR::Type const*, std::__1::vector<IR::StateValue, std::__1::allocator<IR::StateValue>>&&, IR::FnAttrs const&, unsigned int) + 6516

...

According to the error log, has_write_fncall is false.
When allocsize is present, has_write_fncall remains false.
If has_write_fncall is true, it means that the function call writes to global memory (i.e., not inaccessible-only).
Therefore, I think has_write_fncall should be true when both allocsize and allockind are present — or even when only allockind is present.

Also, since Bid is added in Memory::mkFnRet, creating a block during this process seems to result in duplication.

Could you please advise on this case?

Copy link
Contributor Author

@IamYJLee IamYJLee Nov 11, 2025

Choose a reason for hiding this comment

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

@nunoplopes Could you please review this when you get a chance?

FnCallOutput replace(const StateValue &retval) const;

static FnCallOutput mkIf(const smt::expr &cond, const FnCallOutput &then,
const FnCallOutput &els);
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<std::string, std::map<FnCallInput, FnCallOutput>> fn_call_data;
smt::expr fn_call_pre = true;
std::set<smt::expr> fn_call_qvars;
Expand Down
Loading