add support for saturating Add & Sub
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -47,7 +47,7 @@ static void div_ub(const expr &a, const expr &b, expr &ub, bool sign) {
auto bits = b.bits();
ub &= b != expr::mkUInt(0, bits);
if (sign)
- ub &= (a != expr::IntMin(bits) || b != expr::mkInt(-1, bits));
+ ub &= (a != expr::IntSMin(bits) || b != expr::mkInt(-1, bits));
}
pair<expr, expr> ConstantBinOp::toSMT_cnst() const {

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -40,6 +40,10 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
break;
case SRem:
case URem:
+ case SAdd_Sat:
+ case UAdd_Sat:
+ case SSub_Sat:
+ case USub_Sat:
case And:
case Or:
case Xor:
@@ -61,6 +65,10 @@ void BinOp::print(ostream &os) const {
case Shl: str = "shl"; break;
case AShr: str = "ashr"; break;
case LShr: str = "lshr"; break;
+ case SAdd_Sat: str = "sadd_sat"; break;
+ case UAdd_Sat: str = "uadd_sat"; break;
+ case SSub_Sat: str = "ssub_sat"; break;
+ case USub_Sat: str = "usub_sat"; break;
case And: str = "and"; break;
case Or: str = "or"; break;
case Xor: str = "xor"; break;
@@ -84,7 +92,7 @@ static void div_ub(State &s, const expr &a, const expr &b, const expr &ap,
s.addUB(bp);
s.addUB(b != expr::mkUInt(0, bits));
if (sign)
- s.addUB((ap && a != expr::IntMin(bits)) || b != expr::mkInt(-1, bits));
+ s.addUB((ap && a != expr::IntSMin(bits)) || b != expr::mkInt(-1, bits));
}
StateValue BinOp::toSMT(State &s) const {
@@ -177,6 +185,22 @@ StateValue BinOp::toSMT(State &s) const {
not_poison &= a.lshr_exact(b);
break;
}
+ case SAdd_Sat:
+ val = a.sadd_sat(b);
+ break;
+
+ case UAdd_Sat:
+ val = a.uadd_sat(b);
+ break;
+
+ case SSub_Sat:
+ val = a.ssub_sat(b);
+ break;
+
+ case USub_Sat:
+ val = a.usub_sat(b);
+ break;
+
case And:
val = a & b;
break;

MODIFY
ir/instr.h
ir/instr.h
@@ -24,6 +24,7 @@ public:
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,
And, Or, Xor };
enum Flags { None = 0, NSW = 1, NUW = 2, NSWNUW = 3, Exact = 4 };

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -171,7 +171,7 @@ expr expr::mkBoolVar(const char *name) {
return ::mkVar(name, Z3_mk_bool_sort(ctx()));
}
-expr expr::IntMin(unsigned bits) {
+expr expr::IntSMin(unsigned bits) {
assert(bits > 0);
static_assert(sizeof(unsigned long long) == 8);
if (bits <= 64)
@@ -179,7 +179,7 @@ expr expr::IntMin(unsigned bits) {
return mkUInt(1, bits) << mkUInt(bits - 1, bits);
}
-expr expr::IntMax(unsigned bits) {
+expr expr::IntSMax(unsigned bits) {
assert(bits > 0);
static_assert(sizeof(unsigned long long) == 8);
if (bits <= 64)
@@ -187,6 +187,10 @@ expr expr::IntMax(unsigned bits) {
return mkInt(-1, bits).lshr(mkUInt(1, bits));
}
+expr expr::IntUMax(unsigned bits) {
+ return mkInt(-1, bits);
+}
+
bool expr::eq(const expr &rhs) const {
C(rhs);
return ast() == rhs();
@@ -239,15 +243,15 @@ unsigned expr::bits() const {
bool expr::isUInt(uint64_t &n) const {
C();
- return Z3_get_numeral_uint64(ctx(), ast(), &n) == Z3_TRUE;
+ return bits() <= 64 && Z3_get_numeral_uint64(ctx(), ast(), &n);
}
bool expr::isInt(int64_t &n) const {
C();
- if (Z3_get_numeral_int64(ctx(), ast(), &n) == Z3_FALSE)
+ auto bw = bits();
+ if (bw > 64 || !Z3_get_numeral_int64(ctx(), ast(), &n))
return false;
- auto bw = bits();
if (bw < 64)
n = (int64_t)((uint64_t)n << (64 - bw)) >> (64 - bw);
return true;
@@ -393,6 +397,24 @@ expr expr::urem(const expr &rhs) const {
return Z3_mk_bvurem(ctx(), ast(), rhs());
}
+expr expr::sadd_sat(const expr &rhs) const {
+ return mkIf(add_no_soverflow(rhs),
+ *this + rhs,
+ IntSMax(bits()));
+}
+
+expr expr::uadd_sat(const expr &rhs) const {
+ return mkIf(add_no_uoverflow(rhs),
+ *this + rhs,
+ IntUMax(bits()));
+}
+
+expr expr::ssub_sat(const expr &rhs) const {
+}
+
+expr expr::usub_sat(const expr &rhs) const {
+}
+
expr expr::add_no_soverflow(const expr &rhs) const {
return sext(1) + rhs.sext(1) == (*this + rhs).sext(1);
}

MODIFY
smt/expr.h
smt/expr.h
@@ -73,8 +73,9 @@ public:
static expr mkVar(const char *name, unsigned bits);
static expr mkBoolVar(const char *name);
- static expr IntMin(unsigned bits);
- static expr IntMax(unsigned bits);
+ static expr IntSMin(unsigned bits);
+ static expr IntSMax(unsigned bits);
+ static expr IntUMax(unsigned bits);
// structural equivalence
bool eq(const expr &rhs) const;
@@ -104,6 +105,12 @@ public:
expr srem(const expr &rhs) const;
expr urem(const expr &rhs) const;
+ // saturating arithmetic
+ expr sadd_sat(const expr &rhs) const;
+ expr uadd_sat(const expr &rhs) const;
+ expr ssub_sat(const expr &rhs) const;
+ expr usub_sat(const expr &rhs) const;
+
expr add_no_soverflow(const expr &rhs) const;
expr add_no_uoverflow(const expr &rhs) const;
expr sub_no_soverflow(const expr &rhs) const;

ADD
tests/unit/saturating.opt
+Name: add max
+%r = uadd_sat %x, -1
+ =>
+%r = -1
+
+Name: uadd undef
+%r = uadd_sat %x, undef
+ =>
+%r = %x
+
+Name: sadd undef
+%r = sadd_sat %x, undef
+ =>
+%r = %x
+
+Name: sadd 0
+%r = sadd_sat %x, 0
+ =>
+%r = %x
+
+Name: uadd combine
+%a = uadd_sat i3 %x, %val2
+%r = uadd_sat %a, %val
+ =>
+%a = uadd_sat %x, %val2
+%b = uadd_sat %val, %val2
+%r = uadd_sat %x, %b

MODIFY
tools/alive_lexer.h
tools/alive_lexer.h
@@ -27,7 +27,7 @@ token yylex();
extern yylval_t yylval;
extern unsigned yylineno;
-extern const char *token_name[];
+extern const char *const token_name[];
struct LexException {
std::string str;

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -21,7 +21,7 @@ using namespace std;
static const YYCTYPE *YYCURSOR;
static const YYCTYPE *YYLIMIT;
static const YYCTYPE *YYTEXT;
-//static const YYCTYPE *YYMARKER;
+static const YYCTYPE *YYMARKER;
static const YYCTYPE *tag1, *yyt1;
#if 0
@@ -40,7 +40,7 @@ namespace tools {
unsigned yylineno;
yylval_t yylval;
-const char *token_name[] = {
+const char *const token_name[] = {
#define TOKEN(x) #x,
#include "tools/tokens.h"
#undef TOKEN
@@ -161,6 +161,10 @@ re2c:yyfill:check = 0;
"shl" { return SHL; }
"ashr" { return ASHR; }
"lshr" { return LSHR; }
+"sadd_sat" { return SADD_SAT; }
+"uadd_sat" { return UADD_SAT; }
+"ssub_sat" { return SSUB_SAT; }
+"usub_sat" { return USUB_SAT; }
"and" { return AND; }
"or" { return OR; }
"xor" { return XOR; }

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -347,6 +347,10 @@ static BinOp::Flags parse_binop_flags(token op_token) {
return parse_exact();
case SREM:
case UREM:
+ case UADD_SAT:
+ case SADD_SAT:
+ case USUB_SAT:
+ case SSUB_SAT:
case AND:
case OR:
case XOR:
@@ -378,6 +382,10 @@ static unique_ptr<Instr> parse_binop(string_view name, token op_token) {
case AND: op = BinOp::And; break;
case OR: op = BinOp::Or; break;
case XOR: op = BinOp::Xor; break;
+ case SADD_SAT: op = BinOp::SAdd_Sat; break;
+ case UADD_SAT: op = BinOp::UAdd_Sat; break;
+ case SSUB_SAT: op = BinOp::SSub_Sat; break;
+ case USUB_SAT: op = BinOp::USub_Sat; break;
default:
UNREACHABLE();
}
@@ -470,6 +478,10 @@ static unique_ptr<Instr> parse_instr(string_view name) {
case SHL:
case ASHR:
case LSHR:
+ case SADD_SAT:
+ case UADD_SAT:
+ case SSUB_SAT:
+ case USUB_SAT:
case AND:
case OR:
case XOR:

MODIFY
tools/tokens.h
tools/tokens.h
@@ -40,6 +40,7 @@ TOKEN(PRE)
TOKEN(REGISTER)
TOKEN(RETURN)
TOKEN(RPAREN)
+TOKEN(SADD_SAT)
TOKEN(SDIV)
TOKEN(SELECT)
TOKEN(SEXT)
@@ -49,11 +50,13 @@ TOKEN(SHL)
TOKEN(SLE)
TOKEN(SLT)
TOKEN(SREM)
+TOKEN(SSUB_SAT)
TOKEN(STAR)
TOKEN(SUB)
TOKEN(TO)
TOKEN(TRUE)
TOKEN(TRUNC)
+TOKEN(UADD_SAT)
TOKEN(UDIV)
TOKEN(UGE)
TOKEN(UGT)
@@ -62,5 +65,6 @@ TOKEN(ULT)
TOKEN(UNDEF)
TOKEN(UNREACH)
TOKEN(UREM)
+TOKEN(USUB_SAT)
TOKEN(XOR)
TOKEN(ZEXT)

add support for saturating Add & Sub