openharmony/ark_runtime_core
1
0
Fork 0
mirror of https://github.com/openharmony/ark_runtime_core.git synced 2026-07-19 21:23:32 -04:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
ark_runtime_core/isa/isa.yaml
T
openharmony_ci 031d76da4d !114 ISA/ISAPI minor fixes 
Merge pull request !114 from bolshov.maxim/master
2022-03-30 10:58:53 +00:00

3206 lines
101 KiB
YAML
Raw Permalink Blame History

# Copyright (c) 2021-2022 Huawei Device Co., Ltd.
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
---
chapters:
- name: General design
text: >
VM is register based with dedicated accumulator register, which serves as an implicit operand to instructions.
- name: Registers
text: >
Registers are wide enough to hold a single reference when working with objects.
When used for primitive types, registers width should be considered as 64 bits.
When used for object types, registers should be considered wide enough to hold a reference to an object.
The scope of a register is function frame (also known as activation record). If instruction defines not all 64
bits of a register, undefined bits shall not be accessed in verified code.
Register field width in instruction encoding could be 4 (16 addressable registers), 8 (256 registers) or
16 (65536 registers) bits.
- name: Accumulator
text: >
Accumulator is a special register which is implicitly used by instructions as a source and/or destination operand.
The main goal of using accumulator is to improve encoding density without losing much in performance. Therefore,
the general intuition regarding accumulator usage is to utilize the accumulator as much as possible taking it as
a source from previous instruction result and passing it to the next instruction in its destination operand.
Moreover, when instruction has more than one source operands, the value which lives shorter should be passed
through the accumulator. If it is profitable however, variations of instructions that don't write into the
accumulator are also introduced. For example, moving arguments for `call.range` instruction may be done by
register-to-register moves.
- name: Calling sequence
text: >
On execution of a call bytecode a new function frame is created. All necessary arguments are copied from the
caller frame onto the top of the callee frame. For example, the last argument is placed in the register with the largest
index and the first argument is placed into the register with the index equal to the size of frame subtracted by
the number of arguments. Accumulator value is considered as undefined and shall not be read in verified bytecode.
On return, callee frame is destroyed. If function return value is non-void, it is passed to caller via
accumulator. Otherwise accumulator content in caller frame is considered as undefined and shall not
be read in verified bytecode.
- name: Supported primitive types
text: |
VM support operations on registers with i32 and i64 integral values. However, 8-bit and 16-bit integral values
can be loaded/stored into records and arrays with corresponding bytecodes. In that case, VM will extend/truncate
value to match storage size with i32. Similarly, passing an 8-bit or 16-bit value to a function can be emulated by
passing a value, which is zero or sign-extended to i32.
VM support operations on registers with f32 and f64 values, which corresponds to IEEE-754 single and double precision
floating-point represenation.
Primitive data type of a register is not tracked by VM and is interpreted by separate bytecodes.
Integral values are not inherently signed or unsigned, signedness is interpreted by bytecodes as well.
If bytecode treats register value as signed integer, it uses two's complement representation.
To denote that bytecode treats register values as unsigned integer, u32/u64 notation is used.
For moves, loads and stores it is not always possible to denote a type of result, because it depends on type
of source object. In that case, bNN notation is used, where NN is bit size of result. Therefore, for example,
b64 is a union of f64 and i64.
### Floating-point literals
Decimal floating-point literals can have the following parts:
- Sign ("`+`" or "`-`")
- Whole number part
- Decimal point
- Fractional part
- Exponent indicator ("`e`")
- Exponent sign
- Exponent
Decimal floating-point literals must have at least one digit and either decimal point or exponent part.
Special values:
- Positive zero (+0.0, hexadecimal representation is `0x0000000000000000`)
- Negative zero (-0.0, hexadecimal representation is `0x8000000000000000`)
- Minimal positive value (4.9E-324, hexadecimal representation is `0x0000000000000001`)
- Maximal negative value (-4.9E-324, hexadecimal representation is `0x8000000000000001`)
- Maximal positive value (1.7976931348623157e308, hexadecimal representation is `0x7fefffffffffffff`)
- Minimal negative value (-1.7976931348623157e308, hexadecimal representation is `0xffefffffffffffff`)
- Positive infinity (hexadecimal representation is `0x7ff0000000000000`)
- Negative infinity (hexadecimal representation is `0xfff0000000000000`)
- Not a number - set of all NaN values (one of hexadecimal representations is `0x7ff8000000000000`)
- name: Language-dependent types
text: >
Panda VM supports type hierarchies according to the language it executes. That way, creation (or loading
from constant pool) of strings, arrays, exception objects results into an object of type native to language,
including inheritance relations.
- name: Dynamically-typed languages support
text: >
Panda VM supports languages with dynamic types. It represents dynamic values through special 'any' values,
which wraps a value itself (both primitive and objects) and corresponding type info. VM tracks type of registers
that hold 'any' value, whether they are primitive or not. Virtual registers and accumulator are wide enough
to hold 'any' value. When VM executes code inside dynamically-typed language context, regular static instructions
also may be used.
# File format and ISA versioning
min_version: 0.0.0.2
version: 0.0.0.2
properties:
- tag: acc_none
description: Doesn't use accumulator register.
- tag: acc_read
description: Use accumulator as a first source operand.
- tag: acc_write
description: Use accumulator as a destination operand.
- tag: type_id
description: Use an id which resolves into a type constant.
- tag: method_id
description: Use an id which resolves into a method constant.
- tag: string_id
description: Use an id which resolves into a string constant.
- tag: literalarray_id
description: Use an id which resolves into a constant literalarray.
- tag: field_id
description: Use an id which resolves into a field reference.
- tag: call
description: Pass control to the callee method.
- tag: call_virt
description: Pass control to the callee method via virtual call.
- tag: return
description: Pass control to the caller method.
- tag: jump
description: Pass control to another bytecode in a current method.
- tag: conditional
description: Operate based on computed condition, otherwise is no operation.
- tag: float
description: Perform floating point operation.
- tag: dynamic
description: Operate on 'any' values.
- tag: maybe_dynamic
description: May operate on 'any' values depending on language context.
- tag: language_type
description: Create objects of type depending on language context.
exceptions:
- tag: x_none
description: Bytecode doesn't throw exceptions.
- tag: x_null
description: Bytecode throws NullPointerException in case of null reference as a source.
- tag: x_bounds
description: Bytecode throws ArrayIndexOutOfBoundsException if index is out of bounds of an array.
- tag: x_negsize
description: Bytecode throws NegativeArraySizeException if index is less than zero.
- tag: x_store
description: Bytecode throws ArrayStoreException if element isn't instance of array's element type.
- tag: x_abstract
description: Bytecode throws AbstractMethodError if resolved method has no implementation.
- tag: x_arith
description: Bytecode throws ArithmeticException if the divisor is 0.
- tag: x_cast
description: Bytecode throws ClassCastException if type cast failed.
- tag: x_classdef
description: Bytecode throws NoClassDefFoundError if type cast failed.
- tag: x_oom
description: Bytecode throws OutOfMemoryError if failed to allocate object.
- tag: x_init
description: Bytecode throws ExceptionInInitializerError if unexpected exception occurred in a static initializer.
verification:
- tag: none
description: Instruction is always valid.
- tag: v1_array
description: First operand contains a reference to an array.
- tag: v1_object
description: First operand contains a reference to an object (other than array).
- tag: v1_array_type
description: First operand contains a reference to an array of elements of type corresponding to bytecode.
- tag: v1_i32
description: First operand contains a value of i32 type.
- tag: v1_type
description: First operand contains a value of type corresponding to bytecode.
- tag: v1_obj_or_null
description: First operand contains a reference to an object or null.
- tag: v2_i32
description: Second operand contains a value of i32 type.
- tag: v2_object
description: Second operand contains a reference to an object (other than array).
- tag: v2_type
description: Second operand contains a value of type corresponding to bytecode.
- tag: acc_i32
description: Accumulator contains a value of i32 type.
- tag: acc_type
description: Accumulator contains a value of type corresponding to bytecode.
- tag: acc_return_type
description: Accumulator type is compatible with method return type.
- tag: v1_throw_type
description: First operand contains a reference to an instance of class Throwable or of a subclass of Throwable.
- tag: acc_obj_or_null
description: Accumulator contains a reference to an object or null.
- tag: type_id_array
description: Type_id operand must correspond to an array type.
- tag: type_id_object
description: Type_id operand must correspond to an object type (other than array).
- tag: type_id_any_object
description: Type_id operand must correspond to any object type.
- tag: method_id_static
description: Method_id must resolve to a static method.
- tag: method_id_non_static
description: Method_id must resolve to a non-static method.
- tag: method_id_non_abstract
description: Method_id must resolve to a method that has implementation.
- tag: method_id_accessible
description: Method_id must resolve to a method which is accessible.
- tag: constant_string_id
description: Id must resolve into a constant-pool string.
- tag: constant_literalarray_id
description: Id must resolve into a constant literalarray.
- tag: compatible_arguments
description: Arguments provided to a method must be of compatible types.
- tag: method_init_obj
description: Method_id must resolve into initializer for a type other than one-dimensional array.
- tag: branch_target
description: Branch target should point to a beginning of an instruction of the same method.
- tag: field_id_non_static
description: Field_id must resolve to a non-static object field.
- tag: field_id_static
description: Field_id must resolve to a static field.
- tag: field_id_size
description: Field_id must resolve to a field of size corresponding to bytecode.
- tag: valid_in_dynamic_context
description: Instruction is valid only for dynamically-typed language context.
prefixes:
- name: bit
description: Bit operations.
opcode_idx: 0xef
- name: unsigned
description: Unsigned operations.
opcode_idx: 0xee
- name: cast
description: Cast operations.
opcode_idx: 0xed
- name: f32
description: IEEE-754 single precision floating-point operations.
opcode_idx: 0xec
groups:
- title: No operation
description: Perform an operation without behavior.
properties:
- acc_none
exceptions:
- x_none
verification:
- none
pseudo: |
skip
semantics: |-
skip
instructions:
- sig: nop
acc: none
format: [op_none]
opcode_idx: [0x0]
- title: Move register-to-register
description: Move values between registers.
properties:
- acc_none
exceptions:
- x_none
verification:
- v2_type
pseudo: |
vd = vs
semantics: |-
raise exception(WrongRegisterValue) if true that Op == "mov" and type_of(@Vs) is not i32;
raise exception(WrongRegisterValue) if true that Op == "mov.64" and (type_of(@Vs) is not u64 and type_of(@Vs) is not i64);
raise exception(WrongRegisterValue) if true that Op == "mov.obj" and (type_of(@Vs) is not object and type_of(@Vs) is not array);
raise exception(UndefinedSemantics) if true that Op not in [[ "mov", "mov.64", "mov.obj" ]];
Vd <~ Vs
instructions:
- sig: mov v1:out:b32, v2:in:b32
acc: none
format: [op_v1_4_v2_4, op_v1_8_v2_8, op_v1_16_v2_16]
opcode_idx: [0x1, 0x2, 0x3]
- sig: mov.64 v1:out:b64, v2:in:b64
acc: none
format: [op_v1_4_v2_4, op_v1_16_v2_16]
opcode_idx: [0x4, 0x5]
- sig: mov.obj v1:out:ref, v2:in:ref
acc: none
format: [op_v1_4_v2_4, op_v1_8_v2_8, op_v1_16_v2_16]
opcode_idx: [0x6, 0x7, 0x8]
- title: Move immediate-to-register
description: >
Move integer immediate into a register. For short formats immediate is sign extended to operand size.
properties:
- acc_none
exceptions:
- x_none
verification:
- none
pseudo: >
vd = imm
semantics: |-
cases
when Op == "movi" do
raise exception(WrongImmediateValue) if undefined int_of(Imm);
Vd <~ value_of(signed(32), int_of(Imm))
end when;
when Op == "movi.64" do
raise exception(WrongImmediateValue) if undefined int_of(Imm);
Vd <~ value_of(signed(64), int_of(Imm))
end when;
when Op == "fmovi" do
raise exception(WrongImmediateValue) if undefined float_of(Imm);
Vd <~ value_of(float, float_of(Imm))
end when;
when Op == "fmovi.64" do
raise exception(WrongImmediateValue) if undefined float_of(Imm);
Vd <~ value_of(float, float_of(Imm))
end when
else raise exception(UndefinedSemantics) // missed opcode
undefined raise exception(InternalError) // Op is not string
end cases
instructions:
- sig: movi v:out:i32, imm:i32
acc: none
format: [op_v_4_imm_4, op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x9, 0xa, 0xb]
- sig: movi v:out:i32, imm:i32
acc: none
format: [op_v_8_imm_32]
opcode_idx: [0xc]
- sig: movi.64 v:out:i64, imm:i64
acc: none
format: [op_v_8_imm_64]
opcode_idx: [0xd]
- sig: fmovi v:out:f32, imm:f32
acc: none
prefix: f32
format: [pref_op_v_8_imm_32]
opcode_idx: [0x0]
properties: [acc_none, float]
- sig: fmovi.64 v:out:f64, imm:f64
acc: none
format: [op_v_8_imm_64]
opcode_idx: [0xe]
properties: [acc_none, float]
- title: Move null reference into register
description: Move null reference into a register.
properties:
- acc_none
exceptions:
- x_none
verification:
- none
pseudo: >
vd = null
semantics: |-
skip
instructions:
- sig: mov.null v:out:ref
acc: none
format: [op_v_8]
opcode_idx: [0xf]
- title: Load accumulator from register
description: Moves register content into an accumulator.
properties:
- acc_write
exceptions:
- x_none
verification:
- v1_type
pseudo: |
acc = vs
semantics: |-
cases
when Op == "lda" do
raise exception(WrongRegisterValue) if false that type_of(@Vs) is i32;
acc <~ Vs
end when;
when Op == "lda.64" do
raise exception(WrongRegisterValue) if false that type_of(@Vs) is i64 or type_of(@Vs) is u64;
acc <~ Vs
end when;
when Op == "lda.obj" do
raise exception(WrongRegisterValue) if false that type_of(@Vs) is object or type_of(@Vs) is array;
acc <~ Vs
end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: lda v:in:i32
acc: out:i32
format: [op_v_8]
opcode_idx: [0x10]
- sig: lda.64 v:in:b64
acc: out:b64
format: [op_v_8]
opcode_idx: [0x11]
- sig: lda.obj v:in:ref
acc: out:ref
format: [op_v_8]
opcode_idx: [0x12]
- title: Load accumulator from immediate
description: >
Load immediate into accumulator. For short formats immediate is sign extended to operand size.
properties:
- acc_write
exceptions:
- x_none
verification:
- none
pseudo: |
acc = imm
semantics: |-
cases
when Op == "ldai" do
raise exception(WrongImmediateValue) if undefined int_of(Imm);
acc <~ value_of(i32, int_of(Imm))
end when;
when Op == "ldai.64" do
raise exception(WrongImmediateValue) if undefined int_of(Imm);
acc <~ value_of(i64, int_of(Imm))
end when;
when Op == "fldai" do
raise exception(WrongImmediateValue) if undefined float_of(Imm);
acc <~ value_of(float, float_of(Imm))
end when
when Op == "fldai.64" do
raise exception(WrongImmediateValue) if undefined float_of(Imm);
acc <~ value_of(float, float_of(Imm))
end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: ldai imm:i32
acc: out:i32
format: [op_imm_8, op_imm_16]
opcode_idx: [0x13, 0x14]
- sig: ldai imm:i32
acc: out:i32
format: [op_imm_32]
opcode_idx: [0x15]
- sig: ldai.64 imm:i64
acc: out:i64
format: [op_imm_64]
opcode_idx: [0x16]
- sig: fldai imm:f32
acc: out:f32
prefix: f32
format: [pref_op_imm_32]
opcode_idx: [0x1]
properties: [acc_write, float]
- sig: fldai.64 imm:f64
acc: out:f64
format: [op_imm_64]
opcode_idx: [0x17]
properties: [acc_write, float]
- title: Load accumulator from string constant pool
description: >
Load string specified by id into accumulator. In dynamically-typed language context
load string as 'any' value.
properties:
- acc_write
- string_id
- language_type
- maybe_dynamic
exceptions:
- x_none
verification:
- constant_string_id
pseudo: |
acc = load(id)
semantics: |-
acc <~ value_of(string, strOf(StringId))
instructions:
- sig: lda.str string_id
acc: out:ref
format: [op_id_32]
opcode_idx: [0x18]
- title: Create and initialize new constant array
description: >
Create a new single-dimensional constant literal array and put a reference to it into register.
properties:
- acc_none
- literalarray_id
exceptions:
- x_none
verification:
- constant_literalarray_id
pseudo: |
v = load(id)
semantics: |-
skip
instructions:
- sig: lda.const v:out:ref, literalarray_id
acc: none
format: [op_v_8_id_32]
opcode_idx: [0x19]
- title: Load accumulator from type constant pool
description: Load type specified by id into accumulator.
properties:
- acc_write
- type_id
- language_type
exceptions:
- x_none
verification:
- type_id_any_object
pseudo: |
acc = load(id)
semantics: |-
skip
instructions:
- sig: lda.type type_id
acc: out:ref
format: [op_id_16]
opcode_idx: [0x1a]
- title: Load null reference into accumulator
description: Load null reference into accumulator.
properties:
- acc_write
exceptions:
- x_none
verification:
- none
pseudo: |
acc = null
semantics: |-
skip
instructions:
- sig: lda.null
acc: out:ref
format: [op_none]
opcode_idx: [0x1b]
- title: Store accumulator
description: Moves accumulator content into a register.
properties:
- acc_read
exceptions:
- x_none
verification:
- acc_type
pseudo: |
vd = acc
semantics: |-
raise exception(WrongRegisterValue) if true that Op == "sta" and type_of(@acc) is not i32;
raise exception(WrongRegisterValue) if true that Op == "sta.64" and (type_of(@acc) is not i64 and type_of(@acc) is not u64);
raise exception(WrongRegisterValue) if true that Op == "sta.obj" and (type_of(@acc) is not object and type_of(@acc) is not array);
raise exception(UndefinedSemantics) if true that Op not in [[ "sta", "sta.64", "sta.obj" ]];
// raise exception(InternalError) if true that Op is not string // ambig. mixing TypeExp and Exp here... subsort TypeExp < Exp ?
Vd <~ acc
instructions:
- sig: sta v:out:i32
acc: in:i32
format: [op_v_8]
opcode_idx: [0x1c]
- sig: sta.64 v:out:b64
acc: in:b64
format: [op_v_8]
opcode_idx: [0x1d]
- sig: sta.obj v:out:ref
acc: in:ref
format: [op_v_8]
opcode_idx: [0x1e]
- title: Integer comparison
description: Perform specified signed or unsigned integer comparison between register and accumulator.
properties:
- acc_read
- acc_write
exceptions:
- x_none
verification:
- acc_type
- v1_type
pseudo: |
if acc < vs then
acc = -1
else if acc == vs then
acc = 0
else
acc = 1
end
semantics: |-
raise exception(WrongRegisterValue) if false that type_of(@acc) is type_of(@Vs);
raise exception(WrongRegisterValue) if true that Op == "cmp.64" and type_of(@acc) is not i64;
raise exception(WrongRegisterValue) if true that Op == "ucmp" and type_of(@acc) is not u32;
raise exception(WrongRegisterValue) if true that Op == "ucmp.64" and type_of(@acc) is not u64;
raise exception(UndefinedSemantics) if true that Op not in [[ "cmp.64", "ucmp", "ucmp.64" ]];
cases
when @acc < @Vs do acc <~ value(i32, -1) end when;
when @acc == @Vs do acc <~ value(i32, 0) end when;
when @acc > @Vs do acc <~ value(i32, 1) end when
undefined raise exception(InternalError)
end cases
instructions:
- sig: cmp.64 v:in:i64
acc: inout:i64->i32
format: [op_v_8]
opcode_idx: [0x1f]
- sig: ucmp v:in:u32
acc: inout:u32->i32
prefix: unsigned
format: [pref_op_v_8]
opcode_idx: [0x0]
- sig: ucmp.64 v:in:u64
acc: inout:u64->i32
prefix: unsigned
format: [pref_op_v_8]
opcode_idx: [0x1]
- title: Floating-point comparison
description: Perform specified floating point comparison between register and accumulator.
properties:
- acc_read
- acc_write
- float
exceptions:
- x_none
verification:
- acc_type
- v1_type
pseudo: |
if isnan(acc) or isnan(vs) then
switch (op)
case fcmpg:
case fcmpg.64:
acc = 1
case fcmpl:
case fcmpl.64:
acc = -1
else
if acc < vs then
acc = -1
else if acc == vs then
acc = 0
else
acc = 1
end
end
semantics: |-
// strange semantics...
if isnan(@acc) or isnan(@Vs) then
cases
when Op in [[ "fcmpg", "fcmpg.64" ]] do acc <~ value(i32, 1) end when;
when Op in [[ "fcmpl", "fcmpl.64" ]] do acc <~ value(i32, -1) end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
else
cases
when @acc < @Vs do acc <~ value(i32, -1) end when;
when @acc == @Vs do acc <~ value(i32, 0) end when;
when @acc > @Vs do acc <~ value(i32, 1) end when
undefined raise exception(InternalError)
end cases
undefined raise exception(WrongRegisterValue)
end if
instructions:
- sig: fcmpl v:in:f32
acc: inout:f32->i32
prefix: f32
format: [pref_op_v_8]
opcode_idx: [0x2]
- sig: fcmpl.64 v:in:f64
acc: inout:f64->i32
format: [op_v_8]
opcode_idx: [0x20]
- sig: fcmpg v:in:f32
acc: inout:f32->i32
prefix: f32
format: [pref_op_v_8]
opcode_idx: [0x3]
- sig: fcmpg.64 v:in:f64
acc: inout:f64->i32
format: [op_v_8]
opcode_idx: [0x21]
- title: Unconditional jump
description: >
Unconditionally transfer execution to an instruction at offset bytes from the beginning of the current
instruction. Offset is sign extended to the size of instruction address.
properties:
- acc_none
- jump
exceptions:
- x_none
verification:
- branch_target
pseudo: |
pc += imm
semantics: |-
perform_jump(LabelId)
instructions:
- sig: jmp imm:i32
acc: none
format: [op_imm_8, op_imm_16, op_imm_32]
opcode_idx: [0x22, 0x23, 0x24]
- title: Conditional object comparison jump
description: >
Transfer execution to an instruction at offset bytes from the beginning of the current instruction if
object references in accumulator and source register compare as specified. Offset is sign extended to the size of
instruction address.
properties:
- acc_read
- jump
- conditional
exceptions:
- x_none
verification:
- branch_target
- acc_obj_or_null
- v1_obj_or_null
pseudo: |
switch (cc)
case eq:
if acc == vs then
pc += imm
end
case ne:
if acc != vs then
pc += imm
end
semantics:
skip
instructions:
- sig: jeq.obj v:in:ref, imm:i32
acc: in:ref
format: [op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x25, 0x26]
- sig: jne.obj v:in:ref, imm:i32
acc: in:ref
format: [op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x27, 0x28]
- title: Conditional compared to null jump
description: >
Transfer execution to an instruction at offset bytes from the beginning of the current instruction if
object reference in accumulator compares with null as specified. Offset is sign extended to the size of
instruction address.
properties:
- acc_read
- jump
- conditional
exceptions:
- x_none
verification:
- branch_target
- acc_obj_or_null
pseudo: |
switch (cc)
case eq:
if acc == null then
pc += imm
end
case ne:
if acc != null then
pc += imm
end
semantics:
skip
instructions:
- sig: jeqz.obj imm:i32
acc: in:ref
format: [op_imm_8, op_imm_16]
opcode_idx: [0x29, 0x2a]
- sig: jnez.obj imm:i32
acc: in:ref
format: [op_imm_8, op_imm_16]
opcode_idx: [0x2b, 0x2c]
- title: Conditional compared to zero jump
description: >
Transfer execution to an instruction at offset bytes from the beginning of the current instruction if
signed 32-bit integer in accumulator compares with 0 as specified. Offset is sign extended to the size
of instruction address.
properties:
- acc_read
- jump
- conditional
exceptions:
- x_none
verification:
- branch_target
- acc_type
pseudo: |
switch (cc)
case eq:
if acc == 0 then
pc += imm
end
case ne:
if acc != 0 then
pc += imm
end
case lt:
if acc < 0 then
pc += imm
end
case gt:
if acc > 0 then
pc += imm
end
case le:
if acc <= 0 then
pc += imm
end
case ge:
if acc >= 0 then
pc += imm
end
semantics: |-
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
Acc := int_of(@acc);
cases
when Op == "jeqz" and Acc == 0 do perform_jump(LabelId) end when;
when Op == "jnez" and Acc != 0 do perform_jump(LabelId) end when;
when Op == "jltz" and Acc < 0 do perform_jump(LabelId) end when;
when Op == "jgtz" and Acc > 0 do perform_jump(LabelId) end when;
when Op == "jlez" and Acc <= 0 do perform_jump(LabelId) end when;
when Op == "jgez" and Acc >= 0 do perform_jump(LabelId) end when
else skip //branch not taken
undefined raise exception(InternalError)
end cases
instructions:
- sig: jeqz imm:i32
acc: in:i32
format: [op_imm_8, op_imm_16]
opcode_idx: [0x2d, 0x2e]
- sig: jnez imm:i32
acc: in:i32
format: [op_imm_8, op_imm_16]
opcode_idx: [0x2f, 0x30]
- sig: jltz imm:i32
acc: in:i32
format: [op_imm_8, op_imm_16]
opcode_idx: [0x31, 0x32]
- sig: jgtz imm:i32
acc: in:i32
format: [op_imm_8, op_imm_16]
opcode_idx: [0x33, 0x34]
- sig: jlez imm:i32
acc: in:i32
format: [op_imm_8, op_imm_16]
opcode_idx: [0x35, 0x36]
- sig: jgez imm:i32
acc: in:i32
format: [op_imm_8, op_imm_16]
opcode_idx: [0x37, 0x38]
- title: Conditional compared to register jump
description: >
Transfer execution to an instruction at offset bytes from the beginning of the current instruction if signed
32-bit integers in accumulator and register compare as specified. Offset is sign extended to the size of
instruction address.
properties:
- acc_read
- jump
- conditional
exceptions:
- x_none
verification:
- branch_target
- acc_type
- v1_type
pseudo: |
diff = signed_cmp(acc, vs)
switch (cc)
case eq:
if diff == 0 then
pc += imm
end
case ne:
if diff != 0 then
pc += imm
end
case lt:
if diff < 0 then
pc += imm
end
case gt:
if diff > 0 then
pc += imm
end
case le:
if diff <= 0 then
pc += imm
end
case ge:
if diff >= 0 then
pc += imm
end
semantics: |-
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
raise exception(WrongRegisterValue) if false that type_of(@Vs) is i32;
Acc := int_of(@acc);
Vs := int_of(@Vs);
cases
when Op == "jeq" and Acc == Vs do perform_jump(LabelId) end when;
when Op == "jne" and Acc != Vs do perform_jump(LabelId) end when;
when Op == "jlt" and Acc < Vs do perform_jump(LabelId) end when;
when Op == "jgt" and Acc > Vs do perform_jump(LabelId) end when;
when Op == "jle" and Acc <= Vs do perform_jump(LabelId) end when;
when Op == "jge" and Acc >= Vs do perform_jump(LabelId) end when
else skip //branch not taken
undefined raise exception(InternalError)
end cases
instructions:
- sig: jeq v:in:i32, imm:i32
acc: in:i32
format: [op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x39, 0x3a]
- sig: jne v:in:i32, imm:i32
acc: in:i32
format: [op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x3b, 0x3c]
- sig: jlt v:in:i32, imm:i32
acc: in:i32
format: [op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x3d, 0x3e]
- sig: jgt v:in:i32, imm:i32
acc: in:i32
format: [op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x3f, 0x40]
- sig: jle v:in:i32, imm:i32
acc: in:i32
format: [op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x41, 0x42]
- sig: jge v:in:i32, imm:i32
acc: in:i32
format: [op_v_8_imm_8, op_v_8_imm_16]
opcode_idx: [0x43, 0x44]
- title: Floating-point unary
description: Perform specified floating-point operation on accumulator
properties:
- acc_read
- acc_write
- float
exceptions:
- x_none
verification:
- acc_type
pseudo: |
switch (op)
case fneg:
case fneg.64:
acc = -acc
semantics: |-
raise exception(WrongRegisterValue) if false that type_of(@acc) is float;
acc <~ neg(@acc)
instructions:
- sig: fneg
acc: inout:f32
prefix: f32
format: [pref_op_none]
opcode_idx: [0x4]
- sig: fneg.64
acc: inout:f64
format: [op_none]
opcode_idx: [0x45]
- title: Unary
description: Perform specified operation on accumulator
properties:
- acc_read
- acc_write
exceptions:
- x_none
verification:
- acc_type
pseudo: |
switch (op)
case neg:
case neg.64:
acc = -acc
case not:
case not.64:
acc = ~acc
semantics: |-
Acc := @acc;
cases
when Op == "neg" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32;
acc <~ neg(Acc)
end when;
when Op == "neg.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64;
acc <~ neg(Acc)
end when;
when Op == "not" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32;
acc <~ neg(Acc) - value(i32, 1)
end when;
when Op == "not.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64;
acc <~ neg(Acc) - value(i64, 1)
end when;
else raise exception (UndefinedSemantics)
undefined raise exception (InternalError)
end cases
instructions:
- sig: neg
acc: inout:i32
format: [op_none]
opcode_idx: [0x46]
- sig: neg.64
acc: inout:i64
format: [op_none]
opcode_idx: [0x47]
- sig: not
acc: inout:i32
prefix: bit
format: [pref_op_none]
opcode_idx: [0x0]
- sig: not.64
acc: inout:i64
prefix: bit
format: [pref_op_none]
opcode_idx: [0x1]
- title: Two address binary operation on accumulator
description: Perform specified binary operation on accumulator and register and store result into accumulator
properties:
- acc_read
- acc_write
exceptions:
- x_none
verification:
- acc_type
- v1_type
pseudo: |
switch (op)
case add2:
acc = (acc + vs) % 2^32
case add2.64:
acc = (acc + vs) % 2^64
case sub2:
acc = (acc - vs) % 2^32
case sub2.64:
acc = (acc - vs) % 2^64
case mul2:
acc = (acc * vs) % 2^32
case mul2.64:
acc = (acc * vs) % 2^64
case and2:
acc = acc & vs
case and2.64:
acc = acc & vs
case or2:
acc = acc | vs
case or2.64:
acc = acc | vs
case xor2:
acc = acc ^ vs
case xor2.64:
acc = acc ^ vs
case shl2:
acc = acc << (vs & 0x1f)
case shl2.64:
acc = acc << (vs & 0x3f)
case shr2:
acc = acc >> (vs & 0x1f)
case shr2.64:
acc = acc >> (vs & 0x3f)
case ashr2:
acc = arith_shift_right(acc, vs & 0x1f)
case ashr2.64:
acc = arith_shift_right(acc, vs & 0x3f)
semantics: |-
Acc := @acc;
Vs := @Vs;
cases
when Op == "add2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc + Vs)
end when;
when Op == "add2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc + Vs)
end when;
when Op == "sub2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc - Vs)
end when;
when Op == "sub2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc - Vs)
end when;
when Op == "mul2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc * Vs)
end when;
when Op == "mul2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc * Vs)
end when;
when Op == "and2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc & Vs)
end when;
when Op == "and2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc & Vs)
end when;
when Op == "or2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc | Vs)
end when;
when Op == "or2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc | Vs)
end when;
when Op == "xor2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc ^ Vs)
end when;
when Op == "xor2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc ^ Vs)
end when;
when Op == "shl2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc << Vs)
end when;
when Op == "shl2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc << Vs)
end when;
when Op == "shr2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc >> Vs)
end when;
when Op == "shr2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc >> Vs)
end when
// case ashr2:
// acc = arith_shift_right(acc, vs & 0x1f)
// case ashr2.64:
// acc = arith_shift_right(acc, vs & 0x3f)
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: add2 v:in:i32
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x48]
- sig: add2.64 v:in:i64
acc: inout:i64
format: [op_v_8]
opcode_idx: [0x49]
- sig: sub2 v:in:i32
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x4a]
- sig: sub2.64 v:in:i64
acc: inout:i64
format: [op_v_8]
opcode_idx: [0x4b]
- sig: mul2 v:in:i32
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x4c]
- sig: mul2.64 v:in:i64
acc: inout:i64
format: [op_v_8]
opcode_idx: [0x4d]
- sig: and2 v:in:i32
acc: inout:i32
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0x2]
- sig: and2.64 v:in:i64
acc: inout:i64
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0x3]
- sig: or2 v:in:i32
acc: inout:i32
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0x4]
- sig: or2.64 v:in:i64
acc: inout:i64
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0x5]
- sig: xor2 v:in:i32
acc: inout:i32
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0x6]
- sig: xor2.64 v:in:i64
acc: inout:i64
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0x7]
- sig: shl2 v:in:i32
acc: inout:i32
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0x8]
- sig: shl2.64 v:in:i64
acc: inout:i64
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0x9]
- sig: shr2 v:in:i32
acc: inout:i32
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0xa]
- sig: shr2.64 v:in:i64
acc: inout:i64
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0xb]
- sig: ashr2 v:in:i32
acc: inout:i32
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0xc]
- sig: ashr2.64 v:in:i64
acc: inout:i64
prefix: bit
format: [pref_op_v_8]
opcode_idx: [0xd]
- title: Two address floating-point binary operation on accumulator
description: |
Perform specified floating-point binary operation on accumulator and register and store result into accumulator.
The results of instructions correspond IEEE-754 arithmetic rules.
- Any operation with NaN results to NaN value.
- The sum of opposite infinities or the difference of the same sign infinities is NaN.
- Division is NaN if Infinity is divided by Infinity.
- Division is NaN if zero is divided by zero.
- Multiplication is NaN if zero is multiplied by infinity.
- The sign of division or multiplication result is positive if both values have the same sign, negative if the values have different sign.
- Division is infinity if any non zero value is divided by zero.
- Multiplication is infinity if any non zero value is multiplied by infinity.
- 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.
- The sum or the difference of infinity and any finite value is infinity. The sign of result matches the sign of infinity.
- 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.
properties:
- acc_read
- acc_write
- float
exceptions:
- x_none
verification:
- acc_type
- v1_type
pseudo: |
switch (op)
case fadd2:
case fadd2.64:
acc = acc + vs
case fsub2:
case fsub2.64:
acc = acc - vs
case fmul2:
case fmul2.64:
acc = acc * vs
case fdiv2:
case fdiv2.64:
acc = acc / vs
case fmod2:
case fmod2.64:
acc = acc % vs
semantics: |-
raise exception(WrongRegisterValue) if false that type_of(@acc) is float;
raise exception(WrongRegisterValue) if false that type_of(@Vs) is float;
Acc := float_of(@acc);
Vs := float_of(@Vs);
cases
when Op == "fadd2" or Op == "fadd2.64" do acc <~ Acc + Vs end when;
when Op == "fsub2" or Op == "fsub2.64" do acc <~ Acc - Vs end when;
when Op == "fmul2" or Op == "fmul2.64" do acc <~ Acc * Vs end when;
when Op == "fdiv2" or Op == "fdiv2.64" do acc <~ Acc / Vs end when;
when Op == "fmod2" or Op == "fmod2.64" do acc <~ Acc % Vs end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: fadd2 v:in:f32
acc: inout:f32
prefix: f32
format: [pref_op_v_8]
opcode_idx: [0x5]
- sig: fadd2.64 v:in:f64
acc: inout:f64
format: [op_v_8]
opcode_idx: [0x4e]
- sig: fsub2 v:in:f32
acc: inout:f32
prefix: f32
format: [pref_op_v_8]
opcode_idx: [0x6]
- sig: fsub2.64 v:in:f64
acc: inout:f64
format: [op_v_8]
opcode_idx: [0x4f]
- sig: fmul2 v:in:f32
acc: inout:f32
prefix: f32
format: [pref_op_v_8]
opcode_idx: [0x7]
- sig: fmul2.64 v:in:f64
acc: inout:f64
format: [op_v_8]
opcode_idx: [0x50]
- sig: fdiv2 v:in:f32
acc: inout:f32
prefix: f32
format: [pref_op_v_8]
opcode_idx: [0x8]
- sig: fdiv2.64 v:in:f64
acc: inout:f64
format: [op_v_8]
opcode_idx: [0x51]
- sig: fmod2 v:in:f32
acc: inout:f32
prefix: f32
format: [pref_op_v_8]
opcode_idx: [0x9]
- sig: fmod2.64 v:in:f64
acc: inout:f64
format: [op_v_8]
opcode_idx: [0x52]
- title: Two address integer division and modulo on accumulator
description: Perform integer division or modulo on accumulator and register and store result into accumulator
properties:
- acc_read
- acc_write
exceptions:
- x_arith
verification:
- acc_type
- v1_type
pseudo: |
if vs == 0 then
throw ArithmeticException
end
switch (op)
case div:
if acc == INT32_MIN and vs == -1 then
acc = INT32_MIN
else
acc = acc / vs
end
case div.64:
if acc == INT64_MIN and vs == -1 then
acc = INT64_MIN
else
acc = acc / vs
end
case divu:
case divu.64:
acc = acc / vs
case mod:
if acc == INT32_MIN and vs == -1 then
acc = 0
else
acc = acc % vs
end
case mod.64:
if acc == INT64_MIN and vs == -1 then
acc = 0
else
acc = acc % vs
end
case modu:
case modu.64:
acc = acc % vs
semantics: |-
Acc := @acc;
Vs := @Vs;
cases
when Op == "div2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc / Vs)
end when;
when Op == "div2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc / Vs)
end when;
when Op == "mod2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32 and type_of(Vs) is i32;
acc <~ truncate_int(Acc % Vs)
end when;
when Op == "mod2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is i64 and type_of(Vs) is i64;
acc <~ truncate_int(Acc % Vs)
end when;
when Op == "divu2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is u32 and type_of(Vs) is u32;
acc <~ truncate_int(Acc / Vs)
end when;
when Op == "divu2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is u64 and type_of(Vs) is u64;
acc <~ truncate_int(Acc / Vs)
end when;
when Op == "modu2" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is u32 and type_of(Vs) is u32;
acc <~ truncate_int(Acc % Vs)
end when;
when Op == "modu2.64" do
raise exception(WrongRegisterValue) if false that type_of(Acc) is u64 and type_of(Vs) is u64;
acc <~ truncate_int(Acc % Vs)
end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: div2 v:in:i32
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x53]
- sig: div2.64 v:in:i64
acc: inout:i64
format: [op_v_8]
opcode_idx: [0x54]
- sig: mod2 v:in:i32
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x55]
- sig: mod2.64 v:in:i64
acc: inout:i64
format: [op_v_8]
opcode_idx: [0x56]
- sig: divu2 v:in:u32
acc: inout:u32
prefix: unsigned
format: [pref_op_v_8]
opcode_idx: [0x2]
- sig: divu2.64 v:in:u64
acc: inout:u64
prefix: unsigned
format: [pref_op_v_8]
opcode_idx: [0x3]
- sig: modu2 v:in:u32
acc: inout:u32
prefix: unsigned
format: [pref_op_v_8]
opcode_idx: [0x4]
- sig: modu2.64 v:in:u64
acc: inout:u64
prefix: unsigned
format: [pref_op_v_8]
opcode_idx: [0x5]
- title: Two address binary operation with immediate on accumulator
description: >
Perform specified binary operation on accumulator and immediate and store result into accumulator.
Immediate is sign extended to operand size.
properties:
- acc_write
- acc_read
exceptions:
- x_none
verification:
- acc_type
pseudo: |
switch (op)
case addi:
acc = (acc + imm) % 2^32
case subi:
acc = (acc - imm) % 2^32
case muli:
acc = (acc * imm) % 2^32
case andi:
acc = acc & imm
case ori:
acc = acc | imm
case xori:
acc = acc ^ imm
case shli:
acc = acc << (imm & 0x1f)
case shri:
acc = acc >> (imm & 0x1f)
case ashri:
acc = arith_shift_right(acc, imm & 0x1f)
semantics: |-
Acc := @acc;
raise exception(WrongRegisterValue) if false that type_of(Acc) is i32;
Imm := value_of(i32, int_of(Imm));
raise exception(WrongImmediateValue) if undefined Imm;
cases
when Op == "addi" do
acc <~ truncate_int(Acc + Imm)
end when;
when Op == "subi" do
acc <~ truncate_int(Acc - Imm)
end when;
when Op == "muli" do
acc <~ truncate_int(Acc * Imm)
end when;
when Op == "andi" do
acc <~ Acc & Imm
end when;
when Op == "ori" do
acc <~ Acc | Imm
end when;
when Op == "xori" do
acc <~ Acc ^ Imm
end when;
when Op == "shli" do
acc <~ truncate_int(Acc << Imm)
end when;
when Op == "shri" do
acc <~ Acc >> Imm
end when
//when Op == "ashri" do
// acc <~
//end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: addi imm:i32
acc: inout:i32
format: [op_imm_8]
opcode_idx: [0x57]
- sig: subi imm:i32
acc: inout:i32
format: [op_imm_8]
opcode_idx: [0x58]
- sig: muli imm:i32
acc: inout:i32
format: [op_imm_8]
opcode_idx: [0x59]
- sig: andi imm:i32
acc: inout:i32
format: [op_imm_32]
opcode_idx: [0x5a]
- sig: ori imm:i32
acc: inout:i32
format: [op_imm_32]
opcode_idx: [0x5b]
- sig: xori imm:i32
acc: inout:i32
prefix: bit
format: [pref_op_imm_32]
opcode_idx: [0xe]
- sig: shli imm:i32
acc: inout:i32
format: [op_imm_8]
opcode_idx: [0x5c]
- sig: shri imm:i32
acc: inout:i32
format: [op_imm_8]
opcode_idx: [0x5d]
- sig: ashri imm:i32
acc: inout:i32
format: [op_imm_8]
opcode_idx: [0x5e]
- title: Two address integer division or modulo with immediate on accumulator
description: >
Perform two address integer division or modulo on accumulator and immediate and store result into accumulator.
Immediate is sign extended to operand size.
properties:
- acc_write
- acc_read
exceptions:
- x_arith
verification:
- acc_type
pseudo: |
if imm == 0 then
throw ArithmeticException
end
switch(op)
case divi:
if acc == INT32_MIN and imm == -1 then
acc = INT32_MIN
else
acc = acc / imm
end
case modi:
if acc == INT32_MIN and imm == -1 then
acc = 0
else
acc = acc % imm
end
semantics: |-
Vs := @Vs;
Imm := value_of(i32, int_of(Imm));
raise exception(WrongRegisterValue) if false that type_of(Vs) is i32;
raise exception(WrongImmediateValue) if undefined Imm;
cases
when Op == "div" do
acc <~ Vs / Imm
end when;
when Op == "mod" do
acc <~ Vs % Imm
end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: divi imm:i32
acc: inout:i32
format: [op_imm_8]
opcode_idx: [0x5f]
- sig: modi imm:i32
acc: inout:i32
format: [op_imm_8]
opcode_idx: [0x60]
- title: Three address binary operation
description: Perform specified binary operation on two registers and store result into accumulator
properties:
- acc_write
exceptions:
- x_none
verification:
- v1_type
- v2_type
pseudo: |
switch (op)
case add:
acc = (vs1 + vs2) % 2^32
case sub:
acc = (vs1 - vs2) % 2^32
case mul:
acc = (vs1 * vs2) % 2^32
case and:
acc = vs1 & vs2
case or:
acc = vs1 | vs2
case xor:
acc = vs1 ^ vs2
case shl:
acc = vs1 << (vs2 & 0x1f)
case shr:
acc = vs1 >> (vs2 & 0x1f)
case ashr:
acc = arith_shift_right(vs1, vs2 & 0x1f)
semantics: |-
Vs1 := @Vs1;
Vs2 := @Vs2;
raise exception(WrongRegisterValue) if false that type_of(Vs1) is i32 and type_of(Vs2) is i32;
cases
when Op == "add" do
acc <~ truncate_int(Vs1 + Vs2)
end when;
when Op == "sub" do
acc <~ truncate_int(Vs1 - Vs2)
end when;
when Op == "mul" do
acc <~ truncate_int(Vs1 * Vs2)
end when;
when Op == "and" do
acc <~ truncate_int(Vs1 & Vs2)
end when;
when Op == "or" do
acc <~ truncate_int(Vs1 | Vs2)
end when;
when Op == "xor" do
acc <~ truncate_int(Vs1 ^ Vs2)
end when;
when Op == "shl" do
acc <~ truncate_int(Vs1 << Vs2)
end when;
when Op == "shr" do
acc <~ truncate_int(Vs1 >> Vs2)
end when
// when Op == "ashr" do
// end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: add v1:in:i32, v2:in:i32
acc: out:i32
format: [op_v1_4_v2_4]
opcode_idx: [0x61]
- sig: sub v1:in:i32, v2:in:i32
acc: out:i32
format: [op_v1_4_v2_4]
opcode_idx: [0x62]
- sig: mul v1:in:i32, v2:in:i32
acc: out:i32
format: [op_v1_4_v2_4]
opcode_idx: [0x63]
- sig: and v1:in:i32, v2:in:i32
acc: out:i32
prefix: bit
format: [pref_op_v1_4_v2_4]
opcode_idx: [0xf]
- sig: or v1:in:i32, v2:in:i32
acc: out:i32
prefix: bit
format: [pref_op_v1_4_v2_4]
opcode_idx: [0x10]
- sig: xor v1:in:i32, v2:in:i32
acc: out:i32
prefix: bit
format: [pref_op_v1_4_v2_4]
opcode_idx: [0x11]
- sig: shl v1:in:i32, v2:in:i32
acc: out:i32
prefix: bit
format: [pref_op_v1_4_v2_4]
opcode_idx: [0x12]
- sig: shr v1:in:i32, v2:in:i32
acc: out:i32
prefix: bit
format: [pref_op_v1_4_v2_4]
opcode_idx: [0x13]
- sig: ashr v1:in:i32, v2:in:i32
acc: out:i32
prefix: bit
format: [pref_op_v1_4_v2_4]
opcode_idx: [0x14]
- title: Three address integer division or modulo
description: Perform integer division or modulo on two registers and store result into accumulator
properties:
- acc_write
exceptions:
- x_arith
verification:
- v1_type
- v2_type
pseudo: |
if vs2 == 0 then
throw ArithmeticException
end
switch(op)
case div:
if vs1 == INT32_MIN and vs2 == -1 then
acc = INT32_MIN
else
acc = vs1 / vs2
end
case mod:
if vs1 == INT32_MIN and vs2 == -1 then
acc = 0
else
acc = vs1 % vs2
end
semantics: |-
Vs1 := @Vs1;
Vs2 := @Vs2;
raise exception(WrongRegisterValue) if false that type_of(Vs1) is i32 and type_of(Vs2) is i32;
cases
when Op == "div" do
acc <~ Vs1 / Vs2
end when;
when Op == "mod" do
acc <~ Vs1 % Vs2
end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: div v1:in:i32, v2:in:i32
acc: out:i32
format: [op_v1_4_v2_4]
opcode_idx: [0x64]
- sig: mod v1:in:i32, v2:in:i32
acc: out:i32
format: [op_v1_4_v2_4]
opcode_idx: [0x65]
- title: Increment register with immediate
description: >
Increment virtual register by specified immediate. Immediate is sign extended to operand size.
properties:
- acc_none
exceptions:
- x_none
verification:
- v1_i32
pseudo: |
vx = (vx + imm) % 2^32
semantics: |-
V := @Vx;
Imm := value_of(i32, int_of(Imm));
raise exception(WrongRegisterValue) if false that type_of(V) is i32;
raise exception(WrongImmediateValue) if undefined int_of(Imm);
Vx <~ V + Imm
instructions:
- sig: inci v:inout:i32, imm:i32
acc: none
format: [op_v_4_imm_4]
opcode_idx: [0x66]
- title: Conversions between integer and floating point types
description: |
Perform specified primitive type conversion of accumulator.
Conversion from floating-point types to integer one obeys the following rules.
- It is rounding toward zero.
- If converted integer is less than minimal value for destination type, the result is minimal value for that type.
- If source is negative infinity, the result is minimal value for destination type.
- If converted integer is greater than maximum value for destination type, the result is maximum value for that type.
- If source is positive infinity, the result is maximum value for destination type.
- If source is NaN, the result is equal to 0.
properties:
- acc_read
- acc_write
- float
exceptions:
- x_none
verification:
- acc_type
pseudo: |
(dest_type) acc = (src_type) acc
semantics: |-
cases
when Op == "i32tof32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
acc <~ i32tof32(@acc)
end when;
when Op == "i32tof64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
acc <~ i32tof64(@acc)
end when;
when Op == "u32tof32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u32;
acc <~ u32tof32(@acc)
end when;
when Op == "u32tof64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u32;
acc <~ u32tof64(@acc)
end when;
when Op == "i64tof32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i64;
acc <~ i64tof32(@acc)
end when;
when Op == "i64tof64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i64;
acc <~ i64tof64(@acc)
end when;
when Op == "u64tof32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u64;
acc <~ u64tof32(@acc)
end when;
when Op == "u64tof64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u64;
acc <~ u64tof64(@acc)
end when;
when Op == "f32toi32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f32;
acc <~ f32toi32(@acc)
end when;
when Op == "f32tou32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f32;
acc <~ f32tou32(@acc)
end when;
when Op == "f32toi64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f32;
acc <~ f32toi64(@acc)
end when;
when Op == "f32tou64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f32;
acc <~ f32tou64(@acc)
end when
when Op == "f64toi32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f64;
acc <~ f64toi32(@acc)
end when;
when Op == "f64tou32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f64;
acc <~ f64tou32(@acc)
end when;
when Op == "f64toi64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f64;
acc <~ f64toi64(@acc)
end when;
when Op == "f64tou64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f64;
acc <~ f64tou64(@acc)
end when
when Op == "f64tof32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is f64;
acc <~ f64tof32(@acc)
end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: i32tof32
acc: inout:i32->f32
prefix: f32
format: [pref_op_none]
opcode_idx: [0xa]
- sig: i32tof64
acc: inout:i32->f64
prefix: cast
format: [pref_op_none]
opcode_idx: [0x0]
- sig: u32tof32
acc: inout:u32->f32
prefix: f32
format: [pref_op_none]
opcode_idx: [0xb]
- sig: u32tof64
acc: inout:u32->f64
prefix: cast
format: [pref_op_none]
opcode_idx: [0x1]
- sig: i64tof32
acc: inout:i64->f32
prefix: f32
format: [pref_op_none]
opcode_idx: [0xc]
- sig: i64tof64
acc: inout:i64->f64
prefix: cast
format: [pref_op_none]
opcode_idx: [0x2]
- sig: u64tof32
acc: inout:u64->f32
prefix: f32
format: [pref_op_none]
opcode_idx: [0xd]
- sig: u64tof64
acc: inout:u64->f64
prefix: cast
format: [pref_op_none]
opcode_idx: [0x3]
- sig: f32tof64
acc: inout:f32->f64
prefix: f32
format: [pref_op_none]
opcode_idx: [0xe]
- sig: f32toi32
acc: inout:f32->i32
prefix: f32
format: [pref_op_none]
opcode_idx: [0xf]
- sig: f32toi64
acc: inout:f32->i64
prefix: f32
format: [pref_op_none]
opcode_idx: [0x10]
- sig: f32tou32
acc: inout:f32->u32
prefix: f32
format: [pref_op_none]
opcode_idx: [0x11]
- sig: f32tou64
acc: inout:f32->u64
prefix: f32
format: [pref_op_none]
opcode_idx: [0x12]
- sig: f64toi32
acc: inout:f64->i32
prefix: cast
format: [pref_op_none]
opcode_idx: [0x4]
- sig: f64toi64
acc: inout:f64->i64
prefix: cast
format: [pref_op_none]
opcode_idx: [0x5]
- sig: f64tou32
acc: inout:f64->u32
prefix: cast
format: [pref_op_none]
opcode_idx: [0x6]
- sig: f64tou64
acc: inout:f64->u64
prefix: cast
format: [pref_op_none]
opcode_idx: [0x7]
- sig: f64tof32
acc: inout:f64->f32
prefix: f32
format: [pref_op_none]
opcode_idx: [0x13]
- title: Conversions from integer types to u1
description: |
Conversion from integer types to u1 obeys the following rules.
- If converted integer is not equal to zero, the result is 1.
- Otherwise the result is 0.
properties:
- acc_read
- acc_write
exceptions:
- x_none
verification:
- acc_type
pseudo: |
(dest_type) acc = (src_type) acc
semantics: |-
cases
when Op == "i32tou1" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
acc <~ i32tou1(@acc)
end when
when Op == "i64tou1" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i64;
acc <~ i64tou1(@acc)
end when
when Op == "u32tou1" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u32;
acc <~ u32tou1(@acc)
end when
when Op == "u64tou1" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u64;
acc <~ u64tou1(@acc)
end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: i32tou1
acc: inout:i32->u1
prefix: cast
format: [pref_op_none]
opcode_idx: [0x8]
- sig: i64tou1
acc: inout:i64->u1
prefix: cast
format: [pref_op_none]
opcode_idx: [0x9]
- sig: u32tou1
acc: inout:u32->u1
prefix: cast
format: [pref_op_none]
opcode_idx: [0xa]
- sig: u64tou1
acc: inout:u64->u1
prefix: cast
format: [pref_op_none]
opcode_idx: [0xb]
- title: Integer truncations and extensions.
description: >
Perform specified integer extension or truncations of accumulator.
Truncations discard all but N lowest-order bits, where N is the bit size of destination type.
If extension bytecode treats its source as signed integer, the value is sign-extended to destination type.
If extension bytecode treats its source as unsigned integer, the value is zero-extended to destination type.
properties:
- acc_read
- acc_write
exceptions:
- x_none
verification:
- acc_type
pseudo: |
(dest_type) acc = (src_type) acc
semantics: |-
cases
when Op == "i32toi64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
acc <~ i32toi64(@acc)
end when;
when Op == "i32toi16" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
acc <~ i32toi16(@acc)
end when;
when Op == "i32tou16" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
acc <~ i32tou16(@acc)
end when;
when Op == "i32toi8" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
acc <~ i32toi8(@acc)
end when;
when Op == "i32tou8" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i32;
acc <~ i32tou8(@acc)
end when;
when Op == "i64toi32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is i64;
acc <~ i64toi32(@acc)
end when;
when Op == "u32toi64" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u32;
acc <~ u32toi64(@acc)
end when
when Op == "u32toi16" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u32;
acc <~ u32toi16(@acc)
end when
when Op == "u32tou16" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u32;
acc <~ u32tou16(@acc)
end when
when Op == "u32toi8" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u32;
acc <~ u32toi8(@acc)
end when
when Op == "u32tou8" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u32;
acc <~ u32tou8(@acc)
end when
when Op == "u64toi32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u64;
acc <~ u64toi32(@acc)
end when
when Op == "u64tou32" do
raise exception(WrongRegisterValue) if false that type_of(@acc) is u64;
acc <~ u64tou32(@acc)
end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: i32toi64
acc: inout:i32->i64
prefix: cast
format: [pref_op_none]
opcode_idx: [0xc]
- sig: i32toi16
acc: inout:i32->i16
prefix: cast
format: [pref_op_none]
opcode_idx: [0xd]
- sig: i32tou16
acc: inout:i32->u16
prefix: cast
format: [pref_op_none]
opcode_idx: [0xe]
- sig: i32toi8
acc: inout:i32->i8
prefix: cast
format: [pref_op_none]
opcode_idx: [0xf]
- sig: i32tou8
acc: inout:i32->u8
prefix: cast
format: [pref_op_none]
opcode_idx: [0x10]
- sig: i64toi32
acc: inout:i64->i32
prefix: cast
format: [pref_op_none]
opcode_idx: [0x11]
- sig: u32toi64
acc: inout:u32->i64
prefix: cast
format: [pref_op_none]
opcode_idx: [0x12]
- sig: u32toi16
acc: inout:u32->i16
prefix: cast
format: [pref_op_none]
opcode_idx: [0x13]
- sig: u32tou16
acc: inout:u32->u16
prefix: cast
format: [pref_op_none]
opcode_idx: [0x14]
- sig: u32toi8
acc: inout:u32->i8
prefix: cast
format: [pref_op_none]
opcode_idx: [0x15]
- sig: u32tou8
acc: inout:u32->u8
prefix: cast
format: [pref_op_none]
opcode_idx: [0x16]
- sig: u64toi32
acc: inout:u64->i32
prefix: cast
format: [pref_op_none]
opcode_idx: [0x17]
- sig: u64tou32
acc: inout:u64->u32
prefix: cast
format: [pref_op_none]
opcode_idx: [0x18]
- title: Load from array
description: >
Load an element from array using accumulator as an index and puts it into accumulator.
If element size is smaller then 32 bits, it will be zero or sign extended (depending on bytecode)
to i32.
verification:
- v1_array_type
- acc_i32
properties:
- acc_read
- acc_write
exceptions:
- x_null
- x_bounds
pseudo: |
if vs == null then
throw NullPointerException
end
if acc < 0 || acc >= len(vs) then
throw ArrayIndexOutOfBoundsException
end
if op == ldarr.8 then
acc = i8toi32(vs[acc])
else if op == ldarru.8 then
acc = u8toi32(vs[acc])
else if op == ldarr.16 then
acc = i16toi32(vs[acc])
else if op == ldarru.16 then
acc = u16toi32(vs[acc])
else
acc = vs[acc]
end
semantics: |-
acc <~ (@Vs) [@acc]
instructions:
- sig: ldarr.8 v:in:i8[]
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x67]
- sig: ldarru.8 v:in:u8[]
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x68]
- sig: ldarr.16 v:in:i16[]
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x69]
- sig: ldarru.16 v:in:u16[]
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x6a]
- sig: ldarr v:in:i32[]
acc: inout:i32
format: [op_v_8]
opcode_idx: [0x6b]
- sig: ldarr.64 v:in:i64[]
acc: inout:i32->i64
format: [op_v_8]
opcode_idx: [0x6c]
- sig: fldarr.32 v:in:f32[]
acc: inout:i32->f32
format: [op_v_8]
opcode_idx: [0x6d]
properties: [acc_read, acc_write, float]
- sig: fldarr.64 v:in:f64[]
acc: inout:i32->f64
format: [op_v_8]
opcode_idx: [0x6e]
properties: [acc_read, acc_write, float]
- sig: ldarr.obj v:in:ref[]
acc: inout:i32->ref
format: [op_v_8]
opcode_idx: [0x6f]
- title: Store to array
description: >
Store accumulator content into array slot pointed by index.
If size of element to store is less than 32, accumulator content will be truncated
to storage size before storing.
verification:
- v1_array_type
- v2_i32
- acc_type
properties:
- acc_read
exceptions:
- x_null
- x_bounds
- x_store
pseudo: |
if vs1 == null then
throw NullPointerException
end
if vs2 < 0 || vs2 >= len(vs1) then
throw ArrayIndexOutOfBoundsException
end
if op == starr.obj && !has_type(acc, component_type(vs1))
throw ArrayStoreException
end
if op == starr.8 then
vs1[vs2] = truncateto8(acc)
else if op == starr.16 then
vs1[vs2] = truncateto16(acc)
else
vs1[vs2] = acc
end
semantics: |-
(@Vs1) <~ (@Vs1) [ (@Vs2) ] <- (@acc)
instructions:
- sig: starr.8 v1:in:i8[], v2:in:i32
acc: in:i8
format: [op_v1_4_v2_4]
opcode_idx: [0x70]
- sig: starr.16 v1:in:i16[], v2:in:i32
acc: in:i16
format: [op_v1_4_v2_4]
opcode_idx: [0x71]
- sig: starr v1:in:i32[], v2:in:i32
acc: in:i32
format: [op_v1_4_v2_4]
opcode_idx: [0x72]
- sig: starr.64 v1:in:i64[], v2:in:i32
acc: in:i64
format: [op_v1_4_v2_4]
opcode_idx: [0x73]
- sig: fstarr.32 v1:in:f32[], v2:in:i32
acc: in:f32
format: [op_v1_4_v2_4]
opcode_idx: [0x74]
properties: [acc_read, float]
- sig: fstarr.64 v1:in:f64[], v2:in:i32
acc: in:f64
format: [op_v1_4_v2_4]
opcode_idx: [0x75]
properties: [acc_read, float]
- sig: starr.obj v1:in:ref[], v2:in:i32
acc: in:ref
format: [op_v1_4_v2_4]
opcode_idx: [0x76]
- title: Array length
description: Get length of an array and put it into accumulator.
properties:
- acc_write
verification:
- v1_array
exceptions:
- x_null
pseudo: |
if x == null then
throw NullPointerException
end
acc = len(vs)
semantics: |-
acc <~ array_length(@Vs)
instructions:
- sig: lenarr v:in:top[]
acc: out:i32
format: [op_v_8]
opcode_idx: [0x77]
- title: Create new array
description: >
Create a new single-dimensional array of given type and size and put a reference to it into register.
Elements of array are initialized to a default value, i.e. 0 for primitive types and null for objects.
verification:
- type_id_array
- v2_i32
exceptions:
- x_negsize
- x_oom
properties:
- acc_none
- type_id
- language_type
pseudo: |
if v2 < 0 then
throw NegativeArraySizeException
end
type = resolve(type_id)
v1 = new_array(v2, type)
if v1 == null then
throw OutOfMemoryError
end
semantics: |-
@V1 <~ new_array(TypeId, @V2)
instructions:
- sig: newarr v1:out:ref, v2:in:i32, type_id
acc: none
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x78]
- title: Create new object
description: |
Resolve class type from type_id, allocate memory for an object, initialize its fields with their
default values (i.e. 0 for primitives and null for objects) and put a reference to the newly created
object into register. The object should be initialized by calling initialization method before
further usage.
verification:
- type_id_object
exceptions:
- x_oom
properties:
- acc_none
- type_id
pseudo: |
type = resolve(type_id)
v = new(type)
if v == null then
throw OutOfMemoryError
end
semantics: |-
skip
instructions:
- sig: newobj v:out:ref, type_id
acc: none
format: [op_v_8_id_16]
opcode_idx: [0x79]
- title: Create new object and call initializer
description: >
Resolve class type from initializer method_id, allocate memory for an object, initialize its fields with their
default values (i.e. 0 for primitives and null for objects), call specified initializer and put a reference to
the newly created object into accumulator. method_id should resolve to an initializer.
Non-range instructions can be used to pass up to 4 arguments.
Unused register slot values will be discarded and corresponding registers will not be passed to initializer.
For methods with more arguments range kinds of instruction are to be used, which takes the needed number of
arguments starting from 'vs' register.
verification:
- method_id_non_static
- method_id_accessible
- method_init_obj
- compatible_arguments
exceptions:
- x_abstract
- x_oom
properties:
- acc_write
- method_id
pseudo: |
init, type = resolve(method_id)
acc = new(type)
if acc == null then
throw OutOfMemoryError
end
init(acc, args)
semantics: |-
skip
instructions:
- sig: initobj.short method_id, v1:in:none, v2:in:none
acc: out:ref
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x7a]
- sig: initobj method_id, v1:in:none, v2:in:none, v3:in:none, v4:in:none
acc: out:ref
format: [op_v1_4_v2_4_v3_4_v4_4_id_16]
opcode_idx: [0x7b]
- sig: initobj.range method_id, v:in:none
acc: out:ref
format: [op_v_8_id_16]
opcode_idx: [0x7c]
- title: Get field from object to accumulator
description: >
Get field value from an object by field id and put it into accumulator.
For non-object variant, the size of the field is determined by the field_id,
most significant bits are sign or unsigned extended based on the field type to fit accumulator size.
If field type size is less than 32, then loaded value is sign or zero extended to i32 depending on field type.
verification:
- v1_object
- field_id_non_static
- field_id_size
properties:
- acc_write
- field_id
exceptions:
- x_null
pseudo: |
if vs == null then
throw NullPointerException
end
field = resolve(field_id)
if op == ldobj and size(field) < 32 then
acc = extendto32(vs.get(field))
else
acc = vs.get(field)
end
semantics: |-
skip
instructions:
- sig: ldobj v:in:ref, field_id
acc: out:b32
format: [op_v_8_id_16]
opcode_idx: [0x7d]
- sig: ldobj.64 v:in:ref, field_id
acc: out:b64
format: [op_v_8_id_16]
opcode_idx: [0x7e]
- sig: ldobj.obj v:in:ref, field_id
acc: out:ref
format: [op_v_8_id_16]
opcode_idx: [0x7f]
- title: Store accumulator content into object field
description: >
Store accumulator content into object field by field_id. For non-object variant the size of actually stored
value is determined by field_id, other accumulator bits are discarded.
If field type size is less than 32, accumulator content will be truncated to storage size before storing.
verification:
- v1_object
- field_id_non_static
- field_id_size
- acc_type
properties:
- acc_read
- field_id
exceptions:
- x_null
pseudo: |
if vs == null then
throw NullPointerException
end
field = resolve(field_id)
if op == stobj and size(field) < 32 then
vs.set(field, truncate(field, acc))
else
vs.set(field, acc)
end
semantics: |-
skip
instructions:
- sig: stobj v:in:ref, field_id
acc: in:b32
format: [op_v_8_id_16]
opcode_idx: [0x80]
- sig: stobj.64 v:in:ref, field_id
acc: in:b64
format: [op_v_8_id_16]
opcode_idx: [0x81]
- sig: stobj.obj v:in:ref, field_id
acc: in:ref
format: [op_v_8_id_16]
opcode_idx: [0x82]
- title: Get field from object to register
description: >
Get field value from an object by field id and put it into register.
For non-object variant, the size of the field is determined by the field_id,
most significant bits are sign or unsigned extended based on the field type to fit register size.
If field type size is less than 32, then loaded value is sign or zero extended to i32 depending on field type.
If field type is f32, load will implicitly convert value into f64 type.
verification:
- v2_object
- field_id_non_static
- field_id_size
properties:
- acc_none
- field_id
exceptions:
- x_null
pseudo: |
if v2 == null then
throw NullPointerException
end
field = resolve(field_id)
if op == ldobj and size(field) < 32 then
v1 = extendto32(v2.get(field))
else if type(field) == f32 then
v1 = f32tof64(v2.get(field))
else
v1 = v2.get(field)
end
semantics: |-
skip
instructions:
- sig: ldobj.v v1:out:i32, v2:in:ref, field_id
acc: none
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x83]
- sig: ldobj.v.64 v1:out:b64, v2:in:ref, field_id
acc: none
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x84]
- sig: ldobj.v.obj v1:out:ref, v2:in:ref, field_id
acc: none
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x85]
- title: Store register content into object field
description: >
Store register content into object field by field_id. For non-object variant the size of actually stored
value is determined by field_id, other register bits are discarded.
If field type size is less than 32, register content will be truncated to storage size before storing.
verification:
- v1_type
- v2_object
- field_id_non_static
- field_id_size
properties:
- acc_none
- field_id
exceptions:
- x_null
pseudo: |
if v2 == null then
throw NullPointerException
end
field = resolve(field_id)
if op == stobj and size(field) < 32 then
v2.set(field, truncate(field, v1))
else
v2.set(field, v1)
end
semantics: |-
skip
instructions:
- sig: stobj.v v1:in:b32, v2:in:ref, field_id
acc: none
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x86]
- sig: stobj.v.64 v1:in:b64, v2:in:ref, field_id
acc: none
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x87]
- sig: stobj.v.obj v1:in:ref, v2:in:ref, field_id
acc: none
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x88]
- title: Get static field
description: >
Get static field value by field_id and put it into accumulator.
For non-object variant, the size of the field is determined by the field_id,
most significant bits are sign or unsigned extended based on the field type to fit accumulator size.
If field size is less then 32, result will be sign or unsigned extended to i32 depedning on field type.
verification:
- field_id_static
- field_id_size
properties:
- acc_write
- field_id
exceptions:
- x_init
pseudo: |
field = resolve(field_id)
if op == ldstatic and size(field) < 32 then
acc = extendto32(get_static(field))
else
acc = get_static(field)
end
semantics: |-
skip
instructions:
- sig: ldstatic field_id
acc: out:b32
format: [op_id_16]
opcode_idx: [0x89]
- sig: ldstatic.64 field_id
acc: out:b64
format: [op_id_16]
opcode_idx: [0x8a]
- sig: ldstatic.obj field_id
acc: out:ref
format: [op_id_16]
opcode_idx: [0x8b]
- title: Store to static field
description: >
Store accumulator content into static field by field_id. For non-object variant the size of actually stored
value is determined by field_id, other accumulator bits are discarded.
If field type size is less than 32, then accumulator content will be trunctated to field size before storing.
verification:
- field_id_static
- field_id_size
- acc_type
properties:
- acc_read
- field_id
exceptions:
- x_init
pseudo: |
field = resolve(field_id)
if op == ststatic and size(field) < 32 then
set_static(field, truncate(field, acc))
else
set_static(field, acc)
end
semantics: |-
skip
instructions:
- sig: ststatic field_id
acc: in:b32
format: [op_id_16]
opcode_idx: [0x8c]
- sig: ststatic.64 field_id
acc: in:b64
format: [op_id_16]
opcode_idx: [0x8d]
- sig: ststatic.obj field_id
acc: in:ref
format: [op_id_16]
opcode_idx: [0x8e]
- title: Return value from method
description: >
Return from the current method, i.e. restore the frame of method invoker and return control to the
invoker. Return value should be in accumulator.
verification:
- acc_return_type
exceptions:
- x_none
properties:
- acc_read
- return
pseudo: |
return acc
semantics: |-
perform_return(@acc)
instructions:
- sig: return
acc: in:i32
format: [op_none]
opcode_idx: [0x8f]
- sig: return.64
acc: in:b64
format: [op_none]
opcode_idx: [0x90]
- sig: return.obj
acc: in:ref
format: [op_none]
opcode_idx: [0x91]
- title: Return from a void method
description: >
Return from the current method, i.e. restore the frame of method invoker and return control to the invoker.
Caller should treat accumulator value as undefined and cannot use it until accumulator definition in the caller
frame.
verification:
- none
exceptions:
- x_none
properties:
- acc_none
- return
pseudo: |
return
semantics: |-
perform_return_void()
instructions:
- sig: return.void
acc: none
format: [op_none]
opcode_idx: [0x92]
- title: Throw exception
description: >
Throw an exception located in register. The current method is searched for the first exception handler that
matches the class of exception. If exception handler is found, control is passed to the exception handler. If no
exception handler is found, the frame of invoker is restored. If such frame exists, the exception is re-thrown.
If no such frame exists, the current VM thread exits.
verification:
- v1_throw_type
exceptions:
- x_null
properties:
- acc_none
pseudo: |
if vs == null then
throw NullPointerException
end
throw vs
semantics: |-
skip
instructions:
- sig: throw v:in:ref
acc: none
format: [op_v_8]
opcode_idx: [0x93]
- title: Check cast
description: >
Resolve object type by specified id and if an object in accumulator can be cast to the resolved type,
accumulator content remains unchanged. Otherwise ClassCastException is thrown.
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
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
T array elements.
'null' object reference can be cast to every type.
verification:
- type_id_any_object
- acc_obj_or_null
exceptions:
- x_cast
properties:
- acc_read
- type_id
pseudo: |
type = resolve(type_id)
if acc != null and !has_type(acc, type) then
throw ClassCastException
end
semantics: |-
skip
instructions:
- sig: checkcast type_id
acc: in:ref
format: [op_id_16]
opcode_idx: [0x94]
- title: Is instance
description: >
Resolve object type by specified id and if an object in accumulator is an instance of the resolved type,
put 1 into accumulator, otherwise put 0.
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
type in type hierarchy or T is such array that O array elements are the same or subtype of T array elements.
'null' object is not an instance of any class.
verification:
- type_id_any_object
- acc_obj_or_null
exceptions:
- x_classdef
properties:
- acc_read
- acc_write
- type_id
pseudo: |
type = resolve(type_id)
if acc == null or !has_type(acc, type) then
acc = 0
else
acc = 1
end
semantics: |-
skip
instructions:
- sig: isinstance type_id
acc: inout:ref->i32
format: [op_id_16]
opcode_idx: [0x95]
- title: Static call
description: >
Call indicated static method, i.e. create new frame, pass values of arguments and
continue execution from the first instruction of a method.
Callee should treat accumulator value as undefined and cannot use it until accumulator
definition in the new frame.
Result (if any) is returned in accumulator (see 'Calling sequence' chapter for more details).
Method, its class and the number of argument is resolved by given method_id in
runtime constant-pool.
Arguments are passed in source registers in the same order as in method signature.
Non-range instructions can be used to pass up to 4 arguments (unused register slot values will
be discarded and corresponding registers will not be passed to the callee).
For methods with more arguments range kind of instruction is to be used, which takes the needed number
of arguments starting from 'vs' register.
In dynamically-typed language context accept 'any' values in source registers.
verification:
- method_id_static
- method_id_non_abstract
- compatible_arguments
properties:
- acc_write
- method_id
- call
- maybe_dynamic
exceptions:
- x_none
pseudo: |
method = resolve(method_id)
acc = call(method, args)
semantics: |-
cases
when Op == "call.short" do perform_call_fixed_args( MethodId, [[ @Vs1, @Vs2 ]] ) end when;
when Op == "call" do perform_call_fixed_args( MethodId, [[ @Vs1, @Vs2, @Vs3, @Vs4 ]] ) end when;
when Op == "call.range" do perform_call_range_fixed_args( MethodId, Vs ) end when
else raise exception(UndefinedSemantics)
undefined raise exception(InternalError)
end cases
instructions:
- sig: call.short method_id, v1:in:top, v2:in:top
acc: out:top
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x96]
- sig: call method_id, v1:in:top, v2:in:top, v3:in:top, v4:in:top
acc: out:top
format: [op_v1_4_v2_4_v3_4_v4_4_id_16]
opcode_idx: [0x97]
- sig: call.range method_id, v:in:top
acc: out:top
format: [op_v_8_id_16]
opcode_idx: [0x98]
- title: Static call with accumulator as input
description: >
Call indicated static method, i.e. create new frame, pass values of arguments and
continue execution from the first instruction of a method.
Callee should treat accumulator value as undefined and cannot use it until accumulator
definition in the new frame.
Result (if any) is returned in accumulator (see 'Calling sequence' chapter for more details).
Method, its class and the number of argument is resolved by given method_id in
runtime constant-pool.
Arguments are passed in source registers in the same order as in method signature.
Non-range instructions can be used to pass up to 4 arguments (unused register slot values will
be discarded and corresponding registers will not be passed to the callee).
In dynamically-typed language context accept 'any' values in source registers.
Immediate operand encodes a position starting from 0 on which accumulator is passed.
verification:
- method_id_static
- method_id_non_abstract
- compatible_arguments
properties:
- acc_write
- acc_read
- method_id
- call
- maybe_dynamic
exceptions:
- x_none
pseudo: |
args = []
for (i = 0; i < 4; ++i)
if (i < imm) then
args[i] = regs[i]
else if (i == imm) then
args[i] = acc
else
args[i] = regs[i - 1]
end
end
method = resolve(method_id)
acc = call(method, args)
semantics: |-
skip
instructions:
- sig: call.acc.short method_id, v:in:top, imm:u1
acc: inout:top
format: [op_v_4_imm_4_id_16]
opcode_idx: [0x99]
- sig: call.acc method_id, v1:in:top, v2:in:top, v3:in:top, imm:u2
acc: inout:top
format: [op_v1_4_v2_4_v3_4_imm_4_id_16]
opcode_idx: [0x9a]
- title: Object calls
description: >
Call indicated object method, i.e. create new frame, pass values of arguments and
continue execution from the first instruction of a method.
Callee should treat accumulator value as undefined and cannot use it until accumulator
definition in the new frame.
Result (if any) is returned in accumulator (see 'Calling sequence' chapter for more details).
Method, its class and the number of argument is resolved by given method_id in runtime
constant-pool based on object reference using language-specific semantics (currently only Java
virtual methods are supported, further extensions are TBD).
Object reference is passed in the first source register, arguments are passed starting from
the second source register in the same order as in method signature.
Non-range instructions can be used to pass up to 4 arguments (including object reference).
Unused register slot values will be discarded and corresponding registers will not be
passed to the callee).
For methods with more arguments range kinds of instruction are to be used, which takes
the needed number of arguments starting from 'vs' register (including object reference).
verification:
- method_id_non_static
- compatible_arguments
- method_id_accessible
exceptions:
- x_null
- x_abstract
properties:
- acc_write
- method_id
- call
- call_virt
pseudo: |
if args[0] == null then
throw NullPointerException
end
method = resolve(method_id)
if is_abstract(method) then
throw AbstractMethodError
end
acc = call(method, args)
semantics: |-
skip
instructions:
- sig: call.virt.short method_id, v1:in:top, v2:in:top
acc: out:top
format: [op_v1_4_v2_4_id_16]
opcode_idx: [0x9b]
- sig: call.virt method_id, v1:in:top, v2:in:top, v3:in:top, v4:in:top
acc: out:top
format: [op_v1_4_v2_4_v3_4_v4_4_id_16]
opcode_idx: [0x9c]
- sig: call.virt.range method_id, v:in:top
acc: out:top
format: [op_v_8_id_16]
opcode_idx: [0x9d]
- title: Object calls with accumulator as input
description: >
Call indicated object method, i.e. create new frame, pass values of arguments and
continue execution from the first instruction of a method.
Callee should treat accumulator value as undefined and cannot use it until accumulator
definition in the new frame.
Result (if any) is returned in accumulator (see 'Calling sequence' chapter for more details).
Method, its class and the number of argument is resolved by given method_id in runtime
constant-pool based on object reference using language-specific semantics (currently only Java
virtual methods are supported, further extensions are TBD).
Object reference is passed in the first source register, arguments are passed starting from
the second source register in the same order as in method signature.
Non-range instructions can be used to pass up to 4 arguments (including object reference).
Unused register slot values will be discarded and corresponding registers will not be
passed to the callee).
Immediate operand encodes a position starting from 0 on which accumulator is passed.
verification:
- method_id_non_static
- compatible_arguments
- method_id_accessible
exceptions:
- x_null
- x_abstract
properties:
- acc_write
- acc_read
- method_id
- call
- call_virt
pseudo: |
args = []
for (i = 0; i < 4; ++i)
if (i < imm) then
args[i] = regs[i]
else if (i == imm) then
args[i] = acc
else
args[i] = regs[i - 1]
end
end
if args[0] == null then
throw NullPointerException
end
method = resolve(method_id)
if is_abstract(method) then
throw AbstractMethodError
end
acc = call(method, args)
semantics: |-
skip
instructions:
- sig: call.virt.acc.short method_id, v:in:top, imm:u1
acc: inout:top
format: [op_v_4_imm_4_id_16]
opcode_idx: [0x9e]
- sig: call.virt.acc method_id, v1:in:top, v2:in:top, v3:in:top, imm:u2
acc: inout:top
format: [op_v1_4_v2_4_v3_4_imm_4_id_16]
opcode_idx: [0x9f]
- title: Dynamic move register-to-register
description: >
Move 'any' values between registers
verification:
- valid_in_dynamic_context
exceptions:
- x_none
properties:
- acc_none
- dynamic
pseudo: |
vd = vs
semantics: |
skip
instructions:
- sig: mov.dyn v1:out:any, v2:in:any
acc: none
format: [op_v1_8_v2_8, op_v1_16_v2_16]
opcode_idx: [0xa0, 0xa1]
- title: Dynamic load accumulator from register
description: >
Move 'any' value from register to accumulator
verification:
- valid_in_dynamic_context
exceptions:
- x_none
properties:
- acc_write
- dynamic
pseudo: |
acc = v
semantics: |
skip
instructions:
- sig: lda.dyn v:in:any
acc: out:any
format: [op_v_8]
opcode_idx: [0xa2]
- title: Dynamic store accumulator
description: >
Move 'any' value from accumulator to register
verification:
- valid_in_dynamic_context
exceptions:
- x_none
properties:
- acc_read
- dynamic
pseudo: |
v = acc
semantics: |
skip
instructions:
- sig: sta.dyn v:out:any
acc: in:any
format: [op_v_8]
opcode_idx: [0xa3]
- title: Dynamic load accumulator from immediate
description: >
Move immediate as 'any' value to accumulator
verification:
- valid_in_dynamic_context
exceptions:
- x_none
properties:
- acc_write
- dynamic
pseudo: |
acc = imm
semantics: |
skip
instructions:
- sig: ldai.dyn imm:i32
acc: out:any
format: [op_imm_32]
opcode_idx: [0xa4]
- sig: fldai.dyn imm:f64
acc: out:any
format: [op_imm_64]
opcode_idx: [0xa5]
properties: [acc_write, float, dynamic]
- title: Dynamic return from method
description: >
Return 'any' value in accumulator from method to its caller
verification:
- valid_in_dynamic_context
exceptions:
- x_none
properties:
- acc_read
- dynamic
- return
pseudo: |
return acc
semantics: |
skip
instructions:
- sig: return.dyn
acc: in:any
format: [op_none]
opcode_idx: [0xa6]
- title: Dynamic indirect call
description: >
Call 'any' value that represents a function, i.e. create a new frame, pass values of arguments
and continue execution from the first instruction of a method.
Callee should treat accumulator value as undefined and cannot use it until accumulator
definition in the new frame.
The callee must always return the result in the accumulator.
First source register contains a function 'any' value, and the other imm source registers contain
arguments of a function.
Non-range instructions can be used to pass up to 4 arguments (unused register slot values will
be discarded and corresponding registers will not be passed to the callee).
For methods with more arguments range kind of instruction is to be used, which takes the needed number
of arguments starting from 'v' register.
verification:
- valid_in_dynamic_context
exceptions:
- x_none
properties:
- acc_write
- dynamic
- call
pseudo: |
func, args = source_registers
acc = func(args)
semantics: |
skip
instructions:
- sig: calli.dyn.short imm, v1:in:any, v2:in:any, v3:in:any
acc: out:any
format: [op_imm_4_v1_4_v2_4_v3_4]
opcode_idx: [0xa7]
- sig: calli.dyn imm, v1:in:any, v2:in:any, v3:in:any, v4:in:any, v5:in:any
acc: out:any
format: [op_imm_4_v1_4_v2_4_v3_4_v4_4_v5_4]
opcode_idx: [0xa8]
- sig: calli.dyn.range imm, v:in:any
acc: out:any
format: [op_imm_16_v_16]
opcode_idx: [0xa9]
Reference in New Issue View Git Blame Copy Permalink