implement pointer comparison
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -118,7 +118,7 @@ static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
const expr &bp, bool sign) {
auto bits = b.bits();
s.addUB(bp);
- s.addUB(b != expr::mkUInt(0, bits));
+ s.addUB(b != 0);
if (sign)
s.addUB((ap && a != expr::IntSMin(bits)) || b != expr::mkInt(-1, bits));
}
@@ -183,9 +183,7 @@ StateValue BinOp::toSMT(State &s) const {
case Shl:
{
val = a << b;
-
- auto bits = b.bits();
- not_poison &= b.ult(expr::mkUInt(bits, bits));
+ not_poison &= b.ult(b.bits());
if (flags & NSW)
not_poison &= a.shl_no_soverflow(b);
@@ -195,9 +193,7 @@ StateValue BinOp::toSMT(State &s) const {
}
case AShr: {
val = a.ashr(b);
-
- auto bits = b.bits();
- not_poison &= b.ult(expr::mkUInt(bits, bits));
+ not_poison &= b.ult(b.bits());
if (flags & Exact)
not_poison &= a.ashr_exact(b);
@@ -205,9 +201,7 @@ StateValue BinOp::toSMT(State &s) const {
}
case LShr: {
val = a.lshr(b);
-
- auto bits = b.bits();
- not_poison &= b.ult(expr::mkUInt(bits, bits));
+ not_poison &= b.ult(b.bits());
if (flags & Exact)
not_poison &= a.lshr_exact(b);
@@ -493,7 +487,8 @@ StateValue ConversionOp::toSMT(State &s) const {
break;
case BitCast:
if ((getType().isIntType() && val.getType().isIntType()) ||
- (getType().isFloatType() && val.getType().isFloatType()))
+ (getType().isFloatType() && val.getType().isFloatType()) ||
+ (getType().isPtrType() && val.getType().isPtrType()))
newval = v;
else if (getType().isIntType() && val.getType().isFloatType())
newval = v.float2BV();
@@ -785,7 +780,31 @@ void ICmp::print(ostream &os) const {
StateValue ICmp::toSMT(State &s) const {
auto &[av, ap] = s[a];
auto &[bv, bp] = s[b];
- expr val;
+ expr val, non_poison = ap && bp;
+
+ if (a.getType().isPtrType()) {
+ Pointer lhs(s.getMemory(), av);
+ Pointer rhs(s.getMemory(), bv);
+ StateValue cmp;
+
+ switch (cond) {
+ case EQ: cmp = { lhs == rhs, true }; break;
+ case NE: cmp = { lhs != rhs, true }; break;
+ case SLE: cmp = lhs.sle(rhs); break;
+ case SLT: cmp = lhs.slt(rhs); break;
+ case SGE: cmp = lhs.sge(rhs); break;
+ case SGT: cmp = lhs.sgt(rhs); break;
+ case ULE: cmp = lhs.ule(rhs); break;
+ case ULT: cmp = lhs.ult(rhs); break;
+ case UGE: cmp = lhs.uge(rhs); break;
+ case UGT: cmp = lhs.ugt(rhs); break;
+ case Any:
+ UNREACHABLE();
+ }
+ val = move(cmp.value);
+ non_poison &= move(cmp.non_poison);
+
+ } else { // integer comparison
switch (cond) {
case EQ: val = av == bv; break;
case NE: val = av != bv; break;
@@ -800,7 +819,8 @@ StateValue ICmp::toSMT(State &s) const {
case Any:
UNREACHABLE();
}
- return { expr::mkIf(val, expr::mkUInt(1,1), expr::mkUInt(0,1)), ap && bp };
+ }
+ return { val.toBVBool(), move(non_poison) };
}
expr ICmp::getTypeConstraints(const Function &f) const {
@@ -810,7 +830,7 @@ expr ICmp::getTypeConstraints(const Function &f) const {
a.getType().enforceIntOrPtrOrVectorType() &&
a.getType() == b.getType();
if (!defined)
- e &= cond_var().ule(expr::mkUInt(9, 4));
+ e &= cond_var().ule(9);
return e;
}
@@ -1126,7 +1146,12 @@ StateValue GEP::toSMT(State &s) const {
for (auto &[sz, idx] : idxs) {
auto &[v, np] = s[idx];
- ptr += expr::mkUInt(sz, bits_offset) * v.sextOrTrunc(bits_offset);
+ auto inc = expr::mkUInt(sz, bits_offset) * v.sextOrTrunc(bits_offset);
+
+ if (inbounds)
+ non_poison &= ptr.add_no_overflow(inc);
+
+ ptr += inc;
non_poison &= np;
if (inbounds)

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -60,12 +60,16 @@ expr Pointer::get_address() const {
}
expr Pointer::block_size() const {
- expr range = expr::mkUInt(0, m.bits_size_t);
+ // ASSUMPTION: programs can only allocate up to half of address space
+ // so the first bit of size is always zero.
+ // We need this assumption to support negative offsets.
+ expr range = expr::mkUInt(0, m.bits_size_t - 1);
auto local_name = m.mkName("blks_size");
return
+ expr::mkUInt(0, 1).concat(
expr::mkIf(is_local(),
expr::mkUF(local_name.c_str(), { get_local_bid() }, range),
- expr::mkUF("blks_size", { get_nonlocal_bid() }, range));
+ expr::mkUF("blks_size", { get_nonlocal_bid() }, range)));
}
Pointer Pointer::operator+(const expr &bytes) const {
@@ -80,16 +84,36 @@ void Pointer::operator+=(const expr &bytes) {
p = (get_offset() + bytes).concat(get_bid());
}
-expr Pointer::ult(const Pointer &rhs) const {
- return get_bid() == rhs.get_bid() && get_offset().ult(rhs.get_offset());
+expr Pointer::add_no_overflow(const expr &offset) const {
+ return get_offset().add_no_soverflow(offset);
+}
+
+expr Pointer::operator==(const Pointer &rhs) const {
+ return get_bid() == rhs.get_bid() && get_offset() == rhs.get_offset();
+}
+
+expr Pointer::operator!=(const Pointer &rhs) const {
+ return !operator==(rhs);
}
-expr Pointer::uge(const Pointer &rhs) const {
- return get_bid() == rhs.get_bid() && get_offset().uge(rhs.get_offset());
+#define DEFINE_CMP(op) \
+StateValue Pointer::op(const Pointer &rhs) const { \
+ return { get_offset().op(rhs.get_offset()), get_bid() == rhs.get_bid() }; \
}
+DEFINE_CMP(sle)
+DEFINE_CMP(slt)
+DEFINE_CMP(sge)
+DEFINE_CMP(sgt)
+DEFINE_CMP(ule)
+DEFINE_CMP(ult)
+DEFINE_CMP(uge)
+DEFINE_CMP(ugt)
+
expr Pointer::inbounds() const {
- return get_offset().zextOrTrunc(m.bits_size_t).ule(block_size());
+ // equivalent to offset >= 0 && offset <= block_size
+ // because block_size u<= 0x7FFF..
+ return get_offset().sextOrTrunc(m.bits_size_t).ule(block_size());
}
expr Pointer::is_aligned(unsigned align) const {
@@ -117,6 +141,11 @@ void Pointer::is_dereferenceable(unsigned bytes, unsigned align) {
is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset), align);
}
+ostream& operator<<(ostream &os, const Pointer &p) {
+ // TODO
+ return os << p;
+}
+
string Memory::mkName(const char *str, bool src) const {
return string(str) + (src ? "_src" : "_tgt");
@@ -235,7 +264,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,
string name = "#idx_" + to_string(last_idx_ptr++);
Pointer idx(*this, expr::mkVar(name.c_str(), ptr.bits()));
- expr cond = idx.uge(ptr) && idx.ult(ptr + bytes);
+ expr cond = idx.uge(ptr).both() && idx.ult(ptr + bytes).both();
expr val = expr::mkIf(cond, blocks_val.store(idx(), store_val), blocks_val);
blocks_val = expr::mkLambda({ idx() }, move(val));
}

MODIFY
ir/memory.h
ir/memory.h
#include "ir/state_value.h"
#include "smt/expr.h"
+#include <ostream>
#include <string>
#include <utility>
#include <vector>
@@ -17,6 +18,7 @@ class State;
class Pointer {
Memory &m;
// [offset, local_bid, nonlocal_bid]
+ // TODO: missing support for address space
smt::expr p;
unsigned bits_for_bids() const;
@@ -45,13 +47,26 @@ public:
Pointer operator+(const smt::expr &bytes) const;
void operator+=(const smt::expr &bytes);
- smt::expr ult(const Pointer &rhs) const;
- smt::expr uge(const Pointer &rhs) const;
+ smt::expr add_no_overflow(const smt::expr &offset) const;
+
+ smt::expr operator==(const Pointer &rhs) const;
+ smt::expr operator!=(const Pointer &rhs) const;
+
+ StateValue sle(const Pointer &rhs) const;
+ StateValue slt(const Pointer &rhs) const;
+ StateValue sge(const Pointer &rhs) const;
+ StateValue sgt(const Pointer &rhs) const;
+ StateValue ule(const Pointer &rhs) const;
+ StateValue ult(const Pointer &rhs) const;
+ StateValue uge(const Pointer &rhs) const;
+ StateValue ugt(const Pointer &rhs) const;
smt::expr inbounds() const;
smt::expr is_aligned(unsigned align) const;
void is_dereferenceable(unsigned bytes, unsigned align);
void is_dereferenceable(const smt::expr &bytes, unsigned align);
+
+ friend std::ostream& operator<<(std::ostream &os, const Pointer &p);
};

MODIFY
ir/state_value.h
ir/state_value.h
@@ -19,6 +19,8 @@ struct StateValue {
static StateValue mkIf(const smt::expr &cond, const StateValue &then,
const StateValue &els);
+ smt::expr both() const { return value && non_poison; }
+
bool eq(const StateValue &other) const;
StateValue

MODIFY
ir/type.cpp
ir/type.cpp
@@ -105,6 +105,10 @@ bool Type::isFloatType() const {
return false;
}
+bool Type::isPtrType() const {
+ return false;
+}
+
expr Type::enforceIntType(unsigned bits) const {
return false;
}
@@ -391,6 +395,10 @@ void PtrType::fixup(const Model &m) {
addr_space = m.getUInt(ASVar());
}
+bool PtrType::isPtrType() const {
+ return true;
+}
+
expr PtrType::enforceIntOrVectorType() const {
return false;
}
@@ -409,6 +417,7 @@ pair<expr, vector<expr>> PtrType::mkInput(State &s, const char *name) const {
void PtrType::printVal(ostream &os, const expr &e) const {
// TODO
+ os << e;
}
void PtrType::print(ostream &os) const {
@@ -784,6 +793,10 @@ bool SymbolicType::isFloatType() const {
return typ == Float;
}
+bool SymbolicType::isPtrType() const {
+ return typ == Ptr;
+}
+
expr SymbolicType::enforceIntType(unsigned bits) const {
return isInt() && i.enforceIntType(bits);
}

MODIFY
ir/type.h
ir/type.h
@@ -47,6 +47,7 @@ public:
virtual bool isIntType() const;
virtual bool isFloatType() const;
+ virtual bool isPtrType() const;
virtual smt::expr enforceIntType(unsigned bits = 0) const;
virtual smt::expr enforceIntOrVectorType() const;
@@ -161,6 +162,7 @@ public:
smt::expr operator==(const PtrType &rhs) const;
smt::expr sameType(const PtrType &rhs) const;
void fixup(const smt::Model &m) override;
+ bool isPtrType() const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
smt::expr enforcePtrType() const override;
@@ -259,6 +261,7 @@ public:
void fixup(const smt::Model &m) override;
bool isIntType() const override;
bool isFloatType() const override;
+ bool isPtrType() const override;
smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;

implement pointer comparison