memory: further simplifications to nocapture
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -24,5 +24,6 @@ bool has_readonly;
bool has_dead_allocas;
bool does_int_mem_access;
bool does_ptr_mem_access;
+bool does_ptr_store;
}

MODIFY
ir/globals.h
ir/globals.h
@@ -52,5 +52,6 @@ extern bool has_dead_allocas;
/// Whether the programs do memory accesses that load/store int/ptrs
extern bool does_int_mem_access;
extern bool does_ptr_mem_access;
+extern bool does_ptr_store;
}

MODIFY
ir/memory.cpp
ir/memory.cpp
#include "ir/state.h"
#include "ir/value.h"
#include "util/compiler.h"
+#include <string>
using namespace IR;
using namespace smt;
using namespace std;
using namespace util;
-static bool did_pointer_store = false;
static unsigned ptr_next_idx = 0;
static expr concat_if(const expr &ifvalid, expr &&e) {
@@ -23,6 +23,11 @@ static expr prepend_if(const expr &pre, expr &&e, bool prepend) {
return prepend ? pre.concat(e) : move(e);
}
+static string local_name(const State *s, const char *name) {
+ string n = name;
+ return n + (s->isSource() ? "_src" : "_tgt");
+}
+
namespace IR {
Byte::Byte(const Memory &m, expr &&byterepr) : m(m), p(move(byterepr)) {
@@ -363,9 +368,7 @@ expr Pointer::get_value(const char *name, const FunctionExpr &local_fn,
if (auto val = nonlocal_fn.lookup(bid))
non_local = *val;
else {
- string uf = name;
- if (src_name)
- uf += m.state->isSource() ? "_src" : "_tgt";
+ string uf = src_name ? local_name(m.state, name) : name;
non_local = expr::mkUF(uf.c_str(), { bid }, ret_type);
}
@@ -654,7 +657,7 @@ expr Pointer::block_val_refined(const Pointer &other) const {
expr is_ptr = val.is_ptr();
expr is_ptr2 = val2.is_ptr();
expr ptr_cnstr;
- if (!did_pointer_store || is_ptr.isFalse() || is_ptr2.isFalse()) {
+ if (!does_ptr_store || is_ptr.isFalse() || is_ptr2.isFalse()) {
ptr_cnstr = val == val2;
} else {
ptr_cnstr = val2.ptr_nonpoison() && val.ptr().refined(val2.ptr());
@@ -712,7 +715,7 @@ expr Pointer::is_byval() const {
}
expr Pointer::is_nocapture() const {
- if (!has_nocapture || !did_pointer_store)
+ if (!has_nocapture)
return false;
// local pointers can't be no-capture
@@ -756,7 +759,7 @@ ostream& operator<<(ostream &os, const Pointer &p) {
os << ", offset=";
p.get_offset().printSigned(os);
- if (bits_for_ptrattrs) {
+ if (bits_for_ptrattrs && !p.get_attrs().isZero()) {
os << ", attrs=";
p.get_attrs().printUnsigned(os);
}
@@ -766,10 +769,6 @@ ostream& operator<<(ostream &os, const Pointer &p) {
static void store(const Pointer &p, const expr &val, expr &local,
expr &non_local, bool index_bid = false) {
- // check if we are potentially storing a pointer
- if (!index_bid)
- did_pointer_store |= !Byte(p.getMemory(), expr(val)).is_ptr().isFalse();
-
auto is_local = p.is_local();
auto idx = index_bid ? p.get_short_bid() : p.short_ptr();
local = expr::mkIf(is_local, local.store(idx, val), local);
@@ -954,7 +953,6 @@ void Memory::mkAxioms(const Memory &other) const {
void Memory::resetGlobalData() {
resetLocalBids();
last_nonlocal_bid = 1;
- did_pointer_store = false;
}
void Memory::resetLocalBids() {
@@ -1318,7 +1316,11 @@ pair<expr,Pointer> Memory::refined(const Memory &other) const {
}
expr Memory::check_nocapture() const {
- auto ofs = expr::mkFreshVar("ofs", expr::mkUInt(0, bits_for_offset));
+ if (!does_ptr_store)
+ return true;
+
+ auto name = local_name(state, "#offset_nocapture");
+ auto ofs = expr::mkVar(name.c_str(), bits_for_offset);
expr res(true);
for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
@@ -1326,13 +1328,13 @@ expr Memory::check_nocapture() const {
Byte b(*this, non_local_block_val.load(p.short_ptr()));
Pointer loadp(*this, b.ptr_value());
res &= p.is_block_alive().implies(
- expr::mkForAll({ ofs },
- (b.is_ptr() && b.ptr_nonpoison()).implies(!loadp.is_nocapture())));
+ (b.is_ptr() && b.ptr_nonpoison()).implies(!loadp.is_nocapture()));
}
+ if (!res.isTrue())
+ state->addQuantVar(ofs);
return res;
}
-
Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
assert(then.state == els.state);
Memory ret(then);
@@ -1388,8 +1390,7 @@ ostream& operator<<(ostream &os, const Memory &m) {
P("BLOCK SIZE:", local_blk_size, non_local_blk_size);
P("BLOCK ALIGN:", local_blk_align, non_local_blk_align);
P("BLOCK KIND:", local_blk_kind, non_local_blk_kind);
- return os << "LOCAL BLOCK ADDR: " << m.local_blk_addr
- << "\nDid pointer store: " << did_pointer_store << '\n';
+ return os << "LOCAL BLOCK ADDR: " << m.local_blk_addr << '\n';
}
}

MODIFY
ir/memory.h
ir/memory.h
#include "smt/exprs.h"
#include <optional>
#include <ostream>
-#include <string>
#include <utility>
#include <vector>

ADD
tests/alive-tv/attrs/nocapture-fail.src.ll
+; ERROR: Source is more defined than target
+
+@x = global i8* null
+
+define void @f(i8* nocapture %p) {
+ %poison = getelementptr inbounds i8, i8* null, i32 1
+ store i8* %poison, i8** @x
+ ret void
+}

ADD
tests/alive-tv/attrs/nocapture-fail.tgt.ll
+@x = global i8* null
+
+define void @f(i8* nocapture %p) {
+ store i8* %p, i8** @x
+ ret void
+}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -484,6 +484,7 @@ static void calculateAndInitConstants(Transform &t) {
if (auto st = dynamic_cast<const Store *>(&inst)) {
value_ty = &st->getValue()->getType();
align = st->getAlign();
+ does_ptr_store |= hasPtr(*value_ty);
} else if (auto ld = dynamic_cast<const Load *>(&inst)) {
value_ty = &ld->getType();
align = ld->getAlign();
@@ -530,6 +531,7 @@ static void calculateAndInitConstants(Transform &t) {
has_ptr2int = false;
has_malloc = false;
has_free = false;
+ does_ptr_store = false;
does_ptr_mem_access = false;
does_int_mem_access = false;
@@ -614,6 +616,7 @@ static void calculateAndInitConstants(Transform &t) {
"has_ptr2int: " << has_ptr2int << "\n"
"has_malloc: " << has_malloc << "\n"
"has_free: " << has_free << "\n"
+ "does_ptr_store: " << does_ptr_store << "\n"
"does_ptr_mem_access: " << does_ptr_mem_access << "\n"
"does_int_mem_access: " << does_int_mem_access << "\n"
;

memory: further simplifications to nocapture