Support for overflow instructions
+ add Structure type
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -45,6 +45,15 @@ expr IntConst::getTypeConstraints() const {
getType().sizeVar().uge(min_bits);
}
+bool IntConst::isIntConst(int64_t &n) const {
+ if (auto v = get_if<int64_t>(&val))
+ n = *v;
+ else if (auto v = get_if<string>(&val))
+ n = std::stoll(*v);
+
+ return true;
+}
+
pair<expr, expr> ConstantInput::toSMT_cnst() const {
return { expr::mkVar(getName().c_str(), bits()), true };
}

MODIFY
ir/constant.h
ir/constant.h
@@ -29,6 +29,7 @@ public:
IntConst(Type &type, std::string &&val);
virtual std::pair<smt::expr, smt::expr> toSMT_cnst() const override;
smt::expr getTypeConstraints() const override;
+ bool isIntConst(int64_t &n) const override;
};

MODIFY
ir/instr.cpp
ir/instr.cpp
#include "ir/instr.h"
#include "ir/function.h"
+#include "ir/type.h"
#include "smt/expr.h"
#include "smt/solver.h"
#include "util/compiler.h"
@@ -49,6 +50,8 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
case Xor:
case Cttz:
case Ctlz:
+ case SAdd_Overflow:
+ case ExtractValue:
assert(flags == 0);
break;
}
@@ -76,6 +79,8 @@ void BinOp::print(ostream &os) const {
case Xor: str = "xor"; break;
case Cttz: str = "cttz"; break;
case Ctlz: str = "ctlz"; break;
+ case SAdd_Overflow: str = "sadd_overflow"; break;
+ case ExtractValue: str = "extractvalue"; break;
}
const char *flag = nullptr;
@@ -226,25 +231,65 @@ StateValue BinOp::toSMT(State &s) const {
val = a.ctlz();
not_poison &= (b == 0u || a != 0u);
break;
+
+ case SAdd_Overflow:
+ val = a + b;
+ val = val.concat(expr::mkIf(a.add_no_soverflow(b),
+ expr::mkUInt(0, 1),
+ expr::mkUInt(1, 1)));
+ break;
+
+ case ExtractValue:
+ {
+ auto &structType = static_cast<StructureType&>(lhs.getType());
+ uint64_t index;
+ ENSURE(b.isUInt(index));
+ val = structType.extract(a, index);
+ break;
+ }
}
+
return { move(val), move(not_poison) };
}
expr BinOp::getTypeConstraints(const Function &f) const {
expr instrconstr;
switch (op) {
+ case ExtractValue:
+ {
+ int64_t n;
+ instrconstr = lhs.getType().enforceStructureType() &&
+ rhs.isIntConst(n);
+ auto structType = dynamic_cast<StructureType*>(&lhs.getType());
+ if (structType &&
+ n >= 0 && n < static_cast<int64_t>(structType->numElements())) {
+ instrconstr = instrconstr &&
+ structType->getChildType(n) == getType();
+ } else {
+ instrconstr = false;
+ }
+ break;
+ }
+ case SAdd_Overflow:
+ instrconstr = lhs.getType() == rhs.getType() &&
+ lhs.getType().enforceIntType() &&
+ getType().enforceStructureType();
+ break;
case Cttz:
case Ctlz:
- instrconstr = (rhs.getType().enforceIntType() &&
- rhs.getType().sizeVar() == 1u);
+ instrconstr = rhs.getType().enforceIntType() &&
+ rhs.getType().sizeVar() == 1u &&
+ getType().enforceIntOrPtrOrVectorType() &&
+ getType() == lhs.getType();
break;
default:
- instrconstr = (getType() == rhs.getType());
+ instrconstr = getType() == rhs.getType() &&
+ getType().enforceIntOrPtrOrVectorType() &&
+ getType() == lhs.getType();
+ break;
}
return Value::getTypeConstraints() &&
- getType().enforceIntOrPtrOrVectorType() &&
- getType() == lhs.getType() &&
move(instrconstr);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -29,6 +29,7 @@ class BinOp final : public Instr {
public:
enum Op { Add, Sub, Mul, SDiv, UDiv, SRem, URem, Shl, AShr, LShr,
SAdd_Sat, UAdd_Sat, SSub_Sat, USub_Sat,
+ SAdd_Overflow, ExtractValue,
And, Or, Xor, Cttz, Ctlz };
enum Flags { None = 0, NSW = 1, NUW = 2, NSWNUW = 3, Exact = 4 };

MODIFY
ir/type.cpp
ir/type.cpp
@@ -40,6 +40,7 @@ expr Type::isFloat() const { return is(SymbolicType::Float); }
expr Type::isPtr() const { return is(SymbolicType::Ptr); }
expr Type::isArray() const { return is(SymbolicType::Array); }
expr Type::isVector() const { return is(SymbolicType::Vector); }
+expr Type::isStructure() const { return is(SymbolicType::Structure); }
unsigned Type::bits() const {
UNREACHABLE();
@@ -85,6 +86,10 @@ expr Type::enforceIntOrPtrOrVectorType() const {
return false;
}
+expr Type::enforceStructureType() const {
+ return false;
+}
+
ostream& operator<<(ostream &os, const Type &t) {
t.print(os);
return os;
@@ -247,10 +252,78 @@ void VectorType::print(ostream &os) const {
os << "TODO";
}
+expr StructureType::getTypeConstraints() const {
+ expr res(true);
+ for (auto type : children) {
+ res &= type->enforceIntType();
+ }
+
+ return res;
+}
+
+expr StructureType::operator==(const StructureType &rhs) const {
+ if (children.size() != rhs.children.size())
+ return false;
+
+ expr res(false);
+ for (unsigned i = 0; i < children.size(); i++) {
+ res = res || *children[i] == *rhs.children[i];
+ }
+
+ return res;
+}
+
+expr StructureType::enforceStructureType() const {
+ return !children.empty();
+}
+
+void StructureType::fixup(const Model &m) {
+ // TODO
+}
+
+expr StructureType::enforceIntOrPtrOrVectorType() const {
+ return false;
+}
+
+unsigned StructureType::bits() const {
+ unsigned res = 0;
+ for (unsigned i = 0; i < children.size(); i++) {
+ res += children[i]->bits();
+ }
+
+ return res;
+}
+
+void StructureType::print(ostream &os) const {
+ assert(children.size() > 0);
+ os << '{';
+ children[0]->print(os);
+ for (unsigned i = 1; i < children.size(); i++) {
+ os << ", ";
+ children[i]->print(os);
+ }
+ os << '}';
+}
+
+Type& StructureType::getChildType(unsigned index) const {
+ assert(index < children.size());
+ return *children[index];
+}
+
+expr StructureType::extract(const expr &struct_val, unsigned index) const {
+ unsigned total_till_now = 0;
+ assert(index < children.size());
+ for (unsigned i = 0; i <= index; i++) {
+ total_till_now += children[i]->bits();
+ }
+ unsigned low = struct_val.bits() - total_till_now;
+ return struct_val.extract(low + children[index]->bits() - 1, low);
+}
+
SymbolicType::SymbolicType(string &&name, bool named)
: Type(string(name)), i(string(name)), f(string(name)), p(string(name)),
- a(string(name)), v(string(name)), named(named) {}
+ a(string(name)), v(string(name)), st(string(name)), named(named) {}
unsigned SymbolicType::bits() const {
switch (typ) {
@@ -259,6 +332,7 @@ unsigned SymbolicType::bits() const {
case Ptr: return p.bits();
case Array: return a.bits();
case Vector: return v.bits();
+ case Structure: return st.bits();
case Undefined:
assert(0 && "undefined at SymbolicType::bits()");
}
@@ -289,6 +363,8 @@ expr SymbolicType::operator==(const Type &b) const {
return isArray() && a == *rhs;
if (auto rhs = dynamic_cast<const VectorType*>(&b))
return isVector() && v == *rhs;
+ if (auto rhs = dynamic_cast<const StructureType*>(&b))
+ return isStructure() && st == *rhs;
if (auto rhs = dynamic_cast<const SymbolicType*>(&b)) {
expr c(false);
@@ -297,6 +373,7 @@ expr SymbolicType::operator==(const Type &b) const {
c |= isPtr() && p == rhs->p;
c |= isArray() && a == rhs->a;
c |= isVector() && v == rhs->v;
+ c |= isStructure() && st == rhs->st;
return move(c) && typeVar() == rhs->typeVar();
}
assert(0 && "unhandled case in SymbolicType::operator==");
@@ -314,6 +391,7 @@ void SymbolicType::fixup(const Model &m) {
case Ptr: p.fixup(m); break;
case Array: a.fixup(m); break;
case Vector: v.fixup(m); break;
+ case Structure: st.fixup(m); break;
case Undefined:
UNREACHABLE();
}
@@ -331,6 +409,10 @@ expr SymbolicType::enforceIntOrPtrOrVectorType() const {
return isInt() || isPtr() || isVector();
}
+expr SymbolicType::enforceStructureType() const {
+ return isStructure();
+}
+
void SymbolicType::print(ostream &os) const {
if (named) {
os << name;
@@ -343,6 +425,7 @@ void SymbolicType::print(ostream &os) const {
case Ptr: p.print(os); break;
case Array: a.print(os); break;
case Vector: v.print(os); break;
+ case Structure: st.print(os); break;
case Undefined: break;
}
}

MODIFY
ir/type.h
ir/type.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "smt/expr.h"
+
#include <memory>
-#include <string>
#include <ostream>
+#include <string>
namespace smt { class Model; }
@@ -25,6 +26,7 @@ protected:
smt::expr isPtr() const;
smt::expr isArray() const;
smt::expr isVector() const;
+ smt::expr isStructure() const;
public:
Type(std::string &&name) : name(std::move(name)) {}
@@ -38,6 +40,7 @@ public:
virtual smt::expr enforceIntType() const;
virtual smt::expr enforceIntOrVectorType() const;
virtual smt::expr enforceIntOrPtrOrVectorType() const;
+ virtual smt::expr enforceStructureType() const;
virtual void print(std::ostream &os) const = 0;
friend std::ostream& operator<<(std::ostream &os, const Type &t);
@@ -123,9 +126,31 @@ public:
};
+class StructureType final : public Type {
+ const std::vector<Type*> children;
+
+public:
+ StructureType(std::string &&name) : Type(std::move(name)) {}
+ StructureType(std::string &&name, std::vector<Type*> &&children)
+ : Type(std::move(name)), children(children) { }
+
+ unsigned bits() const override;
+ smt::expr enforceStructureType() const override;
+ smt::expr getTypeConstraints() const override;
+ smt::expr operator==(const StructureType &rhs) const;
+ void fixup(const smt::Model &m) override;
+ smt::expr enforceIntOrPtrOrVectorType() const override;
+ void print(std::ostream &os) const override;
+ auto numElements() const { return children.size(); }
+ Type& getChildType(unsigned index) const;
+ // Extracts the type located at \p index from \p struct_val
+ smt::expr extract(const smt::expr &struct_val, unsigned index) const;
+};
+
+
class SymbolicType final : public Type {
public:
- enum TypeNum { Int, Float, Ptr, Array, Vector, Undefined };
+ enum TypeNum { Int, Float, Ptr, Array, Vector, Structure, Undefined };
private:
TypeNum typ = Undefined;
@@ -134,6 +159,7 @@ private:
PtrType p;
ArrayType a;
VectorType v;
+ StructureType st;
bool named;
public:
@@ -145,6 +171,7 @@ public:
smt::expr enforceIntType() const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
+ smt::expr enforceStructureType() const override;
void print(std::ostream &os) const override;
};

MODIFY
ir/value.h
ir/value.h
@@ -42,6 +42,8 @@ public:
static void reset_gbl_id();
+ virtual bool isIntConst(int64_t &n) const { return false; }
+
friend std::ostream& operator<<(std::ostream &os, const Value &val);
virtual ~Value() {}

ADD
tests/unit/overflow.opt
+Name: overflow test
+%a = sadd_overflow i8 20, 120
+%b = extractvalue %a, 1
+ =>
+%a = sadd_overflow i8 20, 120
+%b = 1
+
+Name: overflow test2
+%a = sadd_overflow i8 20, 10
+%b = extractvalue %a, 0
+ =>
+%a = sadd_overflow i8 20, 10
+%b = 30
+
+Name: overflow simple add
+%a = sadd_overflow i8 120, 5
+%b = extractvalue %a, 0
+ =>
+%a = sadd_overflow i8 120, 5
+%b = add i8 120, 5

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -202,6 +202,8 @@ re2c:yyfill:check = 0;
"cttz" { return CTTZ; }
"ctlz" { return CTLZ; }
"ctpop" { return CTPOP; }
+"extractvalue" { return EXTRACTVALUE; }
+"sadd_overflow" { return SADD_OVERFLOW; }
"unreachable" { return UNREACH; }
[a-zA-Z][a-zA-Z0-9]* {

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -220,9 +220,35 @@ static void parse_comma() {
}
+static unordered_map<Type*, unique_ptr<StructureType>> overflow_aggregate_types;
static vector<unique_ptr<SymbolicType>> sym_types;
static unsigned sym_num;
+static Type& get_overflow_type(Type &type) {
+ auto t = make_unique<StructureType>("oaggty",
+ std::initializer_list<Type*>(
+ { &type,
+ int_types[1].get()}));
+ auto res = overflow_aggregate_types.emplace(&type, move(t));
+ return *res.first->second.get();
+}
+
+static Type& get_sym_type() {
+ if (sym_num < sym_types.size())
+ return *sym_types[sym_num++].get();
+
+ auto t = make_unique<SymbolicType>("symty_" + to_string(sym_num++));
+ return *sym_types.emplace_back(move(t)).get();
+}
+
+static Type& get_int_type(unsigned size) {
+ if (!int_types[size])
+ int_types[size] =
+ make_unique<IntType>("i" + to_string(size), size);
+
+ return *int_types[size].get();
+}
+
static Type& parse_type(bool optional = true) {
switch (auto t = *tokenizer) {
case INT_TYPE:
@@ -232,20 +258,12 @@ static Type& parse_type(bool optional = true) {
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();
+ return get_int_type(yylval.num);
default:
if (optional) {
tokenizer.unget(t);
- if (sym_num < sym_types.size())
- return *sym_types[sym_num++].get();
-
- auto t = make_unique<SymbolicType>("symty_" + to_string(sym_num++));
- return *sym_types.emplace_back(move(t)).get();
+ return get_sym_type();
} else {
error("Expecting a type", t);
}
@@ -383,6 +401,8 @@ static BinOp::Flags parse_binop_flags(token op_token) {
case XOR:
case CTTZ:
case CTLZ:
+ case SADD_OVERFLOW:
+ case EXTRACTVALUE:
return BinOp::None;
default:
UNREACHABLE();
@@ -394,8 +414,13 @@ static unique_ptr<Instr> parse_binop(string_view name, token op_token) {
auto &type = parse_type();
auto &a = parse_operand(type);
parse_comma();
- auto &type2 = try_parse_type(type);
- auto &b = parse_operand(type2);
+
+ // 2nd binop argument handling
+ Type *type2 = &try_parse_type(type);
+ if (op_token == EXTRACTVALUE)
+ type2 = &get_int_type(64);
+ auto &b = parse_operand(*type2);
+ Type *rettype = &type;
BinOp::Op op;
switch (op_token) {
@@ -418,10 +443,18 @@ static unique_ptr<Instr> parse_binop(string_view name, token op_token) {
case UADD_SAT: op = BinOp::UAdd_Sat; break;
case SSUB_SAT: op = BinOp::SSub_Sat; break;
case USUB_SAT: op = BinOp::USub_Sat; break;
+ case SADD_OVERFLOW:
+ op = BinOp::SAdd_Overflow;
+ rettype = &get_overflow_type(type);
+ break;
+ case EXTRACTVALUE:
+ op = BinOp::ExtractValue;
+ rettype = &get_sym_type();
+ break;
default:
UNREACHABLE();
}
- return make_unique<BinOp>(type, string(name), a, b, op, flags);
+ return make_unique<BinOp>(*rettype, string(name), a, b, op, flags);
}
static unique_ptr<Instr> parse_unaryop(string_view name, token op_token) {
@@ -558,6 +591,8 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case XOR:
case CTTZ:
case CTLZ:
+ case SADD_OVERFLOW:
+ case EXTRACTVALUE:
return parse_binop(name, t);
case BITREVERSE:
case BSWAP:
@@ -671,6 +706,7 @@ parser_initializer::parser_initializer() {
parser_initializer::~parser_initializer() {
for_each(int_types.begin(), int_types.end(), [](auto &e) { e.reset(); });
sym_types.clear();
+ overflow_aggregate_types.clear();
}
}

MODIFY
tools/tokens.h
tools/tokens.h
@@ -24,6 +24,7 @@ TOKEN(CUGT)
TOKEN(EQ)
TOKEN(EQUALS)
TOKEN(EXACT)
+TOKEN(EXTRACTVALUE)
TOKEN(FALSE)
TOKEN(FREEZE)
TOKEN(FSHL)
@@ -49,6 +50,7 @@ TOKEN(REGISTER)
TOKEN(RETURN)
TOKEN(RPAREN)
TOKEN(SADD_SAT)
+TOKEN(SADD_OVERFLOW)
TOKEN(SDIV)
TOKEN(SELECT)
TOKEN(SEXT)

Support for overflow instructions (#28)

+ add Structure type