[PATCH] D86966: [ConstraintSystem] Improve printing.

Florian Hahn via Phabricator via llvm-commits llvm-commits at lists.llvm.org
Tue Sep 1 12:12:33 PDT 2020


fhahn created this revision.
Herald added a subscriber: hiraditya.
Herald added a project: LLVM.
fhahn requested review of this revision.

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.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D86966

Files:
  llvm/include/llvm/Analysis/ConstraintSystem.h
  llvm/lib/Analysis/ConstraintSystem.cpp
  llvm/utils/convert-constraint-log-to-z3.py

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D86966.289247.patch
Type: text/x-patch
Size: 5674 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200901/0da5e52f/attachment.bin>


More information about the llvm-commits mailing list