diff --git a/.gitmodules b/.gitmodules index 32bdb3b6e5a..5aab73fa80b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [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 6ee29449b9b..23c1b549879 100644 --- a/Makefile +++ b/Makefile @@ -67,6 +67,16 @@ 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 . + all: $(GORUN) build/ci.go install -procs=1 @@ -80,7 +90,7 @@ ios: @echo "Done building." @echo "Import \"$(GOBIN)/Geth.framework\" to use the library." -test: all +test: semantics/z3/build/libz3.a all $(GORUN) build/ci.go test lint: lintci diff --git a/cmd/semantics/main.go b/cmd/semantics/main.go new file mode 100644 index 00000000000..64bdd9840eb --- /dev/null +++ b/cmd/semantics/main.go @@ -0,0 +1,9 @@ +package main + +import ( + "fmt" +) + +func main() { + fmt.Printf("Hello, semantics!\n") +} \ No newline at end of file diff --git a/semantics/libevmsem/src/sem.c b/semantics/libevmsem/src/sem.c new file mode 100644 index 00000000000..d0058ad0fd3 --- /dev/null +++ b/semantics/libevmsem/src/sem.c @@ -0,0 +1,142 @@ +#include "sem.h" +#include +#include +#include + +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; + +// 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); +} + +// 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 new file mode 100644 index 00000000000..6ace149e960 --- /dev/null +++ b/semantics/libevmsem/src/sem.h @@ -0,0 +1,29 @@ +#ifndef _SEM_ +# define _SEM_ + +# ifdef __cplusplus +extern "C" { +# endif + +#include + +#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 new file mode 100644 index 00000000000..7ec8492b2e3 --- /dev/null +++ b/semantics/sem.go @@ -0,0 +1,50 @@ +package semantics + +/* +#include +#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 new file mode 100644 index 00000000000..c10ee11ebe3 --- /dev/null +++ b/semantics/sem_test.go @@ -0,0 +1,19 @@ +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 new file mode 160000 index 00000000000..ab1f2f2e631 --- /dev/null +++ b/semantics/z3 @@ -0,0 +1 @@ +Subproject commit ab1f2f2e631538b6f2435485c10ef81e39c5545c