From faf59b5d111b06c8edb87d073412484d59fc7b59 Mon Sep 17 00:00:00 2001 From: Yingwei Zheng Date: Wed, 16 Oct 2024 16:37:55 +0800 Subject: [PATCH] Add support for `samesign` flag (#1098) --- ir/instr.cpp | 42 ++++++++++++++++++++----------- ir/instr.h | 5 +++- llvm_util/llvm2alive.cpp | 3 ++- tests/alive-tv/samesign.srctgt.ll | 9 +++++++ 4 files changed, 43 insertions(+), 16 deletions(-) create mode 100644 tests/alive-tv/samesign.srctgt.ll diff --git a/ir/instr.cpp b/ir/instr.cpp index 6cd46311e..1a40398c7 100644 --- a/ir/instr.cpp +++ b/ir/instr.cpp @@ -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 @@ -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"; } @@ -2684,7 +2688,10 @@ 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; @@ -2692,17 +2699,17 @@ void ICmp::print(ostream &os) const { } } -static expr build_icmp_chain(const expr &var, - const function &fn, - ICmp::Cond cond = ICmp::Any, - expr last = expr()) { +static StateValue build_icmp_chain(const expr &var, + const function &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)); } @@ -2710,8 +2717,7 @@ StateValue ICmp::toSMT(State &s) const { auto &a_eval = s[*a]; auto &b_eval = s[*b]; - function 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; @@ -2729,8 +2735,15 @@ StateValue ICmp::toSMT(State &s) const { UNREACHABLE(); }; + function 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); @@ -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); } @@ -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(); @@ -2777,7 +2791,7 @@ expr ICmp::getTypeConstraints(const Function &f) const { } unique_ptr ICmp::dup(Function &f, const string &suffix) const { - return make_unique(getType(), getName() + suffix, cond, *a, *b); + return make_unique(getType(), getName() + suffix, cond, *a, *b, flags); } diff --git a/ir/instr.h b/ir/instr.h index de1ae8f3b..4f89aa930 100644 --- a/ir/instr.h +++ b/ir/instr.h @@ -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; } diff --git a/llvm_util/llvm2alive.cpp b/llvm_util/llvm2alive.cpp index 336fbf9e1..911ba9e31 100644 --- a/llvm_util/llvm2alive.cpp +++ b/llvm_util/llvm2alive.cpp @@ -507,7 +507,8 @@ class llvm2alive_ : public llvm::InstVisitor> { default: UNREACHABLE(); } - return make_unique(*ty, value_name(i), cond, *a, *b); + return make_unique(*ty, value_name(i), cond, *a, *b, + i.hasSameSign() ? ICmp::SameSign : ICmp::None); } RetTy visitFCmpInst(llvm::FCmpInst &i) { diff --git a/tests/alive-tv/samesign.srctgt.ll b/tests/alive-tv/samesign.srctgt.ll new file mode 100644 index 000000000..bbbb64e84 --- /dev/null +++ b/tests/alive-tv/samesign.srctgt.ll @@ -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 +}