From e6d8696e2e6aeda0e24d3628ccd50b8d64687df9 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Fri, 15 Jan 2021 18:52:38 -0700 Subject: [PATCH 1/3] Refactor RewriteBitwiseOps The refactoring consists of two parts: 1. improve code structure, in particular modularize special case handling 2. add a special case for &(-2**n) --- include/smack/RewriteBitwiseOps.h | 18 ++ lib/smack/RewriteBitwiseOps.cpp | 232 +++++++++++---------- test/c/special/bitwise_constant_and.c | 64 ++++++ test/c/special/bitwise_constant_and_fail.c | 67 ++++++ 4 files changed, 268 insertions(+), 113 deletions(-) create mode 100644 test/c/special/bitwise_constant_and.c create mode 100644 test/c/special/bitwise_constant_and_fail.c diff --git a/include/smack/RewriteBitwiseOps.h b/include/smack/RewriteBitwiseOps.h index da009d209..8626491fa 100644 --- a/include/smack/RewriteBitwiseOps.h +++ b/include/smack/RewriteBitwiseOps.h @@ -6,15 +6,33 @@ #include "llvm/IR/Module.h" #include "llvm/Pass.h" +#include namespace smack { class RewriteBitwiseOps : public llvm::ModulePass { public: + enum class SpecialCase { + Shr, // Right shift + Shl, // Left shift + AndPoTMO, // And power of 2 minus 1 + AndNPoT // And negative power of 2 + }; static char ID; // Pass identification, replacement for typeid RewriteBitwiseOps() : llvm::ModulePass(ID) {} virtual llvm::StringRef getPassName() const; virtual bool runOnModule(llvm::Module &m); + +private: + boost::optional getSpecialCase(llvm::Instruction *i); + static llvm::Instruction *rewriteShift(llvm::Instruction::BinaryOps, + llvm::Instruction *); + static llvm::Instruction *rewriteShr(llvm::Instruction *); + static llvm::Instruction *rewriteShl(llvm::Instruction *); + static llvm::Instruction *rewriteAndPoTMO(llvm::Instruction *); + static llvm::Instruction *rewriteAndNPot(llvm::Instruction *); + llvm::Instruction *rewriteSpecialCase(SpecialCase, llvm::Instruction *); + boost::optional rewriteGeneralCase(llvm::Instruction *); }; } // namespace smack diff --git a/lib/smack/RewriteBitwiseOps.cpp b/lib/smack/RewriteBitwiseOps.cpp index 5c25d2922..b0ac37a92 100644 --- a/lib/smack/RewriteBitwiseOps.cpp +++ b/lib/smack/RewriteBitwiseOps.cpp @@ -18,143 +18,149 @@ #include "llvm/Support/raw_ostream.h" #include "llvm/Transforms/Utils/BasicBlockUtils.h" #include +#include +#include namespace smack { using namespace llvm; +using SC = RewriteBitwiseOps::SpecialCase; unsigned getOpBitWidth(const Value *V) { const Type *T = V->getType(); - const IntegerType *iType = cast(T); + const IntegerType *iType = cast(T); return iType->getBitWidth(); } -Optional getConstantIntValue(const Value *V) { - if (const ConstantInt *ci = dyn_cast(V)) { - const APInt &value = ci->getValue(); - return Optional(value); - } else { - return Optional(); +int getConstOpId(const Instruction *i) { + return llvm::isa(i->getOperand(1)) + ? 1 + : (llvm::isa(i->getOperand(0)) ? 0 : -1); +} + +Instruction *RewriteBitwiseOps::rewriteShift(Instruction::BinaryOps newOp, + Instruction *i) { + auto ci = llvm::cast(i->getOperand(1)); + auto lhs = i->getOperand(0); + unsigned bitWidth = getOpBitWidth(lhs); + APInt rhsVal = APInt(bitWidth, "1", 10); + const APInt &value = ci->getValue(); + rhsVal <<= value; + Value *rhs = ConstantInt::get(ci->getType(), rhsVal); + return BinaryOperator::Create(newOp, lhs, rhs, "", i); +} + +Instruction *RewriteBitwiseOps::rewriteShr(Instruction *i) { + // Shifting right by a constant amount is equivalent to dividing by + // 2^amount + return rewriteShift(Instruction::SDiv, i); +} + +Instruction *RewriteBitwiseOps::rewriteShl(Instruction *i) { + // Shifting left by a constant amount is equivalent to dividing by + // 2^amount + return rewriteShift(Instruction::Mul, i); +} + +Instruction *RewriteBitwiseOps::rewriteAndPoTMO(Instruction *i) { + // If the operation is a bit-wise `and' and the mask variable is + // constant, it may be possible to replace this operation with a + // remainder operation. If one argument has only ones, and they're only + // in the least significant bit, then the mask is 2^(number of ones) + // - 1. This is equivalent to the remainder when dividing by 2^(number + // of ones). + // Zvonimir: Right-side constants do not work well on SVCOMP + // } else if (isConstantInt(args[1])) { + // maskOperand = 1; + // } + auto constOpId = getConstOpId(i); + auto constVal = + (llvm::cast(i->getOperand(constOpId)))->getValue(); + auto lhs = i->getOperand(1 - constOpId); + Value *rhs = ConstantInt::get(i->getContext(), constVal + 1); + return BinaryOperator::Create(Instruction::URem, lhs, rhs, "", i); +} + +Instruction *RewriteBitwiseOps::rewriteAndNPot(Instruction *i) { + // E.g., rewrite ``x && -32'' into ``x - x % 32'' + auto constOpId = getConstOpId(i); + auto constVal = + (llvm::cast(i->getOperand(constOpId)))->getValue(); + auto lhs = i->getOperand(1 - constOpId); + auto rem = BinaryOperator::Create( + Instruction::URem, lhs, ConstantInt::get(i->getContext(), 0 - constVal), + "", i); + return BinaryOperator::Create(Instruction::Sub, lhs, rem, "", i); +} + +boost::optional RewriteBitwiseOps::getSpecialCase(Instruction *i) { + if (auto bi = dyn_cast(i)) { + auto opcode = bi->getOpcode(); + if (bi->isShift() && llvm::isa(bi->getOperand(1))) { + if (opcode == Instruction::AShr || opcode == Instruction::LShr) + return SC::Shr; + else if (opcode == Instruction::Shl) + return SC::Shl; + } else if (opcode == Instruction::And) { + auto constOpId = getConstOpId(i); + if (constOpId >= 0) { + auto val = + (llvm::cast(i->getOperand(constOpId)))->getValue(); + if ((val + 1).isPowerOf2()) + return SC::AndPoTMO; + else if ((0 - val).isPowerOf2()) + return SC::AndNPoT; + } + } } + return boost::none; +} + +Instruction *RewriteBitwiseOps::rewriteSpecialCase(SC sc, Instruction *i) { + static std::unordered_map table{ + {SC::Shr, &rewriteShr}, + {SC::Shl, &rewriteShl}, + {SC::AndPoTMO, &rewriteAndPoTMO}, + {SC::AndNPoT, &rewriteAndNPot}}; + return table[sc](i); } -bool isConstantInt(const Value *V) { - Optional constantValue = getConstantIntValue(V); - return constantValue.hasValue() && (*constantValue + 1).isPowerOf2(); +boost::optional +RewriteBitwiseOps::rewriteGeneralCase(Instruction *i) { + auto opCode = i->getOpcode(); + if (opCode != Instruction::And && opCode != Instruction::Or) + return boost::none; + unsigned bitWidth = getOpBitWidth(i); + if (bitWidth > 64 || bitWidth < 8 || (bitWidth & (bitWidth - 1))) + return boost::none; + std::string func = + std::string("__SMACK_") + i->getOpcodeName() + std::to_string(bitWidth); + Function *co = i->getModule()->getFunction(func); + assert(co != NULL && "Function __SMACK_[and|or] should be present."); + std::vector args; + args.push_back(i->getOperand(0)); + args.push_back(i->getOperand(1)); + return CallInst::Create(co, args, "", i); } bool RewriteBitwiseOps::runOnModule(Module &m) { - std::vector instsFrom; - std::vector instsTo; + std::vector> insts; for (auto &F : m) { if (Naming::isSmackName(F.getName())) continue; for (inst_iterator I = inst_begin(F), E = inst_end(F); I != E; ++I) { - if (I->isShift()) { - BinaryOperator *bi = cast(&*I); - Value *amount = bi->getOperand(1); - - if (ConstantInt *ci = dyn_cast(amount)) { - unsigned opcode = bi->getOpcode(); - Instruction::BinaryOps op; - if (opcode == Instruction::AShr || opcode == Instruction::LShr) { - // Shifting right by a constant amount is equivalent to dividing by - // 2^amount - op = Instruction::SDiv; - } else if (opcode == Instruction::Shl) { - // Shifting left by a constant amount is equivalent to dividing by - // 2^amount - op = Instruction::Mul; - } - - auto lhs = bi->getOperand(0); - unsigned bitWidth = getOpBitWidth(lhs); - APInt rhsVal = APInt(bitWidth, "1", 10); - const APInt &value = ci->getValue(); - rhsVal <<= value; - Value *rhs = ConstantInt::get(ci->getType(), rhsVal); - Instruction *replacement = BinaryOperator::Create(op, lhs, rhs, ""); - instsFrom.push_back(&*I); - instsTo.push_back(replacement); - } - } else if (I->isBitwiseLogicOp()) { - // If the operation is a bit-wise `and' and the mask variable is - // constant, it may be possible to replace this operation with a - // remainder operation. If one argument has only ones, and they're only - // in the least significant bit, then the mask is 2^(number of ones) - // - 1. This is equivalent to the remainder when dividing by 2^(number - // of ones). - BinaryOperator *bi = cast(&*I); - unsigned opcode = bi->getOpcode(); - if (opcode == Instruction::And) { - Value *args[] = {bi->getOperand(0), bi->getOperand(1)}; - int maskOperand = -1; - - if (isConstantInt(args[0])) { - maskOperand = 0; - } - // Zvonimir: Right-side constants do not work well on SVCOMP - // } else if (isConstantInt(args[1])) { - // maskOperand = 1; - // } - - if (maskOperand == -1) { - unsigned bitWidth = getOpBitWidth(&*I); - Function *co; - if (bitWidth == 64) { - co = m.getFunction("__SMACK_and64"); - } else if (bitWidth == 32) { - co = m.getFunction("__SMACK_and32"); - } else if (bitWidth == 16) { - co = m.getFunction("__SMACK_and16"); - } else if (bitWidth == 8) { - co = m.getFunction("__SMACK_and8"); - } else { - continue; - } - assert(co != NULL && "Function __SMACK_and should be present."); - std::vector args; - args.push_back(bi->getOperand(0)); - args.push_back(bi->getOperand(1)); - instsFrom.push_back(&*I); - instsTo.push_back(CallInst::Create(co, args, "")); - } else { - auto lhs = args[1 - maskOperand]; - Value *rhs = ConstantInt::get( - m.getContext(), *getConstantIntValue(args[maskOperand]) + 1); - Instruction *replacement = - BinaryOperator::Create(Instruction::URem, lhs, rhs, ""); - instsFrom.push_back(&*I); - instsTo.push_back(replacement); - } - } else if (opcode == Instruction::Or) { - unsigned bitWidth = getOpBitWidth(&*I); - Function *co; - if (bitWidth == 64) { - co = m.getFunction("__SMACK_or64"); - } else if (bitWidth == 32) { - co = m.getFunction("__SMACK_or32"); - } else if (bitWidth == 16) { - co = m.getFunction("__SMACK_or16"); - } else if (bitWidth == 8) { - co = m.getFunction("__SMACK_or8"); - } else { - continue; - } - assert(co != NULL && "Function __SMACK_or should be present."); - std::vector args; - args.push_back(bi->getOperand(0)); - args.push_back(bi->getOperand(1)); - instsFrom.push_back(&*I); - instsTo.push_back(CallInst::Create(co, args, "")); - } - } + Instruction *i = &*I; + if (auto sc = getSpecialCase(i)) + insts.push_back(std::make_pair(i, rewriteSpecialCase(*sc, i))); + else if (auto oi = rewriteGeneralCase(i)) + insts.push_back(std::make_pair(i, *oi)); } } - for (size_t i = 0; i < instsFrom.size(); ++i) { - ReplaceInstWithInst(instsFrom[i], instsTo[i]); + for (auto &p : insts) { + p.first->replaceAllUsesWith(p.second); + p.first->removeFromParent(); } return true; diff --git a/test/c/special/bitwise_constant_and.c b/test/c/special/bitwise_constant_and.c new file mode 100644 index 000000000..0c385d8cd --- /dev/null +++ b/test/c/special/bitwise_constant_and.c @@ -0,0 +1,64 @@ +#include "smack.h" + +// @expect verified +// @flag --rewrite-bitwise-ops + +int main(void) { + unsigned char x = __VERIFIER_nondet_unsigned_char(); + // 2**0 + assert((x & 0) == 0); + + // 2**1 + assert((x & 1) == x % 2); + assert((1 & x) == x % 2); + + assert((x & -2) == x - x % 2); + assert((-2 & x) == x - x % 2); + + // 2**2 + assert((x & 3) == x % 4); + assert((3 & x) == x % 4); + + assert((x & -4) == x - x % 4); + assert((-4 & x) == x - x % 4); + + // 2**3 + assert((x & 7) == x % 8); + assert((7 & x) == x % 8); + + assert((x & -8) == x - x % 8); + assert((-8 & x) == x - x % 8); + + // 2**4 + assert((x & 15) == x % 16); + assert((15 & x) == x % 16); + + assert((x & -16) == x - x % 16); + assert((-16 & x) == x - x % 16); + + // 2**5 + assert((x & 31) == x % 32); + assert((31 & x) == x % 32); + + assert((x & -32) == x - x % 32); + assert((-32 & x) == x - x % 32); + + // 2**6 + assert((x & 63) == x % 64); + assert((63 & x) == x % 64); + + assert((x & -64) == x - x % 64); + assert((-64 & x) == x - x % 64); + + // 2**7 + assert((x & 127) == x % 128); + assert((127 & x) == x % 128); + + assert((x & -128) == x - x % 128); + assert((-128 & x) == x - x % 128); + + // 2**8 + assert((x & 255) == x); + + return 0; +} diff --git a/test/c/special/bitwise_constant_and_fail.c b/test/c/special/bitwise_constant_and_fail.c new file mode 100644 index 000000000..236a5f0ef --- /dev/null +++ b/test/c/special/bitwise_constant_and_fail.c @@ -0,0 +1,67 @@ +#include "smack.h" + +// @expect error +// @flag --rewrite-bitwise-ops + +int main(void) { + unsigned char x = __VERIFIER_nondet_unsigned_char(); + unsigned cond = 0; + + // 2**0 + cond = cond || ((x & 0) != 0); + + // 2**1 + cond = cond || ((x & 1) != x % 2); + cond = cond || ((1 & x) != x % 2); + + cond = cond || ((x & -2) != x - x % 2); + cond = cond || ((-2 & x) != x - x % 2); + + // 2**2 + cond = cond || ((x & 3) != x % 4); + cond = cond || ((3 & x) != x % 4); + + cond = cond || ((x & -4) != x - x % 4); + cond = cond || ((-4 & x) != x - x % 4); + + // 2**3 + cond = cond || ((x & 7) != x % 8); + cond = cond || ((7 & x) != x % 8); + + cond = cond || ((x & -8) != x - x % 8); + cond = cond || ((-8 & x) != x - x % 8); + + // 2**4 + cond = cond || ((x & 15) != x % 16); + cond = cond || ((15 & x) != x % 16); + + cond = cond || ((x & -16) != x - x % 16); + cond = cond || ((-16 & x) != x - x % 16); + + // 2**5 + cond = cond || ((x & 31) != x % 32); + cond = cond || ((31 & x) != x % 32); + + cond = cond || ((x & -32) != x - x % 32); + cond = cond || ((-32 & x) != x - x % 32); + + // 2**6 + cond = cond || ((x & 63) != x % 64); + cond = cond || ((63 & x) != x % 64); + + cond = cond || ((x & -64) != x - x % 64); + cond = cond || ((-64 & x) != x - x % 64); + + // 2**7 + cond = cond || ((x & 127) != x % 128); + cond = cond || ((127 & x) != x % 128); + + cond = cond || ((x & -128) != x - x % 128); + cond = cond || ((-128 & x) != x - x % 128); + + // 2**8 + cond = cond || ((x & 255) != x); + + assert(cond); + return 0; +} From d0c238ef5e4fa5e71628a9d53d98ada3d4c5e1b7 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Sun, 17 Jan 2021 16:26:45 -0700 Subject: [PATCH 2/3] Copy ``dbg'' metadata --- lib/smack/RewriteBitwiseOps.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/lib/smack/RewriteBitwiseOps.cpp b/lib/smack/RewriteBitwiseOps.cpp index b0ac37a92..1ccca5769 100644 --- a/lib/smack/RewriteBitwiseOps.cpp +++ b/lib/smack/RewriteBitwiseOps.cpp @@ -38,6 +38,10 @@ int getConstOpId(const Instruction *i) { : (llvm::isa(i->getOperand(0)) ? 0 : -1); } +void copyDbgMetadata(const Instruction *src, Instruction *dest) { + dest->setMetadata("dbg", src->getMetadata("dbg")); +} + Instruction *RewriteBitwiseOps::rewriteShift(Instruction::BinaryOps newOp, Instruction *i) { auto ci = llvm::cast(i->getOperand(1)); @@ -90,6 +94,7 @@ Instruction *RewriteBitwiseOps::rewriteAndNPot(Instruction *i) { auto rem = BinaryOperator::Create( Instruction::URem, lhs, ConstantInt::get(i->getContext(), 0 - constVal), "", i); + copyDbgMetadata(i, rem); return BinaryOperator::Create(Instruction::Sub, lhs, rem, "", i); } @@ -159,6 +164,7 @@ bool RewriteBitwiseOps::runOnModule(Module &m) { } for (auto &p : insts) { + copyDbgMetadata(p.first, p.second); p.first->replaceAllUsesWith(p.second); p.first->removeFromParent(); } From 18e53885f7a27680121121affa0f21c3dae68342 Mon Sep 17 00:00:00 2001 From: Shaobo He Date: Tue, 19 Jan 2021 18:04:02 -0700 Subject: [PATCH 3/3] Renamed a function --- include/smack/RewriteBitwiseOps.h | 2 +- lib/smack/RewriteBitwiseOps.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/include/smack/RewriteBitwiseOps.h b/include/smack/RewriteBitwiseOps.h index 8626491fa..b9d474e18 100644 --- a/include/smack/RewriteBitwiseOps.h +++ b/include/smack/RewriteBitwiseOps.h @@ -30,7 +30,7 @@ class RewriteBitwiseOps : public llvm::ModulePass { static llvm::Instruction *rewriteShr(llvm::Instruction *); static llvm::Instruction *rewriteShl(llvm::Instruction *); static llvm::Instruction *rewriteAndPoTMO(llvm::Instruction *); - static llvm::Instruction *rewriteAndNPot(llvm::Instruction *); + static llvm::Instruction *rewriteAndNPoT(llvm::Instruction *); llvm::Instruction *rewriteSpecialCase(SpecialCase, llvm::Instruction *); boost::optional rewriteGeneralCase(llvm::Instruction *); }; diff --git a/lib/smack/RewriteBitwiseOps.cpp b/lib/smack/RewriteBitwiseOps.cpp index 1ccca5769..fe1fefe36 100644 --- a/lib/smack/RewriteBitwiseOps.cpp +++ b/lib/smack/RewriteBitwiseOps.cpp @@ -85,7 +85,7 @@ Instruction *RewriteBitwiseOps::rewriteAndPoTMO(Instruction *i) { return BinaryOperator::Create(Instruction::URem, lhs, rhs, "", i); } -Instruction *RewriteBitwiseOps::rewriteAndNPot(Instruction *i) { +Instruction *RewriteBitwiseOps::rewriteAndNPoT(Instruction *i) { // E.g., rewrite ``x && -32'' into ``x - x % 32'' auto constOpId = getConstOpId(i); auto constVal = @@ -126,7 +126,7 @@ Instruction *RewriteBitwiseOps::rewriteSpecialCase(SC sc, Instruction *i) { {SC::Shr, &rewriteShr}, {SC::Shl, &rewriteShl}, {SC::AndPoTMO, &rewriteAndPoTMO}, - {SC::AndNPoT, &rewriteAndNPot}}; + {SC::AndNPoT, &rewriteAndNPoT}}; return table[sc](i); }