[clang][dataflow] Generate readable form of input and output of satisfiability checking for debugging purposes.

[wyt]

Summary

As part of the dataflow analysis framework, there is a SAT solver (API defined in Solver.h) which takes llvm::DenseSet<BoolValue*> Constraints as input and checks if the booleans are satisfiable.
This patch implements functionality to produce a readable string representation of the boolean constraints, the status of the SAT check and the satisfying truth assigment if found by the SAT solver.

Note that the booleans in an llvm::DenseSet is not fixed. Therefore, we introduce an overloaded debugString which takes a std::vector<BoolValue *> Constraints as input to guarantee order stability and enable testing against hardcoded expected string values.

Depends On D129547

[wyt]

Use std::vector as input to debugString to maintain order stability of boolean constraints to enable testing. debugString which takes a llvm::DenseSet<BoolValue*> is now a wrapper around the logic applied to std::vector.

[gribozavr2]

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

140

I appreciate the table, but it looks quite bulky... Could we switch to a simple atom=value\natom2=value2\n format?

144–153

We put the llvm_unreachable after the switch, so that clang can warn us if we add a new enumerator but forget to update the switch. Please apply everywhere in this patch stack.

156

[wyt]

Address comments.

[wyt]

Fix comment, remove unused import.

[wyt]

Remove unnecessary enum keyword.

[wyt]

Change propagated from parent patch.

[xazax.hun]

Some nits inline, but looks good to me.

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

116–130

In its current form, I think you could create the final strings in one step and sort those strings instead of the pairs. Or do we expect alignment to mess up the order in that case?

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

415

I don't see a test case for Unsatisfiable constraints.

[gribozavr2]

clang/include/clang/Analysis/FlowSensitive/DebugSupport.h

45–52

[wyt]

Address comments.

[wyt]

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

116–130

In its current form, I think you could create the final strings in one step and sort those strings instead of the pairs. Or do we expect alignment to mess up the order in that case?

Removed LinesData and the intermediate step of storing a pair of strings. There is still a loop at the start of the function to find the max name length for alignment purposes.

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

228

@xazax.hun

I don't see a test case for Unsatisfiable constraints.

Here.

[xazax.hun]

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

228

Whoops, indeed. Sorry :)

clang/include/clang/Analysis/FlowSensitive/DebugSupport.h

 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
 
 #include <string>
 
+#include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 
 namespace clang {
 namespace dataflow {
 /// Returns a string representation for a boolean value `B`.
 ///
 /// Atomic booleans appearing in the boolean value `B` are assigned to labels
 /// either specified in `AtomNames` or created by default rules as B0, B1, ...
 std::string
 debugString(BoolValue &B,
             llvm::DenseMap<AtomicBoolValue *, std::string> AtomNames);
 inline std::string debugString(BoolValue &B) { return debugString(B, {{}}); }
 
+/// Returns a string representation for `Constraints` - a set of boolean
+/// formulas and the `Result` of satisfiability checking.
+///
+/// Atomic booleans appearing in `Constraints` and `Result` are assigned to
+/// labels either specified in `AtomNames` or created by default rules as B0,
+/// B1, ...
+std::string
+debugString(llvm::DenseSet<BoolValue *> &Constraints, Solver::Result &Result,
+            llvm::DenseMap<AtomicBoolValue *, std::string> AtomNames);
+inline std::string debugString(llvm::DenseSet<BoolValue *> &Constraints,
+                               Solver::Result &Result) {
+  return debugString(Constraints, Result, {{}});
+}
+
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

 //===- DebugSupport.cpp -----------------------------------------*- 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 functions which generate more readable forms of data
 //  structures used in the dataflow analyses, for debugging purposes.
 //
 //===----------------------------------------------------------------------===//
 
+#include <utility>
+
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
+#include "clang/Analysis/FlowSensitive/Solver.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
 #include "llvm/ADT/DenseMap.h"
 #include "llvm/ADT/StringSet.h"
 #include "llvm/Support/ErrorHandling.h"
 #include "llvm/Support/FormatAdapters.h"
+#include "llvm/Support/FormatCommon.h"
 #include "llvm/Support/FormatVariadic.h"
 
 namespace clang {
 namespace dataflow {
 
+using llvm::AlignStyle;
 using llvm::fmt_pad;
+using llvm::fmt_repeat;
 using llvm::formatv;
 
 class DebugStringGenerator {
 public:
   explicit DebugStringGenerator(
       llvm::DenseMap<AtomicBoolValue *, std::string> AtomNames)
       : Counter(0), AtomNames(AtomNames) {
     llvm::StringSet<> Names;
std::string debugString(BoolValue &B, size_t Depth = 0) {
     }
     default:
       llvm_unreachable("Unhandled value kind");
     }
     auto Indent = Depth * 4;
     return formatv("{0}", fmt_pad(S, Indent, 0));
   }
 
+  /// Returns a string representation of a set of boolean `Constraints` and the
+  /// `Result` of satisfiability checking on the `Constraints`.
+  std::string debugString(llvm::DenseSet<BoolValue *> &Constraints,
+                          Solver::Result &Result) {
+    auto Template = R"(
+Constraints
+------------
+{0:$[
+
+]}
+------------
+{1}.{2}
+)";
+
+    std::vector<std::string> ConstraintsStrings;
+    for (auto &Constraint : Constraints) {
+      ConstraintsStrings.push_back(debugString(*Constraint));
+    }
+    llvm::sort(ConstraintsStrings.begin(), ConstraintsStrings.end());
+
+    auto StatusString = debugString(Result.getStatus());
+    auto Solution = Result.getSolution();
+    auto SolutionString =
+        Solution.hasValue() ? "\n" + debugString(Solution.getValue()) : "";
+
+    return formatv(
+        Template,
+        llvm::make_range(ConstraintsStrings.begin(), ConstraintsStrings.end()),
+        StatusString, SolutionString);
+  }
+
 private:
+  /// Returns a string representation of a truth assignment to atom booleans.
+  std::string
+  debugString(llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
+                  &ValAssignments) {
+    size_t FirstColWidth = 6;
+    size_t SecondColWidth = 7;
+
+    std::vector<std::pair<std::string, std::string>> LinesData;
+    LinesData.push_back({"Atom", "Value"});
+    for (auto &ValAssignment : ValAssignments) {
+      auto Name = getAtomName(ValAssignment.first);
+      FirstColWidth = std::max(FirstColWidth, Name.size() + 2);
+      LinesData.push_back({Name, debugString(ValAssignment.second)});
+    }
+    llvm::sort(std::next(LinesData.begin()), LinesData.end());
+
+    std::vector<std::string> Lines;
+    auto Separator = formatv("+{0}+{1}+", fmt_repeat('-', FirstColWidth),
+                             fmt_repeat('-', SecondColWidth));
+    Lines.push_back(Separator);
+    for (auto &LineData : LinesData) {
+      auto Line = formatv(
+          "| {0} | {1} |",
+          fmt_align(LineData.first, AlignStyle::Left, FirstColWidth - 2),
+          fmt_align(LineData.second, AlignStyle::Left, SecondColWidth - 2));
+      Lines.push_back(Line);
+      Lines.push_back(Separator);
+    }
+
+    return formatv("{0:$[\n]}", llvm::make_range(Lines.begin(), Lines.end()));
+  }
+
+  /// Returns a string representation of a boolean assignment to true or false.
+  std::string debugString(Solver::Result::Assignment &Assignment) {
+    switch (Assignment) {
+    case Solver::Result::Assignment::AssignedFalse:
+      return "False";
+    case Solver::Result::Assignment::AssignedTrue:
+      return "True";
+    default:
+      llvm_unreachable("Booleans can only be assigned true/false");
+    }
+  }
+
+  /// Returns a string representation of the result status of a SAT check.
+  std::string debugString(enum Solver::Result::Status Status) {
+    switch (Status) {
+    case Solver::Result::Status::Satisfiable:
+      return "Satisfiable";
+    case Solver::Result::Status::Unsatisfiable:
+      return "Unsatisfiable";
+    case Solver::Result::Status::TimedOut:
+      return "TimedOut";
+    default:
+      llvm_unreachable("Unhandled SAT check result status");
+    }
+  }
+
   /// Returns the name assigned to `Atom`, either user-specified or created by
   /// default rules (B0, B1, ...).
   std::string getAtomName(AtomicBoolValue *Atom) {
     auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
     if (Entry.second) {
       Counter++;
     }
     return Entry.first->second;
   }
 
   // Keep track of number of atoms without a user-specified name, used to assign
   // non-repeating default names to such atoms.
   size_t Counter;
 
   // Keep track of names assigned to atoms.
   llvm::DenseMap<AtomicBoolValue *, std::string> AtomNames;
 };
 
 std::string debugString(BoolValue &B,
                         llvm::DenseMap<AtomicBoolValue *, std::string> Names) {
   return DebugStringGenerator(Names).debugString(B);
 }
 
+std::string debugString(llvm::DenseSet<BoolValue *> &Constraints,
+                        Solver::Result &Result,
+                        llvm::DenseMap<AtomicBoolValue *, std::string> Names) {
+  return DebugStringGenerator(Names).debugString(Constraints, Result);
+}
+
 } // namespace dataflow
 } // namespace clang

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

 //===- unittests/Analysis/FlowSensitive/DebugSupportTest.cpp --------------===//
 //
 // 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
 //
 //===----------------------------------------------------------------------===//
 
 #include "clang/Analysis/FlowSensitive/DebugSupport.h"
 #include "TestingSupport.h"
 #include "clang/Analysis/FlowSensitive/Value.h"
+#include "clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h"
 #include "gmock/gmock.h"
 #include "gtest/gtest.h"
 
 namespace {
 
 using namespace clang;
 using namespace dataflow;
 using testing::StrEq;
(and
         (B0))
     (or
         (True)
         (B1))))";
   EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
               StrEq(Expected));
 }
 
+class SATCheckDebugStringTest : public ::testing::Test {
+protected:
+  Solver::Result CheckSAT(llvm::DenseSet<BoolValue *> Constraints) {
+    return WatchedLiteralsSolver().solve(std::move(Constraints));
+  }
+  test::BoolValueManager Bools;
+};
+
+TEST_F(SATCheckDebugStringTest, AtomicBoolean) {
+  // B0
+  llvm::DenseSet<BoolValue *> Constraints({Bools.atom()});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+(B0)
+------------
+Satisfiable.
++------+-------+
+| Atom | Value |
++------+-------+
+| B0   | True  |
++------+-------+
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST_F(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
+  // B0, !B0
+  auto B0 = Bools.atom();
+  llvm::DenseSet<BoolValue *> Constraints({B0, Bools.neg(B0)});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+(B0)
+
+(not
+    (B0))
+------------
+Unsatisfiable.
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST_F(SATCheckDebugStringTest, MultipleAtomicBooleans) {
+  // B0, B1
+  llvm::DenseSet<BoolValue *> Constraints({Bools.atom(), Bools.atom()});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+(B0)
+
+(B1)
+------------
+Satisfiable.
++------+-------+
+| Atom | Value |
++------+-------+
+| B0   | True  |
++------+-------+
+| B1   | True  |
++------+-------+
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST_F(SATCheckDebugStringTest, Implication) {
+  // B0, B0 => B1
+  auto B0 = Bools.atom();
+  auto B1 = Bools.atom();
+  auto Impl = Bools.disj(Bools.neg(B0), B1);
+  llvm::DenseSet<BoolValue *> Constraints({B0, Impl});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+(B0)
+
+(or
+    (not
+        (B0))
+    (B1))
+------------
+Satisfiable.
++------+-------+
+| Atom | Value |
++------+-------+
+| B0   | True  |
++------+-------+
+| B1   | True  |
++------+-------+
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST_F(SATCheckDebugStringTest, Iff) {
+  // B0, B0 <=> B1
+  auto B0 = Bools.atom();
+  auto B1 = Bools.atom();
+  auto Iff =
+      Bools.conj(Bools.disj(Bools.neg(B0), B1), Bools.disj(B0, Bools.neg(B1)));
+  llvm::DenseSet<BoolValue *> Constraints({B0, Iff});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+(B0)
+
+(and
+    (or
+        (not
+            (B0))
+        (B1))
+    (or
+        (B0)
+        (not
+            (B1))))
+------------
+Satisfiable.
++------+-------+
+| Atom | Value |
++------+-------+
+| B0   | True  |
++------+-------+
+| B1   | True  |
++------+-------+
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST_F(SATCheckDebugStringTest, Xor) {
+  // B0, XOR(B0, B1)
+  auto B0 = Bools.atom();
+  auto B1 = Bools.atom();
+  auto XOR =
+      Bools.disj(Bools.conj(B0, Bools.neg(B1)), Bools.conj(Bools.neg(B0), B1));
+  llvm::DenseSet<BoolValue *> Constraints({B0, XOR});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+(B0)
+
+(or
+    (and
+        (B0)
+        (not
+            (B1)))
+    (and
+        (not
+            (B0))
+        (B1)))
+------------
+Satisfiable.
++------+-------+
+| Atom | Value |
++------+-------+
+| B0   | True  |
++------+-------+
+| B1   | False |
++------+-------+
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST_F(SATCheckDebugStringTest, ComplexBooleanWithNames) {
+  // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
+  auto Cond = cast<AtomicBoolValue>(Bools.atom());
+  auto Then = cast<AtomicBoolValue>(Bools.atom());
+  auto Else = cast<AtomicBoolValue>(Bools.atom());
+  auto B = Bools.disj(
+      Bools.conj(Cond, Bools.conj(Then, Bools.neg(Else))),
+      Bools.conj(Bools.neg(Cond), Bools.conj(Bools.neg(Then), Else)));
+  llvm::DenseSet<BoolValue *> Constraints({Cond, B});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+(Cond)
+
+(or
+    (and
+        (Cond)
+        (and
+            (Then)
+            (not
+                (Else))))
+    (and
+        (not
+            (Cond))
+        (and
+            (not
+                (Then))
+            (Else))))
+------------
+Satisfiable.
++------+-------+
+| Atom | Value |
++------+-------+
+| Cond | True  |
++------+-------+
+| Else | False |
++------+-------+
+| Then | True  |
++------+-------+
+)";
+  EXPECT_THAT(debugString(Constraints, Result,
+                          {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
+              StrEq(Expected));
+}
+
+TEST_F(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
+  // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
+  auto IntsAreEq = cast<AtomicBoolValue>(Bools.atom());
+  auto ThisIntEqZero = cast<AtomicBoolValue>(Bools.atom());
+  auto OtherIntEqZero = cast<AtomicBoolValue>(Bools.atom());
+  auto BothZeroImpliesEQ = Bools.disj(
+      Bools.neg(Bools.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
+  llvm::DenseSet<BoolValue *> Constraints(
+      {ThisIntEqZero, Bools.neg(IntsAreEq), BothZeroImpliesEQ});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+(ThisIntEqZero)
+
+(not
+    (IntsAreEq))
+
+(or
+    (not
+        (and
+            (ThisIntEqZero)
+            (OtherIntEqZero)))
+    (IntsAreEq))
+------------
+Satisfiable.
++----------------+-------+
+| Atom           | Value |
++----------------+-------+
+| IntsAreEq      | False |
++----------------+-------+
+| OtherIntEqZero | False |
++----------------+-------+
+| ThisIntEqZero  | True  |
++----------------+-------+
+)";
+  EXPECT_THAT(debugString(Constraints, Result,
+                          {{IntsAreEq, "IntsAreEq"},
+                           {ThisIntEqZero, "ThisIntEqZero"},
+                           {OtherIntEqZero, "OtherIntEqZero"}}),
+              StrEq(Expected));
+}
 } // namespace