fix bug ptr refinement for fn input cannot change from global to local unless it's byval
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -588,12 +588,9 @@ expr Pointer::fninput_refined(const Pointer &other) const {
expr size2 = other.block_size();
expr off2 = other.get_offset();
- // We allow alloca->anything, but not local malloc->alloca/non-local ptr
- // because we can't go from a free'able pointer to a non-free'able
expr local
= expr::mkIf(is_heap_allocated(),
- other.is_local() && other.is_heap_allocated() && off == off2 &&
- size2.uge(size),
+ other.is_heap_allocated() && off == off2 && size2.uge(size),
// must maintain same dereferenceability before & after
expr::mkIf(off.sle(-1),
@@ -604,6 +601,7 @@ expr Pointer::fninput_refined(const Pointer &other) const {
(size2 - off2).uge(size - off),
off2.sgt(size2) && off == off2 &&
size2.uge(size))));
+ local = (other.is_local() || other.is_byval()) && local;
// TODO: this induces an infinite loop
// block_refined(other);
@@ -675,6 +673,15 @@ expr Pointer::is_writable() const {
return is_local() || non_local;
}
+expr Pointer::is_byval() const {
+ auto this_bid = get_short_bid();
+ expr non_local(false);
+ for (auto bid : m.byval_blks) {
+ non_local |= this_bid == bid;
+ }
+ return !is_local() && non_local;
+}
+
Pointer Pointer::mkNullPointer(const Memory &m) {
assert(num_nonlocals > 0);
// A null pointer points to block 0.
@@ -902,6 +909,10 @@ void Memory::resetLocalBids() {
ptr_next_idx = 0;
}
+void Memory::markByVal(unsigned bid) {
+ byval_blks.emplace_back(bid);
+}
+
expr Memory::mkInput(const char *name, unsigned attributes) const {
Pointer p(*this,
prepend_if(expr::mkUInt(0, 1),
@@ -1249,6 +1260,8 @@ pair<expr,Pointer> Memory::refined(const Memory &other) const {
expr bid_expr = expr::mkUInt(bid, bits_for_bid);
Pointer p(*this, bid_expr, offset);
Pointer q(other, p());
+ if ((p.is_byval() && q.is_byval()).isTrue())
+ continue;
ret &= (ptr_bid == bid_expr).implies(p.block_refined(q));
}
return { move(ret), move(ptr) };
@@ -1275,6 +1288,8 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
ret.non_local_blk_size.add(els.non_local_blk_size);
ret.non_local_blk_align.add(els.non_local_blk_align);
ret.non_local_blk_kind.add(els.non_local_blk_kind);
+ ret.byval_blks.insert(ret.byval_blks.end(), els.byval_blks.begin(),
+ els.byval_blks.end());
return ret;
}
@@ -1285,13 +1300,13 @@ bool Memory::operator<(const Memory &rhs) const {
non_local_block_liveness, local_block_liveness, local_blk_addr,
local_blk_size, local_blk_align, local_blk_kind,
non_local_blk_nonwritable, non_local_blk_size, non_local_blk_align,
- non_local_blk_kind) <
+ non_local_blk_kind, byval_blks) <
tie(rhs.non_local_block_val, rhs.local_block_val,
rhs.non_local_block_liveness, rhs.local_block_liveness,
rhs.local_blk_addr, rhs.local_blk_size, rhs.local_blk_align,
rhs.local_blk_kind, rhs.non_local_blk_nonwritable,
rhs.non_local_blk_size, rhs.non_local_blk_align,
- rhs.non_local_blk_kind);
+ rhs.non_local_blk_kind, rhs.byval_blks);
}
#define P(msg, local, nonlocal) \

MODIFY
ir/memory.h
ir/memory.h
@@ -142,6 +142,7 @@ public:
const smt::expr &len2) const;
smt::expr is_block_alive() const;
smt::expr is_writable() const;
+ smt::expr is_byval() const;
enum AllocType {
NON_HEAP,
@@ -185,6 +186,8 @@ class Memory {
smt::FunctionExpr non_local_blk_align;
smt::FunctionExpr non_local_blk_kind;
+ std::vector<unsigned> byval_blks;
+
public:
enum BlockKind {
HEAP, STACK, GLOBAL, CONSTGLOBAL
@@ -197,6 +200,7 @@ public:
static void resetGlobalData();
static void resetLocalBids();
+ void markByVal(unsigned bid);
smt::expr mkInput(const char *name, unsigned attributes) const;
std::pair<smt::expr, smt::expr> mkUndefInput(unsigned attributes) const;
smt::expr mkFnRet(const char *name) const;

MODIFY
ir/value.cpp
ir/value.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/instr.h"
+#include "ir/globals.h"
#include "ir/value.h"
#include "smt/expr.h"
#include "util/compiler.h"
@@ -83,29 +84,33 @@ void GlobalVariable::print(ostream &os) const {
<< " bytes, align " << align;
}
-StateValue GlobalVariable::toSMT(State &s) const {
- auto sizeexpr = expr::mkUInt(allocsize, 64);
- expr ptrval;
- unsigned glbvar_bid;
+static expr get_global(State &s, const string &name, const expr &size,
+ unsigned align, bool isconst, unsigned &bid) {
+ expr ptr;
bool allocated;
auto blkkind = isconst ? Memory::CONSTGLOBAL : Memory::GLOBAL;
- if (s.hasGlobalVarBid(getName(), glbvar_bid, allocated)) {
+ if (s.hasGlobalVarBid(name, bid, allocated)) {
if (!allocated) {
// Use the same block id that is used by src
assert(!s.isSource());
- ptrval = s.getMemory().alloc(sizeexpr, align, blkkind, true, true,
- glbvar_bid).first;
- s.markGlobalAsAllocated(getName());
+ ptr = s.getMemory().alloc(size, align, blkkind, true, true, bid).first;
+ s.markGlobalAsAllocated(name);
} else {
- ptrval = Pointer(s.getMemory(), glbvar_bid, false).release();
+ ptr = Pointer(s.getMemory(), bid, false).release();
}
} else {
- ptrval = s.getMemory().alloc(sizeexpr, align, blkkind, true, true, nullopt,
- &glbvar_bid).first;
- s.addGlobalVarBid(getName(), glbvar_bid);
+ ptr = s.getMemory().alloc(size, align, blkkind, true, true, nullopt,
+ &bid).first;
+ s.addGlobalVarBid(name, bid);
+ }
+ return ptr;
}
- return { move(ptrval), true };
+
+StateValue GlobalVariable::toSMT(State &s) const {
+ unsigned bid;
+ expr size = expr::mkUInt(allocsize, bits_size_t);
+ return { get_global(s, getName(), size, align, isconst, bid), true };
}
@@ -155,6 +160,8 @@ static string attr_str(unsigned attributes) {
string ret;
if (attributes & Input::NonNull)
ret += "nonnull ";
+ if (attributes & Input::ByVal)
+ ret += "byval ";
return ret;
}
@@ -174,7 +181,16 @@ StateValue Input::toSMT(State &s) const {
// 00: normal, 01: undef, else: poison
expr type = getTyVar();
- auto val = getType().mkInput(s, smt_name.c_str(), attributes);
+ expr val;
+ if (attributes & ByVal) {
+ unsigned bid;
+ string sz_name = getName() + "#size";
+ expr size = expr::mkVar(sz_name.c_str(), bits_size_t-1).zext(1);
+ val = get_global(s, getName(), size, 1, false, bid);
+ s.getMemory().markByVal(bid);
+ } else {
+ val = getType().mkInput(s, smt_name.c_str(), attributes);
+ }
if (!config::disable_undef_input) {
auto [undef, vars] = getType().mkUndefInput(s, attributes);

MODIFY
ir/value.h
ir/value.h
@@ -109,7 +109,7 @@ public:
class Input final : public Value {
public:
- enum Attributes { None = 0, NonNull = 1<<0 };
+ enum Attribute { None = 0, NonNull = 1<<0, ByVal = 1<<1 };
private:
std::string smt_name;
unsigned attributes;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -738,6 +738,10 @@ public:
// they don't change
continue;
+ case llvm::Attribute::ByVal:
+ attrs |= Input::ByVal;
+ continue;
+
case llvm::Attribute::NonNull:
attrs |= Input::NonNull;
continue;

MODIFY
tests/alive-tv/call.src.ll
tests/alive-tv/call.src.ll
@@ -28,7 +28,7 @@ define i8 @f5() {
ret i8 %b
}
-define i8 @f6(i8* %p) {
+define i8 @f6(i8* byval %p) {
%a = alloca i8
call void @llvm.memcpy.p0i8.p0i8.i64(i8* %a, i8* %p, i64 1, i1 false)
%b = call i8 @g(i8* %a)

MODIFY
tests/alive-tv/call.tgt.ll
tests/alive-tv/call.tgt.ll
@@ -28,7 +28,7 @@ define i8 @f5() {
ret i8 %b
}
-define i8 @f6(i8* %p) {
+define i8 @f6(i8* byval %p) {
%b = call i8 @g(i8* %p)
ret i8 %b
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -464,8 +464,7 @@ static void calculateAndInitConstants(Transform &t) {
}
unsigned num_ptrinputs = 0;
- const auto &inputs = t.src.getInputs();
- for (auto &arg : inputs) {
+ for (auto &arg : t.src.getInputs()) {
num_ptrinputs += num_ptrs(arg.getType());
}

fix bug #227: ptr refinement for fn input cannot change from global to local unless it's byval