search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Testsuite Reorganisation #330

Open zilinc opened 4 years ago

zilinc commented 4 years ago

Description

Currently in the Cogent testsuite (https://github.com/NICTA/cogent/tree/master/cogent/tests), we only have two categories of test files, named pass_* and fail_*, which are tests which should pass or fail respectively. However Cogent has many phases, and many different configurations, and for any individual test case, we want to have finer-grained specification, indicating in what context and at which stage of compilation it should fail or pass.

This requires a way to specify a testing matrix, detailing the aforementioned information. The test driver should be itself easy to setup (for that reason I prefer some lightweight scripting language instead of a dependency-heavy language, e.g. Haskell). It's currently a shell script (https://github.com/NICTA/cogent/blob/master/cogent/scripts/cogent_validate.sh) invoked by a top-level Makefile (https://github.com/NICTA/cogent/blob/master/cogent/Makefile).

Progress

The new testing script has been merged to master and is in cogent/tests. See the README file for instructions on how to use it. #350 records the new feature requests.

TODOs

cmcl commented 4 years ago

I implemented a small test harness for the Frank programming language using Python. The framework supports a minimal set of directives which occur within comments of a test file. The intention of my framework was to support the aforementioned pass/fail files as well as specify files tied to compiler regressions, e.g. a file rX.cogent would correspond to issue #X on the Github tracker. A summary would split the results of testing into a number of categories: (un)expected passes/fails, and failed regressions.

I have described the main ideas in a document:

https://github.com/frank-lang/frank/blob/master/TestingIdeas

and the code is available here:

https://github.com/frank-lang/frank/blob/master/testharness.py

The small language of directives would need to be extended to support testing different compiler phases as currently it only compares the final return value against the expected output. However, the harness is not specific to Frank and I believe could be used as the basis of a more rigorous testing framework for the Cogent compiler.