[analyzer] Add a Fourier-Motzkin elimination solver backend.

[NoQ]

Summary

LLVM contains an implementation of Fourier-Motzkin elimination by @fhahn. It lives in llvm/Analysis/ConstraintSystem.h and allows solving systems of linear inequalities over real-world (non-wrapping) numbers. Even though machine integers are typically wrapping, Fourier-Motzkin elimination can still be used for refuting inequalities that are impossible *even* in real-world numbers - as long as we guarantee lack of overflows in our own linear operations. And, well, we can still take type size constraints into account.

In this patch I'm (partially) implementing conversion from static analyzer symbolic expressions to linear inequalities and adding Fourier-Motzkin elimination as a refutation backend (similar to our Z3 backend). It's currently off by default but I plan to enable it by default as soon as I double-check that the math is correct and make sure there are no performance regressions. I'd also consider making it a part of the default constraint manager so that to refute infeasible execution paths during analysis but I suspect it may have a much larger performance impact. No matter how this turns out, I see this work as orthogonal to other improvements in RangeConstraintManager; these can still keep coming.

Currently the conversion is very limited. It can already refute some simple constraints such as x < y, y < z, z > x but otherwise it treats most symbols as opaque and doesn't really see linear inequalities when you feed them to it. See the large FIXME for more details. It already did refute some real-world false positives for me, around 1% of total warnings, which is much weaker than Z3 but still very promising. Every false positive refuted this way was also refuted by Z3 which suggests (but of course doesn't prove) correctness of the solution.

[NoQ]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

42

My implementation doesn't make use of abstractions from SMTConv.h but introduces its own abstractions instead. This is because the conversion process is too significantly different: while a generic SMT solver can consume arbitrary expressions which suggests a recursive rewrite, Fourier-Motzkin elimination only consumes expressions of fixed shape, which makes conversion very non-recursive and context-dependent. Once the conversion gets more advanced, it will probably also have to rely on other constraint information to avoid overflows which is redundant for a generic SMT solver.

[NoQ]

Fix modules/shared libs build.

[vsavchenko]

Ooooh, delicious! Diving in!

[martong]

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

3193–3194

This is a good check!

3227

Why don't we need the location context anymore?

3253–3254

This if block and the one at line 3259 seems to be redundant (?). We have an assertion in the constructor that either ShouldCrosscheckWithFME or ShouldCrosscheckWithZ3 is true.

clang/lib/StaticAnalyzer/Core/FMEConv.cpp

39–42

llvm::find(Vars, Sym)

[fhahn]

Great to see this coming along :)

On naming, I'd not reference FME, as this is an implementation detail which could change, e.g. if we chose implement a different algorithm later on.

[martong]

Nice work!

clang/lib/StaticAnalyzer/Core/FMEConv.cpp

59

So, in one row each variable's multiplier is initialized to 0 and later we set the Sym's multiplier to 1. This took me some time to realize ... perhaps a comment could be helpful here.

85

Perhaps assert(Op != BO_NE) ?

100

156

I think we could do better than the default behavior in case of SymIntExpr and IntSymExpr. We could call directly the add(SymbolRef Sym, BinaryOperator::Opcode Op,const APSInt &Val) overload. This would be superior especially in case of ranges with one element, e.g. x == 0.

[martong]

clang/lib/StaticAnalyzer/Core/FMEConv.cpp

156

Umm, please disregard my previous comment. I suppose your comment above with the FIXME (line 94) refers to the handling SymInt and IntSym expressions ? Let's suppose we have x+1 in the range [0, 0]. We could transform this to x <= -1 and x >= 1. What is missing to do the transformation?

[steakhal]

According to the coverage of the test I can propose to test for some edge cases:

• _ExtInt(64+)
• uint64_t(INT64_MAX), uint64_t(INT64_MAX + 1)
• etc...

I'm attaching the related gcov HTMLs about the two interesting files.

coverage-report.zip59 KBDownload

clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h

601

Why not const?

607

We should probably mark this explicit.

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

3249–3250

I think the comment is misleading.
If I comprehend this right, it suggests to me that even if FMA is disabled but Z3 is enabled it would still try to crosscheck with FMA. On the other hand, the behavior of the code reflects a different behavior.

3253–3254

I don't think it's redundant, but I agree that it has a code smell.
If this is the behavior we want to implement we could achieve by something like this:

ShouldCrosscheckWithFME ? crosscheckWithFME(BR, BRC) : crosscheckWithZ3(BR, BRC);

3259–3260

I'm not exactly sure why we check and return here. We would return at the end of the function regadless.

clang/lib/StaticAnalyzer/Core/FMEConv.cpp

53

You probably meant > here.
Otherwise, the condition is always false at L63 is dead.

144

I would rather prefer getValue(), it looks weird now - at least for me.

[martong]

clang/lib/StaticAnalyzer/Core/FMEConv.cpp

144

Even better would be to have an early return if the optional is not set, just to avoid this deep nesting of if blocks. But, you could do that early return only if the whole if (const auto *CompSym = dyn_cast<SymSymExpr>(Sym)) { ...} was in a function (or in a lambda).

[NoQ]

On naming, I'd not reference FME, as this is an implementation detail which could change, e.g. if we chose implement a different algorithm later on.

Got it, will fix! Do I understand correctly that the input format ("a system of linear inequalities over real numbers") probably won't change? So I'll still have to do the same conversion and the same overflow-checking?

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

3227

It never made sense in the first place. The second parameter isn't actually used meaningfully by the bug report, it only contributes to the identity of the invalidation stamp, so that this stamp could be removed later if necessary. Even if we ever wanted to remove this particular invalidation stamp, the location context is a really weird choice for its identity. I think this was a copy-paste from some other invalidation.

3253–3254

I think it makes sense to allow cross-checking with both.

3259–3260

For symmetry. No other reason.

clang/lib/StaticAnalyzer/Core/FMEConv.cpp

53

Nice catch! I'll fix.

85

This is already covered by an unreachable below but I agree that it's better to put this on top as a pre-condition.

156

Let's suppose we have x+1 in the range [0, 0].

We won't actually ever have such range. RangeConstraintManager would simplify it into x in range [-1, -1] before recording in the ProgramState.

But if we did have such range then we'd also have overflow problems. Imagine x is also unsigned. Then your original range is SAT in the original program but UNSAT in FME. We'll need overflow checks. They're not hard but we do need some of them.

[ASDenysPetrov]

That's a great beginning! I'd like to join!

clang/include/clang/StaticAnalyzer/Core/PathSensitive/FMEConv.h

26

I see you frequently use predefined size of 8 in SmallVector. Would it be better to make an alias for that, since the structures refer to each other?

SmallVector8<SymbolRef> Vars;
SmallVector8<std::string> Names;
SmallVector8<int64_t> Rows;

clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

292–293

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

3259–3260

I prefer symmetry as it make code readable twice quicklier.

clang/lib/StaticAnalyzer/Core/FMEConv.cpp

48

Can we get a commented description in a few words about what's going inside the function? (and so in the rest)

50

I'd avoid magic numbers.

105–106

129

Is it supposed any logic for EQ, NE subsequently?

158

Could you write a test case for this(with/without holes)?

clang/test/Analysis/fme-crosscheck.c

27–30

I'd like to see tests with MAX, MIN as well.

[ASDenysPetrov]

Ping. Is this alive?

clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def

ANALYZER_OPTION(bool, ShouldSuppressFromCXXStandardLibrary,
                 "standard library should be suppressed.",
                 true)
 
 ANALYZER_OPTION(bool, ShouldCrosscheckWithZ3, "crosscheck-with-z3",
                 "Whether bug reports should be crosschecked with the Z3 "
                 "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 "
                 "reported in the main source file and not the headers.",
                 false)
 
 ANALYZER_OPTION(bool, ShouldWriteStableReportFilename, "stable-report-filename",
                 "Deprecated: report filenames are now always stable. "

clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h

 /// The bug visitor will walk all the nodes in a path and collect all the
 /// constraints. When it reaches the root node, will create a refutation
 /// manager and check if the constraints are satisfiable
 class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
 private:
   /// 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;
 
   PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
                                    BugReporterContext &BRC,
                                    PathSensitiveBugReport &BR) override;
 
   void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,

clang/include/clang/StaticAnalyzer/Core/PathSensitive/FMEConv.h

+//== 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<SymbolRef, 8> 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

clang/include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h

public:
   ///             where N = size(this)
   bool contains(llvm::APSInt Point) const { return containsImpl(Point); }
 
   void dump(raw_ostream &OS) const;
 
   bool operator==(const RangeSet &Other) const { return *Impl == *Other.Impl; }
   bool operator!=(const RangeSet &Other) const { return !(*this == Other); }
 
+  LLVM_NODISCARD llvm::Optional<bool> 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) {}
 
   /// Pin given points to the type represented by the current range set.
   ///
   /// This makes parameter points to be in-out parameters.
   /// In order to maintain consistent types across all of the ranges in the set

clang/lib/StaticAnalyzer/Core/BugReporter.cpp

while (BugPathInfo *BugPath = BugGraph.getNextBugPath()) {
 
     BugReporterContext BRC(Reporter);
 
     // Run all visitors on a given graph, once.
     std::unique_ptr<VisitorsDiagnosticsTy> visitorNotes =
         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<FalsePositiveRefutationBRVisitor>();
+        R->addVisitor<FalsePositiveRefutationBRVisitor>(Opts);
 
         // We don't overwrite the notes inserted by other visitors because the
         // refutation manager does not add any new note to the path
         generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
       }
 
       // Check if the bug is still valid
       if (R->isValid())

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

 #include "clang/Basic/SourceManager.h"
 #include "clang/Lex/Lexer.h"
 #include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #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"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/None.h"
UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC,
   }
   return nullptr;
 }
 
 //===----------------------------------------------------------------------===//
 // 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();
 
   // Add constraints to the solver
   for (const auto &I : Constraints) {
     const SymbolRef Sym = I.first;
     auto RangeIt = I.second.begin();
void FalsePositiveRefutationBRVisitor::crosscheckWithZ3(
   }
 
   // And check for satisfiability
   Optional<bool> IsSAT = RefutationSolver->check();
   if (!IsSAT.hasValue())
     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(
     const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
   // Collect new constraints
   ConstraintMap NewCs = getConstraintMap(N->getState());
   ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
 

clang/lib/StaticAnalyzer/Core/CMakeLists.txt

 set(LLVM_LINK_COMPONENTS
+  Analysis
   FrontendOpenMP
   Support
 )
 
 add_clang_library(clangStaticAnalyzerCore
   APSIntType.cpp
   AnalysisManager.cpp
   AnalyzerOptions.cpp
add_clang_library(clangStaticAnalyzerCore
   Environment.cpp
   ExplodedGraph.cpp
   ExprEngine.cpp
   ExprEngineC.cpp
   ExprEngineCXX.cpp
   ExprEngineCallAndReturn.cpp
   ExprEngineObjC.cpp
   FunctionSummary.cpp
+  FMEConv.cpp
   HTMLDiagnostics.cpp
   LoopUnrolling.cpp
   LoopWidening.cpp
   MemRegion.cpp
   PlistDiagnostics.cpp
   ProgramState.cpp
   RangeConstraintManager.cpp
   RangedConstraintManager.cpp

clang/lib/StaticAnalyzer/Core/FMEConv.cpp

+//= 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<std::string, 8> 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<SymbolData>(Sym))
+      OS << '(';
+
+    Sym->dumpToStream(OS);
+
+    if (!isa<SymbolData>(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<int64_t, 8> 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<int64_t, 8> 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<SymSymExpr>(Sym)) {
+    BinaryOperator::Opcode Op = CompSym->getOpcode();
+    if (BinaryOperator::isComparisonOp(Op)) {
+      Optional<bool> 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);
+}

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

private:
   }
 
   ProgramStateRef trackEquality(ProgramStateRef State, SymbolRef LHS,
                                 SymbolRef RHS) {
     return EquivalenceClass::merge(RangeFactory, State, LHS, RHS);
   }
 
   LLVM_NODISCARD Optional<bool> 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;
   SValBuilder &Builder;
   RangeSet::Factory &RangeFactory;
 };
 
 //===----------------------------------------------------------------------===//

clang/test/Analysis/analyzer-config.c

 // CHECK-NEXT: core.CallAndMessage:CXXDeallocationArg = true
 // CHECK-NEXT: core.CallAndMessage:CXXThisMethodCall = true
 // CHECK-NEXT: core.CallAndMessage:FunctionPointer = true
 // CHECK-NEXT: core.CallAndMessage:NilReceiver = true
 // CHECK-NEXT: core.CallAndMessage:ParameterCount = true
 // 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
 // CHECK-NEXT: ctu-import-threshold = 24
 // CHECK-NEXT: ctu-index-name = externalDefMap.txt
 // CHECK-NEXT: ctu-invocation-list = invocations.yaml
 // CHECK-NEXT: deadcode.DeadStores:ShowFixIts = false
 // CHECK-NEXT: deadcode.DeadStores:WarnForDeadNestedAssignments = true

clang/test/Analysis/fme-crosscheck.c

+// 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}}
+}