-
Notifications
You must be signed in to change notification settings - Fork 5
Problem statement
While developing test cases aw well as Py2EO transpiler itself we faced the problem of validating:
- The correctness of test execution.
- The Correctness of transpilation of specific Python language statements.
The Py2EO test case processing can be described as follows:
- Using the antlr parser, from the Python source code, we get the (Python) AST tree.
- Performing simplifying passes from (Python) AST tree to (Python) AST tree.
- Generating EO source code from simplified (Python) AST tree.
- Using the translator from EO to Java, we get the source code in java
- Compiling Java source code to Java byte code
- Execute Java byte code on JVM
Due to the facts that:
- Not all tests (even fairly simple ones) go through all these stages successfully, and it is not known whether and how successfully they will be able to do this in the future.
- With the help of our test cases, it is difficult to answer the question what constructs of the input language does our translator support, and in what degree.
- Quickly localize transpilation pass problem/error in the aspect of a particular input language statement.
We came to the problem of constructing a mechanism for validating the correctness of an traspilation pass. Since we noticed the fact that quite similar test cases were often performed in completely different ways, we decided to try the source code mutation approach.
Having considered the possible options and test process artifacts to build a checking mechanism on, we were able to highlight the following: Input language specification:
- Formal grammar as a list of statements
- Formal grammar specified in an other formal way
- Specification written in natural language
Types of test cases:
- Trivial statement(or keyword)-specific synthetic tests (easy to write by hand, easy to generate from formal grammar)
- Test packages supplied by the input language developers (such as CPython for Python)
- Live (popular) projects from github, selected "randomly", considered both in a complex and per file (one file - one test) manner.
Types of mutations:
- Self-written mutations of various types (Injurious/non-injurious, ...), many of which we have tried for Py2EO checker
- Generation of mutations that perform the correct (by syntax) replacement of an arbitrary (specific) statement with an another arbitrary (specific) statement
Stages of test case without applying mutation processing for abstract transpiler:
- Source code in original language
- Instrumented source code (in a trivial case, the same as the original, the option is to insert prints)
- AST tree
- Text in output language
- Execution result
Stages of test case AFTER applying mutation processing for abstract transpiler:
- Source code in original language
- Instrumented source code (in a trivial case, the same as the original, the option is to insert prints)
- AST tree
- Text in output language
- Execution result
Comparison methods (original test case and mutated test case) to evaluate results ("sensitivity"):
- Compare the depth of passing the processing stages
- Compare tests states at one of the particular stage
- Compare by the instrumentation markers
here we need comparison table
Insensitivity == property of the translator, which manifests that when two different inputs generating same result.
Sensitivity == property of the translator, which manifests that there are no two different inputs generating same result.
We get a lot of tests and a lot of mutations + a list of statements (from formal grammar) as input
- Complete coverage of input language by multiple tests and mutations Initial tests + all tests obtained as a result of mutations (each mutation for each test once)
- Search for translation errors comparison in pairs before and after the mutation (there are suspicious constructs in the mutated one, but not in the original one)
Evidence base level:
- Particular experiment on Py2EO
- Experiment for other python translators
- Experiment for other translators of other languages
- Formal proof