-
Notifications
You must be signed in to change notification settings - Fork 3
PLDI16 AEC submission
Download the VM image here: http://goto.ucsd.edu/~pvekris/VMs/PLDI16-AEC/
Load the image on VirtualBox.
If needed, the username and password are both pldi16-aec.
You can find the (conditionally) accepted version of the paper here: http://goto.ucsd.edu/~pvekris/docs/pldi16-paper161.pdf
First, open a terminal and cd ~/refscript.
stack exec -- rsc /path/to/file.ts
This will run our tool on the given TypeScript file; for well-formed inputs the output should end in either *** SAFE *** or *** UNSAFE ***.
See below for demonstrative examples.
stack test refscript:regression
For each of the 571 regression tests, this should output a line looking like obj-07.ts: OK (0.65s). It should take ~8 minutes.
In section 5 of the paper we report the running times of our benchmark suite. You can run those tests as follows:
stack test refscript:pldi16
It should take ~10-15 minutes; the vast majority of that time it will appear to be doing nothing as it handles our most time-consuming test, navier-stokes-typed-octane.ts.
tests/demo contains tests that demonstrate various features of rsc. They are listed below along with some features they exhibit.
-
cast.ts(casting) -
createElt.ts(casting, instanceof test) -
ctor.ts(constructors, mutability of fields) -
d3-sum.ts(inferring loop invariants, optional arguments, higher-order function) -
infer.ts(inference, object literals, safety of array accesses) -
lor.ts(type unions) -
minindex-classic.ts(safety of array accesses) minindex-modern-lib.ts-
minindex-modern.ts(higher-order function) -
negate.ts(typeof test) -
opt-args.ts(optional arguments) -
poly.ts(polymorphism) -
reals.ts(real-valued non-linear arithmetic - note that you need to run this with the --real flag) -
string-coercion.ts(typeof test) -
variadic.ts(anonymous function, invoking a variadic function) while-rec.ts
All return SAFE in their current form, but we encourage you to change them to see that rsc does successfully reject unsafe programs - in some of the tests we've suggested example changes in comments saying // Try [some change]
If you want to build from source:
- stack The Haskell Tool Stack
- Node.js (tested version v4.2.1) (You must get an executable called 'node' on your PATH - some versions may only create a 'nodejs' in which case you can rename/symlink)
- Z3 Binary version >= 4.3.2
git clone --recursive https://github.com/UCSD-PL/refscript
cd refscript
git checkout pldi16
git submodule update
stack setup
stack build