[Analyzer][solver] Simplification: reorganize equalities with adjustment

[martong]

Summary

Initiate the reorganization of the equality information during symbol
simplification. E.g., if we bump into c + 1 == 0 during simplification
then we'd like to express that c == -1. It makes sense to do this only
with SymIntExprs.

[steakhal]

The coverage report of the test shows that L2124 is uncovered. Please add a test demonstrating that path as well.
I'm gonna come back to this tomorrow.

clang/test/Analysis/solver-sym-simplification-adjustment.c

37

Please express that C: [-2,-1] is then intersected with the already associated range which is [-1,1], thus we get c: [-1,-1].

56

Can we infer within this true branch that b must be 0 to make this path feasible?
If we already can infer this, can we put there the appropriate assertion?
If not, an assertion would be justified with a FIXME.

[steakhal]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2161–2165

Can the simplification of a SymSymExpr result in IntSymExpr? If it can happen, then we could see such instances and we should do the right thing with them as well.
WDYT?

[martong]

• Add comment about intersection in the test file
• Add check in the feasible case in the test file

[martong]

• Add a test to cover if (OldState == State)

[martong]

In D111642#3059467, @steakhal wrote:

The coverage report of the test shows that L2124 is uncovered. Please add a test demonstrating that path as well.

I've added such a test, thanks for the notice!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2161–2165

Can the simplification of a SymSymExpr result in IntSymExpr?

Yes it can. However, in order to handle them we should extend computeAdjustment properly, which is absolutely not trivial - considering the test cases in additive-folding.cpp - So, I'd rather address that in another patch.

clang/test/Analysis/solver-sym-simplification-adjustment.c

37

Ok, I've added that comment.

56

Can we infer within this true branch that b must be 0 to make this path feasible?

Yes, we can.

If we already can infer this, can we put there the appropriate assertion?

Ok, I've added the appropriate clang_analyzer_eval to check this.

[steakhal]

Awesome!
So clean, and I also like the tests.
Good job.

clang/test/Analysis/solver-sym-simplification-adjustment.c

59

Please assert clang_analyzer_eval(c == 0) as well.

[martong]

Thanks for the assiduous review guys!

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

public:
 
   LLVM_NODISCARD static inline Optional<bool> areEqual(ProgramStateRef State,
                                                        EquivalenceClass First,
                                                        EquivalenceClass Second);
   LLVM_NODISCARD static inline Optional<bool>
   areEqual(ProgramStateRef State, SymbolRef First, SymbolRef Second);
 
   /// Iterate over all symbols and try to simplify them.
-  LLVM_NODISCARD static inline ProgramStateRef simplify(SValBuilder &SVB,
-                                                        RangeSet::Factory &F,
-                                                        ProgramStateRef State,
-                                                        EquivalenceClass Class);
+  LLVM_NODISCARD static inline ProgramStateRef
+  simplify(SValBuilder &SVB, RangeSet::Factory &F, RangedConstraintManager &RCM,
+           ProgramStateRef State, EquivalenceClass Class);
 
   void dumpToStream(ProgramStateRef State, raw_ostream &os) const;
   LLVM_DUMP_METHOD void dump(ProgramStateRef State) const {
     dumpToStream(State, llvm::errs());
   }
 
   /// Check equivalence data for consistency.
   LLVM_NODISCARD LLVM_ATTRIBUTE_UNUSED static bool

 
 bool ConstraintAssignor::assignSymExprToConst(const SymExpr *Sym,
                                               const llvm::APSInt &Constraint) {
   llvm::SmallSet<EquivalenceClass, 4> SimplifiedClasses;
   // Iterate over all equivalence classes and try to simplify them.
   ClassMembersTy Members = State->get<ClassMembers>();
   for (std::pair<EquivalenceClass, SymbolSet> ClassToSymbolSet : Members) {
     EquivalenceClass Class = ClassToSymbolSet.first;
-    State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);
+    State =
+        EquivalenceClass::simplify(Builder, RangeFactory, RCM, State, Class);
     if (!State)
       return false;
     SimplifiedClasses.insert(Class);
   }
 
   // Trivial equivalence classes (those that have only one symbol member) are
   // not stored in the State. Thus, we must skim through the constraints as
   // well. And we try to simplify symbols in the constraints.
   ConstraintRangeTy Constraints = State->get<ConstraintRange>();
   for (std::pair<EquivalenceClass, RangeSet> ClassConstraint : Constraints) {
     EquivalenceClass Class = ClassConstraint.first;
     if (SimplifiedClasses.count(Class)) // Already simplified.
       continue;
-    State = EquivalenceClass::simplify(Builder, RangeFactory, State, Class);
+    State =
+        EquivalenceClass::simplify(Builder, RangeFactory, RCM, State, Class);
     if (!State)
       return false;
   }
 
   return true;
 }
 
 bool ConstraintAssignor::assignSymSymExprToRangeSet(const SymSymExpr *Sym,
inline Optional<bool> EquivalenceClass::areEqual(ProgramStateRef State,
   return llvm::None;
 }
 
 // Iterate over all symbols and try to simplify them. Once a symbol is
 // simplified then we check if we can merge the simplified symbol's equivalence
 // class to this class. This way, we simplify not just the symbols but the
 // classes as well: we strive to keep the number of the classes to be the
 // absolute minimum.
-LLVM_NODISCARD ProgramStateRef
-EquivalenceClass::simplify(SValBuilder &SVB, RangeSet::Factory &F,
-                           ProgramStateRef State, EquivalenceClass Class) {
+LLVM_NODISCARD ProgramStateRef EquivalenceClass::simplify(
+    SValBuilder &SVB, RangeSet::Factory &F, RangedConstraintManager &RCM,
   SymbolSet ClassMembers = Class.getClassMembers(State);
   for (const SymbolRef &MemberSym : ClassMembers) {
 
     const SVal SimplifiedMemberVal = simplifyToSVal(State, MemberSym);
     const SymbolRef SimplifiedMemberSym = SimplifiedMemberVal.getAsSymbol();
 
     // The symbol is collapsed to a constant, check if the current State is
     // still feasible.
     if (const auto CI = SimplifiedMemberVal.getAs<nonloc::ConcreteInt>()) {
       const llvm::APSInt &SV = CI->getValue();
       const RangeSet *ClassConstraint = getConstraint(State, Class);
       // We have found a contradiction.
       if (ClassConstraint && !ClassConstraint->contains(SV))
         return nullptr;
     }
 
     if (SimplifiedMemberSym && MemberSym != SimplifiedMemberSym) {
       // The simplified symbol should be the member of the original Class,
       // however, it might be in another existing class at the moment. We
       // have to merge these classes.
+      ProgramStateRef OldState = State;
       State = merge(F, State, MemberSym, SimplifiedMemberSym);
       if (!State)
         return nullptr;
+      // No state change, no merge happened actually.
+      if (OldState == State)
+        continue;
+
+      // Initiate the reorganization of the equality information. E.g., if we
+      // have `c + 1 == 0` then we'd like to express that `c == -1`. It makes
+      // sense to do this only with `SymIntExpr`s.
+      // TODO Handle `IntSymExpr` as well, once computeAdjustment can handle
+      // them.
+      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SimplifiedMemberSym)) {
+        if (const RangeSet *ClassConstraint = getConstraint(State, Class)) {
+          // Overestimate the individual Ranges with the RangeSet' lowest and
+          // highest values.
+          State = RCM.assumeSymInclusiveRange(
+              State, SIE, ClassConstraint->getMinValue(),
+              ClassConstraint->getMaxValue(), /*InRange=*/true);
+          if (!State)
+            return nullptr;
+        }
+      }
     }
   }
   return State;
 }
 
 inline ClassSet EquivalenceClass::getDisequalClasses(ProgramStateRef State,
                                                      SymbolRef Sym) {
   return find(State, Sym).getDisequalClasses(State);

clang/test/Analysis/solver-sym-simplification-adjustment.c

+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=false \
+// RUN:   -verify
+
+void clang_analyzer_warnIfReached();
+void clang_analyzer_eval();
+
+void test_simplification_adjustment_concrete_int(int b, int c) {
+  if (b < 0 || b > 1)  // b: [0,1]
+    return;
+  if (c < -1 || c > 1) // c: [-1,1]
+    return;
+  if (c + b != 0)      // c + b == 0
+    return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1)          // b == 1  --> c + 1 == 0 --> c == -1
+    return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);   // expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_range(int b, int c) {
+  if (b < 0 || b > 1)              // b: [0,1]
+    return;
+  if (c < -1 || c > 1)             // c: [-1,1]
+    return;
+  if (c + b < -1 || c + b > 0)     // c + b: [-1,0]
+    return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)                      // b == 1  --> c + 1: [-1,0] --> c: [-2,-1]
+    return;
+                                   // c: [-2,-1] is intersected with the
+                                   // already associated range which is [-1,1],
+                                   // thus we get c: [-1,-1]
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  clang_analyzer_eval(c == -1);    // expected-warning{{TRUE}}
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeasible_concrete_int(int b, int c) {
+  if (b < 0 || b > 1) // b: [0,1]
+    return;
+  if (c < 0 || c > 1) // c: [0,1]
+    return;
+  if (c + b != 0)     // c + b == 0
+    return;
+  clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (b != 1) {       // b == 1  --> c + 1 == 0 --> c == -1 contradiction
+    clang_analyzer_eval(b == 0);  // expected-warning{{TRUE}}
+    clang_analyzer_eval(c == 0);  // expected-warning{{TRUE}}
+    // Keep the symbols and the constraints! alive.
+    (void)(b * c);
+    return;
+  }
+  clang_analyzer_warnIfReached(); // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjustment_to_infeassible_range(int b, int c) {
+  if (b < 0 || b > 1)              // b: [0,1]
+    return;
+  if (c < 0 || c > 1)              // c: [0,1]
+    return;
+  if (c + b < -1 || c + b > 0)     // c + b: [-1,0]
+    return;
+  clang_analyzer_warnIfReached();  // expected-warning{{REACHABLE}}
+  if (b != 1)                      // b == 1  --> c + 1: [-1,0] --> c: [-2,-1] contradiction
+    return;
+  clang_analyzer_warnIfReached();  // no warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_adjusment_no_infinite_loop(int a, int b, int c) {
+  if (a == b)        // a != b
+    return;
+  if (c != 0)        // c == 0
+    return;
+
+  if (b != 0)        // b == 0
+    return;
+  // The above simplification of `b == 0` could result in an infinite loop
+  // unless we detect that the State is unchanged.
+  // The loop:
+  // 1) Simplification of the trivial equivalence class
+  //      "symbol": "(reg_$0<int a>) == (reg_$1<int b>)", "range": "{ [0, 0] }"
+  //    results in
+  //      "symbol": "(reg_$0<int a>) == 0", "range": "{ [0, 0] }" }
+  //    which in turn creates a non-trivial equivalence class
+  //      [ "(reg_$0<int a>) == (reg_$1<int b>)", "(reg_$0<int a>) == 0" ]
+  // 2) We call assumeSymInclusiveRange("(reg_$0<int a>) == 0")
+  //    and that calls **simplify** on the associated non-trivial equivalence
+  //    class. During the simplification the State does not change, we reached
+  //    the fixpoint.
+
+  (void)(a * b * c);
+}