add a GEP instruction
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -935,6 +935,58 @@ unique_ptr<Instr> Free::dup(const string &suffix) const {
}
+void GEP::addIdx(unsigned obj_size, Value &idx) {
+ idxs.emplace_back(obj_size, idx);
+}
+
+void GEP::print(std::ostream &os) const {
+ os << getName() << " = gep ";
+ if (inbounds)
+ os << "inbounds ";
+ os << ptr;
+
+ for (auto &[sz, idx] : idxs) {
+ os << ", " << sz << " x " << idx;
+ }
+}
+
+StateValue GEP::toSMT(State &s) const {
+ auto [val, non_poison] = s[ptr];
+ unsigned bits_offset = s.getMemory().bitsOffset();
+
+ if (inbounds)
+ non_poison &= Pointer(s.getMemory(), val).inbounds();
+
+ for (auto &[sz, idx] : idxs) {
+ auto &[v, np] = s[idx];
+ val = val + expr::mkUInt(sz, bits_offset) * v.sextOrTrunc(bits_offset);
+ non_poison &= np;
+
+ if (inbounds)
+ non_poison &= Pointer(s.getMemory(), val).inbounds();
+ }
+ return { move(val), move(non_poison) };
+}
+
+expr GEP::getTypeConstraints(const Function &f) const {
+ auto c = getType() == ptr.getType() &&
+ ptr.getType().enforcePtrType();
+ for (auto &[sz, idx] : idxs) {
+ (void)sz;
+ c &= idx.getType().enforceIntType();
+ }
+ return c;
+}
+
+unique_ptr<Instr> GEP::dup(const string &suffix) const {
+ auto dup = make_unique<GEP>(getType(), getName() + suffix, ptr, inbounds);
+ for (auto &[sz, idx] : idxs) {
+ dup->addIdx(sz, idx);
+ }
+ return dup;
+}
+
+
void Load::print(std::ostream &os) const {
os << getName() << " = load " << getType() << ", " << ptr
<< ", align " << align;

MODIFY
ir/instr.h
ir/instr.h
@@ -301,6 +301,23 @@ public:
};
+class GEP final : public Instr {
+ Value &ptr;
+ std::vector<std::pair<unsigned, Value&>> idxs;
+ bool inbounds;
+public:
+ GEP(Type &type, std::string &&name, Value &ptr, bool inbounds)
+ : Instr(type, std::move(name)), ptr(ptr), inbounds(inbounds) {}
+
+ void addIdx(unsigned obj_size, Value &idx);
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+ std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+};
+
+
class Load final : public Instr {
Value &ptr;
unsigned align;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -49,12 +49,18 @@ expr Pointer::uge(const Pointer &rhs) const {
return get_bid() == rhs.get_bid() && get_offset().uge(rhs.get_offset());
}
+expr Pointer::inbounds() const {
+ expr block_sz = m.blocks_size.load(get_bid());
+ expr offset = get_offset();
+ return offset.zextOrTrunc(m.bits_size_t).ule(block_sz);
+}
+
void Pointer::is_dereferenceable(const expr &bytes) {
expr block_sz = m.blocks_size.load(get_bid());
expr offset = get_offset();
// 1) check that offset is within bounds and that arith doesn't overflow
- m.state->addUB((offset + bytes).zextOrTrunc(m.bits_size_t).ult(block_sz));
+ m.state->addUB((offset + bytes).zextOrTrunc(m.bits_size_t).ule(block_sz));
m.state->addUB(offset.add_no_uoverflow(bytes));
// 2) check block is alive

MODIFY
ir/memory.h
ir/memory.h
@@ -34,6 +34,7 @@ public:
smt::expr ult(const Pointer &rhs) const;
smt::expr uge(const Pointer &rhs) const;
+ smt::expr inbounds() const;
void is_dereferenceable(unsigned bytes);
void is_dereferenceable(const smt::expr &bytes);
};
@@ -70,6 +71,8 @@ public:
static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);
+ unsigned bitsOffset() const { return bits_for_offset; }
+
friend class Pointer;
};

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -942,6 +942,11 @@ expr expr::trunc(unsigned tobw) const {
return extract(tobw-1, 0);
}
+expr expr::sextOrTrunc(unsigned tobw) const {
+ auto bw = bits();
+ return bw < tobw ? sext(tobw - bw) : trunc(tobw);
+}
+
expr expr::zextOrTrunc(unsigned tobw) const {
auto bw = bits();
return bw < tobw ? zext(tobw - bw) : trunc(tobw);

MODIFY
smt/expr.h
smt/expr.h
@@ -185,6 +185,7 @@ public:
expr sext(unsigned amount) const;
expr zext(unsigned amount) const;
expr trunc(unsigned tobw) const;
+ expr sextOrTrunc(unsigned tobw) const;
expr zextOrTrunc(unsigned tobw) const;
expr concat(const expr &rhs) const;

add a GEP instruction