Merge pull request #247 from jubitaneja/known-negative

teach souper about data flow fact isKnownNegative

include/souper/Inst/Inst.h

@@ -113,7 +113,7 @@ struct Inst : llvm::FoldingSetNode {
   static const char *getKindName(Kind K);
   static std::string getKnownBitsString(llvm::APInt Zero, llvm::APInt One);
   static std::string getMoreKnownBitsString(bool NonZero, bool NonNegative,
-                                            bool PowOfTwo);
+                                            bool PowOfTwo, bool Negative);
   static Kind getKind(std::string Name);
 
   static bool isAssociative(Kind K);
@@ -124,6 +124,7 @@ struct Inst : llvm::FoldingSetNode {
   bool NonZero;
   bool NonNegative;
   bool PowOfTwo;
+  bool Negative;
 };
 
 /// A mapping from an Inst to a replacement. This may either represent a
@@ -187,7 +188,7 @@ class InstContext {
   Inst *createVar(unsigned Width, llvm::StringRef Name,
                   llvm::APInt Zero=llvm::APInt(1, 0, false),
                   llvm::APInt One=llvm::APInt(1, 0, false), bool NonZero=false,
-                  bool NonNegative=false, bool PowOfTwo=false);
+                  bool NonNegative=false, bool PowOfTwo=false, bool Negative=false);
   Block *createBlock(unsigned Preds);
 
   Inst *getPhi(Block *B, const std::vector<Inst *> &Ops);

lib/Extractor/Candidates.cpp

@@ -158,17 +158,18 @@ Inst *ExprBuilder::makeArrayRead(Value *V) {
     Name = V->getName();
   unsigned Width = DL.getTypeSizeInBits(V->getType());
   APInt KnownZero(Width, 0, false), KnownOne(Width, 0, false);
-  bool NonZero = false, NonNegative = false, PowOfTwo = false;
+  bool NonZero = false, NonNegative = false, PowOfTwo = false, Negative = false;
   if (HarvestKnownBits)
     if (V->getType()->isIntOrIntVectorTy() ||
         V->getType()->getScalarType()->isPointerTy()) {
       computeKnownBits(V, KnownZero, KnownOne, DL);
       NonZero = isKnownNonZero(V, DL);
       NonNegative = isKnownNonNegative(V, DL);
       PowOfTwo = isKnownToBeAPowerOfTwo(V, DL);
+      Negative = isKnownNegative(V, DL);
     }
   return IC.createVar(Width, Name, KnownZero, KnownOne, NonZero, NonNegative,
-                      PowOfTwo);
+                      PowOfTwo, Negative);
 }
 
 Inst *ExprBuilder::buildConstant(Constant *c) {

lib/Extractor/KLEEBuilder.cpp

@@ -81,6 +81,7 @@ struct ExprBuilder {
   std::map<Inst *, ref<Expr>> NonZeroBitsMap;
   std::map<Inst *, ref<Expr>> NonNegBitsMap;
   std::map<Inst *, ref<Expr>> PowerTwoBitsMap;
+  std::map<Inst *, ref<Expr>> NegBitsMap;
   std::map<Block *, BlockPCPredMap> BlockPCMap;
   std::vector<std::unique_ptr<Array>> &Arrays;
   std::vector<Inst *> &ArrayVars;
@@ -119,6 +120,7 @@ struct ExprBuilder {
   ref<Expr> getNonZeroBitsMapping(Inst *I);
   ref<Expr> getNonNegBitsMapping(Inst *I);
   ref<Expr> getPowerTwoBitsMapping(Inst *I);
+  ref<Expr> getNegBitsMapping(Inst *I);
   std::vector<ref<Expr >> getBlockPredicates(Inst *I);
   ref<Expr> getUBInstCondition();
   ref<Expr> getBlockPCs();
@@ -177,6 +179,8 @@ ref<Expr> ExprBuilder::makeSizedArrayRead(unsigned Width, StringRef Name,
                                                                                   klee::ConstantExpr::create(i, Width))));
       PowerTwoBitsMap[Origin] = PowerExpr;
     }
+    if (Origin->Negative)
+      NegBitsMap[Origin] = SltExpr::create(Var, klee::ConstantExpr::create(0, Width));
   }
   return Var;
 }
@@ -1065,6 +1069,10 @@ ref<Expr> ExprBuilder::getNonNegBitsMapping(Inst *I) {
   return NonNegBitsMap[I];
 }
 
+ref<Expr> ExprBuilder::getNegBitsMapping(Inst *I) {
+  return NegBitsMap[I];
+}
+
 ref<Expr> ExprBuilder::getPowerTwoBitsMapping(Inst *I) {
   return PowerTwoBitsMap[I];
 }
@@ -1091,6 +1099,8 @@ llvm::Optional<CandidateExpr> souper::GetCandidateExprForReplacement(
         Ante = AndExpr::create(Ante, EB.getNonNegBitsMapping(I));
       if (I->PowOfTwo)
         Ante = AndExpr::create(Ante, EB.getPowerTwoBitsMapping(I));
+      if (I->Negative)
+        Ante = AndExpr::create(Ante, EB.getNegBitsMapping(I));
     }
   }
   // Build PCs

lib/Inst/Inst.cpp

@@ -161,10 +161,11 @@ std::string ReplacementContext::printInst(Inst *I, llvm::raw_ostream &Out,
         if (I->KnownZeros.getBoolValue() || I->KnownOnes.getBoolValue())
           Out << " (" << Inst::getKnownBitsString(I->KnownZeros, I->KnownOnes)
               << ")";
-        if (I->NonZero || I->NonNegative || I->PowOfTwo)
+        if (I->NonZero || I->NonNegative || I->PowOfTwo || I->Negative)
           Out << " (" << Inst::getMoreKnownBitsString(I->NonZero,
                                                       I->NonNegative,
-                                                      I->PowOfTwo)
+                                                      I->PowOfTwo,
+                                                      I->Negative)
               << ")";
       }
       Out << OpsSS.str();
@@ -268,14 +269,17 @@ std::string Inst::getKnownBitsString(llvm::APInt Zero, llvm::APInt One) {
   return Str;
 }
 
-std::string Inst::getMoreKnownBitsString(bool NonZero, bool NonNegative, bool PowOfTwo) {
+std::string Inst::getMoreKnownBitsString(bool NonZero, bool NonNegative, bool PowOfTwo,
+                                         bool Negative) {
   std::string Str;
   if (NonZero)
     Str.append("z");
   if (NonNegative)
     Str.append("n");
   if (PowOfTwo)
     Str.append("2");
+  if (Negative)
+    Str.append("-");
   return Str;
 }
 
@@ -525,7 +529,7 @@ Inst *InstContext::getUntypedConst(const llvm::APInt &Val) {
 
 Inst *InstContext::createVar(unsigned Width, llvm::StringRef Name,
                              llvm::APInt Zero, llvm::APInt One, bool NonZero,
-                             bool NonNegative, bool PowOfTwo) {
+                             bool NonNegative, bool PowOfTwo, bool Negative) {
   auto &InstList = VarInstsByWidth[Width];
   unsigned Number = InstList.size();
   auto I = new Inst;
@@ -540,6 +544,7 @@ Inst *InstContext::createVar(unsigned Width, llvm::StringRef Name,
   I->NonZero = NonZero;
   I->NonNegative = NonNegative;
   I->PowOfTwo = PowOfTwo;
+  I->Negative = Negative;
   return I;
 }
 

lib/Parser/Parser.cpp

@@ -214,7 +214,8 @@ Token Lexer::getNextToken(std::string &ErrStr) {
       ++Begin;
       KnownBitsFlag = true;
     }
-    while (!KnownBitsFlag && (*Begin == 'n' || *Begin == 'z' || *Begin == '2')) {
+    while (!KnownBitsFlag && (*Begin == 'n' || *Begin == 'z' || *Begin == '2' ||
+           *Begin == '-')) {
       ++Begin;
       MoreKnownBitsFlag = true;
     }
@@ -227,7 +228,7 @@ Token Lexer::getNextToken(std::string &ErrStr) {
       return Token{Token::Error, Begin, 0, APInt()};
     }
     if (Begin == NumBegin) {
-      ErrStr = "invalid, expected [0|1|x]+ or [n|z|2]";
+      ErrStr = "invalid, expected [0|1|x]+ or [n|z|2|-]";
       return Token{Token::Error, Begin, 0, APInt()};
     }
     Token T;
@@ -900,7 +901,7 @@ bool Parser::parseLine(std::string &ErrStr) {
       if (IK == Inst::Var) {
         llvm::APInt Zero(InstWidth, 0, false), One(InstWidth, 0, false),
                     ConstOne(InstWidth, 1, false);
-        bool NonZero = false, NonNegative = false, PowOfTwo = false;
+        bool NonZero = false, NonNegative = false, PowOfTwo = false, Negative = false;
         unsigned SignBits = 0;
         while (CurTok.K != Token::ValName && CurTok.K != Token::Ident && CurTok.K != Token::Eof) {
           if (CurTok.K == Token::KnownBits) {
@@ -920,32 +921,38 @@ bool Parser::parseLine(std::string &ErrStr) {
           if (CurTok.K == Token::MoreKnownBits) {
             for (unsigned i=0; i<CurTok.PatternString.length(); ++i) {
               if (CurTok.PatternString[i] == 'z') {
-		if (NonZero) {
-		  ErrStr = makeErrStr(TP, "repeated 'z' flag");
-		  return false;
-		}
+                if (NonZero) {
+                  ErrStr = makeErrStr(TP, "repeated 'z' flag");
+                  return false;
+                }
                 NonZero = true;
-	      } else if (CurTok.PatternString[i] == 'n') {
-		if (NonNegative) {
-		  ErrStr = makeErrStr(TP, "repeated 'n' flag");
-		  return false;
-		}
+              } else if (CurTok.PatternString[i] == 'n') {
+                if (NonNegative) {
+                  ErrStr = makeErrStr(TP, "repeated 'n' flag");
+                  return false;
+                }
                 NonNegative = true;
-	      } else if (CurTok.PatternString[i] == '2') {
-		if (PowOfTwo) {
-		  ErrStr = makeErrStr(TP, "repeated '2' flag");
-		  return false;
-		}
+              } else if (CurTok.PatternString[i] == '2') {
+                if (PowOfTwo) {
+                  ErrStr = makeErrStr(TP, "repeated '2' flag");
+                  return false;
+                }
                 PowOfTwo = true;
-	      } else {
-		llvm_unreachable("nzp should have been checked earlier");
-	      }
-	    }
+              } else if (CurTok.PatternString[i] == '-') {
+                if (Negative) {
+                  ErrStr = makeErrStr(TP, "repeated '-' flag");
+                  return false;
+                }
+                Negative = true;
+              } else {
+                llvm_unreachable("nzp should have been checked earlier");
+              }
+            }
             if (!consumeToken(ErrStr))
               return false;
           }
         }
-        Inst *I = IC.createVar(InstWidth, InstName, Zero, One, NonZero, NonNegative, PowOfTwo);
+        Inst *I = IC.createVar(InstWidth, InstName, Zero, One, NonZero, NonNegative, PowOfTwo, Negative);
         Context.setInst(InstName, I);
         return true;
       }

test/Tool/more-knownbits18.opt

@@ -0,0 +1,12 @@
+; REQUIRES: solver, solver-model
+
+; RUN: %souper-check %solver -infer-rhs -print-replacement %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK:      %0:i32 = var (-)
+; CHECK-NEXT: %1:i1 = slt %0, 0:i32
+; CHECK-NEXT: cand %1 1:i1
+
+%0:i32 = var (-)
+%1:i1 = slt %0, 0:i32
+infer %1

test/Tool/more-knownbits19.opt

@@ -0,0 +1,10 @@
+; REQUIRES: solver
+
+; RUN: %souper-check %solver -print-counterexample=false  %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK: LGTM
+%0:i32 = var (-)
+%1:i32 = var (n)
+%2:i1 = eq %0, %1
+cand %2 0:i1

test/Tool/more-knownbits20.opt

@@ -0,0 +1,10 @@
+; REQUIRES: solver
+
+; RUN: %souper-check %solver -print-counterexample=false  %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK: LGTM
+%0:i32 = var (-)
+%1:i32 = var (2)
+%2:i1 = eq %0, %1
+cand %2 0:i1

test/Tool/more-knownbits21-invalid.opt

@@ -0,0 +1,11 @@
+; REQUIRES: solver
+
+; RUN: %souper-check %solver -print-counterexample=false  %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK: Invalid
+%0:i32 = var (-)
+%1:i32 = var (n)
+%2:i32 = mulnsw %0, %1
+%3:i1 = slt %2, 0:i32
+cand %3 1:i1

test/Tool/more-knownbits21.opt

@@ -0,0 +1,11 @@
+; REQUIRES: solver
+
+; RUN: %souper-check %solver -print-counterexample=false  %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK: LGTM
+%0:i32 = var (-)
+%1:i32 = var (n)
+%2:i32 = mulnsw %0, %1
+%3:i1 = sle %2, 0:i32
+cand %3 1:i1

test/Tool/more-knownbits22-invalid.opt

@@ -0,0 +1,11 @@
+; REQUIRES: solver
+
+; RUN: %souper-check %solver -print-counterexample=false  %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK: Invalid
+%0:i16 = var (-)
+%1:i16 = var
+%2:i16 = mulnsw %0, %1
+%3:i1 = slt 0:i16, %2
+cand %3 1:i1

test/Tool/more-knownbits22.opt

@@ -0,0 +1,11 @@
+; REQUIRES: solver
+
+; RUN: %souper-check %solver -print-counterexample=false  %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK: LGTM
+%0:i16 = var (-)
+%1:i16 = var (-)
+%2:i16 = mulnsw %0, %1
+%3:i1 = slt 0:i16, %2
+cand %3 1:i1

test/Tool/more-knownbits23.opt

@@ -0,0 +1,15 @@
+; REQUIRES: solver, solver-model
+
+; RUN: %souper-check %solver -infer-rhs -print-replacement %s > %t 2>&1
+; RUN: FileCheck %s < %t
+; CHECK:      %0:i16 = var (-)
+; CHECK-NEXT: %1:i32 = sext %0
+; CHECK-NEXT: %2:i32 = ctpop %1
+; CHECK-NEXT: %3:i1 = ule 17:i32, %2
+; CHECK-NEXT: cand %3 1:i1
+
+%0:i16 = var (-)
+%1:i32 = sext %0
+%2:i32 = ctpop %1
+%3:i1 = ule 17:i32, %2
+infer %3

test/Tool/more-knownbits24.opt

@@ -0,0 +1,10 @@
+; REQUIRES: solver
+
+; RUN: %souper-check %solver -print-counterexample=false  %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK: LGTM
+%0:i32 = var (-)
+%1:i32 = subnsw 0:i32, %0
+%2:i1 = slt 0:i32, %1
+cand %2 1:i1

test/Tool/more-knownbits25.opt

@@ -0,0 +1,11 @@
+; REQUIRES: solver
+
+; RUN: %souper-check %solver -print-counterexample=false  %s > %t 2>&1
+; RUN: FileCheck %s < %t
+
+; CHECK: LGTM
+%0:i32 = var (-)
+%1:i32 = var (-)
+%2:i32 = sdivexact %0, %1
+%3:i1 = ne 0:i32, %2
+cand %3 1:i1

unittests/Parser/ParserTests.cpp

@@ -85,7 +85,7 @@ TEST(ParserTest, Errors) {
       { "%0:i4 = var (xxx)\n",
         "<input>:1:1: knownbits pattern must be of same length as var width" },
       { "%0:i4 = var ()\n",
-        "<input>:1:14: invalid, expected [0|1|x]+ or [n|z|2]" },
+        "<input>:1:14: invalid, expected [0|1|x]+ or [n|z|2|-]" },
       { "%0:i4 = var (10x0\n",
         "<input>:1:18: invalid knownbits string" },
       { "%0:i4 = var (10\nx0)\n",
@@ -104,13 +104,15 @@ TEST(ParserTest, Errors) {
       { "%0:i4 = var (0011 (zn)\n",
         "<input>:1:18: invalid knownbits string" },
       { "%0:i4 = var (a)\n",
-        "<input>:1:14: invalid, expected [0|1|x]+ or [n|z|2]" },
+        "<input>:1:14: invalid, expected [0|1|x]+ or [n|z|2|-]" },
       { "%0:i4 = var (zn2\n",
         "<input>:1:17: invalid more knownbits string" },
       { "%0:i8 = var (zn22)\n",
         "<input>:1:1: repeated '2' flag" },
       { "%0:i8 = var (2x)\n",
         "<input>:1:15: invalid more knownbits string" },
+      { "%0:i4 = var (-\n",
+        "<input>:1:15: invalid more knownbits string" },
 
       // type checking
       { "%0 = add 1:i32\n",