add initial support for function calls
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -528,6 +528,65 @@ unique_ptr<Instr> Select::dup(const string &suffix) const {
}
+void FnCall::addArg(Value &arg) {
+ args.emplace_back(&arg);
+}
+
+void FnCall::print(ostream &os) const {
+ auto printType = [](auto &t) {
+ auto type = t.toString();
+ return type.empty() ? type : type + ' ';
+ };
+
+ os << getName() << " = call " << printType(getType()) << fnName << '(';
+
+ bool first = true;
+ for (auto arg : args) {
+ if (!first)
+ os << ", ";
+ os << *arg;
+ first = false;
+ }
+ os << ')';
+}
+
+StateValue FnCall::toSMT(State &s) const {
+ // TODO: add support for memory
+ // TODO: add support for global variables
+ vector<expr> args_eval;
+
+ for (auto arg : args) {
+ auto &[v, p] = s[*arg];
+ // if the value is poison, mask out the arithmetic result
+ args_eval.emplace_back(expr::mkIf(p, v, expr::mkUInt(0, v.bits())));
+ args_eval.emplace_back(p);
+ }
+
+ // impact of the function on the domain of the program
+ // TODO: constraint when certain attributes are on
+ auto ub_name = fnName + "_ub";
+ s.addUB(expr::mkUF(ub_name.c_str(), args_eval, true));
+
+ if (dynamic_cast<VoidType*>(&getType()))
+ return {};
+
+ auto poison_name = fnName + "_poison";
+ return { expr::mkUF(fnName.c_str(), args_eval, getType().getDummyValue()),
+ expr::mkUF(poison_name.c_str(), args_eval, true) };
+}
+
+expr FnCall::getTypeConstraints(const Function &f) const {
+ // TODO : also need to name each arg type smt var uniquely
+ return Value::getTypeConstraints();
+}
+
+unique_ptr<Instr> FnCall::dup(const string &suffix) const {
+ auto r = make_unique<FnCall>(getType(), getName() + suffix, string(fnName));
+ r->args = args;
+ return r;
+}
+
+
ICmp::ICmp(Type &type, string &&name, Cond cond, Value &a, Value &b)
: Instr(type, move(name)), a(a), b(b), cond(cond), defined(cond != Any) {
if (!defined)

MODIFY
ir/instr.h
ir/instr.h
@@ -76,7 +76,8 @@ private:
Op op;
public:
- TernaryOp(Type &type, std::string &&name, Value &A, Value &B, Value &C, Op op)
+ TernaryOp(Type &type, std::string &&name, Value &A, Value &B, Value &C,
+ Op op)
: Instr(type, std::move(name)), A(A), B(B), C(C), op(op) {}
void print(std::ostream &os) const override;
@@ -107,7 +108,21 @@ class Select final : public Instr {
Value &cond, &a, &b;
public:
Select(Type &type, std::string &&name, Value &cond, Value &a, Value &b)
- : Instr(type, move(name)), cond(cond), a(a), b(b) {}
+ : Instr(type, std::move(name)), cond(cond), a(a), b(b) {}
+ 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 FnCall final : public Instr {
+ std::string fnName;
+ std::vector<Value*> args;
+public:
+ FnCall(Type &type, std::string &&name, std::string &&fnName)
+ : Instr(type, std::move(name)) , fnName(std::move(fnName)) {}
+ void addArg(Value &arg);
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints(const Function &f) const override;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -113,6 +113,10 @@ string Type::toString() const {
Type::~Type() {}
+expr VoidType::getDummyValue() const {
+ UNREACHABLE();
+}
+
expr VoidType::getTypeConstraints() const {
return true;
}
@@ -130,6 +134,10 @@ unsigned IntType::bits() const {
return bitwidth;
}
+expr IntType::getDummyValue() const {
+ return expr::mkUInt(0, bits());
+}
+
expr IntType::getTypeConstraints() const {
// since size cannot be unbounded, limit it between 1 and 64 bits if undefined
auto bw = sizeVar();
@@ -170,6 +178,11 @@ void IntType::print(ostream &os) const {
}
+expr FloatType::getDummyValue() const {
+ // TODO
+ return {};
+}
+
expr FloatType::getTypeConstraints() const {
// TODO
return false;
@@ -189,6 +202,11 @@ void FloatType::print(ostream &os) const {
}
+expr PtrType::getDummyValue() const {
+ // TODO
+ return {};
+}
+
expr PtrType::getTypeConstraints() const {
// TODO
return false;
@@ -216,6 +234,11 @@ void PtrType::print(ostream &os) const {
}
+expr ArrayType::getDummyValue() const {
+ // TODO
+ return {};
+}
+
expr ArrayType::getTypeConstraints() const {
// TODO
return false;
@@ -239,6 +262,11 @@ void ArrayType::print(ostream &os) const {
}
+expr VectorType::getDummyValue() const {
+ // TODO
+ return {};
+}
+
expr VectorType::getTypeConstraints() const {
// TODO
return false;
@@ -274,6 +302,11 @@ unsigned StructType::bits() const {
return res;
}
+expr StructType::getDummyValue() const {
+ // TODO
+ return {};
+}
+
expr StructType::getTypeConstraints() const {
expr res(true);
for (auto c : children) {
@@ -362,6 +395,20 @@ unsigned SymbolicType::bits() const {
UNREACHABLE();
}
+expr SymbolicType::getDummyValue() const {
+ switch (typ) {
+ case Int: return i.getDummyValue();
+ case Float: return f.getDummyValue();
+ case Ptr: return p.getDummyValue();
+ case Array: return a.getDummyValue();
+ case Vector: return v.getDummyValue();
+ case Struct: return s.getDummyValue();
+ case Undefined:
+ break;
+ }
+ UNREACHABLE();
+}
+
expr SymbolicType::getTypeConstraints() const {
expr c(false);
c |= isInt() && i.getTypeConstraints();

MODIFY
ir/type.h
ir/type.h
@@ -33,6 +33,9 @@ public:
Type(std::string &&name) : name(std::move(name)) {}
virtual unsigned bits() const;
+ // to use when one needs the corresponding SMT type
+ virtual smt::expr getDummyValue() const = 0;
+
virtual smt::expr getTypeConstraints() const = 0;
virtual smt::expr sizeVar() const;
smt::expr operator==(const Type &rhs) const;
@@ -59,6 +62,7 @@ public:
class VoidType final : public Type {
public:
VoidType() : Type("void") {}
+ smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
void fixup(const smt::Model &m) override;
void print(std::ostream &os) const override;
@@ -75,6 +79,7 @@ public:
: Type(std::move(name)), bitwidth(bitwidth), defined(true) {}
unsigned bits() const override;
+ smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
smt::expr operator==(const IntType &rhs) const;
@@ -89,6 +94,7 @@ public:
class FloatType final : public Type {
public:
FloatType(std::string &&name) : Type(std::move(name)) {}
+ smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const FloatType &rhs) const;
void fixup(const smt::Model &m) override;
@@ -99,6 +105,7 @@ public:
class PtrType final : public Type {
public:
PtrType(std::string &&name) : Type(std::move(name)) {}
+ smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const PtrType &rhs) const;
void fixup(const smt::Model &m) override;
@@ -111,6 +118,7 @@ public:
class ArrayType final : public Type {
public:
ArrayType(std::string &&name) : Type(std::move(name)) {}
+ smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const ArrayType &rhs) const;
void fixup(const smt::Model &m) override;
@@ -122,6 +130,7 @@ public:
class VectorType final : public Type {
public:
VectorType(std::string &&name) : Type(std::move(name)) {}
+ smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const VectorType &rhs) const;
void fixup(const smt::Model &m) override;
@@ -140,6 +149,7 @@ public:
: Type(std::move(name)), children(std::move(children)) {}
unsigned bits() const override;
+ smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const StructType &rhs) const;
void fixup(const smt::Model &m) override;
@@ -172,6 +182,7 @@ private:
public:
SymbolicType(std::string &&name, bool named = false);
unsigned bits() const override;
+ smt::expr getDummyValue() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const Type &rhs) const;
void fixup(const smt::Model &m) override;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -837,6 +837,25 @@ expr expr::extract(unsigned high, unsigned low) const {
return Z3_mk_extract(ctx(), high, low, ast());
}
+expr expr::mkUF(const char *name, const vector<expr> &args, const expr &range){
+ auto num_args = args.size();
+ vector<Z3_ast> z3_args;
+ vector<Z3_sort> z3_sorts;
+ z3_args.reserve(num_args);
+ z3_sorts.reserve(num_args);
+
+ for (auto &arg : args) {
+ if (!arg.isValid())
+ return {};
+ z3_args.emplace_back(arg());
+ z3_sorts.emplace_back(arg.sort());
+ }
+
+ auto decl = Z3_mk_func_decl(ctx(), Z3_mk_string_symbol(ctx(), name),
+ num_args, z3_sorts.data(), range.sort());
+ return Z3_mk_app(ctx(), decl, num_args, z3_args.data());
+}
+
expr expr::mkIf(const expr &cond, const expr &then, const expr &els) {
C2(cond, then, els);
if (cond.isTrue() || then.eq(els))

MODIFY
smt/expr.h
smt/expr.h
@@ -183,6 +183,11 @@ public:
expr concat(const expr &rhs) const;
expr extract(unsigned high, unsigned low) const;
+ // we don't expose SMT expr types, so range must be passed as a dummy value
+ // of the desired type
+ static expr mkUF(const char *name, const std::vector<expr> &args,
+ const expr &range);
+
static expr mkIf(const expr &cond, const expr &then, const expr &els);
static expr mkForAll(const std::set<expr> &vars, expr &&val);

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -283,6 +283,27 @@ public:
ConversionOp::Trunc));
}
+ RetTy visitCallInst(llvm::CallInst &i) {
+ // TODO: support attributes
+ auto fn = i.getCalledFunction();
+ if (!fn) // TODO: support indirect calls
+ return error(i);
+
+ auto ty = llvm_type2alive(i.getType());
+ if (!ty)
+ return error(i);
+
+ string fn_name = '@' + fn->getName().str();
+ auto call = make_unique<FnCall>(*ty, value_name(i), move(fn_name));
+ for (auto &arg : i.args()) {
+ auto a = get_operand(arg);
+ if (!a)
+ error(i);
+ call->addArg(*a);
+ }
+ RETURN_IDENTIFIER(move(call));
+ }
+
RetTy visitICmpInst(llvm::ICmpInst &i) {
PARSE_BINOP();
ICmp::Cond cond;
@@ -610,6 +631,7 @@ struct TVPass : public llvm::FunctionPass {
done = true;
if (!opt_report_dir.empty()) {
+ // TODO: make dir if it doesn't exit
auto &source_file = module.getSourceFileName();
fs::path fname = source_file.empty() ? "alive.txt" : source_file;
fname.replace_extension(".txt");

add initial support for function calls