Skip to content

Commit

Permalink
make compilalbe & consider when bytes is 0 in memset and memcpy
Browse files Browse the repository at this point in the history
  • Loading branch information
@Dongjoo-Kim
Dongjoo-Kim committed Sep 6, 2019
1 parent 97d9d7f commit 7652232
Show file tree
Hide file tree
Showing 4 changed files with 60 additions and 39 deletions.
63 changes: 42 additions & 21 deletions ir/instr.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1496,51 +1496,72 @@ unique_ptr<Instr> Store::dup(const string &suffix) const {
}


void Memset::print(std::ostream &os) const {
os << "memset " << ptr << " align " << align << ", " << val << ", " << bytes;
vector<Value*> Memset::operands() const {
return { ptr, val, bytes };
}

void Memset::rauw(const Value &what, Value &with) {
RAUW(ptr);
RAUW(val);
RAUW(bytes);
}

void Memset::print(ostream &os) const {
os << "memset " << *ptr << " align " << align << ", " << *val
<< ", " << *bytes;
}

StateValue Memset::toSMT(State &s) const {
// TODO: check following lines are correct
auto &[vptr, np] = s[ptr];
auto &[vbytes, np2] = s[bytes];
s.addUB(np);
s.addUB(np2);
s.getMemory().memset(vptr, s[val], vbytes, align);
auto &[vptr, np] = s[*ptr];
auto &[vbytes, np2] = s[*bytes];
s.addUB(vbytes.ugt(0).implies(np));
s.addUB(vbytes.ugt(0).implies(np2));
s.getMemory().memset(vptr, s[*val], vbytes, align);
return {};
}

expr Memset::getTypeConstraints(const Function &f) const {
return ptr.getType().enforcePtrType() && bytes.getType().enforceIntType();
return ptr->getType().enforcePtrType() && bytes->getType().enforceIntType();
}

unique_ptr<Instr> Memset::dup(const string &suffix) const {
return make_unique<Memset>(ptr, val, bytes, align);
return make_unique<Memset>(*ptr, *val, *bytes, align);
}


vector<Value*> Memcpy::operands() const {
return { dst, src, bytes };
}

void Memcpy::rauw(const Value &what, Value &with) {
RAUW(dst);
RAUW(src);
RAUW(bytes);
}

void Memcpy::print(std::ostream &os) const {
os << "memcpy " << dst << " align " << align_dst << ", " << src << " align " << align_src << ", " << bytes;
void Memcpy::print(ostream &os) const {
os << "memcpy " << *dst << " align " << align_dst << ", " << *src
<< " align " << align_src << ", " << *bytes;
}

StateValue Memcpy::toSMT(State &s) const {
// TODO: check following lines are correct
auto &[vdst, np] = s[dst];
s.addUB(np);
auto &[vsrc, np2] = s[src];
s.addUB(np2);
auto &[vbytes, np3] = s[bytes];
s.addUB(np3);
auto &[vdst, np] = s[*dst];
auto &[vsrc, np2] = s[*src];
auto &[vbytes, np3] = s[*bytes];
s.addUB(vbytes.ugt(0).implies(np));
s.addUB(vbytes.ugt(0).implies(np2));
s.addUB(vbytes.ugt(0).implies(np3));
s.getMemory().memcpy(vdst, vsrc, vbytes, align_dst, align_src);
return {};
}

expr Memcpy::getTypeConstraints(const Function &f) const {
return dst.getType().enforcePtrType() && dst.getType().enforcePtrType() && bytes.getType().enforceIntType();
return dst->getType().enforcePtrType() && dst->getType().enforcePtrType()
&& bytes->getType().enforceIntType();
}

unique_ptr<Instr> Memcpy::dup(const string &suffix) const {
return make_unique<Memcpy>(dst, src, bytes, align_dst, align_src);
return make_unique<Memcpy>(*dst, *src, *bytes, align_dst, align_src);
}

}
12 changes: 8 additions & 4 deletions ir/instr.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -431,13 +431,15 @@ class Store final : public Instr {


class Memset final : public Instr {
Value &ptr, &val, &bytes;
Value *ptr, *val, *bytes;
unsigned align;
public:
Memset(Value &ptr, Value &val, Value &bytes, unsigned align)
: Instr(Type::voidTy, "memset"), ptr(ptr), val(val), bytes(bytes),
: Instr(Type::voidTy, "memset"), ptr(&ptr), val(&val), bytes(&bytes),
align(align) {}

std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints(const Function &f) const override;
Expand All @@ -446,14 +448,16 @@ class Memset final : public Instr {


class Memcpy final : public Instr {
Value &dst, &src, &bytes;
Value *dst, *src, *bytes;
unsigned align_dst, align_src;
public:
Memcpy(Value &dst, Value &src, Value &bytes,
unsigned align_dst, unsigned align_src)
: Instr(Type::voidTy, "memcpy"), dst(dst), src(src), bytes(bytes),
: Instr(Type::voidTy, "memcpy"), dst(&dst), src(&src), bytes(&bytes),
align_dst(align_dst), align_src(align_src) {}

std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints(const Function &f) const override;
Expand Down
16 changes: 10 additions & 6 deletions ir/memory.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -130,16 +130,18 @@ expr Pointer::is_aligned(unsigned align) const {
return true;
}

// When bytes is 0, pointer is always derefenceable
void Pointer::is_dereferenceable(const expr &bytes, unsigned align) {
expr block_sz = block_size();
expr offset = get_offset();

// 1) check that offset is within bounds and that arith doesn't overflow
m.state->addUB((offset + bytes).zextOrTrunc(m.bits_size_t).ule(block_sz));
m.state->addUB(offset.add_no_uoverflow(bytes));
m.state->addUB(bytes.ugt(0).implies(
(offset + bytes).zextOrTrunc(m.bits_size_t).ule(block_sz)));
m.state->addUB(bytes.ugt(0).implies(offset.add_no_uoverflow(bytes)));

// 2) check block's address is aligned
m.state->addUB(is_aligned(align));
m.state->addUB(bytes.ugt(0).implies(is_aligned(align)));

// 3) check block is alive
// TODO
Expand All @@ -156,7 +158,9 @@ static expr disjoint(expr begin1, const expr &len1, expr begin2,
}

// offset + len's overflow is checked by 'is_dereferenceable' at line 139.
void Pointer::is_disjoint(const expr &len1, const Pointer &ptr2, const expr &len2) const {
// When bytes is zero, this is already no ub.
void Pointer::is_disjoint(const expr &len1, const Pointer &ptr2,
const expr &len2) const {
m.state->addUB(get_bid() != ptr2.get_bid() ||
disjoint(get_offset(), len1, ptr2.get_offset(), len2));
}
Expand Down Expand Up @@ -316,7 +320,6 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytes,

void Memory::memcpy(const expr &d, const expr &s, const expr &bytes,
unsigned align_dst, unsigned align_src) {
// TODO: Add ub condition - bytes == 0
Pointer dst(*this, d), src(*this, s);
dst.is_dereferenceable(bytes, align_dst);
src.is_dereferenceable(bytes, align_src);
Expand All @@ -334,7 +337,8 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytes,
Pointer idx(*this, expr::mkVar(name.c_str(), dst.bits()));

expr cond = idx.uge(dst).both() && idx.ult(dst + bytes).both();
expr val = expr::mkIf(cond, blocks_val.load((src + idx.get_offset()).release()), blocks_val.load(idx()));
expr val = expr::mkIf(cond, blocks_val.load((src + idx.get_offset()).release()),
blocks_val.load(idx()));
blocks_val = expr::mkLambda({ idx() }, move(val));
}
}
Expand Down
8 changes: 0 additions & 8 deletions llvm_util/utils.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -347,10 +347,6 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
}

RetTy visitMemSetInst(llvm::MemSetInst &i) {
auto ty = llvm_type2alive(i.getType());
if (ty != &Type::voidTy)
return error(i);

auto ptr = get_operand(i.getOperand(0));
auto val = get_operand(i.getOperand(1));
auto bytes = get_operand(i.getOperand(2));
Expand All @@ -362,10 +358,6 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
}

RetTy visitMemCpyInst(llvm::MemCpyInst &i) {
auto ty = llvm_type2alive(i.getType());
if (ty != &Type::voidTy)
return error(i);

auto dst = get_operand(i.getOperand(0));
auto src = get_operand(i.getOperand(1));
auto bytes = get_operand(i.getOperand(2));
Expand Down

0 comments on commit 7652232

Please sign in to comment.