add extremely basic loop support by ignoring back-edges
MODIFY
ir/function.cpp
ir/function.cpp
@@ -88,6 +88,11 @@ const BasicBlock& Function::getBB(string_view name) const {
return BBs.at(string(name));
}
+const BasicBlock* Function::getBBIfExists(std::string_view name) const {
+ auto I = BBs.find(string(name));
+ return I != BBs.end() ? &I->second : nullptr;
+}
+
void Function::removeBB(BasicBlock &BB) {
BBs.erase(BB.getName());

MODIFY
ir/function.h
ir/function.h
@@ -81,6 +81,7 @@ public:
const BasicBlock& getFirstBB() const { return *BB_order[0]; }
BasicBlock& getBB(std::string_view name, bool push_front = false);
const BasicBlock& getBB(std::string_view name) const;
+ const BasicBlock* getBBIfExists(std::string_view name) const;
void removeBB(BasicBlock &BB);
void addConstant(std::unique_ptr<Value> &&c);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -15,7 +15,7 @@ using namespace std;
namespace IR {
-State::State(const Function &f, bool source)
+State::State(Function &f, bool source)
: f(f), source(source), memory(*this),
return_val(f.getType().getDummyValue(false)), return_memory(memory) {}
@@ -122,13 +122,14 @@ bool State::startBB(const BasicBlock &bb) {
return true;
}
-void State::addJump(const BasicBlock &dst, expr &&cond) {
- if (seen_bbs.count(&dst))
- throw AliveException("Loops are not supported yet! Skipping function.",
- false);
+void State::addJump(const BasicBlock &dst0, expr &&cond) {
+ auto dst = &dst0;
+ if (seen_bbs.count(dst)) {
+ dst = &f.getBB("#sink");
+ }
cond &= domain.first;
- auto p = predecessor_data[&dst].try_emplace(current_bb, DomainTy({}, {}),
+ auto p = predecessor_data[dst].try_emplace(current_bb, DomainTy({}, {}),
memory);
if (!p.second) {
p.first->second.second = Memory::mkIf(cond, memory, p.first->second.second);
@@ -300,6 +301,23 @@ void State::finishInitializer() {
memory.finishInitialization();
}
+expr State::sinkDomain() const {
+ auto bb = f.getBBIfExists("#sink");
+ if (!bb)
+ return false;
+
+ auto I = predecessor_data.find(bb);
+ if (I == predecessor_data.end())
+ return false;
+
+ expr ret(false);
+ for (auto &[src, data] : I->second) {
+ (void)src;
+ ret |= data.first.first;
+ }
+ return ret;
+}
+
void State::addGlobalVarBid(const string &glbvar, unsigned bid) {
ENSURE(glbvar_bids.emplace(glbvar, make_pair(bid, true)).second);
}

MODIFY
ir/state.h
ir/state.h
@@ -31,7 +31,8 @@ public:
using DomainTy = std::pair<smt::expr, std::set<smt::expr>>;
private:
- const Function &f;
+ // TODO: make this const again
+ Function &f;
bool source;
bool disable_undef_rewrite = false;
bool is_initialization_phase = true;
@@ -80,7 +81,7 @@ private:
fn_call_data;
public:
- State(const Function &f, bool source);
+ State(Function &f, bool source);
static void resetGlobals();
@@ -129,6 +130,7 @@ public:
const auto& getQuantVars() const { return quantified_vars; }
auto& returnDomain() const { return return_domain; }
+ smt::expr sinkDomain() const;
Memory returnMemory() const { return *return_memory(); }
std::pair<StateValue, const std::set<smt::expr>&> returnVal() const {

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -88,6 +88,7 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
const llvm::TargetLibraryInfo &TLI;
vector<llvm::Instruction*> i_constexprs;
vector<string_view> gvnamesInSrc;
+ vector<tuple<Phi*, llvm::PHINode*, unsigned>> todo_phis;
using RetTy = unique_ptr<Instr>;
@@ -484,10 +485,11 @@ public:
auto phi = make_unique<Phi>(*ty, value_name(i));
for (unsigned idx = 0, e = i.getNumIncomingValues(); idx != e; ++idx) {
- auto op = get_operand(i.getIncomingValue(idx));
- if (!op)
- return error(i);
+ if (auto op = get_operand(i.getIncomingValue(idx))) {
phi->addValue(*op, value_name(*i.getIncomingBlock(idx)));
+ } else {
+ todo_phis.emplace_back(phi.get(), &i, idx);
+ }
}
RETURN_IDENTIFIER(move(phi));
@@ -804,6 +806,16 @@ public:
}
}
+ // patch phi nodes for recursive defs
+ for (auto &[phi, llvm_i, idx] : todo_phis) {
+ auto op = get_operand(llvm_i->getIncomingValue(idx));
+ if (!op) {
+ error(*llvm_i);
+ return {};
+ }
+ phi->addValue(*op, value_name(*llvm_i->getIncomingBlock(idx)));
+ }
+
auto getGlobalVariable =
[this](const string &name) -> llvm::GlobalVariable* {
auto M = f.getParent();

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -35,8 +35,7 @@ unordered_map<const llvm::Type*, unique_ptr<Type>> type_cache;
unsigned type_id_counter; // for unamed types
Function *current_fn;
-unordered_map<const llvm::Value*, Value*> identifiers;
-unordered_map<const llvm::GlobalVariable*, GlobalVariable*> globalvars;
+unordered_map<const llvm::Value*, Value*> value_cache;
ostream *out;
@@ -205,18 +204,25 @@ Value* make_intconst(uint64_t val, int bits) {
return ret;
}
+#define RETURN_CACHE(val) \
+ do { \
+ auto val_cpy = val; \
+ ENSURE(value_cache.emplace(v, val_cpy).second); \
+ return val_cpy; \
+ } while (0)
+
Value* get_operand(llvm::Value *v,
function<Value*(llvm::ConstantExpr*)> constexpr_conv,
function<Value*(AggregateValue*)> copy_inserter) {
- if (isa<llvm::Instruction>(v) || isa<llvm::Argument>(v))
- return identifiers[v];
+ if (auto I = value_cache.find(v);
+ I != value_cache.end())
+ return I->second;
auto ty = llvm_type2alive(v->getType());
if (!ty)
return nullptr;
- // TODO: cache these?
if (auto cnst = dyn_cast<llvm::ConstantInt>(v)) {
unique_ptr<IntConst> c;
if (cnst->getBitWidth() <= 64)
@@ -225,7 +231,7 @@ Value* get_operand(llvm::Value *v,
c = make_unique<IntConst>(*ty, cnst->getValue().toString(10, false));
auto ret = c.get();
current_fn->addConstant(move(c));
- return ret;
+ RETURN_CACHE(ret);
}
if (auto cnst = dyn_cast<llvm::ConstantFP>(v)) {
@@ -247,28 +253,24 @@ Value* get_operand(llvm::Value *v,
}
auto ret = c.get();
current_fn->addConstant(move(c));
- return ret;
+ RETURN_CACHE(ret);
}
if (isa<llvm::UndefValue>(v)) {
auto val = make_unique<UndefValue>(*ty);
auto ret = val.get();
current_fn->addUndef(move(val));
- return ret;
+ RETURN_CACHE(ret);
}
if (isa<llvm::ConstantPointerNull>(v)) {
auto val = make_unique<NullPointerValue>(*ty);
auto ret = val.get();
current_fn->addConstant(move(val));
- return ret;
+ RETURN_CACHE(ret);
}
if (auto gv = dyn_cast<llvm::GlobalVariable>(v)) {
- auto &gvar = globalvars[gv];
- if (gvar)
- return gvar;
-
if (hasOpaqueType(gv->getValueType()))
// TODO: Global variable of opaque type is not supported.
return nullptr;
@@ -294,9 +296,9 @@ Value* get_operand(llvm::Value *v,
}
auto val = make_unique<GlobalVariable>(*ty, move(name), size, align,
gv->isConstant());
- gvar = val.get();
+ auto gvar = val.get();
current_fn->addConstant(move(val));
- return gvar;
+ RETURN_CACHE(gvar);
}
auto fillAggregateValues = [&](AggregateType *aty,
@@ -363,7 +365,7 @@ Value* get_operand(llvm::Value *v,
auto val = make_unique<AggregateValue>(*ty, move(vals));
auto ret = val.get();
current_fn->addConstant(move(val));
- return ret;
+ RETURN_CACHE(ret);
}
if (auto cexpr = dyn_cast<llvm::ConstantExpr>(v)) {
@@ -375,7 +377,7 @@ Value* get_operand(llvm::Value *v,
void add_identifier(const llvm::Value &llvm, Value &v) {
- identifiers.emplace(&llvm, &v);
+ value_cache.emplace(&llvm, &v);
}
@@ -402,9 +404,8 @@ void init_llvm_utils(ostream &os, const llvm::DataLayout &dataLayout) {
void reset_state(Function &f) {
current_fn = &f;
- identifiers.clear();
+ value_cache.clear();
value_names.clear();
- globalvars.clear();
value_id_counter = 0;
}

MODIFY
tests/alive-tv/infinite-loop.src.ll
tests/alive-tv/infinite-loop.src.ll
@@ -10,6 +10,3 @@ loop:
}
declare void @g()
-
-; Currently loops are not supported, so following error appears.
-; ERROR: Loops are not supported yet! Skipping function.

MODIFY
tests/alive-tv/memory/alloca-removal.src.ll
tests/alive-tv/memory/alloca-removal.src.ll
-; TEST-ARGS: -smt-to=5000
+; TEST-ARGS: -disable-poison-input
define i8* @f(i64 %size) {
entry:

ADD
tests/alive-tv/phi.src.ll
+define i32 @f(i32 %n) {
+entry:
+ %cmp = icmp eq i32 %n, 0
+ br i1 %cmp, label %end, label %loop
+
+loop:
+ %i = phi i32 [ %i2, %loop ], [ 0, %entry ]
+ %r = phi i32 [ %r2, %loop ], [ 0, %entry ]
+ %i2 = add i32 %i, 1
+ %r2 = add i32 %r, 2
+ %c2 = icmp eq i32 %i2, %n
+ br i1 %c2, label %end, label %loop
+
+end:
+ %ret = phi i32 [ 0, %entry ], [ %r2, %loop ]
+ ret i32 %ret
+}
+
+define i32 @f2(i32 %n) {
+entry:
+ %cmp = icmp eq i32 %n, 0
+ br i1 %cmp, label %end, label %loop
+
+loop:
+ %i = phi i32 [ %i2, %loop ], [ 0, %entry ]
+ %r = phi i32 [ %r2, %loop ], [ 0, %entry ]
+ %i2 = add i32 %i, 1
+ %r2 = add i32 %r, 2
+ %c2 = icmp eq i32 %i2, %n
+ br i1 %c2, label %end, label %loop
+
+end:
+ %ret = phi i32 [ 0, %entry ], [ %r2, %loop ]
+ ret i32 %ret
+}

ADD
tests/alive-tv/phi.tgt.ll
+define i32 @f(i32 %n) {
+ %r = shl i32 %n, 1
+ ret i32 %r
+}
+
+define i32 @f2(i32 %n) {
+entry:
+ %cmp = icmp eq i32 %n, 0
+ br i1 %cmp, label %end, label %loop
+
+end:
+ %ret = phi i32 [ 0, %entry ], [ %r2, %loop ]
+ ret i32 %ret
+
+loop:
+ %i = phi i32 [ %i2, %loop ], [ 0, %entry ]
+ %r = phi i32 [ %r2, %loop ], [ 0, %entry ]
+ %i2 = add i32 %i, 1
+ %r2 = add i32 %r, 2
+ %c2 = icmp eq i32 %i2, %n
+ br i1 %c2, label %end, label %loop
+}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -316,7 +316,8 @@ static void check_refinement(Errors &errs, Transform &t,
expr axioms_expr = axioms();
expr dom = dom_a && dom_b;
- expr oom_src = src_state.getOOM()();
+ pre_tgt &= src_state.getOOM()();
+ pre_tgt &= !tgt_state.sinkDomain();
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
@@ -325,8 +326,7 @@ static void check_refinement(Errors &errs, Transform &t,
auto [memory_cnstr, ptr_refinement0] = src_mem.refined(tgt_mem);
auto &ptr_refinement = ptr_refinement0;
- if (check_expr(axioms_expr && (oom_src && pre_src && pre_tgt))
- .isUnsat()) {
+ if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) {
errs.add("Precondition is always false", false);
return;
}
@@ -341,7 +341,7 @@ static void check_refinement(Errors &errs, Transform &t,
if (refines.isFalse())
return move(refines);
- auto fml = pre_tgt && oom_src && pre_src.implies(refines);
+ auto fml = pre_tgt && pre_src.implies(refines);
return axioms_expr && preprocess(t, qvars, uvars, move(fml));
};

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -30,7 +30,9 @@ void sym_exec(State &s) {
first = false;
}
- for (auto &bb : f.getBBs()) {
+ // TODO: remove copy
+ auto BBs = f.getBBs();
+ for (auto &bb : BBs) {
if (!s.startBB(*bb))
continue;

add extremely basic loop support by ignoring back-edges