modifications to support llvm backend (#159)

* changes to iele to support llvm backend

* fix race

* more minor fixes

* update submodules

Makefile

@@ -134,14 +134,14 @@ test-bad-packet:
 	netcat 127.0.0.1 $(PORT) < tests/bad-packet-2
 	.build/vm/iele-test-vm tests/iele/albe/sum/sum_zero.iele.json $(PORT)
 
-tests/VMTests/%.json.test: tests/VMTests/%.json | build
+tests/VMTests/%.json.test: tests/VMTests/%.json | .build/standalone/iele-testing-kompiled/interpreter
 	./vmtest $<
-tests/BlockchainTests/%.json.test: tests/BlockchainTests/%.json | build
+tests/BlockchainTests/%.json.test: tests/BlockchainTests/%.json | .build/standalone/iele-testing-kompiled/interpreter
 	./blockchaintest $<
-tests/iele/%.json.test: tests/iele/%.json | build
+tests/iele/%.json.test: tests/iele/%.json | .build/standalone/iele-testing-kompiled/interpreter 
 	./blockchaintest $<
 
-%.iele.test: %.iele | build
+%.iele.test: %.iele | .build/check/well-formedness-kompiled/interpreter
 	./check-iele $<
 
 PORT?=10000

data.md

@@ -107,9 +107,12 @@ Primitives provide the basic conversion from K's sorts `Int` and `Bool` to IELE'
     rule #sizeLVals(REG , REGS, N) => #sizeLVals(REGS, N +Int 1)
     rule #sizeLVals(.LValues, N) => N
 
-    syntax String ::= IeleName2String ( IeleName ) [function, hook(STRING.token2string)]
+    syntax String ::= IeleName2String ( IeleName ) [function]
+                    | IeleNameToken2String ( IeleName ) [function, hook(STRING.token2string)]
     syntax IeleName ::= String2IeleName ( String ) [function, hook(STRING.string2token)]
  // ------------------------------------------------------------------------------------
+    rule IeleName2String(I:Int) => Int2String(I)
+    rule IeleName2String(N) => IeleNameToken2String(N) [owise]
     syntax String ::= StringIeleName2String ( StringIeleName ) [function, hook(STRING.token2string)]
  // ------------------------------------------------------------------------------------------------
 
@@ -469,7 +472,7 @@ We need to interperet a `WordStack` as a `String` again so that we can call `Kec
 -   `#unparseByteStack` turns a stack of bytes (as a `WordStack`) into a `String`.
 
 ```k
-    syntax String ::= #unparseByteStack ( WordStack )                [function, klabel(unparseByteStack)]
+    syntax String ::= #unparseByteStack ( WordStack )                [function]
                     | #unparseByteStack ( WordStack , StringBuffer ) [function, klabel(#unparseByteStackAux)]
  // ---------------------------------------------------------------------------------------------------------
     rule #unparseByteStack ( WS ) => #unparseByteStack(WS, .StringBuffer)

iele-binary.md

@@ -318,9 +318,9 @@ After interpreting the strings representing programs as a `WordStack`, it should
  // --------------------------------------------------------------------
     rule %(REGS, WIDTH, MASK, IDX) => % ((REGS >>Int (IDX *Int WIDTH)) &Int MASK)
 
-    syntax Operands ::= "%o" "(" Int "," Int "," Int "," Int "," Int ")" [function]
+    syntax NonEmptyOperands ::= "%o" "(" Int "," Int "," Int "," Int "," Int ")" [function]
  // -------------------------------------------------------------------------------
-    rule %o(REGS, WIDTH, MASK, IDX, 0) => .Operands
+    rule %o(REGS, WIDTH, MASK, IDX, 0) => .NonEmptyOperands
     rule %o(REGS, WIDTH, MASK, IDX, COUNT) => %(REGS, WIDTH, MASK, IDX) , %o(REGS, WIDTH, MASK, IDX +Int 1, COUNT -Int 1) [owise]
 
     syntax LValues ::= "%l" "(" Int "," Int "," Int "," Int "," Int ")" [function]

iele-gas.md

@@ -594,14 +594,14 @@ constant cost to perform the jump and store the return address.
 The cost to return is folded into the cost of the call instruction.
 
 ```k
-    rule <k> #compute [ ret ARGS::Ints, SCHED ] => Gmove < SCHED > *Int #sizeRegs(ARGS) +Int 8 ... </k>
+    rule <k> #compute [ ret ARGS::NonEmptyInts, SCHED ] => Gmove < SCHED > *Int #sizeRegs(ARGS) +Int 8 ... </k>
          <localCalls> ListItem(_) ... </localCalls>
       requires notBool Gnewmove << SCHED >>
-    rule <k> #compute [ ret _::Ints, SCHED ] => 0 ... </k>
+    rule <k> #compute [ ret _::NonEmptyInts, SCHED ] => 0 ... </k>
          <localCalls> .List </localCalls>
       requires notBool Gnewmove << SCHED >>
 
-    rule <k> #compute [ ret _::Ints, SCHED ] => 0 ... </k>
+    rule <k> #compute [ ret _::NonEmptyInts, SCHED ] => 0 ... </k>
       requires Gnewmove << SCHED >>
     rule #compute [ revert _, SCHED ] => 0
 ```

iele-node.md

@@ -127,6 +127,9 @@ module IELE-NODE
     rule #toList(.Ints) => .List
     rule #toList(I , L) => ListItem(I) #toList(L)
 
+    syntax String ::= unparseByteStack(Bytes) [function]
+    rule unparseByteStack(B::Bytes) => Bytes2String(B)
+
     syntax KItem ::= vmResult(return: List,gas: Int,refund: Int,status: Int,selfdestruct: List,logs: List,AccountsCell, touched: List)
     syntax KItem ::= extractConfig(GeneratedTopCell) [function]
  // ----------------------------------------------------------

iele-syntax.md

@@ -45,7 +45,7 @@ module IELE-COMMON
   syntax NumericIeleName ::= Int
   syntax StringIeleName
   syntax IeleName ::= NumericIeleName
-  syntax IeleName ::= StringIeleName [klabel(StringIeleName), avoid, symbol]
+  syntax IeleName ::= StringIeleName [klabel(StringIeleName), avoid, symbol, function]
 ```
 
 ### Identifiers
@@ -100,6 +100,14 @@ IELE instruction operands are used at the left- and right-hand side of IELE inst
   syntax Ints ::= List{Int, ","} [klabel(operandList)]
 
   syntax Operands ::= Ints
+
+  syntax Operands ::= NonEmptyOperands
+
+  syntax Ints ::= NonEmptyInts
+
+  syntax NonEmptyOperands ::= NonEmptyInts
+
+  syntax NonEmptyInts ::= NeList{Int, ","} [klabel(operandList)]
 ```
 
 ### Assignment

iele.md

@@ -163,6 +163,24 @@ In the comments next to each cell, we explain the purpose of the cell.
     syntax Schedule
     syntax Contract ::= "#emptyCode"
  // --------------------------------
+```
+
+### Uninitialized Accounts
+
+An account to which code has never been deployed has a size in bytes of zero, but contains an implicit public function `@deposit` which takes
+no arguments, returns no values, and does nothing. This function exists to allow accounts to receive payment even if they do not have a contract
+deployed to them. Note that a contract can forbid payments by refusing to declare the `@deposit` function, and explicitly raising an exception
+if any of its entry points are invoked with a balance transfer.
+
+Note that the syntax used in the following `#emptyCode` macro is desugared IELE syntax, where contracts have a size in bytes metadata attachment (`!0` here) and argument lists are replaced with an integer value representing arity (`0` here).
+
+```k
+    syntax IeleName ::= "Main" [token]
+                      | "iele.Wallet" [token]
+    syntax ContractDefinition ::= "contract" IeleName "!" /* size in bytes */ Int /* byte string */ String "{" TopLevelDefinitions "}" /* when desugared to include the code size */
+ // --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
+    rule #emptyCode => contract iele.Wallet !0 "" { define public @deposit ( 0 ) { ret .NonEmptyOperands .Instructions .LabeledBlocks } } .Contract [macro]
+
 endmodule
 ```
 
@@ -342,7 +360,6 @@ Description of registers.
  // ---------------------------
     rule <k> % REG:Int => REGS [ REG ] ... </k> <regs> REGS </regs> <typeChecking> false </typeChecking>
 
-    syntax NonEmptyOperands ::= Operands
     syntax KResult ::= Ints
  // -----------------------
     rule isKResult(.Operands) => true
@@ -657,18 +674,6 @@ After executing a transaction, it's necessary to have the effect of the substate
          <activeAccounts> ACCTS </activeAccounts>
       requires notBool MINER in ACCTS
 
-    rule <k> #finalizeTx(false) ... </k>
-         <mode> NORMAL </mode>
-         <gas> GAVAIL => G*(GAVAIL, GLIMIT, REFUND) </gas>
-         <refund> REFUND => 0 </refund>
-         <txPending> ListItem(MSGID:Int) ... </txPending>
-         <message>
-            <msgID> MSGID </msgID>
-            <txGasLimit> GLIMIT </txGasLimit>
-            ...
-         </message>
-      requires REFUND =/=Int 0
-
     rule <k> #finalizeTx(false => true) ... </k>
          <mode> NORMAL </mode>
          <txPending> ListItem(_) => .List ... </txPending>
@@ -708,22 +713,6 @@ Organization is based roughly on what parts of the execution state are needed to
 We use an explicit call to `@iele.invalid` both for marking the designated invalid operator and for garbage bytes in the input program.
 Executing the INVALID instruction results in an exception.
 
-### Uninitialized Accounts
-
-An account to which code has never been deployed has a size in bytes of zero, but contains an implicit public function `@deposit` which takes
-no arguments, returns no values, and does nothing. This function exists to allow accounts to receive payment even if they do not have a contract
-deployed to them. Note that a contract can forbid payments by refusing to declare the `@deposit` function, and explicitly raising an exception
-if any of its entry points are invoked with a balance transfer.
-
-Note that the syntax used in the following `#emptyCode` macro is desugared IELE syntax, where contracts have a size in bytes metadata attachment (`!0` here) and argument lists are replaced with an integer value representing arity (`0` here).
-
-```k
-    syntax IeleName ::= "Main" [token]
-                      | "iele.Wallet" [token]
- // ----------------------------------
-    rule #emptyCode => contract iele.Wallet !0 "" { define public @deposit ( 0 ) { ret .NonEmptyOperands .Instructions .LabeledBlocks } } .Contract [macro]
-```
-
 ### Register Manipulations
 
 Some operators don't calculate anything, they just manipulate the state of registers.
@@ -1730,7 +1719,6 @@ module IELE-PROGRAM-LOADING
     // when type checking contracts
     rule contract NAME ! _ _ { DEFS } => contract NAME { DEFS }
 
-    syntax ContractDefinition ::= "contract" IeleName "!" /* size in bytes */ Int /* byte string */ String "{" TopLevelDefinitions "}" /* when desugared to include the code size */
     syntax FunctionParameters ::= Int /* when desugared to just the number of parameters */
 
     syntax ProgramCell ::= #loadCode ( Contract ) [function]
@@ -1808,7 +1796,7 @@ module IELE-PROGRAM-LOADING
 
     syntax Int ::= #registers ( Instruction ) [function]
                  | #registers ( LValues ) [function, klabel(registersLValues)]
-                 | #registers ( NonEmptyOperands ) [function, klabel(registersOperands)]
+                 | #registers ( Operands ) [function, klabel(registersOperands)]
     syntax Int ::= #computeNRegs ( Blocks )       [function]
                  | #computeNRegs ( Blocks , Int ) [function, klabel(#computeNRegsAux)]
  // ----------------------------------------------------------------------------------

well-formedness.md

@@ -18,7 +18,7 @@ Our semantics is modal, with the initial mode being set on the command line via
 
 ```k
 module IELE-CONSTANTS
-    syntax Mode ::= "NORMAL" [klabel(NORMAL)] | "VMTESTS"
+    syntax Mode ::= "NORMAL" [klabel(NORMAL), symbol] | "VMTESTS"
     syntax Schedule ::= "ALBE"
                       | "DANSE"
 endmodule
@@ -191,7 +191,6 @@ Each of these instructions takes some number of immediates, globals, or register
 ```k
     syntax KResult ::= Type
                      | Types
-    syntax NonEmptyOperands ::= Operands
     syntax KItem ::= "check"
  // ------------------------
 
@@ -336,8 +335,8 @@ Reserved Names
 All identifiers beginning with "iele." are reserved by the language and cannot be written to.
 
 ```k
-    syntax K ::= checkName(IeleName)
- // --------------------------------
+    syntax KItem ::= checkName(IeleName)
+ // ------------------------------------
     rule checkName(NAME) => .
       requires lengthString(IeleName2String(NAME)) <Int 5 orBool substrString(IeleName2String(NAME), 0, 5) =/=String "iele."
 
@@ -360,7 +359,7 @@ In order to correctly check names, we must convert escaped IELE names to their c
       requires IDX <Int lengthString(S) -Int 1 andBool substrString(S, IDX, IDX +Int 1) ==K "\\"
     rule unescape(S, IDX, SB) => StringBuffer2String(SB)
       requires IDX ==Int lengthString(S) -Int 1
-    rule `StringIeleName`(NAME:StringIeleName) => String2IeleName(unescape(StringIeleName2String(NAME))) [anywhere]
+    rule `StringIeleName`(NAME:StringIeleName) => String2IeleName(unescape(StringIeleName2String(NAME)))
 ```
 
 Checking Operands