These files enable replication of results reported at the 2020 BAR Workshop
For the paper "Creating Human Readable Path Constraints from Symbolic Execution"

Be sure to install angr and the logic synthesis tool SIS.

This code uses sis 1.3, downloaded via a link from:
http://cs.columbia/edu/~cs6861/sis/sis/html

Section II-A, III-B (results for II-A)
   cat sub1or2.c
   objdump -M intel -d sub1or2
   python show_constraint_for_sub1or2.py

Section II-B, III-B (results for II-B)
   cat readtowrite.c
   python show_constraint_for_readtowrite.py

Section II-C, III-C:
  cat authentication.c
  cat authentication.eqn
  python show_constraint_for_authentication.py
  ~/sis1.3/bin/sis -c \
    "full_simplify; decomp -g; read_library authentication.genlib; map" \
    -T eqn -t eqn authentication.eqn 

Logic synthesis for simplification et.al.:
  python misc_bv_to_int_stuff.py
  
If you are interested in this work, you can send me email at:  amon.tod@gmail.com or ttamon@sandia.gov
This work is ongoing and the files in this repository reflect the research state prior to the BAR
conference.  There is a lot of new work, but it has not been publicly released yet.