simplify path constraint of sink BBs
noticed by Juneyoung Lee
MODIFY
ir/state.cpp
ir/state.cpp
@@ -134,13 +134,9 @@ bool State::startBB(const BasicBlock &bb) {
domain.path = path();
domain.UB.add(*UB());
-
- if (!domain)
- return false;
-
memory = *in_memory();
- return true;
+ return domain;
}
void State::addJump(const BasicBlock &dst0, expr &&cond) {
@@ -322,7 +318,7 @@ expr State::sinkDomain() const {
OrExpr ret;
for (auto &[src, data] : I->second) {
(void)src;
- ret.add(data.first());
+ ret.add(data.first.path());
}
return ret();
}
@@ -363,7 +359,7 @@ void State::syncSEdataWithSrc(const State &src) {
void State::mkAxioms(State &tgt) {
assert(isSource() && !tgt.isSource());
- memory.mkAxioms(tgt.memory);
+ returnMemory().mkAxioms(tgt.returnMemory());
// axioms for function calls
// We would potentially need to do refinement check of tgt x tgt, but it

DELETE
tests/alive-tv/infinite-loop.src.ll
-define void @f() {
- br label %loop
-loop:
- ; It is UB to have infinite loop without side effect in C, but
- ; it is not clear it also applies to LLVM.
- ; Here is an unknown function call g() inside this loop, so it doesn't apply
- ; here.
- call void @g()
- br label %loop
-}
-
-declare void @g()

DELETE
tests/alive-tv/infinite-loop.tgt.ll
-define void @f() {
- ret void
-}

simplify path constraint of sink BBs
noticed by Juneyoung Lee