type system fixes for integer ops
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -321,13 +321,13 @@ expr BinOp::getTypeConstraints(const Function &f) const {
break;
case Cttz:
case Ctlz:
- instrconstr = getType().enforceIntOrPtrOrVectorType() &&
+ instrconstr = getType().enforceIntOrVectorType() &&
getType() == lhs.getType() &&
rhs.getType().enforceIntType() &&
rhs.getType().sizeVar() == 1u;
break;
default:
- instrconstr = getType().enforceIntOrPtrOrVectorType() &&
+ instrconstr = getType().enforceIntOrVectorType() &&
getType() == lhs.getType() &&
getType() == rhs.getType();
break;
@@ -381,7 +381,7 @@ expr UnaryOp::getTypeConstraints(const Function &f) const {
[[fallthrough]];
case BitReverse:
case Ctpop:
- instrconstr &= getType().enforceIntOrPtrOrVectorType();
+ instrconstr &= getType().enforceIntOrVectorType();
case Copy:
break;
}
@@ -489,10 +489,9 @@ expr ConversionOp::getTypeConstraints(const Function &f) const {
sizeconstr = getType().sizeVar().ult(val.getType().sizeVar());
break;
}
- // TODO: missing constraint comparing ty and to_ty (e.g. both ints)
return Value::getTypeConstraints() &&
- getType().enforceIntOrPtrOrVectorType() &&
- val.getType().enforceIntOrPtrOrVectorType() && // FIXME: remove
+ getType().enforceIntOrVectorType() &&
+ getType().sameType(val.getType()) &&
move(sizeconstr);
}

MODIFY
ir/type.cpp
ir/type.cpp
@@ -50,9 +50,6 @@ expr Type::operator==(const Type &b) const {
if (auto lhs = dynamic_cast<const Ty*>(this)) { \
if (auto rhs = dynamic_cast<const Ty*>(&b)) \
return *lhs == *rhs; \
- if (auto rhs = dynamic_cast<const SymbolicType*>(&b)) \
- return *rhs == *lhs; \
- return false; \
}
CMP(IntType)
@@ -61,13 +58,41 @@ expr Type::operator==(const Type &b) const {
CMP(ArrayType)
CMP(VectorType)
CMP(StructType)
-
#undef CMP
- if (auto lhs = dynamic_cast<const SymbolicType*>(this)) {
+ if (auto lhs = dynamic_cast<const SymbolicType*>(this))
return *lhs == b;
+
+ if (auto rhs = dynamic_cast<const SymbolicType*>(&b))
+ return *rhs == *this;
+
+ return false;
}
+expr Type::sameType(const Type &b) const {
+ if (this == &b)
+ return true;
+
+#define CMP(Ty) \
+ if (auto lhs = dynamic_cast<const Ty*>(this)) { \
+ if (auto rhs = dynamic_cast<const Ty*>(&b)) \
+ return lhs->sameType(*rhs); \
+ }
+
+ CMP(IntType)
+ CMP(FloatType)
+ CMP(PtrType)
+ CMP(ArrayType)
+ CMP(VectorType)
+ CMP(StructType)
+#undef CMP
+
+ if (auto lhs = dynamic_cast<const SymbolicType*>(this))
+ return lhs->sameType(b);
+
+ if (auto rhs = dynamic_cast<const SymbolicType*>(&b))
+ return rhs->sameType(*this);
+
return false;
}
@@ -159,6 +184,10 @@ expr IntType::operator==(const IntType &rhs) const {
return sizeVar() == rhs.sizeVar();
}
+expr IntType::sameType(const IntType &rhs) const {
+ return true;
+}
+
void IntType::fixup(const Model &m) {
if (!defined)
bitwidth = m.getUInt(sizeVar());
@@ -202,6 +231,10 @@ expr FloatType::operator==(const FloatType &rhs) const {
return false;
}
+expr FloatType::sameType(const FloatType &rhs) const {
+ return true;
+}
+
void FloatType::fixup(const Model &m) {
// TODO
}
@@ -237,6 +270,10 @@ expr PtrType::operator==(const PtrType &rhs) const {
ASVar() == rhs.ASVar();
}
+expr PtrType::sameType(const PtrType &rhs) const {
+ return *this == rhs;
+}
+
void PtrType::fixup(const Model &m) {
if (!defined)
addr_space = m.getUInt(ASVar());
@@ -282,6 +319,11 @@ expr ArrayType::operator==(const ArrayType &rhs) const {
return false;
}
+expr ArrayType::sameType(const ArrayType &rhs) const {
+ // TODO
+ return false;
+}
+
void ArrayType::fixup(const Model &m) {
// TODO
}
@@ -315,16 +357,23 @@ expr VectorType::operator==(const VectorType &rhs) const {
return false;
}
+expr VectorType::sameType(const VectorType &rhs) const {
+ // TODO
+ return false;
+}
+
void VectorType::fixup(const Model &m) {
// TODO
}
expr VectorType::enforceIntOrVectorType() const {
- return true;
+ // TODO: check if elements are int
+ return false;
}
expr VectorType::enforceIntOrPtrOrVectorType() const {
- return true;
+ // TODO: check if elements are int/ptr
+ return false;
}
void VectorType::print(ostream &os) const {
@@ -377,6 +426,17 @@ expr StructType::operator==(const StructType &rhs) const {
return res;
}
+expr StructType::sameType(const StructType &rhs) const {
+ if (children.size() != rhs.children.size())
+ return false;
+
+ expr res(true);
+ for (unsigned i = 0, e = children.size(); i != e; ++i) {
+ res &= children[i]->sameType(*rhs.children[i]);
+ }
+ return res;
+}
+
void StructType::fixup(const Model &m) {
for (auto c : children) {
c->fixup(m);
@@ -502,6 +562,37 @@ expr SymbolicType::operator==(const Type &b) const {
UNREACHABLE();
}
+expr SymbolicType::sameType(const Type &b) const {
+ if (this == &b)
+ return true;
+
+ if (auto rhs = dynamic_cast<const IntType*>(&b))
+ return isInt() && i.sameType(*rhs);
+ if (auto rhs = dynamic_cast<const FloatType*>(&b))
+ return isFloat() && f.sameType(*rhs);
+ if (auto rhs = dynamic_cast<const PtrType*>(&b))
+ return isPtr() && p.sameType(*rhs);
+ if (auto rhs = dynamic_cast<const ArrayType*>(&b))
+ return isArray() && a.sameType(*rhs);
+ if (auto rhs = dynamic_cast<const VectorType*>(&b))
+ return isVector() && v.sameType(*rhs);
+ if (auto rhs = dynamic_cast<const StructType*>(&b))
+ return isStruct() && s.sameType(*rhs);
+
+ if (auto rhs = dynamic_cast<const SymbolicType*>(&b)) {
+ expr c(false);
+ c |= isInt() && i.sameType(rhs->i);
+ c |= isFloat() && f.sameType(rhs->f);
+ c |= isPtr() && p.sameType(rhs->p);
+ c |= isArray() && a.sameType(rhs->a);
+ c |= isVector() && v.sameType(rhs->v);
+ // FIXME: add support for this: c |= isStruct() && s.sameType(rhs->s);
+ return move(c) && typeVar() == rhs->typeVar();
+ }
+ assert(0 && "unhandled case in SymbolicType::sameType");
+ UNREACHABLE();
+}
+
void SymbolicType::fixup(const Model &m) {
unsigned smt_typ = m.getUInt(typeVar());
assert(smt_typ >= Int && smt_typ <= Struct);

MODIFY
ir/type.h
ir/type.h
@@ -39,6 +39,7 @@ public:
virtual smt::expr getTypeConstraints() const = 0;
virtual smt::expr sizeVar() const;
smt::expr operator==(const Type &rhs) const;
+ smt::expr sameType(const Type &rhs) const;
virtual void fixup(const smt::Model &m) = 0;
virtual smt::expr enforceIntType(unsigned bits = 0) const;
@@ -85,6 +86,7 @@ public:
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
smt::expr operator==(const IntType &rhs) const;
+ smt::expr sameType(const IntType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;
@@ -100,6 +102,7 @@ public:
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const FloatType &rhs) const;
+ smt::expr sameType(const FloatType &rhs) const;
void fixup(const smt::Model &m) override;
void print(std::ostream &os) const override;
};
@@ -118,6 +121,7 @@ public:
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const PtrType &rhs) const;
+ smt::expr sameType(const PtrType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
@@ -133,6 +137,7 @@ public:
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const ArrayType &rhs) const;
+ smt::expr sameType(const ArrayType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceAggregateType() const override;
void print(std::ostream &os) const override;
@@ -146,6 +151,7 @@ public:
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const VectorType &rhs) const;
+ smt::expr sameType(const VectorType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
@@ -165,6 +171,7 @@ public:
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const StructType &rhs) const;
+ smt::expr sameType(const StructType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceStructType() const override;
smt::expr enforceAggregateType() const override;
@@ -198,6 +205,7 @@ public:
smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const Type &rhs) const;
+ smt::expr sameType(const Type &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;

type system fixes for integer ops