Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 28 additions & 14 deletions ir/instr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
#include "smt/expr.h"
#include "smt/exprs.h"
#include "smt/solver.h"
#include "state_value.h"
#include "util/compiler.h"
#include "util/config.h"
#include <algorithm>
Expand Down Expand Up @@ -2635,8 +2636,11 @@ InlineAsm::InlineAsm(Type &type, string &&name, const string &asm_str,
std::move(attrs)) {}


ICmp::ICmp(Type &type, string &&name, Cond cond, Value &a, Value &b)
: Instr(type, std::move(name)), a(&a), b(&b), cond(cond), defined(cond != Any) {
ICmp::ICmp(Type &type, string &&name, Cond cond, Value &a, Value &b,
unsigned flags)
: Instr(type, std::move(name)), a(&a), b(&b), cond(cond), flags(flags),
defined(cond != Any) {
assert((flags & SameSign) == flags);
if (!defined)
cond_name = getName() + "_cond";
}
Expand Down Expand Up @@ -2684,34 +2688,36 @@ void ICmp::print(ostream &os) const {
case UGT: condtxt = "ugt "; break;
case Any: condtxt = ""; break;
}
os << getName() << " = icmp " << condtxt << *a << ", " << b->getName();
os << getName() << " = icmp ";
if (flags & SameSign)
os << "samesign ";
os << condtxt << *a << ", " << b->getName();
switch (pcmode) {
case INTEGRAL: break;
case PROVENANCE: os << ", use_provenance"; break;
case OFFSETONLY: os << ", offsetonly"; break;
}
}

static expr build_icmp_chain(const expr &var,
const function<expr(ICmp::Cond)> &fn,
ICmp::Cond cond = ICmp::Any,
expr last = expr()) {
static StateValue build_icmp_chain(const expr &var,
const function<StateValue(ICmp::Cond)> &fn,
ICmp::Cond cond = ICmp::Any,
StateValue last = StateValue()) {
auto old_cond = cond;
cond = ICmp::Cond(cond - 1);

if (old_cond == ICmp::Any)
return build_icmp_chain(var, fn, cond, fn(cond));

auto e = expr::mkIf(var == cond, fn(cond), last);
auto e = StateValue::mkIf(var == cond, fn(cond), last);
return cond == 0 ? e : build_icmp_chain(var, fn, cond, std::move(e));
}

StateValue ICmp::toSMT(State &s) const {
auto &a_eval = s[*a];
auto &b_eval = s[*b];

function<expr(const expr&, const expr&, Cond)> fn =
[&](auto &av, auto &bv, Cond cond) {
auto cmp = [](const expr &av, const expr &bv, Cond cond) {
switch (cond) {
case EQ: return av == bv;
case NE: return av != bv;
Expand All @@ -2729,8 +2735,15 @@ StateValue ICmp::toSMT(State &s) const {
UNREACHABLE();
};

function<StateValue(const expr &, const expr &, Cond)> fn =
[&](auto &av, auto &bv, Cond cond) -> StateValue {
return {cmp(av, bv, cond),
flags & SameSign ? av.sign() == bv.sign() : expr(true)};
};

if (isPtrCmp()) {
fn = [this, &s, fn](const expr &av, const expr &bv, Cond cond) {
fn = [this, &s, fn](const expr &av, const expr &bv,
Cond cond) -> StateValue {
auto &m = s.getMemory();
Pointer lhs(m, av);
Pointer rhs(m, bv);
Expand All @@ -2742,7 +2755,7 @@ StateValue ICmp::toSMT(State &s) const {
return fn(lhs.getAddress(), rhs.getAddress(), cond);
case PROVENANCE:
assert(cond == EQ || cond == NE);
return cond == EQ ? lhs == rhs : lhs != rhs;
return {cond == EQ ? lhs == rhs : lhs != rhs, true};
case OFFSETONLY:
return fn(lhs.getOffset(), rhs.getOffset(), cond);
}
Expand All @@ -2753,7 +2766,8 @@ StateValue ICmp::toSMT(State &s) const {
auto scalar = [&](const StateValue &a, const StateValue &b) -> StateValue {
auto fn2 = [&](Cond c) { return fn(a.value, b.value, c); };
auto v = cond != Any ? fn2(cond) : build_icmp_chain(cond_var(), fn2);
return { v.toBVBool(), a.non_poison && b.non_poison };
return {v.value.toBVBool(),
a.non_poison && b.non_poison && std::move(v.non_poison)};
};

auto &elem_ty = a->getType();
Expand All @@ -2777,7 +2791,7 @@ expr ICmp::getTypeConstraints(const Function &f) const {
}

unique_ptr<Instr> ICmp::dup(Function &f, const string &suffix) const {
return make_unique<ICmp>(getType(), getName() + suffix, cond, *a, *b);
return make_unique<ICmp>(getType(), getName() + suffix, cond, *a, *b, flags);
}


Expand Down
5 changes: 4 additions & 1 deletion ir/instr.h
Original file line number Diff line number Diff line change
Expand Up @@ -418,17 +418,20 @@ class ICmp final : public Instr {
PROVENANCE, // compare pointer provenance & offsets
OFFSETONLY // cmp ofs only. meaningful only when ptrs are based on same obj
};
enum Flags { None = 0, SameSign = 1 << 0 };

private:
Value *a, *b;
std::string cond_name;
Cond cond;
unsigned flags;
bool defined;
PtrCmpMode pcmode = INTEGRAL;
smt::expr cond_var() const;

public:
ICmp(Type &type, std::string &&name, Cond cond, Value &a, Value &b);
ICmp(Type &type, std::string &&name, Cond cond, Value &a, Value &b,
unsigned flags = None);

bool isPtrCmp() const;
PtrCmpMode getPtrCmpMode() const { return pcmode; }
Expand Down
3 changes: 2 additions & 1 deletion llvm_util/llvm2alive.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -507,7 +507,8 @@ class llvm2alive_ : public llvm::InstVisitor<llvm2alive_, unique_ptr<Instr>> {
default:
UNREACHABLE();
}
return make_unique<ICmp>(*ty, value_name(i), cond, *a, *b);
return make_unique<ICmp>(*ty, value_name(i), cond, *a, *b,
i.hasSameSign() ? ICmp::SameSign : ICmp::None);
}

RetTy visitFCmpInst(llvm::FCmpInst &i) {
Expand Down
9 changes: 9 additions & 0 deletions tests/alive-tv/samesign.srctgt.ll
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
define i1 @src(i8 %x, i8 %y) {
%cmp = icmp samesign slt i8 %x, %y
ret i1 %cmp
}

define i1 @tgt(i8 %x, i8 %y) {
%cmp = icmp samesign ult i8 %x, %y
ret i1 %cmp
}