add support for ints > 64 bits
MODIFY
ir/type.cpp
ir/type.cpp
@@ -113,11 +113,12 @@ unsigned IntType::bits() const {
}
expr IntType::getTypeConstraints() const {
- // limit ints to be between 1 and 64 bits
- // TODO: lift 64-bit restriction
+ // since size cannot be unbounded, limit it between 1 and 64 bits if undefined
auto bw = sizeVar();
- return bw != expr::mkUInt(0, var_bw_bits) &&
- bw.ule(expr::mkUInt(64, var_bw_bits));
+ auto r = bw != expr::mkUInt(0, var_bw_bits);
+ if (!defined)
+ r &= bw.ule(expr::mkUInt(64, var_bw_bits));
+ return r;
}
expr IntType::sizeVar() const {

MODIFY
ir/value.cpp
ir/value.cpp
@@ -40,16 +40,24 @@ 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 {
- return { expr::mkInt(val, bits()), true };
+ 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 = (val >= 0 ? 63 : 64) - num_sign_bits(val);
+ 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);

MODIFY
ir/value.h
ir/value.h
#include "smt/expr.h"
#include <ostream>
#include <string>
+#include <variant>
namespace smt { class Model; }
@@ -43,10 +44,11 @@ public:
class IntConst final : public Value {
- int64_t val;
+ 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;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -159,6 +159,10 @@ expr expr::mkInt(int64_t n, unsigned bits) {
return mkInt(n, mkBVSort(bits));
}
+expr expr::mkInt(const char *n, unsigned bits) {
+ return Z3_mk_numeral(ctx(), n, mkBVSort(bits));
+}
+
expr expr::mkConst(Z3_func_decl decl) {
return Z3_mk_app(ctx(), decl, 0, {});
}

MODIFY
smt/expr.h
smt/expr.h
@@ -70,6 +70,7 @@ public:
static expr mkUInt(uint64_t n, unsigned bits);
static expr mkInt(int64_t n, unsigned bits);
+ static expr mkInt(const char *n, unsigned bits);
static expr mkVar(const char *name, unsigned bits);
static expr mkBoolVar(const char *name);

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
#include "tools/alive_lexer.h"
#include "util/compiler.h"
#include <cassert>
+#include <cerrno>
+#include <climits>
#include <cstdlib>
#include <iostream>
@@ -104,6 +106,10 @@ re2c:yyfill:check = 0;
"-"?[0-9]+ {
yylval.num = strtoull((char*)YYTEXT, nullptr, 10);
+ if (yylval.num == ULLONG_MAX && errno == ERANGE) {
+ COPY_STR();
+ return NUM_STR;
+ }
return NUM;
}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
#include "ir/value.h"
#include "tools/alive_lexer.h"
#include "util/compiler.h"
-#include <array>
#include <cassert>
#include <memory>
#include <unordered_map>
+#include <vector>
#define YYDEBUG 0
@@ -33,7 +33,7 @@ static void error(const char *s, token t) {
throw ParseException(string(s) + "; got: " + token_name[t], yylineno);
}
-static array<unique_ptr<IntType>, 65> int_types;
+static vector<unique_ptr<IntType>> int_types;
static unordered_map<string, Value*> identifiers;
static Function *fn;
@@ -44,6 +44,13 @@ static Value& get_constant(uint64_t n, Type &t) {
return *ret;
}
+static Value& get_num_constant(string_view n, Type &t) {
+ auto c = make_unique<IntConst>(t, string(n));
+ auto ret = c.get();
+ fn->addConstant(move(c));
+ return *ret;
+}
+
static Value& get_constant(string_view name, Type &type) {
string id(name);
if (auto I = identifiers.find(id);
@@ -219,10 +226,18 @@ static unsigned sym_num;
static Type& parse_type(bool optional = true) {
switch (auto t = *tokenizer) {
case INT_TYPE:
- if (yylval.num <= 64)
- return *int_types[yylval.num].get();
+ if (yylval.num > 4 * 1024)
error("Int type too long: " + to_string(yylval.num));
- break;
+
+ if (yylval.num >= int_types.size())
+ int_types.resize(yylval.num + 1);
+
+ if (!int_types[yylval.num])
+ int_types[yylval.num] =
+ make_unique<IntType>("i" + to_string(yylval.num), yylval.num);
+
+ return *int_types[yylval.num].get();
+
default:
if (optional) {
tokenizer.unget(t);
@@ -284,6 +299,8 @@ static Value& parse_operand(Type &type) {
switch (auto t = *tokenizer) {
case NUM:
return get_constant(yylval.num, type);
+ case NUM_STR:
+ return get_num_constant(yylval.str, type);
case TRUE:
return get_constant(1, type);
case FALSE:
@@ -619,11 +636,8 @@ vector<Transform> parse(string_view buf) {
parser_initializer::parser_initializer() {
- int_types[0] = nullptr;
-
- for (unsigned i = 1; i <= 64; ++i) {
- int_types[i] = make_unique<IntType>("i" + to_string(i), i);
- }
+ int_types.resize(65);
+ int_types[1] = make_unique<IntType>("i1", 1);
}
parser_initializer::~parser_initializer() {

MODIFY
tools/tokens.h
tools/tokens.h
@@ -37,6 +37,7 @@ TOKEN(NAME)
TOKEN(NE)
TOKEN(NSW)
TOKEN(NUM)
+TOKEN(NUM_STR)
TOKEN(NUW)
TOKEN(OR)
TOKEN(PLUS)

MODIFY
tv/tv.cpp
tv/tv.cpp
#include "llvm/IR/Operator.h"
#include "llvm/Pass.h"
#include "llvm/Support/raw_ostream.h"
-#include <array>
#include <iostream>
#include <optional>
#include <string>
#include <unordered_map>
+#include <vector>
using namespace IR;
using namespace tools;
@@ -33,7 +33,7 @@ string_view s(llvm::StringRef str) {
smt::smt_initializer smt_init;
TransformPrintOpts print_opts;
-array<unique_ptr<IntType>, 65> int_types;
+vector<unique_ptr<IntType>> int_types;
unordered_map<string, Function> fns;
unordered_map<const llvm::Value*, Value*> identifiers;
Function *current_fn;
@@ -45,11 +45,8 @@ unsigned value_id_counter; // for %0, %1, etc..
struct alive_init {
alive_init() {
- int_types[0] = nullptr;
-
- for (unsigned i = 1; i <= 64; ++i) {
- int_types[i] = make_unique<IntType>("i" + to_string(i), i);
- }
+ int_types.resize(65);
+ int_types[1] = make_unique<IntType>("i1", 1);
}
} alive_init;
@@ -77,7 +74,11 @@ Type* llvm_type2alive(const llvm::Type *ty) {
return &Type::voidTy;
case llvm::Type::IntegerTyID: {
auto bits = cast<llvm::IntegerType>(ty)->getBitWidth();
- return bits <= 64 ? int_types[bits].get() : nullptr;
+ if (bits >= int_types.size())
+ int_types.resize(bits + 1);
+ if (!int_types[bits])
+ int_types[bits] = make_unique<IntType>("i" + to_string(bits), bits);
+ return int_types[bits].get();
}
default:
errs() << "Unsupported type: " << *ty << '\n';
@@ -95,8 +96,11 @@ Value* get_operand(llvm::Value *v) {
return nullptr;
if (auto cnst = dyn_cast<llvm::ConstantInt>(v)) {
- // TODO: support > 64 bits
- auto c = make_unique<IntConst>(*ty, cnst->getZExtValue());
+ unique_ptr<IntConst> c;
+ if (cnst->getBitWidth() <= 64)
+ c = make_unique<IntConst>(*ty, cnst->getZExtValue());
+ else
+ c = make_unique<IntConst>(*ty, cnst->getValue().toString(10, false));
auto ret = c.get();
current_fn->addConstant(move(c));
return ret;

add support for ints > 64 bits