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