[ConstraintSystem] Improve printing.

[fhahn]

Summary

This patch improves printing of the constraint system to also allow
specifying names for variables.

It also adds a convert-constraint-log-to-z3.py script, which can parse
the debug output of the constraint system and convert it to a python
script that feeds the constraints into Z3 and checks if it produces the
same result as the LLVM implementation. This is for verification
purposes.

[fhahn]

Folded into D84544

llvm/include/llvm/Analysis/ConstraintSystem.h

 //===- ConstraintSystem.h -  A system of linear constraints. --------------===//
 //
 // 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
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_ANALYSIS_CONSTRAINTSOLVER_H
 #define LLVM_ANALYSIS_CONSTRAINTSOLVER_H
 
 #include "llvm/ADT/APInt.h"
+#include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/SmallVector.h"
 #include <cstdlib>
+#include <string>
 
 namespace llvm {
 
 class ConstraintSystem {
   /// Current linear constraints in the system.
   /// An entry of the form c0, c1, ... cn represents the following constraint:
   ///   c0 >= v0 * c1 + .... + v{n-1} * cn
   SmallVector<SmallVector<int64_t, 8>, 4> Constraints;
 
   /// Current greatest common divisor for all coefficients in the system.
   uint32_t GCD = 1;
 
   uint32_t NumVariables = 0;
 
   // Eliminate constraints from the system using Fourier–Motzkin elimination.
   bool eliminateUsingFM();
 
-  /// Print the constraints in the system.
+  /// Print the constraints in the system, using \p Names as variable names.
+  void dump(ArrayRef<std::string> Names);
+
+  /// Print the constraints in the system, using x0...xn as variable names.
   void dump();
 
+  /// Retuns true if there may be a solution for the constraints in the system.
+  bool mayHaveSolutionImpl();
+
 public:
   void addVariableRow(const SmallVector<int64_t, 8> &R) {
     assert(Constraints.empty() || R.size() == Constraints.back().size());
     for (auto &C : R) {
       auto A = std::abs(C);
       GCD = APIntOps::GreatestCommonDivisor({32, (uint32_t)A}, {32, GCD})
                 .getZExtValue();
     }

llvm/lib/Analysis/ConstraintSystem.cpp

 //===- ConstraintSytem.cpp - A system of linear 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
 //
 //===----------------------------------------------------------------------===//
 
 #include "llvm/Analysis/ConstraintSystem.h"
+#include "llvm/ADT/SmallVector.h"
+#include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/Debug.h"
 
 #include <algorithm>
 #include <cmath>
 #include <iostream>
 
 using namespace llvm;
 
+#define DEBUG_TYPE "constraint-system"
+
 bool ConstraintSystem::eliminateUsingFM() {
   // Implementation of Fourier–Motzkin elimination, with some tricks from the
   // paper Pugh, William. "The Omega test: a fast and practical integer
   // programming algorithm for dependence
   //  analysis."
   // Supercomputing'91: Proceedings of the 1991 ACM/
   // IEEE conference on Supercomputing. IEEE, 1991.
   assert(!Constraints.empty());
for (unsigned R1 = 0; R1 < Constraints.size(); R1++) {
     }
   }
   Constraints = std::move(NewSystem);
   GCD = NewGCD;
 
   return true;
 }
 
-bool ConstraintSystem::mayHaveSolution() {
+bool ConstraintSystem::mayHaveSolutionImpl() {
   while (!Constraints.empty() && Constraints[0].size() > 1) {
     if (!eliminateUsingFM())
       return true;
   }
 
   if (Constraints.empty())
     return true;
   if (Constraints[0].size() > 1)
     return true;
   for (auto &R : Constraints) {
     if (R[0] < 0)
       return false;
   }
   return true;
 }
 
-void ConstraintSystem::dump() {
+void ConstraintSystem::dump(ArrayRef<std::string> Names) {
   if (Constraints.empty())
     return;
 
-  std::cout << "c\t";
-  for (unsigned i = 1; i < Constraints[0].size(); i++)
-    std::cout << "x" << i << "\t";
-  std::cout << "\n";
-  for (auto &R : Constraints) {
-    for (auto a : R)
-      std::cout << a << "\t";
-    std::cout << "\n";
-  }
+  for (auto &Row : Constraints) {
+    SmallVector<std::string, 16> Parts;
+    for (unsigned i = 1; i < Row.size(); ++i) {
+      if (Row[i] == 0)
+        continue;
+      std::string Coefficient = "";
+      if (Row[i] != 1)
+        Coefficient = std::to_string(Row[i]) + " * ";
+      Parts.push_back(Coefficient + Names[i - 1]);
+    }
+    assert(!Parts.empty());
+    LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
+                      << " <= " << std::to_string(Row[0]) << "\n");
+  }
+
+void ConstraintSystem::dump() {
+  SmallVector<std::string, 16> Names;
+  for (unsigned i = 1; i < Constraints.back().size(); ++i)
+    Names.push_back("x" + std::to_string(i));
+  LLVM_DEBUG(dbgs() << "---\n");
+  dump(Names);
+}
+
+bool ConstraintSystem::mayHaveSolution() {
+  dump();
+  bool HasSolution = mayHaveSolutionImpl();
+  LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
+  return HasSolution;
 }
 
 bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) {
   // If there is no solution with the negation of R added to the system, the
   // condition must hold based on the exsisting constraints.
   R = ConstraintSystem::negate(R);
 
   auto NewSystem = *this;
   NewSystem.addVariableRow(R);
   return !NewSystem.mayHaveSolution();
 }

llvm/utils/convert-constraint-log-to-z3.py

+#!/usr/bin/env python
+
+"""
+Helper script to convert the log generated by '-debug-only=constraint-system'
+to a Python script that uses Z3 to verify the decisions using Z3's Python API.
+
+Example usage:
+
+> cat path/to/file.log
+---
+x6 + -1 * x7 <= -1
+x6 + -1 * x7 <= -2
+sat
+
+> ./convert-constraint-log-to-z3.py path/to/file.log > check.py && python ./check.py
+
+> cat check.py
+    from z3 import *
+x3 = Int("x3")
+x1 = Int("x1")
+x2 = Int("x2")
+s = Solver()
+s.add(x1 + -1 * x2 <= 0)
+s.add(x2 + -1 * x3 <= 0)
+s.add(-1 * x1 + x3 <= -1)
+assert(s.check() == unsat)
+print('all checks passed')
+"""
+
+
+import argparse
+import re
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description='Convert constraint log to script to verify using Z3.')
+    parser.add_argument('log_file', metavar='log', type=str,
+                        help='constraint-system log file')
+    args = parser.parse_args()
+
+    content = ''
+    with open(args.log_file, 'rt') as f:
+        content = f.read()
+
+    groups = content.split('---')
+    var_re = re.compile('x\d+')
+
+    print('from z3 import *')
+    for group in groups:
+        constraints = [g.strip() for g in group.split('\n') if g.strip() != '']
+        variables = set()
+        for c in constraints[:-1]:
+            for m in var_re.finditer(c):
+                variables.add(m.group())
+        if len(variables) == 0:
+            continue
+        for v in variables:
+            print('{} = Int("{}")'.format(v, v))
+        print('s = Solver()')
+        for c in constraints[:-1]:
+            print('s.add({})'.format(c))
+        expected = constraints[-1].strip()
+        print('assert(s.check() == {})'.format(expected))
+    print('print("all checks passed")')
+
+
+if __name__ == '__main__':
+    main()