Slicer is an interpreter for a simple ML-like language called iTML (imperative Transparent ML). This is companion code for paper "Imperative Functional Programs that Explain their Work" by Wilmer Ricciotti, Jan Stolarek, Roly Perera and James Cheney, published at International Conference on Functional Programming 2017. Upstream source code repository is located at https://github.com/jstolarek/slicer.
This software is written in Haskell. To build and install it you will need GHC 8.10 or above (some lower versions might work but were not tested) and a typical Haskell infrastructure (Cabal, access to Hackage).
git clone https://github.com/jstolarek/slicer
cd slicer
cabal build
To run the exact version published at ICFP 2017 checkout the relevant tag and follow a README there:
git checkout icfp2017-final
Note: you will need GHC 8.0 and legacy Cabal.
After following the above steps the slicer executable will be located at
dist-newstyle/build/$ARCH/$GHC-VER/slicer-1.0.0.0/x/slicer/build/slicer/slicer
where $ARCH
is your system architecture (e.g. x86_64-linux
) and $GHC-VER
is your GHC version (e.g. ghc-9.0.1
). For ease of use it's best to create a
symlink to the executable, e.g.:
ln -s dist-newstyle/build/x86_64-linux/ghc-9.0.1/slicer-1.0.0.0/x/slicer/build/slicer/slicer slicer
Example TML programs are located in examples
sub-directory. You can run them
by passing file name on the command line:
$ ./slicer examples/icfp17-example.tml
If all went well you should see the output:
Running examples/icfp17-example.tml
val it = let f = (fun f x =>
if x == 0
then y := 6 * !z
else _) in
try
f 0
with _ =>
_
;; !y : trace(int)
You can pass more than one file name at the same time.
Slicer provides a very simple REPL. Invoke it by passing --repl
flag:
$ ./slicer --repl
Welcome to Slicer REPL
slicer>
You can interact with REPL by providing single-line declarations and expressions:
slicer> data intlist = Nil | Cons int * intlist
slicer> let tail = fun tail (xs : intlist) : intlist => case xs of Nil -> Nil; Cons xs' -> snd xs'
val it = (fun tail xs =>
case xs of
Nil -> Nil;
Cons xs' -> snd xs') : (intlist -> intlist)
slicer> let t = trace (tail (Cons (1, Cons (2, Cons (3, Nil)))))
val it = trace (tail Cons (1, Cons (2, Cons (3, Nil)))) : trace(intlist)
slicer> bwdSlice (t, Cons (2, _:intlist))
val it = tail Cons (_, Cons (2, _)) : trace(intlist)
All example programs are packaged into a single test suite. Build and run the testsuite with:
cabal build
cabal test
The test suite will run every program in examples
directory and compare its
output with the expected output stored in a corresponding *.golden
file inside
tests/golden-templates/
.
Note: tests hardcode the executable path, which includes a particular
version of GHC. See SlicerTestSuiteUtils.slicerPath
- you might have to
adjust it on your machine.
You can run benchmarks with:
cabal build
cabal bench
In the paper we have discussed several examples. These are all located as
source files inside examples/
directory.
On the first page of the paper we present a following example:
let f(x) = if (x == 0) then y := 6 * !z else (y := 84 / !z; w := g(!y + 12)) in
try f 0 with x => y := 42);; !y
This example can be found in file icfp17-example.tml
. Run it with:
$ ./slicer examples/icfp17-example.tml
You can tweak initial value of z
and the value of argument passed to f
to
obtain different results. Remember that you must change the slicing
criterion to match the obtained result. So for example if you change initial
value of z
to be 0
rather than 7
you need to change the slicing
criterion from 42
to 0
. If you remove the try
-with
exception handler
and modify the code to cause division by zero the slicing criterion should be
raise "Division by zero"
.
On the third page of the paper we present a more elaborate example containing
a usage of map
. This example can be found in icfp17-example2.tml
source
file. Run it with:
$ ./slicer examples/icfp17-example2.tml
In section 6 we discuss an iTML program that solves a system of linear
equations by using simple Gaussian elimination without pivoting. This
program can be found in gauss.tml
source file (its pretty-printed version
can be found in Appendix C in the extended version of the paper). Run it
with:
$ ./slicer examples/gauss.tml
In this program we define two systems of equations. System defined by arrays
as
and bs
is solved correctly. System defined by arrays as'
and bs'
causes a division by zero. We then map gauss
function over a list
containing arrays defining both systems. This allows us to demonstrate that
our method works in a higher-order setting even for complex functions. Note
that we slice the program w.r.t. "Division by zero" exception. That is
because we know our program divides by zero and we want to understand why.
After running the program observe the results:
all elements of arrays as
and bs
are replaced with holes. This
means that neither of them contributed to raising the exception.
some elements of as'
are replaced with holes and some are not. This
means that some elements of that array contributed to raising the
exception. The last of the elements that was not replaced with a hole
is located at row 2, column 1 (0-based indexing). Knowing the nature of
Gaussian elimination leads us to conclusion that this is where the
division by zero must have taken place.
in the definition of gauss
method code responsible for zeroing
elements above the diagonal has been replaced by a hole. This means
that this code did not contribute to the result and so the exception was
raised when zeroing elements below the diagonal.
Syntax of iTML is based on ML. Here are some basic information that should get you started:
built-in primitive types are: int
, double
, bool
, string
and unit
.
iTML does not support polymorphic types
you can define your own ADTs but iTML only allows them to have two constructors. Moreover, constructors can only be nullary or unary. So a list of integers would be defined as:
data intlist = Nil | Cons (int * intlist)
A standard map
function defined over a list of integers (no polymorphism -
remember!) looks like this:
let map = fun map (f : int -> int) (xs : intlist) : intlist =>
case xs of
Nil -> Nil;
Cons y -> Cons (f (fst y), map f (snd y))
Note the calls to fst
and snd
- these are a consequence of storing head
and tail of a list inside a tuple (Cons
can be at most unary).
all data declarations should be placed before the program code
iTML does not support top-level bindings at the moment. In other words, once you define data types the remaining program is just a single expression.
parser currently binds operators tighter than function application. So for
example fst (raise "foo") + 2
is parsed as fst ((raise "foo") + 2)
rather than (fst (raise "foo")) + 2
. Use parentheses to disambiguate.
enclose code inside a trace
primitive to trace that code. Use bwdSlice
for backward slicing:
let t = trace ( (* YOUR CODE HERE *) ) in
bwdSlice (t, (* SLICING CRITERION HERE *) )
With all that in mind we recommend that you look at programs in examples/
directory.
Source code is divided into a library and an executable that depends on the
library. The library is located in lib
directory. Under
lib/Language/Slicer/
you will find these modules:
Absyn
: abstract syntax for TML language. This is what the parser
produces (Parser
module).
Core
: abstract syntax tree for the core language. Produced from TML
abstract syntax tree (Absyn
module) during desugaring (Desugar
module).
Contains also built-in operators and functions for working with the store
abstraction.
Desugar
- translates TML abstract syntax tree (Absyn
module) into core
language (Core
module).
Env
- definitions of variable and type environments + helper functions.
Error
- data type for handling compilation errors.
Eval
- evaluation of core programs
Monad
module and Monad/
sub-directory - monads for running various
stages of the interpreter pipeline.
Parser
- well, the parser.
Primitives
- built-in language primitives
Resugar
- translate core programs into surface-like syntax. Used for
pretty-printing.
Run
- entry points to the interpreter
Slice
- implementation of slicing
UpperSemiLattice
- lattice definition
Executable is located inside src
directory. src/Language/Slicer/
contains:
Main
- executable logic (parsing command line options, invoking the
library, etc.)
Monad/
- REPL monad
Repl
- REPL logic
This is experimental research software. It comes as-is without any guarantees.