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 5104a46. * Revert "data.md: #take 4 at a time" This reverts commit 0a071f1. * 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
runtimeverification · Jan 6, 2021 · e150736 · e150736
1 parent 5ac7eb4
commit e150736
Show file tree

Hide file tree

Showing 6 changed files with 127 additions and 30 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 <k> load "transactions" : { "arguments" : [ ARGS ],  "contractCode" : TI , "from" : FROM, "function" : FUNC, "gasLimit" : TG , "gasPrice" : TP , "nonce" : TN , "to" : TT , "value" : TV , .JSONs } => . ... </k>
+    rule <k> load "transactionsSorted" : { "arguments" : [ ARGS ],  "contractCode" : TI , "from" : FROM, "function" : FUNC, "gasLimit" : TG , "gasPrice" : TP , "nonce" : TN , "to" : TT , "value" : TV , .JSONs } => . ... </k>
          <txOrder>   ... .List => ListItem(!ID) </txOrder>
          <txPending> ... .List => ListItem(!ID) </txPending>
          <messages>
@@ -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.
            <code> CONTRACT </code>
            ...
          </account>
-         requires #dasmContract(CODE, #mainContract(CONTRACT)) ==K CONTRACT
+         requires #unparseByteStack(CODE) ==String #contractBytes(CONTRACT, #mainContract(CONTRACT))
     rule <k> check "account" : { ACCT : { "code" : .WordStack } } => . ... </k>
          <account>
            <acctID> ACCT </acctID>
@@ -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 <k> check "logs" : HASH:String => . ... </k> <logData> SL </logData> requires #parseByteStack(Keccak256(#rlpEncodeLogs(SL))) ==K #parseByteStack(HASH)
+    rule <k> check "logs" : HASH:String => . ... </k> <logData> SL </logData> 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
@@ -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
@@ -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