From e4c7ba1f292ebf922cc6e42fdf906b0641d6214c Mon Sep 17 00:00:00 2001 From: Vladimir Lebedev Date: Tue, 20 Feb 2024 16:40:37 +0700 Subject: [PATCH] Implement control flow specification (#3) --- README.md | 229 +++++++++-- cp0.json | 1063 ++++++++++++++++++++++++++++++++++++++++++++++++++- schema.json | 208 +++++++++- 3 files changed, 1447 insertions(+), 53 deletions(-) diff --git a/README.md b/README.md index 123399e..71a8f67 100644 --- a/README.md +++ b/README.md @@ -17,64 +17,121 @@ Based on [instructions.csv](https://github.com/ton-community/ton-docs/blob/main/ | doc | ✅ Implemented | Provides human-readable information about instructions. Can be useful to provide integrated docs to user, for example, in disassembler. | bytecode | ✅ Implemented | Describes instruction encoding. It contains information to determine, which instruction we are currently decoding and how to parse its operands. | value_flow | ✅ Implemented | Describes how instruction changes current stack. This part of specification allows to analyze how instructions interact with each other, so it becomes possible to implement high-level tools such as decompilers. -| control_flow | ❌ Not implemented | Describes code flow. It helps to reconstruct a control flow graph. This part mainly contains semantics of cont_* category instructions. For example, both JMPX and CALLX transfers execution to continuation on stack, but only CALLX returns and JMPX is not. +| control_flow | ✅ Implemented | Describes code flow (operations with cc register). It helps to reconstruct a control flow graph. This part mainly contains semantics of cont_* category instructions. For example, both JMPX and CALLX transfers execution to continuation on stack, but only CALLX returns and JMPX is not. | aliases | ✅ Implemented | Specifies instruction aliases. Can be used to provide to user information about special cases (for example, SWAP is a special case of XCHG_0i with i = 1). +## Usage +Convenient way is to add submodule to your tool. This will greatly simplify debugging and upgrading process. +```bash +git submodule add https://github.com/hacker-volodya/tvm-spec +``` +However, nothing can stop you from just copying `cp0.json` (and `schema.json` if necessary). + ## Projects based on tvm-spec 1. [tvm-spec-example](https://github.com/hacker-volodya/tvm-spec-example), tiny TVM disassembler +2. [tvm-research](https://github.com/hacker-volodya/tvm-research), collection of tool prototypes with the power of tvm-spec ## Instruction Specification ### Example ```json -{ - "mnemonic": "LDU", - "doc": { - "category": "cell_parse", - "description": "Loads an unsigned `cc+1`-bit integer `x` from _Slice_ `s`.", - "gas": "26", - "fift": "[cc+1] LDU" - }, - "bytecode": { - "doc_opcode": "D3cc", - "tlb": "#D3 cc:uint8", - "prefix": "D3", - "operands": [ - { - "name": "c", - "loader": "uint", - "loader_args": { - "size": 8 - } - } - ] - }, - "value_flow": { - "doc_stack": "s - x s'", - "inputs": { - "stack": [ +[ + { + "mnemonic": "LDU", + "doc": { + "category": "cell_parse", + "description": "Loads an unsigned `cc+1`-bit integer `x` from _Slice_ `s`.", + "gas": "26", + "fift": "[cc+1] LDU" + }, + "bytecode": { + "doc_opcode": "D3cc", + "tlb": "#D3 cc:uint8", + "prefix": "D3", + "operands": [ { - "type": "simple", - "name": "s", - "value_types": ["Slice"] + "name": "c", + "loader": "uint", + "loader_args": { + "size": 8 + } } ] }, - "outputs": { - "stack": [ - { - "type": "simple", - "name": "x", - "value_types": ["Integer"] - }, + "value_flow": { + "doc_stack": "s - x s'", + "inputs": { + "stack": [ + { + "type": "simple", + "name": "s", + "value_types": ["Slice"] + } + ] + }, + "outputs": { + "stack": [ + { + "type": "simple", + "name": "x", + "value_types": ["Integer"] + }, + { + "type": "simple", + "name": "s2", + "value_types": ["Slice"] + } + ] + } + } + }, + { + "mnemonic": "EXECUTE", + "doc": { + "category": "cont_basic", + "description": "_Calls_, or _executes_, continuation `c`.", + "gas": "18", + "fift": "EXECUTE\nCALLX" + }, + "bytecode": { + "doc_opcode": "D8", + "tlb": "#D8", + "prefix": "D8", + "operands": [] + }, + "value_flow": { + "doc_stack": "c - ", + "inputs": { + "stack": [ + { + "type": "simple", + "name": "c", + "value_types": ["Continuation"] + } + ] + }, + "outputs": { + "stack": [ + ] + } + }, + "control_flow": { + "branches": [ { - "type": "simple", - "name": "s2", - "value_types": ["Slice"] + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } } ] } } -} +] ``` ### Documentation @@ -104,6 +161,9 @@ Based on [instructions.csv](https://github.com/ton-community/ton-docs/blob/main/ | value_flow.inputs.stack[i].type | Type of stack entry. Can be one of "simple", "const", "conditional", "array". Required. | value_flow.inputs.stack[i].* | Properties for stack entries of each type are described below. | value_flow.outputs | Outgoing values constraints. Output is unconstrained if absent. Identical to value_flow.inputs. +| control_flow | Information related to current cc modification by instruction. Optional. +| control_flow.branches | Array of possible branches of an instruction. Specifies all possible values of cc after instruction execution. Empty by default (no branches can be taken by instruction). Each branch described by a `Continuation` object described below. +| control_flow.nobranch | Can this instruction not perform any of specified branches in certain cases (do not modify cc)? False by default. ### Loaders Specification and Examples #### uint @@ -290,9 +350,94 @@ _Stack notation: `pk_1 msg_1 ... pk_n msg_n`_ Specifies a bunch of stack entries with length from variable `length_var`, usually noted as `x_1 ... x_n`. Each part of array, such as `x_i` or `x_i y_i` is described in `array_entry`. Used in tuple, continuation arguments and crypto operations. #### Notes -1. Each variable name is unique across `operands` and `stack` sections of each instruction. Assumed that variables are immutable, so if variable `x` is defined both in inputs and outputs, it goes to output without any modification. +1. Each variable name is unique across `operands`, `value_flow`, and `control_flow` sections of each instruction. Assumed that variables are immutable, so if variable `x` is defined both in inputs and outputs, it goes to output without any modification. 2. Value flow describes only `cc` stack usage before the actual jump or call. Subsequent continuations may have a separate stack, so this will be defined in control flow section of this spec. +### Continuations Specification and Examples +Each object represents a continuation, which can be constructed in several ways: +* from a variable (operand or stack) +* from cc register +* from c0-c3 registers +* by "extraordinary continuation" constructors (as in [tvm.pdf](https://docs.ton.org/tvm.pdf), p.50: "4.1.5. Extraordinary continuations.") + +Savelist can be defined using `save` property. Keys are `c0`, `c1`, `c2`, `c3` and values are continuation objects (in fact, continuation is a recursive type, representing a tree of continuations). Please note that savelist defined here will not override already saved continuation registers (that's the standard behaviour of TVM when saving registers). + +#### variable +```json +{ + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } +} +``` +Specifies a variable-backed continuation. Variable may be not referenced previously (in `operands` or `value_flow` section), assuming that it is defined somewhere in the actual implementation of the instruction. Example of such instruction is `DICTIGETJMP`: internally it does dictionary lookup for continuation retrieval, so `x` in control flow is expected to be defined in the implementation of `DICTIGETJMP`. + +#### cc +```json +{ + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } +} +``` +Specifies a continuation, which is constructed from cc code and `save` registers. In C++ implementation this operation is implemented in [VmState::extract_cc](https://github.com/ton-blockchain/ton/blob/17c3477f7191fe6e5db22b71631b5c7472046c2f/crypto/vm/vm.cpp#L356). + +#### register +```json +{ + "type": "register", + "index": 3, + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } +} +``` +Specifies continuation from register with `index` (`"index": 3` => take continuation from `c3`). + +#### special +```json +{ + "type": "special", + "name": "repeat", + "args": { + "count": "n", + "body": { + "type": "variable", + "var_name": "c" + }, + "after": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } +} +``` + +Specifies extraordinary continuation. `save` property does not apply here. + +| name | args | description +| ---- | ---- | ----------- +| repeat | string count; continuation body, after | Count is the name of a count variable. Jumps to `body` with `c0 = repeat(count - 1, body, after)`, jumps to `after` if `count <= 0`. +| until | continuation body, after | Pops boolean from stack, jumps to `after` if it is `true`, otherwise jumps to `body` with `c0 = until(body, after)`. +| while | continuation cond, body, after | Pops boolean from stack, jumps to `after` if it is `false`, otherwise jumps to `body` with `c0 = cond` and `cond.c0 = while(cond, body, after)`. +| again | continuation body | Jumps to body with `c0 = again(body)`. +| pushint | continuation next; integer value | Push `value` on stack, jump to `next`. + ## Alias Specification ### Example ```json diff --git a/cp0.json b/cp0.json index f98ae65..d6329e5 100644 --- a/cp0.json +++ b/cp0.json @@ -23238,6 +23238,22 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -23269,6 +23285,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23326,6 +23350,22 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -23376,6 +23416,22 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -23426,6 +23482,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23471,6 +23535,11 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 0 } + ] } }, { @@ -23497,6 +23566,11 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 0 } + ] } }, { @@ -23523,6 +23597,11 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 1 } + ] } }, { @@ -23554,6 +23633,12 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 0 }, + { "type": "register", "index": 1 } + ] } }, { @@ -23585,6 +23670,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23616,6 +23709,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23673,6 +23774,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23725,6 +23834,22 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -23772,6 +23897,22 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -23824,6 +23965,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23876,6 +24025,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23908,6 +24065,22 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -23940,6 +24113,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23972,6 +24153,14 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -23998,6 +24187,11 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 0 } + ] } }, { @@ -24064,6 +24258,12 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 0 } + ], + "nobranch": true } }, { @@ -24094,6 +24294,12 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 0 } + ], + "nobranch": true } }, { @@ -24135,6 +24341,23 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ], + "nobranch": true } }, { @@ -24176,6 +24399,23 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ], + "nobranch": true } }, { @@ -24217,6 +24457,15 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ], + "nobranch": true } }, { @@ -24258,6 +24507,15 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ], + "nobranch": true } }, { @@ -24304,6 +24562,34 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + }, + { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -24340,6 +24626,23 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ], + "nobranch": true } }, { @@ -24376,6 +24679,23 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ], + "nobranch": true } }, { @@ -24412,6 +24732,15 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ], + "nobranch": true } }, { @@ -24448,6 +24777,15 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ], + "nobranch": true } }, { @@ -24564,6 +24902,12 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 1 } + ], + "nobranch": true } }, { @@ -24594,6 +24938,12 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { "type": "register", "index": 1 } + ], + "nobranch": true } }, { @@ -24635,6 +24985,34 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + }, + { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -24676,6 +25054,34 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + }, + { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -24717,6 +25123,34 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c1", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + }, + { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -24766,6 +25200,14 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -24815,6 +25257,14 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -24864,6 +25314,14 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -24913,6 +25371,14 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c" + } + ] } }, { @@ -24955,6 +25421,28 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "special", + "name": "repeat", + "args": { + "count": "n", + "body": { + "type": "variable", + "var_name": "c" + }, + "after": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ], + "nobranch": true } }, { @@ -24986,6 +25474,25 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "special", + "name": "repeat", + "args": { + "count": "n", + "body": { + "type": "cc" + }, + "after": { + "type": "register", + "index": 0 + } + } + } + ], + "nobranch": true } }, { @@ -25023,6 +25530,32 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "special", + "name": "until", + "args": { + "body": { + "type": "variable", + "var_name": "c" + }, + "after": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + } + } + ] } }, { @@ -25047,6 +25580,25 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "cc", + "save": { + "c0": { + "type": "special", + "name": "until", + "args": { + "body": { + "type": "cc" + }, + "after": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -25089,6 +25641,36 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "special", + "name": "while", + "args": { + "cond": { + "type": "variable", + "var_name": "c2" + }, + "body": { + "type": "variable", + "var_name": "c" + }, + "after": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + } + } + ] } }, { @@ -25120,6 +25702,31 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "special", + "name": "while", + "args": { + "cond": { + "type": "variable", + "var_name": "c2" + }, + "body": { + "type": "cc" + }, + "after": { "type": "register", "index": 0 } + } + } + } + } + + ] } }, { @@ -25156,6 +25763,20 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "special", + "name": "again", + "args": { + "body": { + "type": "variable", + "var_name": "c" + } + } + } + ] } }, { @@ -25182,6 +25803,19 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "special", + "name": "again", + "args": { + "body": { + "type": "cc" + } + } + } + ] } }, { @@ -25224,6 +25858,38 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "special", + "name": "repeat", + "args": { + "count": "n", + "body": { + "type": "variable", + "var_name": "c", + "save": { + "c1": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 } + } + } + } + }, + "after": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 } + } + } + } + } + ], + "nobranch": true } }, { @@ -25255,6 +25921,31 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "special", + "name": "repeat", + "args": { + "count": "n", + "body": { + "type": "cc", + "save": { + "c1": { + "type": "register", + "index": 0 + } + } + }, + "after": { + "type": "register", + "index": 0 + } + } + } + ], + "nobranch": true } }, { @@ -25292,6 +25983,49 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "special", + "name": "until", + "args": { + "body": { + "type": "variable", + "var_name": "c", + "save": { + "c1": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 } + } + } + } + }, + "after": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 } + } + } + } + }, + "c1": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 } + } + } + } + } + ] } }, { @@ -25318,6 +26052,30 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "cc", + "save": { + "c0": { + "type": "special", + "name": "until", + "args": { + "body": { + "type": "cc", + "save": { + "c1": { "type": "register", "index": 0 } + } + }, + "after": { "type": "register", "index": 0 } + } + }, + "c1": { "type": "register", "index": 0 } + } + } + + ] } }, { @@ -25360,6 +26118,37 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "special", + "name": "while", + "args": { + "cond": { + "type": "variable", + "var_name": "c2" + }, + "body": { + "type": "variable", + "var_name": "c" + }, + "after": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 } + } + } + } + } + } + } + ] } }, { @@ -25460,7 +26249,7 @@ "mnemonic": "SETCONTARGS_N", "doc": { "category": "cont_stack", - "description": "Similar to `[r] -1 SETCONTARGS`, but sets `c.nargs` to the final size of the stack of `c'` plus `n`. In other words, transforms `c` into a _closure_ or a _partially applied function_, with `0 <= n <= 14` arguments missing.", + "description": "Pushes `0 <= r <= 15` values `x_1...x_r` into the stack of (a copy of) the continuation `c`, starting with `x_1`. When `n` is 15 (-1 in Fift notation), does nothing with `c.nargs`. For `0 <= n <= 14`, sets `c.nargs` to the final size of the stack of `c'` plus `n`. In other words, transforms `c` into a _closure_ or a _partially applied function_, with `0 <= n <= 14` arguments missing.", "gas": "26+s\u0432\u0402\u045c", "fift": "[r] [n] SETCONTARGS" }, @@ -26621,6 +27410,44 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "special", + "name": "pushint", + "args": { + "next": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 } + } + }, + "value": -1 + } + }, + "c1": { + "type": "special", + "name": "pushint", + "args": { + "next": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 } + } + }, + "value": 0 + } + } + } + } + ] } }, { @@ -26712,6 +27539,22 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "register", + "index": 3, + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -26751,6 +27594,22 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "register", + "index": 3, + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -26790,6 +27649,14 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "register", + "index": 3 + } + ] } }, { @@ -27440,6 +28307,39 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 }, + "c2": { "type": "register", "index": 2 } + } + }, + "c2": { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 }, + "c2": { "type": "register", "index": 2 } + } + }, + "c2": { "type": "register", "index": 2 } + } + } + } + } + ] } }, { @@ -27502,6 +28402,39 @@ "stack": [ ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "c", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 }, + "c2": { "type": "register", "index": 2 } + } + }, + "c2": { + "type": "variable", + "var_name": "c2", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 }, + "c1": { "type": "register", "index": 1 }, + "c2": { "type": "register", "index": 2 } + } + }, + "c2": { "type": "register", "index": 2 } + } + } + } + } + ] } }, { @@ -36208,6 +37141,14 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x" + } + ] } }, { @@ -36248,6 +37189,14 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x" + } + ] } }, { @@ -36288,6 +37237,22 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -36328,6 +37293,22 @@ "outputs": { "stack": [] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -36532,6 +37513,14 @@ }, "value_flow": { "doc_stack": "s D n - s' s'' or s" + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x" + } + ] } }, { @@ -36583,6 +37572,22 @@ } ] } + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -36614,6 +37619,14 @@ }, "value_flow": { "doc_stack": "s - s' s'' or s" + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x" + } + ] } }, { @@ -36632,6 +37645,14 @@ }, "value_flow": { "doc_stack": "i D n - i or nothing" + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x" + } + ] } }, { @@ -36650,6 +37671,14 @@ }, "value_flow": { "doc_stack": "i D n - i or nothing" + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x" + } + ] } }, { @@ -36668,6 +37697,22 @@ }, "value_flow": { "doc_stack": "i D n - i or nothing" + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { @@ -36686,6 +37731,22 @@ }, "value_flow": { "doc_stack": "i D n - i or nothing" + }, + "control_flow": { + "branches": [ + { + "type": "variable", + "var_name": "x", + "save": { + "c0": { + "type": "cc", + "save": { + "c0": { "type": "register", "index": 0 } + } + } + } + } + ] } }, { diff --git a/schema.json b/schema.json index defa595..0fa4091 100644 --- a/schema.json +++ b/schema.json @@ -149,10 +149,10 @@ }, "name": { "type": "string", - "name": "Variable to pass" + "title": "Variable to pass" }, "value_types": { - "name": "Possible value types", + "title": "Possible value types", "type": "array", "items": { "enum": [ @@ -182,7 +182,7 @@ "const": "const" }, "value_type": { - "name": "Constant type", + "title": "Constant type", "type": "string", "enum": [ "Integer", @@ -190,7 +190,7 @@ ] }, "value": { - "name": "Constant value", + "title": "Constant value", "type": [ "number", "null" @@ -212,14 +212,14 @@ }, "name": { "type": "string", - "name": "Variable to match" + "title": "Variable to match" }, "match": { "type": "array", "additionalItems": false, "items": { "type": "object", - "name": "Match arm", + "title": "Match arm", "description": "", "additionalProperties": false, "required": [ @@ -229,7 +229,7 @@ "properties": { "value": { "type": "integer", - "name": "Arm value", + "title": "Arm value", "description": "" }, "stack": { @@ -257,22 +257,188 @@ "const": "array" }, "name": { - "name": "Variable name", + "title": "Variable name", "type": "string" }, "length_var": { - "name": "Variable which contains array length", + "title": "Variable which contains array length", "type": "string" }, "array_entry": { "allOf": [{ "$ref": "#/definitions/stack" }], - "name": "Array single entry definition", + "title": "Array single entry definition", "description": "Array is a structure like `x1 y1 z1 x2 y2 z2 ... x_n y_n z_n n` which contains `n` entries of `x_i y_i z_i`. This property defines the structure of a single entry." } } } ] }, + "continuation": { + "title": "Continuation", + "description": "Description of a continuation with static savelist", + "oneOf": [ + { + "type": "object", + "additionalProperties": false, + "required": [ + "type" + ], + "properties": { + "type": { "const": "cc" }, + "save": { "$ref": "#/definitions/savelist" } + } + }, + { + "type": "object", + "additionalProperties": false, + "required": [ + "type", + "var_name" + ], + "properties": { + "type": { "const": "variable" }, + "var_name": { "type": "string", "title": "Continuation variable name" }, + "save": { "$ref": "#/definitions/savelist" } + } + }, + { + "type": "object", + "additionalProperties": false, + "required": [ + "type", + "index" + ], + "properties": { + "type": { "const": "register" }, + "index": { "type": "integer", "title": "Register number (0-3)" }, + "save": { "$ref": "#/definitions/savelist" } + } + }, + { + "type": "object", + "additionalProperties": false, + "required": [ + "type", + "name", + "args" + ], + "properties": { + "type": { "const": "special" }, + "name": { "const": "until" }, + "args": { + "type": "object", + "required": ["body", "after"], + "additionalProperties": false, + "properties": { + "body": { "$ref": "#/definitions/continuation" }, + "after": { "$ref": "#/definitions/continuation" } + } + } + } + }, + { + "type": "object", + "additionalProperties": false, + "required": [ + "type", + "name", + "args" + ], + "properties": { + "type": { "const": "special" }, + "name": { "const": "while" }, + "args": { + "type": "object", + "required": ["cond", "body", "after"], + "additionalProperties": false, + "properties": { + "cond": { "$ref": "#/definitions/continuation" }, + "body": { "$ref": "#/definitions/continuation" }, + "after": { "$ref": "#/definitions/continuation" } + } + } + } + }, + { + "type": "object", + "additionalProperties": false, + "required": [ + "type", + "name", + "args" + ], + "properties": { + "type": { "const": "special" }, + "name": { "const": "again" }, + "args": { + "type": "object", + "required": ["body"], + "additionalProperties": false, + "properties": { + "body": { "$ref": "#/definitions/continuation" } + } + } + } + }, + { + "type": "object", + "additionalProperties": false, + "required": [ + "type", + "name", + "args" + ], + "properties": { + "type": { "const": "special" }, + "name": { "const": "repeat" }, + "args": { + "type": "object", + "required": ["count", "body", "after"], + "additionalProperties": false, + "properties": { + "count": { "type": "string", "title": "Variable name" }, + "body": { "$ref": "#/definitions/continuation" }, + "after": { "$ref": "#/definitions/continuation" } + } + } + } + }, + { + "type": "object", + "additionalProperties": false, + "required": [ + "type", + "name", + "args" + ], + "properties": { + "type": { "const": "special" }, + "name": { "const": "pushint" }, + "args": { + "type": "object", + "required": ["next", "value"], + "additionalProperties": false, + "properties": { + "value": { "type": "integer", "title": "Integer to push to stack" }, + "next": { "$ref": "#/definitions/continuation" } + } + } + } + } + ] + }, + "savelist": { + "title": "Continuation savelist", + "description": "Values of saved control flow registers c0-c3", + "type": "object", + "additionalProperties": false, + "properties": { + "c0": { "$ref": "#/definitions/continuation" }, + "c1": { "$ref": "#/definitions/continuation" }, + "c2": { "$ref": "#/definitions/continuation" }, + "c3": { "$ref": "#/definitions/continuation" } + } + }, "instruction": { "type": "object", "additionalProperties": false, @@ -526,6 +692,28 @@ "description": "Outgoing values constraints. Output is unconstrained if absent." } } + }, + "control_flow": { + "type": "object", + "title": "Control flow of instruction", + "description": "Information related to current cc modification by instruction", + "additionalProperties": false, + "properties": { + "branches": { + "type": "array", + "title": "Possible branches of an instruction", + "description": "Array of current continuation possible values after current instruction execution", + "default": [], + "items": { "$ref": "#/definitions/continuation" }, + "additionalItems": false + }, + "nobranch": { + "type": "boolean", + "default": false, + "title": "No branch possibility", + "description": "Can this instruction not perform any of specified branches in certain cases (do not modify cc)?" + } + } } }, "required": [