add support for constant aggregates
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -66,6 +66,45 @@ pair<expr, expr> FloatConst::toSMT_cnst() const {
}
+static string agg_const_str(vector<Constant*> &vals) {
+ string r = "{ ";
+ bool first = true;
+ for (auto val : vals) {
+ if (!first)
+ r += ", ";
+ r += val->getName();
+ first = false;
+ }
+ return r + " }";
+}
+
+AggregateConst::AggregateConst(Type &type, vector<Constant*> &&vals)
+ : Constant(type, agg_const_str(vals)), vals(move(vals)) {}
+
+pair<expr, expr> AggregateConst::toSMT_cnst() const {
+ expr v;
+ bool first = true;
+ for (auto val : vals) {
+ auto [vv, vnp] = val->toSMT_cnst();
+ assert(vnp.isTrue());
+ vv = val->getType().toBV(vv);
+ v = first ? vv : v.concat(vv);
+ first = false;
+ }
+ return { move(v), true };
+}
+
+expr AggregateConst::getTypeConstraints() const {
+ expr r = Value::getTypeConstraints();
+ vector<Type*> types;
+ for (auto val : vals) {
+ types.emplace_back(&val->getType());
+ r &= val->getTypeConstraints();
+ }
+ return r && getType().enforceAggregateType(&types);
+}
+
+
pair<expr, expr> ConstantInput::toSMT_cnst() const {
return { expr::mkVar(getName().c_str(), bits()), true };
}

MODIFY
ir/constant.h
ir/constant.h
@@ -44,6 +44,16 @@ public:
};
+class AggregateConst final : public Constant {
+ std::vector<Constant*> vals;
+public:
+ AggregateConst(Type &type, std::vector<Constant*> &&vals);
+
+ virtual std::pair<smt::expr, smt::expr> toSMT_cnst() const override;
+ smt::expr getTypeConstraints() const override;
+};
+
+
class ConstantInput final : public Constant {
public:
ConstantInput(Type &type, std::string &&name)

MODIFY
ir/type.cpp
ir/type.cpp
@@ -134,7 +134,7 @@ expr Type::enforceStructType() const {
return false;
}
-expr Type::enforceAggregateType() const {
+expr Type::enforceAggregateType(vector<Type*> *element_types) const {
return false;
}
@@ -150,6 +150,10 @@ const FloatType* Type::getAsFloatType() const {
return nullptr;
}
+expr Type::toBV(expr e) const {
+ return e;
+}
+
ostream& operator<<(ostream &os, const Type &t) {
t.print(os);
return os;
@@ -283,6 +287,10 @@ const FloatType* FloatType::getAsFloatType() const {
return this;
}
+expr FloatType::toBV(expr e) const {
+ return e.float2BV();
+}
+
expr FloatType::sizeVar() const {
return defined ? expr::mkUInt(getFpType(), var_bw_bits) : Type::sizeVar();
}
@@ -470,7 +478,8 @@ void ArrayType::fixup(const Model &m) {
// TODO
}
-expr ArrayType::enforceAggregateType() const {
+expr ArrayType::enforceAggregateType(vector<Type*> *element_types) const {
+ // TODO
return true;
}
@@ -518,9 +527,7 @@ unsigned VectorType::bits() const {
}
expr VectorType::getDummyValue() const {
- expr element = elementTy.getDummyValue();
- if (elementTy.isFloatType())
- element = element.float2BV();
+ expr element = elementTy.toBV(elementTy.getDummyValue());
expr ret = element;
for (unsigned i = 1; i < elements; ++i) {
@@ -564,6 +571,17 @@ expr VectorType::enforceIntOrPtrOrVectorType() const {
return elementTy.enforceIntOrPtrType();
}
+expr VectorType::enforceAggregateType(vector<Type*> *element_types) const {
+ if (!element_types)
+ return true;
+
+ expr r = numElements() == element_types->size();
+ for (auto ty : *element_types) {
+ r &= *ty == elementTy;
+ }
+ return r;
+}
+
pair<expr, vector<expr>> VectorType::mkInput(State &s, const char *name) const {
expr val;
vector<expr> vect;
@@ -573,8 +591,7 @@ pair<expr, vector<expr>> VectorType::mkInput(State &s, const char *name) const {
auto [val_i, vect_i] = elementTy.mkInput(s, name_i.c_str());
vect.insert(vect.end(), vect_i.begin(), vect_i.end());
- if (elementTy.isFloatType())
- val_i = val_i.float2BV();
+ val_i = elementTy.toBV(val_i);
val = i == 0 ? move(val_i) : val.concat(val_i);
}
return { move(val), move(vect) };
@@ -610,7 +627,6 @@ expr StructType::getDummyValue() const {
expr res;
bool first = true;
- // TODO: what if a function returns a struct with no children?
for (auto c : children) {
if (first) {
res = c->getDummyValue();
@@ -662,8 +678,19 @@ expr StructType::enforceStructType() const {
return true;
}
-expr StructType::enforceAggregateType() const {
+expr StructType::enforceAggregateType(vector<Type*> *element_types) const {
+ if (!element_types)
return true;
+
+ // TODO: support symbolic structs
+ if (children.size() != element_types->size())
+ return false;
+
+ expr r(true);
+ for (unsigned i = 0, e = children.size(); i != e; ++i) {
+ r &= *children[i] == *(*element_types)[i];
+ }
+ return r;
}
const StructType* StructType::getAsStructType() const {
@@ -903,8 +930,10 @@ expr SymbolicType::enforceStructType() const {
return isStruct();
}
-expr SymbolicType::enforceAggregateType() const {
- return isArray() || isStruct();
+expr SymbolicType::enforceAggregateType(vector<Type*> *element_types) const {
+ return (isArray() && a->enforceAggregateType (element_types)) ||
+ (isVector() && v->enforceAggregateType(element_types)) ||
+ (isStruct() && s->enforceAggregateType(element_types));
}
expr SymbolicType::enforceFloatType() const {

MODIFY
ir/type.h
ir/type.h
@@ -56,12 +56,15 @@ public:
virtual smt::expr enforceIntOrPtrOrVectorType() const;
virtual smt::expr enforcePtrType() const;
virtual smt::expr enforceStructType() const;
- virtual smt::expr enforceAggregateType() const;
+ virtual smt::expr enforceAggregateType(
+ std::vector<Type*> *element_types = nullptr) const;
virtual smt::expr enforceFloatType() const;
virtual const StructType* getAsStructType() const;
virtual const FloatType* getAsFloatType() const;
+ virtual smt::expr toBV(smt::expr e) const;
+
virtual std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const = 0;
virtual void printVal(std::ostream &os, State &s,
@@ -143,6 +146,7 @@ public:
bool isFloatType() const override;
smt::expr enforceFloatType() const override;
const FloatType* getAsFloatType() const override;
+ smt::expr toBV(smt::expr e) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -185,7 +189,8 @@ public:
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;
+ smt::expr enforceAggregateType(
+ std::vector<Type*> *element_types) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -215,6 +220,8 @@ public:
void fixup(const smt::Model &m) override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
+ smt::expr enforceAggregateType(
+ std::vector<Type*> *element_types) const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
@@ -237,7 +244,8 @@ public:
smt::expr sameType(const StructType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceStructType() const override;
- smt::expr enforceAggregateType() const override;
+ smt::expr enforceAggregateType(
+ std::vector<Type*> *element_types) const override;
const StructType* getAsStructType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
@@ -283,7 +291,8 @@ public:
smt::expr enforceIntOrPtrOrVectorType() const override;
smt::expr enforcePtrType() const override;
smt::expr enforceStructType() const override;
- smt::expr enforceAggregateType() const override;
+ smt::expr enforceAggregateType(
+ std::vector<Type*> *element_types) const override;
smt::expr enforceFloatType() const override;
const StructType* getAsStructType() const override;
const FloatType* getAsFloatType() const override;

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -174,6 +174,17 @@ Value* get_operand(llvm::Value *v) {
return ret;
}
+ if (auto cnst = dyn_cast<llvm::ConstantAggregate>(v)) {
+ vector<Constant*> vals;
+ for (auto I = cnst->op_begin(), E = cnst->op_end(); I != E; ++I) {
+ vals.emplace_back(static_cast<Constant*>(get_operand(*I)));
+ }
+ auto val = make_unique<AggregateConst>(*ty, move(vals));
+ auto ret = val.get();
+ current_fn->addConstant(move(val));
+ return ret;
+ }
+
return nullptr;
}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -76,6 +76,7 @@ static Value& get_fp_constant(double n, Type &t) {
return *ret;
}
+namespace {
struct tokenizer_t {
token last;
// true if token last was 'unget' and should be returned next
@@ -139,6 +140,7 @@ private:
}
}
};
+}
static tokenizer_t tokenizer;

add support for constant aggregates