evm, driver, analysis: #end now generates an exception, and sets the statusCode cell

Author: Everett Hildenbrandt

analysis.md

@@ -43,7 +43,7 @@ We'll need to make summaries of the state which collect information about how mu
 
     syntax KItem ::= "#endSummary"
  // ------------------------------
-    rule <k> (#end => .) ~> #endSummary ... </k>
+    rule <statusCode> EVM_SUCCESS </statusCode> <k> (#exception => .) ~> #endSummary ... </k>
     rule <k> #endSummary => . ... </k> <pc> PCOUNT </pc> <gas> GAVAIL </gas> <memoryUsed> MEMUSED </memoryUsed>
          <analysis> ... "blocks" |-> (ListItem({ PCOUNT1 | GAVAIL1 | MEMUSED1 } => { PCOUNT1 ==> PCOUNT | GAVAIL1 -Int GAVAIL | MEMUSED -Int MEMUSED1 }) REST) ... </analysis>
 ```

driver.md

@@ -83,7 +83,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
 
     syntax EthereumCommand ::= "flush"
  // ----------------------------------
-    rule <mode> EXECMODE </mode> <k> #end       ~> flush => #finalizeTx(EXECMODE ==K VMTESTS)               ... </k>
+    rule <mode> EXECMODE </mode> <statusCode> EVM_SUCCESS             </statusCode> <k> #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS)               ... </k>
     rule <mode> EXECMODE </mode> <statusCode> _:ExceptionalStatusCode </statusCode> <k> #exception ~> flush => #finalizeTx(EXECMODE ==K VMTESTS) ~> #exception ... </k>
 ```
 
@@ -181,7 +181,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
     rule <statusCode> _:ExceptionalStatusCode </statusCode> <k> #exception ~> #finishTx => #popCallStack ~> #popWorldState ... </k>
     rule <k> #revert    ~> #finishTx => #popCallStack ~> #popWorldState ~> #refund GAVAIL ... </k> <gas> GAVAIL </gas>
 
-    rule <k> #end ~> #finishTx => #mkCodeDeposit ACCT ... </k>
+    rule <statusCode> EVM_SUCCESS </statusCode>
+         <k> #exception ~> #finishTx => #mkCodeDeposit ACCT ... </k>
          <id> ACCT </id>
          <txPending> ListItem(TXID:Int) ... </txPending>
          <message>
@@ -190,7 +191,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            ...
          </message>
 
-    rule <k> #end ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... </k>
+    rule <statusCode> EVM_SUCCESS </statusCode>
+         <k> #exception ~> #finishTx => #popCallStack ~> #dropWorldState ~> #refund GAVAIL ... </k>
          <id> ACCT </id>
          <gas> GAVAIL </gas>
          <txPending> ListItem(TXID:Int) ... </txPending>

evm.md

@@ -252,11 +252,11 @@ Control Flow
 
 ```k
     syntax KItem     ::= Exception
-    syntax KItem     ::= "#exception" StatusCode
-    syntax Exception ::= "#exception" | "#end" | "#revert"
- // ------------------------------------------------------
-    rule <k> #exception SC => #exception ... </k>
-         <statusCode> _ => SC </statusCode>
+    syntax KItem     ::= "#exception" StatusCode | "#end"
+    syntax Exception ::= "#exception" | "#revert"
+ // ---------------------------------------------
+    rule <k> #end          => #exception EVM_SUCCESS ... </k>
+    rule <k> #exception SC => #exception             ... </k> <statusCode> _ => SC </statusCode>
 
     rule <k> EX:Exception ~> (_:Int    => .) ... </k>
     rule <k> EX:Exception ~> (_:OpCode => .) ... </k>
@@ -271,7 +271,6 @@ Control Flow
  // ----------------------------------
     rule <k>            #? B1 : _  ?# => B1               ... </k>
     rule <k> #revert ~> #? B1 : _  ?# => B1 ~> #revert    ... </k>
-    rule <k> #end    ~> #? B1 : _  ?# => B1 ~> #end       ... </k>
     rule <statusCode> SC </statusCode>
          <k> #exception ~> #? B1 : B2 ?# => #if isExceptionalStatusCode(SC) #then B2 #else B1 #fi ~> #exception ... </k>
 ```
@@ -1455,7 +1454,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
          <output> OUT </output>
          <gas> GAVAIL </gas>
 
-    rule <k> #end ~> #return RETSTART RETWIDTH
+    rule <statusCode> EVM_SUCCESS </statusCode>
+         <k> #exception ~> #return RETSTART RETWIDTH
           => #popCallStack ~> #dropWorldState
           ~> 1 ~> #push ~> #refund GAVAIL ~> #setLocalMem RETSTART RETWIDTH OUT
          ...
@@ -1609,7 +1609,8 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
     rule <k> #revert ~> #codeDeposit _ => #popCallStack ~> #popWorldState ~> #refund GAVAIL ~> 0 ~> #push ... </k>
          <gas> GAVAIL </gas>
 
-    rule <k> #end ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... </k>
+    rule <statusCode> EVM_SUCCESS </statusCode>
+         <k> #exception ~> #codeDeposit ACCT => #mkCodeDeposit ACCT ... </k>
 
     rule <k> #mkCodeDeposit ACCT
           => Gcodedeposit < SCHED > *Int #sizeWordStack(OUT) ~> #deductGas

tests/interactive/gas-analysis/sumTo10.evm.out

@@ -24,7 +24,7 @@
         .WordStack
       </output>
       <statusCode>
-        .StatusCode
+        EVM_SUCCESS
       </statusCode>
       <callStack>
         .List