memory: specialize byte to have just 1 poison if there are no sub-byte accesses
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -26,5 +26,6 @@ bool has_dead_allocas;
bool does_int_mem_access;
bool does_ptr_mem_access;
bool does_ptr_store;
+bool does_sub_byte_access;
}

MODIFY
ir/globals.h
ir/globals.h
@@ -56,4 +56,7 @@ extern bool does_int_mem_access;
extern bool does_ptr_mem_access;
extern bool does_ptr_store;
+/// Whether the programs do memory accesses of less than bits_byte
+extern bool does_sub_byte_access;
+
}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -863,6 +863,10 @@ StateValue ConversionOp::toSMT(State &s) const {
auto retty = getType().getAsAggregateType();
auto elems = retty->numElementsConst();
+ // NOP: ptr vect -> ptr vect
+ if (op == BitCast && retty->getChild(0).isPtrType())
+ return v;
+
// bitcast vect elems size may vary, so create a new data type whose
// element size is aligned with the output vector elem size
IntType elem_ty("int", retty->bits() / elems);

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -15,6 +15,10 @@ using namespace util;
static unsigned ptr_next_idx = 0;
+static unsigned bits_int_poison() {
+ return does_sub_byte_access ? bits_byte : 1;
+}
+
static expr concat_if(const expr &ifvalid, expr &&e) {
return ifvalid.isValid() ? ifvalid.concat(e) : move(e);
}
@@ -58,14 +62,14 @@ Byte::Byte(const Pointer &ptr, unsigned i, const expr &non_poison)
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);
+ assert(!non_poison.isValid() || non_poison.bits() == bits_int_poison());
if (!does_int_mem_access) {
p = expr::mkUInt(0, bitsByte());
return;
}
- unsigned padding = bitsByte() - 2 * bits_byte;
+ unsigned padding = bitsByte() - bits_byte - bits_int_poison();
p = non_poison.concat(data);
if (padding)
p = expr::mkUInt(0, padding).concat(p);
@@ -106,8 +110,8 @@ expr Byte::ptr_byteoffset() const {
expr Byte::nonptr_nonpoison() const {
if (!does_int_mem_access)
- return expr::mkUInt(0, bits_byte);
- return p.extract(bits_byte * 2 - 1, bits_byte);
+ return expr::mkUInt(0, bits_int_poison());
+ return p.extract(bits_byte + bits_int_poison() - 1, bits_byte);
}
expr Byte::nonptr_value() const {
@@ -132,7 +136,7 @@ expr Byte::is_zero() const {
unsigned Byte::bitsByte() {
bool is_ptr_bit = does_int_mem_access && does_ptr_mem_access;
unsigned ptr_bits = does_ptr_mem_access * (1 + Pointer::total_bits() + 3);
- unsigned int_bits = does_int_mem_access * (2 * bits_byte);
+ unsigned int_bits = does_int_mem_access * (bits_byte + bits_int_poison());
// allow at least 1 bit if there's no memory access
return max(1u, is_ptr_bit + max(ptr_bits, int_bits));
}
@@ -153,7 +157,7 @@ Byte Byte::mkNonPtrByte(const Memory &m, const expr &val) {
if (!does_int_mem_access)
return { m, expr::mkUInt(0, bitsByte()) };
- unsigned padding = bitsByte() - 2 * bits_byte;
+ unsigned padding = bitsByte() - bits_byte - bits_int_poison();
expr byte = padding ? expr::mkUInt(0, padding).concat(val) : val;
return { m, move(byte) };
}
@@ -178,8 +182,8 @@ ostream& operator<<(ostream &os, const Byte &byte) {
val.printHexadecimal(os);
} else {
os << "#b";
- for (unsigned i = 0; i < bits_byte; ++i) {
- unsigned idx = bits_byte - i - 1;
+ for (unsigned i = 0; i < bits_int_poison(); ++i) {
+ unsigned idx = bits_int_poison() - 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'));
@@ -205,11 +209,11 @@ static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
unsigned bytesize = divide_up(bitsize, bits_byte);
bvval = bvval.zext(bytesize * bits_byte - bitsize);
+ unsigned np_mul = does_sub_byte_access ? bits_byte : 1;
for (unsigned i = 0; i < bytesize; ++i) {
expr data = bvval.value.extract((i + 1) * bits_byte - 1, i * bits_byte);
- expr np = bvval.non_poison.extract((i + 1) * bits_byte - 1,
- i * bits_byte);
+ expr np = bvval.non_poison.extract((i + 1) * np_mul - 1, i * np_mul);
bytes.emplace_back(mem, data, np);
}
}
@@ -659,8 +663,11 @@ expr Pointer::block_val_refined(const Pointer &other) const {
// refinement if offset had non-ptr value
expr np1 = val.nonptr_nonpoison();
- expr int_cnstr = (val2.nonptr_nonpoison() | np1) == np1 &&
- (val.nonptr_value() | np1) == (val2.nonptr_value() | np1);
+ expr int_cnstr = does_sub_byte_access
+ ? (val2.nonptr_nonpoison() | np1) == np1 &&
+ (val.nonptr_value() | np1) == (val2.nonptr_value() | np1)
+ : val2.nonptr_nonpoison() == 0 &&
+ val.nonptr_value() == val2.nonptr_value();
// fast path: if we didn't do any ptr store, then all ptrs in memory were
// already there and don't need checking

MODIFY
ir/state_value.cpp
ir/state_value.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/state_value.h"
+#include "ir/globals.h"
#include "util/compiler.h"
#include <tuple>
@@ -18,18 +19,21 @@ StateValue StateValue::mkIf(const expr &cond, const StateValue &then,
StateValue StateValue::zext(unsigned amount) const {
return { value.zext(amount),
- non_poison.isBool() ? expr(non_poison) : non_poison.zext(amount) };
+ (!does_sub_byte_access || non_poison.isBool())
+ ? expr(non_poison) : non_poison.zext(amount) };
}
StateValue StateValue::trunc(unsigned amount) const {
return { value.trunc(amount),
- non_poison.isBool() ? expr(non_poison) : non_poison.trunc(amount) };
+ (!does_sub_byte_access || non_poison.isBool())
+ ? expr(non_poison) : non_poison.trunc(amount) };
}
StateValue StateValue::zextOrTrunc(unsigned tobw) const {
return
{ value.zextOrTrunc(tobw),
- non_poison.isBool() ? expr(non_poison) : non_poison.zextOrTrunc(tobw) };
+ (!does_sub_byte_access || non_poison.isBool())
+ ? expr(non_poison) : non_poison.zextOrTrunc(tobw) };
}
StateValue StateValue::concat(const StateValue &other) const {

MODIFY
ir/type.cpp
ir/type.cpp
#include <sstream>
using namespace smt;
+using namespace util;
using namespace std;
static constexpr unsigned var_type_bits = 3;
@@ -22,6 +23,11 @@ namespace IR {
VoidType Type::voidTy;
+unsigned Type::np_bits() const {
+ auto bw = bits();
+ return does_sub_byte_access ? bw : (unsigned)divide_up(bw, bits_byte);
+}
+
expr Type::var(const char *var, unsigned bits) const {
auto str = name + '_' + var;
return expr::mkVar(str.c_str(), bits);
@@ -205,7 +211,7 @@ expr Type::toBV(expr e) const {
StateValue Type::toBV(StateValue v) const {
expr val = toBV(move(v.value));
- auto bw = val.bits();
+ auto bw = np_bits();
return { move(val),
expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
}
@@ -224,7 +230,7 @@ expr Type::toInt(State &s, expr v) const {
StateValue Type::toInt(State &s, StateValue v) const {
expr val = toInt(s, move(v.value));
- auto bw = val.bits();
+ auto bw = np_bits();
return { move(val),
expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
}
@@ -238,11 +244,8 @@ StateValue Type::fromInt(StateValue v) const {
}
expr Type::combine_poison(const expr &boolean, const expr &orig) const {
- if (orig.isBool())
- return boolean && orig;
-
- auto bw = orig.bits();
- return expr::mkIf(boolean, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) | orig;
+ return
+ expr::mkIf(boolean, expr::mkInt(0, orig), expr::mkInt(-1, orig)) | orig;
}
pair<expr, vector<expr>> Type::mkUndefInput(State &s, unsigned attrs) const {
@@ -584,6 +587,10 @@ unsigned PtrType::bits() const {
return Pointer::total_bits();
}
+unsigned PtrType::np_bits() const {
+ return 1;
+}
+
StateValue PtrType::getDummyValue(bool non_poison) const {
return { expr::mkUInt(0, bits()), non_poison };
}
@@ -713,19 +720,21 @@ StateValue AggregateType::aggregateVals(const vector<StateValue> &vals) const {
}
StateValue AggregateType::extract(const StateValue &val, unsigned index) const {
- if (!val.isValid())
- return {};
-
- unsigned total_till_now = 0;
+ unsigned total_value = 0, total_np = 0;
for (unsigned i = 0; i < index; ++i) {
- total_till_now += children[i]->bits();
+ total_value += children[i]->bits();
+ total_np += children[i]->np_bits();
}
- unsigned high = val.bits() - total_till_now;
- unsigned h = high - 1;
- unsigned l = high - children[index]->bits();
+ unsigned high_val = bits() - total_value;
+ unsigned h_val = high_val - 1;
+ unsigned l_val = high_val - children[index]->bits();
+
+ unsigned high_np = np_bits() - total_np;
+ unsigned h_np = high_np - 1;
+ unsigned l_np = high_np - children[index]->np_bits();
- return children[index]->fromBV({ val.value.extract(h, l),
- val.non_poison.extract(h, l) });
+ return children[index]->fromBV({ val.value.extract(h_val, l_val),
+ val.non_poison.extract(h_np, l_np) });
}
unsigned AggregateType::bits() const {
@@ -736,6 +745,14 @@ unsigned AggregateType::bits() const {
return bw;
}
+unsigned AggregateType::np_bits() const {
+ unsigned bw = 0;
+ for (unsigned i = 0; i < elements; ++i) {
+ bw += children[i]->np_bits();
+ }
+ return bw;
+}
+
StateValue AggregateType::getDummyValue(bool non_poison) const {
if (elements == 0)
return { expr::mkUInt(0, 1), expr::mkUInt(non_poison, 1) };
@@ -948,19 +965,21 @@ VectorType::VectorType(string &&name, unsigned elements, Type &elementTy)
StateValue VectorType::extract(const StateValue &vector,
const expr &index) const {
- if (!vector.isValid())
- return {};
-
auto &elementTy = *children[0];
unsigned bw_elem = elementTy.bits();
- unsigned bw_val = vector.bits();
- expr idx = index.zextOrTrunc(bw_val) * expr::mkUInt(bw_elem, bw_val);
+ unsigned bw_val = bw_elem * elements;
+ expr idx_v = index.zextOrTrunc(bw_val) * expr::mkUInt(bw_elem, bw_val);
+ unsigned h_val = elements * bw_elem - 1;
+ unsigned l_val = (elements - 1) * bw_elem;
- unsigned h = elements * bw_elem - 1;
- unsigned l = (elements - 1) * bw_elem;
+ unsigned bw_np_elem = elementTy.np_bits();
+ unsigned bw_np = bw_np_elem * elements;
+ expr idx_np = index.zextOrTrunc(bw_np) * expr::mkUInt(bw_np_elem, bw_np);
+ unsigned h_np = elements * bw_np_elem - 1;
+ unsigned l_np = (elements - 1) * bw_np_elem;
- return elementTy.fromBV({ (vector.value << idx).extract(h, l),
- (vector.non_poison << idx).extract(h, l) });
+ return elementTy.fromBV({(vector.value << idx_v).extract(h_val, l_val),
+ (vector.non_poison << idx_np).extract(h_np, l_np)});
}
StateValue VectorType::update(const StateValue &vector,
@@ -973,17 +992,21 @@ StateValue VectorType::update(const StateValue &vector,
return val_bv;
unsigned bw_elem = elementTy.bits();
- unsigned bw_val = bits();
-
- expr idx = index.zextOrTrunc(bw_val) * expr::mkUInt(bw_elem, bw_val);
- expr fill = expr::mkUInt(0, bw_val - bw_elem);
- expr mask = ~expr::mkInt(-1, bw_elem).concat(fill).lshr(idx);
+ unsigned bw_val = bw_elem * elements;
+ expr idx_v = index.zextOrTrunc(bw_val) * expr::mkUInt(bw_elem, bw_val);
+ expr fill_v = expr::mkUInt(0, bw_val - bw_elem);
+ expr mask_v = ~expr::mkInt(-1, bw_elem).concat(fill_v).lshr(idx_v);
+ expr nv_shifted = val_bv.value.concat(fill_v).lshr(idx_v);
- expr nv_shifted = val_bv.value.concat(fill).lshr(idx);
- expr np_shifted = val_bv.non_poison.concat(fill).lshr(idx);
+ unsigned bw_np_elem = elementTy.np_bits();
+ unsigned bw_np = bw_np_elem * elements;
+ expr idx_np = index.zextOrTrunc(bw_np) * expr::mkUInt(bw_np_elem, bw_np);
+ expr fill_np = expr::mkUInt(0, bw_np - bw_np_elem);
+ expr mask_np = ~expr::mkInt(-1, bw_np_elem).concat(fill_np).lshr(idx_np);
+ expr np_shifted = val_bv.non_poison.concat(fill_np).lshr(idx_np);
- return fromBV({ (vector.value & mask) | nv_shifted,
- (vector.non_poison & mask) | np_shifted});
+ return fromBV({ (vector.value & mask_v) | nv_shifted,
+ (vector.non_poison & mask_np) | np_shifted});
}
expr VectorType::getTypeConstraints() const {
@@ -1106,6 +1129,10 @@ unsigned SymbolicType::bits() const {
DISPATCH(bits(), UNREACHABLE());
}
+unsigned SymbolicType::np_bits() const {
+ DISPATCH(np_bits(), UNREACHABLE());
+}
+
StateValue SymbolicType::getDummyValue(bool non_poison) const {
DISPATCH(getDummyValue(non_poison), UNREACHABLE());
}

MODIFY
ir/type.h
ir/type.h
@@ -42,6 +42,7 @@ protected:
public:
Type(std::string &&name) : name(std::move(name)) {}
virtual unsigned bits() const = 0;
+ virtual unsigned np_bits() const;
// to use when one needs the corresponding SMT type
virtual IR::StateValue getDummyValue(bool non_poison) const = 0;
@@ -224,6 +225,7 @@ public:
PtrType(unsigned addr_space);
unsigned bits() const override;
+ unsigned np_bits() const override;
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
@@ -270,6 +272,7 @@ public:
bool isPadding(unsigned i) const { return is_padding[i]; }
unsigned bits() const override;
+ unsigned np_bits() const override;
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
@@ -360,6 +363,7 @@ public:
SymbolicType(std::string &&name, unsigned type_mask);
unsigned bits() const override;
+ unsigned np_bits() const override;
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -533,6 +533,19 @@ static uint64_t max_gep(const Instr &inst) {
return 0;
}
+static bool has_sub_byte(const Type &t) {
+ if (auto agg = t.getAsAggregateType()) {
+ if (t.isVectorType())
+ return agg->getChild(0).bits() % 8;
+
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ if (has_sub_byte(agg->getChild(i)))
+ return true;
+ }
+ }
+ return false;
+}
+
static void calculateAndInitConstants(Transform &t) {
const auto &globals_tgt = t.tgt.getGlobalVars();
const auto &globals_src = t.src.getGlobalVars();
@@ -641,12 +654,14 @@ static void calculateAndInitConstants(Transform &t) {
uint64_t min_access_size = 8;
bool does_mem_access = false;
bool has_load = false;
+ does_sub_byte_access = false;
for (auto fn : { &t.src, &t.tgt }) {
for (auto BB : fn->getBBs()) {
for (auto &I : BB->instrs()) {
for (auto op : I.operands()) {
nullptr_is_used |= has_nullptr(op);
+ does_sub_byte_access |= has_sub_byte(op->getType());
}
if (auto conv = dynamic_cast<const ConversionOp*>(&I)) {
@@ -663,6 +678,8 @@ static void calculateAndInitConstants(Transform &t) {
has_load |= dynamic_cast<const Load*>(&I) != nullptr;
has_fncall |= dynamic_cast<const FnCall*>(&I) != nullptr;
+ does_sub_byte_access |= has_sub_byte(I.getType());
+
auto accsz = get_access_size(I);
if (accsz != NO_ACCESS) {
min_access_size = gcd(min_access_size, accsz);
@@ -759,6 +776,7 @@ static void calculateAndInitConstants(Transform &t) {
"does_ptr_store: " << does_ptr_store << "\n"
"does_ptr_mem_access: " << does_ptr_mem_access << "\n"
"does_int_mem_access: " << does_int_mem_access << "\n"
+ "does_sub_byte_access: " << does_sub_byte_access << "\n"
;
}

memory: specialize byte to have just 1 poison if there are no sub-byte accesses