Skip to content

Commit

Permalink
Remove ocaml backend (#627)
Browse files Browse the repository at this point in the history 
* Makefile: Remove OCaml

* kevm: Remove OCaml

* Jenkinsfile: Remove OCaml

* Dockerfile: Remove OCaml

* README.md: Remove OCaml

* Changes requested by review

* Dockerfile: Add ocaml pom.xml back in
  • Loading branch information
@gtrepta @rv-jenkins
gtrepta authored and rv-jenkins committed Dec 14, 2019
1 parent b1a2109 commit a694c56
Show file tree
Hide file tree
Showing 5 changed files with 34 additions and 167 deletions.
6 changes: 0 additions & 6 deletions Dockerfile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,6 @@ RUN apt-get update \
make \
maven \
netcat-openbsd \
opam \
openjdk-11-jdk \
pandoc \
pkg-config \
Expand Down Expand Up @@ -77,11 +76,6 @@ RUN npm install -g npx

USER user:user

ADD deps/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev deps/k/k-distribution/src/main/scripts/bin/k-configure-opam-common /home/user/.tmp-opam/bin/
ADD deps/k/k-distribution/src/main/scripts/lib/opam /home/user/.tmp-opam/lib/opam/
RUN cd /home/user \
&& ./.tmp-opam/bin/k-configure-opam-dev

ENV LC_ALL=C.UTF-8
ADD --chown=user:user deps/k/haskell-backend/src/main/native/haskell-backend/stack.yaml /home/user/.tmp-haskell/
ADD --chown=user:user deps/k/haskell-backend/src/main/native/haskell-backend/kore/package.yaml /home/user/.tmp-haskell/kore/
Expand Down
19 changes: 2 additions & 17 deletions Jenkinsfile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,28 +38,21 @@ pipeline {
stage('Dependencies') {
steps {
sh '''
make deps ocaml-deps split-tests -j3
make deps split-tests -j3
'''
}
}
stage('Build') {
steps {
sh '''
make build-all -j4
make build -j4
'''
}
}
stage('Test Execution') {
failFast true
options { timeout(time: 20, unit: 'MINUTES') }
parallel {
stage('Conformance (OCaml)') {
steps {
sh '''
make test-conformance -j8 TEST_CONCRETE_BACKEND=ocaml
'''
}
}
stage('Conformance (LLVM)') {
steps {
sh '''
Expand Down Expand Up @@ -102,13 +95,6 @@ pipeline {
failFast true
options { timeout(time: 35, unit: 'MINUTES') }
parallel {
stage('OCaml krun') {
steps {
sh '''
make test-interactive-run TEST_CONCRETE_BACKEND=ocaml
'''
}
}
stage('LLVM krun') {
steps {
sh '''
Expand Down Expand Up @@ -140,7 +126,6 @@ pipeline {
stage('Failing tests') {
steps {
sh '''
make test-failure TEST_CONCRETE_BACKEND=ocaml
make test-failure TEST_CONCRETE_BACKEND=llvm
'''
}
Expand Down
74 changes: 4 additions & 70 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,10 @@ LUA_PATH := $(PANDOC_TANGLE_SUBMODULE)/?.lua;;
export TANGLER
export LUA_PATH

OPAM ?= opam

.PHONY: all clean clean-submodules distclean install uninstall \
deps all-deps llvm-deps haskell-deps repo-deps k-deps ocaml-deps plugin-deps libsecp256k1 libff proxygen \
build build-all build-ocaml build-java build-node build-haskell build-llvm build-web3 \
defn java-defn ocaml-defn node-defn web3-defn haskell-defn llvm-defn \
deps all-deps llvm-deps haskell-deps repo-deps k-deps plugin-deps libsecp256k1 libff proxygen \
build build-java build-node build-haskell build-llvm build-web3 \
defn java-defn node-defn web3-defn haskell-defn llvm-defn \
split-tests \
test test-all test-conformance test-rest-conformance test-all-conformance test-slow-conformance test-failing-conformance \
test-vm test-rest-vm test-all-vm test-bchain test-rest-bchain test-all-bchain \
Expand Down Expand Up @@ -148,10 +146,6 @@ $(PLUGIN_SUBMODULE)/make.timestamp:
git submodule update --init --recursive -- $(PLUGIN_SUBMODULE)
touch $(PLUGIN_SUBMODULE)/make.timestamp

ocaml-deps:
eval $$($(OPAM) config env) \
$(OPAM) install --yes mlgmp zarith uuidm cryptokit secp256k1.0.3.2 bn128 ocaml-protoc rlp yojson hex ocp-ocamlres

# Building
# --------

Expand All @@ -163,22 +157,19 @@ k_files := driver.k data.k network.k evm.k krypto.k edsl.k evm-node.k web3
EXTRA_K_FILES += $(MAIN_DEFN_FILE).k
ALL_K_FILES := $(k_files) $(EXTRA_K_FILES)

ocaml_dir := $(DEFN_DIR)/ocaml
llvm_dir := $(DEFN_DIR)/llvm
java_dir := $(DEFN_DIR)/java
haskell_dir := $(DEFN_DIR)/haskell
export node_dir := $(CURDIR)/$(DEFN_DIR)/node
export web3_dir := $(CURDIR)/$(DEFN_DIR)/web3

ocaml_files := $(patsubst %, $(ocaml_dir)/%, $(ALL_K_FILES))
llvm_files := $(patsubst %, $(llvm_dir)/%, $(ALL_K_FILES))
java_files := $(patsubst %, $(java_dir)/%, $(ALL_K_FILES))
haskell_files := $(patsubst %, $(haskell_dir)/%, $(ALL_K_FILES))
node_files := $(patsubst %, $(node_dir)/%, $(ALL_K_FILES))
web3_files := $(patsubst %, $(web3_dir)/%, $(ALL_K_FILES))
defn_files := $(ocaml_files) $(llvm_files) $(java_files) $(haskell_files) $(node_files) $(web3_files)
defn_files := $(llvm_files) $(java_files) $(haskell_files) $(node_files) $(web3_files)

ocaml_kompiled := $(ocaml_dir)/$(MAIN_DEFN_FILE)-kompiled/interpreter
java_kompiled := $(java_dir)/$(MAIN_DEFN_FILE)-kompiled/timestamp
node_kompiled := $(DEFN_DIR)/vm/kevm-vm
web3_kompiled := $(web3_dir)/build/kevm-client
Expand All @@ -193,17 +184,12 @@ haskell_tangle := .k:not(.node):not(.concrete):not(.nobytes),.standalone,.symbo
node_tangle := .k:not(.standalone):not(.symbolic):not(.nobytes),.node,.concrete,.bytes

defn: $(defn_files)
ocaml-defn: $(ocaml_files)
llvm-defn: $(llvm_files)
java-defn: $(java_files)
haskell-defn: $(haskell_files)
node-defn: $(node_files)
web3-defn: $(web3_files)

$(ocaml_dir)/%.k: %.md $(TANGLER)
@mkdir -p $(ocaml_dir)
pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(concrete_tangle)" $< > $@

$(llvm_dir)/%.k: %.md $(TANGLER)
@mkdir -p $(llvm_dir)
pandoc --from markdown --to "$(TANGLER)" --metadata=code:"$(concrete_tangle)" $< > $@
Expand All @@ -230,8 +216,6 @@ KOMPILE_OPTS :=
LLVM_KOMPILE_OPTS :=

build: build-llvm build-haskell build-java build-web3 build-node
build-all: build build-ocaml
build-ocaml: $(ocaml_kompiled)
build-java: $(java_kompiled)
build-node: $(node_kompiled)
build-web3: $(web3_kompiled)
Expand All @@ -254,56 +238,6 @@ $(haskell_kompiled): $(haskell_files)
--directory $(haskell_dir) -I $(haskell_dir) \
$(KOMPILE_OPTS)

# OCAML Backend

ifeq ($(BYTE),yes)
EXT=cmo
LIBEXT=cma
DLLEXT=cma
OCAMLC=c
LIBFLAG=-a
else
EXT=cmx
LIBEXT=cmxa
DLLEXT=cmxs
OCAMLC=opt -O3
LIBFLAG=-shared
endif

$(ocaml_dir)/$(MAIN_DEFN_FILE)-kompiled/constants.$(EXT): $(ocaml_files)
eval $$($(OPAM) config env) \
&& $(K_BIN)/kompile --debug --main-module $(MAIN_MODULE) --backend ocaml \
--syntax-module $(SYNTAX_MODULE) $(ocaml_dir)/$(MAIN_DEFN_FILE).k \
--hook-namespaces "KRYPTO" --gen-ml-only -O3 --non-strict \
--directory $(ocaml_dir) -I $(ocaml_dir) $(KOMPILE_OPTS) \
&& cd $(ocaml_dir)/$(MAIN_DEFN_FILE)-kompiled \
&& ocamlfind $(OCAMLC) -c -g constants.ml -package gmp -package zarith -safe-string

$(ocaml_dir)/$(MAIN_DEFN_FILE)-kompiled/plugin/semantics.$(LIBEXT): $(wildcard $(PLUGIN_SUBMODULE)/plugin/*.ml $(PLUGIN_SUBMODULE)/plugin/*.mli) $(ocaml_dir)/$(MAIN_DEFN_FILE)-kompiled/constants.$(EXT)
@mkdir -p $(dir $@)
cp $(PLUGIN_SUBMODULE)/plugin/*.ml $(PLUGIN_SUBMODULE)/plugin/*.mli $(dir $@)
eval $$($(OPAM) config env) \
&& ocp-ocamlres -format ocaml $(PLUGIN_SUBMODULE)/plugin/proto/VERSION -o $(dir $@)/apiVersion.ml \
&& ocaml-protoc $(PLUGIN_SUBMODULE)/plugin/proto/*.proto -ml_out $(dir $@) \
&& cd $(dir $@) \
&& ocamlfind $(OCAMLC) -c -g -I $(CURDIR)/$(ocaml_dir)/$(MAIN_DEFN_FILE)-kompiled \
KRYPTO.ml \
-package cryptokit -package hex -package secp256k1 -package bn128 -package ocaml-protoc -safe-string -thread \
&& ocamlfind $(OCAMLC) -a -o semantics.$(LIBEXT) KRYPTO.$(EXT) -thread \
&& ocamlfind remove ethereum-semantics-plugin-ocaml \
&& ocamlfind install ethereum-semantics-plugin-ocaml $(PLUGIN_SUBMODULE)/plugin/META semantics.* *.cmi *.$(EXT)

$(ocaml_kompiled): $(ocaml_dir)/$(MAIN_DEFN_FILE)-kompiled/plugin/semantics.$(LIBEXT)
eval $$($(OPAM) config env) \
&& cd $(ocaml_dir)/$(MAIN_DEFN_FILE)-kompiled \
&& ocamllex lexer.mll \
&& ocamlyacc parser.mly \
&& ocamlfind $(OCAMLC) -c -g -package gmp -package zarith -package uuidm -safe-string prelude.ml plugin.ml parser.mli parser.ml lexer.ml hooks.ml run.ml -thread \
&& ocamlfind $(OCAMLC) -c -g -w -11-26 -package gmp -package zarith -package uuidm -package ethereum-semantics-plugin-ocaml -safe-string realdef.ml -match-context-rows 2 \
&& ocamlfind $(OCAMLC) $(LIBFLAG) -o realdef.$(DLLEXT) realdef.$(EXT) \
&& ocamlfind $(OCAMLC) -g -o interpreter constants.$(EXT) prelude.$(EXT) plugin.$(EXT) parser.$(EXT) lexer.$(EXT) hooks.$(EXT) run.$(EXT) interpreter.ml \
-package gmp -package hex -package dynlink -package zarith -package str -package uuidm -package unix -package ethereum-semantics-plugin-ocaml -linkpkg -linkall -thread -safe-string

# Node Backend

$(node_kompiled): MAIN_DEFN_FILE=evm-node
Expand Down
34 changes: 5 additions & 29 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ Installing/Building

### K Backends

There are four backends of K available: LLVM (default) and OCaml for concrete execution and Java (default) and Haskell for symbolic execution.
There are three backends of K available: LLVM (default) for concrete execution and Java (default) and Haskell for symbolic execution.
This repository generates the build-products for each backend in `.build/defn/`.

### System Dependencies
Expand All @@ -48,8 +48,6 @@ The following are needed for building/running KEVM:
- GNU [Bison](https://www.gnu.org/software/bison/), [Flex](https://github.com/westes/flex), and [Autoconf](http://www.gnu.org/software/autoconf/).
- GNU [libmpfr](http://www.mpfr.org/) and [libtool](https://www.gnu.org/software/libtool/).
- Java 8 JDK (eg. [OpenJDK](http://openjdk.java.net/))
- [Opam](https://opam.ocaml.org/doc/Install.html), **important**: Ubuntu users prior to 15.04 **must** build from source, as the Ubuntu install for 14.10 and prior is broken.
`opam repository` also requires `rsync`.

On Ubuntu >= 18.04 (for example):

Expand All @@ -59,8 +57,8 @@ sudo apt install \
libboost-test-dev libgmp-dev libjemalloc-dev libmpfr-dev \
libprocps-dev libprotobuf-dev libsecp256k1-dev libtool \
libyaml-dev libz3-dev lld-8 llvm-8 llvm-8-tools make maven \
opam openjdk-11-jdk pandoc pkg-config protobuf-compiler \
z3 zlib1g-dev
openjdk-11-jdk pandoc pkg-config protobuf-compiler z3 \
zlib1g-dev
```

On Ubuntu < 18.04, you'll need to skip `libsecp256k1-dev` and instead build it from source (via our `Makefile`):
Expand All @@ -75,7 +73,7 @@ On ArchLinux:
sudo pacman -S \
base base-devel boost clang cmake crypto++ curl git gmp \
gperf gflags jdk-openjdk jemalloc libsecp256k1 libsodium \
lld llvm maven mpfr opam python stack yaml-cpp z3 zlib
lld llvm maven mpfr python stack yaml-cpp z3 zlib
```

In addition, you'll need the `glog-git` AUR package: <https://aur.archlinux.org/packages/glog-git/>.
Expand All @@ -85,7 +83,7 @@ On OSX, using [Homebrew](https://brew.sh/), after installing the command line to
```sh
brew tap caskroom/cask
brew cask install adoptopenjdk12
brew install automake libtool gmp mpfr pkg-config pandoc maven opam z3 libffi
brew install automake libtool gmp mpfr pkg-config pandoc maven z3 libffi
make libsecp256k1
```

Expand Down Expand Up @@ -140,28 +138,6 @@ make build-llvm RELEASE=1
make build-java
```

#### OPTIONAL: OCaml Backend

If you wish to build the OCaml backend, you will need to take some additional steps.

First, make sure you have our custom OCaml compiler installed (should only need to do this once):

```sh
./deps/k/k-distribution/src/main/scripts/bin/k-configure-opam-dev
```

Next you need to install the specific OCaml packages we requires:

```sh
make ocaml-deps
```

And next you can build the OCaml backend:

```sh
make build-ocaml
```

### Installing

To install the `kevm-vm` binary for use in Firefly and other full-nodes, do:
Expand Down
68 changes: 23 additions & 45 deletions kevm
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,14 +37,10 @@ pretty_diff() {

run_krun() {
export K_OPTS=-Xss500m
case "$backend" in
ocaml) args=(--interpret) ;;
*) args=() ;;
esac
krun --directory "$backend_dir" \
-cSCHEDULE="$cSCHEDULE" -pSCHEDULE='printf %s' \
-cMODE="$cMODE" -pMODE='printf %s' \
"$run_file" "${args[@]-}" "$@"
"$run_file" "$@"
}

run_kast() {
Expand Down Expand Up @@ -178,23 +174,6 @@ run_interpret() {
debugger=
output_format='kore'
case "$backend" in
ocaml) run_kast kast > "$kast"
output_format='kast'
if $debug; then debugger=ocamldebug; fi
$debugger "$interpreter" "$backend_dir/driver-kompiled/realdef.cma" \
-c PGM "$kast" textfile \
-c SCHEDULE "$cSCHEDULE" text \
-c MODE "$cMODE" text \
--initializer 'initKevmCell' \
--output-file "$output" "$@" \
|| exit_status="$?"
if [[ "$unparse" == 'true' ]] && [[ "$exit_status" != '0' ]]; then
k-bin-to-text "$output" "$output_text"
cat "$output_text"
fi
exit "$exit_status"
;;

java) run_kast kast > "$kast"
output_format='kast'
run_file="$kast"
Expand Down Expand Up @@ -236,18 +215,18 @@ run_command="$1" ; shift

if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
echo "
usage: $0 run [--backend (ocaml|java|llvm|haskell)] <pgm> <K arg>*
$0 interpret [--backend (ocaml|llvm)] [--debug|--no-unparse] <pgm> <interpreter arg>*
$0 interpret [--backend (haskell|java)] [--no-unparse] <pgm>
$0 kast [--backend (ocaml|java|llvm|haskell|web3)] <pgm> <output format> <K arg>*
$0 prove [--backend (java|haskell)] <spec> <K arg>* -m <def_module>
$0 search [--backend (java|haskell)] <pgm> <pattern> <K arg>*
$0 web3 [--debug|--dump] <port>
$0 web3-ganache [--debug|--dump] <port>
$0 web3-send <port> [<web3_method> <web3_params>|<web3_file>]
$0 klab-run <pgm> <K arg>*
$0 klab-prove <spec> <K arg>* -m <def_module>
$0 klab-view <spec>
usage: $0 run [--backend (llvm|java|haskell)] <pgm> <K arg>*
$0 interpret [--backend (llvm)] [--debug|--no-unparse] <pgm> <interpreter arg>*
$0 interpret [--backend (java|haskell)] [--no-unparse] <pgm>
$0 kast [--backend (llvm|java|haskell|web3)] <pgm> <output format> <K arg>*
$0 prove [--backend (java|haskell)] <spec> <K arg>* -m <def_module>
$0 search [--backend (java|haskell)] <pgm> <pattern> <K arg>*
$0 web3 [--debug|--dump] <port>
$0 web3-ganache [--debug|--dump] <port>
$0 web3-send <port> [<web3_method> <web3_params>|<web3_file>]
$0 klab-run <pgm> <K arg>*
$0 klab-prove <spec> <K arg>* -m <def_module>
$0 klab-view <spec>
$0 [help|--help|version|--version]
Expand Down Expand Up @@ -312,7 +291,6 @@ while [[ $# -gt 0 ]]; do
esac
done
backend_dir="$defn_dir/$backend"
[[ ! "$backend" == "ocaml" ]] || eval $(${OPAM:-opam} config env)

# get the run file
if [[ ! "$run_command" =~ web3* ]]; then
Expand All @@ -333,15 +311,15 @@ cCHAINID="#token(\"${CHAINID:-28346}\",\"Int\")"
case "$run_command-$backend" in

# Running
run-@(ocaml|java|llvm|haskell) ) run_krun "$@" ;;
kast-@(ocaml|java|llvm|haskell|web3) ) run_kast "$@" ;;
interpret-@(ocaml|llvm|haskell|java) ) run_interpret "$@" ;;
prove-@(java|haskell) ) run_prove "$@" ;;
search-@(java|haskell) ) run_search "$@" ;;
web3-@(llvm) ) run_web3 "$@" ;;
web3-send-@(llvm) ) run_web3_send "$@" ;;
web3-ganache-@(llvm) ) run_web3_ganache "$@" ;;
klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;;
klab-view-java ) view_klab "$@" ;;
run-@(java|llvm|haskell) ) run_krun "$@" ;;
kast-@(java|llvm|haskell|web3) ) run_kast "$@" ;;
interpret-@(llvm|haskell|java) ) run_interpret "$@" ;;
prove-@(java|haskell) ) run_prove "$@" ;;
search-@(java|haskell) ) run_search "$@" ;;
web3-@(llvm) ) run_web3 "$@" ;;
web3-send-@(llvm) ) run_web3_send "$@" ;;
web3-ganache-@(llvm) ) run_web3_ganache "$@" ;;
klab-@(run|prove)-java ) run_klab "${run_command#klab-}" "$@" ;;
klab-view-java ) view_klab "$@" ;;
*) $0 help ; fatal "Unknown command on backend: $run_command $backend" ;;
esac

0 comments on commit a694c56

Please sign in to comment.