stub out pointers & load/store instructions
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -894,4 +894,44 @@ unique_ptr<Instr> Assume::dup(const string &suffix) const {
return make_unique<Assume>(cond, if_non_poison);
}
+
+void Load::print(std::ostream &os) const {
+ os << getName() << " = load " << getType() << ", " << ptr;
+}
+
+StateValue Load::toSMT(State &s) const {
+ // TODO
+ s.addUB({});
+ return {};
+}
+
+expr Load::getTypeConstraints(const Function &f) const {
+ return Value::getTypeConstraints() &&
+ ptr.getType().enforcePtrType();
+}
+
+unique_ptr<Instr> Load::dup(const string &suffix) const {
+ return make_unique<Load>(getType(), getName() + suffix, ptr);
+}
+
+
+void Store::print(std::ostream &os) const {
+ os << "store " << getType() << ", " << ptr << ", " << val;
+}
+
+StateValue Store::toSMT(State &s) const {
+ // TODO
+ s.addUB({});
+ return {};
+}
+
+expr Store::getTypeConstraints(const Function &f) const {
+ return Value::getTypeConstraints() &&
+ ptr.getType().enforcePtrType();
+}
+
+unique_ptr<Instr> Store::dup(const string &suffix) const {
+ return make_unique<Store>(getType(), getName() + suffix, ptr, val);
+}
+
}

MODIFY
ir/instr.h
ir/instr.h
@@ -273,4 +273,30 @@ public:
std::unique_ptr<Instr> dup(const std::string &suffix) const override;
};
+
+class Load final : public Instr {
+ Value &ptr;
+public:
+ Load(Type &type, std::string &&name, Value &ptr)
+ : Instr(type, std::move(name)), ptr(ptr) {}
+
+ 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 Store final : public Instr {
+ Value &ptr, &val;
+public:
+ Store(Type &type, std::string &&name, Value &ptr, Value &val)
+ : Instr(type, std::move(name)), ptr(ptr), val(val) {}
+
+ 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;
+};
+
}

MODIFY
ir/type.cpp
ir/type.cpp
@@ -12,6 +12,7 @@ using namespace std;
static constexpr unsigned var_type_bits = 3;
static constexpr unsigned var_bw_bits = 8;
+static constexpr unsigned sizeof_ptr = 64; // TODO: make this configurable
namespace IR {
@@ -87,6 +88,10 @@ expr Type::enforceIntOrPtrOrVectorType() const {
return false;
}
+expr Type::enforcePtrType() const {
+ return false;
+}
+
expr Type::enforceStructType() const {
return false;
}
@@ -202,23 +207,30 @@ void FloatType::print(ostream &os) const {
}
+PtrType::PtrType(unsigned addr_space)
+ : Type(addr_space == 0 ? "*" : "as(" + to_string(addr_space) + ")*"),
+ addr_space(addr_space), defined(true) {}
+
+expr PtrType::ASVar() const {
+ return defined ? expr::mkUInt(addr_space, 8) : var("as", 8);
+}
+
expr PtrType::getDummyValue() const {
- // TODO
- return {};
+ return expr::mkUInt(0, sizeof_ptr);
}
expr PtrType::getTypeConstraints() const {
- // TODO
- return false;
+ return sizeVar() == sizeof_ptr;
}
expr PtrType::operator==(const PtrType &rhs) const {
- // TODO
- return sizeVar() == rhs.sizeVar();
+ return sizeVar() == rhs.sizeVar() &&
+ ASVar() == rhs.ASVar();
}
void PtrType::fixup(const Model &m) {
- // TODO
+ if (!defined)
+ addr_space = m.getUInt(ASVar());
}
expr PtrType::enforceIntOrVectorType() const {
@@ -229,8 +241,15 @@ expr PtrType::enforceIntOrPtrOrVectorType() const {
return true;
}
+expr PtrType::enforcePtrType() const {
+ return true;
+}
+
void PtrType::print(ostream &os) const {
- os << "TODO";
+ if (addr_space != 0)
+ os << "as(" << addr_space << ")*";
+ else
+ os << '*';
}
@@ -391,8 +410,9 @@ expr StructType::extract(const expr &struct_val, unsigned index) const {
SymbolicType::SymbolicType(string &&name, bool named)
- : Type(string(name)), i(string(name)), f(string(name)), p(string(name)),
- a(string(name)), v(string(name)), s(string(name)), named(named) {}
+ : Type(string(name)), i(name + "_int"), f(name + "_fp"), p(name + "_ptr"),
+ a(name + "_array"), v(name + "_vector"), s(name + "_struct"),
+ named(named) {}
unsigned SymbolicType::bits() const {
switch (typ) {
@@ -493,6 +513,10 @@ expr SymbolicType::enforceIntOrPtrOrVectorType() const {
return isInt() || isPtr() || isVector();
}
+expr SymbolicType::enforcePtrType() const {
+ return isPtr();
+}
+
expr SymbolicType::enforceStructType() const {
return isStruct();
}

MODIFY
ir/type.h
ir/type.h
@@ -44,6 +44,7 @@ public:
virtual smt::expr enforceIntType(unsigned bits = 0) const;
virtual smt::expr enforceIntOrVectorType() const;
virtual smt::expr enforceIntOrPtrOrVectorType() const;
+ virtual smt::expr enforcePtrType() const;
virtual smt::expr enforceStructType() const;
virtual smt::expr enforceAggregateType() const;
@@ -103,14 +104,21 @@ public:
class PtrType final : public Type {
+ unsigned addr_space = 0;
+ bool defined = false;
+ smt::expr ASVar() const;
public:
+ // symbolic addr space ptr
PtrType(std::string &&name) : Type(std::move(name)) {}
+
+ PtrType(unsigned addr_space);
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const PtrType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
+ smt::expr enforcePtrType() const override;
void print(std::ostream &os) const override;
};
@@ -189,6 +197,7 @@ public:
smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
+ smt::expr enforcePtrType() const override;
smt::expr enforceStructType() const override;
smt::expr enforceAggregateType() const override;
const StructType* getAsStructType() const override;

stub out pointers & load/store instructions