[analyzer][Solver] Early return if sym is concrete on assuming (#115579)

This could deduce some complex syms derived from simple ones whose
values could be constrainted to be concrete during execution, thus
reducing some overconstrainted states.

This commit also fix `unix.StdCLibraryFunctions` crash due to these
overconstrainted states being added to the graph, which is marked as
sink node (PosteriorlyOverconstrained). The 'assume' API is used in
non-dual style so the checker should protectively test whether these
newly added nodes are actually impossible.

1. The crash: https://godbolt.org/z/8KKWeKb86
2. The solver needs to solve equivalent: https://godbolt.org/z/ed8WqsbTh

clang/lib/StaticAnalyzer/Checkers/StdLibraryFunctionsChecker.cpp

@@ -1354,6 +1354,8 @@ void StdLibraryFunctionsChecker::checkPreCall(const CallEvent &Call,
             if (BR.isInteresting(ArgSVal))
               OS << Msg;
           }));
+      if (NewNode->isSink())
+        break;
     }
   }
 }

clang/lib/StaticAnalyzer/Core/ConstraintManager.cpp

@@ -74,7 +74,7 @@ ConstraintManager::assumeDualImpl(ProgramStateRef &State,
       // it might happen that a Checker uncoditionally uses one of them if the
       // other is a nullptr. This may also happen with the non-dual and
       // adjacent `assume(true)` and `assume(false)` calls. By implementing
-      // assume in therms of assumeDual, we can keep our API contract there as
+      // assume in terms of assumeDual, we can keep our API contract there as
       // well.
       return ProgramStatePair(StInfeasible, StInfeasible);
     }

clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

@@ -23,7 +23,14 @@ RangedConstraintManager::~RangedConstraintManager() {}
 ProgramStateRef RangedConstraintManager::assumeSym(ProgramStateRef State,
                                                    SymbolRef Sym,
                                                    bool Assumption) {
-  Sym = simplify(State, Sym);
+  SVal SimplifiedVal = simplifyToSVal(State, Sym);
+  if (SimplifiedVal.isConstant()) {
+    bool Feasible = SimplifiedVal.isZeroConstant() != Assumption;
+    return Feasible ? State : nullptr;
+  }
+
+  if (SymbolRef SimplifiedSym = SimplifiedVal.getAsSymbol())
+    Sym = SimplifiedSym;
 
   // Handle SymbolData.
   if (isa<SymbolData>(Sym))

clang/test/Analysis/solver-sym-simplification-on-assumption.c

@@ -0,0 +1,37 @@
+// RUN: %clang_analyze_cc1 -triple=x86_64-unknown-linux-gnu %s \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+void clang_analyzer_eval(int);
+void clang_analyzer_value(int);
+
+void test_derived_sym_simplification_on_assume(int s0, int s1) {
+  int elem = s0 + s1 + 1;
+  if (elem-- == 0)
+    return;
+
+  if (elem-- == 0)
+    return;
+
+  if (s0 < 1)
+    return;
+  clang_analyzer_value(s0); // expected-warning{{[1, 2147483647]}}
+
+  if (s1 < 1)
+    return;
+  clang_analyzer_value(s1); // expected-warning{{[1, 2147483647]}}
+
+  clang_analyzer_eval(elem); // expected-warning{{UNKNOWN}}
+  if (elem-- == 0)
+    return;
+
+  if (s0 > 1)
+    return;
+  clang_analyzer_eval(s0 == 1); // expected-warning{{TRUE}}
+
+  if (s1 > 1)
+    return;
+  clang_analyzer_eval(s1 == 1); // expected-warning{{TRUE}}
+
+  clang_analyzer_eval(elem); // expected-warning{{FALSE}}
+}

clang/test/Analysis/std-c-library-functions-bufsize-nocrash-with-correct-solver.c

@@ -0,0 +1,43 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-max-loop 6 \
+// RUN:   -analyzer-checker=unix.StdCLibraryFunctions \
+// RUN:   -analyzer-config unix.StdCLibraryFunctions:ModelPOSIX=true \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -triple x86_64-unknown-linux-gnu \
+// RUN:   -verify
+
+#include "Inputs/std-c-library-functions-POSIX.h"
+
+void clang_analyzer_value(int);
+void clang_analyzer_warnIfReached();
+void clang_analyzer_printState();
+
+void _add_one_to_index_C(int *indices, int *shape) {
+  int k = 1;
+  for (; k >= 0; k--)
+    if (indices[k] < shape[k])
+      indices[k]++;
+    else
+      indices[k] = 0;
+}
+
+void PyObject_CopyData_sptr(char *i, char *j, int *indices, int itemsize,
+    int *shape, struct sockaddr *restrict sa) {
+  int elements = 1;
+  for (int k = 0; k < 2; k++)
+    elements += shape[k];
+
+  // no contradiction after 3 iterations when 'elements' could be
+  // simplified to 0
+  int iterations = 0;
+  while (elements--) {
+    iterations++;
+    _add_one_to_index_C(indices, shape);
+    getnameinfo(sa, 10, i, itemsize, i, itemsize, 0); // no crash here
+  }
+
+  if (shape[0] == 1 && shape[1] == 1 && indices[0] == 0 && indices[1] == 0) {
+    clang_analyzer_value(iterations == 3 && elements == -1);
+    // expected-warning@-1{{1}}
+  }
+}

clang/test/Analysis/symbol-simplification-fixpoint-two-iterations.cpp

@@ -28,13 +28,13 @@ void test(int a, int b, int c, int d) {
     return;
   clang_analyzer_printState();
   // CHECK:       "constraints": [
-  // CHECK-NEXT:    { "symbol": "(reg_$0<int a>) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
+  // CHECK-NEXT:    { "symbol": "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)", "range": "{ [0, 0] }" },
   // CHECK-NEXT:    { "symbol": "reg_$1<int b>", "range": "{ [0, 0] }" },
   // CHECK-NEXT:    { "symbol": "reg_$2<int c>", "range": "{ [0, 0] }" }
   // CHECK-NEXT:  ],
   // CHECK-NEXT:  "equivalence_classes": [
-  // CHECK-NEXT:    [ "(reg_$0<int a>) != (reg_$3<int d>)" ],
+  // CHECK-NEXT:    [ "((reg_$0<int a>) + (reg_$2<int c>)) != (reg_$3<int d>)" ],
-  // CHECK-NEXT:    [ "reg_$0<int a>", "reg_$3<int d>" ],
+  // CHECK-NEXT:    [ "(reg_$0<int a>) + (reg_$2<int c>)", "reg_$3<int d>" ],
   // CHECK-NEXT:    [ "reg_$2<int c>" ]
   // CHECK-NEXT:  ],
   // CHECK-NEXT:  "disequality_info": null,