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

## 0. System Setup
--------------------------------------------------------------------------------

0.0] Environment + Compilers
............................

0.0.0) System packages
- Bash
- Python 2, Python 3
- OCaml 4.0+

0.0.1) Built from sources
- LLVM+Clang source (3.6+) for invariant inference (cloned in Repos)

0.1] Libraries
..............
- pyparsing (for Python)
- batteries (for OCaml)
- qcheck (0.4+; for OCaml)

0.2] Constraint solvers
.......................
- Z3Str2 (latest version; cloned in Repos)
- CVC4 (latest version; cloned in Repos)

0.3] Notes
..........
- Default Username = Default Password = pie
- ~/Repos is symlinked to ~/Desktop/Repos for convenience



## 1. Running the tests
-------------------------------------------------------------------------------

1.0] Summary of tests and configurations
........................................

1.0.0) A configuration is defined as the following tuple:
           (number_of_tests , size_of_conflict_group)

       In our PLDI submission, we have evaluated the precondition inference
       tests over the following configurations to determine an `optimal`
       configuration: (Refer to Figure 10 in the paper)
           {1600, 3200, 6400, 12800} x {16}   U   {6400} x {2, 16, "all"}

1.0.1) Reported tests in PLDI submission
       We test all of these configurations with 101 precondition inference tests
       and the optimal configuration with the 29 loop invariant inference
       benchmarks. Additionally, we also test all 29 loop invariant inference
       benchmarks with only Escher to show that most of these benchmarks are not
       feasible with simply a program synthesizer.

1.1] Limiting & Monitoring Resource Usage
.........................................

1.1] Precondition Inference
...........................

This subsection would assume that the user's current working directory is
    ~/Repos/PIE/specs

1.1.0) Testing everything
  - Simply run ./test_all.sh

- We infer preconditions within

- 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
.............................
- 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

1.2] Limiting & monitoring resource usage using cgroups
.......................................................



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

2.0] 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.1] 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!