llvm2alive: enable parsing of vector types
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -43,17 +43,25 @@ expr IntConst::getTypeConstraints() const {
FloatConst::FloatConst(Type &type, double val)
: Constant(type, to_string(val)), val(val) {}
+FloatConst::FloatConst(Type &type, std::string &&val)
+ : Constant(type, string(val)), val(move(val)) {}
+
expr FloatConst::getTypeConstraints() const {
return Value::getTypeConstraints() &&
getType().enforceFloatType();
}
StateValue FloatConst::toSMT(State &s) const {
+ if (auto str = get_if<string>(&val))
+ return { expr::mkNumber(str->c_str(), getType().getDummyValue(true).value),
+ true };
+
expr e;
+ double v = get<double>(val);
switch (getType().getAsFloatType()->getFpType()) {
- case FloatType::Half: e = expr::mkHalf((float)val); break;
- case FloatType::Float: e = expr::mkFloat((float)val); break;
- case FloatType::Double: e = expr::mkDouble(val); break;
+ case FloatType::Half: e = expr::mkHalf((float)v); break;
+ case FloatType::Float: e = expr::mkFloat((float)v); break;
+ case FloatType::Double: e = expr::mkDouble(v); break;
case FloatType::Unknown: UNREACHABLE();
}
return { move(e), true };

MODIFY
ir/constant.h
ir/constant.h
@@ -32,9 +32,10 @@ public:
class FloatConst final : public Constant {
- double val;
+ std::variant<double, std::string> val;
public:
FloatConst(Type &type, double val);
+ FloatConst(Type &type, std::string &&val);
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints() const override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -61,13 +61,13 @@ public:
expr is_ptr() const {
auto bit = p.bits() - 1;
- return p.extract(bit, bit);
+ return p.extract(bit, bit) == 1;
}
// Assuming that this is a pointer byte
expr ptr_nonpoison() const {
auto bit = p.bits() - 2;
- return p.extract(bit, bit);
+ return p.extract(bit, bit) == 1;
}
expr ptr_value() const { return p.extract(p.bits() - 3, 3); }
@@ -128,8 +128,8 @@ StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
} else {
non_poison &= ptr_value == loaded_ptr;
}
- non_poison &= b.is_ptr() == 1;
- non_poison &= b.ptr_nonpoison() == 1;
+ non_poison &= b.is_ptr();
+ non_poison &= b.ptr_nonpoison();
non_poison &= b.ptr_byteoffset() == i;
first = false;
}
@@ -141,20 +141,15 @@ StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
StateValue val;
bool first = true;
- // The result is poison if any byte is a pointer byte.
- expr non_poison = true;
+ IntType i8Ty("", 8);
for (auto &b: bytes) {
- StateValue v(b.nonptr_value(), b.nonptr_nonpoison());
-
+ expr ptr_np = i8Ty.toBV({ b.nonptr_nonpoison(), !b.is_ptr() }).non_poison;
+ StateValue v(b.nonptr_value(), ptr_np | b.nonptr_nonpoison());
val = first ? move(v) : v.concat(val);
first = false;
- non_poison &= b.is_ptr() == 0;
}
-
- val = toType.fromBV(val.trunc(bitsize));
- val.non_poison &= non_poison;
- return val;
+ return toType.fromBV(val.trunc(bitsize));
}
}
}
@@ -391,7 +386,7 @@ Memory::Memory(State &state) : state(&state) {
// All non-local blocks cannot initially contain pointers to local blocks.
auto byte = Byte(*this, blocks_val.load(idx()));
Pointer loadedptr(*this, byte.ptr_value());
- expr cond = byte.is_ptr() == 0 || byte.ptr_nonpoison() == 0 ||
+ expr cond = !byte.is_ptr() || !byte.ptr_nonpoison() ||
!loadedptr.is_local();
state.addPre(expr::mkForAll({ idx() }, move(cond)));

MODIFY
ir/type.cpp
ir/type.cpp
@@ -728,10 +728,7 @@ VectorType::VectorType(string &&name, unsigned elements, Type &elementTy)
assert(elements != 0);
this->elements = elements;
defined = true;
-
- for (unsigned i = 0; i < elements; ++i) {
- children.emplace_back(&elementTy);
- }
+ children.resize(elements, &elementTy);
}
expr VectorType::getTypeConstraints() const {

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -104,7 +104,25 @@ Type* llvm_type2alive(const llvm::Type *ty) {
}
return cache.get();
}
+ case llvm::Type::VectorTyID: {
+ auto &cache = type_cache[ty];
+ if (!cache) {
+ auto vty = cast<llvm::VectorType>(ty);
+ // TODO: non-fixed sized vectors
+ if (vty->isScalable())
+ goto err;
+
+ auto elems = vty->getElementCount().Min;
+ auto ety = llvm_type2alive(vty->getElementType());
+ if (!ety || elems > 128)
+ return nullptr;
+ cache = make_unique<VectorType>("ty_" + to_string(type_id_counter++),
+ elems, *ety);
+ }
+ return cache.get();
+ }
default:
+err:
*out << "Unsupported type: " << *ty << '\n';
return nullptr;
}
@@ -141,16 +159,23 @@ Value* get_operand(llvm::Value *v) {
if (auto cnst = dyn_cast<llvm::ConstantFP>(v)) {
auto &apfloat = cnst->getValueAPF();
- auto apint = apfloat.bitcastToAPInt();
- double val;
- if (apint.getBitWidth() == 32) {
- val = apfloat.convertToFloat();
- } else if (apint.getBitWidth() == 64) {
- val = apfloat.convertToDouble();
- } else // TODO
- return nullptr;
-
- auto c = make_unique<FloatConst>(*ty, val);
+ unique_ptr<FloatConst> c;
+ switch (ty->getAsFloatType()->getFpType()) {
+ case FloatType::Half: {
+ llvm::SmallString<32> str;
+ apfloat.toString(str);
+ c = make_unique<FloatConst>(*ty, str.str());
+ break;
+ }
+ case FloatType::Float:
+ c = make_unique<FloatConst>(*ty, apfloat.convertToFloat());
+ break;
+ case FloatType::Double:
+ c = make_unique<FloatConst>(*ty, apfloat.convertToDouble());
+ break;
+ case FloatType::Unknown:
+ UNREACHABLE();
+ }
auto ret = c.get();
current_fn->addConstant(move(c));
return ret;
@@ -209,6 +234,17 @@ Value* get_operand(llvm::Value *v) {
return ret;
}
+ if (auto cnst = dyn_cast<llvm::ConstantAggregateZero>(v)) {
+ vector<Value*> vals;
+ for (auto I = cnst->op_begin(), E = cnst->op_end(); I != E; ++I) {
+ vals.emplace_back(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
smt/expr.cpp
smt/expr.cpp
@@ -192,6 +192,11 @@ expr expr::mkDouble(double n) {
return Z3_mk_fpa_numeral_double(ctx(), n, Z3_mk_fpa_sort_double(ctx()));
}
+expr expr::mkNumber(const char *n, const expr &type) {
+ C2(type);
+ return Z3_mk_numeral(ctx(), n, type.sort());
+}
+
expr expr::mkConst(Z3_func_decl decl) {
return Z3_mk_app(ctx(), decl, 0, {});
}
@@ -1170,6 +1175,16 @@ expr expr::store(const expr &idx, const expr &val) const {
expr expr::load(const expr &idx) const {
C(idx);
+
+ // TODO: add support for alias analysis plugin
+ if (auto app = isAppOf(Z3_OP_STORE)) { // store(array, idx, val)
+ expr cmp = idx == Z3_get_app_arg(ctx(), app, 1);
+
+ if (cmp.isTrue())
+ return Z3_get_app_arg(ctx(), app, 2);
+ if (cmp.isFalse())
+ return expr(Z3_get_app_arg(ctx(), app, 0)).load(idx);
+ }
return Z3_mk_select(ctx(), ast(), idx());
}

MODIFY
smt/expr.h
smt/expr.h
@@ -83,6 +83,7 @@ public:
static expr mkHalf(float n);
static expr mkFloat(float n);
static expr mkDouble(double n);
+ static expr mkNumber(const char *n, const expr &type);
static expr mkVar(const char *name, const expr &type);
static expr mkVar(const char *name, unsigned bits);
static expr mkBoolVar(const char *name);

llvm2alive: enable parsing of vector types