Scilla - A Smart Contract Intermediate Level Language
Clone or download
jjcnn Cashflow analysis, first prototype (#317)
* Commit to initiate branch

* Added the main test contracts for cash tag inference.

* Initial traversal of MoneyFlowChecker

* tmp

* Fix compilation error

* Temporary commit

* Reintroducing Msg literal, which was accidentally removed

* Make Scilla compile again

* A few more cases in mf_tag_expr

* Tagging of expr completed (no testing performed)

* Fixes after merge

* First cashflow checker prototype

* Temporary change to scilla_checker for testing purposes

* Expression vars can be fields

* Added implicit contract and message fields to environments

* Only report changes if variable tags in the program have changed

* Removed Plain, and introduced explicit Bottom and NotMoney tags

* Support for Option and Bool types, and pattern-matching of same

* Builtins should return Bottom to allow information from other usages to survive. Also, minor bugfixes

* Support for builtins for maps

* Fixed builtin signatures and message components. Also fixed minor bugs

* Polymorphism ignored more intelligently

* Fixed error in AssocDictionary.remove

* Add support for pairs, plus minor code cleanup

* Copy of fc70957 - add flag for cashflow analysis

* Update README and changed MoneyFlow to Cashflow

* Changed MF (MoneyFlow) to CF (Cashflow)

* Rename Bottom and Top to something more sensible

* Change output label from tags to cashflow_tags

* Code cleanup

* Allow tests to run with custom arguments, and run checker tests with -cf option to tests cashflow analysis

* Simplify scilla_checker

* Simplify calculation of args_changes

* Simplify calculation of args_changes in Constr

* Removed unnecessary lub for builtin args

* Fixed erroneous fix
Latest commit 62dab15 Dec 10, 2018
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
docs moved readthedocs to a new repo Jun 20, 2018
imgs Added Scilla logos Jun 22, 2018
misc add infrastructure for raising warnings and printing them (#294) Oct 24, 2018
src Cashflow analysis, first prototype (#317) Dec 10, 2018
tests Cashflow analysis, first prototype (#317) Dec 10, 2018
.dockerignore support docker build Jun 29, 2018
.gitignore Updates to contracts to use in-place maps and events where applicable ( Nov 15, 2018
.ocp-indent Initial Project Structure Feb 13, 2018
.travis.yml fix Travis CI and opamdep Make target to use ocaml 4.06.1 (#263) Oct 9, 2018
Dockerfile gas accounting for params and fields in contract (#207) Sep 7, 2018
Dockerfile.slim add Dockerfile.slim to build slim version Dec 6, 2018
INSTALL.md add flycheck support for Emacs. (#288) Oct 15, 2018
LICENSE Update LICENSE Aug 1, 2018
Makefile Update Makefile Dec 6, 2018
README.md Cashflow analysis, first prototype (#317) Dec 10, 2018
dune-project Move to dune builds. Remove jbuilder (#162) Aug 3, 2018
easyrun.sh Support in-place map operations (#290) Oct 22, 2018
scilla-base.opam Move to dune builds. Remove jbuilder (#162) Aug 3, 2018
scilla-checker.opam Move to dune builds. Remove jbuilder (#162) Aug 3, 2018
scilla-checkers.opam 143 multistage level 2 (#194) Aug 29, 2018
scilla-cpp-deps.opam rename scilla-external-deps scilla-cpp-deps Aug 20, 2018
scilla-eval.opam Move to dune builds. Remove jbuilder (#162) Aug 3, 2018
scilla-runner.opam Move to dune builds. Remove jbuilder (#162) Aug 3, 2018
testsuite.opam Move to dune builds. Remove jbuilder (#162) Aug 3, 2018

README.md

Scilla: A Smart Contract Intermediate Level Language

Build Status License Gitter chat

Building and Running

Build requirements

Platform specific instructions for setting up your system for building Scilla can be found in INSTALL.md.

Compiling and Running

To build the project, run make clean; make from the root folder.

Once the project is built you can try the following things:

Evaluating a standalone closed expression:

From the project root, execute

./bin/eval-runner -libdir src/stdlib tests/eval/exp/good/let.scilla

Instead of let.scilla you might want to try any dfferent file in tests/eval/exp. The second argument, which is a path to the Scilla standard library can alternatively be specified in the environment variable SCILLA_STDLIB_PATH. This must be an absolute path (or a list of ; separated paths.

Type-checking a contract

From the project root, execute

./bin/scilla-checker -libdir src/stdlib tests/checker/good/auction.scilla

Instead of auction.scilla you might want to try any dfferent file in tests/checker with a complete implementation of a contract, or your own contract code. The second argument, which is a path to the Scilla standard library can alternatively be specified in the environment variable SCILLA_STDLIB_PATH. As above, this must be an absolute path(s).

If the checker only returns the contract structure in JSON format, it means that the contract has no type errors. Otherwise, a type error trace is provided.

The checker can be run with the following optional flags:

  • -cf to enable the cashflow checker and print its results.

Executing a simple transition

From the project root, execute

./bin/scilla-runner -init tests/contracts/crowdfunding/init.json -istate tests/contracts/crowdfunding/state_4.json -iblockchain tests/contracts/crowdfunding/blockchain_4.json -imessage tests/contracts/crowdfunding/message_4.json -o tests/contracts/crowdfunding/output_4.json -i tests/contracts/crowdfunding/contract -libdir src/stdlib

or

./bin/scilla-runner -init tests/contracts/zil-game/init.json -istate tests/contracts/zil-game/state_5.json -iblockchain tests/contracts/zil-game/blockchain_5.json -imessage tests/contracts/zil-game/message_5.json -o tests/contracts/zil-game/output_5.json -i tests/contracts/zil-game/contract -libdir src/stdlib

Alternatively, use the easyrun script as below:

./easyrun.sh crowdfunding 1

where n is a number 0-5 for the number of "steps" to execute the protocol (the messages and blockchain states are provided for only so many steps in the simulation).

Where to find binaries

  • The runnables are put into the folder
$PROJECT_DIR/_build/install/default/bin

Running the testsuite

The testsuite is based on the OUnit2 framework and is driven by the main module in tests/Testsuite.ml. Currently there are two types of tests run in the testsuite. contracts tests run a full transition on a contract with all input data provided. eval tests only test expression evaluation. To add more tests of either of these kinds, look for the corresponding .ml files in their tests/directory and add accordingly.

To run the testsuite:

make test

To run the testsuite executable manually from bin/testsuite, you have to provide the parameters "-bin-dir" and "-tests-dir", which must be absolute paths to the directory containing scilla-runner, eval-runner and the tests/directory containng the tests. Relative paths may not work.

To obtain a list of tests available:

./bin/testsuite -list-test

To run an individual test(s), for example all_tests:1:exptests:14:let.scilla (one of the tests from the list obtained via ./bin/testsuite -list-test):

./bin/testsuite -only-test all_tests:1:exptests:14:let.scilla -print-cli true 

The optional -print-cli true argument is to produce the command line that has been used to run the test.

Developer Tools

Emacs mode for Scilla

An emacs major mode for editing Scilla contracts is provided. Add the following line to your ~/.emacs file to load this mode for files ending with .scilla. For enabling flycheck mode for Scilla (see INSTALL.md).

;; For enabling flycheck mode for Scilla.
(setq scilla-root "/path/to/scilla/root")
;; Scilla mode
(load-file "/path/to/scilla.el")

Vim plugin for Scilla

A vim plugin for editing Scilla contracts is provided.

You can install the vim config files through Pathogen by:

git clone https://github.com/edisonljh/vim-scilla.git ~/.vim/bundle/vim-scilla

Or through Vundle by adding the following line to your ~/.vimrc:

Plugin 'edisonljh/vim-scilla'

Mirror Repo: vim-scilla.