add support for 'return void'
fixes
MODIFY
ir/type.cpp
ir/type.cpp
@@ -16,7 +16,7 @@ static constexpr unsigned var_bw_bits = 8;
namespace IR {
-VoidType Type::voidTy("void");
+VoidType Type::voidTy;
expr Type::var(const char *var, unsigned bits) const {
auto str = name + '_' + var;

MODIFY
ir/type.h
ir/type.h
@@ -50,7 +50,7 @@ public:
class VoidType final : public Type {
public:
- VoidType(std::string &&name) : Type(std::move(name)) {}
+ VoidType() : Type("void") {}
smt::expr getTypeConstraints() const override;
void fixup(const smt::Model &m) override;
void print(std::ostream &os) const override;

MODIFY
ir/value.cpp
ir/value.cpp
@@ -12,6 +12,8 @@ static unsigned gbl_fresh_id = 0;
namespace IR {
+VoidValue Value::voidVal(Type::voidTy);
+
void Value::reset_gbl_id() {
gbl_fresh_id = 0;
}
@@ -61,6 +63,15 @@ StateValue PoisonValue::toSMT(State &s) const {
}
+void VoidValue::print(ostream &os) const {
+ UNREACHABLE();
+}
+
+StateValue VoidValue::toSMT(State &s) const {
+ return { false, false };
+}
+
+
void Input::print(std::ostream &os) const {
UNREACHABLE();
}

MODIFY
ir/value.h
ir/value.h
@@ -14,6 +14,9 @@ namespace smt { class Model; }
namespace IR {
+class VoidValue;
+
+
class Value {
Type &type;
std::string name;
@@ -35,6 +38,8 @@ public:
virtual smt::expr getTypeConstraints() const;
virtual void fixupTypes(const smt::Model &m);
+ static VoidValue voidVal;
+
static void reset_gbl_id();
friend std::ostream& operator<<(std::ostream &os, const Value &val);
@@ -61,6 +66,14 @@ public:
};
+class VoidValue final : public Value {
+public:
+ VoidValue(Type &type) : Value(type, "void") {}
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+};
+
+
class Input final : public Value {
public:
Input(Type &type, std::string &&name) :

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -95,6 +95,7 @@ Value* get_operand(llvm::Value *v) {
if (!ty)
return nullptr;
+ // TODO: cache these?
if (auto cnst = dyn_cast<llvm::ConstantInt>(v)) {
unique_ptr<IntConst> c;
if (cnst->getBitWidth() <= 64)
@@ -249,6 +250,10 @@ public:
}
RetTy visitReturnInst(llvm::ReturnInst &i) {
+ if (i.getNumOperands() == 0) {
+ assert(i.getType().isVoidTy());
+ return make_unique<Return>(Type::voidTy, Value::voidVal);
+ }
PARSE_UNOP();
return make_unique<Return>(*ty, *val);
}

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -23,6 +23,8 @@ void sym_exec(State &s) {
}
}
+ s.exec(Value::voidVal);
+
for (auto &bb : f.getBBs()) {
if (!s.startBB(*bb))
continue;

add support for 'return void'
fixes #33