[analyzer][solver] Prevent use of a null state

[vsavchenko]

Summary

rdar://77686137

[steakhal]

Dam, we will be always haunted by these.
Looks good btw.
The test looks somewhat artificial - like a raw creduce result.

Do you think It worth the effort to make it look like it was written by a human?
I also somewhy prefer function parameters to globals for this specific use-case.

This seems to depend on the -analyzer-config eagerly-assume=true. We should probably add this option explicitly, just in case.

[vsavchenko]

Modify test

[vsavchenko]

In D102240#2750976, @steakhal wrote:

Dam, we will be always haunted by these.

Yep, it was one place where we didn't expect a null state, but after one of the later patches, it became possible. 🤞it's the final one.

Looks good btw.
The test looks somewhat artificial - like a raw creduce result.

Do you think It worth the effort to make it look like it was written by a human?

OK, I tried. and surprisingly I couldn't transform c == b into a condition, so it crashes. While it's interesting why exactly this happens, I don't think that it's worth it (in this particular case).

I also somewhy prefer function parameters to globals for this specific use-case.

✅

This seems to depend on the -analyzer-config eagerly-assume=true. We should probably add this option explicitly, just in case.

✅

[steakhal]

In D102240#2756967, @vsavchenko wrote:

I couldn't transform c == b into a condition, so it crashes.

Well, that's interesting. It might worth investigating. @NoQ ?
Regardless, it's an improvement, let's land it :D

[NoQ]

Thx for the fix!

In D102240#2757223, @steakhal wrote:

In D102240#2756967, @vsavchenko wrote:

I couldn't transform c == b into a condition, so it crashes.

Well, that's interesting. It might worth investigating. @NoQ ?
Regardless, it's an improvement, let's land it :D

At a glance it looks like this has something to do with liveness. When c == b is surrounded by an if-statement, the CFG starts having more blocks and live variables analysis becomes more fine-grained and constraints for 'b' get cleaned up more quickly. Which is bad because this means that we're cleaning up constraints that are still useful.

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

private:
   template <bool EQ>
   ProgramStateRef track(RangeSet NewConstraint, ProgramStateRef State,
                         SymbolRef Sym, const llvm::APSInt &Int,
                         const llvm::APSInt &Adjustment) {
     if (NewConstraint.isEmpty())
       // This is an infeasible assumption.
       return nullptr;
 
-    ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint);
+    if (ProgramStateRef NewState = setConstraint(State, Sym, NewConstraint)) {
       if (auto Equality = EqualityInfo::extract(Sym, Int, Adjustment)) {
         // If the original assumption is not Sym + Adjustment !=/</> Int,
         // we should invert IsEquality flag.
         Equality->IsEquality = Equality->IsEquality != EQ;
         return track(NewState, *Equality);
       }
 
       return NewState;
     }
 
+    return nullptr;
+  }
+
   ProgramStateRef track(ProgramStateRef State, EqualityInfo ToTrack) {
     if (ToTrack.IsEquality) {
       return trackEquality(State, ToTrack.Left, ToTrack.Right);
     }
     return trackDisequality(State, ToTrack.Left, ToTrack.Right);
   }
 
   ProgramStateRef trackDisequality(ProgramStateRef State, SymbolRef LHS,

clang/test/Analysis/PR50268.c

+// RUN: %clang_analyze_cc1 -w -analyzer-checker=core -verify %s \
+// RUN:    -analyzer-config eagerly-assume=true
+
+// expected-no-diagnostics
+
+
+int test(unsigned long a, unsigned long c, int b) {
+  c -= a;
+  if (0 >= b) {}
+  c == b;
+  return c ? 0 : 2; // no-crash
+}