Folder Structure

Note

Folders marked with (❌PLDI20) are out of scope of the PLDI 2020 Gillian Paper.

  • Gillian-JS

    • bin: The Gillian-JS binary

    • environment: Execution environment, not part of the repository, created using make js-init-env. It contains useful scripts for testing Gillian-JS, and examples are copied in it so that they can be safely modified.

    • examples: Various examples

      • Fantine: Bi-abduction examples (❌PLDI20)

      • Cosette: Symbolic testing examples

        • buckets: Tests for the Buckets.js library

        • case_studies: Data structures used for initial evaluation (not reported)

      • JaVerT: Verification examples (❌PLDI20)

    • lib: The core of Gillian-JS

      • compiler: The JS-2-GIL compiler

      • JSIL: Syntax of JSIL and related constructs

      • JSLogic: Verification-related constructs (assertions, predicates, specifications, etc.) (❌PLDI20)

      • parsing: JSIL parsing (programs, annotations, etc.)

      • semantics: Implementation of concrete and symbolic memory models

        • CObject.ml: Concrete objects

        • CHeap.ml: Concrete heaps

        • JSILCMemory.ml: Concrete memory

        • SFVL.ml: Symbolic field-value lists

        • SHeap.ml: Symbolic heaps

        • JSILSMemory.ml: Symbolic memory

      • test262: Bulk testing for the Test262 test suite

      • utils: Various utilities (configuration, I/O, etc.)

    • runtime: JS-2-GIL compiler runtime (JSIL implementations of JavaScript internal and built-in functions)

    • scripts: Various scripts for setting up the environment and running analyses