Index: clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def =================================================================== --- clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def +++ clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def @@ -183,6 +183,11 @@ "constraint manager backend.", false) +ANALYZER_OPTION(bool, ShouldCrosscheckWithFME, "crosscheck-with-fme", + "Whether bug reports should be crosschecked via " + "Fourier-Motzkin elimination.", + false) + ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile, "report-in-main-source-file", "Whether or not the diagnostic report should be always " Index: clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h @@ -598,8 +598,13 @@ /// Holds the constraints in a given path ConstraintMap Constraints; + bool ShouldCrosscheckWithZ3 = false; + void crosscheckWithZ3(PathSensitiveBugReport &BR, BugReporterContext &BRC); + bool ShouldCrosscheckWithFME = false; + void crosscheckWithFME(PathSensitiveBugReport &BR, BugReporterContext &BRC); + public: - FalsePositiveRefutationBRVisitor(); + FalsePositiveRefutationBRVisitor(const AnalyzerOptions &Opts); void Profile(llvm::FoldingSetNodeID &ID) const override; Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/FMEConv.h =================================================================== --- /dev/null +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/FMEConv.h @@ -0,0 +1,68 @@ +//== FMEConv.h --------------------------------------------------*- C++ -*--==// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// This file defines conversion from static analyzer symbolic expressions to +// systems of linear inequalities suitable for Fourier-Motzkin elimination. +// +//===----------------------------------------------------------------------===// + +#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_FMECONV_H +#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_FMECONV_H + +#include "clang/AST/Expr.h" +#include "llvm/Analysis/ConstraintSystem.h" + +namespace clang { +namespace ento { + +class RangeSet; +class SymExpr; +using SymbolRef = const SymExpr *; + +/// A wrapper that consumes static analyzer symbolic expressions and +/// writes them down as a system of linear inequalities suitable for +/// Fourier-Motzkin elimination. Each FMESolver instance represents one such +/// system. Constraints can be added one-by-one. Finally, conducts +/// said elimination in order to discover whether the system of constraints +/// can be satisfied in real numbers. +class FMESolver { + SmallVector Vars = {}; + llvm::ConstraintSystem Constraints; + + size_t findOrCreateVar(SymbolRef Sym); + + void add(SymbolRef Sym, BinaryOperator::Opcode Op, const llvm::APSInt &Val); + void add(SymbolRef LHS, BinaryOperator::Opcode Op, SymbolRef RHS); + +public: + FMESolver() {} + + LLVM_DUMP_METHOD void dump() const; + + /// Returns false if the system of constraints constructed so far + /// is definitely unsatisfiable, otherwise returns true. + LLVM_NODISCARD bool mayHaveSolution() { + return Constraints.mayHaveSolution(); + } + + /// Adds constraints that represent how the symbolic expression + /// is limited to the given range. It is guaranteed that the added + /// inequalities over real numbers logically follow from the + /// provided constraint in modular arithmetic. The inverse is + /// not necessarily true: this method may add no new inequalities + /// or add inequalities that may be satisfiable more often than + /// the original input. This is acceptable, however, because + /// the solver is not guaranteed to always answer "satisfiable" + /// whenever the original system is satisfiable. + void add(SymbolRef Sym, const RangeSet &Range); +}; + +} // namespace ento +} // namespace clang + +#endif // LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_FMECONV_H Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h @@ -286,6 +286,20 @@ bool operator==(const RangeSet &Other) const { return *Impl == *Other.Impl; } bool operator!=(const RangeSet &Other) const { return !(*this == Other); } + LLVM_NODISCARD llvm::Optional interpreteAsBool() const { + assert(!isEmpty() && "Empty ranges shouldn't get here"); + + if (getConcreteValue()) + return !getConcreteValue()->isNullValue(); + + APSIntType T{getMinValue()}; + const llvm::APSInt &Zero = T.getZeroValue(); + if (!contains(Zero)) + return true; + + return llvm::None; + } + private: /* implicit */ RangeSet(ContainerType *RawContainer) : Impl(RawContainer) {} /* implicit */ RangeSet(UnderlyingType Ptr) : Impl(Ptr) {} Index: clang/lib/StaticAnalyzer/Core/BugReporter.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/BugReporter.cpp +++ clang/lib/StaticAnalyzer/Core/BugReporter.cpp @@ -2854,11 +2854,12 @@ generateVisitorsDiagnostics(R, ErrorNode, BRC); if (R->isValid()) { - if (Reporter.getAnalyzerOptions().ShouldCrosscheckWithZ3) { + const AnalyzerOptions &Opts = Reporter.getAnalyzerOptions(); + if (Opts.ShouldCrosscheckWithZ3 || Opts.ShouldCrosscheckWithFME) { // If crosscheck is enabled, remove all visitors, add the refutation // visitor and check again R->clearVisitors(); - R->addVisitor(); + R->addVisitor(Opts); // We don't overwrite the notes inserted by other visitors because the // refutation manager does not add any new note to the path Index: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -39,6 +39,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/FMEConv.h" #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" @@ -3184,15 +3185,17 @@ // Implementation of FalsePositiveRefutationBRVisitor. //===----------------------------------------------------------------------===// -FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor() - : Constraints(ConstraintMap::Factory().getEmptyMap()) {} - -void FalsePositiveRefutationBRVisitor::finalizeVisitor( - BugReporterContext &BRC, const ExplodedNode *EndPathNode, - PathSensitiveBugReport &BR) { - // Collect new constraints - addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true); +FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor( + const AnalyzerOptions &Opts) + : Constraints(ConstraintMap::Factory().getEmptyMap()), + ShouldCrosscheckWithZ3(Opts.ShouldCrosscheckWithZ3), + ShouldCrosscheckWithFME(Opts.ShouldCrosscheckWithFME) { + assert((ShouldCrosscheckWithZ3 || ShouldCrosscheckWithFME) && + "Refutation requested but no method specified"); +} +void FalsePositiveRefutationBRVisitor::crosscheckWithZ3( + PathSensitiveBugReport &BR, BugReporterContext &BRC) { // Create a refutation manager llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); ASTContext &Ctx = BRC.getASTContext(); @@ -3221,7 +3224,41 @@ return; if (!IsSAT.getValue()) - BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext()); + BR.markInvalid("Constraints refuted by Z3", nullptr); +} + +void FalsePositiveRefutationBRVisitor::crosscheckWithFME( + PathSensitiveBugReport &BR, BugReporterContext &BRC) { + FMESolver Solver; + + for (const auto &I : Constraints) + Solver.add(I.first, I.second); + + if (!Solver.mayHaveSolution()) { + BR.markInvalid("Constraints refuted by Fourier-Motzkin elimination", + nullptr); + } +} + +void FalsePositiveRefutationBRVisitor::finalizeVisitor( + BugReporterContext &BRC, const ExplodedNode *EndPathNode, + PathSensitiveBugReport &BR) { + // Collect new constraints + addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true); + + // Fourier-Motzkin elimination alone will arguably be faster than full Z3. + // So do it first and hope that we don't have to do Z3 later. + if (ShouldCrosscheckWithFME) { + crosscheckWithFME(BR, BRC); + if (!BR.isValid()) + return; + } + + if (ShouldCrosscheckWithZ3) { + crosscheckWithZ3(BR, BRC); + if (!BR.isValid()) + return; + } } void FalsePositiveRefutationBRVisitor::addConstraints( Index: clang/lib/StaticAnalyzer/Core/CMakeLists.txt =================================================================== --- clang/lib/StaticAnalyzer/Core/CMakeLists.txt +++ clang/lib/StaticAnalyzer/Core/CMakeLists.txt @@ -1,4 +1,5 @@ set(LLVM_LINK_COMPONENTS + Analysis FrontendOpenMP Support ) @@ -30,6 +31,7 @@ ExprEngineCallAndReturn.cpp ExprEngineObjC.cpp FunctionSummary.cpp + FMEConv.cpp HTMLDiagnostics.cpp LoopUnrolling.cpp LoopWidening.cpp Index: clang/lib/StaticAnalyzer/Core/FMEConv.cpp =================================================================== --- /dev/null +++ clang/lib/StaticAnalyzer/Core/FMEConv.cpp @@ -0,0 +1,164 @@ +//= FMEConv.cpp - Fourier-Motzkin elimination solver wrapper ---*- C++ -*--===// +// +// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. +// See https://llvm.org/LICENSE.txt for license information. +// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception +// +//===----------------------------------------------------------------------===// +// +// This file defines conversion from static analyzer symbolic expressions to +// systems of linear inequalities suitable for Fourier-Motzkin elimination. +// +//===----------------------------------------------------------------------===// + +#include "clang/StaticAnalyzer/Core/PathSensitive/FMEConv.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" + +using namespace clang; +using namespace ento; +using namespace llvm; + +void FMESolver::dump() const { + SmallVector Names(Vars.size()); + for (size_t I = 0, E = Vars.size(); I < E; ++I) { + SymbolRef Sym = Vars[I]; + llvm::raw_string_ostream OS(Names[I]); + if (!isa(Sym)) + OS << '('; + + Sym->dumpToStream(OS); + + if (!isa(Sym)) + OS << ')'; + } + + Constraints.dump(Names); +} + +size_t FMESolver::findOrCreateVar(SymbolRef Sym) { + size_t I = 0, E = Vars.size(); + for (; I < E; ++I) + if (Vars[I] == Sym) + return I; + + Vars.push_back(Sym); + return E; +} + +void FMESolver::add(SymbolRef Sym, BinaryOperator::Opcode Op, + const APSInt &Val) { + if (Val.getBitWidth() > 64) + return; + + if (Val.isUnsigned() && Val.getZExtValue() >= INT64_MAX) + return; + + // Variable 0 is at position 1. Constant is at position 0. + size_t Pos = findOrCreateVar(Sym) + 1; + + SmallVector Row(Vars.size() + 1); + + int64_t IntVal = Val.getExtValue(); + if (Op == BO_LE) { + if (IntVal == INT64_MAX) { + // The constraint is meaningless. + return; + } + Row[Pos] = 1; + Row[0] = IntVal; + } else if (Op == BO_GE) { + if (IntVal == INT64_MIN) { + // -IntVal will overflow. + return; + } + + // -Val <= -Var. + Row[Pos] = -1; + Row[0] = -IntVal; + } else { + llvm_unreachable("Unsupported opcode"); + } + + Constraints.addVariableRowFill(Row); +} + +void FMESolver::add(SymbolRef LHS, BinaryOperator::Opcode Op, SymbolRef RHS) { + if (Op == BO_EQ) { + add(LHS, BO_LE, RHS); + add(LHS, BO_GE, RHS); + return; + } + + // Treat both the LHS and the RHS as opaque symbols. + // + // FIXME: We can do A LOT better than that. Namely, we can check if either + // LHS or RHS is a linear expression over other symbols (a combination of + // additions/subtractions and multiplications by concrete integers) + // and try to convert it into a full-blown linear inequality + // that'd be fully supported by our underlying engine, llvm::ConstraintSystem. + // The tricky part is to detect potential overflows in linear operations + // and avoid incorrectly coverting them into corresponding + // real-number operations (but use a fresh opaque variable to represent + // the result instead). + + // Variable 0 is at position 1. Constant is at position 0. + size_t LHSPos = findOrCreateVar(LHS) + 1; + size_t RHSPos = findOrCreateVar(RHS) + 1; + + SmallVector Row(Vars.size() + 1); + + if (Op == BO_LE) { + // 0 >= LHS - RHS + Row[LHSPos] = 1; + Row[RHSPos] = -1; + } else if (Op == BO_GE) { + // 0 >= RHS - LHS + Row[LHSPos] = -1; + Row[RHSPos] = 1; + } else if (Op == BO_LT) { + // -1 >= LHS - RHS + Row[LHSPos] = 1; + Row[RHSPos] = -1; + Row[0] = -1; + } else if (Op == BO_GT) { + // -1 >= RHS - LHS + Row[LHSPos] = -1; + Row[RHSPos] = 1; + Row[0] = -1; + } else { + llvm_unreachable("Unimplemented opcode"); + } + + Constraints.addVariableRowFill(Row); +} + +void FMESolver::add(SymbolRef Sym, const RangeSet &Range) { + // If the symbolic expression is a comparison and the range represents + // a concrete boolean "true" or "false" as the result of that comparison, + // convert the comparison into a single inequality. + if (const auto *CompSym = dyn_cast(Sym)) { + BinaryOperator::Opcode Op = CompSym->getOpcode(); + if (BinaryOperator::isComparisonOp(Op)) { + Optional AsBool = Range.interpreteAsBool(); + if (AsBool) { + if (!*AsBool) + Op = BinaryOperator::negateComparisonOp(Op); + + // "a != b" cannot be represented as a system of linear inequalities. + if (Op != BO_NE) { + add(CompSym->getLHS(), Op, CompSym->getRHS()); + return; + } + } + } + } + + // Default behavior. + // - Treat the symbol as opaque. + // - Ignore all holes in the range. + APSInt From = Range.getMinValue(); + add(Sym, BO_GE, From); + + APSInt To = Range.getMaxValue(); + add(Sym, BO_LE, To); +} Index: clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp +++ clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp @@ -1565,17 +1565,7 @@ } LLVM_NODISCARD Optional interpreteAsBool(RangeSet Constraint) { - assert(!Constraint.isEmpty() && "Empty ranges shouldn't get here"); - - if (Constraint.getConcreteValue()) - return !Constraint.getConcreteValue()->isNullValue(); - - APSIntType T{Constraint.getMinValue()}; - Const Zero = T.getZeroValue(); - if (!Constraint.contains(Zero)) - return true; - - return llvm::None; + return Constraint.interpreteAsBool(); } ProgramStateRef State; Index: clang/test/Analysis/analyzer-config.c =================================================================== --- clang/test/Analysis/analyzer-config.c +++ clang/test/Analysis/analyzer-config.c @@ -42,6 +42,7 @@ // CHECK-NEXT: core.CallAndMessage:UndefReceiver = true // CHECK-NEXT: cplusplus.Move:WarnOn = KnownsAndLocals // CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false +// CHECK-NEXT: crosscheck-with-fme = false // CHECK-NEXT: crosscheck-with-z3 = false // CHECK-NEXT: ctu-dir = "" // CHECK-NEXT: ctu-import-cpp-threshold = 8 Index: clang/test/Analysis/fme-crosscheck.c =================================================================== --- /dev/null +++ clang/test/Analysis/fme-crosscheck.c @@ -0,0 +1,30 @@ +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection %s \ +// RUN: -analyzer-config crosscheck-with-fme=false \ +// RUN: -verify=expected,nocrosscheck +// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection %s \ +// RUN: -analyzer-config crosscheck-with-fme=true \ +// RUN: -verify=expected,crosscheck + +void clang_analyzer_warnIfReached(); + +void test_int(int x, int y) { + if (x < 10 && y > 20 && y < x) { + clang_analyzer_warnIfReached(); // nocrosscheck-warning{{REACHABLE}} + } +} + +void test_unsigned(unsigned x, unsigned y) { + if (x < 10 && y > 20 && y < x) { + clang_analyzer_warnIfReached(); // nocrosscheck-warning{{REACHABLE}} + } +} + +void test_fully_symbolic(int x, int y, int z) { + if (x < y && y < z && x > z) + clang_analyzer_warnIfReached(); // nocrosscheck-warning{{REACHABLE}} +} + +void test_sign_extension_in_solver(unsigned x) { + if (x > 0) + clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}} +}