revert changes to int2ptr. the approximation produced false positives
back to a simple and safe abstraction
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1717,15 +1717,11 @@ expr Memory::ptr2int(const expr &ptr) const {
expr Memory::int2ptr(const expr &val) const {
assert(!memory_unused() && observesAddresses());
- // FIXME
- // Note that this is an over-approximation, as it doesn't take escaped
- // pointers into account. Plus it's non-determinisc over overlapping ptrs.
- // We don't mark it as an approximation as Z3 always puts the int2ptr in the
- // partial model in practice, plus LLVM's reasoning power around int2ptr
- // is very limited.
- expr fn = expr::mkUF("int2ptr", { val }, Pointer::mkNullPointer(*this)());
- state->addPre(ptr2int(fn) == val);
- return fn;
+ // TODO
+ expr null = Pointer::mkNullPointer(*this).release();
+ expr fn = expr::mkUF("int2ptr", { val }, null);
+ state->doesApproximation("inttoptr", fn);
+ return expr::mkIf(val == 0, null, fn);
}
expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,

revert changes to int2ptr. the approximation produced false positives
back to a simple and safe abstraction