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

   1 #!/usr/bin/env python
   2
   3 """
   4 Helper script to convert the log generated by '-debug-only=constraint-system'
   5 to a Python script that uses Z3 to verify the decisions using Z3's Python API.
   6
   7 Example usage:
   8
   9 > cat path/to/file.log
  10 ---
  11 x6 + -1 * x7 <= -1
  12 x6 + -1 * x7 <= -2
  13 sat
  14
  15 > ./convert-constraint-log-to-z3.py path/to/file.log > check.py && python ./check.py
  16
  17 > cat check.py
  18     from z3 import *
  19 x3 = Int("x3")
  20 x1 = Int("x1")
  21 x2 = Int("x2")
  22 s = Solver()
  23 s.add(x1 + -1 * x2 <= 0)
  24 s.add(x2 + -1 * x3 <= 0)
  25 s.add(-1 * x1 + x3 <= -1)
  26 assert(s.check() == unsat)
  27 print('all checks passed')
  28 """
  29
  30
  31 import argparse
  32 import re
  33
  34
  35 def main():
  36     parser = argparse.ArgumentParser(
  37         description="Convert constraint log to script to verify using Z3."
  38     )
  39     parser.add_argument(
  40         "log_file", metavar="log", type=str, help="constraint-system log file"
  41     )
  42     args = parser.parse_args()
  43
  44     content = ""
  45     with open(args.log_file, "rt") as f:
  46         content = f.read()
  47
  48     groups = content.split("---")
  49     var_re = re.compile("x\d+")
  50
  51     print("from z3 import *")
  52     for group in groups:
  53         constraints = [g.strip() for g in group.split("\n") if g.strip() != ""]
  54         variables = set()
  55         for c in constraints[:-1]:
  56             for m in var_re.finditer(c):
  57                 variables.add(m.group())
  58         if len(variables) == 0:
  59             continue
  60         for v in variables:
  61             print('{} = Int("{}")'.format(v, v))
  62         print("s = Solver()")
  63         for c in constraints[:-1]:
  64             print("s.add({})".format(c))
  65         expected = constraints[-1].strip()
  66         print("assert(s.check() == {})".format(expected))
  67     print('print("all checks passed")')
  68
  69
  70 if __name__ == "__main__":
  71     main()