Stricter refinement check for nonlocals
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -778,10 +778,8 @@ expr Pointer::refined(const Pointer &other) const {
// TODO: this induces an infinite loop
//local &= block_refined(other);
- return isBlockAlive().implies(
- other.isBlockAlive() &&
- expr::mkIf(isLocal(), isHeapAllocated().implies(local),
- *this == other));
+ return expr::mkIf(isLocal(), isHeapAllocated().implies(local), *this == other)
+ && isBlockAlive().implies(other.isBlockAlive());
}
expr Pointer::fninputRefined(const Pointer &other, set<expr> &undef,
@@ -809,9 +807,8 @@ expr Pointer::fninputRefined(const Pointer &other, set<expr> &undef,
// TODO: this induces an infinite loop
// block_refined(other);
- return isBlockAlive().implies(
- other.isBlockAlive() &&
- expr::mkIf(isLocal(), local, *this == other));
+ return expr::mkIf(isLocal(), local, *this == other)
+ && isBlockAlive().implies(other.isBlockAlive());
}
expr Pointer::isWritable() const {

ADD
tests/alive-tv/refinement/null-glb-fail.srctgt.ll
+@glb = global i8 0
+
+define i8* @src(i8* %p) {
+entry:
+ %c = icmp eq i8* %p, null
+ br i1 %c, label %if.then, label %if.end
+if.then:
+ ret i8* %p
+if.end:
+ ret i8* @glb
+}
+
+define i8* @tgt(i8* %p) {
+ ret i8* @glb
+}
+
+; ERROR: Value mismatch

Stricter refinement check for nonlocals (#447)