add ConstantInt and move IntConst to Constant
MODIFY
ir/constant.cpp
ir/constant.cpp
using namespace smt;
using namespace std;
+using namespace util;
namespace IR {
@@ -15,10 +16,6 @@ void Constant::print(ostream &os) const {
UNREACHABLE();
}
-pair<expr, expr> Constant::toSMT_cnst() const {
- return { expr::mkVar(getName().c_str(), bits()), true };
-}
-
StateValue Constant::toSMT(State &s) const {
auto ret = toSMT_cnst();
s.addUB(move(ret.second));
@@ -26,6 +23,33 @@ StateValue Constant::toSMT(State &s) const {
}
+IntConst::IntConst(Type &type, int64_t val)
+ : Constant(type, to_string(val)), val(val) {}
+
+IntConst::IntConst(Type &type, string &&val)
+ : Constant(type, string(val)), val(move(val)) {}
+
+pair<expr, expr> IntConst::toSMT_cnst() const {
+ if (auto v = get_if<int64_t>(&val))
+ return { expr::mkInt(*v, bits()), true };
+ return { expr::mkInt(get<string>(val).c_str(), bits()), true };
+}
+
+expr IntConst::getTypeConstraints() const {
+ unsigned min_bits = 0;
+ if (auto v = get_if<int64_t>(&val))
+ min_bits = (*v >= 0 ? 63 : 64) - num_sign_bits(*v);
+
+ return Value::getTypeConstraints() &&
+ getType().enforceIntType() &&
+ getType().sizeVar().uge(min_bits);
+}
+
+pair<expr, expr> ConstantInput::toSMT_cnst() const {
+ return { expr::mkVar(getName().c_str(), bits()), true };
+}
+
+
ConstantBinOp::ConstantBinOp(Type &type, Constant &lhs, Constant &rhs, Op op)
: Constant(type, ""), lhs(lhs), rhs(rhs), op(op) {
const char *opname = nullptr;

MODIFY
ir/constant.h
ir/constant.h
@@ -15,9 +15,28 @@ class Constant : public Value {
public:
Constant(Type &type, std::string &&name) : Value(type, std::move(name)) {}
void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
// <value, UB>
+ virtual std::pair<smt::expr, smt::expr> toSMT_cnst() const = 0;
+};
+
+
+class IntConst final : public Constant {
+ std::variant<int64_t, std::string> val;
+
+public:
+ IntConst(Type &type, int64_t val);
+ IntConst(Type &type, std::string &&val);
+ 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)
+ : Constant(type, std::move(name)) {}
virtual std::pair<smt::expr, smt::expr> toSMT_cnst() const;
- StateValue toSMT(State &s) const override;
};

MODIFY
ir/value.cpp
ir/value.cpp
#include "util/compiler.h"
using namespace smt;
-using namespace util;
using namespace std;
static unsigned gbl_fresh_id = 0;
@@ -37,33 +36,6 @@ ostream& operator<<(ostream &os, const Value &val) {
}
-IntConst::IntConst(Type &type, int64_t val)
- : Value(type, to_string(val)), val(val) {}
-
-IntConst::IntConst(Type &type, string &&val)
- : Value(type, string(val)), val(move(val)) {}
-
-void IntConst::print(ostream &os) const {
- UNREACHABLE();
-}
-
-StateValue IntConst::toSMT(State &s) const {
- if (auto v = get_if<int64_t>(&val))
- return { expr::mkInt(*v, bits()), true };
- return { expr::mkInt(get<string>(val).c_str(), bits()), true };
-}
-
-expr IntConst::getTypeConstraints() const {
- unsigned min_bits = 0;
- if (auto v = get_if<int64_t>(&val))
- min_bits = (*v >= 0 ? 63 : 64) - num_sign_bits(*v);
-
- return Value::getTypeConstraints() &&
- getType().enforceIntType() &&
- getType().sizeVar().uge(min_bits);
-}
-
-
void UndefValue::print(ostream &os) const {
UNREACHABLE();
}

MODIFY
ir/value.h
ir/value.h
@@ -43,18 +43,6 @@ public:
};
-class IntConst final : public Value {
- std::variant<int64_t, std::string> val;
-
-public:
- IntConst(Type &type, int64_t val);
- IntConst(Type &type, std::string &&val);
- void print(std::ostream &os) const override;
- StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
-};
-
-
class UndefValue final : public Value {
public:
UndefValue(Type &type) : Value(type, "undef") {}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -57,7 +57,7 @@ static Value& get_constant(string_view name, Type &type) {
I != identifiers.end())
return *I->second;
- auto c = make_unique<Constant>(type, string(id));
+ auto c = make_unique<ConstantInput>(type, string(id));
auto ret = c.get();
fn->addConstant(move(c));
identifiers.emplace(move(id), ret);

add ConstantInt and move IntConst to Constant