KSolidity: Semantics of Solidity in K
This repository presents a prototype formal semantics of Solidity.
This repository generates the build-products for the Java and OCaml backends for K in
The following are needed for building/running KSolidity:
- Pandoc >= 1.17 is used to generate the
*.kfiles from the
- GNU Bison, Flex, and Autoconf.
- GNU libmpfr and libtool.
- Java 8 JDK (eg. OpenJDK)
- Opam, important: Ubuntu users prior to 15.04 must build from source, as the Ubuntu install for 14.10 and prior is broken.
opam repositoryalso requires
On Ubuntu >= 15.04 (for example):
sudo apt install \ autoconf curl flex gcc libffi-dev libmpfr-dev libtool make maven \ opam openjdk-8-jdk pandoc pkg-config python3 python-pygments \ python-recommonmark python-sphinx time zlib1g-dev
After installing the above dependencies, make sure the submodules are setup:
git submodule update --init --recursive
If you haven't already setup K's OCaml dependencies more recently than February 1, 2019, then you also need to setup the K OCaml dependencies:
NOTE: It may prove useful to first do
rm -rf ~/.opam if you've setup K projcets in the past and are experiencing trouble with the newest opam libraries.
This is a fairly destructive operation, and will break any other projects that depend on specific locally installed ocaml packages.
Finally, you can install repository specific dependencies and build the semantics:
make deps make build
To only build specific backends, you can do
make build-ocaml, or
The following files constitute the KSolidity semantics:
- configuration.k is the KSolidity configuration, or state defintion.
- contract.k defines the semantics of defining and loading contracts into the state.
- driver.k loads and runs tests from the test-set.
- expression.k defines the semantics of Solidity expressions.
- function.k defines the semantics of loading functions inside a contract.
- solidity.k is the top-level semantics file which includes all the other files.
- solidity-syntax.k defines the syntax of the Solidity language.
- statement.k the syntax of Solidity statements inside functions.
./ksol runner script
After building the definition, you can run the definition using
The most up-to-date documentation will always be in
Run the file
./ksol run tests/functionCall_2.sol
Run the same file as a test:
./ksol test tests/functionCall_2.sol
You can optionally override the default backend using the
--backend BACKEND flag:
./ksol run --backend ocaml tests/functionCall_2.sol
test contains all the currently passing tests.