[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

145

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

149–158

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.

161

[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

121–135

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

417

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

[gribozavr2]

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

49–56

[wyt]

Address comments.

[wyt]

clang/lib/Analysis/FlowSensitive/DebugSupport.cpp

121–135

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

230

@xazax.hun

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

Here.

[xazax.hun]

clang/unittests/Analysis/FlowSensitive/DebugSupportTest.cpp

230

Whoops, indeed. Sorry :)

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

 //  structures used in the dataflow analyses, for debugging purposes.
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
 #define LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_DEBUGSUPPORT_H_
 
 #include <string>
+#include <vector>
 
+#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 the 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, ...
 ///
 /// Requirements:
 ///
 ///   Names assigned to atoms should not be repeated in `AtomNames`.
 std::string debugString(
     const BoolValue &B,
     llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
 
+/// Returns a string representation for `Constraints` - a collection 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, ...
+///
+/// Requirements:
+///
+///   Names assigned to atoms should not be repeated in `AtomNames`.
+std::string debugString(
+    const std::vector<BoolValue *> &Constraints, const Solver::Result &Result,
+    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}});
+inline std::string debugString(
+    const llvm::DenseSet<BoolValue *> &Constraints,
+    const Solver::Result &Result,
+    llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames = {{}}) {
+  std::vector<BoolValue *> ConstraintsVec(Constraints.begin(),
+                                          Constraints.end());
+  return debugString(ConstraintsVec, Result, std::move(AtomNames));
+}
+
 } // 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::formatv;
 
 namespace {
 
 class DebugStringGenerator {
 public:
   explicit DebugStringGenerator(
std::string debugString(const 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(const std::vector<BoolValue *> &Constraints,
+                          const Solver::Result &Result) {
+    auto Template = R"(
+Constraints
+------------
+{0:$[
+
+]}
+------------
+{1}.
+{2}
+)";
+
+    std::vector<std::string> ConstraintsStrings;
+    ConstraintsStrings.reserve(Constraints.size());
+    for (auto &Constraint : Constraints) {
+      ConstraintsStrings.push_back(debugString(*Constraint));
+    }
+
+    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(
+      const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
+          &AtomAssignments) {
+    size_t MaxNameLength = 0;
+    for (auto &AtomName : AtomNames) {
+      MaxNameLength = std::max(MaxNameLength, AtomName.second.size());
+    }
+
+    std::vector<std::string> Lines;
+    for (auto &AtomAssignment : AtomAssignments) {
+      auto Line = formatv("{0} = {1}",
+                          fmt_align(getAtomName(AtomAssignment.first),
+                                    AlignStyle::Left, MaxNameLength),
+                          debugString(AtomAssignment.second));
+      Lines.push_back(Line);
+    }
+    llvm::sort(Lines.begin(), Lines.end());
+
+    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";
+    }
+    llvm_unreachable("Booleans can only be assigned true/false");
+  }
+
+  /// Returns a string representation of the result status of a SAT check.
+  std::string debugString(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";
+    }
+    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(const AtomicBoolValue *Atom) {
     auto Entry = AtomNames.try_emplace(Atom, formatv("B{0}", Counter));
     if (Entry.second) {
       Counter++;
     }
     return Entry.first->second;

 } // namespace
 
 std::string
 debugString(const BoolValue &B,
             llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
   return DebugStringGenerator(std::move(AtomNames)).debugString(B);
 }
 
+std::string
+debugString(const std::vector<BoolValue *> &Constraints,
+            const Solver::Result &Result,
+            llvm::DenseMap<const AtomicBoolValue *, std::string> AtomNames) {
+  return DebugStringGenerator(std::move(AtomNames))
+      .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;
 
(and
         B0)
     (or
         True
         B1)))";
   EXPECT_THAT(debugString(*B, {{True, "True"}, {False, "False"}}),
               StrEq(Expected));
 }
 
+Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) {
+  llvm::DenseSet<BoolValue *> ConstraintsSet(Constraints.begin(),
+                                             Constraints.end());
+  return WatchedLiteralsSolver().solve(std::move(ConstraintsSet));
+}
+
+TEST(SATCheckDebugStringTest, AtomicBoolean) {
+  // B0
+  ConstraintContext Ctx;
+  std::vector<BoolValue *> Constraints({Ctx.atom()});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+------------
+Satisfiable.
+
+B0 = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, AtomicBooleanAndNegation) {
+  // B0, !B0
+  ConstraintContext Ctx;
+  auto B0 = Ctx.atom();
+  std::vector<BoolValue *> Constraints({B0, Ctx.neg(B0)});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+(not
+    B0)
+------------
+Unsatisfiable.
+
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, MultipleAtomicBooleans) {
+  // B0, B1
+  ConstraintContext Ctx;
+  std::vector<BoolValue *> Constraints({Ctx.atom(), Ctx.atom()});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+B1
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, Implication) {
+  // B0, B0 => B1
+  ConstraintContext Ctx;
+  auto B0 = Ctx.atom();
+  auto B1 = Ctx.atom();
+  auto Impl = Ctx.disj(Ctx.neg(B0), B1);
+  std::vector<BoolValue *> Constraints({B0, Impl});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+(or
+    (not
+        B0)
+    B1)
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, Iff) {
+  // B0, B0 <=> B1
+  ConstraintContext Ctx;
+  auto B0 = Ctx.atom();
+  auto B1 = Ctx.atom();
+  auto Iff = Ctx.conj(Ctx.disj(Ctx.neg(B0), B1), Ctx.disj(B0, Ctx.neg(B1)));
+  std::vector<BoolValue *> Constraints({B0, Iff});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+(and
+    (or
+        (not
+            B0)
+        B1)
+    (or
+        B0
+        (not
+            B1)))
+------------
+Satisfiable.
+
+B0 = True
+B1 = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, Xor) {
+  // B0, XOR(B0, B1)
+  ConstraintContext Ctx;
+  auto B0 = Ctx.atom();
+  auto B1 = Ctx.atom();
+  auto XOR = Ctx.disj(Ctx.conj(B0, Ctx.neg(B1)), Ctx.conj(Ctx.neg(B0), B1));
+  std::vector<BoolValue *> Constraints({B0, XOR});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+B0
+
+(or
+    (and
+        B0
+        (not
+            B1))
+    (and
+        (not
+            B0)
+        B1))
+------------
+Satisfiable.
+
+B0 = True
+B1 = False
+)";
+  EXPECT_THAT(debugString(Constraints, Result), StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, ComplexBooleanWithNames) {
+  // Cond, (Cond ^ Then ^ !Else) v (!Cond ^ !Then ^ Else)
+  ConstraintContext Ctx;
+  auto Cond = cast<AtomicBoolValue>(Ctx.atom());
+  auto Then = cast<AtomicBoolValue>(Ctx.atom());
+  auto Else = cast<AtomicBoolValue>(Ctx.atom());
+  auto B = Ctx.disj(Ctx.conj(Cond, Ctx.conj(Then, Ctx.neg(Else))),
+                    Ctx.conj(Ctx.neg(Cond), Ctx.conj(Ctx.neg(Then), Else)));
+  std::vector<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.
+
+Cond = True
+Else = False
+Then = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result,
+                          {{Cond, "Cond"}, {Then, "Then"}, {Else, "Else"}}),
+              StrEq(Expected));
+}
+
+TEST(SATCheckDebugStringTest, ComplexBooleanWithLongNames) {
+  // ThisIntEqZero, !IntsAreEq, ThisIntEqZero ^ OtherIntEqZero => IntsAreEq
+  ConstraintContext Ctx;
+  auto IntsAreEq = cast<AtomicBoolValue>(Ctx.atom());
+  auto ThisIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
+  auto OtherIntEqZero = cast<AtomicBoolValue>(Ctx.atom());
+  auto BothZeroImpliesEQ =
+      Ctx.disj(Ctx.neg(Ctx.conj(ThisIntEqZero, OtherIntEqZero)), IntsAreEq);
+  std::vector<BoolValue *> Constraints(
+      {ThisIntEqZero, Ctx.neg(IntsAreEq), BothZeroImpliesEQ});
+  auto Result = CheckSAT(Constraints);
+
+  auto Expected = R"(
+Constraints
+------------
+ThisIntEqZero
+
+(not
+    IntsAreEq)
+
+(or
+    (not
+        (and
+            ThisIntEqZero
+            OtherIntEqZero))
+    IntsAreEq)
+------------
+Satisfiable.
+
+IntsAreEq      = False
+OtherIntEqZero = False
+ThisIntEqZero  = True
+)";
+  EXPECT_THAT(debugString(Constraints, Result,
+                          {{IntsAreEq, "IntsAreEq"},
+                           {ThisIntEqZero, "ThisIntEqZero"},
+                           {OtherIntEqZero, "OtherIntEqZero"}}),
+              StrEq(Expected));
+}
 } // namespace