fix nonnull semantics to mean (ptr2int p) != 0.
add optimization for the case addresses aren't observed (common case)
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -490,6 +490,12 @@ expr Pointer::isNull() const {
return *this == mkNullPointer(m);
}
+expr Pointer::isNonZero() const {
+ if (observes_addresses())
+ return get_address() != 0;
+ return get_bid() != 0 || get_offset() != 0;
+}
+
ostream& operator<<(ostream &os, const Pointer &p) {
if (p.isNull().isTrue())
return os << "null";

MODIFY
ir/memory.h
ir/memory.h
@@ -104,6 +104,7 @@ public:
static Pointer mkNullPointer(const Memory &m);
smt::expr isNull() const;
+ smt::expr isNonZero() const;
friend std::ostream& operator<<(std::ostream &os, const Pointer &p);
};

MODIFY
ir/value.cpp
ir/value.cpp
@@ -108,41 +108,6 @@ StateValue GlobalVariable::toSMT(State &s) const {
}
-Input::Input(Type &type, string &&name)
- : Value(type, string(name)), smt_name(move(name)) {}
-
-void Input::copySMTName(const Input &other) {
- smt_name = other.smt_name;
-}
-
-void Input::print(ostream &os) const {
- UNREACHABLE();
-}
-
-StateValue Input::toSMT(State &s) const {
- // 00: normal, 01: undef, else: poison
- expr type = getTyVar();
-
- auto val = getType().mkInput(s, smt_name.c_str());
-
- if (!config::disable_undef_input) {
- auto [undef, vars] = getType().mkUndefInput(s);
- for (auto &v : vars) {
- s.addUndefVar(move(v));
- }
- val = expr::mkIf(type.extract(0, 0) == 0, val, undef);
- }
-
- expr poison = getType().getDummyValue(false).non_poison;
- expr non_poison = getType().getDummyValue(true).non_poison;
-
- return { move(val),
- config::disable_poison_input
- ? move(non_poison)
- : expr::mkIf(type.extract(1, 1) == 0, non_poison, poison) };
-}
-
-
static string agg_str(vector<Value*> &vals) {
string r = "{ ";
bool first = true;
@@ -155,7 +120,6 @@ static string agg_str(vector<Value*> &vals) {
return r + " }";
}
-
AggregateValue::AggregateValue(Type &type, vector<Value*> &&vals)
: Value(type, agg_str(vals)), vals(move(vals)) {}
@@ -186,6 +150,51 @@ void AggregateValue::print(std::ostream &os) const {
}
+static string attr_str(unsigned attributes) {
+ string ret;
+ if (attributes & Input::NonNull)
+ ret += "nonnull ";
+ return ret;
+}
+
+Input::Input(Type &type, string &&name, unsigned attributes)
+ : Value(type, attr_str(attributes) + name), smt_name(move(name)),
+ attributes(attributes) {}
+
+void Input::copySMTName(const Input &other) {
+ smt_name = other.smt_name;
+}
+
+void Input::print(ostream &os) const {
+ UNREACHABLE();
+}
+
+StateValue Input::toSMT(State &s) const {
+ // 00: normal, 01: undef, else: poison
+ expr type = getTyVar();
+
+ auto val = getType().mkInput(s, smt_name.c_str());
+
+ if (!config::disable_undef_input) {
+ auto [undef, vars] = getType().mkUndefInput(s);
+ for (auto &v : vars) {
+ s.addUndefVar(move(v));
+ }
+ val = expr::mkIf(type.extract(0, 0) == 0, val, undef);
+ }
+
+ if (attributes & NonNull)
+ s.addPre(Pointer(s.getMemory(), val).isNonZero());
+
+ expr poison = getType().getDummyValue(false).non_poison;
+ expr non_poison = getType().getDummyValue(true).non_poison;
+
+ return { move(val),
+ config::disable_poison_input
+ ? move(non_poison)
+ : expr::mkIf(type.extract(1, 1) == 0, non_poison, poison) };
+}
+
expr Input::getTyVar() const {
string tyname = "ty_" + smt_name;
return expr::mkVar(tyname.c_str(), 2);

MODIFY
ir/value.h
ir/value.h
@@ -108,9 +108,13 @@ public:
class Input final : public Value {
+public:
+ enum Attributes { None = 0, NonNull = 1<<0 };
+private:
std::string smt_name;
+ unsigned attributes;
public:
- Input(Type &type, std::string &&name);
+ Input(Type &type, std::string &&name, unsigned attributes = 0);
void copySMTName(const Input &other);
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -674,10 +674,10 @@ public:
return true;
}
- bool handleAttributes(BasicBlock &initBB, llvm::Argument &arg) {
- auto attrs = arg.getParent()->getAttributes()
- .getParamAttributes(arg.getArgNo());
- for (auto &attr : attrs) {
+ optional<unsigned> handleAttributes(llvm::Argument &arg) {
+ unsigned attrs = 0;
+ for (auto &attr : arg.getParent()->getAttributes()
+ .getParamAttributes(arg.getArgNo())) {
switch (attr.getKindAsEnum()) {
case llvm::Attribute::ByVal:
case llvm::Attribute::InReg:
@@ -687,26 +687,16 @@ public:
// they don't change
continue;
- case llvm::Attribute::NonNull: {
- auto op = get_operand(&arg);
- auto null = get_operand(llvm::ConstantPointerNull::get(
- cast<llvm::PointerType>(arg.getType())));
- if (!op || !null)
- return false;
- auto ne = make_unique<ICmp>(get_int_type(1),
- "%nonnull#" + value_name(arg), ICmp::NE,
- *op, *null);
- auto ne_ptr = ne.get();
- initBB.addInstr(move(ne));
- initBB.addInstr(make_unique<Assume>(*ne_ptr, true));
+ case llvm::Attribute::NonNull:
+ attrs |= Input::NonNull;
continue;
- }
+
default:
*out << "ERROR: Unsupported attribute: " << attr.getAsString() << '\n';
- return false;
+ return {};
}
}
- return true;
+ return attrs;
}
optional<Function> run() {
@@ -720,18 +710,14 @@ public:
Function Fn(*type, f.getName(), DL().isLittleEndian());
reset_state(Fn);
- auto &InitBB = Fn.getBB("#init", true);
-
for (auto &arg : f.args()) {
auto ty = llvm_type2alive(arg.getType());
- if (!ty)
+ auto attrs = handleAttributes(arg);
+ if (!ty || !attrs)
return {};
- auto val = make_unique<Input>(*ty, value_name(arg));
+ auto val = make_unique<Input>(*ty, value_name(arg), *attrs);
add_identifier(arg, *val.get());
Fn.addInput(move(val));
-
- if (!handleAttributes(InitBB, arg))
- return {};
}
// create all BBs upfront to keep LLVM's order
@@ -779,7 +765,9 @@ public:
};
// If there is a global variable with initializer, put them at init block.
- BB = &InitBB;
+ auto &entry_name = Fn.getFirstBB().getName();
+ BB = &Fn.getBB("#init", true);
+
for (auto &gvname : gvnamesInSrc) {
auto gv = getGlobalVariable(string(gvname));
if (!gv) {
@@ -812,12 +800,12 @@ public:
for (auto &itm : stores)
// Insert stores in lexicographical order of global var's names
- InitBB.addInstr(move(itm.second));
+ BB->addInstr(move(itm.second));
- if (InitBB.empty())
- Fn.removeBB(InitBB);
+ if (BB->empty())
+ Fn.removeBB(*BB);
else
- InitBB.addInstr(make_unique<Branch>(Fn.getBB(Fn.getBBs()[1]->getName())));
+ BB->addInstr(make_unique<Branch>(string(entry_name)));
return move(Fn);
}

fix nonnull semantics to mean (ptr2int p) != 0.
add optimization for the case addresses aren't observed (common case)