Add StartLifetime instruction
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1808,6 +1808,34 @@ unique_ptr<Instr> Calloc::dup(const string &suffix) const {
}
+vector<Value*> StartLifetime::operands() const {
+ return { ptr };
+}
+
+void StartLifetime::rauw(const Value &what, Value &with) {
+ RAUW(ptr);
+}
+
+void StartLifetime::print(std::ostream &os) const {
+ os << "start_lifetime " << *ptr;
+}
+
+StateValue StartLifetime::toSMT(State &s) const {
+ auto &[p, np] = s[*ptr];
+ s.addUB(np);
+ s.getMemory().start_lifetime(p);
+ return {};
+}
+
+expr StartLifetime::getTypeConstraints(const Function &f) const {
+ return ptr->getType().enforcePtrType();
+}
+
+unique_ptr<Instr> StartLifetime::dup(const string &suffix) const {
+ return make_unique<StartLifetime>(*ptr);
+}
+
+
vector<Value*> Free::operands() const {
return { ptr };
}

MODIFY
ir/instr.h
ir/instr.h
@@ -420,6 +420,21 @@ public:
};
+class StartLifetime final : public Instr {
+ Value *ptr;
+public:
+ StartLifetime(Value &ptr) : Instr(Type::voidTy, "start_lifetime"),
+ ptr(&ptr) {}
+
+ std::vector<Value*> operands() const override;
+ void rauw(const Value &what, Value &with) override;
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+ std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+};
+
+
class Free final : public Instr {
Value *ptr;
public:

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -837,6 +837,13 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
return expr::mkIf(allocated, p(), Pointer::mkNullPointer(*this)());
}
+void Memory::start_lifetime(const expr &ptr_local) {
+ assert(!memory_unused());
+ Pointer p(*this, ptr_local);
+ local_block_liveness = local_block_liveness.store(p.get_short_bid(), true);
+ // TODO: encode disjointness of lock blocks if lifetime starts
+}
+
void Memory::free(const expr &ptr) {
assert(!memory_unused() && has_free);
Pointer p(*this, ptr);

MODIFY
ir/memory.h
ir/memory.h
@@ -213,6 +213,8 @@ public:
unsigned *bid_out = nullptr,
const smt::expr &precond = true);
+ // Start lifetime of a local block.
+ void start_lifetime(const smt::expr &ptr_local);
void free(const smt::expr &ptr);
void store(const smt::expr &ptr, const StateValue &val, const Type &type,

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -576,11 +576,7 @@ public:
if (!llvm::isa<llvm::AllocaInst>(llvm::GetUnderlyingObject(
i.getOperand(1), DL())))
return error(i);
- // TODO: a dummy instruction
- static int lifetime_start_dummy = 0;
- string name = "__unused_ls_" + to_string(lifetime_start_dummy++);
- RETURN_IDENTIFIER(make_unique<UnaryOp>(b->getType(), move(name), *b,
- UnaryOp::Copy));
+ RETURN_IDENTIFIER(make_unique<StartLifetime>(*b));
}
case llvm::Intrinsic::lifetime_end:
{

Add StartLifetime instruction (#240)