[analyzer] Add more information to the Exploded Graph

[isuckatcs]

Summary

During non-POD array construction and destruction we store additional data in the program state.

Right now only the index of the actual element being constructed is dumped into the egraph in case
of simple construction invoked by CXXConstructExpr.

This patch dumps information about pending ArrayInitLoopExprs and destructors.

Depends on: D130737

The resulting nodes:

[isuckatcs]

Updated

[NoQ]

Beautiful!!

I think we should add an exploded-graph-rewriter test in which these new traits aren't null.

At this point, with all these Environment-like traits, maybe we can combine them into a single table? (Would be a separate patch).

----
Environment:

  #0 Call S::S (test.cpp:16:19)
    Expressions:
      S1002  .x  &Element{arr,0 S64b,struct S}.x
      S1008  .x  1 S32b

   #1 Call main
      Expressions:
        S967   arr     &arr
        S9088  arr[*]  &Element{arr,0S64b,struct S}
      Objects Under Construction:
        S1058  (construct into local variable)  auto = {arr[*]}  &Element{NonParamVarRegion{D952},0 S64b,struct S}
      Indices Of Elements Under Construction:
        S1018  (Cur: 0)  CXXConstructExpr <test.cpp:16:19, col:10>  'S'  Next: 1
      Pending Array Init Loop Expressions:
        S1018            CXXConstructExpr <test.cpp:16:19, col:10>  'S'  Size: 2
----

clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot

76–84

It may also make sense to drop the : null traits entirely and have the python script treat it as the default value, this may win like 10% performance at this point. Not necessarily worth it given that the primary bottleneck is still the viewer.

[xazax.hun]

Very minor nit: In the construction we have "Size" in the destruction we have "Size of the array". Is it the case that the first size is the flattened size the second in is the currently destroyed array's size only? (I.e., not modified by nesting.) If that is the case, I think the name of the field could be clearer for the ArrayInitLoopExprs, like "Flattened size".

[isuckatcs]

• Rebased
• Updated how the information is displayed.
• Updated the screenshots of the nodes in the description to reflect the changes.

[isuckatcs]

Empty traits are no longer dumped. This also solves the reverse compatibility issue caused by D127973.

[xazax.hun]

clang/lib/StaticAnalyzer/Core/ExprEngine.cpp

778

Nit: is there any reason to have a string literal here instead of a character literal?

783

Same as above.

810

Same as above, and for a few other locations below.

[isuckatcs]

clang/lib/StaticAnalyzer/Core/ExprEngine.cpp

778

I though the code will look more uniform like this. Are there cons of using a string literal instead of a character literal here?

[xazax.hun]

clang/lib/StaticAnalyzer/Core/ExprEngine.cpp

778

Piping a character is more efficient. A string literal decays to a pointer that needs to be dereferenced and we also need to store the closing null character. Passing a literal will save us storing the closing null and the dereference. Although we are on a path where we do IO, so micro-optimizations like this make little difference (if anything at all). So, I'm also fine with the uniformity argument.

[isuckatcs]

Replaced one length string literals with char literals

[isuckatcs]

Added a new test case where the program states are not empty in the dot files

[NoQ]

Thanks a lot!!

clang/lib/StaticAnalyzer/Core/ExprEngine.cpp

if (HasItem)
     Indent(Out, --Space, IsDot) << ']'; // End of "location_context".
   else {
     Out << "null ";
   }
 }
 
 static void printIndicesOfElementsToConstructJson(
     raw_ostream &Out, ProgramStateRef State, const char *NL,
-    const LocationContext *LCtx, const ASTContext &Context,
-    unsigned int Space = 0, bool IsDot = false) {
+    const LocationContext *LCtx, unsigned int Space = 0, bool IsDot = false) {
   using KeyT = std::pair<const Expr *, const LocationContext *>;
 
-  PrintingPolicy PP =
-      LCtx->getAnalysisDeclContext()->getASTContext().getPrintingPolicy();
+  const auto &Context = LCtx->getAnalysisDeclContext()->getASTContext();
+  PrintingPolicy PP = Context.getPrintingPolicy();
 
   ++Space;
   bool HasItem = false;
 
   // Store the last key.
   KeyT LastKey;
   for (const auto &I : State->get<IndexOfElementToConstruct>()) {
     const KeyT &Key = I.first;
for (const auto &I : State->get<IndexOfElementToConstruct>()) {
     Out << "\"" << E->getStmtClassName() << " "
         << E->getSourceRange().printToString(Context.getSourceManager()) << " '"
         << QualType::getAsString(E->getType().split(), PP);
     Out << "'\"";
 
     Out << ", \"value\": \"Next: " << Value << "\" }";
 
     if (Key != LastKey)
       Out << ',';
     Out << NL;
   }
 
   if (HasItem)
     Indent(Out, --Space, IsDot) << ']'; // End of "location_context".
   else {
     Out << "null ";
   }
 }
 
-void ExprEngine::printJson(raw_ostream &Out, ProgramStateRef State,
-                           const LocationContext *LCtx, const char *NL,
-                           unsigned int Space, bool IsDot) const {
-  Indent(Out, Space, IsDot) << "\"constructing_objects\": ";
+static void printPendingInitLoopJson(raw_ostream &Out, ProgramStateRef State,
+                                     const char *NL,
+                                     const LocationContext *LCtx,
+                                     unsigned int Space = 0,
+                                     bool IsDot = false) {
+  using KeyT = std::pair<const CXXConstructExpr *, const LocationContext *>;
+
+  const auto &Context = LCtx->getAnalysisDeclContext()->getASTContext();
+  PrintingPolicy PP = Context.getPrintingPolicy();
 
-  if (LCtx && !State->get<ObjectsUnderConstruction>().isEmpty()) {
-    ++Space;
-    Out << '[' << NL;
-    LCtx->printJson(Out, NL, Space, IsDot, [&](const LocationContext *LC) {
-      printObjectsUnderConstructionJson(Out, State, NL, LC, Space, IsDot);
-    });
+  bool HasItem = false;
 
-    --Space;
-    Indent(Out, Space, IsDot) << "]," << NL; // End of "constructing_objects".
-  } else {
-    Out << "null," << NL;
+  // Store the last key.
+  KeyT LastKey;
+  for (const auto &I : State->get<PendingInitLoop>()) {
+    const KeyT &Key = I.first;
+    if (Key.second != LCtx)
+      continue;
+
+    if (!HasItem) {
+      Out << "[" << NL;
+      HasItem = true;
+    }
+
+    LastKey = Key;
   }
 
-  Indent(Out, Space, IsDot) << "\"index_of_element\": ";
-  if (LCtx && !State->get<IndexOfElementToConstruct>().isEmpty()) {
-    ++Space;
+  for (const auto &I : State->get<PendingInitLoop>()) {
+    const KeyT &Key = I.first;
+    unsigned Value = I.second;
+    if (Key.second != LCtx)
+      continue;
+
+    Indent(Out, Space, IsDot) << "{ ";
+
+    const CXXConstructExpr *E = Key.first;
+    Out << "\"stmt_id\": " << E->getID(Context);
+
+    Out << ", \"kind\": null";
+    Out << ", \"pretty\": ";
+    Out << "\"" << E->getStmtClassName() << " "
+        << E->getSourceRange().printToString(Context.getSourceManager()) << " '"
+        << QualType::getAsString(E->getType().split(), PP);
+    Out << "'\"";
+
+    Out << ", \"value\": \"Size: " << Value << "\"}";
+
+    if (Key != LastKey)
+      Out << ',';
+    Out << NL;
+  }
+
+  if (HasItem)
+    Indent(Out, --Space, IsDot) << ']'; // End of "location_context".
+  else {
+    Out << "null ";
+  }
+}
+
+static void
+printPendingArrayDestructionsJson(raw_ostream &Out, ProgramStateRef State,
+                                  const char *NL, const LocationContext *LCtx,
+                                  unsigned int Space = 0, bool IsDot = false) {
+  using KeyT = const LocationContext *;
+
+  bool HasItem = false;
+
+  // Store the last key.
+  KeyT LastKey = nullptr;
+  for (const auto &I : State->get<PendingArrayDestruction>()) {
+    const KeyT &Key = I.first;
+    if (Key != LCtx)
+      continue;
+
+    if (!HasItem) {
+      Out << "[" << NL;
+      HasItem = true;
+    }
+
+    LastKey = Key;
+  }
+
+  for (const auto &I : State->get<PendingArrayDestruction>()) {
+    const KeyT &Key = I.first;
+    PendingArrayDestructionData Value = I.second;
+    if (Key != LCtx)
+      continue;
 
-    auto &Context = getContext();
+    Indent(Out, Space, IsDot) << "{ ";
+
+    Out << "\"stmt_id\": null";
+    Out << ", \"kind\": null";
+    Out << ", \"pretty\": \"Current index: " << Value.size - Value.idx << "\"";
+    Out << ", \"value\": \"Size of the array: " << Value.size << "\" }";
+
+    if (Key != LastKey)
+      Out << ',';
+    Out << NL;
+  }
+
+  if (HasItem)
+    Indent(Out, --Space, IsDot) << ']'; // End of "location_context".
+  else {
+    Out << "null ";
+  }
+}
+
+/// A helper function to generalize program state trait printing.
+/// The function invokes Printer as 'Printer(Out, State, NL, LC, Space, IsDot,
+/// std::forward<Args>(args)...)'. \n One possible type for Printer is
+/// 'void()(raw_ostream &, ProgramStateRef, const char *, const LocationContext
+/// *, unsigned int, bool, ...)' \n \param Trait The state trait to be printed.
+/// \param Printer A void function that prints Trait.
+/// \param Args An additional parameter pack that is passed to Print upon
+/// invocation.
+template <typename Trait, typename Printer, typename... Args>
+static void printStateTraitWithLocationContextJson(
+    raw_ostream &Out, ProgramStateRef State, const LocationContext *LCtx,
+    const char *NL, unsigned int Space, bool IsDot,
+    const char *jsonPropertyName, Printer printer, Args &&...args) {
+
+  using RequiredType =
+      void (*)(raw_ostream &, ProgramStateRef, const char *,
+               const LocationContext *, unsigned int, bool, Args &&...);
+
+  // Try to do as much compile time checking as possible.
+  // FIXME: check for invocable instead of function?
+  static_assert(std::is_function<std::remove_pointer_t<Printer>>::value,
+                "Printer is not a function!");
+  static_assert(std::is_convertible<Printer, RequiredType>::value,
+                "Printer doesn't have the required type!");
+
+  Indent(Out, Space, IsDot) << "\"" << jsonPropertyName << "\": ";
+  if (LCtx && !State->get<Trait>().isEmpty()) {
+    ++Space;
     Out << '[' << NL;
     LCtx->printJson(Out, NL, Space, IsDot, [&](const LocationContext *LC) {
-      printIndicesOfElementsToConstructJson(Out, State, NL, LC, Context, Space,
-                                            IsDot);
+      printer(Out, State, NL, LC, Space, IsDot, std::forward<Args>(args)...);
     });
 
     --Space;
-    Indent(Out, Space, IsDot) << "]," << NL; // End of "index_of_element".
+    Indent(Out, Space, IsDot) << "]," << NL; // End of "jsonPropertyName".
   } else {
     Out << "null," << NL;
   }
+}
+
+void ExprEngine::printJson(raw_ostream &Out, ProgramStateRef State,
+                           const LocationContext *LCtx, const char *NL,
+                           unsigned int Space, bool IsDot) const {
+
+  printStateTraitWithLocationContextJson<ObjectsUnderConstruction>(
+      Out, State, LCtx, NL, Space, IsDot, "constructing_objects",
+      printObjectsUnderConstructionJson);
+  printStateTraitWithLocationContextJson<IndexOfElementToConstruct>(
+      Out, State, LCtx, NL, Space, IsDot, "index_of_element",
+      printIndicesOfElementsToConstructJson);
+  printStateTraitWithLocationContextJson<PendingInitLoop>(
+      Out, State, LCtx, NL, Space, IsDot, "pending_init_loops",
+      printPendingInitLoopJson);
+  printStateTraitWithLocationContextJson<PendingArrayDestruction>(
+      Out, State, LCtx, NL, Space, IsDot, "pending_destructors",
+      printPendingArrayDestructionsJson);
 
   getCheckerManager().runCheckersForPrintStateJson(Out, State, NL, Space,
                                                    IsDot);
 }
 
 void ExprEngine::processEndWorklist() {
   // This prints the name of the top-level function if we crash.
   PrettyStackTraceLocationContext CrashInfo(getRootLocationContext());

clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot

"{
         }
       ],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "environment": null,
         "checker_messages": [
           { "checker": "alpha.core.FooChecker", "messages": [
             "Foo stuff:",
             "Foo: Bar"
           ]}
         ]
       }
     }
 \l}"];

clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot

"{
       ],
       "program_state": {
         "environment": null,
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": [
           { "checker": "FooChecker", "messages": [
             "Foo: Bar"
           ]},
           { "checker": "BarChecker", "messages": [
             "Bar: Foo"
           ]}
         ]
"{
         {
           "kind": "BlockEntrance", "block_id": 1,
           "terminator": null, "term_kind": null,
           "tag": null, "node_id": 1,
           "has_report": 0, "is_sink": 0
         }
       ],
       "program_state": {
         "environment": null,
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": [
           { "checker": "FooChecker", "messages": [
             "Foo: Bar",
             "Bar: Foo"
           ]},
           { "checker": "DunnoWhateverSomeOtherChecker", "messages": [
             "Dunno, some other message."
           ]}
         ]

clang/test/Analysis/exploded-graph-rewriter/constraints.dot

"{
         }
       ],
       "program_state": {
         "store": null,
         "environment": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "constraints": [
           { "symbol": "reg_$0<x>", "range": "{ [0, 0] }" }
         ]
       }
     }
 \l}"];

clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot

"{
         }
       ],
       "program_state": {
         "store": null,
         "environment": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "constraints": [
           { "symbol": "reg_$0<x>", "range": "{ [0, 10] }" }
         ]
       }
     }
 \l}"];
 
"{
         }
       ],
       "program_state": {
         "store": null,
         "environment": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "constraints": [
           { "symbol": "reg_$0<x>", "range": "{ [0, 5] }" }
         ]
       }
     }
 \l}"];
 
"{
       ],
       "program_state": {
         "store": null,
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null
       }
     }
 \l}"];

clang/test/Analysis/exploded-graph-rewriter/environment.dot

"{
         }
       ],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "environment": {
           "pointer": "0x2",
           "items": [
             {
               "location_context": "#0 Call",
               "lctx_id": 3,
               "calling": "foo",

clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot

"{
         }
       ],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "environment": {
           "pointer": "0x2",
           "items": [
             {
               "location_context": "#0 Call",
               "lctx_id": 3,
               "calling": "foo",
"{
         }
       ],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "environment": {
           "pointer": "0x2",
           "items": [
             {
               "location_context": "#0 Call",
               "lctx_id": 3,
               "calling": "foo",
"{
         }
       ],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "environment": {
           "pointer": "0x2",
           "items": [
             {
               "location_context": "#0 Call",
               "lctx_id": 3,
               "calling": "foo",

clang/test/Analysis/exploded-graph-rewriter/store.dot

"{
         }
       ],
       "program_state": {
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "store": {
           "pointer": "0x2",
           "items": [
             {
               "cluster": "x",
               "pointer": "0x3",
               "items": [

clang/test/Analysis/exploded-graph-rewriter/store_diff.dot

"{
         }
       ],
       "program_state": {
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "store": {
           "pointer": "0x2",
           "items": [
             {
               "cluster": "x",
               "pointer": "0x3",
               "items": [
"{
         }
       ],
       "program_state": {
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": null,
         "store": {
           "pointer": "0x5",
           "items": [
             {
               "cluster": "x",
               "pointer": "0x3",
               "items": [

clang/test/Analysis/exploded-graph-rewriter/topology.dot

"{
         }
       ],
       "program_state": {
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "index_of_element": null,
+        "pending_init_loops": null,
+        "pending_destructors": null,
         "checker_messages": [
           { "checker": "foo", "messages": ["bar"] }
         ],
         "store": null
       }
     }
 \l}"];

clang/test/Analysis/expr-inspection.c

 // CHECK-NEXT:     { "symbol": "reg_$0<int x>", "range": "{ [-2147483648, 13] }" }
 // CHECK-NEXT:   ],
 // CHECK-NEXT:   "equivalence_classes": null,
 // CHECK-NEXT:   "disequality_info": null,
 // CHECK-NEXT:   "dynamic_types": null,
 // CHECK-NEXT:   "dynamic_casts": null,
 // CHECK-NEXT:   "constructing_objects": null,
 // CHECK-NEXT:   "index_of_element": null,
+// CHECK-NEXT:   "pending_init_loops": null,
+// CHECK-NEXT:   "pending_destructors": null,
 // CHECK-NEXT:   "checker_messages": null
 // CHECK-NEXT: }
 
 struct S {
   int x, y;
 };
 
 void test_field_dumps(struct S s, struct S *p) {
   clang_analyzer_dump_pointer(&s.x); // expected-warning{{&s.x}}
   clang_analyzer_dump_pointer(&p->x); // expected-warning{{&SymRegion{reg_$1<struct S * p>}.x}}
   clang_analyzer_dumpSvalType_pointer(&s.x); // expected-warning {{int *}}
 }

clang/utils/analyzer/exploded-graph-rewriter.py

def __init__(self, state_id, json_ps):
         if json_ps is None:
             json_ps = {
                 'store': None,
                 'environment': None,
                 'constraints': None,
                 'dynamic_types': None,
                 'constructing_objects': None,
                 'index_of_element': None,
+                'pending_init_loops': None,
+                'pending_destructors': None,
                 'checker_messages': None
             }
 
         self.state_id = state_id
 
         self.store = Store(json_ps['store']) \
             if json_ps['store'] is not None else None
 
def __init__(self, state_id, json_ps):
 
         self.constructing_objects = \
             GenericEnvironment(json_ps['constructing_objects']) \
             if json_ps['constructing_objects'] is not None else None
 
         self.index_of_element = \
             GenericEnvironment(json_ps['index_of_element']) \
             if json_ps['index_of_element'] is not None else None
         
+        self.pending_init_loops = \
+            GenericEnvironment(json_ps['pending_init_loops']) \
+            if json_ps['pending_init_loops'] is not None else None
+
+        self.pending_destructors = \
+            GenericEnvironment(json_ps['pending_destructors']) \
+            if json_ps['pending_destructors'] is not None else None
+        
         self.checker_messages = CheckerMessages(json_ps['checker_messages']) \
             if json_ps['checker_messages'] is not None else None
 
 
 # A deserialized exploded graph node. Has a default constructor because it
 # may be referenced as part of an edge before its contents are deserialized,
 # and in this moment we already need a room for predecessors and successors.
 class ExplodedNode:
def visit_state(self, s, prev_s):
         self.visit_generic_map_in_state('dynamic_types', 'Dynamic Types',
                                         s, prev_s)
         self.visit_environment_in_state('constructing_objects',
                                         'Objects Under Construction',
                                         s, prev_s)
         self.visit_environment_in_state('index_of_element',
                                         'Indices Of Elements Under Construction',
                                         s, prev_s)
+        self.visit_environment_in_state('pending_init_loops',
+                                        'Pending Array Init Loop Expressions',
+                                        s, prev_s)
+        self.visit_environment_in_state('pending_destructors',
+                                        'Indices of Elements Under Destruction',
+                                        s, prev_s)
         self.visit_checker_messages_in_state(s, prev_s)
 
     def visit_node(self, node):
         self._dump('%s [shape=record,'
                    % (node.node_name()))
         if self._dark_mode:
             self._dump('color="white",fontcolor="gray80",')
         self._dump('label=<<table border="0">')