How to Run Semantics
The following instructions are for standard Debian/Ubuntu distributions, especially for Ubuntu 14.04 LTS 64-bit.
0. Install Basic Dependencies
Install JDK 1.8:
$ sudo add-apt-repository ppa:webupd8team/java $ sudo apt-get update $ sudo apt-get install oracle-java8-installer
$ sudo apt-get install build-essential $ sudo apt-get install git $ sudo apt-get install maven
1. Install K
This semantics is compatible with a customized version of the latest K framework. You can install the version of K as follows:
$ git clone https://github.com/kframework/k.git $ cd k $ git checkout -b kjs origin/kjs $ mvn package
krun are included in your
$ export PATH=$PATH:<path-to-k>/k-distribution/target/release/k/bin
2. Install Node.js
We use Node.js implementation
Number.toString to test programs modulo the unsupported libraries.
$ sudo apt-get install nodejs $ (cd $(dirname `which nodejs`); sudo ln -s nodejs node)
3. Install KJS
You can compile the semantics using Makefile:
4. Run KJS
For a 'hello-world' example,
$ cat >hello-world.js <<EOL console.log("hello world!"); EOL $ ./kjs.sh hello-world.js hello world!
Note that, however, KJS support only a part of standard libraries,
and may fail to run a program with unsupported libraries
KJS fails to run the following program,
getting stuck at the unsupported library function call:
$ cat >time.js <<EOL console.log(Date.now()); EOL $ ./kjs.sh time.js Error: failed to run the program: time.js Check the dumped output: /tmp/kjs.bd7uNgkKud.out $ cat /tmp/kjs.bd7uNgkKud.out <T> <k> Call ( @ ( "Date.now" ) , @DateOid , @Nil ) ~> Exit ; </k> ...
You can run the core ECMAScript conformance test suite (2,782 tests in total) as follows:
N is a number of parallel processes to be used)
$ make -k -j N test262-core
Running all the tests will take 2 hours using 4 parallel processes in a machine with Intel Xeon CPU 3.40GHz and DDR3 RAM 8GB 1600MHz.
You can also selectively run a part of the tests by using the environment variables:
$ TEST262_CORE_POSITIVE=<list-of-positive-tests> make test262-core-positive $ TEST262_CORE_NEGATIVE=<list-of-negative-tests> make test262-core-negative
Test Result of test262
We provide a test result of the core test262, test262.out.
For each test, it reports
succeed when passed the test, and
failed when failed.
Note that there are two types of tests: positive and negative tests. A negative test is identified by
@negative in its preamble. The negative tests should fail to run.
Among the 2,782 core tests, our semantics reports parsing errors for the following 6 programs,
which is the correct behavior according to the language standard
ECMAScript 5.1 specification.
These programs have function declarations inside a local block such as
while function declaration is only allowed at top-level
(refer to the grammar specification Annex A.5 Functions and Programs).
This grammar mismatch problem was already admitted by the standard committee, and will be corrected in the next standard:
Draft Specification of Ecma-262 Edition 6.
test262-9b669da66c78/test/suite/ch10/10.4/10.4.2/10.4.2-1-2.js test262-9b669da66c78/test/suite/ch12/12.14/12.14-13.js test262-9b669da66c78/test/suite/ch12/12.8/S12.8_A3.js test262-9b669da66c78/test/suite/ch12/12.8/S12.8_A4_T1.js test262-9b669da66c78/test/suite/ch12/12.8/S12.8_A4_T2.js test262-9b669da66c78/test/suite/ch12/12.8/S12.8_A4_T3.js
Note that we consider the above tests as negative tests, such that it will report
Built-in Objects Support
Currently, KJS supports the standard built-in objects as follows:
- Fully defined:
- Partially defined:
- Not defined:
js-main.k: Core semantics
js-core-syntax.k: IR syntax
js-pseudo-code.k: Pseudo-code semantics
js-str-numeric-literal.k: Paring numeric literals
js-init-configuration.k: Initial configuration
js-prelude.k: K built-in modules
js-standard-builtin-objects.k: Standard built-in objects' constructor semantics
security-attack: Security attack detection using symbolic execution
test262-coverage: Test coverage measurement of test262 w.r.t. the standard
verification: Program verification based on the semantics
Makefile: Compile semantics
kpp.py: Create a single K file from the multiple files
Makefile.test262: Run test262 programs
test262.out: Test result of the core test262
prelude.js: Prelude of test262
jsmassage.sh: Wrapper of SAFE framework
Note: A virtual machine, in which all of the required programs and libraries have been installed and configured, is provided at: