fix fn argument checking of align, nonnull, and dereferenceable
MODIFY
ir/attrs.h
ir/attrs.h
@@ -18,8 +18,8 @@ public:
ParamAttrs(unsigned bits = None) : bits(bits) {}
uint64_t derefBytes; // Dereferenceable
- uint64_t blockSize; // exact block size for e.g. byval args
- uint64_t align = 1;
+ unsigned blockSize; // exact block size for e.g. byval args
+ unsigned align = 1;
bool has(Attribute a) const { return (bits & a) != 0; }
void set(Attribute a) { bits |= (unsigned)a; }
@@ -52,7 +52,7 @@ public:
void set(Attribute a) { bits |= (unsigned)a; }
uint64_t derefBytes; // Dereferenceable
- uint64_t align = 1;
+ unsigned align = 1;
// Returns true if returning poison or an aggregate having a poison is UB
bool poisonImpliesUB() const

MODIFY
ir/state.cpp
ir/state.cpp
@@ -22,12 +22,6 @@ State::CurrentDomain::operator bool() const {
return !path.isFalse() && UB;
}
-void State::CurrentDomain::reset() {
- path = true;
- UB.reset();
- undef_vars.clear();
-}
-
expr State::DomainPreds::operator()() const {
return path() && *UB();
}
@@ -522,8 +516,6 @@ bool State::startBB(const BasicBlock &bb) {
ENSURE(seen_bbs.emplace(&bb).second);
current_bb = &bb;
- domain.reset();
-
if (&f.getFirstBB() == &bb)
return true;
@@ -554,7 +546,7 @@ bool State::startBB(const BasicBlock &bb) {
}
domain.path = path();
- domain.UB.add(*UB());
+ domain.UB = *UB();
memory = *in_memory();
var_args_data = *var_args_in();

MODIFY
ir/state.h
ir/state.h
@@ -30,7 +30,7 @@ public:
private:
struct CurrentDomain {
- smt::expr path; // path from fn entry
+ smt::expr path = true; // path from fn entry
smt::AndExpr UB;
std::set<smt::expr> undef_vars;

MODIFY
ir/value.cpp
ir/value.cpp
@@ -197,11 +197,8 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
return agg->aggregateVals(vals);
}
- bool has_byval = hasAttribute(ParamAttrs::ByVal);
- bool has_deref = hasAttribute(ParamAttrs::Dereferenceable);
-
expr val;
- if (has_byval) {
+ if (hasAttribute(ParamAttrs::ByVal)) {
unsigned bid;
expr size = expr::mkUInt(attrs.blockSize, bits_size_t);
val = get_global(s, getName(), size, attrs.align, false, bid);
@@ -221,10 +218,15 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
s.addUndefVar(move(var));
}
- if (has_deref) {
- Pointer p(s.getMemory(), val);
- s.addAxiom(p.isDereferenceable(attrs.derefBytes, bits_byte/8, false));
- }
+ if (hasAttribute(ParamAttrs::NonNull))
+ s.addUB(!Pointer(s.getMemory(), val).isNull());
+
+ if (hasAttribute(ParamAttrs::Align))
+ s.addUB(Pointer(s.getMemory(), val).isAligned(attrs.align));
+
+ if (hasAttribute(ParamAttrs::Dereferenceable))
+ s.addUB(Pointer(s.getMemory(), val)
+ .isDereferenceable(attrs.derefBytes, bits_byte/8, false));
bool never_poison = config::disable_poison_input || attrs.poisonImpliesUB();
string np_name = "np_" + getSMTName(child);

MODIFY
tests/alive-tv/issue476.srctgt.ll
tests/alive-tv/issue476.srctgt.ll
+; ERROR: Source is more defined than target
+
define i32 @src(i8* dereferenceable(4) %p) {
ret i32 0
}
@@ -5,5 +7,3 @@ define i32 @src(i8* dereferenceable(4) %p) {
define i32 @tgt(i8* dereferenceable(8) %p) {
ret i32 0
}
-
-; ERROR: Unsupported interprocedural transformation: signature mismatch between src and tgt

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -703,7 +703,7 @@ static void calculateAndInitConstants(Transform &t) {
}
if (i->hasAttribute(ParamAttrs::ByVal)) {
does_mem_access = true;
- auto sz = i->getAttributes().blockSize;
+ uint64_t sz = i->getAttributes().blockSize;
max_access_size = max(max_access_size, sz);
min_global_size = min_global_size != UINT64_MAX
? gcd(sz, min_global_size)

fix fn argument checking of align, nonnull, and dereferenceable