Skip to content

Commit

Permalink
support indirect calls with ptr attributes
Browse files Browse the repository at this point in the history
  • Loading branch information
nunoplopes committed Sep 18, 2023
1 parent 3bb4af9 commit 834ce61
Show file tree
Hide file tree
Showing 5 changed files with 45 additions and 10 deletions.
10 changes: 5 additions & 5 deletions ir/instr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2359,18 +2359,18 @@ StateValue FnCall::toSMT(State &s) const {
ostringstream fnName_mangled;
if (ptr) {
fnName_mangled << "#indirect_call";
inputs.emplace_back(s.getAndAddPoisonUB(*ptr, true));

Pointer ptr(s.getMemory(), inputs.back().value);
s.addUB(ptr.isDereferenceable(1, 1, false));
Pointer p(s.getMemory(), s.getAndAddPoisonUB(*ptr, true).value);
inputs.emplace_back(p.reprWithoutAttrs(), true);
s.addUB(p.isDereferenceable(1, 1, false));

Function::FnDecl decl;
decl.output = &getType();
for (auto &[arg, params] : args) {
decl.inputs.emplace_back(&arg->getType(), params);
}
s.addUB(expr::mkUF("#fndeclty", { std::move(ptr).release() },
expr::mkUInt(0, 32)) == decl.hash());
s.addUB(expr::mkUF("#fndeclty", { inputs[0].value }, expr::mkUInt(0, 32)) ==
decl.hash());
} else {
fnName_mangled << fnName;
}
Expand Down
11 changes: 9 additions & 2 deletions ir/pointer.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -268,6 +268,14 @@ expr Pointer::blockSizeOffsetT() const {
return bits_for_offset > bits_size_t ? sz.zextOrTrunc(bits_for_offset) : sz;
}

expr Pointer::reprWithoutAttrs() const {
return p.extract(totalBits() - 1, bits_for_ptrattrs);
}

Pointer Pointer::mkPointerFromNoAttrs(const Memory &m, const expr &e) {
return { m, e.concat_zeros(bits_for_ptrattrs) };
}

Pointer Pointer::operator+(const expr &bytes) const {
return { m, getBid(), getOffset() + bytes.zextOrTrunc(bits_for_offset),
getAttrs() };
Expand All @@ -293,8 +301,7 @@ expr Pointer::addNoOverflow(const expr &offset) const {
}

expr Pointer::operator==(const Pointer &rhs) const {
return p.extract(totalBits() - 1, bits_for_ptrattrs) ==
rhs.p.extract(totalBits() - 1, bits_for_ptrattrs);
return reprWithoutAttrs() == rhs.reprWithoutAttrs();
}

expr Pointer::operator!=(const Pointer &rhs) const {
Expand Down
3 changes: 3 additions & 0 deletions ir/pointer.h
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,9 @@ class Pointer {
smt::expr release() && { return std::move(p); }
unsigned bits() const { return p.bits(); }

smt::expr reprWithoutAttrs() const;
static Pointer mkPointerFromNoAttrs(const Memory &m, const smt::expr &e);

Pointer operator+(unsigned) const;
Pointer operator+(const smt::expr &bytes) const;
void operator+=(const smt::expr &bytes);
Expand Down
8 changes: 5 additions & 3 deletions ir/state.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -977,7 +977,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,

auto isgvar = [&](const auto &decl) {
if (auto gv = getFn().getConstant(string_view(decl.name).substr(1)))
return Pointer(memory, fn_ptr).getAddress() ==
return Pointer::mkPointerFromNoAttrs(memory, fn_ptr).getAddress() ==
Pointer(memory, (*this)[*gv].value).getAddress();
return expr();
};
Expand Down Expand Up @@ -1303,8 +1303,10 @@ void State::mkAxioms(State &tgt) {
if (has_indirect_fncalls) {
for (auto &decl : f.getFnDecls()) {
if (auto gv = f.getConstant(string_view(decl.name).substr(1)))
addAxiom(expr::mkUF("#fndeclty", { (*this)[*gv].value },
expr::mkUInt(0, 32)) == decl.hash());
addAxiom(
expr::mkUF("#fndeclty",
{ Pointer(memory, (*this)[*gv].value).reprWithoutAttrs() },
expr::mkUInt(0, 32)) == decl.hash());
}
}
}
Expand Down
23 changes: 23 additions & 0 deletions tests/alive-tv/calls/indirect-call-ptr-attrbiutes.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
define i8 @src(ptr nocapture %0) {
%2 = call i8 %0(ptr null)
ret i8 %2
}

define i8 @tgt(ptr nocapture %0) {
%2 = icmp eq ptr %0, @_Z3fooPi
br i1 %2, label %then, label %else

else:
%3 = call i8 %0(ptr null)
br label %ret

then:
%4 = call i8 @_Z3fooPi(ptr null)
br label %ret

ret:
%5 = phi i8 [ %3, %else ], [ %4, %then ]
ret i8 %5
}

declare i8 @_Z3fooPi(ptr)

0 comments on commit 834ce61

Please sign in to comment.