From 4477eef671113e49cfbf3214d736643bd02ceef8 Mon Sep 17 00:00:00 2001 From: dwightguth Date: Thu, 15 Nov 2018 12:25:59 -0600 Subject: [PATCH] modifications to support llvm backend (#159) * changes to iele to support llvm backend * fix race * more minor fixes * update submodules --- Makefile | 8 ++++---- data.md | 7 +++++-- iele-binary.md | 4 ++-- iele-gas.md | 6 +++--- iele-node.md | 3 +++ iele-syntax.md | 10 +++++++++- iele.md | 50 ++++++++++++++++++---------------------------- plugin | 2 +- tests/ci/rv-k | 2 +- well-formedness.md | 9 ++++----- 10 files changed, 51 insertions(+), 50 deletions(-) diff --git a/Makefile b/Makefile index 0a3a62bda..923e535a4 100644 --- a/Makefile +++ b/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 diff --git a/data.md b/data.md index e91a834c5..58fb09a79 100644 --- a/data.md +++ b/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) diff --git a/iele-binary.md b/iele-binary.md index c637fc301..63dd582a1 100644 --- a/iele-binary.md +++ b/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] diff --git a/iele-gas.md b/iele-gas.md index 06b2ec02d..829b11430 100644 --- a/iele-gas.md +++ b/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 #compute [ ret ARGS::Ints, SCHED ] => Gmove < SCHED > *Int #sizeRegs(ARGS) +Int 8 ... + rule #compute [ ret ARGS::NonEmptyInts, SCHED ] => Gmove < SCHED > *Int #sizeRegs(ARGS) +Int 8 ... ListItem(_) ... requires notBool Gnewmove << SCHED >> - rule #compute [ ret _::Ints, SCHED ] => 0 ... + rule #compute [ ret _::NonEmptyInts, SCHED ] => 0 ... .List requires notBool Gnewmove << SCHED >> - rule #compute [ ret _::Ints, SCHED ] => 0 ... + rule #compute [ ret _::NonEmptyInts, SCHED ] => 0 ... requires Gnewmove << SCHED >> rule #compute [ revert _, SCHED ] => 0 ``` diff --git a/iele-node.md b/iele-node.md index 8040a702a..87b34a8b0 100644 --- a/iele-node.md +++ b/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] // ---------------------------------------------------------- diff --git a/iele-syntax.md b/iele-syntax.md index ed92d33d4..f519586f0 100644 --- a/iele-syntax.md +++ b/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 diff --git a/iele.md b/iele.md index e28b0e358..e2ef36884 100644 --- a/iele.md +++ b/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 % REG:Int => REGS [ REG ] ... REGS false - 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 ACCTS requires notBool MINER in ACCTS - rule #finalizeTx(false) ... - NORMAL - GAVAIL => G*(GAVAIL, GLIMIT, REFUND) - REFUND => 0 - ListItem(MSGID:Int) ... - - MSGID - GLIMIT - ... - - requires REFUND =/=Int 0 - rule #finalizeTx(false => true) ... NORMAL ListItem(_) => .List ... @@ -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)] // ---------------------------------------------------------------------------------- diff --git a/plugin b/plugin index 6bbaadc4c..0d2eb8b2d 160000 --- a/plugin +++ b/plugin @@ -1 +1 @@ -Subproject commit 6bbaadc4c6ce1ba4cfa2edece4bc4f694516b171 +Subproject commit 0d2eb8b2dc128bc82caf21819b5a68df89c27134 diff --git a/tests/ci/rv-k b/tests/ci/rv-k index 952843c7c..65cf94b03 160000 --- a/tests/ci/rv-k +++ b/tests/ci/rv-k @@ -1 +1 @@ -Subproject commit 952843c7cbb33300d2201735b23164207d9df49a +Subproject commit 65cf94b03485c0d9bccfd6c648afddb737a54958 diff --git a/well-formedness.md b/well-formedness.md index 5d185c093..b470ab1a7 100644 --- a/well-formedness.md +++ b/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)) 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