Support lifetime.end
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1845,13 +1845,14 @@ void Free::rauw(const Value &what, Value &with) {
}
void Free::print(std::ostream &os) const {
- os << "free " << *ptr;
+ os << "free " << *ptr << (heaponly ? "" : " unconstrained");
}
StateValue Free::toSMT(State &s) const {
auto &[p, np] = s[*ptr];
s.addUB(np);
- s.getMemory().free(p);
+ // If not heaponly, don't encode constraints
+ s.getMemory().free(p, !heaponly);
return {};
}
@@ -1860,7 +1861,7 @@ expr Free::getTypeConstraints(const Function &f) const {
}
unique_ptr<Instr> Free::dup(const string &suffix) const {
- return make_unique<Free>(*ptr);
+ return make_unique<Free>(*ptr, heaponly);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -437,8 +437,10 @@ public:
class Free final : public Instr {
Value *ptr;
+ bool heaponly;
public:
- Free(Value &ptr) : Instr(Type::voidTy, "free"), ptr(&ptr) {}
+ Free(Value &ptr, bool heaponly = true) : Instr(Type::voidTy, "free"),
+ ptr(&ptr), heaponly(heaponly) {}
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -844,9 +844,10 @@ void Memory::start_lifetime(const expr &ptr_local) {
// TODO: encode disjointness of lock blocks if lifetime starts
}
-void Memory::free(const expr &ptr) {
+void Memory::free(const expr &ptr, bool unconstrained) {
assert(!memory_unused() && has_free);
Pointer p(*this, ptr);
+ if (!unconstrained)
state->addUB(p.isNull() || (p.get_offset() == 0 &&
p.is_block_alive() &&
p.get_alloc_type() == Pointer::MALLOC));

MODIFY
ir/memory.h
ir/memory.h
@@ -215,7 +215,10 @@ public:
// Start lifetime of a local block.
void start_lifetime(const smt::expr &ptr_local);
- void free(const smt::expr &ptr);
+
+ // If unconstrained is true, the pointer offset, liveness, and block kind
+ // are not checked.
+ void free(const smt::expr &ptr, bool unconstrained);
void store(const smt::expr &ptr, const StateValue &val, const Type &type,
unsigned align, bool deref_check = true);

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -584,11 +584,7 @@ public:
if (!llvm::isa<llvm::AllocaInst>(llvm::GetUnderlyingObject(
i.getOperand(1), DL())))
return error(i);
- // TODO: a dummy instruction
- static int lifetime_end_dummy = 0;
- string name = "__unused_le_" + to_string(lifetime_end_dummy++);
- RETURN_IDENTIFIER(make_unique<UnaryOp>(b->getType(), move(name), *b,
- UnaryOp::Copy));
+ RETURN_IDENTIFIER(make_unique<Free>(*b, false));
}
// do nothing intrinsics

ADD
tests/alive-tv/memory/lifetime-2.src.ll
+declare void @llvm.lifetime.start.p0i8(i64, i8*)
+declare void @llvm.lifetime.end.p0i8(i64, i8*)
+
+define i32 @f() {
+ %p = alloca i32
+
+ %p0 = bitcast i32* %p to i8*
+ call void @llvm.lifetime.start.p0i8(i64 4, i8* %p0)
+ call void @llvm.lifetime.end.p0i8(i64 4, i8* %p0)
+
+ store i32 10, i32* %p
+ %v = load i32, i32* %p
+
+ ret i32 %v
+}
+

ADD
tests/alive-tv/memory/lifetime-2.tgt.ll
+declare void @llvm.lifetime.start.p0i8(i64, i8*)
+declare void @llvm.lifetime.end.p0i8(i64, i8*)
+
+define i32 @f() {
+ %p = alloca i32
+
+ %p0 = bitcast i32* %p to i8*
+ call void @llvm.lifetime.start.p0i8(i64 4, i8* %p0)
+ call void @llvm.lifetime.end.p0i8(i64 4, i8* %p0)
+
+ store i32 10, i32* %p
+
+ ret i32 undef
+}
+

ADD
tests/alive-tv/memory/lifetime-noub.src.ll
+declare void @llvm.lifetime.start.p0i8(i64, i8*)
+declare void @llvm.lifetime.end.p0i8(i64, i8*)
+
+define void @f() {
+ %p = alloca i32
+
+ %p0 = bitcast i32* %p to i8*
+ %p1 = getelementptr i8, i8* %p0, i32 1
+ call void @llvm.lifetime.start.p0i8(i64 4, i8* %p1)
+ call void @llvm.lifetime.end.p0i8(i64 4, i8* %p1)
+
+ ret void
+}
+
+; ERROR: Source is more defined than target

ADD
tests/alive-tv/memory/lifetime-noub.tgt.ll
+declare void @llvm.lifetime.start.p0i8(i64, i8*)
+declare void @llvm.lifetime.end.p0i8(i64, i8*)
+
+define void @f() {
+ %p = alloca i32
+
+ %p0 = bitcast i32* %p to i8*
+ %p1 = getelementptr i8, i8* %p0, i32 1
+ call void @llvm.lifetime.start.p0i8(i64 4, i8* %p1)
+ call void @llvm.lifetime.end.p0i8(i64 4, i8* %p1)
+
+ unreachable
+}
+

Support lifetime.end (#239)