Skip to content

Commit

Permalink
deref check
Browse files Browse the repository at this point in the history
  • Loading branch information
nunoplopes committed Dec 20, 2023
1 parent 5996523 commit a377de0
Showing 1 changed file with 6 additions and 5 deletions.
11 changes: 6 additions & 5 deletions ir/pointer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -529,16 +529,16 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
DisjointExpr<expr> UB(expr(false)), is_aligned(expr(false)), all_ptrs;

for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, 3)) {
Pointer ptr(m, ptr_expr);
auto [ptr, inboundsd] = Pointer(m, ptr_expr).toLogical();
auto [ub, aligned] = ::is_dereferenceable(ptr, bytes_off, bytes, align,
iswrite, ignore_accessability);

// record pointer if not definitely unfeasible
if (!ub.isFalse() && !aligned.isFalse() && !ptr.blockSize().isZero())
all_ptrs.add(std::move(ptr).release(), domain);

UB.add(std::move(ub), domain);
is_aligned.add(std::move(aligned), domain);
UB.add(ub && inboundsd, domain);
is_aligned.add(std::move(aligned), std::move(domain));
}

AndExpr exprs;
Expand Down Expand Up @@ -833,16 +833,17 @@ Pointer::mkIf(const expr &cond, const Pointer &then, const Pointer &els) {
}

ostream& operator<<(ostream &os, const Pointer &p) {
auto logical = p.isLogical();

if (p.isNull().isTrue())
return os << "null";
return os << (logical.isFalse() ? "0x0" : "null");

#define P(field, fn) \
if (field.isConst()) \
field.fn(os); \
else \
os << field

auto logical = p.isLogical();
os << (logical.isFalse() ? "phy-ptr(" : "pointer(");

if (!logical.isFalse()) {
Expand Down

0 comments on commit a377de0

Please sign in to comment.