Implementation of DDPA and related program analyses.
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.


Artifact for the paper Higher-Order Demand-Driven Program Analysis.

Leandro Facchinetti The Johns Hopkins University
Zachary Palmer Swarthmore College
Scott F. Smith The Johns Hopkins University


  1. Install OCaml and OPAM.

    Windows Instructions

    Install OCaml for Windows, which includes the Cygwin shell with OCaml and OPAM preinstalled.

  2. Initialize OPAM:

    $ opam init
    $ eval `opam config env`
  3. Update & upgrade:

    $ opam update
    $ opam upgrade
  4. Switch to the appropriate compiler version:

    $ opam switch 4.06.1
    $ eval `opam config env`
    Windows Instructions


    $ opam switch 4.06.1+mingw64
    $ eval `opam config env`


    $ opam switch 4.06.1+mingw32
    $ eval `opam config env`

    depending on the system.

  5. Install the dependencies:

    $ opam install oasis \
                   batteries \
                   menhir \
                   ounit \
                   ppx_deriving \
                   ppx_deriving_yojson \
                   "ocaml-monadic=0.4.0" \
                   monadlib \
                   "jhupllib=0.1.1" \

    Note that newer versions of some of the constrained packages above may work, but the above-listed versions were tested with this project.

  6. If your shell hashes binary locations, you may need to clear your hashes, for example (in Bash):

    $ hash -r
  7. Generate configuration:

    $ oasis setup -setup-update dynamic
  8. Configure:

    $ ./configure
  9. Enable tests:

    $ ocaml -configure --enable-tests
  10. Build:

    $ make
  11. Interact with the toploop (find sample programs at test-sources/):

    $ ./toploop_main.native
  12. Run the tests:

    $ make test

toploop_main.native Command-Line Arguments

  • --log=trace: Enable verbose logging.
  • --disable-inconsistency-check: By default, the toploop checks programs for inconsistencies. For example, it checks that only functions appear in the operator position of a function call, and that only records appear in the subject position of a record projection. This inconsistency check forces variable lookups that interfere with benchmarking, and this flag disables it.
  • --select-context-stack=0ddpa: Uses DDPA with a 0-level context stack (which is a monovariant analysis). Any positive integer value is admitted here (e.g. 7ddpa).

Run the following for extended help (including options to produce diagrams of the incremental PDR graphs):

$ ./toploop_main.native --help


  1. Install Odefa.
  2. Install Racket 6.12 or newer.
  3. Install Racket dependencies:
    $ raco pkg install gregor
  4. Install P4F.
  5. Run benchmark/
    $ bash benchmark/
  6. Run benchmark/collect-results.rkt:
    $ racket benchmark/collect-results.rkt

Developer Setup

Odefa depends on libraries which tend to develop at the same time as it does, but which are functionally independent and are designed to be used by other projects. Configure these libraries for local development by pinning them:

  1. jhupllib:

    $ git clone ../jhu-pl-lib
    $ opam pin add jhupllib ../jhu-pl-lib
  2. pds-reachability:

    $ git clone ../pds-reachability
    $ opam pin add pds-reachability ../pds-reachability

Re-run opam pin when these libraries change.