=================================================
PIE : Precondition Inference Engine
--------------------------------------------------------------------------------------------------

0. Dependencies
..................................................................................................

0.0] Environment + Compilers
- Bash
- Python 2, Python 3
- OCaml 4.0+
- LLVM+Clang source (3.6+) for invariant inference (cloned in Repos)

0.1] Libraries
- pyparsing (Python)
- batteries (OCaml)
- qcheck (OCaml)

0.2] Constraint solvers
- Z3Str2 (cloned in Repos)
- CVC4 (cloned in Repos)


1. Running the tests
..................................................................................................

1.1] Precondition Inference tests:
- Precondition Inference
- Repos/PIE/specs
- Run all tests: ./test_all.sh <cg>
  - cg = optional cgroup container name or ""
- Test specific func F in module M:
    ./test.sh <M> <F> <cg> <tests> <sz_c>
  - M = Module file (list.ml)
  - F = Function Id (4)
  - cg = cgroup name (leave "")*
  - tests = random tests count (6400)
  - sz_c = size of conflict groups (16); use "all" for full size

1.1] Loop Invariant Inference tests:
- Run in Repos/llvm/build
- To run all tests over all configs: ./check_all <cg>
  - cg = optional cgroup container name or ""
- To run specific benchmark B:
    ./checker <B> <tests> <tool> <cg> <sz_c>
  - B = Path to benchmark file (../../PIE/bm_strings/cav2014d.cpp)
  - tests = random tests count (6400)
  - tool = PIE vs just Escher (pie)
  - cg = cgroup container name (leave "")
  - sz_c = size of conflict groups (16); use "all" for full size

2. Modifying and re-building
..................................................................................................

2.1] Modifying PIE
- Repos/PIE/base/ has PIE code
- Repos/PIE/abduce/ has code for abduction using PIE
- Repos/PIE/bm_*/ are various benchmark suits (for loop invariant inference)
- Repos/PIE/specs/ has test code & cases for precondition inference
- Repos/PIE/hybrid has the interface for hybrid verifier to PIE (CVC4 + Z3Str2)
- Repos/PIE/pldi_logs has cleaned logs generated on my machine for benchmarks mentioned in PLDI submission
- No rebuilding necessary

2.2] Modifying clang tool
- Modify within Repos/PIE/ClangTool/pinvgen/
- Run Repos/PIE/ClangTool/setup.sh <LLVM_ROOT> <cg>
  - LLVM_ROOT = ../../llvm
  - cg = cgroup container name (if you have created one); or ""

Thanks for testing!
=================================================