Deal with the byval case

AliveToolkit · Oct 17, 2021 · a3c793d · a3c793d
1 parent e27fccc
commit a3c793d
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 8 deletions.
diff --git a/ir/memory.cpp b/ir/memory.cpp
@@ -1902,7 +1902,8 @@ expr Memory::blockPropertiesRefined(const Pointer &src, const Pointer &tgt)
 
   return src.isBlockAlive() == tgt.isBlockAlive() &&
          src.blockSize() == tgt.blockSize() &&
-         src.getAllocType() == tgt.getAllocType() &&
+         ((src.isLocal() && tgt.isByval()) ||
+          src.getAllocType() == tgt.getAllocType()) &&
          aligned;
 }
 

diff --git a/ir/pointer.cpp b/ir/pointer.cpp
@@ -497,7 +497,6 @@ expr Pointer::encodeLoadedByteRefined(
 expr Pointer::encodeLocalPtrRefinement(
     const Pointer &other, set<expr> &undefs) const {
   expr tgt_bid = other.getShortBid();
-
   expr ofs = expr::mkFreshVar("localblk_ofs", expr::mkUInt(0, bits_for_offset));
   Pointer this_ofs = *this + ofs;
   Pointer other_ofs = other + ofs;
@@ -506,15 +505,19 @@ expr Pointer::encodeLocalPtrRefinement(
   bool is_const_bid = this_ofs.getShortBid().isUInt(bid_const) &&
                       tgt_bid.isUInt(bid_tgt_const);
   expr blkrefined;
-  if (is_const_bid)
-    // Look into the bytes
+  if (is_const_bid && this->isByval().isFalse() && other.isByval().isFalse()) {
+    // Look into the bytes.
+    // If this or other pointer is byval, blockRefined cannot be used because
+    // it requires both bids to be local or nonlocal
+    // In the byval case, return the approximated result by simply checking
+    // the block properties in the else clause below
     blkrefined = m.blockRefined(*this, other, (unsigned)bid_const,
                                 (unsigned)bid_tgt_const, undefs);
-  else
+  } else
     blkrefined = m.blockPropertiesRefined(*this, other);
 
-  return other.isLocal() && getOffset() == other.getOffset() &&
-      move(blkrefined);
+  return (other.isLocal() || other.isByval()) &&
+      getOffset() == other.getOffset() && move(blkrefined);
 }
 
 expr Pointer::encodeByValArgRefinement(
@@ -541,7 +544,8 @@ expr Pointer::fninputRefined(const Pointer &other, set<expr> &undef,
 
   expr islocal = isLocal();
   expr local = false;
-  if (!islocal.isFalse() && !other.isLocal().isFalse())
+  if (!islocal.isFalse() &&
+      (!other.isLocal().isFalse() || !other.isByval().isFalse()))
     local = encodeLocalPtrRefinement(other, undef);
 
   local = (other.isLocal() || other.isByval()) && local;

diff --git a/ir/pointer.h b/ir/pointer.h
@@ -37,8 +37,11 @@ class Pointer {
 
   smt::expr encodeLoadedByteRefined(const Pointer &other,
                                     std::set<smt::expr> &undefs) const;
+  // Encode the refinement between
+  // (src ptr, tgt ptr) = (local, local) or (local, byval ptr)
   smt::expr encodeLocalPtrRefinement(const Pointer &other,
                                      std::set<smt::expr> &undefs) const;
+  // Encode the refinement when two ptrs are given as byval args
   smt::expr encodeByValArgRefinement(const Pointer &otherByval,
                                      std::set<smt::expr> &undefs,
                                      unsigned byval_size) const;