[StaticAnalyzer] early return if sym is concrete on assuming

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.

Author: danix800

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 : 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,31 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=debug.ExprInspection \
+// RUN:   -verify
+
+void clang_analyzer_eval(int);
+
+void test_derived_sym_simplification_on_assume(int s0, int s1) {
+  int elem = s0 + s1 + 1;
+  if (elem-- == 0) // elem = s0 + s1
+    return;
+
+  if (elem-- == 0) // elem = s0 + s1 - 1
+    return;
+
+  if (s0 < 1) // s0: [1, 2147483647]
+    return;
+  if (s1 < 1) // s0: [1, 2147483647]
+    return;
+
+  if (elem-- == 0) // elem = s0 + s1 - 2
+    return;
+
+  if (s0 > 1) // s0: [-2147483648, 0] U [1, 2147483647] => s0 = 0
+    return;
+
+  if (s1 > 1) // s1: [-2147483648, 0] U [1, 2147483647] => s1 = 0
+    return;
+
+  // elem = s0 + s1 - 2 should be 0
+  clang_analyzer_eval(elem); // expected-warning{{FALSE}}
+}

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

@@ -0,0 +1,33 @@
+// RUN: %clang_analyze_cc1 %s \
+// 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
+
+// expected-no-diagnostics
+
+#include "Inputs/std-c-library-functions-POSIX.h"
+
+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
+  while (elements--) {
+    _add_one_to_index_C(indices, shape);
+    getnameinfo(sa, 10, i, itemsize, i, itemsize, 0);
+  }
+}

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_$3<int d>" ],
+  // CHECK-NEXT:    [ "((reg_$0<int a>) + (reg_$2<int c>)) != (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,