# Copyright (c) 2021 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 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 == "u32tou64" do raise exception(WrongRegisterValue) if false that type_of(@acc) is u32; acc <~ u32tou64(@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 when Op == "u64tou8" do raise exception(WrongRegisterValue) if false that type_of(@acc) is u64; acc <~ u64tou8(@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 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 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]