Skip to content

Commit

Permalink
fix assume alignment UB false positive due to too few offset bits
Browse files Browse the repository at this point in the history
  • Loading branch information
@nunoplopes
nunoplopes committed Dec 12, 2024
1 parent dd2a435 commit e4f7ed1
Show file tree
Hide file tree
Showing 3 changed files with 106 additions and 70 deletions.
51 changes: 48 additions & 3 deletions ir/instr.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,18 @@ using namespace smt;
using namespace util;
using namespace std;

#define DEFINE_AS_RETZERO(cls, method) \
uint64_t cls::method() const { return 0; }
#define DEFINE_AS_RETZEROALIGN(cls, method) \
pair<uint64_t, uint64_t> cls::method() const { return { 0, 1 }; }
#define DEFINE_AS_RETFALSE(cls, method) \
bool cls::method() const { return false; }
#define DEFINE_AS_EMPTYACCESS(cls) \
MemInstr::ByteAccessInfo cls::getByteAccessInfo() const { return {}; }

// log2 of max number of var args per function
#define VARARG_BITS 8

namespace {
struct print_type {
IR::Type &ty;
Expand Down Expand Up @@ -3321,12 +3333,12 @@ bool Return::isTerminator() const {
}

Assume::Assume(Value &cond, Kind kind)
: Instr(Type::voidTy, "assume"), args({&cond}), kind(kind) {
: MemInstr(Type::voidTy, "assume"), args({&cond}), kind(kind) {
assert(kind == AndNonPoison || kind == WellDefined || kind == NonNull);
}

Assume::Assume(vector<Value *> &&args0, Kind kind)
: Instr(Type::voidTy, "assume"), args(std::move(args0)), kind(kind) {
: MemInstr(Type::voidTy, "assume"), args(std::move(args0)), kind(kind) {
switch (kind) {
case AndNonPoison:
case WellDefined:
Expand Down Expand Up @@ -3365,6 +3377,24 @@ bool Assume::hasSideEffects() const {
return true;
}

DEFINE_AS_RETZERO(Assume, getMaxGEPOffset)
DEFINE_AS_RETZEROALIGN(Assume, getMaxAllocSize)
DEFINE_AS_EMPTYACCESS(Assume)

uint64_t Assume::getMaxAccessSize() const {
switch (kind) {
case AndNonPoison:
case WellDefined:
case NonNull:
return 0;
case Align:
case Dereferenceable:
case DereferenceableOrNull:
return getIntOr(*args[1], UINT64_MAX);
}
UNREACHABLE();
}

void Assume::rauw(const Value &what, Value &with) {
for (auto &arg: args)
RAUW(arg);
Expand Down Expand Up @@ -3453,7 +3483,7 @@ unique_ptr<Instr> Assume::dup(Function &f, const string &suffix) const {

AssumeVal::AssumeVal(Type &type, string &&name, Value &val,
vector<Value *> &&args0, Kind kind, bool is_welldefined)
: Instr(type, std::move(name)), val(&val), args(std::move(args0)),
: MemInstr(type, std::move(name)), val(&val), args(std::move(args0)),
kind(kind), is_welldefined(is_welldefined) {
switch (kind) {
case Align:
Expand Down Expand Up @@ -3482,6 +3512,21 @@ bool AssumeVal::hasSideEffects() const {
return false;
}

DEFINE_AS_RETZERO(AssumeVal, getMaxGEPOffset)
DEFINE_AS_RETZEROALIGN(AssumeVal, getMaxAllocSize)
DEFINE_AS_EMPTYACCESS(AssumeVal)

uint64_t AssumeVal::getMaxAccessSize() const {
switch (kind) {
case NonNull:
case Range:
return 0;
case Align:
return getIntOr(*args[0], UINT64_MAX);
}
UNREACHABLE();
}

void AssumeVal::rauw(const Value &what, Value &with) {
RAUW(val);
for (auto &arg: args)
Expand Down
123 changes: 57 additions & 66 deletions ir/instr.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,25 +12,6 @@
#define RAUW(val) \
if (val == &what) \
val = &with
#define DEFINE_AS_RETZERO(cls, method) \
uint64_t cls::method() const { \
return 0; \
}
#define DEFINE_AS_RETZEROALIGN(cls, method) \
pair<uint64_t, uint64_t> cls::method() const { \
return {0, 1}; \
}
#define DEFINE_AS_RETFALSE(cls, method) \
bool cls::method() const { \
return false; \
}
#define DEFINE_AS_EMPTYACCESS(cls) \
MemInstr::ByteAccessInfo cls::getByteAccessInfo() const { \
return {}; \
}

// log2 of max number of var args per function
#define VARARG_BITS 8

namespace IR {

Expand Down Expand Up @@ -664,7 +645,52 @@ class Return final : public Instr {
};


class Assume final : public Instr {
class MemInstr : public Instr {
public:
MemInstr(Type &type, std::string &&name) : Instr(type, std::move(name)) {}

bool hasSideEffects() const override;

// If this instruction allocates a memory block, return its size and
// alignment. Returns 0 if it doesn't allocate anything.
virtual std::pair<uint64_t, uint64_t> getMaxAllocSize() const = 0;

// If this instruction performs load or store, return its max access size.
virtual uint64_t getMaxAccessSize() const = 0;

// If this instruction performs pointer arithmetic, return the absolute
// value of the adding offset.
// If this instruction is accessing the memory, it is okay to return 0.
// ex) Given `store i32 0, ptr`, 0 can be returned, because its access size
// already contains the offset.
virtual uint64_t getMaxGEPOffset() const = 0;

struct ByteAccessInfo {
bool hasIntByteAccess = false;
bool doesPtrLoad = false;
bool doesPtrStore = false;
bool observesAddresses = false;

// The maximum size of a byte that this instruction can support.
// If zero, this instruction does not read/write bytes.
// Otherwise, bytes of a memory can be widened to this size.
unsigned byteSize = 0;

unsigned subByteAccess = 0;

bool doesMemAccess() const { return byteSize; }

static ByteAccessInfo intOnly(unsigned byteSize);
static ByteAccessInfo anyType(unsigned byteSize);
static ByteAccessInfo get(const Type &t, bool store, unsigned align);
static ByteAccessInfo full(unsigned byteSize);
};

virtual ByteAccessInfo getByteAccessInfo() const = 0;
};


class Assume final : public MemInstr {
public:
enum Kind {
AndNonPoison, /// cond should be non-poison and hold
Expand All @@ -683,6 +709,11 @@ class Assume final : public Instr {
Assume(Value &cond, Kind kind);
Assume(std::vector<Value *> &&args, Kind kind);

std::pair<uint64_t, uint64_t> getMaxAllocSize() const override;
uint64_t getMaxAccessSize() const override;
uint64_t getMaxGEPOffset() const override;
ByteAccessInfo getByteAccessInfo() const override;

Kind getKind() const { return kind; }
std::vector<Value*> operands() const override;
bool propagatesPoison() const override;
Expand All @@ -697,7 +728,7 @@ class Assume final : public Instr {


// yields poison if invalid
class AssumeVal final : public Instr {
class AssumeVal final : public MemInstr {
public:
enum Kind {
Align,
Expand All @@ -716,6 +747,11 @@ class AssumeVal final : public Instr {
std::vector<Value *> &&args, Kind kind,
bool is_welldefined = false);

std::pair<uint64_t, uint64_t> getMaxAllocSize() const override;
uint64_t getMaxAccessSize() const override;
uint64_t getMaxGEPOffset() const override;
ByteAccessInfo getByteAccessInfo() const override;

Kind getKind() const { return kind; }
bool isWellDefined() const { return is_welldefined; }
std::vector<Value*> operands() const override;
Expand All @@ -730,51 +766,6 @@ class AssumeVal final : public Instr {
};


class MemInstr : public Instr {
public:
MemInstr(Type &type, std::string &&name) : Instr(type, std::move(name)) {}

bool hasSideEffects() const override;

// If this instruction allocates a memory block, return its size and
// alignment. Returns 0 if it doesn't allocate anything.
virtual std::pair<uint64_t, uint64_t> getMaxAllocSize() const = 0;

// If this instruction performs load or store, return its max access size.
virtual uint64_t getMaxAccessSize() const = 0;

// If this instruction performs pointer arithmetic, return the absolute
// value of the adding offset.
// If this instruction is accessing the memory, it is okay to return 0.
// ex) Given `store i32 0, ptr`, 0 can be returned, because its access size
// already contains the offset.
virtual uint64_t getMaxGEPOffset() const = 0;

struct ByteAccessInfo {
bool hasIntByteAccess = false;
bool doesPtrLoad = false;
bool doesPtrStore = false;
bool observesAddresses = false;

// The maximum size of a byte that this instruction can support.
// If zero, this instruction does not read/write bytes.
// Otherwise, bytes of a memory can be widened to this size.
unsigned byteSize = 0;

unsigned subByteAccess = 0;

bool doesMemAccess() const { return byteSize; }

static ByteAccessInfo intOnly(unsigned byteSize);
static ByteAccessInfo anyType(unsigned byteSize);
static ByteAccessInfo get(const Type &t, bool store, unsigned align);
static ByteAccessInfo full(unsigned byteSize);
};

virtual ByteAccessInfo getByteAccessInfo() const = 0;
};


class Alloc final : public MemInstr {
Value *size, *mul;
uint64_t align;
Expand Down
2 changes: 1 addition & 1 deletion ir/x86_intrinsics.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -269,7 +269,7 @@ StateValue X86IntrinBinOp::toSMT(State &s) const {
case x86_avx512_psllv_w_256:
case x86_avx512_psllv_w_512:
fn = [](auto a, auto b) {
return expr::mkIf(b.uge( a.bits()), expr::mkUInt(0, a), a << b);
return expr::mkIf(b.uge(a.bits()), expr::mkUInt(0, a), a << b);
};
break;
case x86_sse2_pmulh_w:
Expand Down

0 comments on commit e4f7ed1

Please sign in to comment.