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     parser.add_argument('log_file', metavar='log', type=str,
  39                         help='constraint-system log file')
  40     args = parser.parse_args()
  41
  42     content = ''
  43     with open(args.log_file, 'rt') as f:
  44         content = f.read()
  45
  46     groups = content.split('---')
  47     var_re = re.compile('x\d+')
  48
  49     print('from z3 import *')
  50     for group in groups:
  51         constraints = [g.strip() for g in group.split('\n') if g.strip() != '']
  52         variables = set()
  53         for c in constraints[:-1]:
  54             for m in var_re.finditer(c):
  55                 variables.add(m.group())
  56         if len(variables) == 0:
  57             continue
  58         for v in variables:
  59             print('{} = Int("{}")'.format(v, v))
  60         print('s = Solver()')
  61         for c in constraints[:-1]:
  62             print('s.add({})'.format(c))
  63         expected = constraints[-1].strip()
  64         print('assert(s.check() == {})'.format(expected))
  65     print('print("all checks passed")')
  66
  67
  68 if __name__ == '__main__':
  69     main()