[analyzer] print() JSONify: Constraints implementation

[Charusso]

Summary

-

[NoQ]

clang/lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

780 ↗

(On Diff #200101)

Let's be informative: "symbol": ..., "range": ...

[Charusso]

• Improved the JSON format.

[NoQ]

Looks great!

[Charusso]

• 100% pure JSON.

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

virtual const llvm::APSInt* getSymVal(ProgramStateRef state,
     return nullptr;
   }
 
   /// Scan all symbols referenced by the constraints. If the symbol is not
   /// alive, remove it.
   virtual ProgramStateRef removeDeadBindings(ProgramStateRef state,
                                                  SymbolReaper& SymReaper) = 0;
 
-  virtual void print(ProgramStateRef state,
-                     raw_ostream &Out,
-                     const char* nl,
-                     const char *sep) = 0;
+  virtual void printJson(raw_ostream &Out, ProgramStateRef State,
+                         const char *NL, unsigned int Space,
+                         bool IsDot) const = 0;
 
   virtual void EndPath(ProgramStateRef state) {}
 
   /// Convenience method to query the state to see if a symbol is null or
   /// not null, or if neither assumption can be made.
   ConditionTruthVal isNull(ProgramStateRef State, SymbolRef Sym) {
     SaveAndRestore<bool> DisableNotify(NotifyAssumeClients, false);
 

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

 //== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines a SMT generic API, which will be the base class for
 //  every SMT solver specific class.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
 
+#include "clang/Basic/JsonSupport.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 
 typedef llvm::ImmutableSet<
     std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>
     ConstraintSMTType;
 REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTType)
 
ProgramStateRef removeDeadBindings(ProgramStateRef State,
     for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
       if (SymReaper.isDead(I->first))
         CZ = CZFactory.remove(CZ, *I);
     }
 
     return State->set<ConstraintSMT>(CZ);
   }
 
-  void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
-             const char *sep) override {
-
-    auto CZ = St->get<ConstraintSMT>();
-
-    OS << nl << sep << "Constraints:";
-    for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
-      OS << nl << ' ' << I->first << " : ";
-      I->second->print(OS);
+  void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
+                 unsigned int Space = 0, bool IsDot = false) const override {
+    ConstraintSMTType Constraints = State->get<ConstraintSMT>();
+
+    Indent(Out, Space, IsDot) << "\"constraints\": ";
+    if (Constraints.isEmpty()) {
+      Out << "null," << NL;
+      return;
+    }
+
+    ++Space;
+    Out << '[' << NL;
+    for (ConstraintSMTType::iterator I = Constraints.begin();
+         I != Constraints.end(); ++I) {
+      Indent(Out, Space, IsDot)
+          << "{ \"symbol\": \"" << I->first << "\", \"range\": \"";
+      I->second->print(Out);
+      Out << "\" }";
+
+      if (std::next(I) != Constraints.end())
+        Out << ',';
+      Out << NL;
     }
-    OS << nl;
+
+    --Space;
+    Indent(Out, Space, IsDot) << "],";
   }
 
   bool haveEqualConstraints(ProgramStateRef S1,
                             ProgramStateRef S2) const override {
     return S1->get<ConstraintSMT>() == S2->get<ConstraintSMT>();
   }
 
   bool canReasonAbout(SVal X) const override {

lib/StaticAnalyzer/Core/ProgramState.cpp

void ProgramState::printJson(raw_ostream &Out, const LocationContext *LCtx,
   ProgramStateManager &Mgr = getStateManager();
   const ASTContext &Context = getStateManager().getContext();
   Mgr.getStoreManager().printJson(Out, getStore(), NL, Space, IsDot);
 
   // Print out the environment.
   Env.printJson(Out, Context, LCtx, NL, Space, IsDot);
 
   // Print out the constraints.
-  Mgr.getConstraintManager().print(this, Out, NL, Sep);
+  Mgr.getConstraintManager().printJson(Out, this, NL, Space, IsDot);
 
   // Print out the tracked dynamic types.
   printDynamicTypeInfo(this, Out, NL, Sep);
 
   // Print checker-specific data.
   Mgr.getOwningEngine().printState(Out, this, LCtx, NL, Space, IsDot);
 }
 

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 //== RangeConstraintManager.cpp - Manage range constraints.------*- C++ -*--==//
 //
 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
 // See https://llvm.org/LICENSE.txt for license information.
 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines RangeConstraintManager, a class that tracks simple
 //  equality and inequality constraints on symbolic values of ProgramState.
 //
 //===----------------------------------------------------------------------===//
 
+#include "clang/Basic/JsonSupport.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/ImmutableSet.h"
 #include "llvm/Support/raw_ostream.h"
 
public:
   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
 
   const llvm::APSInt *getSymVal(ProgramStateRef State,
                                 SymbolRef Sym) const override;
 
   ProgramStateRef removeDeadBindings(ProgramStateRef State,
                                      SymbolReaper &SymReaper) override;
 
-  void print(ProgramStateRef State, raw_ostream &Out, const char *nl,
-             const char *sep) override;
+  void printJson(raw_ostream &Out, ProgramStateRef State, const char *NL = "\n",
+                 unsigned int Space = 0, bool IsDot = false) const override;
 
   //===------------------------------------------------------------------===//
   // Implementation for interface from RangedConstraintManager.
   //===------------------------------------------------------------------===//
 
   ProgramStateRef assumeSymNE(ProgramStateRef State, SymbolRef Sym,
                               const llvm::APSInt &V,
                               const llvm::APSInt &Adjustment) override;
ProgramStateRef RangeConstraintManager::assumeSymOutsideInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, const llvm::APSInt &Adjustment) {
   RangeSet RangeLT = getSymLTRange(State, Sym, From, Adjustment);
   RangeSet RangeGT = getSymGTRange(State, Sym, To, Adjustment);
   RangeSet New(RangeLT.addRange(F, RangeGT));
   return New.isEmpty() ? nullptr : State->set<ConstraintRange>(Sym, New);
 }
 
-//===------------------------------------------------------------------------===
+//===----------------------------------------------------------------------===//
 // Pretty-printing.
-//===------------------------------------------------------------------------===/
-
-void RangeConstraintManager::print(ProgramStateRef St, raw_ostream &Out,
-                                   const char *nl, const char *sep) {
-
-  ConstraintRangeTy Ranges = St->get<ConstraintRange>();
+//===----------------------------------------------------------------------===//
 
-  if (Ranges.isEmpty()) {
-    Out << nl << sep << "Ranges are empty." << nl;
+void RangeConstraintManager::printJson(raw_ostream &Out, ProgramStateRef State,
+                                       const char *NL, unsigned int Space,
+                                       bool IsDot) const {
+  ConstraintRangeTy Constraints = State->get<ConstraintRange>();
+
+  Indent(Out, Space, IsDot) << "\"constraints\": ";
+  if (Constraints.isEmpty()) {
+    Out << "null," << NL;
     return;
   }
 
-  Out << nl << sep << "Ranges of symbol values:";
-  for (ConstraintRangeTy::iterator I = Ranges.begin(), E = Ranges.end(); I != E;
-       ++I) {
-    Out << nl << ' ' << I.getKey() << " : ";
+  ++Space;
+  Out << '[' << NL;
+  for (ConstraintRangeTy::iterator I = Constraints.begin();
+       I != Constraints.end(); ++I) {
+    Indent(Out, Space, IsDot)
+        << "{ \"symbol\": \"" << I.getKey() << "\", \"range\": \"";
     I.getData().print(Out);
+    Out << "\" }";
+
+    if (std::next(I) != Constraints.end())
+      Out << ',';
+    Out << NL;
   }
-  Out << nl;
+
+  --Space;
+  Indent(Out, Space, IsDot) << "]," << NL;
 }

test/Analysis/expr-inspection.c

 // CHECK-NEXT:     { "kind": "Direct", "offset": 0, "value": "2 S32b" }
 // CHECK-NEXT:   ]}
 // CHECK-NEXT: ],
 // CHECK-NEXT: "environment": [
 // CHECK-NEXT:   { "location_context": "#0 Call", "calling": "foo", "call_line": null, "items": [
 // CHECK-NEXT:     { "lctx_id": 1, "stmt_id": 847, "pretty": "clang_analyzer_printState", "value": "&code{clang_analyzer_printState}" }
 // CHECK-NEXT:   ]}
 // CHECK-NEXT: ],
+// CHECK-NEXT: "constraints": [
+// CHECK-NEXT:   { "symbol": "reg_$0<int x>", "range": "{ [-2147483648, 13] }" }
+// CHECK-NEXT: ],
 
-// CHECK:      Ranges of symbol values:
-// CHECK-NEXT:  reg_$0<int x> : { [-2147483648, 13] }