diff --git a/.circleci/config.yml b/.circleci/config.yml
index e8502010ba5df5c82383ba7adb54da6f7add6449..cfddeb1489d438b113469803de6d898b7de272e9 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -20,16 +20,11 @@ jobs:
- run: mkdir -p ${TEST_RESULTS}
- run: go env
- run: git submodule update --init --recursive
- - run: git submodule status semantics/z3 | awk '{ print $1 }' > /tmp/z3.version
- restore_cache:
keys:
- v1-pkg-cache-{{ arch }}-{{ checksum "go.sum" }}
- - restore_cache:
- keys:
- - v1-z3-cache-{{ arch }}-{{ checksum "/tmp/z3.version" }}
-
- run: go mod tidy && test -z "$(git status --porcelain)"
- run: go mod download
- run: go mod verify
@@ -54,10 +49,6 @@ jobs:
key: v1-pkg-cache-{{ arch }}-{{ checksum "go.sum" }}
paths: "/go/pkg/mod"
- - save_cache:
- key: v1-z3-cache-{{ arch }}-{{ checksum "/tmp/z3.version" }}
- paths: "/go/src/github.com/ledgerwatch/turbo-geth/semantics/z3/build"
-
- store_artifacts:
path: /tmp/test-results
destination: raw-test-output
diff --git a/.gitmodules b/.gitmodules
index 5aab73fa80bd7fd12105aa52fcfc93e6eaccedb8..32bdb3b6e5a68a1a06d685b9fe830d242cae097d 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,6 +1,3 @@
[submodule "tests"]
path = tests/testdata
url = https://github.com/ethereum/tests
-[submodule "semantics/z3"]
- path = semantics/z3
- url = https://github.com/Z3Prover/z3
diff --git a/Makefile b/Makefile
index f65ed5660e4f5ae0d617e705ce463bb6b1e15c3a..3fcb2c37471f1af9f8749630acfb8d3e7821fead 100644
--- a/Makefile
+++ b/Makefile
@@ -81,16 +81,6 @@ rpcdaemon:
@echo "Done building."
@echo "Run \"$(GOBIN)/rpcdaemon\" to launch rpcdaemon."
-semantics: semantics/z3/build/libz3.a
- build/env.sh go run build/ci.go install ./cmd/semantics
- @echo "Done building."
- @echo "Run \"$(GOBIN)/semantics\" to launch semantics."
-
-semantics/z3/build/libz3.a:
- cd semantics/z3 && python scripts/mk_make.py --staticlib
- cd semantics/z3/build && ${MAKE} -j8
- cp semantics/z3/build/libz3.a .
-
integration:
$(GOBUILD) -o $(GOBIN)/integration ./cmd/integration
@echo "Done building."
@@ -118,18 +108,18 @@ ethdb/mdbx/dist/libmdbx.a:
echo "Building mdbx"
cd ethdb/mdbx/dist/ && make libmdbx.a && cat config.h
-test: semantics/z3/build/libz3.a ethdb/mdbx/dist/libmdbx.a
+test: ethdb/mdbx/dist/libmdbx.a
$(GOTEST)
-test-lmdb: semantics/z3/build/libz3.a
+test-lmdb:
TEST_DB=lmdb $(GOTEST)
-test-mdbx: semantics/z3/build/libz3.a ethdb/mdbx/dist/libmdbx.a
+test-mdbx: ethdb/mdbx/dist/libmdbx.a
TEST_DB=mdbx $(GOTEST_MDBX)
lint: lintci
-lintci: semantics/z3/build/libz3.a ethdb/mdbx/dist/libmdbx.a
+lintci: ethdb/mdbx/dist/libmdbx.a
@echo "--> Running linter for code diff versus commit $(LATEST_COMMIT)"
@./build/bin/golangci-lint run \
--new-from-rev=$(LATEST_COMMIT) \
diff --git a/cmd/semantics/main.go b/cmd/semantics/main.go
deleted file mode 100644
index c3ee937d99d02b5605a4144dbf74e0cd171fe1bd..0000000000000000000000000000000000000000
--- a/cmd/semantics/main.go
+++ /dev/null
@@ -1,9 +0,0 @@
-package main
-
-import (
- "fmt"
-)
-
-func main() {
- fmt.Printf("Hello, semantics!\n")
-}
diff --git a/semantics/libevmsem/src/sem.c b/semantics/libevmsem/src/sem.c
deleted file mode 100644
index 5d8c1c35486c9af24e0eb57964a26a6664e9cfb2..0000000000000000000000000000000000000000
--- a/semantics/libevmsem/src/sem.c
+++ /dev/null
@@ -1,146 +0,0 @@
-#include "sem.h"
-#include <stdlib.h>
-#include <string.h>
-#include <z3.h>
-
-Z3_context ctx;
-// Integer sort to act as account addresses, balances, nonces, indices in arrays, and storage keys and values
-Z3_sort int_sort;
-// Array sort that is used for contract storage, mapping keys (int) to values (int)
-Z3_sort contract_storage_sort;
-// Array sort that is used for contract code, mapping indices (program counter, int) to opcodes (int)
-Z3_sort contract_code_sort;
-// Account type constructor
-Z3_constructor account_constructor;
-// Account type
-Z3_sort account_sort;
-// Ethereum state type (array sort of accounts)
-Z3_sort state_sort;
-
-// Maximum number of terms in the sequence - constant for now to avoid dynamic memory allocation
-#define MAX_TERMS 1024*1024
-
-enum TermKind {
- None,
- StateHash,
- GasCounter,
- InputByte,
-};
-
-// Kind of a specific term
-typedef enum TermKind term_kind_type;
-
-// Kinds of terms in the sequence
-term_kind_type term_kinds[MAX_TERMS];
-
-// Type of state root
-typedef struct {
- int depth; // Depth of the key prefix
- char key_prefix[32]; // Key prefix
- char hash[32]; // Hash of the merkle subtree
-} state_hash_type;
-
-// Pointers to hash structures for StateHash terms
-state_hash_type* state_hashes[MAX_TERMS];
-
-// Gas counters
-__uint64_t gas_counters[MAX_TERMS];
-
-// Actual bytes for the InputByte terms
-char input_bytes[MAX_TERMS];
-
-// Create z3 context and necessary sorts and datatypes
-void init() {
- Z3_config cfg;
- cfg = Z3_mk_config();
- ctx = Z3_mk_context(cfg);
- Z3_del_config(cfg);
- int_sort = Z3_mk_int_sort(ctx);
- contract_storage_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
- contract_code_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
- Z3_symbol account_fields[5] = {
- Z3_mk_string_symbol(ctx, "balance"),
- Z3_mk_string_symbol(ctx, "nonce"),
- Z3_mk_string_symbol(ctx, "codelen"),
- Z3_mk_string_symbol(ctx, "code"),
- Z3_mk_string_symbol(ctx, "storage"),
- };
- Z3_sort account_field_sorts[5] = {
- int_sort, // balance
- int_sort, // nonce
- int_sort, // codelen
- contract_code_sort, // code
- contract_storage_sort, // storage
- };
- unsigned int account_sort_refs[5] = { 0, 0, 0, 0, 0 }; // There are no recursive datatypes, therefore all zeroes
- account_constructor = Z3_mk_constructor(ctx,
- Z3_mk_string_symbol(ctx, "account_const"), // name of the constructor
- Z3_mk_string_symbol(ctx, "is_account"), // name of the recognizer function
- 5, // number of fields
- account_fields, // field symbols
- account_field_sorts, // field sorts
- account_sort_refs // sort references
- );
- Z3_constructor account_constructors[1];
- account_constructors[0] = account_constructor;
- account_sort = Z3_mk_datatype(ctx, Z3_mk_string_symbol(ctx, "account"), 1, account_constructors);
- // state is the sort of accounts
- state_sort = Z3_mk_array_sort(ctx, int_sort, account_sort);
-}
-
-// Initialises the sequence with given state root and transaction data
-// Returns 0 if the initialisation is successful, otherwise error code
-int initialise(void* state_root, void *from_address, void *to_address, __uint128_t value, int tx_data_len, void* tx_data, __uint64_t gas_price, __uint64_t gas) {
- if (2 + tx_data_len > MAX_TERMS) {
- // First term is to state root
- // Second term is for gas counter
- return ERR_TX_DATA_TOO_LONG;
- }
-
- // Initialise state root
- term_kinds[0] = StateHash;
- state_hash_type* root = (state_hash_type*)(malloc(sizeof(state_hash_type)));
- root -> depth = 0; // depth 0 means root hash
- // key prefix can contain anything, it does not matter
- memcpy(root -> hash, state_root, 32); // copy state root so that input can be freed
- state_hashes[0] = root;
-
- // Initialise gas counter
- term_kinds[1] = GasCounter;
- gas_counters[1] = gas;
-
- // Initialise transaction input bytes
- const int tx_data_offset = 2;
- char* tx_bytes = (char*)tx_data;
- for(int i = tx_data_offset; i < tx_data_len+tx_data_offset; i++) {
- term_kinds[i] = InputByte;
- input_bytes[i] = tx_bytes[i-tx_data_offset];
- }
-
- // Fill the rest of sequence with empties
- for(int i = tx_data_len+tx_data_offset; i < MAX_TERMS; i++) {
- term_kinds[i] = None;
- }
- return 0;
-}
-
-// Free any memory allocated during initialisation and semantic execution
-void cleanup() {
- for(int i = 0; i < MAX_TERMS; i++) {
- switch (term_kinds[i]) {
- case None:
- break;
- case StateHash:
- free(state_hashes[i]);
- break;
- case GasCounter:
- break;
- case InputByte:
- break;
- }
- }
-}
-
-void destroy() {
- Z3_del_context(ctx);
-}
\ No newline at end of file
diff --git a/semantics/libevmsem/src/sem.h b/semantics/libevmsem/src/sem.h
deleted file mode 100644
index 6ace149e9605a0d22097cdd194fe58dd3368faa0..0000000000000000000000000000000000000000
--- a/semantics/libevmsem/src/sem.h
+++ /dev/null
@@ -1,29 +0,0 @@
-#ifndef _SEM_
-# define _SEM_
-
-# ifdef __cplusplus
-extern "C" {
-# endif
-
-#include <stddef.h>
-
-#define ERR_TX_DATA_TOO_LONG 1
-
-// Create z3 context and necessary sorts and datatypes
-void init();
-// Deletes z3 context and all sorts and datatypes
-void destroy();
-
-// Initialise sequence with given state root and transaction data,
-// all other terms being empty
-// Returns 0 if the initialisation is successful, otherwise error code (ERR_*)
-int initialise(void* state_root, void *from_address, void *to_address, __uint128_t value, int tx_data_len, void* tx_data, __uint64_t gas_price, __uint64_t gas);
-
-// Free any memory allocated during initialisation and semantic execution
-void clean();
-
-# ifdef __cplusplus
-}
-# endif
-
-#endif // _SEM_
\ No newline at end of file
diff --git a/semantics/sem.go b/semantics/sem.go
deleted file mode 100644
index 7ec8492b2e333500bd9d6ad097b78e27ac6d9896..0000000000000000000000000000000000000000
--- a/semantics/sem.go
+++ /dev/null
@@ -1,50 +0,0 @@
-package semantics
-
-/*
-#include <stdlib.h>
-#cgo CFLAGS: -I${SRCDIR}/libevmsem/src/
-#cgo CFLAGS: -I${SRCDIR}/libevmsem/
-#cgo CFLAGS: -I${SRCDIR}/z3/src/api
-#cgo LDFLAGS: ${SRCDIR}/z3/build/libz3.a -lstdc++ -lm
-#include "libevmsem/src/sem.h"
-#include "libevmsem/src/sem.c"
-#include "z3/src/api/z3.h"
-*/
-import "C"
-import (
- "unsafe"
-)
-
-// Initialise the term sequence for semantic execution
-func Initialise(stateRoot [32]byte, from [20]byte, to [20]byte, toPresent bool, value [16]byte, txData []byte, gasPrice uint64, gas uint64) int {
- stateRootPtr := C.CBytes(stateRoot[:])
- txDataPtr := C.CBytes(txData)
- fromPtr := C.CBytes(from[:])
- var toPtr unsafe.Pointer
- if toPresent {
- toPtr = C.CBytes(to[:])
- }
- result := int(C.initialise(stateRootPtr, fromPtr, toPtr, value, C.int(len(txData)), txDataPtr, C.__uint64_t(gasPrice), C.__uint64_t(gas)))
- if toPresent {
- C.free(toPtr)
- }
- C.free(fromPtr)
- C.free(txDataPtr)
- C.free(stateRootPtr)
- return result
-}
-
-// Cleanup release any dynamic memory allocated during the initialisation and semantic execution
-func Cleanup() {
- C.cleanup()
-}
-
-// Init creates z3 context, sorts and datatypes
-func Init() {
- C.init()
-}
-
-// Destroy deletes z3 contrxt, sorts and datatypes
-func Destroy() {
- C.destroy()
-}
\ No newline at end of file
diff --git a/semantics/sem_test.go b/semantics/sem_test.go
deleted file mode 100644
index c10ee11ebe32ddea99d7aad0b07bfca7d1a30963..0000000000000000000000000000000000000000
--- a/semantics/sem_test.go
+++ /dev/null
@@ -1,19 +0,0 @@
-package semantics
-
-import (
- "fmt"
- "testing"
-)
-
-func TestSemantics(t *testing.T) {
- var stateRoot [32]byte
- var fromAddr [20]byte
- var toAddr [20]byte
- var value [16]byte
- result := Initialise(stateRoot, fromAddr, toAddr, false, value, []byte{}, 1, 100)
- if result != 0 {
- t.Errorf("Could not initialise: %d", result)
- }
- fmt.Printf("Got it1!\n")
- Cleanup()
-}
diff --git a/semantics/z3 b/semantics/z3
deleted file mode 160000
index ab1f2f2e631538b6f2435485c10ef81e39c5545c..0000000000000000000000000000000000000000
--- a/semantics/z3
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit ab1f2f2e631538b6f2435485c10ef81e39c5545c