The new branch contains a direct port of the interpreter and concolic tester that were present in Safe 1.0. This branch contains most of the functionalities of these components from Safe 1.0. Most notably, the code for dealing with regexes has not been ported, so the new interpreter and tester do not support regexes (and will throw a Scala NotImplementedError). Also of note is the fact that I added a new internal call for "print", to print something to stdout. This call corresponds to the _<>_print feature of the original Safe 1.0 framework,
The interpreter can be executed via:
safe interpret file_name [-interpreter:ecma]
The concolic tester can be executed via:
safe concolic file_name
The optional -interpreter:ecma flag can be used when running the ECMA specification tests from the tests/test262 folder. This flag makes it possible to test the correctness of the interpreter for to these files by checking whether the variables of the form "resultX" have the same value as the corresponding variable of the form "expectX". When using this flag, if a violation is dected (when the value of these variables is not equal), the Safe interpreter logs the name of the testfile that caused the violation in the file "ecma_violations.txt". If an uncaught run-time exception is thrown, part of the stacktrace is logged to "ecma_errors.txt:".
I have run the interpreter of Safe 1 and Safe 2 with the ECMA flag on all non-todo ECMA tests in the test262/ folder (see also the run_interpreter_tests.sh script) and added the resulting "ecma_violations.txt" and "ecma_errors.txt" files to the repository. It seems that the new interpreter has about the same accuracy as the Safe 1.0 interpreter, although both interpreters fail on a (rather small) number of test cases.
The new concolic tester seems to achieve as much coverage as the Safe 1.0 concolic tester. The tester still fails on some files, such as most of the files in the tests/concolic_tests/benchmarks folder, but it seems that the Safe 1.0 tester also failed on those.
The console messages that are printed during concolic execution have been changed slightly: most notably, when an unsatisfiable path constraint is generated, the tester ignores this instead of printing the stacktrace.
I have updated most of the old Safe 1.0 code for these two components so that they follow the most essential rules from the Safe development style guides, but some parts of the code could still use some refactoring so that they are completely up-to-date with the new style (e.g., by using a more functional style instead of the current, imperative one, using optional values instead of null-values, more documentation etc.).
I will probably keep working on this code for my own research projects, so I would be happy to create other pull requests when this code has been updated, or when I have fixed some of the small bugs still remaining in the interpreter and concolic tester.
If you have any questions or comments about the port, I'd be happy to answer them.
The new branch contains a direct port of the interpreter and concolic tester that were present in Safe 1.0. This branch contains most of the functionalities of these components from Safe 1.0. Most notably, the code for dealing with regexes has not been ported, so the new interpreter and tester do not support regexes (and will throw a Scala NotImplementedError). Also of note is the fact that I added a new internal call for "print", to print something to stdout. This call corresponds to the _<>_print feature of the original Safe 1.0 framework,
The interpreter can be executed via: safe interpret file_name [-interpreter:ecma]
The concolic tester can be executed via: safe concolic file_name
The optional -interpreter:ecma flag can be used when running the ECMA specification tests from the tests/test262 folder. This flag makes it possible to test the correctness of the interpreter for to these files by checking whether the variables of the form "resultX" have the same value as the corresponding variable of the form "expectX". When using this flag, if a violation is dected (when the value of these variables is not equal), the Safe interpreter logs the name of the testfile that caused the violation in the file "ecma_violations.txt". If an uncaught run-time exception is thrown, part of the stacktrace is logged to "ecma_errors.txt:".
I have run the interpreter of Safe 1 and Safe 2 with the ECMA flag on all non-todo ECMA tests in the test262/ folder (see also the run_interpreter_tests.sh script) and added the resulting "ecma_violations.txt" and "ecma_errors.txt" files to the repository. It seems that the new interpreter has about the same accuracy as the Safe 1.0 interpreter, although both interpreters fail on a (rather small) number of test cases.
The new concolic tester seems to achieve as much coverage as the Safe 1.0 concolic tester. The tester still fails on some files, such as most of the files in the tests/concolic_tests/benchmarks folder, but it seems that the Safe 1.0 tester also failed on those. The console messages that are printed during concolic execution have been changed slightly: most notably, when an unsatisfiable path constraint is generated, the tester ignores this instead of printing the stacktrace.
I have updated most of the old Safe 1.0 code for these two components so that they follow the most essential rules from the Safe development style guides, but some parts of the code could still use some refactoring so that they are completely up-to-date with the new style (e.g., by using a more functional style instead of the current, imperative one, using optional values instead of null-values, more documentation etc.). I will probably keep working on this code for my own research projects, so I would be happy to create other pull requests when this code has been updated, or when I have fixed some of the small bugs still remaining in the interpreter and concolic tester.
If you have any questions or comments about the port, I'd be happy to answer them.