further fixes for 64-bit alignments
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2704,7 +2704,7 @@ bool Malloc::canFree() const {
return ptr != nullptr;
}
-unsigned Malloc::getAlign() const {
+uint64_t Malloc::getAlign() const {
return align ? align : heap_block_alignment;
}
@@ -2804,7 +2804,7 @@ Calloc::ByteAccessInfo Calloc::getByteAccessInfo() const {
return info;
}
-unsigned Calloc::getAlign() const {
+uint64_t Calloc::getAlign() const {
return align ? align : heap_block_alignment;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -473,10 +473,10 @@ public:
class Alloc final : public MemInstr {
Value *size, *mul;
- unsigned align;
+ uint64_t align;
bool initially_dead = false;
public:
- Alloc(Type &type, std::string &&name, Value &size, Value *mul, unsigned align)
+ Alloc(Type &type, std::string &&name, Value &size, Value *mul, uint64_t align)
: MemInstr(type, std::move(name)), size(&size), mul(mul), align(align) {}
Value& getSize() const { return *size; }
@@ -501,23 +501,23 @@ public:
class Malloc final : public MemInstr {
Value *ptr = nullptr, *size;
- unsigned align;
+ uint64_t align;
// Is this malloc (or equivalent operation, like new()) never returning
// null?
bool isNonNull = false;
public:
Malloc(Type &type, std::string &&name, Value &size, bool isNonNull,
- unsigned align = 0)
+ uint64_t align = 0)
: MemInstr(type, std::move(name)), size(&size), align(align),
isNonNull(isNonNull) {}
Malloc(Type &type, std::string &&name, Value &ptr, Value &size,
- unsigned align = 0)
+ uint64_t align = 0)
: MemInstr(type, std::move(name)), ptr(&ptr), size(&size), align(align) {}
Value& getSize() const { return *size; }
- unsigned getAlign() const;
+ uint64_t getAlign() const;
bool isRealloc() const { return ptr != nullptr; }
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
@@ -537,15 +537,15 @@ public:
class Calloc final : public MemInstr {
Value *num, *size;
- unsigned align;
+ uint64_t align;
public:
Calloc(Type &type, std::string &&name, Value &num, Value &size,
- unsigned align = 0)
+ uint64_t align = 0)
: MemInstr(type, std::move(name)), num(&num), size(&size), align(align) {}
Value& getNum() const { return *num; }
Value& getSize() const { return *size; }
- unsigned getAlign() const;
+ uint64_t getAlign() const;
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
uint64_t getMaxAccessSize() const override;
@@ -635,13 +635,13 @@ public:
class Load final : public MemInstr {
Value *ptr;
- unsigned align;
+ uint64_t align;
public:
- Load(Type &type, std::string &&name, Value &ptr, unsigned align)
+ Load(Type &type, std::string &&name, Value &ptr, uint64_t align)
: MemInstr(type, std::move(name)), ptr(&ptr), align(align) {}
Value& getPtr() const { return *ptr; }
- unsigned getAlign() const { return align; }
+ uint64_t getAlign() const { return align; }
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
uint64_t getMaxAccessSize() const override;
@@ -660,14 +660,14 @@ public:
class Store final : public MemInstr {
Value *ptr, *val;
- unsigned align;
+ uint64_t align;
public:
- Store(Value &ptr, Value &val, unsigned align)
+ Store(Value &ptr, Value &val, uint64_t align)
: MemInstr(Type::voidTy, "store"), ptr(&ptr), val(&val), align(align) {}
Value& getValue() const { return *val; }
Value& getPtr() const { return *ptr; }
- unsigned getAlign() const { return align; }
+ uint64_t getAlign() const { return align; }
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
uint64_t getMaxAccessSize() const override;
@@ -687,14 +687,14 @@ public:
class Memset final : public MemInstr {
Value *ptr, *val, *bytes;
- unsigned align;
+ uint64_t align;
public:
- Memset(Value &ptr, Value &val, Value &bytes, unsigned align)
+ Memset(Value &ptr, Value &val, Value &bytes, uint64_t align)
: MemInstr(Type::voidTy, "memset"), ptr(&ptr), val(&val), bytes(&bytes),
align(align) {}
Value& getBytes() const { return *bytes; }
- unsigned getAlign() const { return align; }
+ uint64_t getAlign() const { return align; }
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
uint64_t getMaxAccessSize() const override;
@@ -733,17 +733,17 @@ public:
class Memcpy final : public MemInstr {
Value *dst, *src, *bytes;
- unsigned align_dst, align_src;
+ uint64_t align_dst, align_src;
bool move;
public:
Memcpy(Value &dst, Value &src, Value &bytes,
- unsigned align_dst, unsigned align_src, bool move)
+ uint64_t align_dst, uint64_t align_src, bool move)
: MemInstr(Type::voidTy, "memcpy"), dst(&dst), src(&src), bytes(&bytes),
align_dst(align_dst), align_src(align_src), move(move) {}
Value& getBytes() const { return *bytes; }
- unsigned getSrcAlign() const { return align_src; }
- unsigned getDstAlign() const { return align_dst; }
+ uint64_t getSrcAlign() const { return align_src; }
+ uint64_t getDstAlign() const { return align_dst; }
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
uint64_t getMaxAccessSize() const override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -712,7 +712,7 @@ expr Memory::isBlockAlive(const expr &bid, bool local) const {
}
bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
- unsigned bytes, unsigned align, bool write) const {
+ unsigned bytes, uint64_t align, bool write) const {
if (local && bid0 >= next_local_bid)
return false;
@@ -754,7 +754,7 @@ bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
}
Memory::AliasSet Memory::computeAliasing(const Pointer &ptr, unsigned bytes,
- unsigned align, bool write) const {
+ uint64_t align, bool write) const {
assert(bytes % (bits_byte/8) == 0);
AliasSet aliasing(*this);
@@ -821,7 +821,7 @@ end:
}
template <typename Fn>
-void Memory::access(const Pointer &ptr, unsigned bytes, unsigned align,
+void Memory::access(const Pointer &ptr, unsigned bytes, uint64_t align,
bool write, Fn &fn) {
auto aliasing = computeAliasing(ptr, bytes, align, write);
unsigned has_local = aliasing.numMayAlias(true);
@@ -861,7 +861,7 @@ void Memory::access(const Pointer &ptr, unsigned bytes, unsigned align,
}
vector<Byte> Memory::load(const Pointer &ptr, unsigned bytes, set<expr> &undef,
- unsigned align, bool left2right, DataType type) {
+ uint64_t align, bool left2right, DataType type) {
if (bytes == 0)
return {};
@@ -921,7 +921,7 @@ Memory::DataType Memory::data_type(const vector<pair<unsigned, expr>> &data,
void Memory::store(const Pointer &ptr,
const vector<pair<unsigned, expr>> &data,
- const set<expr> &undef, unsigned align) {
+ const set<expr> &undef, uint64_t align) {
if (data.empty())
return;
@@ -976,7 +976,7 @@ void Memory::store(const Pointer &ptr,
void Memory::storeLambda(const Pointer &ptr, const expr &offset,
const expr &bytes, const expr &val,
- const set<expr> &undef, unsigned align) {
+ const set<expr> &undef, uint64_t align) {
assert(!state->isInitializationPhase());
// offset in [ptr, ptr+sz)
auto offset_cond = offset.uge(ptr.getShortOffset()) &&
@@ -1480,7 +1480,7 @@ void Memory::mkLocalDisjAddrAxioms(const expr &allocated, const expr &short_bid,
}
pair<expr, expr>
-Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
+Memory::alloc(const expr &size, uint64_t align, BlockKind blockKind,
const expr &precond, const expr &nonnull,
optional<unsigned> bidopt, unsigned *bid_out) {
assert(!memory_unused());
@@ -1642,7 +1642,7 @@ void Memory::store(const StateValue &v, const Type &type, unsigned offset0,
}
void Memory::store(const expr &p, const StateValue &v, const Type &type,
- unsigned align, const set<expr> &undef_vars) {
+ uint64_t align, const set<expr> &undef_vars) {
assert(!memory_unused());
Pointer ptr(*this, p);
@@ -1656,7 +1656,7 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
}
StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
- unsigned align) {
+ uint64_t align) {
unsigned bytecount = getStoreByteSize(type);
auto aty = type.getAsAggregateType();
@@ -1712,7 +1712,7 @@ StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
}
pair<StateValue, AndExpr>
-Memory::load(const expr &p, const Type &type, unsigned align) {
+Memory::load(const expr &p, const Type &type, uint64_t align) {
assert(!memory_unused());
Pointer ptr(*this, p);
@@ -1732,7 +1732,7 @@ Byte Memory::raw_load(const Pointer &p) {
}
void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
- unsigned align, const set<expr> &undef_vars,
+ uint64_t align, const set<expr> &undef_vars,
bool deref_check) {
assert(!memory_unused());
assert(!val.isValid() || val.bits() == 8);
@@ -1766,7 +1766,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
}
void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
- unsigned align_dst, unsigned align_src, bool is_move) {
+ uint64_t align_dst, uint64_t align_src, bool is_move) {
assert(!memory_unused());
unsigned bytesz = bits_byte / 8;

MODIFY
ir/memory.h
ir/memory.h
@@ -166,34 +166,34 @@ class Memory {
void mkNonlocalValAxioms(bool skip_consts);
bool mayalias(bool local, unsigned bid, const smt::expr &offset,
- unsigned bytes, unsigned align, bool write) const;
+ unsigned bytes, uint64_t align, bool write) const;
- AliasSet computeAliasing(const Pointer &ptr, unsigned btyes, unsigned align,
+ AliasSet computeAliasing(const Pointer &ptr, unsigned btyes, uint64_t align,
bool write) const;
template <typename Fn>
- void access(const Pointer &ptr, unsigned btyes, unsigned align, bool write,
+ void access(const Pointer &ptr, unsigned btyes, uint64_t align, bool write,
Fn &fn);
std::vector<Byte> load(const Pointer &ptr, unsigned bytes,
- std::set<smt::expr> &undef, unsigned align,
+ std::set<smt::expr> &undef, uint64_t align,
bool left2right = true,
DataType type = DATA_ANY);
StateValue load(const Pointer &ptr, const Type &type,
- std::set<smt::expr> &undef, unsigned align);
+ std::set<smt::expr> &undef, uint64_t align);
DataType data_type(const std::vector<std::pair<unsigned, smt::expr>> &data,
bool full_store) const;
void store(const Pointer &ptr,
const std::vector<std::pair<unsigned, smt::expr>> &data,
- const std::set<smt::expr> &undef, unsigned align);
+ const std::set<smt::expr> &undef, uint64_t align);
void store(const StateValue &val, const Type &type, unsigned offset,
std::vector<std::pair<unsigned, smt::expr>> &data);
void storeLambda(const Pointer &ptr, const smt::expr &offset,
const smt::expr &bytes, const smt::expr &val,
- const std::set<smt::expr> &undef, unsigned align);
+ const std::set<smt::expr> &undef, uint64_t align);
smt::expr blockValRefined(const Memory &other, unsigned bid, bool local,
const smt::expr &offset,
@@ -271,7 +271,7 @@ public:
// In this case, it is caller's responsibility to give a unique bid.
// The newly assigned bid is stored to bid_out if bid_out != nullptr.
// Returns <pointer if allocated, allocated?>
- std::pair<smt::expr, smt::expr> alloc(const smt::expr &size, unsigned align,
+ std::pair<smt::expr, smt::expr> alloc(const smt::expr &size, uint64_t align,
BlockKind blockKind, const smt::expr &precond = true,
const smt::expr &nonnull = false,
std::optional<unsigned> bid = std::nullopt, unsigned *bid_out = nullptr);
@@ -285,19 +285,19 @@ public:
static unsigned getStoreByteSize(const Type &ty);
void store(const smt::expr &ptr, const StateValue &val, const Type &type,
- unsigned align, const std::set<smt::expr> &undef_vars);
+ uint64_t align, const std::set<smt::expr> &undef_vars);
std::pair<StateValue, smt::AndExpr>
- load(const smt::expr &ptr, const Type &type, unsigned align);
+ load(const smt::expr &ptr, const Type &type, uint64_t align);
// raw load; NB: no UB check
Byte raw_load(const Pointer &p, std::set<smt::expr> &undef_vars);
Byte raw_load(const Pointer &p);
void memset(const smt::expr &ptr, const StateValue &val,
- const smt::expr &bytesize, unsigned align,
+ const smt::expr &bytesize, uint64_t align,
const std::set<smt::expr> &undef_vars, bool deref_check = true);
void memcpy(const smt::expr &dst, const smt::expr &src,
- const smt::expr &bytesize, unsigned align_dst, unsigned align_src,
+ const smt::expr &bytesize, uint64_t align_dst, uint64_t align_src,
bool move);
// full copy of memory blocks

MODIFY
ir/pointer.cpp
ir/pointer.cpp
@@ -327,7 +327,7 @@ expr Pointer::isBlockAligned(uint64_t align, bool exact) const {
return exact ? blk_align == bits : blk_align.uge(bits);
}
-expr Pointer::isAligned(unsigned align) {
+expr Pointer::isAligned(uint64_t align) {
if (align == 1)
return true;
@@ -360,7 +360,7 @@ expr Pointer::isAligned(unsigned align) {
static pair<expr, expr> is_dereferenceable(Pointer &p,
const expr &bytes_off,
const expr &bytes,
- unsigned align, bool iswrite) {
+ uint64_t align, bool iswrite) {
expr block_sz = p.blockSizeOffsetT();
expr offset = p.getOffset();
@@ -387,7 +387,7 @@ static pair<expr, expr> is_dereferenceable(Pointer &p,
}
// When bytes is 0, pointer is always derefenceable
-AndExpr Pointer::isDereferenceable(const expr &bytes0, unsigned align,
+AndExpr Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
bool iswrite) {
expr bytes_off = bytes0.zextOrTrunc(bits_for_offset);
expr bytes = bytes0.zextOrTrunc(bits_size_t);
@@ -425,7 +425,7 @@ AndExpr Pointer::isDereferenceable(const expr &bytes0, unsigned align,
return exprs;
}
-AndExpr Pointer::isDereferenceable(uint64_t bytes, unsigned align,
+AndExpr Pointer::isDereferenceable(uint64_t bytes, uint64_t align,
bool iswrite) {
return isDereferenceable(expr::mkUInt(bytes, bits_size_t), align, iswrite);
}

MODIFY
ir/pointer.h
ir/pointer.h
@@ -85,10 +85,10 @@ public:
smt::expr inbounds(bool simplify_ptr = false, bool strict = false);
smt::expr blockAlignment() const; // log(bits)
smt::expr isBlockAligned(uint64_t align, bool exact = false) const;
- smt::expr isAligned(unsigned align);
- smt::AndExpr isDereferenceable(uint64_t bytes, unsigned align,
+ smt::expr isAligned(uint64_t align);
+ smt::AndExpr isDereferenceable(uint64_t bytes, uint64_t align,
bool iswrite = false);
- smt::AndExpr isDereferenceable(const smt::expr &bytes, unsigned align,
+ smt::AndExpr isDereferenceable(const smt::expr &bytes, uint64_t align,
bool iswrite);
void isDisjointOrEqual(const smt::expr &len1, const Pointer &ptr2,
const smt::expr &len2) const;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -85,13 +85,13 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
auto DL() const { return f.getParent()->getDataLayout(); }
template <typename T>
- unsigned alignment(T &i, llvm::Type *ty) const {
+ uint64_t alignment(T &i, llvm::Type *ty) const {
auto a = i.getAlignment();
return a != 0 ? a : DL().getABITypeAlignment(ty);
}
template <typename T>
- unsigned pref_alignment(T &i, llvm::Type *ty) const {
+ uint64_t pref_alignment(T &i, llvm::Type *ty) const {
auto a = i.getAlignment();
return a != 0 ? a : DL().getPrefTypeAlignment(ty);
}

further fixes for 64-bit alignments