fix crashes when memory ops
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -894,8 +894,50 @@ unique_ptr<Instr> Assume::dup(const string &suffix) const {
}
+void Alloc::print(std::ostream &os) const {
+ os << getName() << " = alloca " << size << ", align " << align;
+}
+
+StateValue Alloc::toSMT(State &s) const {
+ auto &[sz, np] = s[size];
+ s.addUB(np);
+ return { s.getMemory().alloc(sz, align, true), true };
+}
+
+expr Alloc::getTypeConstraints(const Function &f) const {
+ return Value::getTypeConstraints() &&
+ getType().enforcePtrType() &&
+ size.getType().enforceIntType();
+}
+
+unique_ptr<Instr> Alloc::dup(const string &suffix) const {
+ return make_unique<Alloc>(getType(), getName() + suffix, size, align);
+}
+
+
+void Free::print(std::ostream &os) const {
+ os << "free " << ptr;
+}
+
+StateValue Free::toSMT(State &s) const {
+ auto &[p, np] = s[ptr];
+ s.addUB(np);
+ s.getMemory().free(p);
+ return {};
+}
+
+expr Free::getTypeConstraints(const Function &f) const {
+ return ptr.getType().enforcePtrType();
+}
+
+unique_ptr<Instr> Free::dup(const string &suffix) const {
+ return make_unique<Free>(ptr);
+}
+
+
void Load::print(std::ostream &os) const {
- os << getName() << " = load " << getType() << ", " << ptr;
+ os << getName() << " = load " << getType() << ", " << ptr
+ << ", align " << align;
}
StateValue Load::toSMT(State &s) const {
@@ -910,12 +952,12 @@ expr Load::getTypeConstraints(const Function &f) const {
}
unique_ptr<Instr> Load::dup(const string &suffix) const {
- return make_unique<Load>(getType(), getName() + suffix, ptr);
+ return make_unique<Load>(getType(), getName() + suffix, ptr, align);
}
void Store::print(std::ostream &os) const {
- os << "store " << val << ", " << ptr;
+ os << "store " << val << ", " << ptr << ", align " << align;
}
StateValue Store::toSMT(State &s) const {
@@ -926,12 +968,11 @@ StateValue Store::toSMT(State &s) const {
}
expr Store::getTypeConstraints(const Function &f) const {
- return Value::getTypeConstraints() &&
- ptr.getType().enforcePtrType();
+ return ptr.getType().enforcePtrType();
}
unique_ptr<Instr> Store::dup(const string &suffix) const {
- return make_unique<Store>(getName() + suffix, ptr, val);
+ return make_unique<Store>(ptr, val, align);
}
}

MODIFY
ir/instr.h
ir/instr.h
@@ -274,11 +274,39 @@ public:
};
+// TODO: only supports alloca for now
+class Alloc final : public Instr {
+ Value &size;
+ unsigned align;
+public:
+ Alloc(Type &type, std::string &&name, Value &size, unsigned align)
+ : Instr(type, std::move(name)), size(size), align(align) {}
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+ std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+};
+
+
+class Free final : public Instr {
+ Value &ptr;
+public:
+ Free(Value &ptr) : Instr(Type::voidTy, "free"), ptr(ptr) {}
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+ std::unique_ptr<Instr> dup(const std::string &suffix) const override;
+};
+
+
class Load final : public Instr {
Value &ptr;
+ unsigned align;
public:
- Load(Type &type, std::string &&name, Value &ptr)
- : Instr(type, std::move(name)), ptr(ptr) {}
+ Load(Type &type, std::string &&name, Value &ptr, unsigned align)
+ : Instr(type, std::move(name)), ptr(ptr), align(align) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
@@ -289,9 +317,10 @@ public:
class Store final : public Instr {
Value &ptr, &val;
+ unsigned align;
public:
- Store(std::string &&name, Value &ptr, Value &val)
- : Instr(Type::voidTy, std::move(name)), ptr(ptr), val(val) {}
+ Store(Value &ptr, Value &val, unsigned align)
+ : Instr(Type::voidTy, "store"), ptr(ptr), val(val), align(align) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -43,7 +43,7 @@ void Pointer::is_dereferenceable(unsigned bytes) {
expr length = expr::mkUInt(bytes, m.bits_for_offset);
// 1) check that offset is within bounds and that arith doesn't overflow
- m.state.addUB((offset + length).ult(block_sz));
+ m.state.addUB((offset + length).zextOrTrunc(m.bits_size_t).ult(block_sz));
m.state.addUB(offset.add_no_uoverflow(length));
// 2) check block is alive
@@ -62,13 +62,18 @@ Memory::Memory(State &state) : state(state) {
expr::mkUInt(0, byte_size + 1)); // val+poison bit
}
-expr Memory::alloc(const expr &bytes, bool local) {
+expr Memory::alloc(const expr &bytes, unsigned align, bool local) {
Pointer p(*this, last_bid++, local);
+ // TODO: handle alignment
blocks_size = blocks_size.store(p(), bytes.zextOrTrunc(bits_size_t));
memset(p(), { expr::mkUInt(0, byte_size), false }, bytes);
return p();
}
+void Memory::free(const expr &ptr) {
+ // TODO
+}
+
void Memory::store(const expr &p, const StateValue &v) {
unsigned bits = v.value.bits();
unsigned bytes = divide_up(bits, byte_size);

MODIFY
ir/memory.h
ir/memory.h
@@ -50,7 +50,9 @@ class Memory {
public:
Memory(State &state);
- smt::expr alloc(const smt::expr &bytes, bool local);
+ smt::expr alloc(const smt::expr &bytes, unsigned align, bool local);
+ void free(const smt::expr &ptr);
+
void store(const smt::expr &ptr, const StateValue &val);
StateValue load(const smt::expr &ptr, unsigned bits);

MODIFY
ir/type.cpp
ir/type.cpp
@@ -254,7 +254,7 @@ expr PtrType::ASVar() const {
unsigned PtrType::bits() const {
// TODO: make this configurable
- return 64;
+ return 48;
}
expr PtrType::getDummyValue() const {

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -283,18 +283,19 @@ public:
}
RetTy visitLoadInst(llvm::LoadInst &i) {
- // TODO: Add support for isVolatile(), getAlignment(), getOrdering()
+ // TODO: Add support for isVolatile(), getOrdering()
PARSE_UNOP();
- RETURN_IDENTIFIER(make_unique<Load>(*ty, value_name(i), *val));
+ RETURN_IDENTIFIER(make_unique<Load>(*ty, value_name(i), *val,
+ i.getAlignment()));
}
RetTy visitStoreInst(llvm::StoreInst &i) {
- // TODO: Add support for isVolatile(), getAlignment(), getOrdering()
+ // TODO: Add support for isVolatile(), getOrdering()
auto val = get_operand(i.getValueOperand());
auto ptr = get_operand(i.getPointerOperand());
if (!val || !ptr)
return error(i);
- RETURN_IDENTIFIER(make_unique<Store>(value_name(i), *ptr, *val));
+ RETURN_IDENTIFIER(make_unique<Store>(*ptr, *val, i.getAlignment()));
}
RetTy visitPHINode(llvm::PHINode &i) {

fix crashes when memory ops