fix misc bug fixes & crashes
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -160,7 +160,7 @@ BinOp::~BinOp() {}
void Return::print(ostream &os) const {
- os << "return ";
+ os << "ret ";
printType(os);
os << val.getName();
}

MODIFY
ir/type.cpp
ir/type.cpp
@@ -114,11 +114,12 @@ expr IntType::getTypeConstraints() const {
auto bw = var("bw", var_bw_bits);
if (defined) {
c &= bw == expr::mkUInt(bitwidth, var_bw_bits);
- } else {
+ }
+
// limit ints to be between 1 and 64 bits
+ // TODO: lift 64-bit restriction
c &= bw.uge(expr::mkUInt(1, var_bw_bits));
c &= bw.ule(expr::mkUInt(64, var_bw_bits));
- }
return c;
}

MODIFY
ir/value.cpp
ir/value.cpp
@@ -38,7 +38,7 @@ ostream& operator<<(ostream &os, const Value &val) {
}
-IntConst::IntConst(unique_ptr<Type> &&type, uint64_t val)
+IntConst::IntConst(unique_ptr<Type> &&type, int64_t val)
: Value(move(type), to_string(val), true), val(val) {
getWType().enforceIntType();
}
@@ -48,12 +48,13 @@ void IntConst::print(ostream &os) const {
}
StateValue IntConst::toSMT(State &s) const {
- return { expr::mkUInt(val, bits()), true };
+ return { expr::mkInt(val, bits()), true };
}
expr IntConst::getTypeConstraints() const {
+ unsigned min_bits = (val >= 0 ? 63 : 64) - num_sign_bits(val);
return getType().getTypeConstraints() &&
- getType().atLeastBits(ilog2(val));
+ getType().atLeastBits(min_bits);
}
IntConst::~IntConst() {}

MODIFY
ir/value.h
ir/value.h
@@ -39,10 +39,10 @@ public:
class IntConst final : public Value {
- uint64_t val;
+ int64_t val;
public:
- IntConst(std::unique_ptr<Type> &&type, uint64_t val);
+ IntConst(std::unique_ptr<Type> &&type, int64_t 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
@@ -213,6 +213,16 @@ bool expr::isAllOnes() const {
return isInt(n) && n == -1;
}
+bool expr::isSMin() const {
+ uint64_t n = 0;
+ return isUInt(n) && n == (1ull << (bits() - 1));
+}
+
+bool expr::isSMax() const {
+ uint64_t n = 0;
+ return isUInt(n) && n == ((uint64_t)INT64_MAX >> (64 - bits()));
+}
+
unsigned expr::bits() const {
return Z3_get_bv_sort_size(ctx(), sort());
}
@@ -224,7 +234,13 @@ bool expr::isUInt(uint64_t &n) const {
bool expr::isInt(int64_t &n) const {
C();
- return Z3_get_numeral_int64(ctx(), ast(), &n) == Z3_TRUE;
+ if (Z3_get_numeral_int64(ctx(), ast(), &n) == Z3_FALSE)
+ return false;
+
+ auto bw = bits();
+ if (bw < 64)
+ n = (int64_t)((uint64_t)n << (64 - bw)) >> (64 - bw);
+ return true;
}
bool expr::isNot(expr &neg) const {
@@ -293,6 +309,8 @@ expr expr::operator+(const expr &rhs) const {
}
expr expr::operator-(const expr &rhs) const {
+ if (eq(rhs))
+ return mkUInt(0, sort());
return *this + mkInt(-1, sort()) * rhs;
}
@@ -303,6 +321,15 @@ expr expr::operator*(const expr &rhs) const {
expr expr::sdiv(const expr &rhs) const {
C(rhs);
+ if (eq(rhs))
+ return mkUInt(1, sort());
+
+ if (rhs.isZero())
+ return rhs;
+
+ if (isSMin() && rhs.isAllOnes())
+ return mkUInt(0, sort());
+
expr r;
if (binop_sfold(rhs, [](auto a, auto b) { return a / b; }, r))
return r;
@@ -313,6 +340,12 @@ expr expr::sdiv(const expr &rhs) const {
expr expr::udiv(const expr &rhs) const {
C(rhs);
+ if (eq(rhs))
+ return mkUInt(1, sort());
+
+ if (rhs.isZero())
+ return rhs;
+
expr r;
if (binop_ufold(rhs, [](auto a, auto b) { return a / b; }, r))
return r;

MODIFY
smt/expr.h
smt/expr.h
@@ -84,6 +84,8 @@ public:
bool isZero() const;
bool isOne() const;
bool isAllOnes() const;
+ bool isSMin() const;
+ bool isSMax() const;
unsigned bits() const;
bool isUInt(uint64_t &n) const;

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -97,7 +97,7 @@ re2c:yyfill:check = 0;
return INT_TYPE;
}
-[0-9]+ {
+"-"?[0-9]+ {
yylval.num = strtoull((char*)YYTEXT, nullptr, 10);
return NUM;
}
@@ -135,7 +135,7 @@ re2c:yyfill:check = 0;
"nsw" { return NSW; }
"nuw" { return NUW; }
"exact" { return EXACT; }
-"return" { return RETURN; }
+"ret" { return RETURN; }
"unreachable" { return UNREACH; }
* { error("couldn't parse: '" + string((char*)YYTEXT, 16) + '\''); }

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -90,6 +90,8 @@ void TypingAssignments::operator++(void) {
}
TypingAssignments Transform::getTypings() const {
+ // TODO: missing cross-program type constraints
+ // e.g. for inputs and return values
return { src.getTypeConstraints() && tgt.getTypeConstraints() };
}

MODIFY
util/compiler.cpp
util/compiler.cpp
@@ -22,4 +22,12 @@ unsigned ilog2(uint64_t n) {
#endif
}
+unsigned num_sign_bits(uint64_t n) {
+#ifdef __GNUC__
+ return __builtin_clrsbll(n);
+#else
+# error Unknown compiler
+#endif
+}
+
}

MODIFY
util/compiler.h
util/compiler.h
@@ -41,5 +41,6 @@ struct const_strip_unique_ptr {
};
unsigned ilog2(uint64_t n);
+unsigned num_sign_bits(uint64_t n);
}

fix misc bug fixes & crashes