add printing of memory refinement counterexamples
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -11,33 +11,13 @@ using namespace smt;
using namespace std;
using namespace util;
-namespace {
-
-// A data structure that represents a byte.
-// A byte is either a pointer byte or a non-pointer byte.
-// Pointer byte's representation:
-// +-+-------+-----------+------------------+----------------+-------------+
-// |1|padding|non-poison?| ptr offset | block id | byte offset |
-// | | |(1 bit) | (bits_for_offset)| (bits_for_bid) | (3 bits) |
-// +-+-------+-----------+------------------+----------------+-------------+
-// Non-pointer byte's representation:
-// +-+--------------------------+--------------------+---------------------+
-// |0| padding(zero) | non-poison bits? | data |
-// | | | (bits_byte) | (bits_byte) |
-// +-+--------------------------+--------------------+---------------------+
-class Byte {
- const Memory &m;
- expr p;
-
-public:
- // Creates a byte with its raw representation.
- Byte(const Memory &m, expr &&byterepr) : m(m), p(move(byterepr)) {
+namespace IR {
+
+Byte::Byte(const Memory &m, expr &&byterepr) : m(m), p(move(byterepr)) {
assert(!p.isValid() || p.bits() == m.bitsByte());
}
- // Creates a pointer byte that represents i'th byte of p.
- // non_poison should be an one-bit vector or boolean.
- Byte(const Pointer &ptr, unsigned i, const expr &non_poison)
+Byte::Byte(const Pointer &ptr, unsigned i, const expr &non_poison)
: m(ptr.getMemory()) {
// TODO: support pointers larger than 64 bits.
assert(bits_size_t <= 64 && bits_size_t % 8 == 0);
@@ -52,9 +32,7 @@ public:
assert(!p.isValid() || p.bits() == m.bitsByte());
}
- // Creates a non-pointer byte that has data and non_poison.
- // data and non_poison should have bits_byte bits.
- Byte(const Memory &m, const expr &data, const expr &non_poison) : m(m) {
+Byte::Byte(const Memory &m, const expr &data, const expr &non_poison) : m(m) {
assert(!data.isValid() || data.bits() == bits_byte);
assert(!non_poison.isValid() || non_poison.bits() == bits_byte);
@@ -66,42 +44,69 @@ public:
assert(!p.isValid() || p.bits() == m.bitsByte());
}
- expr is_ptr() const {
+expr Byte::is_ptr() const {
auto bit = p.bits() - 1;
return p.extract(bit, bit) == 1;
}
- // Assuming that this is a pointer byte
- expr ptr_nonpoison() const {
+expr Byte::ptr_nonpoison() const {
auto bit = p.bits() - 2;
return p.extract(bit, bit) == 1;
}
- expr ptr_value() const {
+expr Byte::ptr_value() const {
return p.extract(bits_for_offset + bits_for_bid + 2, 3);
}
- expr ptr_byteoffset() const { return p.extract(2, 0); }
- // Assuming that this is a non-pointer byte
- expr nonptr_nonpoison() const { return p.extract(bits_byte * 2 - 1,
- bits_byte); };
- expr nonptr_value() const { return p.extract(bits_byte - 1, 0); }
+expr Byte::ptr_byteoffset() const {
+ return p.extract(2, 0);
+}
- const expr& operator()() const { return p; }
+expr Byte::nonptr_nonpoison() const {
+ return p.extract(bits_byte * 2 - 1, bits_byte);
+}
- expr operator==(const Byte &rhs) const {
- return p == rhs.p;
+expr Byte::nonptr_value() const {
+ return p.extract(bits_byte - 1, 0);
}
- static Byte mkPoisonByte(const Memory &m) {
+Byte Byte::mkPoisonByte(const Memory &m) {
IntType ty("", bits_byte);
auto v = ty.toBV(ty.getDummyValue(false));
return { m, v.value, v.non_poison };
}
-};
+ostream& operator<<(ostream &os, const Byte &byte) {
+ if (byte.is_ptr().isTrue()) {
+ if (byte.ptr_nonpoison().isTrue()) {
+ os << Pointer(byte.m, byte.ptr_value())
+ << ", byte offset=";
+ byte.ptr_byteoffset().printSigned(os);
+ } else {
+ os << "poison";
+ }
+ } else {
+ auto np = byte.nonptr_nonpoison();
+ auto val = byte.nonptr_value();
+ if (np.isAllOnes()) {
+ os << "poison";
+ } else if (np.isZero()) {
+ val.printHexadecimal(os);
+ } else {
+ os << "#b";
+ for (unsigned i = 0; i < bits_byte; ++i) {
+ unsigned idx = bits_byte - i - 1;
+ auto is_poison = (np.extract(idx, idx) == 1).isTrue();
+ auto v = (val.extract(idx, idx) == 1).isTrue();
+ os << (is_poison ? 'p' : (v ? '1' : '0'));
+ }
+ }
+ }
+ return os;
+}
+}
-vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
+static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
const Memory &mem) {
vector<Byte> bytes;
if (fromType.isPtrType()) {
@@ -127,7 +132,7 @@ vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
return bytes;
}
-StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
+static StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
assert(!bytes.empty());
if (toType.isPtrType()) {
@@ -171,7 +176,6 @@ StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
return toType.fromBV(val.trunc(bitsize));
}
}
-}
static bool observes_addresses() {
return IR::has_ptr2int || IR::has_int2ptr;
@@ -493,7 +497,7 @@ expr Pointer::isNull() const {
expr Pointer::isNonZero() const {
if (observes_addresses())
return get_address() != 0;
- return get_bid() != 0 || get_offset() != 0;
+ return !isNull();
}
ostream& operator<<(ostream &os, const Pointer &p) {
@@ -878,6 +882,10 @@ StateValue Memory::load(const expr &p, const Type &type, unsigned align,
}
}
+Byte Memory::load(const Pointer &p) {
+ return { *this, ::load(p, local_block_val, non_local_block_val) };
+}
+
void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
unsigned align) {
assert(!memory_unused());
@@ -946,10 +954,11 @@ expr Memory::int2ptr(const expr &val) {
return {};
}
-expr Memory::refined(const Memory &other) const {
- if (memory_unused())
- return true;
+pair<expr,Pointer> Memory::refined(const Memory &other) const {
+ if (num_nonlocals <= 1)
+ return { true, Pointer(*this, expr()) };
+ assert(!memory_unused());
Pointer ptr(*this, "#idx");
expr ptr_bid = ptr.get_bid();
expr offset = ptr.get_offset();
@@ -961,7 +970,8 @@ expr Memory::refined(const Memory &other) const {
Pointer q(other, p());
ret &= (ptr_bid == bid_expr).implies(p.block_refined(q));
}
- return ptr_bid.ult(num_nonlocals).implies(ret);
+ return { (ptr_bid != 0 && ptr_bid.ult(num_nonlocals)).implies(ret),
+ move(ptr) };
}
Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {

MODIFY
ir/memory.h
ir/memory.h
#include <string>
#include <utility>
-namespace smt { class FunctionExpr; }
-
namespace IR {
class Memory;
+class Pointer;
class State;
+
+// A data structure that represents a byte.
+// A byte is either a pointer byte or a non-pointer byte.
+// Pointer byte's representation:
+// +-+-------+-----------+------------------+----------------+-------------+
+// |1|padding|non-poison?| ptr offset | block id | byte offset |
+// | | |(1 bit) | (bits_for_offset)| (bits_for_bid) | (3 bits) |
+// +-+-------+-----------+------------------+----------------+-------------+
+// Non-pointer byte's representation:
+// +-+--------------------------+--------------------+---------------------+
+// |0| padding(zero) | non-poison bits? | data |
+// | | | (bits_byte) | (bits_byte) |
+// +-+--------------------------+--------------------+---------------------+
+class Byte {
+ const Memory &m;
+ smt::expr p;
+
+public:
+ // Creates a byte with its raw representation.
+ Byte(const Memory &m, smt::expr &&byterepr);
+
+ // Creates a pointer byte that represents i'th byte of p.
+ // non_poison should be an one-bit vector or boolean.
+ Byte(const Pointer &ptr, unsigned i, const smt::expr &non_poison);
+
+ // Creates a non-pointer byte that has data and non_poison.
+ // data and non_poison should have bits_byte bits.
+ Byte(const Memory &m, const smt::expr &data, const smt::expr &non_poison);
+
+ smt::expr is_ptr() const;
+ smt::expr ptr_nonpoison() const;
+ smt::expr ptr_value() const;
+ smt::expr ptr_byteoffset() const;
+ smt::expr nonptr_nonpoison() const;
+ smt::expr nonptr_value() const;
+
+ const smt::expr& operator()() const { return p; }
+
+ smt::expr operator==(const Byte &rhs) const {
+ return p == rhs.p;
+ }
+
+ static Byte mkPoisonByte(const Memory &m);
+ friend std::ostream& operator<<(std::ostream &os, const Byte &byte);
+};
+
+
class Pointer {
const Memory &m;
@@ -173,6 +219,9 @@ public:
StateValue load(const smt::expr &ptr, const Type &type, unsigned align,
bool deref_check = true);
+ // raw load
+ Byte load(const Pointer &p);
+
void memset(const smt::expr &ptr, const StateValue &val,
const smt::expr &bytesize, unsigned align);
void memcpy(const smt::expr &dst, const smt::expr &src,
@@ -182,7 +231,7 @@ public:
smt::expr ptr2int(const smt::expr &ptr);
smt::expr int2ptr(const smt::expr &val);
- smt::expr refined(const Memory &other) const;
+ std::pair<smt::expr,Pointer> refined(const Memory &other) const;
static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -101,11 +101,12 @@ static void print_varval(ostream &os, State &st, const Model &m,
}
+using print_var_val_ty = function<void(ostream&, const Model&)>;
+
static void error(Errors &errs, State &src_state, State &tgt_state,
- const Result &r, bool print_var, const Value *var,
- const Type &type,
- const StateValue &src, const StateValue &tgt,
- const char *msg, bool check_each_var) {
+ const Result &r, const Value *var,
+ const char *msg, bool check_each_var,
+ print_var_val_ty print_var_val) {
if (r.isInvalid()) {
errs.add("Invalid expr", false);
@@ -175,13 +176,7 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
}
}
- if (print_var) {
- s << "Source value: ";
- print_varval(s, src_state, m, var, type, src);
- s << "\nTarget value: ";
- print_varval(s, tgt_state, m, var, type, tgt);
- }
-
+ print_var_val(s, m);
errs.add(s.str(), true);
}
@@ -254,9 +249,15 @@ static void check_refinement(Errors &errs, Transform &t,
auto qvars = src_state.getQuantVars();
qvars.insert(ap.second.begin(), ap.second.end());
- auto err = [&](const Result &r, bool print_var, const char *msg) {
- error(errs, src_state, tgt_state, r, print_var, var, type, a, b, msg,
- check_each_var);
+ auto err = [&](const Result &r, print_var_val_ty print, const char *msg) {
+ error(errs, src_state, tgt_state, r, var, msg, check_each_var, print);
+ };
+
+ auto print_value = [&](ostream &s, const Model &m) {
+ s << "Source value: ";
+ print_varval(s, src_state, m, var, type, a);
+ s << "\nTarget value: ";
+ print_varval(s, tgt_state, m, var, type, b);
};
AndExpr axioms = src_state.getAxioms();
@@ -291,12 +292,15 @@ static void check_refinement(Errors &errs, Transform &t,
expr pre_src = pre_src_and();
expr pre_tgt = pre_tgt_and();
- auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
- expr memory_cnstr
- = src_state.returnMemory().refined(tgt_state.returnMemory());
expr axioms_expr = axioms();
expr dom = dom_a && dom_b;
+ auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
+
+ auto src_mem = src_state.returnMemory();
+ auto tgt_mem = tgt_state.returnMemory();
+ auto [memory_cnstr, ptr_refinement] = src_mem.refined(tgt_mem);
+
if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) {
errs.add("Precondition is always false", false);
return;
@@ -316,23 +320,30 @@ static void check_refinement(Errors &errs, Transform &t,
preprocess(t, qvars, uvars, pre_tgt && pre_src.implies(refines));
};
+ auto print_ptr_load = [&](ostream &s, const Model &m) {
+ Pointer p(src_mem, m[ptr_refinement()]);
+ s << "\nMismatch in " << p
+ << "\nSource value: " << Byte(src_mem, m[src_mem.load(p)()])
+ << "\nTarget value: " << Byte(tgt_mem, m[tgt_mem.load(p)()]);
+ };
+
Solver::check({
{ mk_fml(dom_a.notImplies(dom_b)),
[&](const Result &r) {
- err(r, false, "Source is more defined than target");
+ err(r, [](ostream&, const Model&){},
+ "Source is more defined than target");
}},
{ mk_fml(dom && !poison_cnstr),
[&](const Result &r) {
- err(r, true, "Target is more poisonous than source");
+ err(r, print_value, "Target is more poisonous than source");
}},
{ mk_fml(dom && !value_cnstr),
[&](const Result &r) {
- err(r, true, "Value mismatch");
+ err(r, print_value, "Value mismatch");
}},
{ mk_fml(dom && !memory_cnstr),
- // FIXME: counterxample is broken (eg should print memory id that differs)
[&](const Result &r) {
- err(r, true, "Mismatch in memory");
+ err(r, print_ptr_load, "Mismatch in memory");
}}
});
}

add printing of memory refinement counterexamples