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

Author: IamYJLee

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

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)

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<StateValue> &&inputs,
                  vector<PtrInput> &&ptr_inputs,
                  const Type &out_type, StateValue &&ret_arg,
@@ -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;
@@ -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,
                     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<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,

ir/state.h

@@ -233,8 +233,6 @@ class State {
     Memory::CallState callstate;
     std::vector<Memory::FnRetData> 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<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;
@@ -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<StateValue> &&inputs,
               std::vector<PtrInput> &&ptr_inputs,
               const Type &out_type,