1753f127fSDimitry Andric //===- DebugSupport.cpp -----------------------------------------*- C++ -*-===//
2753f127fSDimitry Andric //
3753f127fSDimitry Andric // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4753f127fSDimitry Andric // See https://llvm.org/LICENSE.txt for license information.
5753f127fSDimitry Andric // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6753f127fSDimitry Andric //
7753f127fSDimitry Andric //===----------------------------------------------------------------------===//
8753f127fSDimitry Andric //
9753f127fSDimitry Andric //  This file defines functions which generate more readable forms of data
10753f127fSDimitry Andric //  structures used in the dataflow analyses, for debugging purposes.
11753f127fSDimitry Andric //
12753f127fSDimitry Andric //===----------------------------------------------------------------------===//
13753f127fSDimitry Andric 
14753f127fSDimitry Andric #include <utility>
15753f127fSDimitry Andric 
16753f127fSDimitry Andric #include "clang/Analysis/FlowSensitive/DebugSupport.h"
17753f127fSDimitry Andric #include "clang/Analysis/FlowSensitive/Solver.h"
18753f127fSDimitry Andric #include "clang/Analysis/FlowSensitive/Value.h"
19bdd1243dSDimitry Andric #include "llvm/ADT/StringRef.h"
20753f127fSDimitry Andric #include "llvm/Support/ErrorHandling.h"
21753f127fSDimitry Andric 
22753f127fSDimitry Andric namespace clang {
23753f127fSDimitry Andric namespace dataflow {
24753f127fSDimitry Andric 
debugString(Value::Kind Kind)25bdd1243dSDimitry Andric llvm::StringRef debugString(Value::Kind Kind) {
26bdd1243dSDimitry Andric   switch (Kind) {
27bdd1243dSDimitry Andric   case Value::Kind::Integer:
28bdd1243dSDimitry Andric     return "Integer";
29bdd1243dSDimitry Andric   case Value::Kind::Pointer:
30bdd1243dSDimitry Andric     return "Pointer";
31*c9157d92SDimitry Andric   case Value::Kind::Record:
32*c9157d92SDimitry Andric     return "Record";
33bdd1243dSDimitry Andric   case Value::Kind::AtomicBool:
34bdd1243dSDimitry Andric     return "AtomicBool";
35bdd1243dSDimitry Andric   case Value::Kind::TopBool:
36bdd1243dSDimitry Andric     return "TopBool";
37fe013be4SDimitry Andric   case Value::Kind::FormulaBool:
38fe013be4SDimitry Andric     return "FormulaBool";
39bdd1243dSDimitry Andric   }
40bdd1243dSDimitry Andric   llvm_unreachable("Unhandled value kind");
41bdd1243dSDimitry Andric }
42bdd1243dSDimitry Andric 
operator <<(llvm::raw_ostream & OS,Solver::Result::Assignment Assignment)43fe013be4SDimitry Andric llvm::raw_ostream &operator<<(llvm::raw_ostream &OS,
44fe013be4SDimitry Andric                               Solver::Result::Assignment Assignment) {
45fcaf7f86SDimitry Andric   switch (Assignment) {
46fcaf7f86SDimitry Andric   case Solver::Result::Assignment::AssignedFalse:
47fe013be4SDimitry Andric     return OS << "False";
48fcaf7f86SDimitry Andric   case Solver::Result::Assignment::AssignedTrue:
49fe013be4SDimitry Andric     return OS << "True";
50fcaf7f86SDimitry Andric   }
51fcaf7f86SDimitry Andric   llvm_unreachable("Booleans can only be assigned true/false");
52fcaf7f86SDimitry Andric }
53fcaf7f86SDimitry Andric 
debugString(Solver::Result::Status Status)54bdd1243dSDimitry Andric llvm::StringRef debugString(Solver::Result::Status Status) {
55fcaf7f86SDimitry Andric   switch (Status) {
56fcaf7f86SDimitry Andric   case Solver::Result::Status::Satisfiable:
57fcaf7f86SDimitry Andric     return "Satisfiable";
58fcaf7f86SDimitry Andric   case Solver::Result::Status::Unsatisfiable:
59fcaf7f86SDimitry Andric     return "Unsatisfiable";
60fcaf7f86SDimitry Andric   case Solver::Result::Status::TimedOut:
61fcaf7f86SDimitry Andric     return "TimedOut";
62fcaf7f86SDimitry Andric   }
63fcaf7f86SDimitry Andric   llvm_unreachable("Unhandled SAT check result status");
64fcaf7f86SDimitry Andric }
65fcaf7f86SDimitry Andric 
operator <<(llvm::raw_ostream & OS,const Solver::Result & R)66fe013be4SDimitry Andric llvm::raw_ostream &operator<<(llvm::raw_ostream &OS, const Solver::Result &R) {
67fe013be4SDimitry Andric   OS << debugString(R.getStatus()) << "\n";
68fe013be4SDimitry Andric   if (auto Solution = R.getSolution()) {
69fe013be4SDimitry Andric     std::vector<std::pair<Atom, Solver::Result::Assignment>> Sorted = {
70fe013be4SDimitry Andric         Solution->begin(), Solution->end()};
71fe013be4SDimitry Andric     llvm::sort(Sorted);
72fe013be4SDimitry Andric     for (const auto &Entry : Sorted)
73fe013be4SDimitry Andric       OS << Entry.first << " = " << Entry.second << "\n";
74753f127fSDimitry Andric   }
75fe013be4SDimitry Andric   return OS;
76753f127fSDimitry Andric }
77753f127fSDimitry Andric 
78753f127fSDimitry Andric } // namespace dataflow
79753f127fSDimitry Andric } // namespace clang
80