1 //===- DebugSupport.cpp -----------------------------------------*- C++ -*-===//
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
7 //===----------------------------------------------------------------------===//
9 // This file defines functions which generate more readable forms of data
10 // structures used in the dataflow analyses, for debugging purposes.
12 //===----------------------------------------------------------------------===//
16 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
17 #include "clang/Analysis/FlowSensitive/Solver.h"
18 #include "clang/Analysis/FlowSensitive/Value.h"
19 #include "llvm/ADT/StringRef.h"
20 #include "llvm/Support/ErrorHandling.h"
25 llvm::StringRef debugString(Value::Kind Kind) {
27 case Value::Kind::Integer:
29 case Value::Kind::Reference:
31 case Value::Kind::Pointer:
33 case Value::Kind::Struct:
35 case Value::Kind::AtomicBool:
37 case Value::Kind::TopBool:
39 case Value::Kind::FormulaBool:
42 llvm_unreachable("Unhandled value kind");
45 llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
46 Solver::Result::Assignment Assignment) {
48 case Solver::Result::Assignment::AssignedFalse:
50 case Solver::Result::Assignment::AssignedTrue:
53 llvm_unreachable("Booleans can only be assigned true/false");
56 llvm::StringRef debugString(Solver::Result::Status Status) {
58 case Solver::Result::Status::Satisfiable:
60 case Solver::Result::Status::Unsatisfiable:
61 return "Unsatisfiable";
62 case Solver::Result::Status::TimedOut:
65 llvm_unreachable("Unhandled SAT check result status");
68 llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
69 OS << debugString(R.getStatus()) << "\n";
70 if (auto Solution = R.getSolution()) {
71 std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
72 Solution->begin(), Solution->end()};
74 for (const auto &Entry : Sorted)
75 OS << Entry.first << " = " << Entry.second << "\n";
80 } // namespace dataflow