• Home
  • Line#
  • Scopes#
  • Navigate#
  • Raw
  • Download
1# Copyright (c) 2021-2022 Huawei Device Co., Ltd.
2# Licensed under the Apache License, Version 2.0 (the "License");
3# you may not use this file except in compliance with the License.
4# You may obtain a copy of the License at
5#
6# http://www.apache.org/licenses/LICENSE-2.0
7#
8# Unless required by applicable law or agreed to in writing, software
9# distributed under the License is distributed on an "AS IS" BASIS,
10# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
11# See the License for the specific language governing permissions and
12# limitations under the License.
13
14---
15
16chapters:
17  - name: General design
18    text: >
19      VM is register based with dedicated accumulator register, which serves as an implicit operand to instructions.
20
21  - name: Registers
22    text: >
23      Registers are wide enough to hold a single reference when working with objects.
24      When used for primitive types, registers width should be considered as 64 bits.
25      When used for object types, registers should be considered wide enough to hold a reference to an object.
26      The scope of a register is function frame (also known as activation record). If instruction defines not all 64
27      bits of a register, undefined bits shall not be accessed in verified code.
28      Register field width in instruction encoding could be 4 (16 addressable registers), 8 (256 registers) or
29      16 (65536 registers) bits.
30
31  - name: Accumulator
32    text: >
33      Accumulator is a special register which is implicitly used by instructions as a source and/or destination operand.
34      The main goal of using accumulator is to improve encoding density without losing much in performance. Therefore,
35      the general intuition regarding accumulator usage is to utilize the accumulator as much as possible taking it as
36      a source from previous instruction result and passing it to the next instruction in its destination operand.
37      Moreover, when instruction has more than one source operands, the value which lives shorter should be passed
38      through the accumulator. If it is profitable however, variations of instructions that don't write into the
39      accumulator are also introduced. For example, moving arguments for `call.range` instruction may be done by
40      register-to-register moves.
41
42  - name: Calling sequence
43    text: >
44      On execution of a call bytecode a new function frame is created. All necessary arguments are copied from the
45      caller frame onto the top of the callee frame such as the last argument is placed in the register with the largest
46      index and the first argument is placed into the register with the index equal to the size of frame subtracted by
47      the number of arguments. Accumulator value is considered as undefined and shall not be read in verified bytecode.
48      On return, callee frame is destroyed. If function return value is non-void, it is passed to caller via
49      accumulator. Otherwise accumulator content in caller frame is considered as undefined and shall not
50      be read in verified bytecode.
51
52  - name: Supported primitive types
53    text: |
54      VM support operations on registers with i32 and i64 integral values. However, 8-bit and 16-bit integral values
55      can be loaded/stored into records and arrays with corresponding bytecodes. In that case, VM will extend/truncate
56      value to match storage size with i32. Similarly, passing an 8-bit or 16-bit value to a function can be emulated by
57      passing a value, which is zero or sign-extended to i32.
58      VM support operations on registers with f32 and f64 values, which corresponds to IEEE-754 single and double precision
59      floating-point represenation.
60      Primitive data type of a register is not tracked by VM and is interpreted by separate bytecodes.
61      Integral values are not inherently signed or unsigned, signedness is interpreted by bytecodes as well.
62      If bytecode treats register value as signed integer, it uses two's complement representation.
63      To denote that bytecode treats register values as unsigned integer, u32/u64 notation is used.
64      For moves, loads and stores it is not always possible to denote a type of result, because it depends on type
65      of source object. In that case, bNN notation is used, where NN is bit size of result. Therefore, for example,
66      b64 is a union of f64 and i64.
67
68      ### Floating-point literals
69
70      Decimal floating-point literals can have the following parts:
71
72      - Sign ("`+`" or "`-`")
73      - Whole number part
74      - Decimal point
75      - Fractional part
76      - Exponent indicator ("`e`")
77      - Exponent sign
78      - Exponent
79
80      Decimal floating-point literals must have at least one digit and either decimal point or exponent part.
81
82      Special values:
83
84      - Positive zero (+0.0, hexadecimal representation is `0x0000000000000000`)
85      - Negative zero (-0.0, hexadecimal representation is `0x8000000000000000`)
86      - Minimal positive value (4.9E-324, hexadecimal representation is `0x0000000000000001`)
87      - Maximal negative value (-4.9E-324, hexadecimal representation is `0x8000000000000001`)
88      - Maximal positive value (1.7976931348623157e308, hexadecimal representation is `0x7fefffffffffffff`)
89      - Minimal negative value (-1.7976931348623157e308, hexadecimal representation is `0xffefffffffffffff`)
90      - Positive infinity (hexadecimal representation is `0x7ff0000000000000`)
91      - Negative infinity (hexadecimal representation is `0xfff0000000000000`)
92      - Not a number - set of all NaN values (one of hexadecimal representations is `0x7ff8000000000000`)
93
94  - name: Language-dependent types
95    text: >
96      Panda VM supports type hierarchies according to the language it executes. That way, creation (or loading
97      from constant pool) of strings, arrays, exception objects results into an object of type native to language,
98      including inheritance relations.
99
100  - name: Dynamically-typed languages support
101    text: >
102      Panda VM supports languages with dynamic types. It represents dynamic values through special 'any' values,
103      which wraps a value itself (both primitive and objects) and corresponding type info. VM tracks type of registers,
104      that hold 'any' value, whether they are primitive or not. Virtual registers and accumulator are wide enough
105      to hold 'any' value. When VM executes code inside dynamically-typed language context, regular static instructions
106      also may be used.
107
108# File format and ISA versioning
109min_version: 0.0.0.5
110version: 0.0.0.5
111
112properties:
113  - tag: type_id
114    description: Use an id which resolves into a type constant.
115  - tag: method_id
116    description: Use an id which resolves into a method constant.
117  - tag: string_id
118    description: Use an id which resolves into a string constant.
119  - tag: literalarray_id
120    description: Use an id which resolves into a constant literalarray.
121  - tag: field_id
122    description: Use an id which resolves into a field reference.
123  - tag: short_long_range
124    description: Instruction is used to pass arguments, exists in short, long and range forms.
125  - tag: call
126    description: Pass control to the callee method.
127  - tag: call_virt
128    description: Pass control to the callee method via virtual call.
129  - tag: return
130    description: Pass control to the caller method.
131  - tag: suspend
132    description: Suspend current method and pass control to the caller one.
133  - tag: jump
134    description: Pass control to another bytecode in a current method.
135  - tag: conditional
136    description: Operate based on computed condition, otherwise is no operation.
137  - tag: float
138    description: Perform floating point operation.
139  - tag: dynamic
140    description: Operates on 'any' values.
141  - tag: maybe_dynamic
142    description: May operate on 'any' values depending on language context.
143  - tag: language_type
144    description: Creates objects of type depending on language context.
145  - tag: initialize_type
146    description: May initialize type instance during execution.
147  - tag: init_obj
148    description: Calls the object initialization function.
149exceptions:
150  - tag: x_none
151    description: Bytecode doesn't throw exceptions.
152  - tag: x_null
153    description: Bytecode throws NullPointerException in case of null reference as a source.
154  - tag: x_bounds
155    description: Bytecode throws ArrayIndexOutOfBoundsException if index is out of bounds of an array.
156  - tag: x_negsize
157    description: Bytecode throws NegativeArraySizeException if index is less than zero.
158  - tag: x_store
159    description: Bytecode throws ArrayStoreException if element isn't instance of array's element type.
160  - tag: x_abstract
161    description: Bytecode throws AbstractMethodError if resolved method has no implementation.
162  - tag: x_arith
163    description: Bytecode throws ArithmeticException if the divisor is 0.
164  - tag: x_cast
165    description: Bytecode throws ClassCastException if type cast failed.
166  - tag: x_classdef
167    description: Bytecode throws NoClassDefFoundError if type cast failed.
168  - tag: x_oom
169    description: Bytecode throws OutOfMemoryError if failed to allocate object.
170  - tag: x_init
171    description: Bytecode throws ExceptionInInitializerError if unexpected exception occurred in a static initializer.
172  - tag: x_call
173    description: Bytecode may throw an error if an exception occures in the called bytecode.
174  - tag: x_throw
175    description: Bytecode's primary role is to throw provided exception object.
176  - tag: x_link
177    description: Bytecode may throw NoClassDefFoundError if failed to resolve id.
178verification:
179  - tag: none
180    description: Instruction is always valid.
181  - tag: v1_array
182    description: First operand contains a reference to an array.
183  - tag: v1_object
184    description: First operand contains a reference to an object (other than array).
185  - tag: v1_array_type
186    # TODO: specify
187    description: First operand contains a reference to an array of elements of type corresponding to bytecode.
188  - tag: v1_i32
189    description: First operand contains a value of i32 type.
190  - tag: v1_type
191    description: First operand contains a value of type corresponding to bytecode.
192  - tag: v1_obj_or_null
193    description: First operand contains a reference to an object or null.
194  - tag: v2_i32
195    description: Second operand contains a value of i32 type.
196  - tag: v2_object
197    description: Second operand contains a reference to an object (other than array).
198  - tag: v2_type
199    description: Second operand contains a value of type corresponding to bytecode.
200  - tag: acc_i32
201    description: Accumulator contains a value of i32 type.
202  - tag: acc_type
203    description: Accumulator contains a value of type corresponding to bytecode.  # TODO: specify
204  - tag: acc_return_type
205    # TODO: specify, including assignment compatibility (see Java 'areturn')
206    description: Accumulator type is compatible with method return type.
207  - tag: v1_throw_type
208    description: First operand contains a reference to an instance of class Throwable or of a subclass of Throwable.
209  - tag: acc_obj_or_null
210    description: Accumulator contains a reference to an object or null.
211  - tag: type_id_array
212    description: Type_id operand must correspond to an array type.
213  - tag: type_id_object
214    description: Type_id operand must correspond to an object type (other than array).
215  - tag: type_id_any_object
216    description: Type_id operand must correspond to any object type.
217  - tag: type_id_class
218    description: Type_id operand must correspond to a Class type.
219  - tag: method_id_static
220    description: Method_id must resolve to a static method or into initializer for a type other than one-dimensional array.
221  - tag: method_id_non_static
222    description: Method_id must resolve to a non-static method.
223  - tag: method_id_non_abstract
224    description: Method_id must resolve to a method that has implementation.
225  - tag: method_id_accessible
226    description: Method_id must resolve to a method which is accessible.
227  - tag: constant_string_id
228    description: Id must resolve into a constant-pool string.
229  - tag: constant_literalarray_id
230    description: Id must resolve into a constant literalarray.
231  - tag: compatible_arguments
232    description: Arguments provided to a method must be of compatible types.  # TODO: specify compatibility
233  - tag: method_init_obj
234    description: Method_id must resolve into initializer for a type other than one-dimensional array.
235  - tag: branch_target
236    description: Branch target should point to a beginning of an instruction of the same method.
237  - tag: field_id_non_static
238    description: Field_id must resolve to a non-static object field.
239  - tag: field_id_static
240    description: Field_id must resolve to a static field.
241  - tag: field_id_size
242    description: Field_id must resolve to a field of size corresponding to bytecode.
243  - tag: valid_in_dynamic_context
244    description: Instruction valid only for dynamically-typed language context.
245
246prefixes:
247  - name: bit
248    description: Bit operations.
249    opcode_idx: 0xef
250  - name: unsigned
251    description: Unsigned operations.
252    opcode_idx: 0xee
253  - name: cast
254    description: Cast operations.
255    opcode_idx: 0xed
256  - name: f32
257    description: IEEE-754 single precision floating-point operations.
258    opcode_idx: 0xec
259
260# Define elements, that allowed to be used in a profile description.
261profiles_schema: {}
262
263# Profiles should be specified in an ISA description for a specific language.
264profiles: []
265
266namespaces:
267  - namespace: core
268    used_instructions: []
269
270groups:
271  - title: No operation
272    description: Perform an operation without behavior.
273    exceptions:
274      - x_none
275    verification:
276      - none
277    pseudo: |
278      skip
279    instructions:
280      - sig: nop
281        acc: none
282        format: [op_none]
283        opcode_idx: [0x0]
284
285  - title: Move register-to-register
286    description: Move values between registers.
287    exceptions:
288      - x_none
289    verification:
290      - v2_type
291    pseudo: |
292      vd = vs
293    instructions:
294      - sig: mov v1:out:b32, v2:in:b32
295        acc: none
296        format: [op_v1_4_v2_4, op_v1_8_v2_8, op_v1_16_v2_16]
297        opcode_idx: [0x1, 0x2, 0x3]
298      - sig: mov.64 v1:out:b64, v2:in:b64
299        acc: none
300        format: [op_v1_4_v2_4, op_v1_16_v2_16]
301        opcode_idx: [0x4, 0x5]
302      - sig: mov.obj v1:out:ref, v2:in:ref
303        acc: none
304        format: [op_v1_4_v2_4, op_v1_8_v2_8, op_v1_16_v2_16]
305        opcode_idx: [0x6, 0x7, 0x8]
306
307  - title: Move immediate-to-register
308    description: >
309      Move integer immediate into a register. For short formats immediate is sign extended to operand size.
310    exceptions:
311      - x_none
312    verification:
313      - none
314    pseudo: >
315      vd = imm
316    instructions:
317      - sig: movi v:out:i32, imm:i32
318        acc: none
319        format: [op_v_4_imm_4, op_v_8_imm_8, op_v_8_imm_16, op_v_8_imm_32]
320        opcode_idx: [0x9, 0xa, 0xb, 0xc]
321      - sig: movi.64 v:out:i64, imm:i64
322        acc: none
323        format: [op_v_8_imm_64]
324        opcode_idx: [0xd]
325      - sig: fmovi v:out:f32, imm:f32
326        acc: none
327        prefix: f32
328        format: [pref_op_v_8_imm_32]
329        opcode_idx: [0x0]
330        properties: [float]
331      - sig: fmovi.64 v:out:f64, imm:f64
332        acc: none
333        format: [op_v_8_imm_64]
334        opcode_idx: [0xe]
335        properties: [float]
336
337  - title: Move null reference into register
338    description: Move null reference into a register.
339    exceptions:
340      - x_none
341    verification:
342      - none
343    pseudo: >
344      vd = null
345    instructions:
346      - sig: mov.null v:out:ref
347        acc: none
348        format: [op_v_8]
349        opcode_idx: [0xf]
350
351  - title: Load accumulator from register
352    description: Moves register content into an accumulator.
353    exceptions:
354      - x_none
355    verification:
356      - v1_type
357    pseudo: |
358      acc = vs
359    instructions:
360      - sig: lda v:in:b32
361        acc: out:b32
362        format: [op_v_8]
363        opcode_idx: [0x10]
364      - sig: lda.64 v:in:b64
365        acc: out:b64
366        format: [op_v_8]
367        opcode_idx: [0x11]
368      - sig: lda.obj v:in:ref
369        acc: out:ref
370        format: [op_v_8]
371        opcode_idx: [0x12]
372
373  - title: Load accumulator from immediate
374    description: >
375      Load immediate into accumulator. For short formats immediate is sign extended to operand size.
376    exceptions:
377      - x_none
378    verification:
379      - none
380    pseudo: |
381      acc = imm
382    instructions:
383      - sig: ldai imm:i32
384        acc: out:i32
385        format: [op_imm_8, op_imm_16, op_imm_32]
386        opcode_idx: [0x13, 0x14, 0x15]
387      - sig: ldai.64 imm:i64
388        acc: out:i64
389        format: [op_imm_64]
390        opcode_idx: [0x16]
391      - sig: fldai imm:f32
392        acc: out:f32
393        prefix: f32
394        format: [pref_op_imm_32]
395        opcode_idx: [0x1]
396        properties: [float]
397      - sig: fldai.64 imm:f64
398        acc: out:f64
399        format: [op_imm_64]
400        opcode_idx: [0x17]
401        properties: [float]
402
403  - title: Load accumulator from string constant pool
404    description: >
405      Load string specified by id into accumulator. In dynamically-typed language context
406      load string as 'any' value.
407    properties:
408      - string_id
409      - language_type
410      - maybe_dynamic
411    exceptions:
412      - x_oom
413    verification:
414      - constant_string_id
415    pseudo: |
416      acc = load(id)
417    instructions:
418      - sig: lda.str string_id
419        acc: out:ref
420        format: [op_id_32]
421        opcode_idx: [0x18]
422
423  - title: Create and initialize new constant array
424    description: >
425      Create a new single-dimensional constant literal array and put a reference to it into register.
426    properties:
427      - literalarray_id
428    exceptions:
429      - x_oom
430    verification:
431      - constant_literalarray_id
432    pseudo: |
433      arr = load(id)
434      if arr == nullptr then
435        throw OutOfMemoryError
436      end
437      v = arr
438    instructions:
439      - sig: lda.const v:out:ref, literalarray_id
440        acc: none
441        format: [op_v_8_id_16]
442        opcode_idx: [0x19]
443
444  - title: Load accumulator from type constant pool
445    description: Load type specified by id into accumulator.
446    properties:
447      - type_id
448      - language_type
449    exceptions:
450      - x_link
451    verification:
452      - type_id_class
453    pseudo: |
454      type = load(id)
455      if type == nullptr then
456        throw NoClassDefFoundError
457      end
458      acc = type
459    instructions:
460      - sig: lda.type type_id
461        acc: out:ref
462        format: [op_id_16]
463        opcode_idx: [0x1a]
464
465  - title: Load null reference into accumulator
466    description: Load null reference into accumulator.
467    exceptions:
468      - x_none
469    verification:
470      - none
471    pseudo: |
472      acc = null
473    instructions:
474      - sig: lda.null
475        acc: out:ref
476        format: [op_none]
477        opcode_idx: [0x1b]
478
479  - title: Store accumulator
480    description: Moves accumulator content into a register.
481    exceptions:
482      - x_none
483    verification:
484      - acc_type
485    pseudo: |
486      vd = acc
487    instructions:
488      - sig: sta v:out:b32
489        acc: in:b32
490        format: [op_v_8]
491        opcode_idx: [0x1c]
492      - sig: sta.64 v:out:b64
493        acc: in:b64
494        format: [op_v_8]
495        opcode_idx: [0x1d]
496      - sig: sta.obj v:out:ref
497        acc: in:ref
498        format: [op_v_8]
499        opcode_idx: [0x1e]
500
501  - title: Integer comparison
502    description: Perform specified signed or unsigned integer comparison between register and accumulator.
503    exceptions:
504      - x_none
505    verification:
506      - acc_type
507      - v1_type
508    pseudo: |
509        if acc < vs then
510          acc = -1
511        else if acc == vs then
512          acc = 0
513        else
514          acc = 1
515        end
516    instructions:
517      - sig: cmp.64 v:in:i64
518        acc: inout:i64->i32
519        format: [op_v_8]
520        opcode_idx: [0x1f]
521      - sig: ucmp v:in:u32
522        acc: inout:u32->i32
523        prefix: unsigned
524        format: [pref_op_v_8]
525        opcode_idx: [0x0]
526      - sig: ucmp.64 v:in:u64
527        acc: inout:u64->i32
528        prefix: unsigned
529        format: [pref_op_v_8]
530        opcode_idx: [0x1]
531
532  - title: Floating-point comparison
533    description: Perform specified floating point comparison between register and accumulator.
534    properties:
535      - float
536    exceptions:
537      - x_none
538    verification:
539      - acc_type
540      - v1_type
541    pseudo: |
542      if isnan(acc) or isnan(vs) then
543        switch (op)
544        case fcmpg:
545        case fcmpg.64:
546          acc = 1
547        case fcmpl:
548        case fcmpl.64:
549          acc = -1
550      else
551        if acc < vs then
552          acc = -1
553        else if acc == vs then
554          acc = 0
555        else
556          acc = 1
557        end
558      end
559    instructions:
560      - sig: fcmpl v:in:f32
561        acc: inout:f32->i32
562        prefix: f32
563        format: [pref_op_v_8]
564        opcode_idx: [0x2]
565      - sig: fcmpl.64 v:in:f64
566        acc: inout:f64->i32
567        format: [op_v_8]
568        opcode_idx: [0x20]
569      - sig: fcmpg v:in:f32
570        acc: inout:f32->i32
571        prefix: f32
572        format: [pref_op_v_8]
573        opcode_idx: [0x3]
574      - sig: fcmpg.64 v:in:f64
575        acc: inout:f64->i32
576        format: [op_v_8]
577        opcode_idx: [0x21]
578
579  - title: Unconditional jump
580    description: >
581      Unconditionally transfer execution to an instruction at offset bytes from the beginning of the current
582      instruction. Offset is sign extended to the size of instruction address.
583    properties:
584      - jump
585    exceptions:
586      - x_none
587    verification:
588      - branch_target
589    pseudo: |
590      pc += imm
591    instructions:
592      - sig: jmp imm:i32
593        acc: none
594        format: [op_imm_8, op_imm_16, op_imm_32]
595        opcode_idx: [0x22, 0x23, 0x24]
596
597  - title: Conditional object comparison jump
598    description: >
599      Transfer execution to an instruction at offset bytes from the beginning of the current instruction if
600      object references in accumulator and source register compare as specified. Offset is sign extended to the size of
601      instruction address.
602    properties:
603      - jump
604      - conditional
605    exceptions:
606      - x_none
607    verification:
608      - branch_target
609      - acc_obj_or_null
610      - v1_obj_or_null
611    pseudo: |
612      switch (cc)
613      case eq:
614        if acc == vs then
615          pc += imm
616        end
617      case ne:
618        if acc != vs then
619          pc += imm
620      end
621    instructions:
622      - sig: jeq.obj v:in:ref, imm:i32
623        acc: in:ref
624        format: [op_v_8_imm_8, op_v_8_imm_16]
625        opcode_idx: [0x25, 0x26]
626      - sig: jne.obj v:in:ref, imm:i32
627        acc: in:ref
628        format: [op_v_8_imm_8, op_v_8_imm_16]
629        opcode_idx: [0x27, 0x28]
630
631  - title: Conditional compared to null jump
632    description: >
633      Transfer execution to an instruction at offset bytes from the beginning of the current instruction if
634      object reference in accumulator compares with null as specified. Offset is sign extended to the size of
635      instruction address.
636    properties:
637      - jump
638      - conditional
639    exceptions:
640      - x_none
641    verification:
642      - branch_target
643      - acc_obj_or_null
644    pseudo: |
645      switch (cc)
646      case eq:
647        if acc == null then
648          pc += imm
649        end
650      case ne:
651        if acc != null then
652          pc += imm
653      end
654    instructions:
655      - sig: jeqz.obj imm:i32
656        acc: in:ref
657        format: [op_imm_8, op_imm_16]
658        opcode_idx: [0x29, 0x2a]
659      - sig: jnez.obj imm:i32
660        acc: in:ref
661        format: [op_imm_8, op_imm_16]
662        opcode_idx: [0x2b, 0x2c]
663
664  - title: Conditional compared to zero jump
665    description: >
666      Transfer execution to an instruction at offset bytes from the beginning of the current instruction if
667      signed 32-bit integer in accumulator compares with 0 as specified. Offset is sign extended to the size
668      of instruction address.
669    properties:
670      - jump
671      - conditional
672    exceptions:
673      - x_none
674    verification:
675      - branch_target
676      - acc_type
677    pseudo: |
678      switch (cc)
679      case eq:
680        if acc == 0 then
681          pc += imm
682        end
683      case ne:
684        if acc != 0 then
685          pc += imm
686        end
687      case lt:
688        if acc < 0 then
689          pc += imm
690        end
691      case gt:
692        if acc > 0 then
693          pc += imm
694        end
695      case le:
696        if acc <= 0 then
697          pc += imm
698        end
699      case ge:
700        if acc >= 0 then
701          pc += imm
702        end
703    instructions:
704      - sig: jeqz imm:i32
705        acc: in:i32
706        format: [op_imm_8, op_imm_16]
707        opcode_idx: [0x2d, 0x2e]
708      - sig: jnez imm:i32
709        acc: in:i32
710        format: [op_imm_8, op_imm_16]
711        opcode_idx: [0x2f, 0x30]
712      - sig: jltz imm:i32
713        acc: in:i32
714        format: [op_imm_8, op_imm_16]
715        opcode_idx: [0x31, 0x32]
716      - sig: jgtz imm:i32
717        acc: in:i32
718        format: [op_imm_8, op_imm_16]
719        opcode_idx: [0x33, 0x34]
720      - sig: jlez imm:i32
721        acc: in:i32
722        format: [op_imm_8, op_imm_16]
723        opcode_idx: [0x35, 0x36]
724      - sig: jgez imm:i32
725        acc: in:i32
726        format: [op_imm_8, op_imm_16]
727        opcode_idx: [0x37, 0x38]
728
729  - title: Conditional compared to register jump
730    description: >
731      Transfer execution to an instruction at offset bytes from the beginning of the current instruction if signed
732      32-bit integers in accumulator and register compare as specified. Offset is sign extended to the size of
733      instruction address.
734    properties:
735      - jump
736      - conditional
737    exceptions:
738      - x_none
739    verification:
740      - branch_target
741      - acc_type
742      - v1_type
743    pseudo: |
744      diff = signed_cmp(acc, vs)
745      switch (cc)
746      case eq:
747        if diff == 0 then
748          pc += imm
749        end
750      case ne:
751        if diff != 0 then
752          pc += imm
753        end
754      case lt:
755        if diff < 0 then
756          pc += imm
757        end
758      case gt:
759        if diff > 0 then
760          pc += imm
761        end
762      case le:
763        if diff <= 0 then
764          pc += imm
765        end
766      case ge:
767        if diff >= 0 then
768          pc += imm
769        end
770    instructions:
771      - sig: jeq v:in:i32, imm:i32
772        acc: in:i32
773        format: [op_v_8_imm_8, op_v_8_imm_16]
774        opcode_idx: [0x39, 0x3a]
775      - sig: jne v:in:i32, imm:i32
776        acc: in:i32
777        format: [op_v_8_imm_8, op_v_8_imm_16]
778        opcode_idx: [0x3b, 0x3c]
779      - sig: jlt v:in:i32, imm:i32
780        acc: in:i32
781        format: [op_v_8_imm_8, op_v_8_imm_16]
782        opcode_idx: [0x3d, 0x3e]
783      - sig: jgt v:in:i32, imm:i32
784        acc: in:i32
785        format: [op_v_8_imm_8, op_v_8_imm_16]
786        opcode_idx: [0x3f, 0x40]
787      - sig: jle v:in:i32, imm:i32
788        acc: in:i32
789        format: [op_v_8_imm_8, op_v_8_imm_16]
790        opcode_idx: [0x41, 0x42]
791      - sig: jge v:in:i32, imm:i32
792        acc: in:i32
793        format: [op_v_8_imm_8, op_v_8_imm_16]
794        opcode_idx: [0x43, 0x44]
795
796  - title: Floating-point unary
797    description: Perform specified floating-point operation on accumulator
798    properties:
799      - float
800    exceptions:
801      - x_none
802    verification:
803      - acc_type
804    pseudo: |
805      switch (op)
806      case fneg:
807      case fneg.64:
808        acc = -acc
809    instructions:
810      - sig: fneg
811        acc: inout:f32
812        prefix: f32
813        format: [pref_op_none]
814        opcode_idx: [0x4]
815      - sig: fneg.64
816        acc: inout:f64
817        format: [op_none]
818        opcode_idx: [0x45]
819
820  - title: Unary
821    description: Perform specified operation on accumulator
822    exceptions:
823      - x_none
824    verification:
825      - acc_type
826    pseudo: |
827      switch (op)
828      case neg:
829      case neg.64:
830        acc = -acc
831      case not:
832      case not.64:
833        acc = ~acc
834    instructions:
835      - sig: neg
836        acc: inout:i32
837        format: [op_none]
838        opcode_idx: [0x46]
839      - sig: neg.64
840        acc: inout:i64
841        format: [op_none]
842        opcode_idx: [0x47]
843      - sig: not
844        acc: inout:i32
845        prefix: bit
846        format: [pref_op_none]
847        opcode_idx: [0x0]
848      - sig: not.64
849        acc: inout:i64
850        prefix: bit
851        format: [pref_op_none]
852        opcode_idx: [0x1]
853
854  - title: Two address binary operation on accumulator
855    description: Perform specified binary operation on accumulator and register and store result into accumulator
856    exceptions:
857      - x_none
858    verification:
859      - acc_type
860      - v1_type
861    pseudo: |
862      switch (op)
863      case add2:
864        acc = (acc + vs) % 2^32
865      case add2.64:
866        acc = (acc + vs) % 2^64
867      case sub2:
868        acc = (acc - vs) % 2^32
869      case sub2.64:
870        acc = (acc - vs) % 2^64
871      case mul2:
872        acc = (acc * vs) % 2^32
873      case mul2.64:
874        acc = (acc * vs) % 2^64
875      case and2:
876        acc = acc & vs
877      case and2.64:
878        acc = acc & vs
879      case or2:
880        acc = acc | vs
881      case or2.64:
882        acc = acc | vs
883      case xor2:
884        acc = acc ^ vs
885      case xor2.64:
886        acc = acc ^ vs
887      case shl2:
888        acc = (acc << (vs & 0x1f)) % 2^32
889      case shl2.64:
890        acc = (acc << (vs & 0x3f)) % 2^64
891      case shr2:
892        acc = acc >> (vs & 0x1f)
893      case shr2.64:
894        acc = acc >> (vs & 0x3f)
895      case ashr2:
896        acc = (acc < 0) ? ~(~acc >> vs & 0x1f) : acc >> vs & 0x1f
897      case ashr2.64:
898        acc = (acc < 0) ? ~(~acc >> vs & 0x3f) : acc >> vs & 0x3f
899    instructions:
900      - sig: add2 v:in:i32
901        acc: inout:i32
902        format: [op_v_8]
903        opcode_idx: [0x48]
904      - sig: add2.64 v:in:i64
905        acc: inout:i64
906        format: [op_v_8]
907        opcode_idx: [0x49]
908      - sig: sub2 v:in:i32
909        acc: inout:i32
910        format: [op_v_8]
911        opcode_idx: [0x4a]
912      - sig: sub2.64 v:in:i64
913        acc: inout:i64
914        format: [op_v_8]
915        opcode_idx: [0x4b]
916      - sig: mul2 v:in:i32
917        acc: inout:i32
918        format: [op_v_8]
919        opcode_idx: [0x4c]
920      - sig: mul2.64 v:in:i64
921        acc: inout:i64
922        format: [op_v_8]
923        opcode_idx: [0x4d]
924      - sig: and2 v:in:i32
925        acc: inout:i32
926        prefix: bit
927        format: [pref_op_v_8]
928        opcode_idx: [0x2]
929      - sig: and2.64 v:in:i64
930        acc: inout:i64
931        prefix: bit
932        format: [pref_op_v_8]
933        opcode_idx: [0x3]
934      - sig: or2 v:in:i32
935        acc: inout:i32
936        prefix: bit
937        format: [pref_op_v_8]
938        opcode_idx: [0x4]
939      - sig: or2.64 v:in:i64
940        acc: inout:i64
941        prefix: bit
942        format: [pref_op_v_8]
943        opcode_idx: [0x5]
944      - sig: xor2 v:in:i32
945        acc: inout:i32
946        prefix: bit
947        format: [pref_op_v_8]
948        opcode_idx: [0x6]
949      - sig: xor2.64 v:in:i64
950        acc: inout:i64
951        prefix: bit
952        format: [pref_op_v_8]
953        opcode_idx: [0x7]
954      - sig: shl2 v:in:i32
955        acc: inout:i32
956        prefix: bit
957        format: [pref_op_v_8]
958        opcode_idx: [0x8]
959      - sig: shl2.64 v:in:i64
960        acc: inout:i64
961        prefix: bit
962        format: [pref_op_v_8]
963        opcode_idx: [0x9]
964      - sig: shr2 v:in:i32
965        acc: inout:i32
966        prefix: bit
967        format: [pref_op_v_8]
968        opcode_idx: [0xa]
969      - sig: shr2.64 v:in:i64
970        acc: inout:i64
971        prefix: bit
972        format: [pref_op_v_8]
973        opcode_idx: [0xb]
974      - sig: ashr2 v:in:i32
975        acc: inout:i32
976        prefix: bit
977        format: [pref_op_v_8]
978        opcode_idx: [0xc]
979      - sig: ashr2.64 v:in:i64
980        acc: inout:i64
981        prefix: bit
982        format: [pref_op_v_8]
983        opcode_idx: [0xd]
984
985  - title: Two address binary operation on accumulator with result in register
986    description: Perform specified binary operation on accumulator and register and store result into register
987    exceptions:
988      - x_none
989    verification:
990      - acc_type
991      - v1_type
992    pseudo: |
993      switch (op)
994      case add2:
995        vd = (acc + vs) % 2^32
996      case add2.64:
997        vd = (acc + vs) % 2^64
998      case sub2:
999        vd = (acc - vs) % 2^32
1000      case sub2.64:
1001        vd = (acc - vs) % 2^64
1002      case mul2:
1003        vd = (acc * vs) % 2^32
1004      case mul2.64:
1005        acc = (acc * vs) % 2^64
1006      case and2:
1007        vd = acc & vs
1008      case and2.64:
1009        vd = acc & vs
1010      case or2:
1011        vd = acc | vs
1012      case or2.64:
1013        vd = acc | vs
1014      case xor2:
1015        vd = acc ^ vs
1016      case xor2.64:
1017        vd = acc ^ vs
1018      case shl2:
1019        vd = (acc << (vs & 0x1f)) % 2^32
1020      case shl2.64:
1021        vd = (acc << (vs & 0x3f)) % 2^64
1022      case shr2:
1023        vd = acc >> (vs & 0x1f)
1024      case shr2.64:
1025        vd = acc >> (vs & 0x3f)
1026      case ashr2:
1027        vd = (acc < 0) ? ~(~acc >> vs & 0x1f) : acc >> vs & 0x1f
1028      case ashr2.64:
1029        vd = (acc < 0) ? ~(~acc >> vs & 0x3f) : acc >> vs & 0x3f
1030    instructions:
1031      - sig: add2v v1:out:i32, v2:in:i32
1032        acc: in:i32
1033        format: [op_v1_8_v2_8]
1034      - sig: add2v.64 v1:out:i64, v2:in:i64
1035        acc: in:i64
1036        format: [op_v1_8_v2_8]
1037      - sig: sub2v v1:out:i32, v2:in:i32
1038        acc: in:i32
1039        format: [op_v1_8_v2_8]
1040      - sig: sub2v.64 v1:out:i64, v2:in:i64
1041        acc: in:i64
1042        format: [op_v1_8_v2_8]
1043      - sig: mul2v v1:out:i32, v2:in:i32
1044        acc: in:i32
1045        format: [op_v1_8_v2_8]
1046      - sig: mul2v.64 v1:out:i64, v2:in:i64
1047        acc: in:i64
1048        format: [op_v1_8_v2_8]
1049      - sig: and2v v1:out:i32, v2:in:i32
1050        acc: in:i32
1051        prefix: bit
1052        format: [pref_op_v1_8_v2_8]
1053      - sig: and2v.64 v1:out:i64, v2:in:i64
1054        acc: in:i64
1055        prefix: bit
1056        format: [pref_op_v1_8_v2_8]
1057      - sig: or2v v1:out:i32, v2:in:i32
1058        acc: in:i32
1059        prefix: bit
1060        format: [pref_op_v1_8_v2_8]
1061      - sig: or2v.64 v1:out:i64, v2:in:i64
1062        acc: in:i64
1063        prefix: bit
1064        format: [pref_op_v1_8_v2_8]
1065      - sig: xor2v v1:out:i32, v2:in:i32
1066        acc: in:i32
1067        prefix: bit
1068        format: [pref_op_v1_8_v2_8]
1069      - sig: xor2v.64 v1:out:i64, v2:in:i64
1070        acc: in:i64
1071        prefix: bit
1072        format: [pref_op_v1_8_v2_8]
1073      - sig: shl2v v1:out:i32, v2:in:i32
1074        acc: in:i32
1075        prefix: bit
1076        format: [pref_op_v1_8_v2_8]
1077      - sig: shl2v.64 v1:out:i64, v2:in:i64
1078        acc: in:i64
1079        prefix: bit
1080        format: [pref_op_v1_8_v2_8]
1081      - sig: shr2v v1:out:i32, v2:in:i32
1082        acc: in:i32
1083        prefix: bit
1084        format: [pref_op_v1_8_v2_8]
1085      - sig: shr2v.64 v1:out:i64, v2:in:i64
1086        acc: in:i64
1087        prefix: bit
1088        format: [pref_op_v1_8_v2_8]
1089      - sig: ashr2v v1:out:i32, v2:in:i32
1090        acc: in:i32
1091        prefix: bit
1092        format: [pref_op_v1_8_v2_8]
1093      - sig: ashr2v.64 v1:out:i64, v2:in:i64
1094        acc: in:i64
1095        prefix: bit
1096        format: [pref_op_v1_8_v2_8]
1097
1098  - title: Two address floating-point binary operation on accumulator
1099    description: |
1100      Perform specified floating-point binary operation on accumulator and register and store result into accumulator.
1101      The results of instructions correspond IEEE-754 arithmetic rules.
1102
1103      - Any operation with NaN results to NaN value.
1104      - The sum of opposite infinities or the difference of the same sign infinities is NaN.
1105      - Division is NaN if Infinity is divided by Infinity.
1106      - Division is NaN if zero is divided by zero.
1107      - Multiplication is NaN if zero is multiplied by infinity.
1108      - The sign of division or multiplication result is positive if both values have the same sign, negative if the values have different sign.
1109      - Division is infinity if any non zero value is divided by zero.
1110      - Multiplication is infinity if any non zero value is multiplied by infinity.
1111      - The sum of two infinities of the same sign or the difference of two infinities of opposite sign is infinity. The sign of result matches the sign of accumulator value.
1112      - The sum or the difference of infinity and any finite value is infinity. The sign of result matches the sign of infinity.
1113      - The sum or the difference of zeros is zero. Exceptions are the sum of two negative zeros and the difference of negative and positive zero - the result is negative zero.
1114
1115    properties:
1116      - float
1117    exceptions:
1118      - x_none
1119    verification:
1120      - acc_type
1121      - v1_type
1122    pseudo: |
1123      switch (op)
1124      case fadd2:
1125      case fadd2.64:
1126        acc = acc + vs
1127      case fsub2:
1128      case fsub2.64:
1129        acc = acc - vs
1130      case fmul2:
1131      case fmul2.64:
1132        acc = acc * vs
1133      case fdiv2:
1134      case fdiv2.64:
1135        acc = acc / vs
1136      case fmod2:
1137      case fmod2.64:
1138        acc = acc % vs
1139    instructions:
1140      - sig: fadd2 v:in:f32
1141        acc: inout:f32
1142        prefix: f32
1143        format: [pref_op_v_8]
1144        opcode_idx: [0x5]
1145      - sig: fadd2.64 v:in:f64
1146        acc: inout:f64
1147        format: [op_v_8]
1148        opcode_idx: [0x4e]
1149      - sig: fsub2 v:in:f32
1150        acc: inout:f32
1151        prefix: f32
1152        format: [pref_op_v_8]
1153        opcode_idx: [0x6]
1154      - sig: fsub2.64 v:in:f64
1155        acc: inout:f64
1156        format: [op_v_8]
1157        opcode_idx: [0x4f]
1158      - sig: fmul2 v:in:f32
1159        acc: inout:f32
1160        prefix: f32
1161        format: [pref_op_v_8]
1162        opcode_idx: [0x7]
1163      - sig: fmul2.64 v:in:f64
1164        acc: inout:f64
1165        format: [op_v_8]
1166        opcode_idx: [0x50]
1167      - sig: fdiv2 v:in:f32
1168        acc: inout:f32
1169        prefix: f32
1170        format: [pref_op_v_8]
1171        opcode_idx: [0x8]
1172      - sig: fdiv2.64 v:in:f64
1173        acc: inout:f64
1174        format: [op_v_8]
1175        opcode_idx: [0x51]
1176      - sig: fmod2 v:in:f32
1177        acc: inout:f32
1178        prefix: f32
1179        format: [pref_op_v_8]
1180        opcode_idx: [0x9]
1181      - sig: fmod2.64 v:in:f64
1182        acc: inout:f64
1183        format: [op_v_8]
1184        opcode_idx: [0x52]
1185
1186  - title: Two address floating-point binary operation on accumulator with result in register
1187    description: |
1188      Perform specified floating-point binary operation on accumulator and register and store result into register.
1189      The results of instructions correspond IEEE-754 arithmetic rules.
1190
1191      - Any operation with NaN results to NaN value.
1192      - The sum of opposite infinities or the difference of the same sign infinities is NaN.
1193      - Division is NaN if Infinity is divided by Infinity.
1194      - Division is NaN if zero is divided by zero.
1195      - Multiplication is NaN if zero is multiplied by infinity.
1196      - The sign of division or multiplication result is positive if both values have the same sign, negative if the values have different sign.
1197      - Division is infinity if any non zero value is divided by zero.
1198      - Multiplication is infinity if any non zero value is multiplied by infinity.
1199      - The sum of two infinities of the same sign or the difference of two infinities of opposite sign is infinity. The sign of result matches the sign of accumulator value.
1200      - The sum or the difference of infinity and any finite value is infinity. The sign of result matches the sign of infinity.
1201      - The sum or the difference of zeros is zero. Exceptions are the sum of two negative zeros and the difference of negative and positive zero - the result is negative zero.
1202
1203    properties:
1204      - float
1205    exceptions:
1206      - x_none
1207    verification:
1208      - acc_type
1209      - v1_type
1210    pseudo: |
1211      switch (op)
1212      case fadd2:
1213      case fadd2.64:
1214        vd = acc + vs
1215      case fsub2:
1216      case fsub2.64:
1217        vd = acc - vs
1218      case fmul2:
1219      case fmul2.64:
1220        vd = acc * vs
1221      case fdiv2:
1222      case fdiv2.64:
1223        vd = acc / vs
1224      case fmod2:
1225      case fmod2.64:
1226        vd = acc % vs
1227    instructions:
1228      - sig: fadd2v v1:out:f32, v2:in:f32
1229        acc: in:f32
1230        prefix: f32
1231        format: [pref_op_v1_8_v2_8]
1232      - sig: fadd2v.64 v1:out:f64, v2:in:f64
1233        acc: in:f64
1234        format: [op_v1_8_v2_8]
1235      - sig: fsub2v v1:out:f32, v2:in:f32
1236        acc: in:f32
1237        prefix: f32
1238        format: [pref_op_v1_8_v2_8]
1239      - sig: fsub2v.64 v1:out:f64, v2:in:f64
1240        acc: in:f64
1241        format: [op_v1_8_v2_8]
1242      - sig: fmul2v v1:out:f32, v2:in:f32
1243        acc: in:f32
1244        prefix: f32
1245        format: [pref_op_v1_8_v2_8]
1246      - sig: fmul2v.64 v1:out:f64, v2:in:f64
1247        acc: in:f64
1248        format: [op_v1_8_v2_8]
1249      - sig: fdiv2v v1:out:f32, v2:in:f32
1250        acc: in:f32
1251        prefix: f32
1252        format: [pref_op_v1_8_v2_8]
1253      - sig: fdiv2v.64 v1:out:f64, v2:in:f64
1254        acc: in:f64
1255        format: [op_v1_8_v2_8]
1256      - sig: fmod2v v1:out:f32, v2:in:f32
1257        acc: in:f32
1258        prefix: f32
1259        format: [pref_op_v1_8_v2_8]
1260      - sig: fmod2v.64 v1:out:f64, v2:in:f64
1261        acc: in:f64
1262        format: [op_v1_8_v2_8]
1263
1264  - title: Two address integer division and modulo on accumulator
1265    description: Perform integer division or modulo on accumulator and register and store result into accumulator
1266    exceptions:
1267      - x_arith
1268    verification:
1269      - acc_type
1270      - v1_type
1271    pseudo: |
1272      if vs == 0 then
1273        throw ArithmeticException
1274      end
1275      switch (op)
1276      case div:
1277        if acc == INT32_MIN and vs == -1 then
1278          acc = INT32_MIN
1279        else
1280          acc = acc / vs
1281        end
1282      case div.64:
1283        if acc == INT64_MIN and vs == -1 then
1284          acc = INT64_MIN
1285        else
1286          acc = acc / vs
1287        end
1288      case divu:
1289      case divu.64:
1290        acc = acc / vs
1291      case mod:
1292        if acc == INT32_MIN and vs == -1 then
1293          acc = 0
1294        else
1295          acc = acc % vs
1296        end
1297      case mod.64:
1298        if acc == INT64_MIN and vs == -1 then
1299          acc = 0
1300        else
1301          acc = acc % vs
1302        end
1303      case modu:
1304      case modu.64:
1305        acc = acc % vs
1306    instructions:
1307      - sig: div2 v:in:i32
1308        acc: inout:i32
1309        format: [op_v_8]
1310        opcode_idx: [0x53]
1311      - sig: div2.64 v:in:i64
1312        acc: inout:i64
1313        format: [op_v_8]
1314        opcode_idx: [0x54]
1315      - sig: mod2 v:in:i32
1316        acc: inout:i32
1317        format: [op_v_8]
1318        opcode_idx: [0x55]
1319      - sig: mod2.64 v:in:i64
1320        acc: inout:i64
1321        format: [op_v_8]
1322        opcode_idx: [0x56]
1323      - sig: divu2 v:in:u32
1324        acc: inout:u32
1325        prefix: unsigned
1326        format: [pref_op_v_8]
1327        opcode_idx: [0x2]
1328      - sig: divu2.64 v:in:u64
1329        acc: inout:u64
1330        prefix: unsigned
1331        format: [pref_op_v_8]
1332        opcode_idx: [0x3]
1333      - sig: modu2 v:in:u32
1334        acc: inout:u32
1335        prefix: unsigned
1336        format: [pref_op_v_8]
1337        opcode_idx: [0x4]
1338      - sig: modu2.64 v:in:u64
1339        acc: inout:u64
1340        prefix: unsigned
1341        format: [pref_op_v_8]
1342        opcode_idx: [0x5]
1343
1344  - title: Two address integer division and modulo on accumulator with result in register
1345    description: Perform integer division or modulo on accumulator and register and store result into register
1346    exceptions:
1347      - x_arith
1348    verification:
1349      - acc_type
1350      - v1_type
1351    pseudo: |
1352      if vs == 0 then
1353        throw ArithmeticException
1354      end
1355      switch (op)
1356      case div:
1357        if acc == INT32_MIN and vs == -1 then
1358          vd = INT32_MIN
1359        else
1360          vd = acc / vs
1361        end
1362      case div.64:
1363        if acc == INT64_MIN and vs == -1 then
1364          vd = INT64_MIN
1365        else
1366          vd = acc / vs
1367        end
1368      case divu:
1369      case divu.64:
1370        vd = acc / vs
1371      case mod:
1372        if acc == INT32_MIN and vs == -1 then
1373          vd = 0
1374        else
1375          vd = acc % vs
1376        end
1377      case mod.64:
1378        if acc == INT64_MIN and vs == -1 then
1379          vd = 0
1380        else
1381          vd = acc % vs
1382        end
1383      case modu:
1384      case modu.64:
1385        vd = acc % vs
1386    instructions:
1387      - sig: div2v v1:out:i32, v2:in:i32
1388        acc: in:i32
1389        format: [op_v1_8_v2_8]
1390      - sig: div2v.64 v1:out:i64, v2:in:i64
1391        acc: in:i64
1392        format: [op_v1_8_v2_8]
1393      - sig: mod2v v1:out:i32, v2:in:i32
1394        acc: in:i32
1395        format: [op_v1_8_v2_8]
1396      - sig: mod2v.64 v1:out:i64, v2:in:i64
1397        acc: in:i64
1398        format: [op_v1_8_v2_8]
1399      - sig: divu2v v1:out:u32, v2:in:u32
1400        acc: in:u32
1401        prefix: unsigned
1402        format: [pref_op_v1_8_v2_8]
1403      - sig: divu2v.64 v1:out:u64, v2:in:u64
1404        acc: in:u64
1405        prefix: unsigned
1406        format: [pref_op_v1_8_v2_8]
1407      - sig: modu2v v1:out:u32, v2:in:u32
1408        acc: in:u32
1409        prefix: unsigned
1410        format: [pref_op_v1_8_v2_8]
1411      - sig: modu2v.64 v1:out:u64, v2:in:u64
1412        acc: in:u64
1413        prefix: unsigned
1414        format: [pref_op_v1_8_v2_8]
1415
1416  - title: Two address binary operation with immediate on accumulator
1417    description: >
1418      Perform specified binary operation on accumulator and immediate and store result into accumulator.
1419      Immediate is sign extended to operand size.
1420    exceptions:
1421      - x_none
1422    verification:
1423      - acc_type
1424    pseudo: |
1425      switch (op)
1426      case addi:
1427        acc = (acc + imm) % 2^32
1428      case subi:
1429        acc = (acc - imm) % 2^32
1430      case muli:
1431        acc = (acc * imm) % 2^32
1432      case andi:
1433        acc = acc & imm
1434      case ori:
1435        acc = acc | imm
1436      case xori:
1437        acc = acc ^ imm
1438      case shli:
1439        acc = (acc << (imm & 0x1f)) % 2^32
1440      case shri:
1441        acc = acc >> (imm & 0x1f)
1442      case ashri:
1443        acc = (acc < 0) ? ~(~acc >> imm & 0x1f) : acc >> imm & 0x1f
1444    instructions:
1445      - sig: addi imm:i32
1446        acc: inout:i32
1447        format: [op_imm_8]
1448        opcode_idx: [0x57]
1449      - sig: subi imm:i32
1450        acc: inout:i32
1451        format: [op_imm_8]
1452        opcode_idx: [0x58]
1453      - sig: muli imm:i32
1454        acc: inout:i32
1455        format: [op_imm_8]
1456        opcode_idx: [0x59]
1457      - sig: andi imm:i32
1458        acc: inout:i32
1459        format: [op_imm_32]
1460        opcode_idx: [0x5a]
1461      - sig: ori imm:i32
1462        acc: inout:i32
1463        format: [op_imm_32]
1464        opcode_idx: [0x5b]
1465      - sig: xori imm:i32
1466        acc: inout:i32
1467        prefix: bit
1468        format: [pref_op_imm_32]
1469        opcode_idx: [0xe]
1470      - sig: shli imm:i32
1471        acc: inout:i32
1472        format: [op_imm_8]
1473        opcode_idx: [0x5c]
1474      - sig: shri imm:i32
1475        acc: inout:i32
1476        format: [op_imm_8]
1477        opcode_idx: [0x5d]
1478      - sig: ashri imm:i32
1479        acc: inout:i32
1480        format: [op_imm_8]
1481        opcode_idx: [0x5e]
1482
1483  - title: Two address binary operation with immediate
1484    description: >
1485      Perform specified binary operation and immediate and store result into register.
1486      Immediate is sign extended to operand size.
1487    exceptions:
1488      - x_none
1489    verification:
1490      - v1_type
1491      - v2_type
1492    pseudo: |
1493      switch (op)
1494      case addi:
1495        v1 = (v2 + imm) % 2^32
1496      case subi:
1497        v1 = (v2 - imm) % 2^32
1498      case muli:
1499        v1 = (v2 * imm) % 2^32
1500      case andi:
1501        v1 = v2 & imm
1502      case ori:
1503        v1 = v2 | imm
1504      case xori:
1505        v1 = v2 ^ imm
1506      case shli:
1507        v1 = (v2 << (imm & 0x1f)) % 2^32
1508      case shri:
1509        v1 = v2 >> (imm & 0x1f)
1510      case ashri:
1511        v1 = (v2 < 0) ? ~(~v2 >> imm & 0x1f) : v2 >> imm & 0x1f
1512    instructions:
1513      - sig: addiv v1:out:i32, v2:in:i32, imm:i32
1514        acc: none
1515        format: [op_v1_4_v2_4_imm_8]
1516      - sig: subiv v1:out:i32, v2:in:i32, imm:i32
1517        acc: none
1518        format: [op_v1_4_v2_4_imm_8]
1519      - sig: muliv v1:out:i32, v2:in:i32, imm:i32
1520        acc: none
1521        format: [op_v1_4_v2_4_imm_8]
1522      - sig: andiv v1:out:i32, v2:in:i32, imm:i32
1523        acc: none
1524        format: [op_v1_4_v2_4_imm_32]
1525      - sig: oriv v1:out:i32, v2:in:i32, imm:i32
1526        acc: none
1527        format: [op_v1_4_v2_4_imm_32]
1528      - sig: xoriv v1:out:i32, v2:in:i32, imm:i32
1529        acc: none
1530        prefix: bit
1531        format: [pref_op_v1_4_v2_4_imm_32]
1532      - sig: shliv v1:out:i32, v2:in:i32, imm:i32
1533        acc: none
1534        format: [op_v1_4_v2_4_imm_8]
1535      - sig: shriv v1:out:i32, v2:in:i32, imm:i32
1536        acc: none
1537        format: [op_v1_4_v2_4_imm_8]
1538      - sig: ashriv v1:out:i32, v2:in:i32, imm:i32
1539        acc: none
1540        format: [op_v1_4_v2_4_imm_8]
1541
1542  - title: Two address integer division or modulo with immediate on accumulator
1543    description: >
1544      Perform two address integer division or modulo on accumulator and immediate and store result into accumulator.
1545      Immediate is sign extended to operand size.
1546    exceptions:
1547      - x_arith
1548    verification:
1549      - acc_type
1550    pseudo: |
1551      if imm == 0 then
1552        throw ArithmeticException
1553      end
1554      switch(op)
1555      case divi:
1556        if acc == INT32_MIN and imm == -1 then
1557          acc = INT32_MIN
1558        else
1559          acc = acc / imm
1560        end
1561      case modi:
1562        if acc == INT32_MIN and imm == -1 then
1563          acc = 0
1564        else
1565          acc = acc % imm
1566        end
1567    instructions:
1568      - sig: divi imm:i32
1569        acc: inout:i32
1570        format: [op_imm_8]
1571        opcode_idx: [0x5f]
1572      - sig: modi imm:i32
1573        acc: inout:i32
1574        format: [op_imm_8]
1575        opcode_idx: [0x60]
1576
1577  - title: Two address integer division or modulo with immediate
1578    description: >
1579      Perform two address integer division or modulo and immediate and store result into register.
1580      Immediate is sign extended to operand size.
1581    exceptions:
1582      - x_arith
1583    verification:
1584      - v1_type
1585      - v2_type
1586    pseudo: |
1587      if imm == 0 then
1588        throw ArithmeticException
1589      end
1590      switch(op)
1591      case divi:
1592        if v1 == INT32_MIN and imm == -1 then
1593          v1 = INT32_MIN
1594        else
1595          v1 = v2 / imm
1596        end
1597      case modi:
1598        if v1 == INT32_MIN and imm == -1 then
1599          v1 = 0
1600        else
1601          v1 = v2 % imm
1602        end
1603    instructions:
1604      - sig: diviv v1:out:i32, v2:in:i32, imm:i32
1605        acc: none
1606        format: [op_v1_4_v2_4_imm_8]
1607      - sig: modiv v1:out:i32, v2:in:i32, imm:i32
1608        acc: none
1609        format: [op_v1_4_v2_4_imm_8]
1610
1611  - title: Three address binary operation
1612    description: Perform specified binary operation on two registers and store result into accumulator
1613    exceptions:
1614      - x_none
1615    verification:
1616      - v1_type
1617      - v2_type
1618    pseudo: |
1619      switch (op)
1620      case add:
1621        acc = (vs1 + vs2) % 2^32
1622      case sub:
1623        acc = (vs1 - vs2) % 2^32
1624      case mul:
1625        acc = (vs1 * vs2) % 2^32
1626      case and:
1627        acc = vs1 & vs2
1628      case or:
1629        acc = vs1 | vs2
1630      case xor:
1631        acc = vs1 ^ vs2
1632      case shl:
1633        acc = (vs1 << (vs2 & 0x1f)) % 2^32
1634      case shr:
1635        acc = vs1 >> (vs2 & 0x1f)
1636      case ashr:
1637        acc = (vs1 < 0) ? ~(~vs1 >> vs2 & 0x1f) : vs1 >> vs2 & 0x1f
1638    instructions:
1639      - sig: add v1:in:i32, v2:in:i32
1640        acc: out:i32
1641        format: [op_v1_4_v2_4]
1642        opcode_idx: [0x61]
1643      - sig: sub v1:in:i32, v2:in:i32
1644        acc: out:i32
1645        format: [op_v1_4_v2_4]
1646        opcode_idx: [0x62]
1647      - sig: mul v1:in:i32, v2:in:i32
1648        acc: out:i32
1649        format: [op_v1_4_v2_4]
1650        opcode_idx: [0x63]
1651      - sig: and v1:in:i32, v2:in:i32
1652        acc: out:i32
1653        prefix: bit
1654        format: [pref_op_v1_4_v2_4]
1655        opcode_idx: [0xf]
1656      - sig: or v1:in:i32, v2:in:i32
1657        acc: out:i32
1658        prefix: bit
1659        format: [pref_op_v1_4_v2_4]
1660        opcode_idx: [0x10]
1661      - sig: xor v1:in:i32, v2:in:i32
1662        acc: out:i32
1663        prefix: bit
1664        format: [pref_op_v1_4_v2_4]
1665        opcode_idx: [0x11]
1666      - sig: shl v1:in:i32, v2:in:i32
1667        acc: out:i32
1668        prefix: bit
1669        format: [pref_op_v1_4_v2_4]
1670        opcode_idx: [0x12]
1671      - sig: shr v1:in:i32, v2:in:i32
1672        acc: out:i32
1673        prefix: bit
1674        format: [pref_op_v1_4_v2_4]
1675        opcode_idx: [0x13]
1676      - sig: ashr v1:in:i32, v2:in:i32
1677        acc: out:i32
1678        prefix: bit
1679        format: [pref_op_v1_4_v2_4]
1680        opcode_idx: [0x14]
1681
1682  - title: Three address binary operation with result in register
1683    description: Perform specified binary operation on two registers and store result into register
1684    exceptions:
1685      - x_none
1686    verification:
1687      - v1_type
1688      - v2_type
1689    pseudo: |
1690      switch (op)
1691      case add:
1692        v1 = (v1 + v2) % 2^32
1693      case sub:
1694        v1 = (v1 - v2) % 2^32
1695      case mul:
1696        v1 = (v1 * v2) % 2^32
1697      case and:
1698        v1 = v1 & v2
1699      case or:
1700        v1 = v1 | v2
1701      case xor:
1702        v1 = v1 ^ v2
1703      case shl:
1704        v1 = (v1 << (v2 & 0x1f)) % 2^32
1705      case shr:
1706        v1 = v1 >> (v2 & 0x1f)
1707      case ashr:
1708        v1 = (v1 < 0) ? ~(~v1 >> v2 & 0x1f) : v1 >> v2 & 0x1f
1709    instructions:
1710      - sig: addv v1:inout:i32, v2:in:i32
1711        acc: none
1712        format: [op_v1_4_v2_4]
1713      - sig: subv v1:inout:i32, v2:in:i32
1714        acc: none
1715        format: [op_v1_4_v2_4]
1716      - sig: mulv v1:inout:i32, v2:in:i32
1717        acc: none
1718        format: [op_v1_4_v2_4]
1719      - sig: andv v1:inout:i32, v2:in:i32
1720        acc: none
1721        prefix: bit
1722        format: [pref_op_v1_4_v2_4]
1723      - sig: orv v1:inout:i32, v2:in:i32
1724        acc: none
1725        prefix: bit
1726        format: [pref_op_v1_4_v2_4]
1727      - sig: xorv v1:inout:i32, v2:in:i32
1728        acc: none
1729        prefix: bit
1730        format: [pref_op_v1_4_v2_4]
1731      - sig: shlv v1:inout:i32, v2:in:i32
1732        acc: none
1733        prefix: bit
1734        format: [pref_op_v1_4_v2_4]
1735      - sig: shrv v1:inout:i32, v2:in:i32
1736        acc: none
1737        prefix: bit
1738        format: [pref_op_v1_4_v2_4]
1739      - sig: ashrv v1:inout:i32, v2:in:i32
1740        acc: none
1741        prefix: bit
1742        format: [pref_op_v1_4_v2_4]
1743
1744  - title: Three address integer division or modulo
1745    description: Perform integer division or modulo on two registers and store result into accumulator
1746    exceptions:
1747      - x_arith
1748    verification:
1749      - v1_type
1750      - v2_type
1751    pseudo: |
1752      if vs2 == 0 then
1753        throw ArithmeticException
1754      end
1755      switch(op)
1756      case div:
1757        if vs1 == INT32_MIN and vs2 == -1 then
1758          acc = INT32_MIN
1759        else
1760          acc = vs1 / vs2
1761        end
1762      case mod:
1763        if vs1 == INT32_MIN and vs2 == -1 then
1764          acc = 0
1765        else
1766          acc = vs1 % vs2
1767        end
1768    instructions:
1769      - sig: div v1:in:i32, v2:in:i32
1770        acc: out:i32
1771        format: [op_v1_4_v2_4]
1772        opcode_idx: [0x64]
1773      - sig: mod v1:in:i32, v2:in:i32
1774        acc: out:i32
1775        format: [op_v1_4_v2_4]
1776        opcode_idx: [0x65]
1777
1778  - title: Three address integer division or modulo with result in register
1779    description: Perform integer division or modulo on two registers and store result into accumulator
1780    exceptions:
1781      - x_arith
1782    verification:
1783      - v1_type
1784      - v2_type
1785    pseudo: |
1786      if v2 == 0 then
1787        throw ArithmeticException
1788      end
1789      switch(op)
1790      case div:
1791        if v1 == INT32_MIN and v2 == -1 then
1792          v1 = INT32_MIN
1793        else
1794          v1 = v1 / v2
1795        end
1796      case mod:
1797        if v1 == INT32_MIN and v2 == -1 then
1798          v1 = 0
1799        else
1800          v1 = v1 % v2
1801        end
1802    instructions:
1803      - sig: divv v1:inout:i32, v2:in:i32
1804        acc: none
1805        format: [op_v1_4_v2_4]
1806      - sig: modv v1:inout:i32, v2:in:i32
1807        acc: none
1808        format: [op_v1_4_v2_4]
1809
1810  - title: Increment register with immediate
1811    description: >
1812      Increment virtual register by specified immediate. Immediate is sign extended to operand size.
1813    exceptions:
1814      - x_none
1815    verification:
1816      - v1_i32
1817    pseudo: |
1818      vx = (vx + imm) % 2^32
1819    instructions:
1820      - sig: inci v:inout:i32, imm:i32
1821        acc: none
1822        format: [op_v_4_imm_4]
1823        opcode_idx: [0x66]
1824
1825  - title: Conversions between integer and floating point types
1826    description: |
1827      Perform specified primitive type conversion of accumulator.
1828      Conversion from floating-point types to integer one obeys the following rules.
1829
1830      - It is rounding toward zero.
1831      - If converted value is less than minimal value for destination type, the result is minimal value for that type.
1832      - If source is negative infinity, the result is minimal value for destination type.
1833      - If converted value is greater than maximum value for destination type, the result is maximum value for that type.
1834      - If source is positive infinity, the result is maximum value for destination type.
1835      - If source is NaN, the result is equal to 0.
1836
1837    properties:
1838      - float
1839    exceptions:
1840      - x_none
1841    verification:
1842      - acc_type
1843    pseudo: |
1844      (dest_type) acc = (src_type) acc
1845    instructions:
1846      - sig: i32tof32
1847        acc: inout:i32->f32
1848        prefix: f32
1849        format: [pref_op_none]
1850        opcode_idx: [0xa]
1851      - sig: i32tof64
1852        acc: inout:i32->f64
1853        prefix: cast
1854        format: [pref_op_none]
1855        opcode_idx: [0x0]
1856      - sig: u32tof32
1857        acc: inout:u32->f32
1858        prefix: f32
1859        format: [pref_op_none]
1860        opcode_idx: [0xb]
1861      - sig: u32tof64
1862        acc: inout:u32->f64
1863        prefix: cast
1864        format: [pref_op_none]
1865        opcode_idx: [0x1]
1866      - sig: i64tof32
1867        acc: inout:i64->f32
1868        prefix: f32
1869        format: [pref_op_none]
1870        opcode_idx: [0xc]
1871      - sig: i64tof64
1872        acc: inout:i64->f64
1873        prefix: cast
1874        format: [pref_op_none]
1875        opcode_idx: [0x2]
1876      - sig: u64tof32
1877        acc: inout:u64->f32
1878        prefix: f32
1879        format: [pref_op_none]
1880        opcode_idx: [0xd]
1881      - sig: u64tof64
1882        acc: inout:u64->f64
1883        prefix: cast
1884        format: [pref_op_none]
1885        opcode_idx: [0x3]
1886      - sig: f32tof64
1887        acc: inout:f32->f64
1888        prefix: f32
1889        format: [pref_op_none]
1890        opcode_idx: [0xe]
1891      - sig: f32toi32
1892        acc: inout:f32->i32
1893        prefix: f32
1894        format: [pref_op_none]
1895        opcode_idx: [0xf]
1896      - sig: f32toi64
1897        acc: inout:f32->i64
1898        prefix: f32
1899        format: [pref_op_none]
1900        opcode_idx: [0x10]
1901      - sig: f32tou32
1902        acc: inout:f32->u32
1903        prefix: f32
1904        format: [pref_op_none]
1905        opcode_idx: [0x11]
1906      - sig: f32tou64
1907        acc: inout:f32->u64
1908        prefix: f32
1909        format: [pref_op_none]
1910        opcode_idx: [0x12]
1911      - sig: f64toi32
1912        acc: inout:f64->i32
1913        prefix: cast
1914        format: [pref_op_none]
1915        opcode_idx: [0x4]
1916      - sig: f64toi64
1917        acc: inout:f64->i64
1918        prefix: cast
1919        format: [pref_op_none]
1920        opcode_idx: [0x5]
1921      - sig: f64tou32
1922        acc: inout:f64->u32
1923        prefix: cast
1924        format: [pref_op_none]
1925        opcode_idx: [0x6]
1926      - sig: f64tou64
1927        acc: inout:f64->u64
1928        prefix: cast
1929        format: [pref_op_none]
1930        opcode_idx: [0x7]
1931      - sig: f64tof32
1932        acc: inout:f64->f32
1933        prefix: f32
1934        format: [pref_op_none]
1935        opcode_idx: [0x13]
1936
1937  - title: Conversions from integer types to u1
1938    description: |
1939      Conversion from integer types to u1 obeys the following rules.
1940
1941      - If converted integer is not equal to zero, the result is 1.
1942      - Otherwise the result is 0.
1943
1944    exceptions:
1945      - x_none
1946    verification:
1947      - acc_type
1948    pseudo: |
1949      (dest_type) acc = (src_type) acc
1950    instructions:
1951      - sig: i32tou1
1952        acc: inout:i32->u1
1953        prefix: cast
1954        format: [pref_op_none]
1955        opcode_idx: [0x8]
1956      - sig: i64tou1
1957        acc: inout:i64->u1
1958        prefix: cast
1959        format: [pref_op_none]
1960        opcode_idx: [0x9]
1961      - sig: u32tou1
1962        acc: inout:u32->u1
1963        prefix: cast
1964        format: [pref_op_none]
1965        opcode_idx: [0xa]
1966      - sig: u64tou1
1967        acc: inout:u64->u1
1968        prefix: cast
1969        format: [pref_op_none]
1970        opcode_idx: [0xb]
1971
1972  - title: Integer truncations and extensions.
1973    description: >
1974      Perform specified integer extension or truncations of accumulator.
1975      Truncations discard all but N lowest-order bits, where N is the bit size of destination type.
1976      If extension bytecode treats its source as signed integer, the value is sign-extended to destination type.
1977      If extension bytecode treats its source as unsigned integer, the value is zero-extended to destination type.
1978    exceptions:
1979      - x_none
1980    verification:
1981      - acc_type
1982    pseudo: |
1983      (dest_type) acc = (src_type) acc
1984    instructions:
1985      - sig: i32toi64
1986        acc: inout:i32->i64
1987        prefix: cast
1988        format: [pref_op_none]
1989        opcode_idx: [0xc]
1990      - sig: i32toi16
1991        acc: inout:i32->i16
1992        prefix: cast
1993        format: [pref_op_none]
1994        opcode_idx: [0xd]
1995      - sig: i32tou16
1996        acc: inout:i32->u16
1997        prefix: cast
1998        format: [pref_op_none]
1999        opcode_idx: [0xe]
2000      - sig: i32toi8
2001        acc: inout:i32->i8
2002        prefix: cast
2003        format: [pref_op_none]
2004        opcode_idx: [0xf]
2005      - sig: i32tou8
2006        acc: inout:i32->u8
2007        prefix: cast
2008        format: [pref_op_none]
2009        opcode_idx: [0x10]
2010      - sig: i64toi32
2011        acc: inout:i64->i32
2012        prefix: cast
2013        format: [pref_op_none]
2014        opcode_idx: [0x11]
2015      - sig: u32toi64
2016        acc: inout:u32->i64
2017        prefix: cast
2018        format: [pref_op_none]
2019        opcode_idx: [0x12]
2020      - sig: u32toi16
2021        acc: inout:u32->i16
2022        prefix: cast
2023        format: [pref_op_none]
2024        opcode_idx: [0x13]
2025      - sig: u32tou16
2026        acc: inout:u32->u16
2027        prefix: cast
2028        format: [pref_op_none]
2029        opcode_idx: [0x14]
2030      - sig: u32toi8
2031        acc: inout:u32->i8
2032        prefix: cast
2033        format: [pref_op_none]
2034        opcode_idx: [0x15]
2035      - sig: u32tou8
2036        acc: inout:u32->u8
2037        prefix: cast
2038        format: [pref_op_none]
2039        opcode_idx: [0x16]
2040      - sig: u64toi32
2041        acc: inout:u64->i32
2042        prefix: cast
2043        format: [pref_op_none]
2044        opcode_idx: [0x17]
2045      - sig: u64tou32
2046        acc: inout:u64->u32
2047        prefix: cast
2048        format: [pref_op_none]
2049        opcode_idx: [0x18]
2050
2051  - title: Load from array
2052    description: >
2053      Load an element from array using accumulator as an index and puts it into accumulator.
2054      If element size is smaller then 32 bits, it will be zero or sign extended (depending on bytecode)
2055      to i32.
2056    verification:
2057      - v1_array_type
2058      - acc_i32
2059    exceptions:
2060      - x_null
2061      - x_bounds
2062    pseudo: |
2063      if vs == null then
2064        throw NullPointerException
2065      end
2066      if acc < 0 || acc >= len(vs) then
2067        throw ArrayIndexOutOfBoundsException
2068      end
2069      if op == ldarr.8 then
2070        acc = i8toi32(vs[acc])
2071      else if op == ldarru.8 then
2072        acc = u8toi32(vs[acc])
2073      else if op == ldarr.16 then
2074        acc = i16toi32(vs[acc])
2075      else if op == ldarru.16 then
2076        acc = u16toi32(vs[acc])
2077      else
2078        acc = vs[acc]
2079      end
2080    instructions:
2081      - sig: ldarr.8 v:in:i8[]
2082        acc: inout:i32
2083        format: [op_v_8]
2084        opcode_idx: [0x67]
2085      - sig: ldarru.8 v:in:u8[]
2086        acc: inout:i32
2087        format: [op_v_8]
2088        opcode_idx: [0x68]
2089      - sig: ldarr.16 v:in:i16[]
2090        acc: inout:i32
2091        format: [op_v_8]
2092        opcode_idx: [0x69]
2093      - sig: ldarru.16 v:in:u16[]
2094        acc: inout:i32
2095        format: [op_v_8]
2096        opcode_idx: [0x6a]
2097      - sig: ldarr v:in:i32[]
2098        acc: inout:i32
2099        format: [op_v_8]
2100        opcode_idx: [0x6b]
2101      - sig: ldarr.64 v:in:i64[]
2102        acc: inout:i32->i64
2103        format: [op_v_8]
2104        opcode_idx: [0x6c]
2105      - sig: fldarr.32 v:in:f32[]
2106        acc: inout:i32->f32
2107        format: [op_v_8]
2108        opcode_idx: [0x6d]
2109        properties: [float]
2110      - sig: fldarr.64 v:in:f64[]
2111        acc: inout:i32->f64
2112        format: [op_v_8]
2113        opcode_idx: [0x6e]
2114        properties: [float]
2115      - sig: ldarr.obj v:in:ref[]
2116        acc: inout:i32->ref
2117        format: [op_v_8]
2118        opcode_idx: [0x6f]
2119
2120  - title: Store to array
2121    description: >
2122      Store accumulator content into array slot pointed by index.
2123      If size of element to store is less than 32, accumulator content will be truncated
2124      to storage size before storing.
2125    verification:
2126      - v1_array_type
2127      - v2_i32
2128      - acc_type
2129    exceptions:
2130      - x_null
2131      - x_bounds
2132      - x_store
2133    pseudo: |
2134      if vs1 == null then
2135        throw NullPointerException
2136      end
2137      if vs2 < 0 || vs2 >= len(vs1) then
2138        throw ArrayIndexOutOfBoundsException
2139      end
2140      if op == starr.obj && !has_type(acc, component_type(vs1))
2141        throw ArrayStoreException
2142      end
2143      if op == starr.8 then
2144        vs1[vs2] = truncateto8(acc)
2145      else if op == starr.16 then
2146        vs1[vs2] = truncateto16(acc)
2147      else
2148        vs1[vs2] = acc
2149      end
2150    instructions:
2151      - sig: starr.8 v1:in:i8[], v2:in:i32
2152        acc: in:i8
2153        format: [op_v1_4_v2_4]
2154        opcode_idx: [0x70]
2155      - sig: starr.16 v1:in:i16[], v2:in:i32
2156        acc: in:i16
2157        format: [op_v1_4_v2_4]
2158        opcode_idx: [0x71]
2159      - sig: starr v1:in:i32[], v2:in:i32
2160        acc: in:i32
2161        format: [op_v1_4_v2_4]
2162        opcode_idx: [0x72]
2163      - sig: starr.64 v1:in:i64[], v2:in:i32
2164        acc: in:i64
2165        format: [op_v1_4_v2_4]
2166        opcode_idx: [0x73]
2167      - sig: fstarr.32 v1:in:f32[], v2:in:i32
2168        acc: in:f32
2169        format: [op_v1_4_v2_4]
2170        opcode_idx: [0x74]
2171        properties: [float]
2172      - sig: fstarr.64 v1:in:f64[], v2:in:i32
2173        acc: in:f64
2174        format: [op_v1_4_v2_4]
2175        opcode_idx: [0x75]
2176        properties: [float]
2177      - sig: starr.obj v1:in:ref[], v2:in:i32
2178        acc: in:ref
2179        format: [op_v1_4_v2_4]
2180        opcode_idx: [0x76]
2181
2182  - title: Array length
2183    description: Get length of an array and put it into accumulator.
2184    verification:
2185      - v1_array
2186    exceptions:
2187      - x_null
2188    pseudo: |
2189      if x == null then
2190        throw NullPointerException
2191      end
2192      acc = len(vs)
2193    instructions:
2194      - sig: lenarr v:in:top[]
2195        acc: out:i32
2196        format: [op_v_8]
2197        opcode_idx: [0x77]
2198
2199  - title: Create new array
2200    description: >
2201      Create a new single-dimensional array of given type and size and put a reference to it into register.
2202      Elements of array are initialized to a default value, i.e. 0 for primitive types and null for objects.
2203    verification:
2204      - type_id_array
2205      - v2_i32
2206    exceptions:
2207      - x_negsize
2208      - x_oom
2209    properties:
2210      - type_id
2211      - language_type
2212      - initialize_type
2213    pseudo: |
2214      if v2 < 0 then
2215        throw NegativeArraySizeException
2216      end
2217      type = resolve(type_id)
2218      v1 = new_array(v2, type)
2219      if not initialized(type)
2220        initialize(type)
2221      end
2222      if v1 == null then
2223        throw OutOfMemoryError
2224      end
2225    instructions:
2226      - sig: newarr v1:out:ref, v2:in:i32, type_id
2227        acc: none
2228        format: [op_v1_4_v2_4_id_16]
2229        opcode_idx: [0x78]
2230
2231  - title: Create new object
2232    description: |
2233      Resolve class type from type_id, allocate memory for an object, initialize its fields with their
2234      default values (i.e. 0 for primitives and null for objects) and put a reference to the newly created
2235      object into register. The object should be initialized by calling initialization method before
2236      further usage.
2237    verification:
2238      - type_id_object
2239    exceptions:
2240      - x_oom
2241    properties:
2242      - type_id
2243      - initialize_type
2244    pseudo: |
2245      type = resolve(type_id)
2246      if not initialized(type)
2247        initialize(type)
2248      end
2249      v = new_instance(type)
2250      if v == null then
2251        throw OutOfMemoryError
2252      end
2253    instructions:
2254      - sig: newobj v:out:ref, type_id
2255        acc: none
2256        format: [op_v_8_id_16]
2257        opcode_idx: [0x79]
2258
2259  - title: Create new object and call initializer
2260    description: >
2261      Resolve class type from initializer method_id, allocate memory for an object, initialize its fields with their
2262      default values (i.e. 0 for primitives and null for objects), call specified initializer and put a reference to
2263      the newly created object into accumulator. method_id should resolve to an initializer.
2264      Non-range instructions can be used to pass up to 4 arguments.
2265      Unused register slot values will be discarded and corresponding registers will not be passed to initializer).
2266      For methods with more arguments range kinds of instruction are to be used, which takes the needed number of
2267      arguments starting from 'vs' register.
2268    verification:
2269      - method_id_non_static
2270      - method_id_accessible
2271      - method_init_obj
2272      - compatible_arguments
2273    exceptions:
2274      - x_abstract
2275      - x_oom
2276      - x_call
2277    properties:
2278      - method_id
2279      - call
2280      - initialize_type
2281      - init_obj
2282      - short_long_range
2283    pseudo: |
2284      init, type = resolve(method_id)
2285      if not initialized(type)
2286        initialize(type)
2287      end
2288      acc = new_instance(type)
2289      if acc == null then
2290        throw OutOfMemoryError
2291      end
2292      init(acc, args)
2293    instructions:
2294      - sig: initobj.short method_id, v1:in:none, v2:in:none
2295        acc: out:ref
2296        format: [op_v1_4_v2_4_id_16]
2297        opcode_idx: [0x7a]
2298      - sig: initobj method_id, v1:in:none, v2:in:none, v3:in:none, v4:in:none
2299        acc: out:ref
2300        format: [op_v1_4_v2_4_v3_4_v4_4_id_16]
2301        opcode_idx: [0x7b]
2302      - sig: initobj.range method_id, v:in:none
2303        acc: out:ref
2304        format: [op_v_8_id_16]
2305        opcode_idx: [0x7c]
2306
2307  - title: Get field from object to accumulator
2308    description: >
2309      Get field value from an object by field id and put it into accumulator.
2310      For non-object variant, the size of the field is determined by the field_id,
2311      most significant bits are sign or unsigned extended based on the field type to fit accumulator size.
2312      If field type size is less than 32, then loaded value is sign or zero extended to i32 depending on field type.
2313    verification:
2314      - v1_object
2315      - field_id_non_static
2316      - field_id_size
2317    properties:
2318      - field_id
2319    exceptions:
2320      - x_null
2321    pseudo: |
2322      if vs == null then
2323        throw NullPointerException
2324      end
2325      field = resolve(field_id)
2326      if op == ldobj and size(field) < 32 then
2327        acc = extendto32(vs.get(field))
2328      else
2329        acc = vs.get(field)
2330      end
2331    instructions:
2332      - sig: ldobj v:in:ref, field_id
2333        acc: out:b32
2334        format: [op_v_8_id_16]
2335        opcode_idx: [0x7d]
2336      - sig: ldobj.64 v:in:ref, field_id
2337        acc: out:b64
2338        format: [op_v_8_id_16]
2339        opcode_idx: [0x7e]
2340      - sig: ldobj.obj v:in:ref, field_id
2341        acc: out:ref
2342        format: [op_v_8_id_16]
2343        opcode_idx: [0x7f]
2344
2345  - title: Store accumulator content into object field
2346    description: >
2347      Store accumulator content into object field by field_id. For non-object variant the size of actually stored
2348      value is determined by field_id, other accumulator bits are discarded.
2349      If field type size is less than 32, accumulator content will be truncated to storage size before storing.
2350    verification:
2351      - v1_object
2352      - field_id_non_static
2353      - field_id_size
2354      - acc_type
2355    properties:
2356      - field_id
2357    exceptions:
2358      - x_null
2359    pseudo: |
2360      if vs == null then
2361        throw NullPointerException
2362      end
2363      field = resolve(field_id)
2364      if op == stobj and size(field) < 32 then
2365        vs.set(field, truncate(field, acc))
2366      else
2367        vs.set(field, acc)
2368      end
2369    instructions:
2370      - sig: stobj v:in:ref, field_id
2371        acc: in:b32
2372        format: [op_v_8_id_16]
2373        opcode_idx: [0x80]
2374      - sig: stobj.64 v:in:ref, field_id
2375        acc: in:b64
2376        format: [op_v_8_id_16]
2377        opcode_idx: [0x81]
2378      - sig: stobj.obj v:in:ref, field_id
2379        acc: in:ref
2380        format: [op_v_8_id_16]
2381        opcode_idx: [0x82]
2382
2383  - title: Get field from object to register
2384    description: >
2385      Get field value from an object by field id and put it into register.
2386      For non-object variant, the size of the field is determined by the field_id,
2387      most significant bits are sign or unsigned extended based on the field type to fit register size.
2388      If field type size is less than 32, then loaded value is sign or zero extended to i32 depending on field type.
2389    verification:
2390      - v2_object
2391      - field_id_non_static
2392      - field_id_size
2393    properties:
2394      - field_id
2395    exceptions:
2396      - x_null
2397    pseudo: |
2398      if v2 == null then
2399        throw NullPointerException
2400      end
2401      field = resolve(field_id)
2402      if op == ldobj and size(field) < 32 then
2403        v1 = extendto32(v2.get(field))
2404      else
2405        v1 = v2.get(field)
2406      end
2407    instructions:
2408      - sig: ldobj.v v1:out:b32, v2:in:ref, field_id
2409        acc: none
2410        format: [op_v1_4_v2_4_id_16]
2411        opcode_idx: [0x83]
2412      - sig: ldobj.v.64 v1:out:b64, v2:in:ref, field_id
2413        acc: none
2414        format: [op_v1_4_v2_4_id_16]
2415        opcode_idx: [0x84]
2416      - sig: ldobj.v.obj v1:out:ref, v2:in:ref, field_id
2417        acc: none
2418        format: [op_v1_4_v2_4_id_16]
2419        opcode_idx: [0x85]
2420
2421  - title: Store register content into object field
2422    description: >
2423      Store register content into object field by field_id. For non-object variant the size of actually stored
2424      value is determined by field_id, other register bits are discarded.
2425      If field type size is less than 32, register content will be truncated to storage size before storing.
2426    verification:
2427      - v1_type
2428      - v2_object
2429      - field_id_non_static
2430      - field_id_size
2431    properties:
2432      - field_id
2433    exceptions:
2434      - x_null
2435    pseudo: |
2436      if v2 == null then
2437        throw NullPointerException
2438      end
2439      field = resolve(field_id)
2440      if op == stobj and size(field) < 32 then
2441        v2.set(field, truncate(field, v1))
2442      else
2443        v2.set(field, v1)
2444      end
2445    instructions:
2446      - sig: stobj.v v1:in:b32, v2:in:ref, field_id
2447        acc: none
2448        format: [op_v1_4_v2_4_id_16]
2449        opcode_idx: [0x86]
2450      - sig: stobj.v.64 v1:in:b64, v2:in:ref, field_id
2451        acc: none
2452        format: [op_v1_4_v2_4_id_16]
2453        opcode_idx: [0x87]
2454      - sig: stobj.v.obj v1:in:ref, v2:in:ref, field_id
2455        acc: none
2456        format: [op_v1_4_v2_4_id_16]
2457        opcode_idx: [0x88]
2458
2459  - title: Get static field
2460    description: >
2461      Get static field value by field_id and put it into accumulator.
2462      For non-object variant, the size of the field is determined by the field_id,
2463      most significant bits are sign or unsigned extended based on the field type to fit accumulator size.
2464      If field size is less then 32, result will be sign or unsigned extended to i32 depedning on field type.
2465    verification:
2466      - field_id_static
2467      - field_id_size
2468    properties:
2469      - field_id
2470      - initialize_type
2471    exceptions:
2472      - x_init
2473    pseudo: |
2474      field, type = resolve(field_id)
2475      if not initialized(type)
2476        initialize(type)
2477      end
2478      if op == ldstatic and size(field) < 32 then
2479        acc = extendto32(get_static(field))
2480      else
2481        acc = get_static(field)
2482      end
2483    instructions:
2484      - sig: ldstatic field_id
2485        acc: out:b32
2486        format: [op_id_16]
2487        opcode_idx: [0x89]
2488      - sig: ldstatic.64 field_id
2489        acc: out:b64
2490        format: [op_id_16]
2491        opcode_idx: [0x8a]
2492      - sig: ldstatic.obj field_id
2493        acc: out:ref
2494        format: [op_id_16]
2495        opcode_idx: [0x8b]
2496
2497  - title: Store to static field
2498    description: >
2499      Store accumulator content into static field by field_id. For non-object variant the size of actually stored
2500      value is determined by field_id, other accumulator bits are discarded.
2501      If field type size is less than 32, then accumulator content will be trunctated to field size before storing.
2502    verification:
2503      - field_id_static
2504      - field_id_size
2505      - acc_type
2506    properties:
2507      - field_id
2508      - initialize_type
2509    exceptions:
2510      - x_init
2511    pseudo: |
2512      field, type = resolve(field_id)
2513      if not initialized(type)
2514        initialize(type)
2515      end
2516      if op == ststatic and size(field) < 32 then
2517        set_static(field, truncate(field, acc))
2518      else
2519        set_static(field, acc)
2520      end
2521    instructions:
2522      - sig: ststatic field_id
2523        acc: in:b32
2524        format: [op_id_16]
2525        opcode_idx: [0x8c]
2526      - sig: ststatic.64 field_id
2527        acc: in:b64
2528        format: [op_id_16]
2529        opcode_idx: [0x8d]
2530      - sig: ststatic.obj field_id
2531        acc: in:ref
2532        format: [op_id_16]
2533        opcode_idx: [0x8e]
2534
2535  - title: Return value from method
2536    description: >
2537      Return from the current method, i.e. restore the frame of method invoker and return control to the
2538      invoker. Return value should be in accumulator.
2539    verification:
2540      - acc_return_type
2541    exceptions:
2542      - x_none
2543    properties:
2544      - return
2545    pseudo: |
2546      return acc
2547    instructions:
2548      - sig: return
2549        acc: in:b32
2550        format: [op_none]
2551        opcode_idx: [0x8f]
2552      - sig: return.64
2553        acc: in:b64
2554        format: [op_none]
2555        opcode_idx: [0x90]
2556      - sig: return.obj
2557        acc: in:ref
2558        format: [op_none]
2559        opcode_idx: [0x91]
2560
2561  - title: Return from a void method
2562    description: >
2563      Return from the current method, i.e. restore the frame of method invoker and return control to the invoker.
2564      Caller should treat accumulator value as undefined and cannot use it until accumulator definition in the caller
2565      frame.
2566    verification:
2567      - none
2568    exceptions:
2569      - x_none
2570    properties:
2571      - return
2572    pseudo: |
2573      return
2574    instructions:
2575      - sig: return.void
2576        acc: none
2577        format: [op_none]
2578        opcode_idx: [0x92]
2579
2580  - title: Throw exception
2581    description: >
2582      Throw an exception located in register. The current method is searched for the first exception handler that
2583      matches the class of exception. If exception handler is found, control is passed to the exception handler. If no
2584      exception handler is found, the frame of invoker is restored. If such frame exists, the exception is re-thrown.
2585      If no such frame exists, the current VM thread exits.
2586    verification:
2587      - v1_throw_type
2588    exceptions:
2589      - x_null
2590      - x_throw
2591    pseudo: |
2592      if vs == null then
2593        throw NullPointerException
2594      end
2595      throw vs
2596    instructions:
2597      - sig: throw v:in:ref
2598        acc: none
2599        format: [op_v_8]
2600        opcode_idx: [0x93]
2601
2602  - title: Check cast
2603    description: >
2604      Resolve object type by specified id and if an object in accumulator can be cast to the resolved type,
2605      accumulator content remains unchanged. Otherwise ClassCastException is thrown.
2606      Object of type O can be cast to type T if O is the same as T or is subtype of T. For arrays O can be cast
2607      to T if T is a root type in type hierarchy or T is such array that O array elements are the same or subtype of
2608      T array elements.
2609      'null' object reference can be cast to every type.
2610    verification:
2611      - type_id_any_object
2612      - acc_obj_or_null
2613    exceptions:
2614      - x_cast
2615    properties:
2616      - type_id
2617    pseudo: |
2618      type = resolve(type_id)
2619      if acc != null and !has_type(acc, type) then
2620        throw ClassCastException
2621      end
2622    instructions:
2623      - sig: checkcast type_id
2624        acc: in:ref
2625        format: [op_id_16]
2626        opcode_idx: [0x94]
2627
2628  - title: Is instance
2629    description: >
2630      Resolve object type by specified id and if an object in accumulator is an instance of the resolved type,
2631      put 1 into accumulator, otherwise put 0.
2632      Object of type O is instance of type T if O is the same as T or is subtype of T. For arrays T should be a root
2633      type in type hierarchy or T is such array that O array elements are the same or subtype of T array elements.
2634      'null' object is not an instance of any class.
2635    verification:
2636      - type_id_any_object
2637      - acc_obj_or_null
2638    exceptions:
2639      - x_classdef
2640    properties:
2641      - type_id
2642    pseudo: |
2643      type = resolve(type_id)
2644      if acc == null or !has_type(acc, type) then
2645        acc = 0
2646      else
2647        acc = 1
2648      end
2649    instructions:
2650      - sig: isinstance type_id
2651        acc: inout:ref->i32
2652        format: [op_id_16]
2653        opcode_idx: [0x95]
2654
2655  - title: Static call
2656    description: >
2657      Call indicated static method, i.e. create new frame, pass values of arguments and
2658      continue execution from the first instruction of a method.
2659      Callee should treat accumulator value as undefined and cannot use it until accumulator
2660      definition in the new frame.
2661      Result (if any) is returned in accumulator (see 'Calling sequence' chapter for more details).
2662      Method, its class and the number of argument is resolved by given method_id in
2663      runtime constant-pool.
2664      Arguments are passed in source registers in the same order as in method signature.
2665      Non-range instructions can be used to pass up to 4 arguments (unused register slot values will
2666      be discarded and corresponding registers will not be passed to the callee).
2667      For methods with more arguments range kind of instruction is to be used, which takes the needed number
2668      of arguments starting from 'vs' register.
2669    verification:
2670      - method_id_static
2671      - method_id_non_abstract
2672      - compatible_arguments
2673    properties:
2674      - method_id
2675      - call
2676      - initialize_type
2677      - short_long_range
2678    exceptions:
2679      - x_call
2680    pseudo: |
2681      if not initialized(type)
2682        initialize(type)
2683      end
2684      acc = call(method, args)
2685    instructions:
2686      - sig: call.short method_id, v1:in:top, v2:in:top
2687        acc: out:top
2688        format: [op_v1_4_v2_4_id_16]
2689        opcode_idx: [0x96]
2690      - sig: call method_id, v1:in:top, v2:in:top, v3:in:top, v4:in:top
2691        acc: out:top
2692        format: [op_v1_4_v2_4_v3_4_v4_4_id_16]
2693        opcode_idx: [0x97]
2694      - sig: call.range method_id, v:in:top
2695        acc: out:top
2696        format: [op_v_8_id_16]
2697        opcode_idx: [0x98]
2698
2699  - title: Static call with accumulator as input
2700    description: >
2701      Call indicated static method, i.e. create new frame, pass values of arguments and
2702      continue execution from the first instruction of a method.
2703      Callee should treat accumulator value as undefined and cannot use it until accumulator
2704      definition in the new frame.
2705      Result (if any) is returned in accumulator (see 'Calling sequence' chapter for more details).
2706      Method, its class and the number of argument is resolved by given method_id in
2707      runtime constant-pool.
2708      Arguments are passed in source registers in the same order as in method signature.
2709      Non-range instructions can be used to pass up to 4 arguments (unused register slot values will
2710      be discarded and corresponding registers will not be passed to the callee).
2711      Immediate operand encodes a position starting from 0 on which accumulator is passed.
2712    verification:
2713      - method_id_static
2714      - method_id_non_abstract
2715      - compatible_arguments
2716    properties:
2717      - method_id
2718      - call
2719      - short_long_range
2720    exceptions:
2721      - x_call
2722    pseudo: |
2723      args = []
2724      for (i = 0; i < 4; ++i)
2725        if (i < imm) then
2726          args[i] = regs[i]
2727        else if (i == imm) then
2728          args[i] = acc
2729        else
2730          args[i] = regs[i - 1]
2731        end
2732      end
2733      method = resolve(method_id)
2734      acc = call(method, args)
2735    instructions:
2736      - sig: call.acc.short method_id, v:in:top, imm:u1
2737        acc: inout:top
2738        format: [op_v_4_imm_4_id_16]
2739        opcode_idx: [0x99]
2740      - sig: call.acc method_id, v1:in:top, v2:in:top, v3:in:top, imm:u2
2741        acc: inout:top
2742        format: [op_v1_4_v2_4_v3_4_imm_4_id_16]
2743        opcode_idx: [0x9a]
2744
2745  - title: Virtual calls
2746    description: >
2747      Call indicated virtual method, i.e. create new frame, pass values of arguments and
2748      continue execution from the first instruction of a method.
2749      Callee should treat accumulator value as undefined and cannot use it until accumulator
2750      definition in the new frame.
2751      Result (if any) is returned in accumulator (see 'Calling sequence' chapter for more details).
2752      Method, its class and the number of argument is resolved by given method_id in runtime
2753      constant-pool based on object reference using language-specific semantics (currently only Java
2754      virtual methods are supported, further extensions are TBD).
2755      Object reference is passed in the first source register, arguments are passed starting from
2756      the second source register in the same order as in method signature.
2757      Non-range instructions can be used to pass up to 4 arguments (including object reference).
2758      Unused register slot values will be discarded and corresponding registers will not be
2759      passed to the callee).
2760      For methods with more arguments range kinds of instruction are to be used, which takes
2761      the needed number of arguments starting from 'vs' register (including object reference).
2762    verification:
2763      - compatible_arguments
2764      - method_id_accessible
2765    exceptions:
2766      - x_null
2767      - x_abstract
2768      - x_call
2769    properties:
2770      - method_id
2771      - call
2772      - call_virt
2773      - short_long_range
2774    pseudo: |
2775      if args[0] == null then
2776        throw NullPointerException
2777      end
2778      method = resolve(method_id)
2779      if is_abstract(method) then
2780        throw AbstractMethodError
2781      end
2782      acc = call(method, args)
2783    instructions:
2784      - sig: call.virt.short method_id, v1:in:top, v2:in:top
2785        acc: out:top
2786        format: [op_v1_4_v2_4_id_16]
2787        opcode_idx: [0x9b]
2788      - sig: call.virt method_id, v1:in:top, v2:in:top, v3:in:top, v4:in:top
2789        acc: out:top
2790        format: [op_v1_4_v2_4_v3_4_v4_4_id_16]
2791        opcode_idx: [0x9c]
2792      - sig: call.virt.range method_id, v:in:top
2793        acc: out:top
2794        format: [op_v_8_id_16]
2795        opcode_idx: [0x9d]
2796
2797  - title: Virtual calls with accumulator as input
2798    description: >
2799      Call indicated virtual method, i.e. create new frame, pass values of arguments and
2800      continue execution from the first instruction of a method.
2801      Callee should treat accumulator value as undefined and cannot use it until accumulator
2802      definition in the new frame.
2803      Result (if any) is returned in accumulator (see 'Calling sequence' chapter for more details).
2804      Method, its class and the number of argument is resolved by given method_id in runtime
2805      constant-pool based on object reference using language-specific semantics (currently only Java
2806      virtual methods are supported, further extensions are TBD).
2807      Object reference is passed in the first source register, arguments are passed starting from
2808      the second source register in the same order as in method signature.
2809      Non-range instructions can be used to pass up to 4 arguments (including object reference).
2810      Unused register slot values will be discarded and corresponding registers will not be
2811      passed to the callee).
2812      Immediate operand encodes a position starting from 0 on which accumulator is passed.
2813    verification:
2814      - compatible_arguments
2815      - method_id_accessible
2816    exceptions:
2817      - x_null
2818      - x_abstract
2819      - x_call
2820    properties:
2821      - method_id
2822      - call
2823      - call_virt
2824      - short_long_range
2825    pseudo: |
2826      args = []
2827      for (i = 0; i < 4; ++i)
2828        if (i < imm) then
2829          args[i] = regs[i]
2830        else if (i == imm) then
2831          args[i] = acc
2832        else
2833          args[i] = regs[i - 1]
2834        end
2835      end
2836      if args[0] == null then
2837        throw NullPointerException
2838      end
2839      method = resolve(method_id)
2840      if is_abstract(method) then
2841        throw AbstractMethodError
2842      end
2843      acc = call(method, args)
2844    instructions:
2845      - sig: call.virt.acc.short method_id, v:in:top, imm:u1
2846        acc: inout:top
2847        format: [op_v_4_imm_4_id_16]
2848        opcode_idx: [0x9e]
2849      - sig: call.virt.acc method_id, v1:in:top, v2:in:top, v3:in:top, imm:u2
2850        acc: inout:top
2851        format: [op_v1_4_v2_4_v3_4_imm_4_id_16]
2852        opcode_idx: [0x9f]
2853
2854  - title: Dynamic move register-to-register
2855    description: >
2856      Move 'any' values between registers
2857    verification:
2858      - valid_in_dynamic_context
2859    exceptions:
2860      - x_none
2861    properties:
2862      - dynamic
2863    pseudo: |
2864      vd = vs
2865    instructions:
2866      - sig: mov.dyn v1:out:any, v2:in:any
2867        acc: none
2868        format: [op_v1_8_v2_8, op_v1_16_v2_16]
2869        opcode_idx: [0xa0, 0xa1]
2870
2871  - title: Dynamic load accumulator from register
2872    description: >
2873      Move 'any' value from register to accumulator
2874    verification:
2875      - valid_in_dynamic_context
2876    exceptions:
2877      - x_none
2878    properties:
2879      - dynamic
2880    pseudo: |
2881      acc = v
2882    instructions:
2883      - sig: lda.dyn v:in:any
2884        acc: out:any
2885        format: [op_v_8]
2886        opcode_idx: [0xa2]
2887
2888  - title: Dynamic store accumulator
2889    description: >
2890      Move 'any' value from accumulator to register
2891    verification:
2892      - valid_in_dynamic_context
2893    exceptions:
2894      - x_none
2895    properties:
2896      - dynamic
2897    pseudo: |
2898      v = acc
2899    instructions:
2900      - sig: sta.dyn v:out:any
2901        acc: in:any
2902        format: [op_v_8]
2903        opcode_idx: [0xa3]
2904
2905  - title: Dynamic load accumulator from immediate
2906    description: >
2907      Move immediate as 'any' value to accumulator
2908    verification:
2909      - valid_in_dynamic_context
2910    exceptions:
2911      - x_none
2912    properties:
2913      - dynamic
2914    pseudo: |
2915      acc = imm
2916    instructions:
2917      - sig: ldai.dyn imm:i32
2918        acc: out:any
2919        format: [op_imm_32]
2920        opcode_idx: [0xa4]
2921      - sig: fldai.dyn imm:f64
2922        acc: out:any
2923        format: [op_imm_64]
2924        opcode_idx: [0xa5]
2925        properties: [float, dynamic]
2926