refactor code duplication in fn/paramattr encoding
MODIFY
ir/attrs.cpp
ir/attrs.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/attrs.h"
+#include "ir/memory.h"
+#include "ir/state.h"
+#include "ir/state_value.h"
+#include "ir/type.h"
#include <cassert>
using namespace std;
+using namespace smt;
namespace IR {
ostream& operator<<(ostream &os, const ParamAttrs &attr) {
@@ -83,6 +88,45 @@ uint64_t ParamAttrs::getDerefBytes() const {
return bytes;
}
+static void
+encodePtrAttrs(const State &s, const expr &ptrvalue,
+ AndExpr &UB, expr &non_poison,
+ uint64_t derefBytes, uint64_t derefOrNullBytes, uint64_t align,
+ bool nonnull) {
+ Pointer p(s.getMemory(), ptrvalue);
+
+ if (nonnull)
+ non_poison &= p.isNonZero();
+
+ if (derefBytes || derefOrNullBytes) {
+ // dereferenceable, byval (ParamAttrs), dereferenceable_or_null
+ if (derefBytes)
+ UB.add(p.isDereferenceable(derefBytes, align));
+ if (derefOrNullBytes)
+ UB.add(p.isDereferenceable(derefOrNullBytes, align)() || !p.isNonZero());
+ } else if (align != 1)
+ // align
+ non_poison &= p.isAligned(align);
+}
+
+pair<AndExpr, expr>
+ParamAttrs::encode(const State &s, const StateValue &val, const Type &ty) const {
+ AndExpr UB;
+ expr new_non_poison = val.non_poison;
+
+ if (ty.isPtrType())
+ encodePtrAttrs(s, val.value, UB, new_non_poison,
+ getDerefBytes(), derefOrNullBytes, align, has(NonNull));
+
+ if (poisonImpliesUB()) {
+ UB.add(move(new_non_poison));
+ new_non_poison = true;
+ }
+
+ return { move(UB), move(new_non_poison) };
+}
+
+
bool FnAttrs::poisonImpliesUB() const {
return has(Dereferenceable) || has(NoUndef) || has(NNaN) ||
has(DereferenceableOrNull);
@@ -93,4 +137,27 @@ bool FnAttrs::undefImpliesUB() const {
assert(!ub || poisonImpliesUB());
return ub;
}
+
+pair<AndExpr, expr>
+FnAttrs::encode(const State &s, const StateValue &val, const Type &ty) const {
+ AndExpr UB;
+ expr new_non_poison = val.non_poison;
+
+ if (has(FnAttrs::NNaN)) {
+ assert(ty.isFloatType());
+ UB.add(val.non_poison.implies(!val.value.isNaN()));
+ }
+
+ if (ty.isPtrType())
+ encodePtrAttrs(s, val.value, UB, new_non_poison,
+ derefBytes, derefOrNullBytes, align, has(NonNull));
+
+ if (poisonImpliesUB()) {
+ UB.add(move(new_non_poison));
+ new_non_poison = true;
+ }
+
+ return { move(UB), move(new_non_poison) };
+}
+
}

MODIFY
ir/attrs.h
ir/attrs.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include "smt/exprs.h"
#include <ostream>
namespace IR {
+class State;
+struct StateValue;
+class Type;
+
class ParamAttrs final {
unsigned bits;
@@ -18,8 +23,8 @@ public:
ParamAttrs(unsigned bits = None) : bits(bits) {}
- uint64_t derefBytes; // Dereferenceable
- uint64_t derefOrNullBytes; // DereferenceableOrNull
+ uint64_t derefBytes = 0; // Dereferenceable
+ uint64_t derefOrNullBytes = 0; // DereferenceableOrNull
unsigned blockSize; // exact block size for e.g. byval args
unsigned align = 1;
@@ -37,6 +42,10 @@ public:
uint64_t getDerefBytes() const;
friend std::ostream& operator<<(std::ostream &os, const ParamAttrs &attr);
+
+ // Encodes the semantics of attributes using UB and poison.
+ std::pair<smt::AndExpr, smt::expr>
+ encode(const State &s, const StateValue &val, const Type &ty) const;
};
@@ -56,8 +65,8 @@ public:
bool has(Attribute a) const { return (bits & a) != 0; }
void set(Attribute a) { bits |= (unsigned)a; }
- uint64_t derefBytes; // Dereferenceable
- uint64_t derefOrNullBytes; // DereferenceableOrNull
+ uint64_t derefBytes = 0; // Dereferenceable
+ uint64_t derefOrNullBytes = 0; // DereferenceableOrNull
unsigned align = 1;
// Returns true if returning poison or an aggregate having a poison is UB
@@ -67,6 +76,10 @@ public:
bool undefImpliesUB() const;
friend std::ostream& operator<<(std::ostream &os, const FnAttrs &attr);
+
+ // Encodes the semantics of attributes using UB and poison.
+ std::pair<smt::AndExpr, smt::expr>
+ encode(const State &s, const StateValue &val, const Type &ty) const;
};
}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1704,33 +1704,12 @@ static void unpack_inputs(State &s, Value &argv, Type &ty,
}
auto unpack = [&](StateValue &&value) {
- if (ty.isPtrType()) {
- expr np(true);
- Pointer p(s.getMemory(), move(value.value));
-
- bool isDeref = argflag.has(ParamAttrs::Dereferenceable) ||
- argflag.has(ParamAttrs::ByVal);
- bool isDerefOrNull = argflag.has(ParamAttrs::DereferenceableOrNull);
-
- if (isDeref || isDerefOrNull) {
- if (isDeref)
- s.addUB(p.isDereferenceable(argflag.getDerefBytes(), argflag.align));
- if (isDerefOrNull)
- s.addUB(
- p.isDereferenceable(argflag.derefOrNullBytes, argflag.align)() ||
- !p.isNonZero());
- } else if (argflag.has(ParamAttrs::Align))
- np &= p.isAligned(argflag.align);
-
- if (argflag.has(ParamAttrs::NonNull))
- np &= p.isNonZero();
+ auto [UB, new_non_poison] = argflag.encode(s, value, ty);
+ s.addUB(move(UB));
+ value.non_poison = move(new_non_poison);
- if (argflag.poisonImpliesUB()) {
- s.addUB(move(np));
- np = true;
- }
-
- ptr_inputs.emplace_back(StateValue(p.release(), np && value.non_poison),
+ if (ty.isPtrType()) {
+ ptr_inputs.emplace_back(move(value),
argflag.has(ParamAttrs::ByVal),
argflag.has(ParamAttrs::NoCapture));
} else {
@@ -1756,39 +1735,15 @@ static void unpack_ret_ty (vector<Type*> &out_types, Type &ty) {
static void check_return_value(State &s, StateValue &val, const Type &ty,
const FnAttrs &attrs, bool is_ret_instr) {
- if (attrs.has(FnAttrs::NNaN)) {
- assert(ty.isFloatType());
- s.addUB(val.non_poison.implies(!val.value.isNaN()));
- }
+ auto [UB, new_non_poison] = attrs.encode(s, val, ty);
+ s.addUB(move(UB));
+ val.non_poison = move(new_non_poison);
- if (ty.isPtrType()) {
+ if (ty.isPtrType() && is_ret_instr) {
Pointer p(s.getMemory(), val.value);
-
- if (is_ret_instr) {
s.addUB(val.non_poison.implies(!p.isStackAllocated() &&
!p.isNocapture()));
}
-
- bool isDeref = attrs.has(FnAttrs::Dereferenceable);
- bool isDerefOrNull = attrs.has(FnAttrs::DereferenceableOrNull);
-
- if (isDeref || isDerefOrNull) {
- if (isDeref)
- s.addUB(p.isDereferenceable(attrs.derefBytes, attrs.align));
- if (isDerefOrNull)
- s.addUB(p.isDereferenceable(attrs.derefOrNullBytes, attrs.align)() ||
- !p.isNonZero());
- } else if (attrs.has(FnAttrs::Align))
- val.non_poison &= p.isAligned(attrs.align);
-
- if (attrs.has(FnAttrs::NonNull))
- val.non_poison &= p.isNonZero();
- }
-
- if (attrs.poisonImpliesUB()) {
- s.addUB(move(val.non_poison));
- val.non_poison = true;
- }
}
static StateValue

MODIFY
ir/type.h
ir/type.h
@@ -275,7 +275,7 @@ public:
unsigned numPaddingsConst() const;
StateValue aggregateVals(const std::vector<StateValue> &vals) const;
- IR::StateValue extract(const IR::StateValue &val, unsigned index,
+ StateValue extract(const StateValue &val, unsigned index,
bool fromInt = false) const;
Type& getChild(unsigned index) const { return *children[index]; }
bool isPadding(unsigned i) const { return is_padding[i]; }

MODIFY
ir/value.cpp
ir/value.cpp
@@ -218,37 +218,14 @@ StateValue Input::mkInput(State &s, const Type &ty, unsigned child) const {
s.addUndefVar(move(var));
}
- // Some attributes generate poison rather than raise UB
- expr np_from_attr(true);
- if (ty.isPtrType()) {
- Pointer p(s.getMemory(), val);
-
- if (hasAttribute(ParamAttrs::NonNull))
- np_from_attr = p.isNonZero();
-
- bool hasDeref = hasAttribute(ParamAttrs::Dereferenceable) ||
- hasAttribute(ParamAttrs::ByVal);
- bool hasDerefOrNull = hasAttribute(ParamAttrs::DereferenceableOrNull);
- if (hasDeref || hasDerefOrNull) {
- if (hasDeref)
- s.addUB(p.isDereferenceable(attrs.getDerefBytes(), attrs.align));
- if (hasDerefOrNull)
- s.addUB(p.isDereferenceable(attrs.derefOrNullBytes, attrs.align)() ||
- !p.isNonZero());
- } else if (hasAttribute(ParamAttrs::Align))
- np_from_attr &= p.isAligned(attrs.align);
- }
-
- if (attrs.poisonImpliesUB()) {
- s.addUB(move(np_from_attr));
- np_from_attr = true;
- }
+ auto [UB, non_poison] = attrs.encode(s, {expr(val), expr(true)}, ty);
+ s.addUB(move(UB));
bool never_poison = config::disable_poison_input || attrs.poisonImpliesUB();
string np_name = "np_" + getSMTName(child);
return { move(val),
- np_from_attr && (never_poison ? true :
+ move(non_poison) && (never_poison ? true :
expr::mkBoolVar(np_name.c_str())) };
}
@@ -264,12 +241,7 @@ StateValue Input::toSMT(State &s) const {
}
expr Input::getUndefVar(const Type &ty, unsigned child) const {
- // TODO: Clarify whether byval/dereferenceable accept partially undefined
- // pointers
- if (config::disable_undef_input ||
- hasAttribute(ParamAttrs::ByVal) ||
- hasAttribute(ParamAttrs::Dereferenceable) ||
- attrs.undefImpliesUB())
+ if (config::disable_undef_input || attrs.undefImpliesUB())
return {};
string tyname = "isundef_" + getSMTName(child);

refactor code duplication in fn/paramattr encoding (#683)