[analyzer][solver] Handle simplification to ConcreteInt

[martong]

Summary

The solver's symbol simplification mechanism was not able to handle cases
when a symbol is simplified to a concrete integer. This patch adds the
capability.

E.g., in the attached lit test case, the original symbol is c + 1 and
it has a [0, 0] range associated with it. Then, a new condition c == 0
is assumed, so a new range constraint [0, 0] comes in for c and
simplification kicks in. c + 1 becomes 0 + 1, but the associated
range is [0, 0], so now we are able to realize the contradiction.

[steakhal]

The patch seems reasonable, but I will need slightly more time to digest it.
I'll get back to this.

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

391–400

I'm confused about which comment corresponds to which function.
You should also signify the difference between the two APIs.

Shouldn't be one of them an implementation detail? If so, why do we have the same visibility?

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

23

Could we have an eval(c == -1) // TRUE?
Also, please disable eager bifurcation to prevent state-splits in the eval arguments.

[martong]

• Add better comments to simplify functions
• Add a new check and explanation to the test file

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

391–400

Shouldn't be one of them an implementation detail? If so, why do we have the same visibility?

No, we use both of them. simplify that always returns a symbol is used e.g. in RangedConstraintManager::assumeSym.

And we use simplifyToSVal directly in EquivalenceClass::simplify.

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

23

Actually, it is eval(c == -1) // FALSE that holds.

This is because after the simplification with b==1 we have a constraint c+1==0 but we do not reorder this equality to c==-1. Besides we have another constraint that we inherited from a previous State, this is c: [0, 1]. Now, when you query c==-1 then the latter constraint is found, thus resulting in an infeasible state, so you'll receive FALSE in the warning. Actually, these are the constraints after line 19:

"constraints": [
  { "symbol": "(reg_$1<int c>) + (reg_$0<int b>)", "range": "{ [0, 0] }" },
  { "symbol": "(reg_$1<int c>) + 1", "range": "{ [0, 0] }" },
  { "symbol": "reg_$0<int b>", "range": "{ [1, 1] }" },
  { "symbol": "reg_$1<int c>", "range": "{ [0, 1] }" }
],

I am considering to create a follow-up patch, where the reordering of c+1==0 to c==-1 is done (perhaps by reusing RangedConstraintManager::assumeSymRel).

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2114

We usually use R or RS. It gets readability better IMO.

2117–2119

What prevents you to not put this stuff inside ento::simplify. I think it should perfectly fit in there.

[ASDenysPetrov]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2109–2123

UPD. I mean all this new snippet.

[martong]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2114

There are many other cases in this file where we spell out ClassConstraint, e.g. in mergeImpl we have NewClassConstraint. Also, I think the name ClassConstraint is telling way more than RS, so I'd like to keep this name.

2117–2119

ento::simplify is at a different abstraction level, it works on a SymbolRef and the SVal associated to it; and it uses the SValBuilder to achieve the desired constant folding. We have absolutely no knowledge about the equivalence classes there.

[martong]

• Make the test case way simpler (and independent from other solver patches)

[martong]

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

23

I've just updated the test case to be way more direct and simple.

[steakhal]

Looks good to me. I very much like this.
Check my nits inline. Given those are fixed I'm gonna accept this.

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

392–400

Okay, I like it!
However, it's still not entirely clear to me *when* to use which.
Could you clarify that aspect too?
Sorry for being picky but I'm not an expert on this part of the code and if it's not clear to me, it probably won't be clear to newcomers either.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2110

By initializing it here, it will be much cleaner:

1. It's not mutated, thus it can be const
2. We can spare the else branch.

Also consider marking the rest of the variables const, so that the lack of constness would actually suggest mutability.

2112

I think a comment would be appreciated describing that we only look for infeasibility here, nothing else.
Thus, the fallthrough in the feasible case is intentional.

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

18

Consider following the convention and using the // no-warning comment instead.
I'm also requesting an additional test case, exercising the fallthrough behavior I stated in an earlier comment.

[martong]

• Use getAsSymbol to initialize the simplified member symbol
• Add some more explanation to ento::simplify
• Add a comment about checking only feasiblity
• Add a new test case for the "fallthrough"

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

392–400

Okay, I've added the following comment (though this feels a bit too mouthful for me):

/// ... We use this function in the family of assumeSymNE/EQ/LT/../GE
/// functions where we can work only with symbols. Use the other function
/// (simplifyToSVal) if you are interested in a simplification that may yield
/// a concrete constant value.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

2110

Good point! I've made the suggested change.

2112

Ok, I've added a comment for that.

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

18

Okay, makes sense. I've added a new test case.

[steakhal]

I love this! The coverage is great and looks good.

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

virtual ProgramStateRef assumeSymOutsideInclusiveRange(
       const llvm::APSInt &To, const llvm::APSInt &Adjustment) = 0;
 
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 private:
   static void computeAdjustment(SymbolRef &Sym, llvm::APSInt &Adjustment);
 };
 
-/// Try to simplify a given symbolic expression's associated value based on the
-/// constraints in State. This is needed because the Environment bindings are
-/// not getting updated when a new constraint is added to the State.
+/// Try to simplify a given symbolic expression based on the constraints in
+/// State. This is needed because the Environment bindings are not getting
+/// updated when a new constraint is added to the State. If the symbol is
+/// simplified to a non-symbol (e.g. to a constant) then the original symbol
+/// is returned. We use this function in the family of assumeSymNE/EQ/LT/../GE
+/// functions where we can work only with symbols. Use the other function
+/// (simplifyToSVal) if you are interested in a simplification that may yield
+/// a concrete constant value.
 SymbolRef simplify(ProgramStateRef State, SymbolRef Sym);
 
+/// Try to simplify a given symbolic expression's associated `SVal` based on the
+/// constraints in State. This is very similar to `simplify`, but this function
+/// always returns the simplified SVal. The simplified SVal might be a single
+/// constant (i.e. `ConcreteInt`).
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym);
+
 } // namespace ento
 } // namespace clang
 
 REGISTER_FACTORY_WITH_PROGRAMSTATE(ConstraintMap)
 
 #endif

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 // 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) {
   SymbolSet ClassMembers = Class.getClassMembers(State);
   for (const SymbolRef &MemberSym : ClassMembers) {
-    SymbolRef SimplifiedMemberSym = ento::simplify(State, MemberSym);
+
+    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.
       State = merge(F, State, MemberSym, SimplifiedMemberSym);
       if (!State)
         return nullptr;
     }
   }

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

if (Op == BO_Add || Op == BO_Sub) {
       // This should happen /after/ promotion, in case the value being
       // subtracted is, say, CHAR_MIN, and the promoted type is 'int'.
       if (Op == BO_Sub)
         Adjustment = -Adjustment;
     }
   }
 }
 
-SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+SVal simplifyToSVal(ProgramStateRef State, SymbolRef Sym) {
   SValBuilder &SVB = State->getStateManager().getSValBuilder();
-  SVal SimplifiedVal = SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+  return SVB.simplifySVal(State, SVB.makeSymbolVal(Sym));
+}
+
+SymbolRef simplify(ProgramStateRef State, SymbolRef Sym) {
+  SVal SimplifiedVal = simplifyToSVal(State, Sym);
   if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
     return SimplifiedSym;
   return Sym;
 }
 
 } // end of namespace ento
 } // end of namespace clang

clang/test/Analysis/solver-sym-simplification-concreteint.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_to_concrete_int_infeasible(int b, int c) {
+  if (c + b != 0)     // c + b == 0
+    return;
+  if (b != 1)         // b == 1  --> c + 1 == 0
+    return;
+  if (c != 1)         // c == 1  --> 1 + 1 == 0 contradiction
+    return;
+  clang_analyzer_warnIfReached(); // no-warning
+
+  // Keep the symbols and the constraints! alive.
+  (void)(b * c);
+  return;
+}
+
+void test_simplification_to_concrete_int_feasible(int b, int c) {
+  if (c + b != 0)
+    return;
+                      // c + b == 0
+  if (b != 1)
+    return;
+                      // b == 1   -->  c + 1 == 0
+  if (c != -1)
+    return;
+                      // c == -1  --> -1 + 1 == 0 OK
+  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;
+}