From e150736848041304f074e653a54adb76d1bd4799 Mon Sep 17 00:00:00 2001
From: gtrepta <50716988+gtrepta@users.noreply.github.com>
Date: Wed, 6 Jan 2021 11:50:09 -0600
Subject: [PATCH] General Performance Improvements (#231)
* iele-testing: Don't run #parseByteStack on both terms in ==K
* iele-testing: Skip calling #dasmContract, just compare the bytecode
* data.md: Use KEVM's parseByteStack
* data.md: Build the WordStack 4 elements at a time with #parseByteStack
* data.md: unparseByteStack 4 at a time
* iele-testing: Split checks into stages to skip isSorted
* data.md: #take 4 at a time
* data.md: Use #parseHexBytesAux in #parseByteStackRaw
* data.md: Remove unused #rev
* tests/{slow,failing}.haskell,Makefile: Add failing and slow test lists to haskell and targets to run them
* Revert "data.md: Remove unused #rev"
This reverts commit 5104a461c0cb615e266426d3744d52b0f0441987.
* Revert "data.md: #take 4 at a time"
This reverts commit 0a071f1bfcf431ce9a01fb93dc9e38902288c69d.
* Jenkinsfile: Add IELE tests stage on haskell backend
* Jenkinsfile: Try sleeping while .test-assembled files get generated by another stage in parallel
* Jenkinsfile: Raise timeout to 30 minutes
* Jenkinsfile: Assemble iele tests in separate stage
---
Jenkinsfile | 17 +++++-----
Makefile | 13 ++++++--
data.md | 34 ++++++++++++++------
iele-testing.md | 19 +++++------
tests/failing.haskell | 1 +
tests/slow.haskell | 73 +++++++++++++++++++++++++++++++++++++++++++
6 files changed, 127 insertions(+), 30 deletions(-)
create mode 100644 tests/slow.haskell
diff --git a/Jenkinsfile b/Jenkinsfile
index 8a8eec2d6..dc1fec9b2 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -22,16 +22,17 @@ pipeline {
}
}
stages {
- stage('Build') { steps { sh 'make build -j4' } }
- stage('Split Tests') { steps { sh 'make split-tests -j4' } }
+ stage('Build') { steps { sh 'make build -j4' } }
+ stage('Split Tests') { steps { sh 'make split-tests -j4' } }
+ stage('Assemble Iele Tests') { steps { sh 'make assemble-iele-test -j4' } }
stage('Test') {
- options { timeout(time: 5, unit: 'MINUTES') }
+ options { timeout(time: 30, unit: 'MINUTES') }
parallel {
- stage('EVM Tests') { steps { sh 'make test-vm -j4' } }
- stage('IELE Tests') { steps { sh 'make test-iele -j4' } }
- stage('VM Tests (Haskell)') { steps { sh 'make test-vm -j4 TEST_BACKEND=haskell' } }
- stage('Well Formed Check') { steps { sh 'make test-wellformed -j4' } }
- stage('Interactive') { steps { sh 'make test-interactive' } }
+ stage('EVM Tests') { steps { sh 'make test-vm -j4' } }
+ stage('IELE Tests') { steps { sh 'make test-iele -j4' } }
+ stage('IELE Tests (Haskell)') { steps { sh 'make test-iele -j4 TEST_BACKEND=haskell' } }
+ stage('Well Formed Check') { steps { sh 'make test-wellformed -j4' } }
+ stage('Interactive') { steps { sh 'make test-interactive' } }
stage('Node') {
steps {
sh '''
diff --git a/Makefile b/Makefile
index 75d1121ce..bc666e92f 100644
--- a/Makefile
+++ b/Makefile
@@ -46,7 +46,8 @@ export PATH:=$(IELE_BIN):$(PATH)
build build-interpreter build-vm build-haskell build-node build-testnode \
install install-interpreter install-vm uninstall \
split-tests split-vm-tests split-blockchain-tests \
- test-evm test-vm test-blockchain test-iele test-iele-node test-wellformed test-bad-packet test-interactive
+ test-evm test-vm test-blockchain test-wellformed test-bad-packet test-interactive \
+ test-iele test-iele-failing test-iele-slow test-iele-node assemble-iele-test
.SECONDARY:
all: build split-tests
@@ -101,6 +102,7 @@ vm_tests=$(wildcard tests/VMTests/*/*/*.iele.json)
blockchain_tests=$(wildcard tests/BlockchainTests/*/*/*/*.iele.json)
all_tests=$(vm_tests) $(blockchain_tests)
failing_tests = $(shell cat tests/failing.$(TEST_BACKEND))
+slow_tests = $(shell cat tests/slow.$(TEST_BACKEND))
skipped_tests=$(failing_tests) \
$(wildcard tests/VMTests/vmPerformance/*/*.json) \
$(wildcard tests/BlockchainTests/GeneralStateTests/*/*/*_Frontier.iele.json) \
@@ -122,7 +124,11 @@ passing_vm_targets=$(passing_vm_tests:=.test)
passing_blockchain_targets=$(passing_blockchain_tests:=.test)
iele_tests=$(wildcard tests/iele/*/*/*.iele.json)
-iele_passing_tests=$(filter-out $(failing_tests), $(iele_tests))
+iele_assembled=$(iele_tests:=.test-assembled)
+iele_quick_tests=$(filter-out $(slow_tests), $(iele_tests))
+iele_passing_tests=$(filter-out $(failing_tests), $(iele_quick_tests))
+iele_slow=$(slow_tests:=.test)
+iele_failing=$(failing_tests:=.test)
iele_targets=$(iele_passing_tests:=.test)
iele_node_targets=$(iele_tests:=.nodetest)
@@ -134,7 +140,10 @@ test-evm: test-vm test-blockchain
test-vm: $(passing_vm_targets)
test-blockchain: $(passing_blockchain_targets)
test-iele: $(iele_targets)
+test-iele-slow: $(iele_slow)
+test-iele-failing: $(iele_failing)
test-iele-node: $(iele_node_targets)
+assemble-iele-test: $(iele_assembled)
test-wellformed: $(well_formedness_targets)
test-bad-packet:
diff --git a/data.md b/data.md
index 38e687730..adbd5be66 100644
--- a/data.md
+++ b/data.md
@@ -431,17 +431,32 @@ These parsers can interperet hex-encoded strings as `Int`s, `WordStack`s, and `M
rule #parseWord(S) => #parseHexWord(S) requires lengthString(S) >=Int 2 andBool substrString(S, 0, 2) ==String "0x"
rule #parseWord(S) => String2Int(S) [owise]
+ syntax String ::= #alignHexString ( String ) [function, functional]
+ // -------------------------------------------------------------------
+ rule #alignHexString(S) => S requires lengthString(S) modInt 2 ==Int 0
+ rule #alignHexString(S) => "0" +String S requires notBool lengthString(S) modInt 2 ==Int 0
+
syntax WordStack ::= #parseByteStack ( String ) [function]
- | #parseByteStack ( String , WordStack , Int , Int ) [function, klabel(#parseByteStackAux)]
+ | #parseHexBytes ( String ) [function]
+ | #parseHexBytesAux ( String ) [function]
+ | #parseHexBytesAux ( Bytes ) [function]
| #parseByteStackRaw ( String ) [function]
| #parseByteStackRaw ( String , WordStack , Int , Int ) [function, klabel(#parseByteStackRawAux)]
// --------------------------------------------------------------------------------------------------------------------
- rule #parseByteStack(S) => #fun(STR => #parseByteStack(STR, .WordStack, 0, lengthString(STR)))(replaceAll(S, "0x", ""))
- rule #parseByteStack(_, WS, LEN, LEN) => #rev(WS, .WordStack)
- rule #parseByteStack(S, WS, I, LEN) => #parseByteStack(S, #parseHexWord(substrString(S, I, I +Int 2)) : WS, I +Int 2, LEN) [owise]
- rule #parseByteStackRaw(S) => #parseByteStackRaw(S, .WordStack, 0, lengthString(S))
- rule #parseByteStackRaw(S, WS, LEN, LEN) => #rev(WS, .WordStack)
- rule #parseByteStackRaw(S, WS, I, LEN) => #parseByteStackRaw(S, ordChar(substrString(S, I, I +Int 1)) : WS, I +Int 1, LEN) [owise]
+ rule #parseByteStack(S) => #parseHexBytes(replaceAll(S, "0x", ""))
+
+ rule #parseHexBytes(S) => #parseHexBytesAux(#alignHexString(S))
+ rule #parseHexBytesAux("") => .WordStack
+ rule #parseHexBytesAux(S) => #parseHexBytesAux( Int2Bytes(lengthString(S) /Int 2, String2Base(S, 16), BE) )
+ requires lengthString(S) >=Int 2
+
+ rule #parseHexBytesAux(BS) => BS[0] : BS[1] : BS[2] : BS[3] : #parseHexBytesAux( substrBytes(BS, 4, lengthBytes(BS)) ) requires lengthBytes(BS) >=Int 4
+ rule #parseHexBytesAux(BS) => BS[0] : BS[1] : BS[2] : .WordStack requires lengthBytes(BS) ==Int 3
+ rule #parseHexBytesAux(BS) => BS[0] : BS[1] : .WordStack requires lengthBytes(BS) ==Int 2
+ rule #parseHexBytesAux(BS) => BS[0] : .WordStack requires lengthBytes(BS) ==Int 1
+ rule #parseHexBytesAux(BS) => .WordStack requires lengthBytes(BS) ==Int 0
+
+ rule #parseByteStackRaw(S) => #parseHexBytesAux(String2Bytes(S))
syntax Map ::= #parseMap ( JSON ) [function]
// --------------------------------------------
@@ -467,8 +482,9 @@ We need to interperet a `WordStack` as a `String` again so that we can call `Kec
// ---------------------------------------------------------------------------------------------------------
rule #unparseByteStack ( WS ) => #unparseByteStack(WS, .StringBuffer)
- rule #unparseByteStack( .WordStack, BUFFER ) => StringBuffer2String(BUFFER)
- rule #unparseByteStack( W : WS, BUFFER ) => #unparseByteStack(WS, BUFFER +String chrChar(W))
+ rule #unparseByteStack( W1 : W2 : W3 : W4 : WS, BUFFER ) => #unparseByteStack(WS, BUFFER +String (chrChar(W1) +String chrChar(W2) +String chrChar(W3) +String chrChar(W4)))
+ rule #unparseByteStack( W1 : WS, BUFFER ) => #unparseByteStack(WS, BUFFER +String chrChar(W1)) [owise]
+ rule #unparseByteStack( .WordStack, BUFFER ) => StringBuffer2String(BUFFER)
```
Recursive Length Prefix (RLP)
diff --git a/iele-testing.md b/iele-testing.md
index 67b72d8a5..fef5adf99 100644
--- a/iele-testing.md
+++ b/iele-testing.md
@@ -348,7 +348,7 @@ State Manipulation
// ----------------------------------
rule load DATA : { .JSONs } => .
rule load DATA : { KEY : VALUE:JSON , REST } => load DATA : { KEY : VALUE } ~> load DATA : { REST }
- requires REST =/=K .JSONs andBool DATA =/=String "transactions"
+ requires REST =/=K .JSONs andBool notBool DATA in (SetItem("transactions") SetItem("transactionsSorted"))
rule load DATA : [ .JSONs ] => .
rule load DATA : [ { TEST } , REST ] => load DATA : { TEST } ~> load DATA : [ REST ]
@@ -493,10 +493,9 @@ The `"blockHeader"` key loads the block information.
The `"transactions"` key loads the transactions.
```{.k .standalone}
- rule load "transactions" : { TX } => load "transactions" : { #sortJSONList(TX) }
- requires notBool #isSorted(TX)
+ rule load "transactions" : { TX } => load "transactionsSorted" : { #sortJSONList(TX) }
- rule load "transactions" : { "arguments" : [ ARGS ], "contractCode" : TI , "from" : FROM, "function" : FUNC, "gasLimit" : TG , "gasPrice" : TP , "nonce" : TN , "to" : TT , "value" : TV , .JSONs } => . ...
+ rule load "transactionsSorted" : { "arguments" : [ ARGS ], "contractCode" : TI , "from" : FROM, "function" : FUNC, "gasLimit" : TG , "gasPrice" : TP , "nonce" : TN , "to" : TT , "value" : TV , .JSONs } => . ...
... .List => ListItem(!ID)
... .List => ListItem(!ID)
@@ -533,14 +532,11 @@ The `"transactions"` key loads the transactions.
rule #exception CODE ~> check J:JSON => check J ~> #exception CODE
rule check DATA : { .JSONs } => . requires DATA =/=String "transactions"
rule check DATA : { (KEY:String) : VALUE , REST } => check DATA : { KEY : VALUE } ~> check DATA : { REST }
- requires REST =/=K .JSONs andBool notBool DATA in (SetItem("callcreates") SetItem("transactions"))
+ requires REST =/=K .JSONs andBool notBool DATA in (SetItem("callcreates") SetItem("callcreatesSorted") SetItem("transactions"))
rule check DATA : [ .JSONs ] => . requires DATA =/=String "ommerHeaders" andBool DATA =/=String "out"
rule check DATA : [ { TEST } , REST ] => check DATA : { TEST } ~> check DATA : [ REST ] requires DATA =/=String "transactions"
- rule check (KEY:String) : { JS:JSONs => #sortJSONList(JS) }
- requires KEY in (SetItem("callcreates")) andBool notBool #isSorted(JS)
-
rule check TESTID : { "post" : POST } => check "account" : POST ~> failure TESTID
rule check "account" : { ACCTID: { KEY : VALUE:JSON , REST } } => check "account" : { ACCTID : { KEY : VALUE } } ~> check "account" : { ACCTID : { REST } } requires REST =/=K .JSONs
// -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
@@ -579,7 +575,7 @@ The `"transactions"` key loads the transactions.
CONTRACT
...
- requires #dasmContract(CODE, #mainContract(CONTRACT)) ==K CONTRACT
+ requires #unparseByteStack(CODE) ==String #contractBytes(CONTRACT, #mainContract(CONTRACT))
rule check "account" : { ACCT : { "code" : .WordStack } } => . ...
ACCT
@@ -602,7 +598,7 @@ Here we check the other post-conditions associated with an EVM test.
rule check TESTID : { "logs" : LOGS } => check "logs" : LOGS ~> failure TESTID
// ------------------------------------------------------------------------------
- rule check "logs" : HASH:String => . ... SL requires #parseByteStack(Keccak256(#rlpEncodeLogs(SL))) ==K #parseByteStack(HASH)
+ rule check "logs" : HASH:String => . ... SL requires "0x" +String Keccak256(#rlpEncodeLogs(SL)) ==K HASH
rule check TESTID : { "status" : STATUS } => check "status" : STATUS ~> failure TESTID
// --------------------------------------------------------------------------------------
@@ -632,7 +628,8 @@ Here we check the other post-conditions associated with an EVM test.
rule check TESTID : { "callcreates" : CCREATES } => check "callcreates" : CCREATES ~> failure TESTID
// ----------------------------------------------------------------------------------------------------
- rule check "callcreates" : { ("data" : (DATA:String)) , ("destination" : (ACCTTO:String)) , ("gasLimit" : (GLIMIT:String)) , ("value" : (VAL:String)) , .JSONs }
+ rule check "callcreates" : { JS:JSONs } => check "callcreatesSorted" : { #sortJSONList(JS) }
+ rule check "callcreatesSorted" : { ("data" : (DATA:String)) , ("destination" : (ACCTTO:String)) , ("gasLimit" : (GLIMIT:String)) , ("value" : (VAL:String)) , .JSONs }
=> .
rule check TESTID : { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ~> failure TESTID
diff --git a/tests/failing.haskell b/tests/failing.haskell
index 6108068dd..c055025ba 100644
--- a/tests/failing.haskell
+++ b/tests/failing.haskell
@@ -507,3 +507,4 @@ tests/VMTests/vmSha3Test/sha3_2/sha3_2.iele.json
tests/VMTests/vmSha3Test/sha3_memSizeQuadraticCost65/sha3_memSizeQuadraticCost65.iele.json
tests/VMTests/vmSha3Test/sha3_3/sha3_3.iele.json
tests/VMTests/vmSha3Test/sha3_memSizeQuadraticCost32/sha3_memSizeQuadraticCost32.iele.json
+tests/iele/danse/unit/precompiled.iele.json
diff --git a/tests/slow.haskell b/tests/slow.haskell
new file mode 100644
index 000000000..850f182a7
--- /dev/null
+++ b/tests/slow.haskell
@@ -0,0 +1,73 @@
+tests/iele/danse/ERC20/totalSupply_Zero.iele.json
+tests/iele/danse/ERC20/totalSupply_Positive.iele.json
+tests/iele/danse/unit/precompiled.iele.json
+tests/iele/danse/ERC20/balanceOf_NonCaller.iele.json
+tests/iele/danse/auction/create.iele.json
+tests/iele/danse/ERC20/balanceOf_Caller.iele.json
+tests/iele/danse/ERC20/transfer_Other-MoreThanBalance.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-MoreThanBalanceLessThanAllowance.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-EntireAllowanceMoreThanBalance.iele.json
+tests/iele/danse/ERC20/transferFrom_FromEqTo-EntireAllowanceMoreThanBalance.iele.json
+tests/iele/danse/ERC20/transferFrom_FromEqTo-MoreThanBalanceLessThanAllowance.iele.json
+tests/iele/danse/ERC20/transfer_Caller-MoreThanBalance.iele.json
+tests/iele/danse/ERC20/transferFrom_CallerEqTo-MoreThanBalanceLessThanAllowance.iele.json
+tests/iele/danse/ERC20/transferFrom_CallerEqFrom-MoreThanBalance.iele.json
+tests/iele/danse/unit/blockhash.iele.json
+tests/iele/danse/auction/settle_success.iele.json
+tests/iele/danse/sum/sum_positive.iele.json
+tests/iele/danse/factorial/factorial_positive.iele.json
+tests/iele/danse/ERC20/allowance_OtherNEqOther.iele.json
+tests/iele/danse/ERC20/allowance_OtherEqOther.iele.json
+tests/iele/danse/ERC20/allowance_OtherCaller.iele.json
+tests/iele/danse/ERC20/allowance_CallerOther.iele.json
+tests/iele/danse/ERC20/allowance_CallerCaller.iele.json
+tests/iele/danse/ERC20/transfer_Caller-EntireBalance.iele.json
+tests/iele/danse/unit/logarithm.iele.json
+tests/iele/danse/unit/endian.iele.json
+tests/iele/danse/ERC20/transfer_Caller-NoOverflow.iele.json
+tests/iele/danse/unit/calladdress.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-BalanceNEqAllowance.iele.json
+tests/iele/danse/ERC20/transfer_Other-StillNoOverflow.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-EntireBalanceMoreThanAllowance.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-MoreThanAllowanceLessThanBalance.iele.json
+tests/iele/danse/ERC20/transfer_Other-EntireBalance.iele.json
+tests/iele/danse/ERC20/transfer_Other-NoOverflow.iele.json
+tests/iele/danse/ERC20/approve_Caller-Zero.iele.json
+tests/iele/danse/ERC20/approve_Other-Positive.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-EntireBalanceEqAllowance.iele.json
+tests/iele/danse/ERC20/transfer_Other-Positive.iele.json
+tests/iele/danse/forwarder/copycreate.iele.json
+tests/iele/danse/ERC20/approve_Caller-Positive.iele.json
+tests/iele/danse/unit/bits2.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-BalanceEqAllowance.iele.json
+tests/iele/danse/ERC20/transferFrom_FromEqTo-BalanceEqAllowance.iele.json
+tests/iele/danse/ERC20/approve_Other-Zero.iele.json
+tests/iele/danse/ERC20/transferFrom_AllEqual-EntireBalance.iele.json
+tests/iele/danse/ERC20/transferFrom_CallerEqFrom-AllowanceRelevant.iele.json
+tests/iele/danse/ERC20/transferFrom_FromEqTo-EntireBalanceMoreThanAllowance.iele.json
+tests/iele/danse/ERC20/transfer_Caller-Positive.iele.json
+tests/iele/danse/ERC20/transfer_Caller-StillNoOverflow.iele.json
+tests/iele/danse/ERC20/transferFrom_CallerEqFrom-EntireBalance.iele.json
+tests/iele/danse/ERC20/transfer_Caller-AllowanceIrrelevant.iele.json
+tests/iele/danse/ERC20/transferFrom_AllEqual-AllowanceRelevant.iele.json
+tests/iele/danse/ERC20/transferFrom_FromEqTo-NoOverflow.iele.json
+tests/iele/danse/ERC20/transferFrom_CallerEqTo-BalanceNEqAllowance.iele.json
+tests/iele/danse/ERC20/transferFrom_FromEqTo-EntireBalanceEqAllowance.iele.json
+tests/iele/danse/ERC20/transfer_Other-Zero.iele.json
+tests/iele/danse/auction/bid_higher.iele.json
+tests/iele/danse/forwarder/create.iele.json
+tests/iele/danse/ERC20/transferFrom_FromEqTo-MoreThanAllowanceLessThanBalance.iele.json
+tests/iele/danse/ERC20/transfer_Other-AllowanceIrrelevant.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-NoOverflow.iele.json
+tests/iele/danse/ERC20/transfer_Caller-Zero.iele.json
+tests/iele/danse/ERC20/approve_SwitchCaller.iele.json
+tests/iele/danse/ERC20/transferFrom_FromEqTo-BalanceNEqAllowance.iele.json
+tests/iele/danse/ERC20/create.iele.json
+tests/iele/danse/ERC20/transferFrom_AllDistinct-StillNoOverflow.iele.json
+tests/iele/danse/unit/fptr.iele.json
+tests/iele/danse/ERC20/transferFrom_CallerEqTo-MoreThanAllowanceLessThanBalance.iele.json
+tests/iele/danse/ERC20/transferFrom_Exploratory-MultipleTransfersThrow.iele.json
+tests/iele/danse/unit/staticcall.iele.json
+tests/iele/danse/ERC20/transferFrom_Exploratory-MultipleTransfersSucceed.iele.json
+tests/iele/danse/unit/exceptions.iele.json
+tests/iele/danse/ill-formed/illFormed2.iele.json