PLDI 2020 Artifact Documentation

This is the documentation for the Gillian-JS aspect of the 'Gillian, Part I' PLDI 2020 submission artifact.

• JS-2-GIL and Test262
• Symbolic Test Results

Folder structure

INFO

Folders marked with 🚫 are out of scope of the PLDI 2020 Gillian Paper.

The relevant folders are located under the Gillian-JS/ directory:

• 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 example programs
  • 🚫 Fantine/: Bi-abduction examples
  • Cosette/: Symbolic testing examples
    • buckets/: Tests for the Buckets.js library
    • case_studies/: Data structures used for initial evaluation (not reported)
  • 🚫 JaVerT/: Verification examples
• lib/../: Gillian-JS source code
  • compiler/: The JS-2-GIL compiler
  • JSIL/: Syntax of JSIL and related constructs
  • 🚫 JSLogic/: Verification-related constructs (assertions, predicates, specifications, etc.)
  • 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 executing analyses

Symbolic testing

Fixes

Symbolic testing with Collections-C led to the following pull requests, fixing previously unknown bugs and instances of undefined behaviour:

• Fix buffer overflow (bug)
• Remove the usage of cc_comp_ptr (undefined behaviour)
• Test coincidentally passing while they should not (bugs and undefined behaviours)
• Fix overallocation (bug)
• Fix hashing function (performance-reducing bug)

Reproducing the results

For licensing reasons, we do not include the Collections-C code in the Gillian repository. There is an external repository that contains Collections-C code adapted for testing in Gillian-C and Klee.

To clone it, run these commands from the Gillian folder:

cd ..
git clone https://github.com/GillianPlatform/collections-c-for-gillian.git collection-c --branch PLDI20
cd Gillian

There are two ways to launch the tests:

• Using the bulk-wpst command of Gillian-C which has nicer output (using Rely), but cannot run the tests in parallel.
• Using a bash script that will run gillian-c wpst as many times as there are files to test, in parallel if desired (this is what we used in our measurements).

Using bulk-wpst

From the Gillian folder, run:

dune exec -- gillian-c bulk-wpst ../collections-c/for-gillian

You will see each test suite execute in sequence. Two tests will fail, as intended; they represent the two bugs described below.

Using the bash script

From the Gillian folder, for each folder you want to test, use:

Gillian-C/scripts/testFolder.sh ../collections-c/for-gillian/<folder>

For example, to run the test suite on singly-linked lists, run:

Gillian-C/scripts/testFolder.sh ../collections-c/for-gillian/slist

Notable bugs found

The array_test_remove.c buffer overflow bug

This test corresponds to the 'Fix buffer overflow' pull request. It is particularly interesting as the original test suite did not catch it. Interestingly, we expected a concrete test with the right values to catch it, but it could not; since our symbolic memory model cannot overflow, it caught the bug. This is because the buffer overflow didn't cause a failure, therefor indicating that this bug is a security issue.

The list_test_zipIterAdd.c flawed test

This is interesting for different reasons; while the library code it tests (list_zip_iter_add()) does not contain a bug, the test itself contains a bug, yet passes anyway.

The test adds two elements ("h" and "i") in two separate lists at index 2. It then tests that the elements actually appears at index 2 in the respective list, like so:

list_index_of(list1, "h", zero_if_ptr_eq, &index);
CHECK_EQUAL_C_INT(2, index);

list_index_of(list1, "i", zero_if_ptr_eq, &index);
CHECK_EQUAL_C_INT(2, index);

Notice that both tests are executed on list! Since "i" doesn't exist in list1 and list_index_of couldn't find it, it therefore didn't modify index. Since the first check succeeded, the value of index is still 2 and the test passes regardless.

Our symbolic tests, however, use symbolic 1-character strings, and assume the bare minimum information about the input values to make them pass, in order to explore as many paths as possible.

Here, we replaced every one-character string "X" with a respective one-character symbolic string str_X. For the test to pass, it should be enough for str_h to be different from every element in list1 and for str_i to be different from every element in list2; this is exactly what we assumed. However, we never assumed that str_i had to be different from every element in list1 as it's not required for the test to pass.

However, here, the equality between every element of list1 and str_i is tested. There is no indication as to the result of this test, so the execution branches. Therefore, there is a path created where list_index_of(list1, str_i, zero_if_ptr_eq, &index) will assign 0 to index, causing the test to fail.

This shows how symbolic testing can help write more robust tests.