fix printing of counterexamples with bw > 64 bits
fixes bug
MODIFY
smt/expr.cpp
smt/expr.cpp
#include "smt/ctx.h"
#include "smt/expr.h"
+#include "util/compiler.h"
+#include <algorithm>
#include <cassert>
#include <memory>
+#include <string>
+#include <iostream>
#include <z3.h>
#define DEBUG_Z3_RC 0
@@ -240,6 +244,10 @@ bool expr::isSMax() const {
return isUInt(n) && n == ((uint64_t)INT64_MAX >> (64 - bits()));
}
+bool expr::isSigned() const {
+ return (extract(0, 0) == mkUInt(1, 1)).simplify().isTrue();
+}
+
unsigned expr::bits() const {
C();
return Z3_get_bv_sort_size(ctx(), sort());
@@ -247,7 +255,7 @@ unsigned expr::bits() const {
bool expr::isUInt(uint64_t &n) const {
C();
- return bits() <= 64 && Z3_get_numeral_uint64(ctx(), ast(), &n);
+ return Z3_get_numeral_uint64(ctx(), ast(), &n);
}
bool expr::isInt(int64_t &n) const {
@@ -871,6 +879,39 @@ expr expr::subst(const expr &from, const expr &to) const {
return Z3_substitute(ctx(), ast(), 1, &f, &t);
}
+void expr::printUnsigned(std::ostream &os) const {
+ expr zero = mkUInt(0, sort());
+ expr ten = mkUInt(10, sort());
+ expr n = *this;
+
+ string str;
+ uint64_t d;
+
+ do {
+ expr digit = n.urem(ten).simplify();
+ ENSURE(digit.isUInt(d));
+ str.push_back('0' + d);
+ n = n.udiv(ten).simplify();
+ } while (!n.eq(zero));
+
+ reverse(str.begin(), str.end());
+ os << str;
+}
+
+void expr::printSigned(std::ostream &os) const {
+ if (isSigned()) {
+ os << '-';
+ (~*this + mkUInt(1, sort())).simplify().printUnsigned(os);
+ } else {
+ printUnsigned(os);
+ }
+}
+
+void expr::printHexadecimal(std::ostream &os) const {
+ auto rem = bits() % 4;
+ os << (rem == 0 ? *this : zext(4 - rem)).simplify();
+}
+
ostream& operator<<(ostream &os, const expr &e) {
return os << (e.isValid() ? Z3_ast_to_string(ctx(), e()) : "(null)");
}

MODIFY
smt/expr.h
smt/expr.h
@@ -91,6 +91,7 @@ public:
bool isAllOnes() const;
bool isSMin() const;
bool isSMax() const;
+ bool isSigned() const;
unsigned bits() const;
bool isUInt(uint64_t &n) const;
@@ -187,6 +188,9 @@ public:
expr subst(const std::vector<std::pair<expr, expr>> &repls) const;
expr subst(const expr &from, const expr &to) const;
+ void printUnsigned(std::ostream &os) const;
+ void printSigned(std::ostream &os) const;
+ void printHexadecimal(std::ostream &os) const;
friend std::ostream &operator<<(std::ostream &os, const expr &e);
// for container use only

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -37,13 +37,12 @@ static void print_varval(ostream &s, const Model &m, const Value *var,
}
expr e = m[val.value];
- uint64_t n;
- ENSURE(e.isUInt(n));
- auto bw = e.bits();
- s << "0x" << hex << n << dec;
- s << " (" << n;
- if (n != 0 && num_leading_zeros(n) == (64 - bw)) {
- s << ", " << ((int64_t)(n << (64 - bw)) >> (64 - bw));
+ e.printHexadecimal(s);
+ s << " (";
+ e.printUnsigned(s);
+ if (e.bits() > 1 && e.isSigned()) {
+ s << ", ";
+ e.printSigned(s);
}
s << ')';
}

fix printing of counterexamples with bw > 64 bits
fixes bug #37