Skip to content

Commit 10c54db

Browse files
nunoplopesnunoplopes
committed
further fixes for 64-bit alignments
1 parent ec634ba commit 10c54db

File tree

7 files changed

+57
-57
lines changed

7 files changed

+57
-57
lines changed

‎ir/instr.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2704,7 +2704,7 @@ bool Malloc::canFree() const {
27042704
return ptr != nullptr;
27052705
}
27062706

2707-
unsigned Malloc::getAlign() const {
2707+
uint64_t Malloc::getAlign() const {
27082708
return align ? align : heap_block_alignment;
27092709
}
27102710

@@ -2804,7 +2804,7 @@ Calloc::ByteAccessInfo Calloc::getByteAccessInfo() const {
28042804
return info;
28052805
}
28062806

2807-
unsigned Calloc::getAlign() const {
2807+
uint64_t Calloc::getAlign() const {
28082808
return align ? align : heap_block_alignment;
28092809
}
28102810

‎ir/instr.h‎

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -473,10 +473,10 @@ class MemInstr : public Instr {
473473

474474
class Alloc final : public MemInstr {
475475
Value *size, *mul;
476-
unsigned align;
476+
uint64_t align;
477477
bool initially_dead = false;
478478
public:
479-
Alloc(Type &type, std::string &&name, Value &size, Value *mul, unsigned align)
479+
Alloc(Type &type, std::string &&name, Value &size, Value *mul, uint64_t align)
480480
: MemInstr(type, std::move(name)), size(&size), mul(mul), align(align) {}
481481

482482
Value& getSize() const { return *size; }
@@ -501,23 +501,23 @@ class Alloc final : public MemInstr {
501501

502502
class Malloc final : public MemInstr {
503503
Value *ptr = nullptr, *size;
504-
unsigned align;
504+
uint64_t align;
505505
// Is this malloc (or equivalent operation, like new()) never returning
506506
// null?
507507
bool isNonNull = false;
508508

509509
public:
510510
Malloc(Type &type, std::string &&name, Value &size, bool isNonNull,
511-
unsigned align = 0)
511+
uint64_t align = 0)
512512
: MemInstr(type, std::move(name)), size(&size), align(align),
513513
isNonNull(isNonNull) {}
514514

515515
Malloc(Type &type, std::string &&name, Value &ptr, Value &size,
516-
unsigned align = 0)
516+
uint64_t align = 0)
517517
: MemInstr(type, std::move(name)), ptr(&ptr), size(&size), align(align) {}
518518

519519
Value& getSize() const { return *size; }
520-
unsigned getAlign() const;
520+
uint64_t getAlign() const;
521521
bool isRealloc() const { return ptr != nullptr; }
522522

523523
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
@@ -537,15 +537,15 @@ class Malloc final : public MemInstr {
537537

538538
class Calloc final : public MemInstr {
539539
Value *num, *size;
540-
unsigned align;
540+
uint64_t align;
541541
public:
542542
Calloc(Type &type, std::string &&name, Value &num, Value &size,
543-
unsigned align = 0)
543+
uint64_t align = 0)
544544
: MemInstr(type, std::move(name)), num(&num), size(&size), align(align) {}
545545

546546
Value& getNum() const { return *num; }
547547
Value& getSize() const { return *size; }
548-
unsigned getAlign() const;
548+
uint64_t getAlign() const;
549549

550550
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
551551
uint64_t getMaxAccessSize() const override;
@@ -635,13 +635,13 @@ class GEP final : public MemInstr {
635635

636636
class Load final : public MemInstr {
637637
Value *ptr;
638-
unsigned align;
638+
uint64_t align;
639639
public:
640-
Load(Type &type, std::string &&name, Value &ptr, unsigned align)
640+
Load(Type &type, std::string &&name, Value &ptr, uint64_t align)
641641
: MemInstr(type, std::move(name)), ptr(&ptr), align(align) {}
642642

643643
Value& getPtr() const { return *ptr; }
644-
unsigned getAlign() const { return align; }
644+
uint64_t getAlign() const { return align; }
645645

646646
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
647647
uint64_t getMaxAccessSize() const override;
@@ -660,14 +660,14 @@ class Load final : public MemInstr {
660660

661661
class Store final : public MemInstr {
662662
Value *ptr, *val;
663-
unsigned align;
663+
uint64_t align;
664664
public:
665-
Store(Value &ptr, Value &val, unsigned align)
665+
Store(Value &ptr, Value &val, uint64_t align)
666666
: MemInstr(Type::voidTy, "store"), ptr(&ptr), val(&val), align(align) {}
667667

668668
Value& getValue() const { return *val; }
669669
Value& getPtr() const { return *ptr; }
670-
unsigned getAlign() const { return align; }
670+
uint64_t getAlign() const { return align; }
671671

672672
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
673673
uint64_t getMaxAccessSize() const override;
@@ -687,14 +687,14 @@ class Store final : public MemInstr {
687687

688688
class Memset final : public MemInstr {
689689
Value *ptr, *val, *bytes;
690-
unsigned align;
690+
uint64_t align;
691691
public:
692-
Memset(Value &ptr, Value &val, Value &bytes, unsigned align)
692+
Memset(Value &ptr, Value &val, Value &bytes, uint64_t align)
693693
: MemInstr(Type::voidTy, "memset"), ptr(&ptr), val(&val), bytes(&bytes),
694694
align(align) {}
695695

696696
Value& getBytes() const { return *bytes; }
697-
unsigned getAlign() const { return align; }
697+
uint64_t getAlign() const { return align; }
698698

699699
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
700700
uint64_t getMaxAccessSize() const override;
@@ -733,17 +733,17 @@ class FillPoison final : public MemInstr {
733733

734734
class Memcpy final : public MemInstr {
735735
Value *dst, *src, *bytes;
736-
unsigned align_dst, align_src;
736+
uint64_t align_dst, align_src;
737737
bool move;
738738
public:
739739
Memcpy(Value &dst, Value &src, Value &bytes,
740-
unsigned align_dst, unsigned align_src, bool move)
740+
uint64_t align_dst, uint64_t align_src, bool move)
741741
: MemInstr(Type::voidTy, "memcpy"), dst(&dst), src(&src), bytes(&bytes),
742742
align_dst(align_dst), align_src(align_src), move(move) {}
743743

744744
Value& getBytes() const { return *bytes; }
745-
unsigned getSrcAlign() const { return align_src; }
746-
unsigned getDstAlign() const { return align_dst; }
745+
uint64_t getSrcAlign() const { return align_src; }
746+
uint64_t getDstAlign() const { return align_dst; }
747747

748748
std::pair<uint64_t, unsigned> getMaxAllocSize() const override;
749749
uint64_t getMaxAccessSize() const override;

‎ir/memory.cpp‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -712,7 +712,7 @@ expr Memory::isBlockAlive(const expr &bid, bool local) const {
712712
}
713713

714714
bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
715-
unsigned bytes, unsigned align, bool write) const {
715+
unsigned bytes, uint64_t align, bool write) const {
716716
if (local && bid0 >= next_local_bid)
717717
return false;
718718

@@ -754,7 +754,7 @@ bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
754754
}
755755

756756
Memory::AliasSet Memory::computeAliasing(const Pointer &ptr, unsigned bytes,
757-
unsigned align, bool write) const {
757+
uint64_t align, bool write) const {
758758
assert(bytes % (bits_byte/8) == 0);
759759

760760
AliasSet aliasing(*this);
@@ -821,7 +821,7 @@ Memory::AliasSet Memory::computeAliasing(const Pointer &ptr, unsigned bytes,
821821
}
822822

823823
template <typename Fn>
824-
void Memory::access(const Pointer &ptr, unsigned bytes, unsigned align,
824+
void Memory::access(const Pointer &ptr, unsigned bytes, uint64_t align,
825825
bool write, Fn &fn) {
826826
auto aliasing = computeAliasing(ptr, bytes, align, write);
827827
unsigned has_local = aliasing.numMayAlias(true);
@@ -861,7 +861,7 @@ void Memory::access(const Pointer &ptr, unsigned bytes, unsigned align,
861861
}
862862

863863
vector<Byte> Memory::load(const Pointer &ptr, unsigned bytes, set<expr> &undef,
864-
unsigned align, bool left2right, DataType type) {
864+
uint64_t align, bool left2right, DataType type) {
865865
if (bytes == 0)
866866
return {};
867867

@@ -921,7 +921,7 @@ Memory::DataType Memory::data_type(const vector<pair<unsigned, expr>> &data,
921921

922922
void Memory::store(const Pointer &ptr,
923923
const vector<pair<unsigned, expr>> &data,
924-
const set<expr> &undef, unsigned align) {
924+
const set<expr> &undef, uint64_t align) {
925925
if (data.empty())
926926
return;
927927

@@ -976,7 +976,7 @@ void Memory::store(const Pointer &ptr,
976976

977977
void Memory::storeLambda(const Pointer &ptr, const expr &offset,
978978
const expr &bytes, const expr &val,
979-
const set<expr> &undef, unsigned align) {
979+
const set<expr> &undef, uint64_t align) {
980980
assert(!state->isInitializationPhase());
981981
// offset in [ptr, ptr+sz)
982982
auto offset_cond = offset.uge(ptr.getShortOffset()) &&
@@ -1480,7 +1480,7 @@ void Memory::mkLocalDisjAddrAxioms(const expr &allocated, const expr &short_bid,
14801480
}
14811481

14821482
pair<expr, expr>
1483-
Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
1483+
Memory::alloc(const expr &size, uint64_t align, BlockKind blockKind,
14841484
const expr &precond, const expr &nonnull,
14851485
optional<unsigned> bidopt, unsigned *bid_out) {
14861486
assert(!memory_unused());
@@ -1642,7 +1642,7 @@ void Memory::store(const StateValue &v, const Type &type, unsigned offset0,
16421642
}
16431643

16441644
void Memory::store(const expr &p, const StateValue &v, const Type &type,
1645-
unsigned align, const set<expr> &undef_vars) {
1645+
uint64_t align, const set<expr> &undef_vars) {
16461646
assert(!memory_unused());
16471647
Pointer ptr(*this, p);
16481648

@@ -1656,7 +1656,7 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
16561656
}
16571657

16581658
StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
1659-
unsigned align) {
1659+
uint64_t align) {
16601660
unsigned bytecount = getStoreByteSize(type);
16611661

16621662
auto aty = type.getAsAggregateType();
@@ -1712,7 +1712,7 @@ StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
17121712
}
17131713

17141714
pair<StateValue, AndExpr>
1715-
Memory::load(const expr &p, const Type &type, unsigned align) {
1715+
Memory::load(const expr &p, const Type &type, uint64_t align) {
17161716
assert(!memory_unused());
17171717

17181718
Pointer ptr(*this, p);
@@ -1732,7 +1732,7 @@ Byte Memory::raw_load(const Pointer &p) {
17321732
}
17331733

17341734
void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
1735-
unsigned align, const set<expr> &undef_vars,
1735+
uint64_t align, const set<expr> &undef_vars,
17361736
bool deref_check) {
17371737
assert(!memory_unused());
17381738
assert(!val.isValid() || val.bits() == 8);
@@ -1766,7 +1766,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
17661766
}
17671767

17681768
void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
1769-
unsigned align_dst, unsigned align_src, bool is_move) {
1769+
uint64_t align_dst, uint64_t align_src, bool is_move) {
17701770
assert(!memory_unused());
17711771
unsigned bytesz = bits_byte / 8;
17721772

‎ir/memory.h‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -166,34 +166,34 @@ class Memory {
166166
void mkNonlocalValAxioms(bool skip_consts);
167167

168168
bool mayalias(bool local, unsigned bid, const smt::expr &offset,
169-
unsigned bytes, unsigned align, bool write) const;
169+
unsigned bytes, uint64_t align, bool write) const;
170170

171-
AliasSet computeAliasing(const Pointer &ptr, unsigned btyes, unsigned align,
171+
AliasSet computeAliasing(const Pointer &ptr, unsigned btyes, uint64_t align,
172172
bool write) const;
173173

174174
template <typename Fn>
175-
void access(const Pointer &ptr, unsigned btyes, unsigned align, bool write,
175+
void access(const Pointer &ptr, unsigned btyes, uint64_t align, bool write,
176176
Fn &fn);
177177

178178
std::vector<Byte> load(const Pointer &ptr, unsigned bytes,
179-
std::set<smt::expr> &undef, unsigned align,
179+
std::set<smt::expr> &undef, uint64_t align,
180180
bool left2right = true,
181181
DataType type = DATA_ANY);
182182
StateValue load(const Pointer &ptr, const Type &type,
183-
std::set<smt::expr> &undef, unsigned align);
183+
std::set<smt::expr> &undef, uint64_t align);
184184

185185
DataType data_type(const std::vector<std::pair<unsigned, smt::expr>> &data,
186186
bool full_store) const;
187187

188188
void store(const Pointer &ptr,
189189
const std::vector<std::pair<unsigned, smt::expr>> &data,
190-
const std::set<smt::expr> &undef, unsigned align);
190+
const std::set<smt::expr> &undef, uint64_t align);
191191
void store(const StateValue &val, const Type &type, unsigned offset,
192192
std::vector<std::pair<unsigned, smt::expr>> &data);
193193

194194
void storeLambda(const Pointer &ptr, const smt::expr &offset,
195195
const smt::expr &bytes, const smt::expr &val,
196-
const std::set<smt::expr> &undef, unsigned align);
196+
const std::set<smt::expr> &undef, uint64_t align);
197197

198198
smt::expr blockValRefined(const Memory &other, unsigned bid, bool local,
199199
const smt::expr &offset,
@@ -271,7 +271,7 @@ class Memory {
271271
// In this case, it is caller's responsibility to give a unique bid.
272272
// The newly assigned bid is stored to bid_out if bid_out != nullptr.
273273
// Returns <pointer if allocated, allocated?>
274-
std::pair<smt::expr, smt::expr> alloc(const smt::expr &size, unsigned align,
274+
std::pair<smt::expr, smt::expr> alloc(const smt::expr &size, uint64_t align,
275275
BlockKind blockKind, const smt::expr &precond = true,
276276
const smt::expr &nonnull = false,
277277
std::optional<unsigned> bid = std::nullopt, unsigned *bid_out = nullptr);
@@ -285,19 +285,19 @@ class Memory {
285285

286286
static unsigned getStoreByteSize(const Type &ty);
287287
void store(const smt::expr &ptr, const StateValue &val, const Type &type,
288-
unsigned align, const std::set<smt::expr> &undef_vars);
288+
uint64_t align, const std::set<smt::expr> &undef_vars);
289289
std::pair<StateValue, smt::AndExpr>
290-
load(const smt::expr &ptr, const Type &type, unsigned align);
290+
load(const smt::expr &ptr, const Type &type, uint64_t align);
291291

292292
// raw load; NB: no UB check
293293
Byte raw_load(const Pointer &p, std::set<smt::expr> &undef_vars);
294294
Byte raw_load(const Pointer &p);
295295

296296
void memset(const smt::expr &ptr, const StateValue &val,
297-
const smt::expr &bytesize, unsigned align,
297+
const smt::expr &bytesize, uint64_t align,
298298
const std::set<smt::expr> &undef_vars, bool deref_check = true);
299299
void memcpy(const smt::expr &dst, const smt::expr &src,
300-
const smt::expr &bytesize, unsigned align_dst, unsigned align_src,
300+
const smt::expr &bytesize, uint64_t align_dst, uint64_t align_src,
301301
bool move);
302302

303303
// full copy of memory blocks

‎ir/pointer.cpp‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -327,7 +327,7 @@ expr Pointer::isBlockAligned(uint64_t align, bool exact) const {
327327
return exact ? blk_align == bits : blk_align.uge(bits);
328328
}
329329

330-
expr Pointer::isAligned(unsigned align) {
330+
expr Pointer::isAligned(uint64_t align) {
331331
if (align == 1)
332332
return true;
333333

@@ -360,7 +360,7 @@ expr Pointer::isAligned(unsigned align) {
360360
static pair<expr, expr> is_dereferenceable(Pointer &p,
361361
const expr &bytes_off,
362362
const expr &bytes,
363-
unsigned align, bool iswrite) {
363+
uint64_t align, bool iswrite) {
364364
expr block_sz = p.blockSizeOffsetT();
365365
expr offset = p.getOffset();
366366

@@ -387,7 +387,7 @@ static pair<expr, expr> is_dereferenceable(Pointer &p,
387387
}
388388

389389
// When bytes is 0, pointer is always derefenceable
390-
AndExpr Pointer::isDereferenceable(const expr &bytes0, unsigned align,
390+
AndExpr Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
391391
bool iswrite) {
392392
expr bytes_off = bytes0.zextOrTrunc(bits_for_offset);
393393
expr bytes = bytes0.zextOrTrunc(bits_size_t);
@@ -425,7 +425,7 @@ AndExpr Pointer::isDereferenceable(const expr &bytes0, unsigned align,
425425
return exprs;
426426
}
427427

428-
AndExpr Pointer::isDereferenceable(uint64_t bytes, unsigned align,
428+
AndExpr Pointer::isDereferenceable(uint64_t bytes, uint64_t align,
429429
bool iswrite) {
430430
return isDereferenceable(expr::mkUInt(bytes, bits_size_t), align, iswrite);
431431
}

‎ir/pointer.h‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -85,10 +85,10 @@ class Pointer {
8585
smt::expr inbounds(bool simplify_ptr = false, bool strict = false);
8686
smt::expr blockAlignment() const; // log(bits)
8787
smt::expr isBlockAligned(uint64_t align, bool exact = false) const;
88-
smt::expr isAligned(unsigned align);
89-
smt::AndExpr isDereferenceable(uint64_t bytes, unsigned align,
88+
smt::expr isAligned(uint64_t align);
89+
smt::AndExpr isDereferenceable(uint64_t bytes, uint64_t align,
9090
bool iswrite = false);
91-
smt::AndExpr isDereferenceable(const smt::expr &bytes, unsigned align,
91+
smt::AndExpr isDereferenceable(const smt::expr &bytes, uint64_t align,
9292
bool iswrite);
9393
void isDisjointOrEqual(const smt::expr &len1, const Pointer &ptr2,
9494
const smt::expr &len2) const;

0 commit comments

Comments
 (0)