Factor out function attributes as an independent class
ADD
ir/attrs.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include <string>
+
+namespace IR {
+
+class ParamAttrs final {
+public:
+ enum Attribute { None = 0, NonNull = 1<<0, ByVal = 1<<1, NoCapture = 1<<2,
+ ReadOnly = 1<<3, ReadNone = 1<<4 };
+
+ unsigned bits;
+
+ ParamAttrs(unsigned bits = None) : bits(bits) {}
+
+ std::string str() const {
+ std::string ret;
+ if (has(ParamAttrs::NonNull))
+ ret += "nonnull ";
+ if (has(ParamAttrs::ByVal))
+ ret += "byval ";
+ if (has(ParamAttrs::NoCapture))
+ ret += "nocapture ";
+ if (has(ParamAttrs::ReadOnly))
+ ret += "readonly ";
+ if (has(ParamAttrs::ReadNone))
+ ret += "readnone ";
+ return ret;
+ }
+
+ bool has(Attribute a) const { return (bits & a) != 0; }
+ void set(Attribute a) { bits = bits | (unsigned)a; }
+};
+
+}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1271,8 +1271,8 @@ unique_ptr<Instr> InsertValue::dup(const string &suffix) const {
}
-void FnCall::addArg(Value &arg, unsigned flags) {
- args.emplace_back(&arg, flags);
+void FnCall::addArg(Value &arg, ParamAttrs &&attrs) {
+ args.emplace_back(&arg, move(attrs));
}
vector<Value*> FnCall::operands() const {
@@ -1295,13 +1295,11 @@ void FnCall::print(ostream &os) const {
os << "call " << print_type(getType()) << fnName << '(';
bool first = true;
- for (auto &[arg, flags] : args) {
+ for (auto &[arg, attrs] : args) {
if (!first)
os << ", ";
- if (flags & ArgByVal)
- os << "byval ";
- os << *arg;
+ os << attrs.str() << *arg;
first = false;
}
os << ')';
@@ -1321,7 +1319,7 @@ void FnCall::print(ostream &os) const {
os << "\t; WARNING: unknown known function";
}
-static void unpack_inputs(State&s, Type &ty, unsigned argflag,
+static void unpack_inputs(State&s, Type &ty, const ParamAttrs &argflag,
const StateValue &value, vector<StateValue> &inputs,
vector<pair<StateValue, bool>> &ptr_inputs) {
if (auto agg = ty.getAsAggregateType()) {
@@ -1334,7 +1332,7 @@ static void unpack_inputs(State&s, Type &ty, unsigned argflag,
Pointer p(s.getMemory(), value.value);
p.stripAttrs();
ptr_inputs.emplace_back(StateValue(p.release(), expr(value.non_poison)),
- argflag & FnCall::ArgByVal);
+ argflag.has(ParamAttrs::ByVal));
} else {
inputs.emplace_back(value);
}

MODIFY
ir/instr.h
ir/instr.h
@@ -191,10 +191,9 @@ class FnCall final : public Instr {
public:
enum Flags { None = 0, NoRead = 1 << 0, NoWrite = 1 << 1, ArgMemOnly = 1 << 2,
NNaN = 1 << 3, NoReturn = 1 << 4 };
- enum ArgFlags { ArgNone = 0, ArgByVal = 1 << 0 };
private:
std::string fnName;
- std::vector<std::pair<Value*, unsigned>> args;
+ std::vector<std::pair<Value*, ParamAttrs>> args;
unsigned flags;
bool valid;
public:
@@ -202,7 +201,7 @@ public:
unsigned flags = None, bool valid = true)
: Instr(type, std::move(name)), fnName(std::move(fnName)), flags(flags),
valid(valid) {}
- void addArg(Value &arg, unsigned flags);
+ void addArg(Value &arg, ParamAttrs &&attrs);
const auto& getFnName() const { return fnName; }
const auto& getArgs() const { return args; }

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -356,18 +356,18 @@ static unsigned bits_shortbid() {
return bits_for_bid - ptr_has_local_bit();
}
-static expr attr_to_bitvec(unsigned attributes) {
+static expr attr_to_bitvec(const ParamAttrs &attrs) {
if (!bits_for_ptrattrs)
return expr();
uint64_t bits = 0;
auto idx = 0;
- auto to_bit = [&](bool b, Input::Attribute a) -> uint64_t {
- return b ? (((attributes & a) ? 1 : 0) << idx++) : 0;
+ auto to_bit = [&](bool b, const ParamAttrs::Attribute &a) -> uint64_t {
+ return b ? ((attrs.has(a) ? 1 : 0) << idx++) : 0;
};
- bits |= to_bit(has_nocapture, Input::NoCapture);
- bits |= to_bit(has_readonly, Input::ReadOnly);
- bits |= to_bit(has_readnone, Input::ReadNone);
+ bits |= to_bit(has_nocapture, ParamAttrs::NoCapture);
+ bits |= to_bit(has_readonly, ParamAttrs::ReadOnly);
+ bits |= to_bit(has_readnone, ParamAttrs::ReadNone);
return expr::mkUInt(bits, bits_for_ptrattrs);
}
@@ -1180,17 +1180,17 @@ void Memory::markByVal(unsigned bid) {
byval_blks.emplace_back(bid);
}
-expr Memory::mkInput(const char *name, unsigned attributes) const {
- Pointer p(*this, name, false, false, false, attr_to_bitvec(attributes));
- if (attributes & Input::NonNull)
+expr Memory::mkInput(const char *name, const ParamAttrs &attrs) const {
+ Pointer p(*this, name, false, false, false, attr_to_bitvec(attrs));
+ if (attrs.has(ParamAttrs::NonNull))
state->addAxiom(p.isNonZero());
state->addAxiom(p.getShortBid().ule(numNonlocals() - 1));
return p.release();
}
-pair<expr, expr> Memory::mkUndefInput(unsigned attributes) const {
- bool nonnull = attributes & Input::NonNull;
+pair<expr, expr> Memory::mkUndefInput(const ParamAttrs &attrs) const {
+ bool nonnull = attrs.has(ParamAttrs::NonNull);
unsigned log_offset = ilog2_ceil(bits_for_offset, false);
unsigned bits_undef = bits_for_offset + nonnull * log_offset;
expr undef = expr::mkFreshVar("undef", expr::mkUInt(0, bits_undef));
@@ -1205,7 +1205,7 @@ pair<expr, expr> Memory::mkUndefInput(unsigned attributes) const {
offset = undef.extract(bits_undef - 1, log_offset) | shl;
}
Pointer p(*this, expr::mkUInt(0, bits_for_bid), offset,
- attr_to_bitvec(attributes));
+ attr_to_bitvec(attrs));
return { p.release(), move(undef) };
}

MODIFY
ir/memory.h
ir/memory.h
@@ -242,8 +242,8 @@ public:
static void resetBids(unsigned last_nonlocal);
void markByVal(unsigned bid);
- smt::expr mkInput(const char *name, unsigned attributes) const;
- std::pair<smt::expr, smt::expr> mkUndefInput(unsigned attributes) const;
+ smt::expr mkInput(const char *name, const ParamAttrs &attrs) const;
+ std::pair<smt::expr, smt::expr> mkUndefInput(const ParamAttrs &attrs) const;
std::pair<smt::expr, smt::expr>
mkFnRet(const char *name,

MODIFY
ir/type.cpp
ir/type.cpp
@@ -248,7 +248,8 @@ expr Type::combine_poison(const expr &boolean, const expr &orig) const {
expr::mkIf(boolean, expr::mkInt(0, orig), expr::mkInt(-1, orig)) | orig;
}
-pair<expr, vector<expr>> Type::mkUndefInput(State &s, unsigned attrs) const {
+pair<expr, vector<expr>>
+Type::mkUndefInput(State &s, const ParamAttrs &attrs) const {
auto var = expr::mkFreshVar("undef", mkInput(s, "", attrs));
return { var, { var } };
}
@@ -289,7 +290,8 @@ VoidType::refines(State &src_s, State &tgt_s, const StateValue &src,
return { true, true };
}
-expr VoidType::mkInput(State &s, const char *name, unsigned attributes) const {
+expr VoidType::mkInput(State &s, const char *name,
+ const ParamAttrs &attrs) const {
UNREACHABLE();
}
@@ -347,7 +349,8 @@ IntType::refines(State &src_s, State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
}
-expr IntType::mkInput(State &s, const char *name, unsigned attributes) const {
+expr IntType::mkInput(State &s, const char *name,
+ const ParamAttrs &attrs) const {
return expr::mkVar(name, bits());
}
@@ -531,7 +534,8 @@ FloatType::refines(State &src_s, State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
}
-expr FloatType::mkInput(State &s, const char *name, unsigned attrs) const {
+expr FloatType::mkInput(State &s, const char *name,
+ const ParamAttrs &attrs) const {
switch (fpType) {
case Half: return expr::mkHalfVar(name);
case Float: return expr::mkFloatVar(name);
@@ -647,11 +651,13 @@ PtrType::refines(State &src_s, State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(p.refined(q)) };
}
-expr PtrType::mkInput(State &s, const char *name, unsigned attrs) const {
+expr PtrType::mkInput(State &s, const char *name,
+ const ParamAttrs &attrs) const {
return s.getMemory().mkInput(name, attrs);
}
-pair<expr, vector<expr>> PtrType::mkUndefInput(State &s, unsigned attrs) const {
+pair<expr, vector<expr>>
+PtrType::mkUndefInput(State &s, const ParamAttrs &attrs) const {
auto [val, var] = s.getMemory().mkUndefInput(attrs);
return { move(val), { move(var) } };
}
@@ -918,7 +924,8 @@ AggregateType::refines(State &src_s, State &tgt_s, const StateValue &src,
return { expr::mk_and(poison), expr::mk_and(value) };
}
-expr AggregateType::mkInput(State &s, const char *name, unsigned attrs) const {
+expr AggregateType::mkInput(State &s, const char *name,
+ const ParamAttrs &attrs) const {
expr val;
for (unsigned i = 0; i < elements; ++i) {
string c_name = string(name) + "#" + to_string(i);
@@ -930,7 +937,7 @@ expr AggregateType::mkInput(State &s, const char *name, unsigned attrs) const {
}
pair<expr, vector<expr>>
-AggregateType::mkUndefInput(State &s, unsigned attrs) const {
+AggregateType::mkUndefInput(State &s, const ParamAttrs &attrs) const {
expr val;
vector<expr> vars;
@@ -1362,12 +1369,13 @@ SymbolicType::refines(State &src_s, State &tgt_s, const StateValue &src,
DISPATCH(refines(src_s, tgt_s, src, tgt), UNREACHABLE());
}
-expr SymbolicType::mkInput(State &st, const char *name, unsigned attrs) const {
+expr SymbolicType::mkInput(State &st, const char *name,
+ const ParamAttrs &attrs) const {
DISPATCH(mkInput(st, name, attrs), UNREACHABLE());
}
pair<expr, vector<expr>>
-SymbolicType::mkUndefInput(State &st, unsigned attrs) const {
+SymbolicType::mkUndefInput(State &st, const ParamAttrs &attrs) const {
DISPATCH(mkUndefInput(st, attrs), UNREACHABLE());
}

MODIFY
ir/type.h
ir/type.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include "ir/attrs.h"
#include "smt/expr.h"
#include <functional>
@@ -109,9 +110,9 @@ public:
const StateValue &tgt) const = 0;
virtual smt::expr
- mkInput(State &s, const char *name, unsigned attributes) const = 0;
+ mkInput(State &s, const char *name, const ParamAttrs &attrs) const = 0;
virtual std::pair<smt::expr, std::vector<smt::expr>>
- mkUndefInput(State &s, unsigned attributes) const;
+ mkUndefInput(State &s, const ParamAttrs &attrs) const;
virtual void printVal(std::ostream &os, State &s,
const smt::expr &e) const = 0;
@@ -137,7 +138,7 @@ public:
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
- mkInput(State &s, const char *name, unsigned attributes) const override;
+ mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -164,7 +165,7 @@ public:
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
- mkInput(State &s, const char *name, unsigned attributes) const override;
+ mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -209,7 +210,7 @@ public:
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
- mkInput(State &s, const char *name, unsigned attributes) const override;
+ mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -241,9 +242,9 @@ public:
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
- mkInput(State &s, const char *name, unsigned attributes) const override;
+ mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkUndefInput(State &s, unsigned attributes) const override;
+ mkUndefInput(State &s, const ParamAttrs &attrs) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -297,9 +298,9 @@ public:
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
- mkInput(State &s, const char *name, unsigned attributes) const override;
+ mkInput(State &s, const char *name, const ParamAttrs &attrs) const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkUndefInput(State &s, unsigned attributes) const override;
+ mkUndefInput(State &s, const ParamAttrs &attrs) const override;
unsigned numPointerElements() const;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
const AggregateType* getAsAggregateType() const override;
@@ -404,9 +405,10 @@ public:
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
smt::expr
- mkInput(State &s, const char *name, unsigned attributes) const override;
+ mkInput(State &s, const char *name, const ParamAttrs &attrs)
+ const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkUndefInput(State &s, unsigned attributes) const override;
+ mkUndefInput(State &s, const ParamAttrs &attrs) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};

MODIFY
ir/value.cpp
ir/value.cpp
@@ -156,24 +156,9 @@ void AggregateValue::print(std::ostream &os) const {
}
-static string attr_str(unsigned attributes) {
- string ret;
- if (attributes & Input::NonNull)
- ret += "nonnull ";
- if (attributes & Input::ByVal)
- ret += "byval ";
- if (attributes & Input::NoCapture)
- ret += "nocapture ";
- if (attributes & Input::ReadOnly)
- ret += "readonly ";
- if (attributes & Input::ReadNone)
- ret += "readnone ";
- return ret;
-}
-
-Input::Input(Type &type, string &&name, unsigned attributes)
- : Value(type, attr_str(attributes) + name), smt_name(move(name)),
- attributes(attributes) {}
+Input::Input(Type &type, string &&name, const ParamAttrs &attributes)
+ : Value(type, attributes.str() + name), smt_name(move(name)),
+ attrs(attributes) {}
void Input::copySMTName(const Input &other) {
smt_name = other.smt_name;
@@ -188,18 +173,18 @@ StateValue Input::toSMT(State &s) const {
expr type = getTyVar();
expr val;
- if (attributes & ByVal) {
+ if (hasAttribute(ParamAttrs::ByVal)) {
unsigned bid;
string sz_name = getName() + "#size";
expr size = expr::mkVar(sz_name.c_str(), bits_size_t-1).zext(1);
val = get_global(s, getName(), size, 1, false, bid);
s.getMemory().markByVal(bid);
} else {
- val = getType().mkInput(s, smt_name.c_str(), attributes);
+ val = getType().mkInput(s, smt_name.c_str(), attrs);
}
if (!config::disable_undef_input) {
- auto [undef, vars] = getType().mkUndefInput(s, attributes);
+ auto [undef, vars] = getType().mkUndefInput(s, attrs);
for (auto &v : vars) {
s.addUndefVar(move(v));
}

MODIFY
ir/value.h
ir/value.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+#include "ir/attrs.h"
#include "ir/state.h"
#include "ir/type.h"
#include "smt/expr.h"
@@ -108,17 +109,14 @@ public:
class Input final : public Value {
-public:
- enum Attribute { None = 0, NonNull = 1<<0, ByVal = 1<<1, NoCapture = 1<<2,
- ReadOnly = 1 << 3, ReadNone = 1 << 4 };
-private:
std::string smt_name;
- unsigned attributes;
+ ParamAttrs attrs;
public:
- Input(Type &type, std::string &&name, unsigned attributes = 0);
+ Input(Type &type, std::string &&name,
+ const ParamAttrs &attrs = ParamAttrs::None);
void copySMTName(const Input &other);
void print(std::ostream &os) const override;
- bool hasAttribute(Attribute a) const { return (attributes & a) != 0; }
+ bool hasAttribute(ParamAttrs::Attribute a) const { return attrs.has(a); }
StateValue toSMT(State &s) const override;
smt::expr getTyVar() const;
};

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -271,17 +271,17 @@ public:
unique_ptr<Instr> ret_val;
auto argI = fn->arg_begin(), argE = fn->arg_end();
for (auto &arg : args) {
- unsigned attr = FnCall::ArgNone;
+ ParamAttrs attr;
if (argI != argE) {
// Check whether arg itr finished early because it was var arg
if (argI->hasByValAttr())
- attr |= FnCall::ArgByVal;
+ attr.set(ParamAttrs::ByVal);
else if (argI->hasReturnedAttr()) {
auto call2
= make_unique<FnCall>(Type::voidTy, "", string(call->getFnName()),
flags, !known);
for (auto &[arg, flags] : call->getArgs()) {
- call2->addArg(*arg, flags);
+ call2->addArg(*arg, ParamAttrs(flags));
}
call = move(call2);
@@ -297,7 +297,7 @@ public:
}
++argI;
}
- call->addArg(*arg, attr);
+ call->addArg(*arg, move(attr));
}
if (ret_val) {
BB->addInstr(move(call));
@@ -815,8 +815,8 @@ public:
return true;
}
- optional<unsigned> handleAttributes(llvm::Argument &arg) {
- unsigned attrs = 0;
+ optional<ParamAttrs> handleAttributes(llvm::Argument &arg) {
+ ParamAttrs attrs;
for (auto &attr : arg.getParent()->getAttributes()
.getParamAttributes(arg.getArgNo())) {
switch (attr.getKindAsEnum()) {
@@ -828,28 +828,28 @@ public:
continue;
case llvm::Attribute::ByVal:
- attrs |= Input::ByVal;
+ attrs.set(ParamAttrs::ByVal);
continue;
case llvm::Attribute::NonNull:
- attrs |= Input::NonNull;
+ attrs.set(ParamAttrs::NonNull);
continue;
case llvm::Attribute::NoCapture:
- attrs |= Input::NoCapture;
+ attrs.set(ParamAttrs::NoCapture);
continue;
case llvm::Attribute::ReadOnly:
- attrs |= Input::ReadOnly;
+ attrs.set(ParamAttrs::ReadOnly);
continue;
case llvm::Attribute::ReadNone:
- attrs |= Input::ReadNone;
+ attrs.set(ParamAttrs::ReadNone);
continue;
default:
*out << "ERROR: Unsupported attribute: " << attr.getAsString() << '\n';
- return {};
+ return nullopt;
}
}
return attrs;

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -945,7 +945,7 @@ static unique_ptr<Instr> parse_call(string_view name) {
tokenizer.ensure(COMMA);
first = false;
auto &ty = parse_type();
- call->addArg(parse_operand(ty), FnCall::ArgNone);
+ call->addArg(parse_operand(ty), ParamAttrs::None);
}
tokenizer.ensure(RPAREN);
return call;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -799,7 +799,7 @@ static void calculateAndInitConstants(Transform &t) {
if (!does_int_mem_access && !does_ptr_mem_access && has_fncall)
does_int_mem_access = true;
- auto has_attr = [&](Input::Attribute a) -> bool {
+ auto has_attr = [&](ParamAttrs::Attribute a) -> bool {
for (auto fn : { &t.src, &t.tgt }) {
for (auto &v : fn->getInputs()) {
auto i = dynamic_cast<const Input*>(&v);
@@ -811,10 +811,10 @@ static void calculateAndInitConstants(Transform &t) {
};
// The number of bits needed to encode pointer attributes
// nonnull and byval isn't encoded in ptr attribute bits
- bool has_byval = has_attr(Input::ByVal);
- has_nocapture = has_attr(Input::NoCapture);
- has_readonly = has_attr(Input::ReadOnly);
- has_readnone = has_attr(Input::ReadNone);
+ bool has_byval = has_attr(ParamAttrs::ByVal);
+ has_nocapture = has_attr(ParamAttrs::NoCapture);
+ has_readonly = has_attr(ParamAttrs::ReadOnly);
+ has_readnone = has_attr(ParamAttrs::ReadNone);
bits_for_ptrattrs = has_nocapture + has_readonly + has_readnone;
// ceil(log2(maxblks)) + 1 for local bit

Factor out function attributes as an independent class (#376)