fix stack condition for fn calls
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1758,17 +1758,16 @@ static void check_return_value(State &s, StateValue &val, const Type &ty,
const FnAttrs &attrs, bool is_ret_instr) {
if (attrs.has(FnAttrs::NNaN)) {
assert(ty.isFloatType());
- expr nnan = !val.value.isNaN();
- if (is_ret_instr)
- s.addUB(nnan);
- val.non_poison &= move(nnan);
+ s.addUB(val.non_poison.implies(!val.value.isNaN()));
}
if (ty.isPtrType()) {
Pointer p(s.getMemory(), val.value);
- if (is_ret_instr && has_nocapture)
- s.addUB(val.non_poison.implies(!p.isNocapture()));
+ if (is_ret_instr) {
+ s.addUB(val.non_poison.implies(!p.isStackAllocated() &&
+ !p.isNocapture()));
+ }
bool isDeref = attrs.has(FnAttrs::Dereferenceable);
bool isDerefOrNull = attrs.has(FnAttrs::DereferenceableOrNull);
@@ -1779,9 +1778,6 @@ static void check_return_value(State &s, StateValue &val, const Type &ty,
if (isDerefOrNull)
s.addUB(p.isDereferenceable(attrs.derefOrNullBytes, attrs.align)() ||
!p.isNonZero());
-
- if (is_ret_instr && has_alloca)
- s.addUB(p.getAllocType() != Pointer::STACK);
} else if (attrs.has(FnAttrs::Align))
val.non_poison &= p.isAligned(attrs.align);

MODIFY
ir/pointer.cpp
ir/pointer.cpp
@@ -426,6 +426,15 @@ expr Pointer::getAllocType() const {
expr::mkUInt(0, 2));
}
+expr Pointer::isStackAllocated() const {
+ // 1) if a stack object is returned by a callee it's UB
+ // 2) if a stack object is given as argument by the caller, we can upgrade it
+ // to a global object, so we can do POR here.
+ if (!has_alloca || isLocal().isFalse())
+ return false;
+ return getAllocType() == STACK;
+}
+
expr Pointer::isHeapAllocated() const {
assert(MALLOC == 2 && CXX_NEW == 3);
return getAllocType().extract(1, 1) == 1;

MODIFY
ir/pointer.h
ir/pointer.h
@@ -108,6 +108,7 @@ public:
CXX_NEW,
};
smt::expr getAllocType() const;
+ smt::expr isStackAllocated() const;
smt::expr isHeapAllocated() const;
smt::expr isNocapture(bool simplify = true) const;
smt::expr isNoRead() const;

fix stack condition for fn calls