Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -134,9 +134,9 @@ // A value has been obtained, check if it is the only value SMTExprRef NotExp = SMTConv::fromBinOp( Solver, Exp, BO_NE, - Ty->isBooleanType() ? Solver->fromBoolean(Value.getBoolValue()) - : Solver->fromAPSInt(Value), - false); + Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue()) + : Solver->mkBitvector(Value, Value.getBitWidth()), + /*isSigned=*/false); Solver->addConstraint(NotExp); Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -246,7 +246,7 @@ // Logical operators case BO_LAnd: case BO_LOr: - return fromBinOp(Solver, LHS, Op, RHS, false); + return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false); default:; } @@ -294,14 +294,14 @@ if (FromTy->isIntegralOrEnumerationType() && ToTy->isRealFloatingType()) { SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); return FromTy->isSignedIntegerOrEnumerationType() - ? Solver->mkFPtoSBV(Exp, Sort) - : Solver->mkFPtoUBV(Exp, Sort); + ? Solver->mkSBVtoFP(Exp, Sort) + : Solver->mkUBVtoFP(Exp, Sort); } if (FromTy->isRealFloatingType() && ToTy->isIntegralOrEnumerationType()) return ToTy->isSignedIntegerOrEnumerationType() - ? Solver->mkSBVtoFP(Exp, ToBitWidth) - : Solver->mkUBVtoFP(Exp, ToBitWidth); + ? Solver->mkFPtoSBV(Exp, ToBitWidth) + : Solver->mkFPtoUBV(Exp, ToBitWidth); llvm_unreachable("Unsupported explicit type cast!"); } @@ -379,14 +379,14 @@ getSymExpr(Solver, Ctx, SIE->getLHS(), <y, hasComparison); llvm::APSInt NewRInt; std::tie(NewRInt, RTy) = fixAPSInt(Ctx, SIE->getRHS()); - SMTExprRef RHS = Solver->fromAPSInt(NewRInt); + SMTExprRef RHS = Solver->mkBitvector(NewRInt, NewRInt.getBitWidth()); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); } if (const IntSymExpr *ISE = dyn_cast(BSE)) { llvm::APSInt NewLInt; std::tie(NewLInt, LTy) = fixAPSInt(Ctx, ISE->getLHS()); - SMTExprRef LHS = Solver->fromAPSInt(NewLInt); + SMTExprRef LHS = Solver->mkBitvector(NewLInt, NewLInt.getBitWidth()); SMTExprRef RHS = getSymExpr(Solver, Ctx, ISE->getRHS(), &RTy, hasComparison); return getBinExpr(Solver, Ctx, LHS, LTy, Op, RHS, RTy, RetTy); @@ -466,7 +466,7 @@ llvm::APFloat Zero = llvm::APFloat::getZero(Ctx.getFloatTypeSemantics(Ty)); return fromFloatBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE, - Solver->fromAPFloat(Zero)); + Solver->mkFloat(Zero)); } if (Ty->isIntegralOrEnumerationType() || Ty->isAnyPointerType() || @@ -477,8 +477,10 @@ if (Ty->isBooleanType()) return Assumption ? fromUnOp(Solver, UO_LNot, Exp) : Exp; - return fromBinOp(Solver, Exp, Assumption ? BO_EQ : BO_NE, - Solver->fromInt("0", Ctx.getTypeSize(Ty)), isSigned); + return fromBinOp( + Solver, Exp, Assumption ? BO_EQ : BO_NE, + Solver->mkBitvector(llvm::APSInt("0"), Ctx.getTypeSize(Ty)), + isSigned); } llvm_unreachable("Unsupported type for zero value!"); @@ -493,7 +495,8 @@ QualType FromTy; llvm::APSInt NewFromInt; std::tie(NewFromInt, FromTy) = fixAPSInt(Ctx, From); - SMTExprRef FromExp = Solver->fromAPSInt(NewFromInt); + SMTExprRef FromExp = + Solver->mkBitvector(NewFromInt, NewFromInt.getBitWidth()); // Convert symbol QualType SymTy; @@ -507,7 +510,7 @@ QualType ToTy; llvm::APSInt NewToInt; std::tie(NewToInt, ToTy) = fixAPSInt(Ctx, To); - SMTExprRef ToExp = Solver->fromAPSInt(NewToInt); + SMTExprRef ToExp = Solver->mkBitvector(NewToInt, NewToInt.getBitWidth()); assert(FromTy == ToTy && "Range values have different types!"); // Construct two (in)equalities, and a logical and/or Index: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h =================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h @@ -226,23 +226,23 @@ /// operation virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0; - /// Creates a floating-point conversion from floatint-point to signed - /// bitvector operation - virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, - const SMTSortRef &To) = 0; - - /// Creates a floating-point conversion from floatint-point to unsigned - /// bitvector operation - virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, - const SMTSortRef &To) = 0; - /// Creates a floating-point conversion from signed bitvector to /// floatint-point operation - virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0; + virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, + const SMTSortRef &To) = 0; /// Creates a floating-point conversion from unsigned bitvector to /// floatint-point operation - virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) = 0; + virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, + const SMTSortRef &To) = 0; + + /// Creates a floating-point conversion from floatint-point to signed + /// bitvector operation + virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0; + + /// Creates a floating-point conversion from floatint-point to unsigned + /// bitvector operation + virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0; /// Creates a new symbol, given a name and a sort virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0; @@ -273,18 +273,6 @@ virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) = 0; - /// Construct an SMTExprRef value from a boolean. - virtual SMTExprRef fromBoolean(const bool Bool) = 0; - - /// Construct an SMTExprRef value from a finite APFloat. - virtual SMTExprRef fromAPFloat(const llvm::APFloat &Float) = 0; - - /// Construct an SMTExprRef value from an APSInt. - virtual SMTExprRef fromAPSInt(const llvm::APSInt &Int) = 0; - - /// Construct an SMTExprRef value from an integer. - virtual SMTExprRef fromInt(const char *Int, uint64_t BitWidth) = 0; - /// Check if the constraints are satisfiable virtual Optional check() const = 0; Index: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -2448,15 +2448,19 @@ // Add constraints to the solver for (const auto &I : Constraints) { - SymbolRef Sym = I.first; + const SymbolRef Sym = I.first; + auto RangeIt = I.second.begin(); - SMTExprRef Constraints = RefutationSolver->fromBoolean(false); - for (const auto &Range : I.second) { + SMTExprRef Constraints = SMTConv::getRangeExpr( + RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(), + /*InRange=*/true); + while ((++RangeIt) != I.second.end()) { Constraints = RefutationSolver->mkOr( Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, - Range.From(), Range.To(), + RangeIt->From(), RangeIt->To(), /*InRange=*/true)); } + RefutationSolver->addConstraint(Constraints); } Index: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -671,7 +671,7 @@ toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); } - SMTExprRef mkFPtoSBV(const SMTExprRef &From, const SMTSortRef &To) override { + SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override { SMTExprRef RoundingMode = getFloatRoundingMode(); return newExprRef(Z3Expr( Context, @@ -679,7 +679,7 @@ toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); } - SMTExprRef mkFPtoUBV(const SMTExprRef &From, const SMTSortRef &To) override { + SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override { SMTExprRef RoundingMode = getFloatRoundingMode(); return newExprRef(Z3Expr( Context, @@ -687,14 +687,14 @@ toZ3Expr(*From).AST, toZ3Sort(*To).Sort))); } - SMTExprRef mkSBVtoFP(const SMTExprRef &From, unsigned ToWidth) override { + SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override { SMTExprRef RoundingMode = getFloatRoundingMode(); return newExprRef(Z3Expr( Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST, toZ3Expr(*From).AST, ToWidth))); } - SMTExprRef mkUBVtoFP(const SMTExprRef &From, unsigned ToWidth) override { + SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override { SMTExprRef RoundingMode = getFloatRoundingMode(); return newExprRef(Z3Expr( Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST, @@ -747,36 +747,6 @@ return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context))); } - SMTExprRef fromBoolean(const bool Bool) override { - Z3_ast AST = - Bool ? Z3_mk_true(Context.Context) : Z3_mk_false(Context.Context); - return newExprRef(Z3Expr(Context, AST)); - } - - SMTExprRef fromAPFloat(const llvm::APFloat &Float) override { - SMTSortRef Sort = - getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics())); - - llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false); - SMTExprRef Z3Int = fromAPSInt(Int); - return newExprRef(Z3Expr( - Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST, - toZ3Sort(*Sort).Sort))); - } - - SMTExprRef fromAPSInt(const llvm::APSInt &Int) override { - SMTSortRef Sort = getBitvectorSort(Int.getBitWidth()); - Z3_ast AST = Z3_mk_numeral(Context.Context, Int.toString(10).c_str(), - toZ3Sort(*Sort).Sort); - return newExprRef(Z3Expr(Context, AST)); - } - - SMTExprRef fromInt(const char *Int, uint64_t BitWidth) override { - SMTSortRef Sort = getBitvectorSort(BitWidth); - Z3_ast AST = Z3_mk_numeral(Context.Context, Int, toZ3Sort(*Sort).Sort); - return newExprRef(Z3Expr(Context, AST)); - } - bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST, llvm::APFloat &Float, bool useSemantics) { assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");